Module SMTSolver

module SMTSolver: sig .. end
High-level methods for an SMT solver
Author(s): Alain Mebsout, Christoph Sticksel

type t 
Type of a solver instance
exception Unknown
Exception raised when the solver returns "unknown" to a check-sat.

Creating and finalizing a solver instance


val create_instance : ?produce_assignments:bool ->
?produce_proofs:bool ->
?produce_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 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 -> SMTExpr.t -> unit
Name a term, convert a term to an SMT expression and assert
val assert_named_term_wr : t -> SMTExpr.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
val get_unsat_core_of_names : t -> Term.t list
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.

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 SMTSolver.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 SMTSolver.check_sat_assuming, but the two continuations can return different values that are wrappen in the SMTSolver.sat_or_unsat type
val check_sat_assuming_tf : t -> Term.t list -> bool
Check satisfiability under assumptions as with SMTSolver.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