ContractorForall< ContextType > Class Template Reference

Contractor for forall constraints. More...

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

Inheritance diagram for ContractorForall< ContextType >:

Public Member Functions
	ContractorForall (Formula f, const Box &box, double epsilon, double inner_delta, const Config &config)
	Constructs Forall contractor using f and box. More...
	ContractorForall (const ContractorForall &)=delete
	Deleted copy constructor.
	ContractorForall (ContractorForall &&)=delete
	Deleted move constructor.
ContractorForall &	operator= (const ContractorForall &)=delete
	Deleted copy assign operator.
ContractorForall &	operator= (ContractorForall &&)=delete
	Deleted move assign operator.
bool	PruneWithCounterexample (ContractorStatus *cs, Box *const current_box, const Box &counterexample) const
	~ContractorForall () override=default
	Default destructor.
void	Prune (ContractorStatus *cs) const override
	Performs pruning on cs.
std::ostream &	display (std::ostream &os) const override
	Outputs this contractor to os.
Public Member Functions inherited from ContractorCell
	ContractorCell (Contractor::Kind kind, DynamicBitset input, Config config)
	Constructs a cell with kind and input.
	ContractorCell ()=delete
	Deleted default constructor.
	ContractorCell (const ContractorCell &)=delete
	Deleted copy constructor.
	ContractorCell (ContractorCell &&)=delete
	Deleted move constructor.
void	operator= (const ContractorCell &)=delete
	Deleted copy assign operator.
void	operator= (ContractorCell &&)=delete
	Deleted move assign operator.
virtual	~ContractorCell ()=default
	Default destructor.
Contractor::Kind	kind () const
	Returns its kind.
const DynamicBitset &	input () const
	Returns its input.
DynamicBitset &	mutable_input ()
	Returns its input.
const Config &	config () const
	Returns config.
bool	include_forall () const
	Returns true if this contractor includes a forall contractor.
void	set_include_forall ()
	Sets include_forall true.

Detailed Description

template<typename ContextType>
class dreal::ContractorForall< ContextType >

Contractor for forall constraints.

See the following problem definition and our approach.

Problem: Given a box B ∈ IRⁿ and a formula F =
∃x₁...xₙ. ∀y₁....yₘ. φ(x₁, ..., xₙ, y₁, ..., yₘ), design a
contractor reducing B into B' where B' ⊆ B.

Approach: Find a counterexample (a₁, ..., aₙ, b₁, ..., bₘ) such
that ¬φ(a₁, ..., aₙ, b₁, ..., bₘ) holds while (a₁, ..., aₙ) ∈ B.
We do this by computing Solve(strengthen(¬φ, ε), δ) where ε > δ.

Case 1: No CE found.
           This means that any point in B satisfies the quantified
           portion of F.

Case 2: Found a CE, (a₁, ..., aₙ, b₁, ..., bₘ).
           Use the CE to reduce B into B'. That is compute,
B' = Contract(φ(x₁, ..., xₙ, b₁, ..., bₘ), B)

Constructor & Destructor Documentation

ContractorForall()

ContractorForall ( Formula  f, const Box &  box, double  epsilon, double  inner_delta, const Config &  config  )

inline

Constructs Forall contractor using f and box.

epsilon is used to strengthen ¬φ and inner_delta is used to solve (¬φ)⁻ᵟ¹.

Precondition

0.0 < inner_delta < epsilon < config.precision().

---

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

• /home/soonhokong/work/dreal4/dreal/contractor/contractor.h
• /home/soonhokong/work/dreal4/dreal/contractor/contractor_forall.h