package alt-ergo-lib

  1. Overview
  2. Docs
package alt-ergo-lib
Legend:
Library
Module
Module type
Parameter
Class
Class type

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 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