carl  24.04
Computer ARithmetic Library
Public Member Functions | Static Public Member Functions | Private Member Functions | Private Attributes
carl::UFInstanceManager Class Reference

Implements a manager for uninterpreted function instances, containing their actual contents and allocating their ids. More...

#include <UFInstanceManager.h>

Inheritance diagram for carl::UFInstanceManager:
Inheritance graph
[legend]
Collaboration diagram for carl::UFInstanceManager:
Collaboration graph
[legend]

Public Member Functions

const UninterpretedFunction & getUninterpretedFunction (const UFInstance &ufi) const
 
const std::vector< UTerm > & getArgs (const UFInstance &ufi) const
 
UFInstance newUFInstance (const UninterpretedFunction &uf, std::vector< UTerm > &&args)
 Gets the uninterpreted function instance with the given name, domain, arguments and codomain. More...
 
UFInstance newUFInstance (const UninterpretedFunction &uf, const std::vector< UTerm > &args)
 Gets the uninterpreted function instance with the given name, domain, arguments and codomain. More...
 

Static Public Member Functions

static bool argsCorrect (const UFInstanceContent &ufic)
 
static UFInstanceManager & getInstance ()
 Returns the single instance of this class by reference. More...
 

Private Member Functions

 UFInstanceManager ()
 Constructs an uninterpreted function instances manager. More...
 
 ~UFInstanceManager () override
 
UFInstance newUFInstance (std::unique_ptr< UFInstanceContent > &&ufic)
 Tries to add the given uninterpreted function instance's content to the so far stored uninterpreted function instance's contents. More...
 

Private Attributes

friend Singleton< UFInstanceManager >
 
FastPointerMap< UFInstanceContent, std::size_t > mUFInstanceIdMap
 Stores all instantiated uninterpreted function instance's contents and maps them to their unique id. More...
 
std::vector< std::unique_ptr< UFInstanceContent > > mUFInstances
 Maps the unique ids to the instantiated uninterpreted function instance's content. More...
 

Detailed Description

Implements a manager for uninterpreted function instances, containing their actual contents and allocating their ids.

Definition at line 144 of file UFInstanceManager.h.

Constructor & Destructor Documentation

◆ UFInstanceManager()

carl::UFInstanceManager::UFInstanceManager ( )
inlineprivate

Constructs an uninterpreted function instances manager.

Definition at line 156 of file UFInstanceManager.h.

◆ ~UFInstanceManager()

carl::UFInstanceManager::~UFInstanceManager ( )
inlineoverrideprivate

Definition at line 161 of file UFInstanceManager.h.

Member Function Documentation

◆ argsCorrect()

bool carl::UFInstanceManager::argsCorrect ( const UFInstanceContent &  ufic)
static
Returns
true, if the arguments domains coincide with those of the domain.

Definition at line 25 of file UFInstanceManager.cpp.

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

◆ getArgs()

const std::vector<UTerm>& carl::UFInstanceManager::getArgs ( const UFInstance &  ufi) const
inline
Parameters
ufiAn uninterpreted function instance.
Returns
The arguments of the given uninterpreted function instance.

Definition at line 190 of file UFInstanceManager.h.

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

◆ getInstance()

static UFInstanceManager & carl::Singleton< UFInstanceManager >::getInstance ( )
inlinestaticinherited

Returns the single instance of this class by reference.

If there is no instance yet, a new one is created.

Definition at line 45 of file Singleton.h.

◆ getUninterpretedFunction()

const UninterpretedFunction& carl::UFInstanceManager::getUninterpretedFunction ( const UFInstance &  ufi) const
inline
Parameters
ufiAn uninterpreted function instance.
Returns
The underlying uninterpreted function of the uninterpreted function of the given uninterpreted function instance.

Definition at line 180 of file UFInstanceManager.h.

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

◆ newUFInstance() [1/3]

UFInstance carl::UFInstanceManager::newUFInstance ( const UninterpretedFunction &  uf,
const std::vector< UTerm > &  args 
)
inline

Gets the uninterpreted function instance with the given name, domain, arguments and codomain.

Parameters
ufThe underlying function of the uninterpreted function instance to get.
argsThe arguments of the uninterpreted function instance to get.
Returns
The resulting uninterpreted function instance.

Definition at line 214 of file UFInstanceManager.h.

Here is the call graph for this function:

◆ newUFInstance() [2/3]

UFInstance carl::UFInstanceManager::newUFInstance ( const UninterpretedFunction &  uf,
std::vector< UTerm > &&  args 
)
inline

Gets the uninterpreted function instance with the given name, domain, arguments and codomain.

Parameters
ufThe underlying function of the uninterpreted function instance to get.
argsThe arguments of the uninterpreted function instance to get.
Returns
The resulting uninterpreted function instance.

Definition at line 202 of file UFInstanceManager.h.

Here is the call graph for this function:

◆ newUFInstance() [3/3]

UFInstance carl::UFInstanceManager::newUFInstance ( std::unique_ptr< UFInstanceContent > &&  ufic)
private

Tries to add the given uninterpreted function instance's content to the so far stored uninterpreted function instance's contents.

If it has already been stored, if will be deleted and the id of the already existing uninterpreted function instance's content will be used to create the returned uninterpreted function instance.

Parameters
uficThe uninterpreted function instance's content to store.
Returns
The uninterpreted function instance corresponding to the given content.

Definition at line 12 of file UFInstanceManager.cpp.

Here is the caller graph for this function:

Field Documentation

◆ mUFInstanceIdMap

FastPointerMap<UFInstanceContent, std::size_t> carl::UFInstanceManager::mUFInstanceIdMap
private

Stores all instantiated uninterpreted function instance's contents and maps them to their unique id.

Definition at line 149 of file UFInstanceManager.h.

◆ mUFInstances

std::vector<std::unique_ptr<UFInstanceContent> > carl::UFInstanceManager::mUFInstances
private

Maps the unique ids to the instantiated uninterpreted function instance's content.

Definition at line 151 of file UFInstanceManager.h.

◆ Singleton< UFInstanceManager >

friend carl::UFInstanceManager::Singleton< UFInstanceManager >
private

Definition at line 145 of file UFInstanceManager.h.

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