Evaluator for forall formulas. More...

#include </home/soonhokong/work/dreal4/dreal/solver/forall_formula_evaluator.h>

Inheritance diagram for ForallFormulaEvaluator:

Public Member Functions
	ForallFormulaEvaluator (Formula f, double epsilon, double delta, int number_of_jobs)

	ForallFormulaEvaluator (const ForallFormulaEvaluator &)=delete
	Deleted copy constructor.

	ForallFormulaEvaluator (ForallFormulaEvaluator &&)=delete
	Deleted move constructor.

ForallFormulaEvaluator &	operator= (const ForallFormulaEvaluator &)=delete
	Deleted copy-assignment operator.

ForallFormulaEvaluator &	operator= (ForallFormulaEvaluator &&)=delete
	Deleted move-assignment operator.

	~ForallFormulaEvaluator () override=default
	Default destructor.

FormulaEvaluationResult	operator() (const Box &box) const override
	Evaluates the constraint/formula with `box`.

std::ostream &	Display (std::ostream &os) const override

const Variables &	variables () const override

Public Member Functions inherited from FormulaEvaluatorCell
	FormulaEvaluatorCell (Formula f)

	FormulaEvaluatorCell (const FormulaEvaluatorCell &)=delete
	Deleted copy-constructor.

	FormulaEvaluatorCell (FormulaEvaluatorCell &&)=default
	Deleted move-constructor.

FormulaEvaluatorCell &	operator= (const FormulaEvaluatorCell &)=delete
	Deleted copy-assignment operator.

FormulaEvaluatorCell &	operator= (FormulaEvaluatorCell &&)=delete
	Deleted move-assignment operator.

virtual	~FormulaEvaluatorCell ()=default
	Default destructor.

const Formula &	formula () const

bool	is_simple_relational () const
	Returns true if the based formula is a simple relational formula which is in form of `constant relop variable` or `!(constant relop variable)`. More...

bool	is_neq () const
	Returns true if the based formula is a not-equal formula which is in form of `e1 != e2` or `!(e1 == e2)`. More...

Detailed Description

Evaluator for forall formulas.

In the standard first-order logic semantics, A universally quantified formula is evaluated to a Boolean value. Here, however, we want to have a quantitative measure when a universally-quantified formula is false. We return an error interval in order to utilize it as a termination criteria in ICP (Interval Constraint Propagation).

Given f = ∀y. [(e₁(x, y) ≥ 0) ∨ ... ∨ (eₙ(x, y) ≥ 0)], we check if there is a counterexample of f. To prevent a spurious counterexample, we check the satisfiability of the ε-strengthened version of the negation of the nested formula, strengthen((e₁(x, y) < 0) ∧ ... ∧ (eₙ(x, y) < 0), ε), with delta = δ. There can be two possible results for this query:

UNSAT: Return a zero error-interval, [0, 0].
δ-SAT: Given a counter example (a, b), evaluate eᵢ(Iₓ, b) where Iₓ is the current interval assignment on x. Returns [0, maxᵢ{|eᵢ(Iₓ, b)|}].

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

/home/soonhokong/work/dreal4/dreal/solver/forall_formula_evaluator.h
/home/soonhokong/work/dreal4/dreal/solver/forall_formula_evaluator.cc

Public Member Functions

Detailed Description