msat
Library containing a SAT solver that can be parametrized by a theory
1024" x-on:close-sidebar="sidebar=window.innerWidth > 1024 && true">
package msat
-
msat
-
-
msat.backend
-
-
msat.backtrack
-
msat.tseitin
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
Library msat.tseitin
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
.
ON THIS PAGE
No table of contents