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.