carl  25.02
Computer ARithmetic Library
carl::Formula< Pol > Class Template Reference

Represent an SMT formula, which can be an atom for some background theory or a boolean combination of (sub)formulas. More...

#include <Formula.h>

Inheritance diagram for carl::Formula< Pol >:

Public Types

using const_iterator = typename Formulas< Pol >::const_iterator
 A constant iterator to a sub-formula of a formula. More...
 
using const_reverse_iterator = typename Formulas< Pol >::const_reverse_iterator
 A constant reverse iterator to a sub-formula of a formula. More...
 
using PolynomialType = Pol
 A typedef for the template argument. More...
 

Public Member Functions

 Formula (FormulaType _type=FALSE)
 
 Formula (Variable::Arg _booleanVar)
 
 Formula (const Pol &_pol, Relation _rel)
 
 Formula (const Constraint< Pol > &_constraint)
 
 Formula (const VariableComparison< Pol > &_variableComparison)
 
 Formula (const VariableAssignment< Pol > &_variableAssignment)
 
 Formula (const BVConstraint &_constraint)
 
 Formula (FormulaType _type, Formula &&_subformula)
 
 Formula (FormulaType _type, const Formula &_subformula)
 
 Formula (FormulaType _type, const Formula &_subformulaA, const Formula &_subformulaB)
 
 Formula (FormulaType _type, const Formula &_subformulaA, const Formula &_subformulaB, const Formula &_subformulaC)
 
 Formula (FormulaType _type, const FormulasMulti< Pol > &_subformulas)
 
 Formula (FormulaType _type, const Formulas< Pol > &_subasts)
 
 Formula (FormulaType _type, Formulas< Pol > &&_subasts)
 
 Formula (FormulaType _type, const std::initializer_list< Formula< Pol >> &_subasts)
 
 Formula (FormulaType _type, const FormulaSet< Pol > &_subasts)
 
 Formula (FormulaType _type, FormulaSet< Pol > &&_subasts)
 
 Formula (FormulaType _type, std::vector< Variable > &&_vars, const Formula &_term)
 
 Formula (FormulaType _type, const std::vector< Variable > &_vars, const Formula &_term)
 
 Formula (FormulaType _type, std::vector< Variable > &&_vars, const Formula &_aux_term, const Formula &_term)
 
 Formula (FormulaType _type, const std::vector< Variable > &_vars, const Formula &_aux_term, const Formula &_term)
 
 Formula (const UTerm &_lhs, const UTerm &_rhs, bool _negated)
 
 Formula (UEquality &&_eq)
 
 Formula (const UEquality &_eq)
 
 Formula (const Formula &_formula)
 
 Formula (Formula &&_formula) noexcept
 
 ~Formula ()
 
Formulaoperator= (const Formula &_formula)
 
Formulaoperator= (Formula &&_formula)
 
double activity () const
 
void set_activity (double _activity) const
 Sets the activity to the given value. More...
 
FormulaType type () const
 
std::size_t hash () const
 
std::size_t id () const
 
bool is_true () const
 
bool is_false () const
 
const Conditionproperties () const
 
const Variablesvariables () const
 
Formula negated () const
 
Formula base_formula () const
 
const Formularemove_negations () const
 
const Formulasubformula () const
 
const Formulapremise () const
 
const Formulaconclusion () const
 
const Formulacondition () const
 
const Formulafirst_case () const
 
const Formulasecond_case () const
 
const std::vector< carl::Variable > & quantified_variables () const
 
const Formulaquantified_formula () const
 
const Formulaquantified_aux_formula () const
 
const Formulas< Pol > & subformulas () const
 
const Constraint< Pol > & constraint () const
 
const VariableComparison< Pol > & variable_comparison () const
 
const VariableAssignment< Pol > & variable_assignment () const
 
const BVConstraintbv_constraint () const
 
carl::Variable::Arg boolean () const
 
const UEqualityu_equality () const
 
size_t size () const
 
bool empty () const
 
const_iterator begin () const
 
const_iterator end () const
 
const_reverse_iterator rbegin () const
 
const_reverse_iterator rend () const
 
const Formulaback () const
 
bool property_holds (const Condition &_property) const
 Checks if the given property holds for this formula. More...
 
bool is_atom () const
 
bool is_literal () const
 
bool is_boolean_combination () const
 
bool is_bound () const
 
bool is_nary () const
 
bool is_constraint_conjunction () const
 
bool is_real_constraint_conjunction () const
 
bool is_integer_constraint_conjunction () const
 
bool is_only_propositional () const
 
Logic logic () const
 
bool contains (const Formula &_formula) const
 
bool operator== (const Formula &_formula) const
 
bool operator!= (const Formula &_formula) const
 
bool operator< (const Formula &_formula) const
 
bool operator> (const Formula &_formula) const
 
bool operator<= (const Formula &_formula) const
 
bool operator>= (const Formula &_formula) const
 
Formula operator! () const
 

Static Public Member Functions

static void init (FormulaContent< Pol > &_content)
 Gets the propositions of this formula. More...
 

Private Member Functions

 Formula (const FormulaContent< Pol > *_content)
 

Static Private Member Functions

static void addConstraintProperties (const Constraint< Pol > &_constraint, Condition &_properties)
 Adds the propositions of the given constraint to the propositions of this formula. More...
 

Private Attributes

const FormulaContent< Pol > * mpContent
 The content of this formula. More...
 

Friends

class FormulaPool< Pol >
 
class FormulaContent< Pol >
 
template<typename P >
std::ostream & operator<< (std::ostream &os, const Formula< P > &f)
 The output operator of a formula. More...
 

Detailed Description

template<typename Pol>
class carl::Formula< Pol >

Represent an SMT formula, which can be an atom for some background theory or a boolean combination of (sub)formulas.

Definition at line 46 of file Formula.h.

Member Typedef Documentation

◆ const_iterator

template<typename Pol >
using carl::Formula< Pol >::const_iterator = typename Formulas<Pol>::const_iterator

A constant iterator to a sub-formula of a formula.

Definition at line 55 of file Formula.h.

◆ const_reverse_iterator

template<typename Pol >
using carl::Formula< Pol >::const_reverse_iterator = typename Formulas<Pol>::const_reverse_iterator

A constant reverse iterator to a sub-formula of a formula.

Definition at line 57 of file Formula.h.

◆ PolynomialType

template<typename Pol >
using carl::Formula< Pol >::PolynomialType = Pol

A typedef for the template argument.

Definition at line 59 of file Formula.h.

Constructor & Destructor Documentation

◆ Formula() [1/27]

template<typename Pol >
carl::Formula< Pol >::Formula ( const FormulaContent< Pol > *  _content)
inlineexplicitprivate

Definition at line 75 of file Formula.h.

Here is the call graph for this function:
Here is the caller graph for this function:

◆ Formula() [2/27]

template<typename Pol >
carl::Formula< Pol >::Formula ( FormulaType  _type = FALSE)
inlineexplicit

Definition at line 98 of file Formula.h.

◆ Formula() [3/27]

template<typename Pol >
carl::Formula< Pol >::Formula ( Variable::Arg  _booleanVar)
inlineexplicit

Definition at line 102 of file Formula.h.

◆ Formula() [4/27]

template<typename Pol >
carl::Formula< Pol >::Formula ( const Pol _pol,
Relation  _rel 
)
inlineexplicit

Definition at line 106 of file Formula.h.

◆ Formula() [5/27]

template<typename Pol >
carl::Formula< Pol >::Formula ( const Constraint< Pol > &  _constraint)
inlineexplicit

Definition at line 110 of file Formula.h.

◆ Formula() [6/27]

template<typename Pol >
carl::Formula< Pol >::Formula ( const VariableComparison< Pol > &  _variableComparison)
inlineexplicit

Definition at line 114 of file Formula.h.

◆ Formula() [7/27]

template<typename Pol >
carl::Formula< Pol >::Formula ( const VariableAssignment< Pol > &  _variableAssignment)
inlineexplicit

Definition at line 118 of file Formula.h.

◆ Formula() [8/27]

template<typename Pol >
carl::Formula< Pol >::Formula ( const BVConstraint _constraint)
inlineexplicit

Definition at line 122 of file Formula.h.

◆ Formula() [9/27]

template<typename Pol >
carl::Formula< Pol >::Formula ( FormulaType  _type,
Formula< Pol > &&  _subformula 
)
inlineexplicit

Definition at line 126 of file Formula.h.

◆ Formula() [10/27]

template<typename Pol >
carl::Formula< Pol >::Formula ( FormulaType  _type,
const Formula< Pol > &  _subformula 
)
inlineexplicit

Definition at line 130 of file Formula.h.

◆ Formula() [11/27]

template<typename Pol >
carl::Formula< Pol >::Formula ( FormulaType  _type,
const Formula< Pol > &  _subformulaA,
const Formula< Pol > &  _subformulaB 
)
inlineexplicit

Definition at line 134 of file Formula.h.

◆ Formula() [12/27]

template<typename Pol >
carl::Formula< Pol >::Formula ( FormulaType  _type,
const Formula< Pol > &  _subformulaA,
const Formula< Pol > &  _subformulaB,
const Formula< Pol > &  _subformulaC 
)
inlineexplicit

Definition at line 140 of file Formula.h.

◆ Formula() [13/27]

template<typename Pol >
carl::Formula< Pol >::Formula ( FormulaType  _type,
const FormulasMulti< Pol > &  _subformulas 
)
inlineexplicit

Definition at line 144 of file Formula.h.

◆ Formula() [14/27]

template<typename Pol >
carl::Formula< Pol >::Formula ( FormulaType  _type,
const Formulas< Pol > &  _subasts 
)
inlineexplicit

Definition at line 150 of file Formula.h.

◆ Formula() [15/27]

template<typename Pol >
carl::Formula< Pol >::Formula ( FormulaType  _type,
Formulas< Pol > &&  _subasts 
)
inlineexplicit

Definition at line 154 of file Formula.h.

◆ Formula() [16/27]

template<typename Pol >
carl::Formula< Pol >::Formula ( FormulaType  _type,
const std::initializer_list< Formula< Pol >> &  _subasts 
)
inlineexplicit

Definition at line 158 of file Formula.h.

◆ Formula() [17/27]

template<typename Pol >
carl::Formula< Pol >::Formula ( FormulaType  _type,
const FormulaSet< Pol > &  _subasts 
)
inlineexplicit

Definition at line 162 of file Formula.h.

◆ Formula() [18/27]

template<typename Pol >
carl::Formula< Pol >::Formula ( FormulaType  _type,
FormulaSet< Pol > &&  _subasts 
)
inlineexplicit

Definition at line 166 of file Formula.h.

◆ Formula() [19/27]

template<typename Pol >
carl::Formula< Pol >::Formula ( FormulaType  _type,
std::vector< Variable > &&  _vars,
const Formula< Pol > &  _term 
)
inlineexplicit

Definition at line 170 of file Formula.h.

◆ Formula() [20/27]

template<typename Pol >
carl::Formula< Pol >::Formula ( FormulaType  _type,
const std::vector< Variable > &  _vars,
const Formula< Pol > &  _term 
)
inlineexplicit

Definition at line 174 of file Formula.h.

◆ Formula() [21/27]

template<typename Pol >
carl::Formula< Pol >::Formula ( FormulaType  _type,
std::vector< Variable > &&  _vars,
const Formula< Pol > &  _aux_term,
const Formula< Pol > &  _term 
)
inlineexplicit

Definition at line 178 of file Formula.h.

◆ Formula() [22/27]

template<typename Pol >
carl::Formula< Pol >::Formula ( FormulaType  _type,
const std::vector< Variable > &  _vars,
const Formula< Pol > &  _aux_term,
const Formula< Pol > &  _term 
)
inlineexplicit

Definition at line 182 of file Formula.h.

◆ Formula() [23/27]

template<typename Pol >
carl::Formula< Pol >::Formula ( const UTerm _lhs,
const UTerm _rhs,
bool  _negated 
)
inlineexplicit

Definition at line 186 of file Formula.h.

◆ Formula() [24/27]

template<typename Pol >
carl::Formula< Pol >::Formula ( UEquality &&  _eq)
inlineexplicit

Definition at line 190 of file Formula.h.

◆ Formula() [25/27]

template<typename Pol >
carl::Formula< Pol >::Formula ( const UEquality _eq)
inlineexplicit

Definition at line 194 of file Formula.h.

◆ Formula() [26/27]

template<typename Pol >
carl::Formula< Pol >::Formula ( const Formula< Pol > &  _formula)
inline

Definition at line 198 of file Formula.h.

Here is the call graph for this function:

◆ Formula() [27/27]

template<typename Pol >
carl::Formula< Pol >::Formula ( Formula< Pol > &&  _formula)
inlinenoexcept

Definition at line 205 of file Formula.h.

◆ ~Formula()

template<typename Pol >
carl::Formula< Pol >::~Formula ( )
inline

Definition at line 211 of file Formula.h.

Here is the call graph for this function:

Member Function Documentation

◆ activity()

template<typename Pol >
double carl::Formula< Pol >::activity ( ) const
inline
Returns
The activity for this formula, which means, how much is this formula involved in the solving procedure.

Definition at line 243 of file Formula.h.

◆ addConstraintProperties()

template<typename Pol >
static void carl::Formula< Pol >::addConstraintProperties ( const Constraint< Pol > &  _constraint,
Condition _properties 
)
staticprivate

Adds the propositions of the given constraint to the propositions of this formula.

Parameters
_constraintThe constraint to add propositions for.
_properties

◆ back()

template<typename Pol >
const Formula& carl::Formula< Pol >::back ( ) const
inline
Returns
A reference to the last sub-formula of this formula.

Definition at line 540 of file Formula.h.

Here is the call graph for this function:
Here is the caller graph for this function:

◆ base_formula()

template<typename Pol >
Formula carl::Formula< Pol >::base_formula ( ) const
inline

Definition at line 320 of file Formula.h.

Here is the call graph for this function:

◆ begin()

template<typename Pol >
const_iterator carl::Formula< Pol >::begin ( ) const
inline
Returns
A constant iterator to the beginning of the list of sub-formulas of this formula.

Definition at line 504 of file Formula.h.

Here is the call graph for this function:

◆ boolean()

template<typename Pol >
carl::Variable::Arg carl::Formula< Pol >::boolean ( ) const
inline
Returns
The name of the Boolean variable represented by this formula. Note, that this formula has to be of type BOOL, if you invoke this method.

Definition at line 458 of file Formula.h.

Here is the caller graph for this function:

◆ bv_constraint()

template<typename Pol >
const BVConstraint& carl::Formula< Pol >::bv_constraint ( ) const
inline

Definition at line 448 of file Formula.h.

Here is the caller graph for this function:

◆ conclusion()

template<typename Pol >
const Formula& carl::Formula< Pol >::conclusion ( ) const
inline
Returns
A constant reference to the conclusion, in case this formula is an implication.

Definition at line 353 of file Formula.h.

Here is the caller graph for this function:

◆ condition()

template<typename Pol >
const Formula& carl::Formula< Pol >::condition ( ) const
inline
Returns
A constant reference to the condition, in case this formula is an ite-expression of formulas.

Definition at line 362 of file Formula.h.

Here is the caller graph for this function:

◆ constraint()

template<typename Pol >
const Constraint<Pol>& carl::Formula< Pol >::constraint ( ) const
inline
Returns
A constant reference to the constraint represented by this formula. Note, that this formula has to be of type CONSTRAINT, if you invoke this method.

Definition at line 432 of file Formula.h.

Here is the caller graph for this function:

◆ contains()

template<typename Pol >
bool carl::Formula< Pol >::contains ( const Formula< Pol > &  _formula) const
inline
Parameters
_formulaThe pointer to the formula for which to check whether it points to a sub-formula of this formula.
Returns
true, the given pointer to a formula points to a sub-formula of this formula; false, otherwise.

Definition at line 712 of file Formula.h.

Here is the call graph for this function:

◆ empty()

template<typename Pol >
bool carl::Formula< Pol >::empty ( ) const
inline
Returns
true, if this formula has sub-formulas; false, otherwise.

Definition at line 491 of file Formula.h.

◆ end()

template<typename Pol >
const_iterator carl::Formula< Pol >::end ( ) const
inline
Returns
A constant iterator to the end of the list of sub-formulas of this formula.

Definition at line 513 of file Formula.h.

Here is the call graph for this function:
Here is the caller graph for this function:

◆ first_case()

template<typename Pol >
const Formula& carl::Formula< Pol >::first_case ( ) const
inline
Returns
A constant reference to the then-case, in case this formula is an ite-expression of formulas.

Definition at line 371 of file Formula.h.

Here is the caller graph for this function:

◆ hash()

template<typename Pol >
std::size_t carl::Formula< Pol >::hash ( ) const
inline
Returns
A hash value for this formula.

Definition at line 270 of file Formula.h.

Here is the caller graph for this function:

◆ id()

template<typename Pol >
std::size_t carl::Formula< Pol >::id ( ) const
inline
Returns
The unique id for this formula.

Definition at line 278 of file Formula.h.

Here is the caller graph for this function:

◆ init()

template<typename Pol >
static void carl::Formula< Pol >::init ( FormulaContent< Pol > &  _content)
static

Gets the propositions of this formula.

It updates and stores the propositions if they are not up to date, hence this method is quite efficient.

◆ is_atom()

template<typename Pol >
bool carl::Formula< Pol >::is_atom ( ) const
inline
Returns
true, if this formula is a Boolean atom.

Definition at line 563 of file Formula.h.

Here is the caller graph for this function:

◆ is_boolean_combination()

template<typename Pol >
bool carl::Formula< Pol >::is_boolean_combination ( ) const
inline
Returns
true, if the outermost operator of this formula is Boolean; false, otherwise.

Definition at line 580 of file Formula.h.

Here is the call graph for this function:
Here is the caller graph for this function:

◆ is_bound()

template<typename Pol >
bool carl::Formula< Pol >::is_bound ( ) const
inline

Definition at line 585 of file Formula.h.

Here is the call graph for this function:

◆ is_constraint_conjunction()

template<typename Pol >
bool carl::Formula< Pol >::is_constraint_conjunction ( ) const
inline
Returns
true, if this formula is a conjunction of constraints; false, otherwise.

Definition at line 607 of file Formula.h.

Here is the call graph for this function:

◆ is_false()

template<typename Pol >
bool carl::Formula< Pol >::is_false ( ) const
inline
Returns
true, if this formula represents FALSE.

Definition at line 294 of file Formula.h.

Here is the caller graph for this function:

◆ is_integer_constraint_conjunction()

template<typename Pol >
bool carl::Formula< Pol >::is_integer_constraint_conjunction ( ) const
inline
Returns
true, if this formula is a conjunction of integer constraints; false, otherwise.

Definition at line 631 of file Formula.h.

Here is the call graph for this function:

◆ is_literal()

template<typename Pol >
bool carl::Formula< Pol >::is_literal ( ) const
inline

Definition at line 571 of file Formula.h.

Here is the call graph for this function:
Here is the caller graph for this function:

◆ is_nary()

template<typename Pol >
bool carl::Formula< Pol >::is_nary ( ) const
inline
Returns
true, if the type of this formulas allows n-ary combinations of sub-formulas, for an arbitrary n.

Definition at line 598 of file Formula.h.

Here is the caller graph for this function:

◆ is_only_propositional()

template<typename Pol >
bool carl::Formula< Pol >::is_only_propositional ( ) const
inline
Returns
true, if this formula is propositional; false, otherwise.

Definition at line 643 of file Formula.h.

Here is the call graph for this function:

◆ is_real_constraint_conjunction()

template<typename Pol >
bool carl::Formula< Pol >::is_real_constraint_conjunction ( ) const
inline
Returns
true, if this formula is a conjunction of real constraints; false, otherwise.

Definition at line 619 of file Formula.h.

Here is the call graph for this function:

◆ is_true()

template<typename Pol >
bool carl::Formula< Pol >::is_true ( ) const
inline
Returns
true, if this formula represents TRUE.

Definition at line 286 of file Formula.h.

Here is the caller graph for this function:

◆ logic()

template<typename Pol >
Logic carl::Formula< Pol >::logic ( ) const
inline

Definition at line 652 of file Formula.h.

Here is the call graph for this function:

◆ negated()

template<typename Pol >
Formula carl::Formula< Pol >::negated ( ) const
inline

Definition at line 316 of file Formula.h.

Here is the call graph for this function:
Here is the caller graph for this function:

◆ operator!()

template<typename Pol >
Formula carl::Formula< Pol >::operator! ( ) const
inline

Definition at line 787 of file Formula.h.

Here is the call graph for this function:

◆ operator!=()

template<typename Pol >
bool carl::Formula< Pol >::operator!= ( const Formula< Pol > &  _formula) const
inline
Parameters
_formulaThe formula to compare with.
Returns
true, if this formula and the given formula are not equal.

Definition at line 738 of file Formula.h.

◆ operator<()

template<typename Pol >
bool carl::Formula< Pol >::operator< ( const Formula< Pol > &  _formula) const
inline
Parameters
_formulaThe formula to compare with.
Returns
true, if the id of this formula is less than the id of the given one.

Definition at line 747 of file Formula.h.

Here is the call graph for this function:

◆ operator<=()

template<typename Pol >
bool carl::Formula< Pol >::operator<= ( const Formula< Pol > &  _formula) const
inline
Parameters
_formulaThe formula to compare with.
Returns
true, if the id of this formula is less or equal than the id of the given one.

Definition at line 769 of file Formula.h.

Here is the call graph for this function:

◆ operator=() [1/2]

template<typename Pol >
Formula& carl::Formula< Pol >::operator= ( const Formula< Pol > &  _formula)
inline

Definition at line 219 of file Formula.h.

Here is the call graph for this function:

◆ operator=() [2/2]

template<typename Pol >
Formula& carl::Formula< Pol >::operator= ( Formula< Pol > &&  _formula)
inline

Definition at line 229 of file Formula.h.

Here is the call graph for this function:

◆ operator==()

template<typename Pol >
bool carl::Formula< Pol >::operator== ( const Formula< Pol > &  _formula) const
inline
Parameters
_formulaThe formula to compare with.
Returns
true, if this formula and the given formula are equal; false, otherwise.

Definition at line 729 of file Formula.h.

◆ operator>()

template<typename Pol >
bool carl::Formula< Pol >::operator> ( const Formula< Pol > &  _formula) const
inline
Parameters
_formulaThe formula to compare with.
Returns
true, if the id of this formula is greater than the id of the given one.

Definition at line 758 of file Formula.h.

Here is the call graph for this function:

◆ operator>=()

template<typename Pol >
bool carl::Formula< Pol >::operator>= ( const Formula< Pol > &  _formula) const
inline
Parameters
_formulaThe formula to compare with.
Returns
true, if the id of this formula is greater or equal than the id of the given one.

Definition at line 780 of file Formula.h.

Here is the call graph for this function:

◆ premise()

template<typename Pol >
const Formula& carl::Formula< Pol >::premise ( ) const
inline
Returns
A constant reference to the premise, in case this formula is an implication.

Definition at line 344 of file Formula.h.

Here is the caller graph for this function:

◆ properties()

template<typename Pol >
const Condition& carl::Formula< Pol >::properties ( ) const
inline
Returns
The bit-vector representing the propositions of this formula. For further information see the Condition class.

Definition at line 302 of file Formula.h.

Here is the caller graph for this function:

◆ property_holds()

template<typename Pol >
bool carl::Formula< Pol >::property_holds ( const Condition _property) const
inline

Checks if the given property holds for this formula.

(Very cheap operation which only relies on bit checks)

Parameters
_propertyThe property to check this formula for.
Returns
true, if the given property holds for this formula; false, otherwise.

Definition at line 555 of file Formula.h.

Here is the caller graph for this function:

◆ quantified_aux_formula()

template<typename Pol >
const Formula& carl::Formula< Pol >::quantified_aux_formula ( ) const
inline

Definition at line 412 of file Formula.h.

Here is the caller graph for this function:

◆ quantified_formula()

template<typename Pol >
const Formula& carl::Formula< Pol >::quantified_formula ( ) const
inline
Returns
A constant reference to the bound formula, in case this formula is a quantified formula.

Definition at line 402 of file Formula.h.

Here is the caller graph for this function:

◆ quantified_variables()

template<typename Pol >
const std::vector<carl::Variable>& carl::Formula< Pol >::quantified_variables ( ) const
inline
Returns
A constant reference to the quantifed variables, in case this formula is a quantified formula.

Definition at line 389 of file Formula.h.

Here is the caller graph for this function:

◆ rbegin()

template<typename Pol >
const_reverse_iterator carl::Formula< Pol >::rbegin ( ) const
inline
Returns
A constant reverse iterator to the beginning of the list of sub-formulas of this formula.

Definition at line 522 of file Formula.h.

Here is the call graph for this function:

◆ remove_negations()

template<typename Pol >
const Formula& carl::Formula< Pol >::remove_negations ( ) const
inline

Definition at line 325 of file Formula.h.

Here is the call graph for this function:
Here is the caller graph for this function:

◆ rend()

template<typename Pol >
const_reverse_iterator carl::Formula< Pol >::rend ( ) const
inline
Returns
A constant reverse iterator to the end of the list of sub-formulas of this formula.

Definition at line 531 of file Formula.h.

Here is the call graph for this function:

◆ second_case()

template<typename Pol >
const Formula& carl::Formula< Pol >::second_case ( ) const
inline
Returns
A constant reference to the else-case, in case this formula is an ite-expression of formulas.

Definition at line 380 of file Formula.h.

Here is the caller graph for this function:

◆ set_activity()

template<typename Pol >
void carl::Formula< Pol >::set_activity ( double  _activity) const
inline

Sets the activity to the given value.

Parameters
_activityThe value to set the activity to.

Definition at line 253 of file Formula.h.

◆ size()

template<typename Pol >
size_t carl::Formula< Pol >::size ( ) const
inline
Returns
The number of sub-formulas of this formula.

Definition at line 477 of file Formula.h.

Here is the caller graph for this function:

◆ subformula()

template<typename Pol >
const Formula& carl::Formula< Pol >::subformula ( ) const
inline
Returns
A constant reference to the only sub-formula, in case this formula is an negation.

Definition at line 335 of file Formula.h.

Here is the caller graph for this function:

◆ subformulas()

template<typename Pol >
const Formulas<Pol>& carl::Formula< Pol >::subformulas ( ) const
inline
Returns
A constant reference to the list of sub-formulas of this formula. Note, that this formula has to be a Boolean combination, if you invoke this method.

Definition at line 422 of file Formula.h.

Here is the call graph for this function:
Here is the caller graph for this function:

◆ type()

template<typename Pol >
FormulaType carl::Formula< Pol >::type ( ) const
inline
Returns
The type of this formula.

Definition at line 262 of file Formula.h.

Here is the caller graph for this function:

◆ u_equality()

template<typename Pol >
const UEquality& carl::Formula< Pol >::u_equality ( ) const
inline
Returns
A constant reference to the uninterpreted equality represented by this formula. Note, that this formula has to be of type UEQ, if you invoke this method.

Definition at line 468 of file Formula.h.

Here is the caller graph for this function:

◆ variable_assignment()

template<typename Pol >
const VariableAssignment<Pol>& carl::Formula< Pol >::variable_assignment ( ) const
inline

Definition at line 443 of file Formula.h.

Here is the caller graph for this function:

◆ variable_comparison()

template<typename Pol >
const VariableComparison<Pol>& carl::Formula< Pol >::variable_comparison ( ) const
inline

Definition at line 438 of file Formula.h.

Here is the caller graph for this function:

◆ variables()

template<typename Pol >
const Variables& carl::Formula< Pol >::variables ( ) const
inline

Definition at line 307 of file Formula.h.

Here is the call graph for this function:
Here is the caller graph for this function:

Friends And Related Function Documentation

◆ FormulaContent< Pol >

template<typename Pol >
friend class FormulaContent< Pol >
friend

Definition at line 798 of file Formula.h.

◆ FormulaPool< Pol >

template<typename Pol >
friend class FormulaPool< Pol >
friend

Definition at line 798 of file Formula.h.

◆ operator<<

template<typename Pol >
template<typename P >
std::ostream& operator<< ( std::ostream &  os,
const Formula< P > &  f 
)
friend

The output operator of a formula.

Parameters
osThe stream to print on.
fThe formula to print.

Definition at line 798 of file Formula.h.

Field Documentation

◆ mpContent

template<typename Pol >
const FormulaContent<Pol>* carl::Formula< Pol >::mpContent
private

The content of this formula.

Definition at line 72 of file Formula.h.


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