carl::UEquality Class Reference

Implements an uninterpreted equality, that is an equality of either two uninterpreted function instances, two uninterpreted variables, or an uninterpreted function instance and an uninterpreted variable. More...

#include <UEquality.h>

Collaboration diagram for carl::UEquality:

Public Member Functions
	UEquality ()=default
	UEquality (const UEquality &)=default
	UEquality (UEquality &&)=default
UEquality &	operator= (const UEquality &)=default
UEquality &	operator= (UEquality &&)=default
	UEquality (const UTerm &lhs, const UTerm &rhs, bool negated)
	Constructs an uninterpreted equality. More...
	UEquality (const UEquality &ueq, bool invert)
	Copies the given uninterpreted equality. More...
bool	negated () const
const UTerm &	lhs () const
const UTerm &	rhs () const
std::size_t	complexity () const
UEquality	negation () const
void	gatherVariables (carlVariables &vars) const
void	gatherUFs (std::set< UninterpretedFunction > &ufs) const
void	gatherUVariables (std::set< UVariable > &uvars) const

Private Attributes
bool	mNegated = false
	A flag indicating whether this equality shall hold (if being false) or its negation (if being true), hence the inequality, shall hold. More...
UTerm	mLhs
	The left-hand side of this uninterpreted equality. More...
UTerm	mRhs
	The right-hand side of this uninterpreted equality. More...

Detailed Description

Implements an uninterpreted equality, that is an equality of either two uninterpreted function instances, two uninterpreted variables, or an uninterpreted function instance and an uninterpreted variable.

Definition at line 23 of file UEquality.h.

Constructor & Destructor Documentation

UEquality() [1/5]

carl::UEquality::UEquality ( )

default

Here is the caller graph for this function:

UEquality() [2/5]

carl::UEquality::UEquality ( const UEquality &  )

default

UEquality() [3/5]

carl::UEquality::UEquality ( UEquality &&  )

default

UEquality() [4/5]

carl::UEquality::UEquality ( const UTerm &  lhs, const UTerm &  rhs, bool  negated  )

inline

Constructs an uninterpreted equality.

Parameters

negated	true, if the negation of this equality shall hold, which means that it is actually an inequality.
lhs	An uninterpreted variable, which is going to be the left-hand side of this uninterpreted equality.
rhs	An uninterpreted variable, which is going to be the right-hand side of this uninterpreted equality.

Definition at line 46 of file UEquality.h.

Here is the call graph for this function:

UEquality() [5/5]

carl::UEquality::UEquality ( const UEquality &  ueq, bool  invert  )

inline

Copies the given uninterpreted equality.

Parameters

ueq	The uninterpreted equality to copy.
invert	true, if the inverse of the given uninterpreted equality shall be constructed. (== -> != resp. != -> ==)

Definition at line 57 of file UEquality.h.

Member Function Documentation

complexity()

std::size_t carl::UEquality::complexity ( ) const

inline

Returns

An approximation of the complexity of this uninterpreted equality.

Definition at line 86 of file UEquality.h.

Here is the call graph for this function:

gatherUFs()

void carl::UEquality::gatherUFs ( std::set< UninterpretedFunction > &  ufs ) const

inline

Definition at line 101 of file UEquality.h.

Here is the call graph for this function:

gatherUVariables()

void carl::UEquality::gatherUVariables

(

std::set< UVariable > &

uvars

)

const

Definition at line 22 of file UEquality.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

gatherVariables()

void carl::UEquality::gatherVariables ( carlVariables &  vars ) const

inline

Definition at line 97 of file UEquality.h.

Here is the call graph for this function:

lhs()

const UTerm& carl::UEquality::lhs ( ) const

inline

Returns

The left-hand side of this equality.

Definition at line 72 of file UEquality.h.

Here is the caller graph for this function:

negated()

bool carl::UEquality::negated ( ) const

inline

Returns

true, if the negation of this equation shall hold, that is, it is actually an inequality.

Definition at line 65 of file UEquality.h.

Here is the caller graph for this function:

negation()

UEquality carl::UEquality::negation ( ) const

inline

Definition at line 93 of file UEquality.h.

Here is the call graph for this function:

operator=() [1/2]

UEquality& carl::UEquality::operator= ( const UEquality &  )

default

operator=() [2/2]

UEquality& carl::UEquality::operator= ( UEquality &&  )

default

rhs()

const UTerm& carl::UEquality::rhs ( ) const

inline

Returns

The right-hand side of this equality.

Definition at line 79 of file UEquality.h.

Here is the caller graph for this function:

Field Documentation

mLhs

UTerm carl::UEquality::mLhs

private

The left-hand side of this uninterpreted equality.

Definition at line 28 of file UEquality.h.

mNegated

bool carl::UEquality::mNegated = false

private

A flag indicating whether this equality shall hold (if being false) or its negation (if being true), hence the inequality, shall hold.

Definition at line 26 of file UEquality.h.

mRhs

UTerm carl::UEquality::mRhs

private

The right-hand side of this uninterpreted equality.

Definition at line 30 of file UEquality.h.

---

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

• carl-formula/uninterpreted/UEquality.h
• carl-formula/uninterpreted/UEquality.cpp