val solver_time : float Smtml_prelude.refTime spent inside SMT solver.
val solver_count : int Smtml_prelude.refNumber of queries to the SMT solver.
val pp_statistics : t Smtml_prelude.Fmt.tPrint solver statistics.
create ?params ?logic () creates a new solver.
?params is of type Params.t and is used to modify/set parameters inside the solver.
?logic is of type Ty.logic and is used to set the theory of the assertions used. When knowing what the underlying theory is going to be, setting this parameter can help the SMT solver be more performant. The default logic is unknown_theory.
val interrupt : t -> unitInterrupt solver.
val push : t -> unitCreate a backtracking point.
val pop : t -> int -> unitpop solver n backtracks n backtracking points.
val reset : t -> unitResets the solver, i.e., remove all assertions from the solver.
val add_set : t -> Expr.Set.t -> unitSame as add but receives and Expr.Set.t
The set of assertions in the solver.
val get_statistics : t -> Statistics.tval check : t -> Expr.t list -> Solver_intf.satisfiabilitycheck solver es checks the satisfiability of the assertions in the solver using the assumptions in es.
val check_set : t -> Expr.Set.t -> Solver_intf.satisfiabilitySame as check but receives an Expr.Set.t
get_value solver e get an expression denoting the model value of a given expression.
Requires that the last check query returned true.