module Sat: sig .. end
sig
end
Sat solver
This modules instanciates a pure sat solver using integers to represent atomic propositions.
module Expr: sig .. end
The module defining formulas
module Make: functor (Dummy : sigend) -> Solver.S with type St.formula = Expr.t
functor (
Dummy
:
end) -> Solver.S with type St.formula = Expr.t
) ->
Solver.S
with type St.formula = Expr.t
A functor that can generate as many solvers as needed.