Solver_intf.EXPR
Formulas and Terms required for mcSAT
type proof
An abstract type for proofs
module Term : sig ... end
module Value : sig ... end
module Formula : FORMULA