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

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

#include <UFManager.h>

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

Public Member Functions

const auto & ufContents () const
 
const auto & ufIDMap () const
 
const std::string & get_name (const UninterpretedFunction &uf) const
 
const std::vector< Sort > & getDomain (const UninterpretedFunction &uf) const
 
Sort getCodomain (const UninterpretedFunction &uf) const
 
UninterpretedFunction newUninterpretedFunction (std::string &&name, std::vector< Sort > &&domain, Sort codomain)
 Gets the uninterpreted function with the given name, domain, arguments and codomain. More...
 

Static Public Member Functions

static UFManager & getInstance ()
 Returns the single instance of this class by reference. More...
 

Private Member Functions

 UFManager ()
 Constructs an uninterpreted functions manager. More...
 
UninterpretedFunction newUF (std::unique_ptr< UFContent > &&sc)
 Tries to add the given uninterpreted function's content to the so far stored uninterpreted function's contents. More...
 
const auto & getUF (const UninterpretedFunction &uf) const
 

Private Attributes

friend Singleton< UFManager >
 
FastPointerMap< UFContent, std::size_t > mUFIdMap
 Stores all instantiated uninterpreted function's contents and maps them to their unique id. More...
 
std::vector< std::unique_ptr< UFContent > > mUFs
 Maps the unique ids to the instantiated uninterpreted function's content. More...
 

Detailed Description

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

Definition at line 116 of file UFManager.h.

Constructor & Destructor Documentation

◆ UFManager()

carl::UFManager::UFManager ( )
inlineprivate

Constructs an uninterpreted functions manager.

Definition at line 128 of file UFManager.h.

Member Function Documentation

◆ get_name()

const std::string& carl::UFManager::get_name ( const UninterpretedFunction &  uf) const
inline
Parameters
ufAn uninterpreted function.
Returns
The name of the uninterpreted function of the given uninterpreted function.

Definition at line 159 of file UFManager.h.

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

◆ getCodomain()

Sort carl::UFManager::getCodomain ( const UninterpretedFunction &  uf) const
inline
Parameters
ufAn uninterpreted function.
Returns
The codomain of the uninterpreted function of the given uninterpreted function.

Definition at line 175 of file UFManager.h.

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

◆ getDomain()

const std::vector<Sort>& carl::UFManager::getDomain ( const UninterpretedFunction &  uf) const
inline
Parameters
ufAn uninterpreted function.
Returns
The domain of the uninterpreted function of the given uninterpreted function.

Definition at line 167 of file UFManager.h.

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

◆ getInstance()

static UFManager & carl::Singleton< UFManager >::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.

◆ getUF()

const auto& carl::UFManager::getUF ( const UninterpretedFunction &  uf) const
inlineprivate

Definition at line 141 of file UFManager.h.

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

◆ newUF()

UninterpretedFunction carl::UFManager::newUF ( std::unique_ptr< UFContent > &&  sc)
private

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

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

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

Definition at line 13 of file UFManager.cpp.

Here is the caller graph for this function:

◆ newUninterpretedFunction()

UninterpretedFunction carl::UFManager::newUninterpretedFunction ( std::string &&  name,
std::vector< Sort > &&  domain,
Sort  codomain 
)
inline

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

Parameters
nameThe name of the uninterpreted function of the uninterpreted function to get.
domainThe domain of the uninterpreted function of the uninterpreted function to get.
codomainThe codomain of the uninterpreted function of the uninterpreted function to get.
Returns
The resulting uninterpreted function.

Definition at line 186 of file UFManager.h.

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

◆ ufContents()

const auto& carl::UFManager::ufContents ( ) const
inline

Definition at line 148 of file UFManager.h.

◆ ufIDMap()

const auto& carl::UFManager::ufIDMap ( ) const
inline

Definition at line 151 of file UFManager.h.

Field Documentation

◆ mUFIdMap

FastPointerMap<UFContent, std::size_t> carl::UFManager::mUFIdMap
private

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

Definition at line 121 of file UFManager.h.

◆ mUFs

std::vector<std::unique_ptr<UFContent> > carl::UFManager::mUFs
private

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

Definition at line 123 of file UFManager.h.

◆ Singleton< UFManager >

friend carl::UFManager::Singleton< UFManager >
private

Definition at line 117 of file UFManager.h.

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