#include <FormulaContent.h>

Inheritance diagram for carl::FormulaContent< Pol >:

Collaboration diagram for carl::FormulaContent< Pol >:

[legend]

Public Member Functions
	~FormulaContent ()
	Destructor. More...

std::size_t	hash () const

std::size_t	id () const

bool	is_nary () const

bool	operator== (const FormulaContent &_content) const

Private Member Functions
	FormulaContent ()=delete

	FormulaContent (const FormulaContent &)=delete

	FormulaContent (FormulaContent &&o)

	FormulaContent (FormulaType _type, std::size_t _id=0)
	Constructs the formula (true), if the given bool is true and the formula (false) otherwise. More...

	FormulaContent (Variable _variable)
	Constructs a formula being a variable. More...

	FormulaContent (Constraint< Pol > &&_constraint)
	Constructs a formula being a constraint. More...

	FormulaContent (VariableComparison< Pol > &&_variableComparison)

	FormulaContent (VariableAssignment< Pol > &&_variableAssignment)

	FormulaContent (BVConstraint &&_constraint)
	Constructs a formula being a bitvector constraint. More...

	FormulaContent (UEquality &&_ueq)
	Constructs a formula being an uninterpreted equality. More...

	FormulaContent (FormulaType _type, Formula< Pol > &&_subformula)
	Constructs a formula of the given type with a single subformula. More...

	FormulaContent (FormulaType _type, const std::initializer_list< Formula< Pol >> &_subformula)

	FormulaContent (FormulaType _type, Formulas< Pol > &&_subformula)

	FormulaContent (FormulaType _type, std::vector< carl::Variable > &&_vars, const Formula< Pol > &_term)
	Constructs a quantifier expression: (exists (vars) term) or (forall (vars) term) More...

Private Attributes
size_t	mHash = 0
	The hash value. More...

size_t	mId = 0
	The unique id. More...

double	mActivity = 0.0
	The activity for this formula, which means, how much is this formula involved in the solving procedure. More...

size_t	mUsages = 0
	The number of formulas existing with this content. More...

FormulaType	mType
	The type of this formula. More...

std::variant< carl::Variable, Constraint< Pol >, VariableComparison< Pol >, VariableAssignment< Pol >, BVConstraint, UEquality, Formula< Pol >, Formulas< Pol >, QuantifierContent< Pol > >	mContent
	The content of this formula. More...

const FormulaContent< Pol > *	mNegation = nullptr
	The negation. More...

Condition	mProperties
	The propositions of this formula. More...

Variables *	mpVariables = nullptr
	Container collecting the variables which occur in this formula. More...

Friends
class	Formula< Pol >

class	FormulaPool< Pol >

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

Detailed Description

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

Definition at line 124 of file FormulaContent.h.

Constructor & Destructor Documentation

◆ FormulaContent() [1/14]

template<typename Pol >

carl::FormulaContent< Pol >::FormulaContent ( )

privatedelete

◆ FormulaContent() [2/14]

template<typename Pol >

carl::FormulaContent< Pol >::FormulaContent ( const FormulaContent< Pol > & )

privatedelete

◆ FormulaContent() [3/14]

template<typename Pol >

carl::FormulaContent< Pol >::FormulaContent ( FormulaContent< Pol > && o )

inlineprivate

Definition at line 169 of file FormulaContent.h.

◆ FormulaContent() [4/14]

template<typename Pol >

carl::FormulaContent< Pol >::FormulaContent	(	FormulaType	_type,
		std::size_t	_id = `0`
	)

private

Constructs the formula (true), if the given bool is true and the formula (false) otherwise.

Parameters

_true	Specifies whether to create the formula (true) or (false).
_id	A unique id of the formula to create.

◆ FormulaContent() [5/14]

template<typename Pol >

carl::FormulaContent< Pol >::FormulaContent ( Variable _variable )

private

Constructs a formula being a variable.

Parameters

_variable

◆ FormulaContent() [6/14]

template<typename Pol >

carl::FormulaContent< Pol >::FormulaContent ( Constraint< Pol > && _constraint )

private

Constructs a formula being a constraint.

Parameters

_constraint The pointer to the constraint.

◆ FormulaContent() [7/14]

template<typename Pol >

carl::FormulaContent< Pol >::FormulaContent ( VariableComparison< Pol > && _variableComparison )

private

◆ FormulaContent() [8/14]

template<typename Pol >

carl::FormulaContent< Pol >::FormulaContent ( VariableAssignment< Pol > && _variableAssignment )

private

◆ FormulaContent() [9/14]

template<typename Pol >

carl::FormulaContent< Pol >::FormulaContent ( BVConstraint && _constraint )

private

Constructs a formula being a bitvector constraint.

Parameters

_constraint The pointer to the constraint.

◆ FormulaContent() [10/14]

template<typename Pol >

carl::FormulaContent< Pol >::FormulaContent ( UEquality && _ueq )

private

Constructs a formula being an uninterpreted equality.

Parameters

_ueq	The pointer to the constraint.

◆ FormulaContent() [11/14]

template<typename Pol >

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

private

Constructs a formula of the given type with a single subformula.

This is usually a negation.

◆ FormulaContent() [12/14]

template<typename Pol >

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

private

◆ FormulaContent() [13/14]

template<typename Pol >

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

private

◆ FormulaContent() [14/14]

template<typename Pol >

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

private

Constructs a quantifier expression: (exists (vars) term) or (forall (vars) term)

Parameters

_type	The type of the quantifier to construct.
_vars	The variables that are bound.
_term	The term in which the variables are bound.

◆ ~FormulaContent()

template<typename Pol >

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

inline

Destructor.

Definition at line 229 of file FormulaContent.h.

Member Function Documentation

◆ hash()

template<typename Pol >

std::size_t carl::FormulaContent< Pol >::hash ( ) const

inline

Definition at line 234 of file FormulaContent.h.

Here is the caller graph for this function:

◆ id()

template<typename Pol >

std::size_t carl::FormulaContent< Pol >::id ( ) const

inline

Definition at line 237 of file FormulaContent.h.

◆ is_nary()

template<typename Pol >

bool carl::FormulaContent< Pol >::is_nary ( ) const

inline

Definition at line 241 of file FormulaContent.h.

Here is the caller graph for this function:

◆ operator==()

template<typename Pol >

bool carl::FormulaContent< Pol >::operator== ( const FormulaContent< Pol > & _content ) const

Friends And Related Function Documentation

◆ Formula< Pol >

template<typename Pol >

friend class Formula< Pol >

friend

Definition at line 117 of file FormulaContent.h.

◆ FormulaPool< Pol >

template<typename Pol >

friend class FormulaPool< Pol >

friend

Definition at line 117 of file FormulaContent.h.

◆ operator<<

template<typename Pol >

template<typename P >

std::ostream& operator<<	(	std::ostream &	os,
		const FormulaContent< P > &	f
	)

friend

Field Documentation

◆ mActivity

template<typename Pol >

double carl::FormulaContent< Pol >::mActivity = 0.0

mutableprivate

The activity for this formula, which means, how much is this formula involved in the solving procedure.

Definition at line 139 of file FormulaContent.h.

◆ mContent

template<typename Pol >

std::variant<carl::Variable, Constraint<Pol>, VariableComparison<Pol>, VariableAssignment<Pol>, BVConstraint, UEquality, Formula<Pol>, Formulas<Pol>, QuantifierContent<Pol> > carl::FormulaContent< Pol >::mContent

private

The content of this formula.

Definition at line 153 of file FormulaContent.h.

◆ mHash

template<typename Pol >

size_t carl::FormulaContent< Pol >::mHash = 0

private

The hash value.

Definition at line 135 of file FormulaContent.h.

◆ mId

template<typename Pol >

size_t carl::FormulaContent< Pol >::mId = 0

private

The unique id.

Definition at line 137 of file FormulaContent.h.

◆ mNegation

template<typename Pol >

const FormulaContent<Pol>* carl::FormulaContent< Pol >::mNegation = nullptr

private

The negation.

Definition at line 155 of file FormulaContent.h.

◆ mProperties

template<typename Pol >

Condition carl::FormulaContent< Pol >::mProperties

private

The propositions of this formula.

Definition at line 157 of file FormulaContent.h.

◆ mpVariables

template<typename Pol >

Variables* carl::FormulaContent< Pol >::mpVariables = nullptr

mutableprivate

Container collecting the variables which occur in this formula.

Definition at line 165 of file FormulaContent.h.

◆ mType

template<typename Pol >

FormulaType carl::FormulaContent< Pol >::mType

private

The type of this formula.

Definition at line 143 of file FormulaContent.h.

◆ mUsages

template<typename Pol >

size_t carl::FormulaContent< Pol >::mUsages = 0

mutableprivate

The number of formulas existing with this content.

Definition at line 141 of file FormulaContent.h.

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

carl-formula/formula/FormulaContent.h

Public Member Functions

Private Member Functions

Private Attributes

Friends

Detailed Description

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

Constructor & Destructor Documentation

◆ FormulaContent() [1/14]

◆ FormulaContent() [2/14]

◆ FormulaContent() [3/14]

◆ FormulaContent() [4/14]

◆ FormulaContent() [5/14]

◆ FormulaContent() [6/14]

◆ FormulaContent() [7/14]

◆ FormulaContent() [8/14]

◆ FormulaContent() [9/14]

◆ FormulaContent() [10/14]

◆ FormulaContent() [11/14]

◆ FormulaContent() [12/14]

◆ FormulaContent() [13/14]

◆ FormulaContent() [14/14]

◆ ~FormulaContent()

Member Function Documentation

◆ hash()

◆ id()

◆ is_nary()

◆ operator==()

Friends And Related Function Documentation

◆ Formula< Pol >

◆ FormulaPool< Pol >

◆ operator<<

Field Documentation

◆ mActivity

◆ mContent

◆ mHash

◆ mId

◆ mNegation

◆ mProperties

◆ mpVariables

◆ mType

◆ mUsages

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