Module `YicesNative`

An interface to the Yices SMT solver in native format.

Use this module as input to the SMTSolver.Make functor

include SolverSig.S

module Create : functor (P : SolverSig.Params) -> SolverSig.Inst: 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.