Module SMTSolver

High-level methods for an SMT solver

type t

Type of a solver instance

exception Unknown

Exception raised when the solver returns "unknown" to a check-sat.

exception Timeout
exception Exiting

Exception raised by create_instance when the process is exiting. No solver can be created from then on: the ones that exist have been killed, and a new one would be left running.

Creating and finalizing a solver instance

val create_instance : ?timeout:int -> ?produce_models:bool -> ?produce_proofs:bool -> ?produce_unsat_cores:bool -> ?produce_unsat_assumptions:bool -> ?minimize_cores:bool -> ?produce_interpolants:bool -> TermLib.logic -> Flags.Smt.solver -> t

Create a new instance of an SMT solver of the given kind and with the given flags.

  • raises Exiting

    if the process is exiting, in which case no solver is left running.

val set_shutting_down : bool -> unit

Set while the supervisor is terminating the engines of an analysis: solver instances are then killed outright instead of shut down gracefully.

val delete_instance : t -> unit

Delete an instance of an SMT solver

val destroy_all : unit -> unit

Destroys all live solver instances owned by the calling domain.

val destroy_all_of_process : unit -> unit

Destroys every live solver instance of the whole process and bars any further one, so that no solver outlives Kind 2. Only for final cleanup before the process exits: create_instance raises Exiting once this has been called.

val kill_solvers_of_domain : int -> unit

Kills the solver processes owned by the given domain (as returned by (Domain.self () :> int) in that domain) without interacting with them. Used by the supervisor to unblock an engine domain stuck in a solver call.

val id_of_instance : t -> int

Return the unique identifier of the solver instance

Declarations

val declare_sort : t -> Type.t -> unit

Define uninterpreted sort

val declare_fun : t -> UfSymbol.t -> unit

Define uninterpreted symbol

val define_fun : t -> UfSymbol.t -> Var.t list -> Term.t -> unit

Define uninterpreted symbol

Primitives

val assert_expr : t -> SMTExpr.t -> unit

Assert an SMT expression in the current context

val assert_soft_expr : t -> SMTExpr.t -> int -> unit

Assert-soft an SMT expression in the current context

val assert_term : t -> Term.t -> unit

Convert a term to an SMT expression and assert

val assert_soft_term : t -> Term.t -> int -> unit

Convert a term to an SMT expression and assert-soft

val assert_named_term : t -> Term.t -> unit

Name a term, convert a term to an SMT expression and assert

val assert_named_term_wr : t -> Term.t -> string

Name a term, convert a term to an SMT expression and assert, and return the name

val push : ?n:int -> t -> unit

Push a new scope to the context stack

val pop : ?n:int -> t -> unit

Pop one scope from the context stack

val check_sat : ?timeout:int -> t -> bool

Check satisfiability of the current context

The optional parameter timeout limits the maximum runtime to the given number of milliseconds.

val get_model : t -> Model.t

Return a model of the current context if satisfiable

val get_var_values : t -> LustreExpr.expr LustreExpr.bound_or_fixed list StateVar.StateVarHashtbl.t -> Var.t list -> Model.t

Return a values of the terms in the current context if satisfiable

val get_unsat_core_of_names : t -> Term.t list

Return an unsatisfiable core of named expressions if the current context is unsatisfiable. Interpret unsatisfiable core as names and return corresponing terms

val get_unsat_core_lits : t -> Term.t list

Interpret unsatisfiable core as literals and return as terms

Higher-level functions

val check_sat_assuming : t -> (t -> 'a) -> (t -> 'a) -> Term.t list -> 'a

Checks satisfiability of the current context assuming the given list of literals, and evaluate one of two continuation functions depending on the result

check_sat_assuming s t f l assumes each of the literals in l to be true, and checks satisfiablilty of the context of the SMT solver instance s. If the solver returns satisfiable, the continuation t is evaluated, and if the solver returns unsatisfiable, the continuation f is evaluated.

Important: If a solver does not support check-sat with assumptions, it will be simulated by checking satisfiability on a new context level with the literals asserted. This context is removed after the continuations have been evaluated, hence all operations performed in the continuations affecting the context will be undone upon return from this function. Do not rely on context-modifying operations in the continuations being persistent, and keep the continuations as short as possible. Moreover, any call to get_unsat_core_lits should be done INSIDE the continutation if_unsat, and NOT in AFTER the call to check_sat_assuming.

The list l should contain only positive Boolean constants, although this is not enforced. If the solver does not support the check-sat-assuming command it is simulated by asserting the literals on a new context.

val check_sat_and_get_term_values : t -> (t -> (Term.t * Term.t) list -> 'a) -> (t -> 'a) -> Term.t list -> 'a

Checks satisfiability of the current context, and evaluate one of two continuation functions depending on the result

check_sat_and_get_term_values s t f l checks satisfiablilty of the context of the SMT solver instance s. If the solver returns satisfiable, the continuation t is evaluated with the values of the terms of l, and if the solver returns unsatisfiable, the continuation f is evaluated.

val get_term_values : t -> Term.t list -> (Term.t * Term.t) list

Get the values of the given terms in the current context. The context must be satisfiable, as after a check_sat that returned true.

val check_sat_assuming_and_get_term_values : t -> (t -> (Term.t * Term.t) list -> 'a) -> (t -> 'a) -> Term.t list -> Term.t list -> 'a

Check satisfiability under assumptions as with check_sat_assuming, but if the solver returns satisfiable, the values of the terms in the current context are given to the continuation t as its second argument

type ('a, 'b) sat_or_unsat =
  1. | Sat of 'a
  2. | Unsat of 'b

Alternative between type 'a and 'b

val check_sat_assuming_ab : t -> (t -> 'a) -> (t -> 'b) -> Term.t list -> ('a, 'b) sat_or_unsat

Check satisfiability under assumptions as with check_sat_assuming, but the two continuations can return different values that are wrappen in the sat_or_unsat type

val check_sat_assuming_tf : t -> Term.t list -> bool

Check satisfiability under assumptions as with check_sat_assuming, but return true or false without continuations as arguments

val execute_custom_command : t -> string -> SMTExpr.custom_arg list -> int -> SolverResponse.custom_response

Execute the a custom command with the given arguments, and expect the given number of S-expressions as a result

val execute_custom_check_sat_command : string -> t -> SolverResponse.check_sat_response

Execute the a custom command in place of check-sat

Utility functions

val converter : t -> (module SMTExpr.Conv)
val kind : t -> Flags.Smt.solver
val trace_comment : t -> string -> unit

Output a comment into the trace

val get_interpolants : t -> SMTExpr.custom_arg list -> SMTExpr.t list
val get_qe_interpolants : bool -> t -> Term.t list -> Term.t list
val get_qe_expr : t -> SMTExpr.t -> Term.t list

Apply quantifier elimination to a SMTExpr

val get_qe_term : t -> Term.t -> Term.t list

Apply quantifier elimination to a term

val simplify_expr : t -> SMTExpr.t -> Term.t

Simplify a SMTExpr

val simplify_term : t -> Term.t -> Term.t

Simplify a term