PredicateAbstractor Class Reference

Public Member Functions
Formula	Convert (const Formula &f)
	Converts a first-order logic formula f into a Boolean formula by predicate abstraction. More...
Formula	Convert (const std::vector< Formula > &formulas)
	Converts formulas into a conjunction of Boolean formulas. More...
const std::unordered_map< Variable, Formula, hash_value< Variable > > &	var_to_formula_map () const
const Variable &	operator[] (const Formula &f) const
const Formula &	operator[] (const Variable &var) const

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

Member Function Documentation

Convert() [1/2]

Formula Convert

(

const Formula &

f

)

Converts a first-order logic formula f into a Boolean formula by predicate abstraction.

For example, a formula (x > 0) ∧ (y < 0) will be converted into b₁ ∧ b₂ while b₁ corresponds with x > 0 and b₂ corresponds with y < 0. The class provides operator[b] which looks up the corresponding formula for a Boolean variable b.

Convert() [2/2]

Formula Convert

(

const std::vector< Formula > &

formulas

)

Converts formulas into a conjunction of Boolean formulas.

See the above method.

---

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

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