Evaluator for forall formulas. More...
#include </home/soonhokong/work/dreal4/dreal/solver/forall_formula_evaluator.h>
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), evaluateeᵢ(Iₓ, b)whereIₓ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
