Module Native_solver.SolverSource

Parameters

Signature

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