carl  24.04
Computer ARithmetic Library
carl::UFInstanceContent Class Reference

The actual content of an uninterpreted function instance. More...

#include <UFInstanceManager.h>

Collaboration diagram for carl::UFInstanceContent:

Public Member Functions

 UFInstanceContent ()=delete
 
 UFInstanceContent (const UFInstanceContent &)=delete
 
 UFInstanceContent (UFInstanceContent &&)=delete
 
 UFInstanceContent (const UninterpretedFunction &uf, std::vector< UTerm > &&args)
 Constructs the content of an uninterpreted function instance. More...
 
 UFInstanceContent (const UninterpretedFunction &uf, const std::vector< UTerm > &args)
 Constructs the content of an uninterpreted function instance. More...
 
const UninterpretedFunctionuninterpretedFunction () const
 
const std::vector< UTerm > & args () const
 
bool operator== (const UFInstanceContent &ufic) const
 
bool operator< (const UFInstanceContent &ufic) const
 

Private Attributes

UninterpretedFunction mUninterpretedFunction
 The underlying uninterpreted function of theinstance. More...
 
std::vector< UTermmArgs
 The uninterpreted function instance's arguments. More...
 

Friends

class UFInstanceManager
 

Detailed Description

The actual content of an uninterpreted function instance.

Definition at line 33 of file UFInstanceManager.h.

Constructor & Destructor Documentation

◆ UFInstanceContent() [1/5]

carl::UFInstanceContent::UFInstanceContent ( )
delete

◆ UFInstanceContent() [2/5]

carl::UFInstanceContent::UFInstanceContent ( const UFInstanceContent )
delete

◆ UFInstanceContent() [3/5]

carl::UFInstanceContent::UFInstanceContent ( UFInstanceContent &&  )
delete

◆ UFInstanceContent() [4/5]

carl::UFInstanceContent::UFInstanceContent ( const UninterpretedFunction uf,
std::vector< UTerm > &&  args 
)
inlineexplicit

Constructs the content of an uninterpreted function instance.

Parameters
ufThe underlying function of the uninterpreted function instance to construct.
argsThe arguments of the uninterpreted function instance to construct.

Definition at line 52 of file UFInstanceManager.h.

◆ UFInstanceContent() [5/5]

carl::UFInstanceContent::UFInstanceContent ( const UninterpretedFunction uf,
const std::vector< UTerm > &  args 
)
inlineexplicit

Constructs the content of an uninterpreted function instance.

Parameters
ufThe underlying function of the uninterpreted function instance to construct.
argsThe arguments of the uninterpreted function instance to construct.

Definition at line 61 of file UFInstanceManager.h.

Member Function Documentation

◆ args()

const std::vector<UTerm>& carl::UFInstanceContent::args ( ) const
inline
Returns
The arguments of the uninterpreted function instance.

Definition at line 75 of file UFInstanceManager.h.

Here is the caller graph for this function:

◆ operator<()

bool carl::UFInstanceContent::operator< ( const UFInstanceContent ufic) const
inline
Parameters
uficThe uninterpreted function instance's content to compare with.
Returns
true, if this uninterpreted function instance's content is less than the given one.

Definition at line 91 of file UFInstanceManager.h.

Here is the call graph for this function:

◆ operator==()

bool carl::UFInstanceContent::operator== ( const UFInstanceContent ufic) const
inline
Parameters
uficThe uninterpreted function instance's content to compare with.
Returns
true, if this uninterpreted function instance's content is less than the given one.

Definition at line 83 of file UFInstanceManager.h.

Here is the call graph for this function:

◆ uninterpretedFunction()

const UninterpretedFunction& carl::UFInstanceContent::uninterpretedFunction ( ) const
inline
Returns
The underlying function of the uninterpreted function instance

Definition at line 68 of file UFInstanceManager.h.

Here is the caller graph for this function:

Friends And Related Function Documentation

◆ UFInstanceManager

friend class UFInstanceManager
friend

Definition at line 34 of file UFInstanceManager.h.

Field Documentation

◆ mArgs

std::vector<UTerm> carl::UFInstanceContent::mArgs
private

The uninterpreted function instance's arguments.

Definition at line 40 of file UFInstanceManager.h.

◆ mUninterpretedFunction

UninterpretedFunction carl::UFInstanceContent::mUninterpretedFunction
private

The underlying uninterpreted function of theinstance.

Definition at line 38 of file UFInstanceManager.h.


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