Module type SolverSig.S

The functor Create creates a new instance of the SMT solver with paramters passed as its arguments. The parameter argument P conataints a unique identifier id, initialized to the logic l and produces assignments if the optional labelled argument produce_assignments is true, proofs if produce_proofs is true and unsatisfiable cores if produce_cores is true.