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.