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 >:

[legend]

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 (const UTerm &_lhs, const UTerm &_rhs, bool _negated)

	Formula (UEquality &&_eq)

	Formula (const UEquality &_eq)

	Formula (const Formula &_formula)

	Formula (Formula &&_formula) noexcept

	~Formula ()

Formula &	operator= (const Formula &_formula)

Formula &	operator= (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 Condition &	properties () const

const Variables &	variables () const

Formula	negated () const

Formula	base_formula () const

const Formula &	remove_negations () const

const Formula &	subformula () const

const Formula &	premise () const

const Formula &	conclusion () const

const Formula &	condition () const

const Formula &	first_case () const

const Formula &	second_case () const

const std::vector< carl::Variable > &	quantified_variables () const

const Formula &	quantified_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 BVConstraint &	bv_constraint () const

carl::Variable::Arg	boolean () const

const UEquality &	u_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 Formula &	back () 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/25]

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/25]

template<typename Pol >

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

inlineexplicit

Definition at line 98 of file Formula.h.

◆ Formula() [3/25]

template<typename Pol >

carl::Formula< Pol >::Formula ( Variable::Arg _booleanVar )

inlineexplicit

Definition at line 102 of file Formula.h.

◆ Formula() [4/25]

template<typename Pol >

carl::Formula< Pol >::Formula	(	const Pol &	_pol,
		Relation	_rel
	)

inlineexplicit

Definition at line 106 of file Formula.h.

◆ Formula() [5/25]

template<typename Pol >

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

inlineexplicit

Definition at line 110 of file Formula.h.

◆ Formula() [6/25]

template<typename Pol >

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

inlineexplicit

Definition at line 114 of file Formula.h.

◆ Formula() [7/25]

template<typename Pol >

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

inlineexplicit

Definition at line 118 of file Formula.h.

◆ Formula() [8/25]

template<typename Pol >

carl::Formula< Pol >::Formula ( const BVConstraint & _constraint )

inlineexplicit

Definition at line 122 of file Formula.h.

◆ Formula() [9/25]

template<typename Pol >

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

inlineexplicit

Definition at line 126 of file Formula.h.

◆ Formula() [10/25]

template<typename Pol >

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

inlineexplicit

Definition at line 130 of file Formula.h.

◆ Formula() [11/25]

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/25]

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/25]

template<typename Pol >

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

inlineexplicit

Definition at line 144 of file Formula.h.

◆ Formula() [14/25]

template<typename Pol >

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

inlineexplicit

Definition at line 150 of file Formula.h.

◆ Formula() [15/25]

template<typename Pol >

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

inlineexplicit

Definition at line 154 of file Formula.h.

◆ Formula() [16/25]

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/25]

template<typename Pol >

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

inlineexplicit

Definition at line 162 of file Formula.h.

◆ Formula() [18/25]

template<typename Pol >

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

inlineexplicit

Definition at line 166 of file Formula.h.

◆ Formula() [19/25]

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/25]

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/25]

template<typename Pol >

carl::Formula< Pol >::Formula	(	const UTerm &	_lhs,
		const UTerm &	_rhs,
		bool	_negated
	)

inlineexplicit

Definition at line 178 of file Formula.h.

◆ Formula() [22/25]

template<typename Pol >

carl::Formula< Pol >::Formula ( UEquality && _eq )

inlineexplicit

Definition at line 182 of file Formula.h.

◆ Formula() [23/25]

template<typename Pol >

carl::Formula< Pol >::Formula ( const UEquality & _eq )

inlineexplicit

Definition at line 186 of file Formula.h.

◆ Formula() [24/25]

template<typename Pol >

carl::Formula< Pol >::Formula ( const Formula< Pol > & _formula )

inline

Definition at line 190 of file Formula.h.

Here is the call graph for this function:

◆ Formula() [25/25]

template<typename Pol >

carl::Formula< Pol >::Formula ( Formula< Pol > && _formula )

inlinenoexcept

Definition at line 197 of file Formula.h.

◆ ~Formula()

template<typename Pol >

carl::Formula< Pol >::~Formula ( )

inline

Definition at line 203 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 235 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

_constraint	The 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 518 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 312 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 482 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 436 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 426 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 345 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 354 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 410 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

_formula The 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 690 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 469 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 491 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 363 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 262 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 270 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 541 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 558 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 563 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 585 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 286 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 609 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 549 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 576 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 621 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 597 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 278 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 630 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 308 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 765 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

_formula The formula to compare with.

Returns: true, if this formula and the given formula are not equal.

Definition at line 716 of file Formula.h.

◆ operator<()

template<typename Pol >

bool carl::Formula< Pol >::operator< ( const Formula< Pol > & _formula ) const

inline

Parameters

_formula The formula to compare with.

Returns: true, if the id of this formula is less than the id of the given one.

Definition at line 725 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

_formula The 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 747 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 211 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 221 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

_formula The formula to compare with.

Returns: true, if this formula and the given formula are equal; false, otherwise.

Definition at line 707 of file Formula.h.

◆ operator>()

template<typename Pol >

bool carl::Formula< Pol >::operator> ( const Formula< Pol > & _formula ) const

inline

Parameters

_formula The formula to compare with.

Returns: true, if the id of this formula is greater than the id of the given one.

Definition at line 736 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

_formula The 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 758 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 336 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 294 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

_property The property to check this formula for.

Returns: true, if the given property holds for this formula; false, otherwise.

Definition at line 533 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 390 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 381 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 500 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 317 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 509 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 372 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

_activity The value to set the activity to.

Definition at line 245 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 455 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 327 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 400 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 254 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 446 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 421 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 416 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 299 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 776 of file Formula.h.

◆ FormulaPool< Pol >

template<typename Pol >

friend class FormulaPool< Pol >

friend

Definition at line 776 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

os	The stream to print on.
f	The formula to print.

Definition at line 776 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:

carl-formula/formula/Formula.h

Public Types

Public Member Functions

Static Public Member Functions

Private Member Functions

Static Private Member Functions

Private Attributes

Friends

Detailed Description

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

Member Typedef Documentation

◆ const_iterator

◆ const_reverse_iterator

◆ PolynomialType

Constructor & Destructor Documentation

◆ Formula() [1/25]

◆ Formula() [2/25]

◆ Formula() [3/25]

◆ Formula() [4/25]

◆ Formula() [5/25]

◆ Formula() [6/25]

◆ Formula() [7/25]

◆ Formula() [8/25]

◆ Formula() [9/25]

◆ Formula() [10/25]

◆ Formula() [11/25]

◆ Formula() [12/25]

◆ Formula() [13/25]

◆ Formula() [14/25]

◆ Formula() [15/25]

◆ Formula() [16/25]

◆ Formula() [17/25]

◆ Formula() [18/25]

◆ Formula() [19/25]

◆ Formula() [20/25]

◆ Formula() [21/25]

◆ Formula() [22/25]

◆ Formula() [23/25]

◆ Formula() [24/25]

◆ Formula() [25/25]

◆ ~Formula()

Member Function Documentation

◆ activity()

◆ addConstraintProperties()

◆ back()

◆ base_formula()

◆ begin()

◆ boolean()

◆ bv_constraint()

◆ conclusion()

◆ condition()

◆ constraint()

◆ contains()

◆ empty()

◆ end()

◆ first_case()

◆ hash()

◆ id()

◆ init()

◆ is_atom()

◆ is_boolean_combination()

◆ is_bound()

◆ is_constraint_conjunction()

◆ is_false()

◆ is_integer_constraint_conjunction()

◆ is_literal()

◆ is_nary()

◆ is_only_propositional()

◆ is_real_constraint_conjunction()

◆ is_true()

◆ logic()

◆ negated()

◆ operator!()

◆ operator!=()

◆ operator<()

◆ operator<=()

◆ operator=() [1/2]

◆ operator=() [2/2]

◆ operator==()

◆ operator>()

◆ operator>=()

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