Module Smt

module Smt: sig .. end
Common interface for SMT solvers

module Solver: sig .. end
val mk_solver : ?theory:string -> 'a Syntax.context -> 'a Solver.t
val get_model : ?symbols:Syntax.symbol list ->
'a Syntax.context ->
'a Syntax.formula ->
[ `Sat of 'a Interpretation.interpretation | `Unknown | `Unsat ]
val get_concrete_model : 'a Syntax.context ->
Syntax.symbol list ->
'a Syntax.formula ->
[ `Sat of 'a Interpretation.interpretation | `Unknown | `Unsat ]
val is_sat : 'a Syntax.context -> 'a Syntax.formula -> [ `Sat | `Unknown | `Unsat ]
val entails : 'a Syntax.context ->
'a Syntax.formula -> 'a Syntax.formula -> [ `No | `Unknown | `Yes ]
val equiv : 'a Syntax.context ->
'a Syntax.formula -> 'a Syntax.formula -> [ `No | `Unknown | `Yes ]
val affine_interpretation : 'a Syntax.context ->
'a Interpretation.interpretation ->
'a Syntax.formula ->
[ `Sat of 'a Interpretation.interpretation | `Unknown | `Unsat ]
Given an a model m and a formula phi such that m |= phi, attempt to compute a new interpretation m' such that m' |= phi, m(x) = m'(x) for all constant symbols and non-real functions, and for all real functions f, m'(f) is affine. Return `Unsat if there is no such m', or `Unknown if the status of the associated SMT query could not be determined.