package encoding

You can search for identifiers within the package.

in-package search v0.2.0

Legend:
Library
Module
Module type
Parameter
Class
Class type

type t

type solver

val solver_time : float ref

Time spent inside SMT solver.

val solver_count : int ref

Number of queries to the SMT solver.

val create : ?params:Params.t -> unit -> t

Create a new solver.

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

Checks the satisfiability of the assertions.

Raises Unknown if 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.