Tseitin.Make
Conversion functions from boolean gates to Tseitin form. The first argument to each function is the newly introduced sat literal for this gate, which should be referenced by its fanouts. The return value is the corresponding CNF.
module B : S
val bfalse : B.t -> B.t Base.list Base.list
constant false
val btrue : B.t -> B.t Base.list Base.list
constant true
val bnot : B.t -> B.t -> B.t Base.list Base.list
not
val bwire : B.t -> B.t -> B.t Base.list Base.list
wire (copy input to output)
val bnor : B.t -> B.t Base.list -> B.t Base.list Base.list
n-input not-or
val bor : B.t -> B.t Base.list -> B.t Base.list Base.list
n-input or
val bnand : B.t -> B.t Base.list -> B.t Base.list Base.list
n-input not-and
val band : B.t -> B.t Base.list -> B.t Base.list Base.list
n-input and
val bxor : B.t -> B.t -> B.t -> B.t Base.list Base.list
2-input xor