SMTSolver (kind2dev@731decdf5fb1.SMTSolver)

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.

exception Killed

Raised by a command to a solver instance whose process was killed from outside, by kill_solvers_of_domain or destroy_all_of_process, when the command fails on the dead process: on a reply cut short or a closed pipe, whatever exception that raised. The solver did not fail on what it was given: its owner is being stopped. A reply the solver gave before it was killed is reported as what it is, an error included.

exception Died of string

Raised by a command to a solver instance whose process is gone although it was not killed from outside -- it crashed, or the out-of-memory killer killed it -- when the command fails on the dead process: on a reply cut short or a closed pipe. As for Killed, the solver did not fail on what it was given. The message says how the process ended, with what it wrote to its standard error.

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. For a solver killed from outside, by kill_solvers_of_domain or destroy_all_of_process, only the pipes to it are left to close. Deleting a solver again does nothing.

val destroy_all : unit -> unit

Destroys all live solver instances owned by the calling domain, and closes the pipes to those of its solvers that were killed from outside.

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 solver_pids_by_domain : unit -> (int * int) list

The live solvers, as the domain that owns each (by its identifier, as for kill_solvers_of_domain) and the identifier of its process.

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

val define_funs_rec : t -> (UfSymbol.t * Var.t list * Term.t) list -> unit

Define a group of (mutually) recursive function symbols, each given with its formal parameters and its body, in a single define-funs-rec command. The bodies may apply any symbol of the group. If none does, the group is not recursive, and each function is defined with define-fun instead.

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

type array_limit = [

| `Raise of int
| `Omit of int

]

How many elements of arrays a model is read with at most:

`Raise n: Too_many_array_elements is raised if the arrays of the model have more than n elements in all;
`Omit n: an array whose elements would take the elements read past n in all is given no values, as an unbounded array is, and the others are read.

exception Too_many_array_elements

Raised by get_var_values for `Raise

val max_array_elements : int

The limit on the array elements of the models of the engines

val get_var_values : 
  ?array_limit:array_limit ->
  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.

The value of an array is read element by element, over the indices its bounds give it: 2^w elements for an index of w bits. With array_limit, the arrays read are limited (see array_limit).

With the theory of arrays, and Flags.Arrays.read_whole, the value of an array is read whole instead, as a term: the solver gives it as a constant array with stores, which is kept in the canonical form of TermLib.canonical_array_value. A value of another form is read element by element.

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 get_term_values_at_once : t -> Term.t list -> (Term.t * Term.t) list

Get the values of the given terms as get_term_values does, but in one query rather than one per term: the values are matched with the terms by their order in the response, which SMT-LIB gives as the order of the terms, whatever form of each term the solver repeats.

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_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