Module VDescr.Dnf

Explicit Disjunctive Normal Forms (DNF) of variables and monomorphic descriptors.

type atom = Var.t
type leaf
type t = (atom list * atom list * leaf) list

t represents a disjunctive normal form, that is, a disjunction of clauses. For leaf components, leaf is a boolean that should be true. If set to false, the corresponding clause will be ignored.

val simplify : t -> t

simplify t removes from t useless clauses and summands. In particular, simplify t is ensured not to contain any empty summand nor any clause.