VDescr.Dnf
Explicit Disjunctive Normal Forms (DNF) of variables and monomorphic descriptors.
type atom = Var.t
type leaf = Descr.t
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.
t
leaf
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.
simplify t
empty
any