package alt-ergo-lib

  1. Overview
  2. Docs
package alt-ergo-lib
Legend:
Library
Module
Module type
Parameter
Class
Class type
type t
type view = private
  1. | UNIT of Atom.atom
  2. | AND of t list
  3. | OR of t list
type hcons_env
val equal : t -> t -> bool
val compare : t -> t -> int
val print : Format.formatter -> t -> unit
val print_stats : 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) Util.MI.t -> Atom.atom option
val cnf_abstr : hcons_env -> t -> (Atom.atom * Atom.atom list * bool) Util.MI.t -> Atom.var list -> Atom.atom * (Atom.atom * Atom.atom list * bool) list * (Atom.atom * Atom.atom list * bool) 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 : Set.S with type elt = t
module Map : Map.S with type key = t