Module type Satml_types.FLAT_FORMULA

type t
type view = private
  1. | UNIT of Atom.atom
  2. | AND of t list
  3. | OR of t list
type hcons_env
type proxy_defn

A proxy definition, encoding an equivalence p <=> l_1 /\ ... /\ l_n or p <=> l_1 \/ ... \/ l_n where p is a proxy and l_1, ..., l_n are literals.

See get_proxy_of and expand_proxy_defn.

type proxies

Mapping from flat formulas to their proxy definition, if any.

val empty_proxies : proxies
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 atom_hcons_env : hcons_env -> Atom.hcons_env
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 -> proxies -> Atom.atom option

get_proxy_of ff proxies returns the proxy registered for ff in proxies, if it exists.

Note: If ff is a unit formula (i.e. a literal), get_proxy_of returns None.

The proxy of a flat formula ff is an atom p with the (implicit) equivalent p <=> ff. Proxies are used to perform lazy CNF conversion of formulas in the CDCL-Tableaux solver.

val cnf_abstr : hcons_env -> t -> proxies -> Atom.var list -> Atom.atom * proxy_defn list * proxies * Atom.var list
val expand_proxy_defn : Atom.atom list list -> proxy_defn -> Atom.atom list list

Expand a proxy definition into clausal normal form.

The definition p <=> l_1 \/ ... \/ l_n is expanded into:

(~p \/ l_1 \/ ... \/ l_n) /\ (p \/ ~l_1) /\ ... /\ (p \/ ~l_n)

and the definition p <=> l_1 /\ ... /\ l_n is expanded into:

(p \/ ~l_1 \/ ... \/ ~l_n) /\ (~p \/ l_1) /\ ... /\ (~p \/ l_n)

val reinit_cpt : unit -> unit

Resets to 0 the counter

module Set : Stdlib.Set.S with type elt = t
module Map : Stdlib.Map.S with type key = t