Module Native_solver.SolverSource

Parameters

Signature

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