Module Libterm.SolverSource

Sourcemodule type S = sig ... end
Sourcemodule type OPEN = functor () -> S
Sourcetype lazy_memory = {
  1. addr_space : int;
  2. content : (Z.t * Binsec.Loader_buf.t) Binsec.Imap.t;
  3. mutable lemmas : Sexpr.Expr.t list;
}
Sourcetype result =
  1. | Sat of Sexpr.Model.t
  2. | Unsat
  3. | Unknown
Sourcemodule type GET_MODEL = sig ... end