carl  24.04
Computer ARithmetic Library
Public Member Functions | Private Types | Private Attributes
carl::UTerm Class Reference

Implements an uninterpreted term, that is either an uninterpreted variable or an uninterpreted function instance. More...

#include <UTerm.h>

Public Member Functions

 UTerm ()=default
 Default constructor. More...
 
 UTerm (UVariable v)
 
 UTerm (UFInstance ufi)
 
 UTerm (const Super &term)
 Constructs an uninterpreted term. More...
 
const auto & asVariant () const
 
bool isUVariable () const
 
bool isUFInstance () const
 
UVariable asUVariable () const
 
UFInstance asUFInstance () const
 
Sort domain () const
 
std::size_t complexity () const
 
void gatherVariables (carlVariables &vars) const
 
void gatherUFs (std::set< UninterpretedFunction > &ufs) const
 

Private Types

using Super = std::variant< UVariable, UFInstance >
 

Private Attributes

Super mTerm
 

Detailed Description

Implements an uninterpreted term, that is either an uninterpreted variable or an uninterpreted function instance.

Definition at line 22 of file UTerm.h.

Member Typedef Documentation

◆ Super

using carl::UTerm::Super = std::variant<UVariable, UFInstance>
private

Definition at line 23 of file UTerm.h.

Constructor & Destructor Documentation

◆ UTerm() [1/4]

carl::UTerm::UTerm ( )
default

Default constructor.

◆ UTerm() [2/4]

carl::UTerm::UTerm ( UVariable  v)
inline

Definition at line 32 of file UTerm.h.

◆ UTerm() [3/4]

carl::UTerm::UTerm ( UFInstance  ufi)
inline

Definition at line 33 of file UTerm.h.

◆ UTerm() [4/4]

carl::UTerm::UTerm ( const Super &  term)
inlineexplicit

Constructs an uninterpreted term.

Parameters
term

Definition at line 39 of file UTerm.h.

Member Function Documentation

◆ asUFInstance()

UFInstance carl::UTerm::asUFInstance ( ) const
inline
Returns
The stored term as UFInstance.

Definition at line 69 of file UTerm.h.

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

◆ asUVariable()

UVariable carl::UTerm::asUVariable ( ) const
inline
Returns
The stored term as UVariable.

Definition at line 62 of file UTerm.h.

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

◆ asVariant()

const auto& carl::UTerm::asVariant ( ) const
inline

Definition at line 41 of file UTerm.h.

Here is the caller graph for this function:

◆ complexity()

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

Definition at line 23 of file UTerm.cpp.

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

◆ domain()

Sort carl::UTerm::domain ( ) const
Returns
The domain of this uninterpreted term.

Definition at line 16 of file UTerm.cpp.

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

◆ gatherUFs()

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

Definition at line 37 of file UTerm.cpp.

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

◆ gatherVariables()

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

Definition at line 30 of file UTerm.cpp.

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

◆ isUFInstance()

bool carl::UTerm::isUFInstance ( ) const
inline
Returns
true, if the stored term is a UFInstance.

Definition at line 55 of file UTerm.h.

Here is the caller graph for this function:

◆ isUVariable()

bool carl::UTerm::isUVariable ( ) const
inline
Returns
true, if the stored term is a UVariable.

Definition at line 48 of file UTerm.h.

Here is the caller graph for this function:

Field Documentation

◆ mTerm

Super carl::UTerm::mTerm
private

Definition at line 24 of file UTerm.h.

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