NaiveCnfizer Class Reference

Transforms a symbolic formula f into a CNF formula by preserving its semantics. More...

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

Public Member Functions
Formula	Convert (const Formula &f) const
	Convert f into its CNF form.

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

Detailed Description

Transforms a symbolic formula f into a CNF formula by preserving its semantics.

Note

This transform can increase the size exponentially. We are using this transformation in TseitinCnfizer when we process the nested formula in a universally quantified formula.

---

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

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