Skip to content

Instantly share code, notes, and snippets.

@CodaFi CodaFi/3SAT.swift
Last active Jul 22, 2019

Embed
What would you like to do?
// swift -Xfrontend -debug-constraints
infix operator ^&&^ : LogicalConjunctionPrecedence
infix operator ^||^ : LogicalConjunctionPrecedence
struct T{}
struct F{}
func λ(_ f : (T) -> ()) {
print("true")
f(T())
}
func λ(_ f : (F) -> ()) {
print("false")
f(F())
}
// MARK: Trinary operators
func ^||^(_ : T, _ : T) -> (T) -> T { return { _ in T() } }
func ^||^(_ : T, _ : T) -> (F) -> T { return { _ in T() } }
func ^||^(_ : T, _ : F) -> (T) -> T { return { _ in T() } }
func ^||^(_ : T, _ : F) -> (F) -> T { return { _ in T() } }
func ^||^(_ : F, _ : T) -> (T) -> T { return { _ in T() } }
func ^||^(_ : F, _ : T) -> (F) -> T { return { _ in T() } }
func ^||^(_ : F, _ : F) -> (T) -> T { return { _ in T() } }
func ^||^(_ : F, _ : F) -> (F) -> F { return { _ in F() } }
func ^||^(_ : (T) -> T, _ : T) -> T { return T() }
func ^||^(_ : (T) -> T, _ : F) -> T { return T() }
func ^||^(_ : (T) -> F, _ : T) -> T { return T() }
func ^||^(_ : (T) -> F, _ : F) -> T { return T() }
func ^||^(_ : (F) -> T, _ : T) -> T { return T() }
func ^||^(_ : (F) -> T, _ : F) -> T { return T() }
func ^||^(_ : (F) -> F, _ : T) -> T { return T() }
func ^||^(_ : (F) -> F, _ : F) -> F { return F() }
// MARK: Binary operators
func ^&&^(_ : T, _ : T) -> T { return T() }
func ^&&^(_ : T, _ : F) -> F { return F() }
func ^&&^(_ : F, _ : T) -> F { return F() }
func ^&&^(_ : F, _ : F) -> F { return F() }
// MARK: Unary operators
prefix func !(_ : T) -> F { return F() }
prefix func !(_ : F) -> T { return T() }
func assert(true : T) {}
func assert(false : F) {}
λ { x1 in
λ { x2 in
λ { x3 in
assert(true: (x1 ^||^ x2 ^||^ !x3) ^&&^ (x1 ^||^ !x2 ^||^ x3) ^&&^ (!x1 ^||^ !x2 ^||^ x3) ^&&^ (!x1 ^||^ !x2 ^||^ !x3))
}
}
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.