Make (p.alt-ergo-lib.2.5.2.doc.alt-ergo-lib.AltErgoLib.Satml.Make)

Parameters

module Th : Theory.S

Signature

type th = Th.t

type t

val solve : t -> unit

val set_new_proxies : 
  t ->
  (Satml_types.Atom.atom * Satml_types.Atom.atom list * bool) Util.MI.t ->
  unit

val new_vars : 
  t ->
  nbv:int ->
  Satml_types.Atom.var list ->
  Satml_types.Atom.atom list list ->
  Satml_types.Atom.atom list list ->
  Satml_types.Atom.atom list list * Satml_types.Atom.atom list list

val assume : 
  t ->
  Satml_types.Atom.atom list list ->
  Satml_types.Atom.atom list list ->
  Expr.t ->
  cnumber:int ->
  Satml_types.Atom.atom option Satml_types.Flat_Formula.Map.t ->
  dec_lvl:int ->
  unit

val boolean_model : t -> Satml_types.Atom.atom list

val instantiation_context : 
  t ->
  Satml_types.Flat_Formula.hcons_env ->
  Satml_types.Atom.Set.t

val current_tbox : t -> th

val set_current_tbox : t -> th -> unit

val empty : unit -> t

val assume_th_elt : t -> Expr.th_elt -> Explanation.t -> unit

val decision_level : t -> int

val cancel_until : t -> int -> unit

val update_lazy_cnf : 
  t ->
  do_bcp:bool ->
  Satml_types.Atom.atom option Satml_types.Flat_Formula.Map.t ->
  dec_lvl:int ->
  unit

val exists_in_lazy_cnf : t -> Satml_types.Flat_Formula.t -> bool

val known_lazy_formulas : t -> int Satml_types.Flat_Formula.Map.t

val reason_of_deduction : Satml_types.Atom.atom -> Satml_types.Atom.Set.t

val assume_simple : t -> Satml_types.Atom.atom list list -> unit

val decide : t -> Satml_types.Atom.atom -> unit

val conflict_analyze_and_fix : t -> conflict_origin -> unit

val push : t -> Satml_types.Atom.atom -> unit

val pop : t -> unit