Module Comp.Dnf'

Explicit DNF over condensed atoms.

An condensed explicit DNF of atoms.

type atom = Atom.t
type leaf = bool
type t = (atom * leaf) list

t represents a condensed disjunctive normal form, that is, a disjunction of atoms. leaf is a boolean that should be true. If set to false, the corresponding atom will be ignored.

val simplify : t -> t

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