Parameter State.F

Parameters

Signature

type result =
  1. | Sat
  2. | Unsat
  3. | Unknown
type term
val put : Binsec.Suid.t -> Sexpr.Expr.t list -> unit
val set_memory : addr:Z.t -> Z.t -> unit
val neq : term -> Z.t -> unit
val bind : Binsec.Suid.t -> Sexpr.Expr.t -> Sexpr.Expr.t list -> term
val iter_free_variables : (string -> Sexpr.Expr.t -> unit) -> unit
val iter_free_arrays : (string -> Sexpr.Memory.t -> unit) -> unit
val get : Sexpr.Expr.t -> term
val check_sat : unit -> result
val get_value : term -> Z.t
val get_array : Sexpr.Memory.t -> (Z.t * char) array
val close : unit -> unit