| dReal4
    | 
Symbolic formula representing disequality (e1 ≠ e2). More...
 
  
 | Public Member Functions | |
| FormulaNeq (const Expression &e1, const Expression &e2) | |
| Constructs from e1ande2.  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 sin the current formula cell with the corresponding expressions ins. | |
| std::ostream & | Display (std::ostream &os) const override | 
| Outputs string representation of formula into output stream os.  More... | |
|  Public Member Functions inherited from RelationalFormulaCell | |
| 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 kwithlhsandrhs.  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... | |
|  Public Member Functions inherited from FormulaCell | |
| 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 | |
|  Protected Member Functions inherited from FormulaCell | |
| FormulaCell (FormulaKind k, size_t hash, bool include_ite, Variables variables) | |
| Construct FormulaCell of kind kwithhash.  More... | |
| virtual | ~FormulaCell ()=default | 
| Default destructor.  More... | |
| Formula | GetFormula () | 
| Returns a Formula pointing to this FormulaCell.  More... | |
Symbolic formula representing disequality (e1 ≠ e2).
| FormulaNeq | ( | 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.