Module Smt2_solver.Solver

Parameters

Signature

type result =
  1. | Sat
  2. | Unsat
  3. | Unknown
type term
type value
type memory
type access =
  1. | Select of term * int
  2. | Store of term
val put : Smt.Suid.t -> Sexpr.Expr.t list -> unit
val set_memory : addr:Z.t -> Z.t -> unit
val neq : term -> Z.t -> unit
val bind : Smt.Suid.t -> Sexpr.Expr.t -> Sexpr.Expr.t list -> term
val get : Sexpr.Expr.t -> term
val check_sat : unit -> result
val get_memory : unit -> memory * access Queue.t
val get_value : term -> value
val assignment : value -> Z.t
val get_at : memory -> value -> Z.t
val succ : value -> value
val close : unit -> unit