Module Satml_types.Flat_Formula

type t
type view = private
| UNIT of Atom.atom
| AND of t list
| OR of t list
type hcons_env
val equal : t -> t -> bool
val compare : t -> t -> int
val print : Stdlib.Format.formatter -> t -> unit
val print_stats : Stdlib.Format.formatter -> unit
val vrai : t
val faux : t
val view : t -> view
val mk_lit : hcons_env -> Expr.t -> Atom.var list -> t * Atom.var list
val mk_and : hcons_env -> t list -> t
val mk_or : hcons_env -> t list -> t
val mk_not : t -> t
val empty_hcons_env : unit -> hcons_env
val nb_made_vars : hcons_env -> int
val get_atom : hcons_env -> Expr.t -> Atom.atom
val simplify : hcons_env -> Expr.t -> ( Expr.t -> t * 'a ) -> Atom.var list -> t * (Expr.t * (t * Atom.atom)) list * Atom.var list
val get_proxy_of : t -> (Atom.atom * Atom.atom list * bool) AltErgoLib.Util.MI.t -> Atom.atom option
val cnf_abstr : hcons_env -> t -> (Atom.atom * Atom.atom list * bool) AltErgoLib.Util.MI.t -> Atom.var list -> Atom.atom * (Atom.atom * Atom.atom list * bool) list * (Atom.atom * Atom.atom list * bool) AltErgoLib.Util.MI.t * Atom.var list
val expand_proxy_defn : Atom.atom list list -> (Atom.atom * Atom.atom list * bool) -> Atom.atom list list
module Set : Stdlib.Set.S with type elt = t
module Map : Stdlib.Map.S with type key = t