Conjunction of expressions.
An atom, ie a free proposition.
Abstract base type for all NNF expressions.
Conditional selection.
Negation (only over an atom since we're in Negation Normal Form).
Disjunction.
Translator from Core to NNF.
Creates a fresh uniquely identified atom.
Builds the dependency graph of an expression (frome leaves to top node).
Builds the inverse dependency graph of an expression (from top node to leaves).
A map associating to each sub expression of the expression a boolean flag true iff the sub expression is in a proper subtree tree wrt the root of the expression.
TODO fix bug in the way this flag is computed, introduce notion of polarity with monotony.
TODO fix bug in the way this flag is computed, introduce notion of polarity with monotony.
A map associating to each sub expression of the expression a boolean flagtrue iff the sub expression has a montonic influence wrt the root of the expression.
Propositional logic in negation-normal-form.