Module Sat

module Sat: 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 : sig
end) -> Solver.S  with type St.formula = Expr.t

A functor that can generate as many solvers as needed.