dReal4
|
Symbolic formula representing 'less-than-or-equal-to' (e1 ≤ e2). More...
Public Member Functions | |
FormulaLeq (const Expression &e1, const Expression &e2) | |
Constructs from e1 and e2 . More... | |
bool | Evaluate (const Environment &env) const override |
Evaluates under a given environment. More... | |
Formula | Substitute (const ExpressionSubstitution &expr_subst, const FormulaSubstitution &formula_subst) override |
Returns a Formula obtained by replacing all occurrences of the variables in s in the current formula cell with the corresponding expressions in s . | |
std::ostream & | Display (std::ostream &os) const override |
Outputs string representation of formula into output stream os . More... | |
![]() | |
RelationalFormulaCell ()=delete | |
Default constructor (deleted). More... | |
~RelationalFormulaCell () override=default | |
Default destructor (deleted). More... | |
RelationalFormulaCell (RelationalFormulaCell &&f)=delete | |
Move-construct a formula from an rvalue (DELETED). More... | |
RelationalFormulaCell (const RelationalFormulaCell &f)=delete | |
Copy-construct a formula from an lvalue (DELETED). More... | |
RelationalFormulaCell & | operator= (RelationalFormulaCell &&f)=delete |
Move-assign (DELETED). More... | |
RelationalFormulaCell & | operator= (const RelationalFormulaCell &f)=delete |
Copy-assign (DELETED). More... | |
RelationalFormulaCell (FormulaKind k, const Expression &lhs, const Expression &rhs) | |
Construct RelationalFormulaCell of kind k with lhs and rhs . More... | |
bool | EqualTo (const FormulaCell &f) const override |
Checks structural equality. More... | |
bool | Less (const FormulaCell &f) const override |
Checks ordering. More... | |
const Expression & | get_lhs_expression () const |
Returns the expression on left-hand-side. More... | |
const Expression & | get_rhs_expression () const |
Returns the expression on right-hand-side. More... | |
![]() | |
FormulaCell ()=delete | |
Default constructor (DELETED). More... | |
FormulaCell & | operator= (FormulaCell &&f)=delete |
Move-assign (DELETED). More... | |
FormulaCell (const FormulaCell &f)=delete | |
Copy-construct a formula from an lvalue. More... | |
FormulaCell (FormulaCell &&f)=delete | |
Move-construct a formula from an rvalue (DELETED). More... | |
FormulaCell & | operator= (const FormulaCell &f)=delete |
Copy-assign (DELETED). More... | |
FormulaKind | get_kind () const |
Returns kind of formula. More... | |
size_t | get_hash () const |
Returns hash of formula. More... | |
const Variables & | GetFreeVariables () const |
Returns set of free variables in formula. More... | |
unsigned | use_count () const |
Returns the reference count of this cell. More... | |
bool | include_ite () const |
Returns true if this symbolic formula includes an ITE (If-Then-Else) expression. More... | |
Additional Inherited Members | |
![]() | |
FormulaCell (FormulaKind k, size_t hash, bool include_ite, Variables variables) | |
Construct FormulaCell of kind k with hash . More... | |
virtual | ~FormulaCell ()=default |
Default destructor. More... | |
Formula | GetFormula () |
Returns a Formula pointing to this FormulaCell. More... | |
Symbolic formula representing 'less-than-or-equal-to' (e1 ≤ e2).
FormulaLeq | ( | const Expression & | e1, |
const Expression & | e2 | ||
) |
Constructs from e1
and e2
.
|
overridevirtual |
Outputs string representation of formula into output stream os
.
Implements FormulaCell.
|
overridevirtual |
Evaluates under a given environment.
Implements FormulaCell.