package soteria

  1. Overview
  2. Docs
package soteria
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Z3.Make

Create a Z3 solver module from a value type. It can be configured, see Config.

Parameters

module Value : Value.S

Signature

type t

The solver state type.

include Soteria.Soteria_std.Reversible.Mutable with type t := t
val init : unit -> t

Create a new reversible state initialized with the default value.

val backtrack_n : t -> int -> unit

Remove the last n checkpoints from state.

val save : t -> unit

Save the current state as a new checkpoint.

val reset : t -> unit

Clear all checkpoints and reset to the default value.

type value = Value.t

The type of symbolic expressions.

type ty = Value.ty

The type of value types (for variable declarations).

val add_constraint : t -> value -> unit

add_constraint solver v adds constraint v to the solver.

val check_sat : t -> Soteria.Symex.Solver_result.t

check_sat solver checks satisfiability of current constraints. This may return Symex.Solver_result.t.Unknown if the solver cannot determine satisfiability or if it times out.

val declare_var : t -> Soteria.Symex.Var.t -> ty -> unit

declare_var solver var ty declares a variable with type ty.

val push : t -> int -> unit

push solver n pushes n levels onto the assertion stack.

Constraints added after push can be removed by pop.

val pop : t -> int -> unit

pop solver n pops n levels from the assertion stack.

Removes all constraints added since the corresponding push.

val get_model : t -> Smt.sexp option

Gets the model from the last satisfiability check, if available.