-
msat
-
-
msat.backend
-
-
msat.backtrack
-
msat.tseitin
Library
Module
Module type
Parameter
Class
Class type
The exposed interface of Tseitin's CNF conversion.
CNF conversion
This modules converts arbitrary boolean formulas into CNF.
The type of arbitrary boolean formulas. Arbitrary boolean formulas can be built using functions in this module, and then converted to a CNF, which is a list of clauses that only use atomic formulas.
val f_true : t
The true
formula, i.e a formula that is always satisfied.
val f_false : t
The false
formula, i.e a formula that cannot be satisfied.
Creates the conjunction of a list of formulas. An empty conjunction is always satisfied.
Creates the disjunction of a list of formulas. An empty disjunction is never satisfied.
make_cnf f
returns a conjunctive normal form of f
under the form: a list (which is a conjunction) of lists (which are disjunctions) of atomic formulas.
val pp : Format.formatter -> t -> unit
print fmt f
prints the formula on the formatter fmt
.