GenericContractorGenerator Class Reference

Converts an arbitrary formula into a contractor. More...

#include </home/soonhokong/work/dreal4/dreal/contractor/generic_contractor_generator.h>

Public Member Functions
Contractor	Generate (const Formula &f, const Box &box, const Config &config) const
	Generates f into a contractor using box. More...

Friends
Contractor	drake::symbolic::VisitFormula (const GenericContractorGenerator *, const Formula &, const dreal::Box &, const Config &)

Detailed Description

Converts an arbitrary formula into a contractor.

This is used in the forall contractor.

Member Function Documentation

Generate()

Contractor Generate	(	const Formula &	f,
		const Box &	box,
		const Config &	config
	)		const

Generates f into a contractor using box.

It converts a conjunction f₁ ∧ ... ∧ fₙ into a sequential contractor ContractorSeq(c(f₁), ..., c(fₙ)). For a disjunction f₁ ∨ ... ∨ fₙ, this method transforms it into a join contractor ContractorJoin(c(f₁), ..., c(fₙ)).

When use_polytope is true, it adds IbexPolytope contractor when it processes conjunctions. Otherwise, it uses ContractorIbexFwdbwd.

---

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

• /home/soonhokong/work/dreal4/dreal/contractor/generic_contractor_generator.h
• /home/soonhokong/work/dreal4/dreal/contractor/generic_contractor_generator.cc