Module `SMTSolver`

High-level methods for an SMT solver

author: Alain Mebsout, Christoph Sticksel, Daniel Larraz

type t: Type of a solver instance

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

exception Timeout

Creating and finalizing a solver instance

val create_instance : ?⁠timeout:int -> ?⁠produce_assignments:bool -> ?⁠produce_proofs:bool -> ?⁠produce_cores: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

val delete_instance : t -> unit: Delete an instance of an SMT solver

val destroy_all : unit -> unit: Destroys all live solver instances.

val delete_instance_entries : unit -> unit: Delete instance entries (should be called after forking, on child processes).

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_term : t -> Term.t -> unit: Convert a term to an SMT expression and assert

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 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 = | Sat of 'a | 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_expr : ?⁠simpl:bool -> t -> SMTExpr.t -> Term.t list: Apply quantifier elimination to a SMTExpr

val get_qe_term : ?⁠simpl:bool -> t -> Term.t -> Term.t list: Apply quantifier elimination to a term