Module Comp.Dnf

An explicit DNF of atoms.

type atom = Atom.t
type leaf = bool
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.