package encoding

  1. Overview
  2. Docs

The Incremental module, akin to Batch, presents a solver parameterized by the mapping module M. In this mode, the Incremental solver engages with the underlying SMT solver in nearly every interaction.

Parameters

Signature

type t
type solver
val solver_time : float Stdlib.ref

Time spent inside SMT solver.

val solver_count : int Stdlib.ref

Number of queries to the SMT solver.

val pp_statistics : Stdlib.Format.formatter -> t -> unit

Print solver statistics.

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

val interrupt : unit -> unit

Interrupt solver.

val clone : t -> t

Clone a given solver.

val push : t -> unit

Create a backtracking point.

val pop : t -> int -> unit

pop solver n backtracks n backtracking points.

val reset : t -> unit

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

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

Assert one or multiple constraints into the solver.

val get_assertions : t -> Expr.t list

The set of assertions in the solver.

val check : t -> Expr.t list -> bool

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.

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

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

OCaml

Innovation. Community. Security.