sig
module Solver :
sig
type 'a t
val add : 'a Smt.Solver.t -> 'a Syntax.formula list -> unit
val push : 'a Smt.Solver.t -> unit
val pop : 'a Smt.Solver.t -> int -> unit
val reset : 'a Smt.Solver.t -> unit
val check :
'a Smt.Solver.t ->
'a Syntax.formula list -> [ `Sat | `Unknown | `Unsat ]
val to_string : 'a Smt.Solver.t -> string
val get_model :
?symbols:Syntax.symbol list ->
'a Smt.Solver.t ->
[ `Sat of 'a Interpretation.interpretation | `Unknown | `Unsat ]
val get_concrete_model :
'a Smt.Solver.t ->
Syntax.symbol list ->
[ `Sat of 'a Interpretation.interpretation | `Unknown | `Unsat ]
val get_unsat_core :
'a Smt.Solver.t ->
'a Syntax.formula list ->
[ `Sat | `Unknown | `Unsat of 'a Syntax.formula list ]
end
val mk_solver : ?theory:string -> 'a Syntax.context -> 'a Smt.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 ]
end