TseitinCnfizer Class Reference

Transforms a symbolic formula f into an equi-satisfiable CNF formula by introducing extra Boolean variables (Tseitin transformation). More...

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

Public Member Functions
std::vector< Formula >	Convert (const Formula &f)
	Convert f into an equi-satisfiable formula f' in CNF.
const std::map< Variable, Formula > &	map () const
	Returns a const reference of map_ member. More...

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

Detailed Description

Transforms a symbolic formula f into an equi-satisfiable CNF formula by introducing extra Boolean variables (Tseitin transformation).

Member Function Documentation

map()

const std::map<Variable, Formula>& map ( ) const

inline

Returns a const reference of map_ member.

Note

that this member map_ is cleared at the beginning of Convert method.

---

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

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