IfThenElseEliminator Class Reference

Eliminates If-Then-Else expressions by introducing new variables. More...

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

Public Member Functions
Formula	Process (const Formula &f)
	Returns a equisatisfiable formula by eliminating if-then-expressions in f by introducing new variables. More...
const std::unordered_set< Variable, hash_value< Variable > > &	variables () const

Friends
Formula	drake::symbolic::VisitFormula (IfThenElseEliminator *, const Formula &, const Formula &)
Expression	drake::symbolic::VisitExpression (IfThenElseEliminator *, const Expression &, const Formula &)

Detailed Description

Eliminates If-Then-Else expressions by introducing new variables.

TODO(soonho): Check "Efficient Term ITE Conversion for Satisfiability Modulo Theories", H. Kim, F. Somenzi, H. Jin. Twelfth International Conference on Theory and Applications of Satisfiability Testing (SAT'09).

Member Function Documentation

Process()

Formula Process

(

const Formula &

f

)

Returns a equisatisfiable formula by eliminating if-then-expressions in f by introducing new variables.

---

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

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