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.backend
module type S = Backend_intf.S
Interface for exporting proofs.
module type Arg = sig ... end
Term printing for DOT
module Default
(S : Msat.S) :
Arg
with type atom := S.atom
and type hyp := S.clause
and type lemma := S.clause
and type assumption := S.clause
Provides a reasonnable default to instantiate the Make
functor, assuming the original printing functions are compatible with DOT html labels.
module Make
(S : Msat.S)
(A :
Arg
with type atom := S.atom
and type hyp := S.clause
and type lemma := S.clause
and type assumption := S.clause) :
S with type t := S.proof
Functor for making a module to export proofs to the DOT format.
module Simple
(S : Msat.S)
(A :
Arg
with type atom := S.formula
and type hyp = S.formula list
and type lemma := S.lemma
and type assumption = S.formula) :
S with type t := S.proof
Functor for making a module to export proofs to the DOT format. The substitution of the hyp type is non-destructive due to a restriction of destructive substitutions on earlier versions of ocaml.
ON THIS PAGE
No table of contents