Module Solver.BatchSource

Batch is parameterized by the mapping module M implementing Mappings_intf.S. In this mode, the solver delays all interactions with the underlying SMT solver until it becomes necessary.

Parameters

module _ : Mappings_intf.S

Signature

Sourcetype t
Sourcetype solver
Sourceval solver_time : float ref

Time spent inside SMT solver.

Sourceval solver_count : int ref

Number of queries to the SMT solver.

Sourceval pp_statistics : Format.formatter -> t -> unit

Print solver statistics.

Sourceval create : ?params:Params.t -> ?logic:Ty.logic -> unit -> t

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 Solver_intf.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.

Sourceval interrupt : t -> unit

Interrupt solver.

Sourceval clone : t -> t

Clone a given solver.

Sourceval push : t -> unit

Create a backtracking point.

Sourceval pop : t -> int -> unit

pop solver n backtracks n backtracking points.

Sourceval reset : t -> unit

Resets the solver, i.e., remove all assertions from the solver.

Sourceval add : t -> Expr.t list -> unit

Assert one or multiple constraints into the solver.

Sourceval get_assertions : t -> Expr.t list

The set of assertions in the solver.

check solver es checks the satisfiability of the assertions in the solver using the assumptions in es.

Raises Unknown if the SMT solver returns unknown.

Sourceval get_value : t -> Expr.t -> Expr.t

get_value solver e get an expression denoting the model value of a given expression.

Requires that the last check query returned true.

Sourceval model : ?symbols:Symbol.t list -> t -> Model.t option

The model of the last check.

The result is None if check was not invoked before, or its result was not Satisfiable.