Internal use only. 
Provides implementation-details of symbolic formulas. 
 | 
| bool  | is_false (const FormulaCell &f) | 
|   | Checks if f is structurally equal to False formula.  More...
  | 
|   | 
| bool  | is_true (const FormulaCell &f) | 
|   | Checks if f is structurally equal to True formula.  More...
  | 
|   | 
| bool  | is_variable (const FormulaCell &f) | 
|   | Checks if f is a variable formula.  More...
  | 
|   | 
| bool  | is_equal_to (const FormulaCell &f) | 
|   | Checks if f is a formula representing equality (==).  More...
  | 
|   | 
| bool  | is_not_equal_to (const FormulaCell &f) | 
|   | Checks if f is a formula representing disequality (!=).  More...
  | 
|   | 
| bool  | is_greater_than (const FormulaCell &f) | 
|   | Checks if f is a formula representing greater-than (>).  More...
  | 
|   | 
| bool  | is_greater_than_or_equal_to (const FormulaCell &f) | 
|   | Checks if f is a formula representing greater-than-or-equal-to (>=).  More...
  | 
|   | 
| bool  | is_less_than (const FormulaCell &f) | 
|   | Checks if f is a formula representing less-than (<).  More...
  | 
|   | 
| bool  | is_less_than_or_equal_to (const FormulaCell &f) | 
|   | Checks if f is a formula representing less-than-or-equal-to (<=).  More...
  | 
|   | 
| bool  | is_relational (const FormulaCell &f) | 
|   | Checks if f is a relational formula ({==, !=, >, >=, <, <=}).  More...
  | 
|   | 
| bool  | is_conjunction (const FormulaCell &f) | 
|   | Checks if f is a conjunction (∧).  More...
  | 
|   | 
| bool  | is_disjunction (const FormulaCell &f) | 
|   | Checks if f is a disjunction (∨).  More...
  | 
|   | 
| bool  | is_nary (const FormulaCell &f) | 
|   | Checks if f is N-ary.  More...
  | 
|   | 
| bool  | is_negation (const FormulaCell &f) | 
|   | Checks if f is a negation (¬).  More...
  | 
|   | 
| bool  | is_forall (const FormulaCell &f) | 
|   | Checks if f is a Forall formula (∀).  More...
  | 
|   | 
| bool  | is_isnan (const FormulaCell &f) | 
|   | Checks if f is an isnan formula.  More...
  | 
|   | 
| bool  | is_positive_semidefinite (const FormulaCell &f) | 
|   | Checks if f is a positive semidefinite formula.  More...
  | 
|   | 
| std::shared_ptr< const FormulaFalse >  | to_false (const std::shared_ptr< const FormulaCell > &f_ptr) | 
|   | Casts f_ptr to shared_ptr<const FormulaFalse>.  More...
  | 
|   | 
| std::shared_ptr< const FormulaTrue >  | to_true (const std::shared_ptr< const FormulaCell > &f_ptr) | 
|   | Casts f_ptr to shared_ptr<const FormulaTrue>.  More...
  | 
|   | 
| std::shared_ptr< const FormulaVar >  | to_variable (const std::shared_ptr< const FormulaCell > &f_ptr) | 
|   | Casts f_ptr to shared_ptr<const FormulaVar>.  More...
  | 
|   | 
| std::shared_ptr< const RelationalFormulaCell >  | to_relational (const std::shared_ptr< const FormulaCell > &f_ptr) | 
|   | Casts f_ptr to shared_ptr<const RelationalFormulaCell>.  More...
  | 
|   | 
| std::shared_ptr< const FormulaEq >  | to_equal_to (const std::shared_ptr< const FormulaCell > &f_ptr) | 
|   | Casts f_ptr to shared_ptr<const FormulaEq>.  More...
  | 
|   | 
| std::shared_ptr< const FormulaNeq >  | to_not_equal_to (const std::shared_ptr< const FormulaCell > &f_ptr) | 
|   | Casts f_ptr to shared_ptr<const FormulaNeq>.  More...
  | 
|   | 
| std::shared_ptr< const FormulaGt >  | to_greater_than (const std::shared_ptr< const FormulaCell > &f_ptr) | 
|   | Casts f_ptr to shared_ptr<const FormulaGt>.  More...
  | 
|   | 
| std::shared_ptr< const FormulaGeq >  | to_greater_than_or_equal_to (const std::shared_ptr< const FormulaCell > &f_ptr) | 
|   | Casts f_ptr to shared_ptr<const FormulaGeq>.  More...
  | 
|   | 
| std::shared_ptr< const FormulaLt >  | to_less_than (const std::shared_ptr< const FormulaCell > &f_ptr) | 
|   | Casts f_ptr to shared_ptr<const FormulaLt>.  More...
  | 
|   | 
| std::shared_ptr< const FormulaLeq >  | to_less_than_or_equal_to (const std::shared_ptr< const FormulaCell > &f_ptr) | 
|   | Casts f_ptr to shared_ptr<const FormulaLeq>.  More...
  | 
|   | 
| std::shared_ptr< const FormulaAnd >  | to_conjunction (const std::shared_ptr< const FormulaCell > &f_ptr) | 
|   | Casts f_ptr to shared_ptr<const FormulaAnd>.  More...
  | 
|   | 
| std::shared_ptr< const FormulaOr >  | to_disjunction (const std::shared_ptr< const FormulaCell > &f_ptr) | 
|   | Casts f_ptr to shared_ptr<const FormulaOr>.  More...
  | 
|   | 
| std::shared_ptr< const NaryFormulaCell >  | to_nary (const std::shared_ptr< const FormulaCell > &f_ptr) | 
|   | Casts f_ptr to shared_ptr<const NaryFormulaCell>.  More...
  | 
|   | 
| std::shared_ptr< const FormulaNot >  | to_negation (const std::shared_ptr< const FormulaCell > &f_ptr) | 
|   | Casts f_ptr to shared_ptr<const FormulaNot>.  More...
  | 
|   | 
| std::shared_ptr< const FormulaForall >  | to_forall (const std::shared_ptr< const FormulaCell > &f_ptr) | 
|   | Casts f_ptr to shared_ptr<const FormulaForall>.  More...
  | 
|   | 
| std::shared_ptr< const FormulaIsnan >  | to_isnan (const std::shared_ptr< const FormulaCell > &f_ptr) | 
|   | Casts f_ptr to shared_ptr<const FormulaIsnan>.  More...
  | 
|   | 
| std::shared_ptr< const FormulaPositiveSemidefinite >  | to_positive_semidefinite (const std::shared_ptr< const FormulaCell > &f_ptr) | 
|   | Casts f_ptr to shared_ptr<const FormulaPositiveSemidefinite>.  More...
  | 
|   |