Class to evaluate a symbolic formula with a box. More...

Public Member Functions
	FormulaEvaluator (const FormulaEvaluator &)=default
	Default copy constructor.

	FormulaEvaluator (FormulaEvaluator &&)=default
	Default move constructor.

FormulaEvaluator &	operator= (const FormulaEvaluator &)=default
	Default copy assign operator.

FormulaEvaluator &	operator= (FormulaEvaluator &&)=default
	Default move assign operator.

	~FormulaEvaluator ()=default
	Default destruction.

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

const Variables &	variables () const
	Returns the occurred variables in the formula.

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`. 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...

Friends
std::ostream &	operator<< (std::ostream &os, const FormulaEvaluator &evaluator)

FormulaEvaluator	make_relational_formula_evaluator (const Formula &f)
	Creates FormulaEvaluator for a relational formula `f` using `variables`.

FormulaEvaluator	make_forall_formula_evaluator (const Formula &f, double epsilon, double delta, int number_of_jobs)
	Creates FormulaEvaluator for a universally quantified formula `f` using `variables`, `epsilon`, `delta`, and `number_of_jobs`. More...

Detailed Description

Class to evaluate a symbolic formula with a box.

Member Function Documentation

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).

bool is_simple_relational ( ) const

Returns true if the based formula is a simple relational formula which is in form of constant relop variable.

FormulaEvaluator make_forall_formula_evaluator	(	const Formula &	f,
		double	epsilon,
		double	delta,
		int	number_of_jobs
	)

friend

Creates FormulaEvaluator for a universally quantified formula f using variables, epsilon, delta, and number_of_jobs.

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