Module Default.Solver

type status = Binsec_symbolic.Smtlib.Solver.status =
  1. | Sat
  2. | Unsat
  3. | Unknown
module type S = sig ... end
module Dummy : S
type lazy_memory = {
  1. contents : Binsec_kernel.Loader_types.buffer option Binsec_kernel.Zmap.t Binsec_symbolic__Default__.Types.AsMap.t;
  2. mutable lemmas : ([ `Exp ], string, [ `Some ] Binsec_symbolic__Default__.Types.Memory.node) Binsec_base.Term.t list;
}
type result =
  1. | Sat of Binsec_symbolic__Default__.Types.Model.t
  2. | Unsat
  3. | Unknown
type cache
val empty_cache : unit -> cache
val clear_cache : cache -> unit
type mode =
  1. | One_shot
  2. | Multi_checks of cache
val open_session : ?carbon_copy:(unit -> string) -> Binsec_symbolic.Smtlib.Solver.backend -> unit -> (module S)
val check_sat : (unit -> (module S)) -> mode -> ?timeout:float -> lazy_memory -> ([ `Exp ], string, [ `Some ] Binsec_symbolic__Default__.Types.Memory.node) Binsec_base.Term.t list -> result
type enumeration
val enumerate_values : (unit -> (module S)) -> ?timeout:float -> lazy_memory -> ([ `Exp ], string, [ `Some ] Binsec_symbolic__Default__.Types.Memory.node) Binsec_base.Term.t list -> ([ `Exp ], string, [ `Some ] Binsec_symbolic__Default__.Types.Memory.node) Binsec_base.Term.t -> except:Binsec_kernel.Bitvector.t list -> enumeration
val next_value : enumeration -> (Binsec_kernel.Bitvector.t * Binsec_symbolic__Default__.Types.Model.t) option
val release_enumeration : enumeration -> unit