Parameter Make.Solver

type t

The type of solvers.

type solver

The type of underlying solver instances.

val solver_time : float Smtml_prelude.ref

solver_time tracks the time spent inside the SMT solver.

val solver_count : int Smtml_prelude.ref

solver_count tracks the number of queries made to the SMT solver.

val pp_statistics : t Fmt.t

pp_statistics fmt solver pretty-prints solver statistics using the formatter fmt.

val create : ?params:Params.t -> ?logic:Logic.t -> 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 Logic.t and is used to set the theory of the assertions used. When the underlying theory is known, setting this parameter can improve solver performance. The default logic is ALL.
val interrupt : t -> unit

interrupt solver interrupts the current solver operation.

val was_interrupted : t -> bool

was_interrupted solver returns true if the interrupt solver was called.

val clone : t -> t

clone solver creates a copy of the solver solver.

val push : t -> unit

push solver creates a backtracking point in the solver solver.

val pop : t -> int -> unit

pop solver n backtracks n backtracking points in the solver solver.

val reset : t -> unit

reset solver resets the solver solver, removing all assertions.

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

add solver exprs asserts one or multiple constraints exprs into the solver solver.

val add_set : t -> Expr.Set.t -> unit

add_set solver set asserts constraints from the set set into the solver solver.

val get_assertions : t -> Expr.t list

get_assertions solver retrieves the set of assertions in the solver solver.

  • deprecated Please use 'get_statistics' instead
val get_statistics : t -> Statistics.t

get_statistics solver retrieves statistics from the solver solver.

val check : t -> Expr.t list -> [ `Sat | `Unsat | `Unknown ]

check solver es checks the satisfiability of the assertions in the solver solver using the assumptions in es. Returns `Sat, `Unsat, or `Unknown.

val check_set : t -> Expr.Set.t -> [ `Sat | `Unsat | `Unknown ]

check_set solver set checks the satisfiability of the assertions in the solver solver using the assumptions in the set set. Returns `Sat, `Unsat, or `Unknown.

val get_value : t -> Expr.t -> Expr.t

get_value solver expr retrieves an expression denoting the model value of the given expression expr. Requires that the last check query returned `Sat.

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

model ?symbols solver retrieves the model of the last check query. If ?symbols is provided, only the values of the specified symbols are included. Returns None if check was not invoked before or its result was not `Sat.

Not compatible with cached solver mode - use get_sat_model instead

  • see get_sat_model

    For cached solver-compatible alternative

val get_sat_model : ?symbols:Symbol.t list -> t -> Expr.Set.t -> [ `Model of Model.t | `Unsat | `Unknown ]

Compute and retrieve a model for specific constraints.

get_sat_model ?symbols solver exprs performs: 1. check_set with exprs constraints 2. Returns model if result is `Sat

Filters output using ?symbols when provided. Designed for cached solvers.

  • see model

    For non-cached solvers when you have already performed your own check/check_set and want to retrieve the results