Nnfizer Class Reference

A class implementing NNF (Negation Normal Form) conversion. More...

#include </home/soonhokong/work/dreal4/dreal/util/nnfizer.h>

Public Member Functions
Formula	Convert (const Formula &f, bool push_negation_into_relationals=false) const
	Converts f into an equivalent formula f' in NNF.

Friends
Formula	drake::symbolic::VisitFormula (const Nnfizer *, const Formula &, const bool &, const bool &)

Detailed Description

A class implementing NNF (Negation Normal Form) conversion.

See https://en.wikipedia.org/wiki/Negation_normal_form for more information on NNF. When push_negation_into_relationals is true, it pushed negations into relational formulas by flipping relational operators. For example, ¬(x >= 10) is transformed into (x < 10).

---

The documentation for this class was generated from the following files:

• /home/soonhokong/work/dreal4/dreal/util/nnfizer.h
• /home/soonhokong/work/dreal4/dreal/util/nnfizer.cc