Implements a manager for sorts, containing the actual contents of these sort and allocating their ids. More...

#include <SortManager.h>

Inheritance diagram for carl::SortManager:

Collaboration diagram for carl::SortManager:

[legend]

Public Types
using	SortTemplate = std::pair< std::vector< std::string >, Sort >
	The type of a sort template, define by define-sort. More...

Public Member Functions
	SortManager (const SortManager &)=delete

	SortManager (SortManager &&)=delete

SortManager &	operator= (const SortManager &)=delete

SortManager &	operator= (SortManager &&)=delete

	~SortManager () noexcept override=default

void	clear ()

const std::string &	get_name (const Sort &sort) const

const std::vector< Sort > *	getParameters (const Sort &sort) const

const std::vector< std::size_t > *	getIndices (const Sort &sort) const

VariableType	getType (const Sort &sort) const

std::ostream &	print (std::ostream &os, const Sort &sort) const
	Prints the given sort on the given output stream. More...

void	exportDefinitions (std::ostream &os) const

Sort	getInterpreted (VariableType type) const

Sort	replace (const Sort &sort, const std::map< std::string, Sort > &parameters)
	Recursively replaces sorts within the given sort according to the mapping of sort names to sorts as declared by the given map. More...

bool	declare (const std::string &name, std::size_t arity)
	Adds a sort declaration. More...

bool	define (const std::string &name, const std::vector< std::string > &params, const Sort &sort)
	Adds a sort template definitions. More...

std::size_t	getArity (const Sort &sort) const

Sort	addInterpretedMapping (const Sort &sort, VariableType type)

Sort	addInterpretedSort (const std::string &name, VariableType type)

Sort	addInterpretedSort (const std::string &name, const std::vector< Sort > &parameters, VariableType type)

Sort	addSort (const std::string &name, VariableType type=VariableType::VT_UNINTERPRETED)

Sort	addSort (const std::string &name, const std::vector< Sort > &parameters, VariableType type=VariableType::VT_UNINTERPRETED)

void	makeSortIndexable (const Sort &sort, std::size_t indices, VariableType type)

bool	isInterpreted (const Sort &sort) const

Sort	index (const Sort &sort, const std::vector< std::size_t > &indices)

Sort	getSort (const std::string &name)
	Gets the sort with arity zero (thus it is maybe interpreted) corresponding the given name. More...

Sort	getSort (const std::string &name, const std::vector< Sort > &params)
	Gets the sort with arity greater than zero corresponding the given name and having the arguments of the given sorts. More...

Sort	getSort (const std::string &name, const std::vector< std::size_t > &indices)

Sort	getSort (const std::string &name, const std::vector< std::size_t > &indices, const std::vector< Sort > &params)

Static Public Member Functions
static SortManager &	getInstance ()
	Returns the single instance of this class by reference. More...

Private Member Functions
	SortManager ()
	Constructs a sort manager. More...

const SortContent &	getContent (const Sort &sort) const

bool	isSymbolFree (const std::string &name) const

Sort	getSort (std::unique_ptr< SortContent > &&content, VariableType type)

std::size_t	addSortContent (std::unique_ptr< SortContent > &&content, VariableType type)

VariableType	checkIndices (const SortContent &content, std::size_t count) const

Private Attributes
friend	Singleton< SortManager >

std::vector< std::unique_ptr< SortContent > >	mSorts
	Maps the unique ids to the sort content. More...

std::vector< VariableType >	mSortTypes
	Maps the unique ids to the sort types. More...

std::map< const SortContent , std::size_t, carl::less< const SortContent > >	mSortMap
	Maps the sort contents to unique ids. More...

std::map< std::string, std::size_t >	mDeclarations
	Stores all sort declarations invoked by a declare-sort. More...

std::map< std::string, SortTemplate >	mDefinitions
	Stores all sort definitions invoked by a define-sort. More...

std::map< Sort, std::pair< std::size_t, VariableType > >	mIndexable
	Stores all sorts that may become interpreted when indexed. More...

std::map< VariableType, Sort >	mInterpreted
	Maps variable types to actual sorts. More...

Detailed Description

Implements a manager for sorts, containing the actual contents of these sort and allocating their ids.

Definition at line 105 of file SortManager.h.

Member Typedef Documentation

◆ SortTemplate

using carl::SortManager::SortTemplate = std::pair<std::vector<std::string>, Sort>

The type of a sort template, define by define-sort.

Definition at line 110 of file SortManager.h.

Constructor & Destructor Documentation

◆ SortManager() [1/3]

carl::SortManager::SortManager ( )

inlineprivate

Constructs a sort manager.

Definition at line 133 of file SortManager.h.

Here is the call graph for this function:

◆ SortManager() [2/3]

carl::SortManager::SortManager ( const SortManager & )

delete

◆ SortManager() [3/3]

carl::SortManager::SortManager ( SortManager && )

delete

◆ ~SortManager()

carl::SortManager::~SortManager ( )

overridedefaultnoexcept

Member Function Documentation

◆ addInterpretedMapping()

Sort carl::SortManager::addInterpretedMapping	(	const Sort &	sort,
		VariableType	type
	)

inline

Definition at line 262 of file SortManager.h.

Here is the caller graph for this function:

◆ addInterpretedSort() [1/2]

Sort carl::SortManager::addInterpretedSort	(	const std::string &	name,
		const std::vector< Sort > &	parameters,
		VariableType	type
	)

inline

Definition at line 270 of file SortManager.h.

Here is the call graph for this function:

◆ addInterpretedSort() [2/2]

Sort carl::SortManager::addInterpretedSort	(	const std::string &	name,
		VariableType	type
	)

inline

Definition at line 267 of file SortManager.h.

Here is the call graph for this function:

◆ addSort() [1/2]

Sort carl::SortManager::addSort	(	const std::string &	name,
		const std::vector< Sort > &	parameters,
		VariableType	type = `VariableType::VT_UNINTERPRETED`
	)

Definition at line 77 of file SortManager.cpp.

Here is the call graph for this function:

◆ addSort() [2/2]

Sort carl::SortManager::addSort	(	const std::string &	name,
		VariableType	type = `VariableType::VT_UNINTERPRETED`
	)

Definition at line 73 of file SortManager.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ addSortContent()

std::size_t carl::SortManager::addSortContent	(	std::unique_ptr< SortContent > &&	content,
		VariableType	type
	)

inlineprivate

Definition at line 159 of file SortManager.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ checkIndices()

VariableType carl::SortManager::checkIndices	(	const SortContent &	content,
		std::size_t	count
	)		const

inlineprivate

Definition at line 166 of file SortManager.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ clear()

void carl::SortManager::clear ( )

inline

Definition at line 183 of file SortManager.h.

Here is the caller graph for this function:

◆ declare()

bool carl::SortManager::declare	(	const std::string &	name,
		std::size_t	arity
	)

Adds a sort declaration.

Parameters

name	The name of the declared sort.
arity	The arity of the declared sort.

Returns: true, if the given sort declaration has not been added before; false, otherwise.

Definition at line 54 of file SortManager.cpp.

Here is the call graph for this function:

◆ define()

bool carl::SortManager::define	(	const std::string &	name,
		const std::vector< std::string > &	params,
		const Sort &	sort
	)

Adds a sort template definitions.

Parameters

name	The name of the defined sort template.
params	The template parameter of the defined sort.
sort	The sort to instantiate into.

Returns: true, if the given sort template definition has not been added before; false, otherwise.

Definition at line 61 of file SortManager.cpp.

Here is the call graph for this function:

◆ exportDefinitions()

void carl::SortManager::exportDefinitions ( std::ostream & os ) const

Todo:: fix this

Definition at line 31 of file SortManager.cpp.

◆ get_name()

const std::string& carl::SortManager::get_name ( const Sort & sort ) const

inline

Parameters

sort A sort.

Returns: The name if the given sort.

Definition at line 199 of file SortManager.h.

Here is the call graph for this function:

◆ getArity()

size_t carl::SortManager::getArity ( const Sort & sort ) const

Parameters

sort	The sort to get the arity for.

Returns: The arity of the given sort.

Definition at line 67 of file SortManager.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ getContent()

const SortContent& carl::SortManager::getContent ( const Sort & sort ) const

inlineprivate

Definition at line 137 of file SortManager.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ getIndices()

const std::vector<std::size_t>* carl::SortManager::getIndices ( const Sort & sort ) const

inline

Definition at line 205 of file SortManager.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ getInstance()

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

◆ getInterpreted()

Sort carl::SortManager::getInterpreted ( VariableType type ) const

inline

Definition at line 224 of file SortManager.h.

◆ getParameters()

const std::vector<Sort>* carl::SortManager::getParameters ( const Sort & sort ) const

inline

Definition at line 202 of file SortManager.h.

Here is the call graph for this function:

◆ getSort() [1/5]

Sort carl::SortManager::getSort ( const std::string & name )

Gets the sort with arity zero (thus it is maybe interpreted) corresponding the given name.

Parameters

name	The name of the sort to get.

Returns: The resulting sort.

Definition at line 96 of file SortManager.cpp.

◆ getSort() [2/5]

Sort carl::SortManager::getSort	(	const std::string &	name,
		const std::vector< Sort > &	params
	)

Gets the sort with arity greater than zero corresponding the given name and having the arguments of the given sorts.

Parameters

name	The name of the sort to get.
params	The sort of the arguments of the sort to get.

Returns: The resulting sort.

Definition at line 107 of file SortManager.cpp.

Here is the call graph for this function:

◆ getSort() [3/5]

Sort carl::SortManager::getSort	(	const std::string &	name,
		const std::vector< std::size_t > &	indices
	)

Definition at line 135 of file SortManager.cpp.

Here is the call graph for this function:

◆ getSort() [4/5]

Sort carl::SortManager::getSort	(	const std::string &	name,
		const std::vector< std::size_t > &	indices,
		const std::vector< Sort > &	params
	)

Definition at line 139 of file SortManager.cpp.

Here is the call graph for this function:

◆ getSort() [5/5]

Sort carl::SortManager::getSort	(	std::unique_ptr< SortContent > &&	content,
		VariableType	type
	)

inlineprivate

Definition at line 151 of file SortManager.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ getType()

VariableType carl::SortManager::getType ( const Sort & sort ) const

inline

Definition at line 208 of file SortManager.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ index()

Sort carl::SortManager::index	(	const Sort &	sort,
		const std::vector< std::size_t > &	indices
	)

Definition at line 85 of file SortManager.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ isInterpreted()

bool carl::SortManager::isInterpreted ( const Sort & sort ) const

inline

Parameters

sort A sort.

Returns: true, if the given sort is interpreted.

Definition at line 281 of file SortManager.h.

Here is the call graph for this function:

◆ isSymbolFree()

bool carl::SortManager::isSymbolFree ( const std::string & name ) const

inlineprivate

Definition at line 142 of file SortManager.h.

Here is the caller graph for this function:

◆ makeSortIndexable()

void carl::SortManager::makeSortIndexable	(	const Sort &	sort,
		std::size_t	indices,
		VariableType	type
	)

Definition at line 81 of file SortManager.cpp.

◆ operator=() [1/2]

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

delete

◆ operator=() [2/2]

SortManager& carl::SortManager::operator= ( SortManager && )

delete

◆ print()

std::ostream & carl::SortManager::print	(	std::ostream &	os,
		const Sort &	sort
	)		const

Prints the given sort on the given output stream.

Parameters

os	The output stream to print the given sort on.
sort	The sort to print.

Returns: The output stream after printing the given sort on it.

Definition at line 13 of file SortManager.cpp.

Here is the call graph for this function:

◆ replace()

Sort carl::SortManager::replace	(	const Sort &	sort,
		const std::map< std::string, Sort > &	parameters
	)

Recursively replaces sorts within the given sort according to the mapping of sort names to sorts as declared by the given map.

Parameters

sort	The sort to replace sorts by sorts in.
parameters	The map of sort names to sorts.

Returns: The resulting sort.

Definition at line 41 of file SortManager.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

Field Documentation

◆ mDeclarations

std::map<std::string, std::size_t> carl::SortManager::mDeclarations

private

Stores all sort declarations invoked by a declare-sort.

Definition at line 122 of file SortManager.h.

◆ mDefinitions

std::map<std::string, SortTemplate> carl::SortManager::mDefinitions

private

Stores all sort definitions invoked by a define-sort.

Definition at line 124 of file SortManager.h.

◆ mIndexable

std::map<Sort, std::pair<std::size_t, VariableType> > carl::SortManager::mIndexable

private

Stores all sorts that may become interpreted when indexed.

Definition at line 126 of file SortManager.h.

◆ mInterpreted

std::map<VariableType, Sort> carl::SortManager::mInterpreted

private

Maps variable types to actual sorts.

Definition at line 128 of file SortManager.h.

◆ mSortMap

std::map<const SortContent*, std::size_t, carl::less<const SortContent*> > carl::SortManager::mSortMap

private

Maps the sort contents to unique ids.

Definition at line 120 of file SortManager.h.

◆ mSorts

std::vector<std::unique_ptr<SortContent> > carl::SortManager::mSorts

private

Maps the unique ids to the sort content.

Definition at line 116 of file SortManager.h.

◆ mSortTypes

std::vector<VariableType> carl::SortManager::mSortTypes

private

Maps the unique ids to the sort types.

Definition at line 118 of file SortManager.h.

◆ Singleton< SortManager >

friend carl::SortManager::Singleton< SortManager >

private

Definition at line 106 of file SortManager.h.

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

carl-formula/sort/SortManager.h
carl-formula/sort/SortManager.cpp

Public Types

Public Member Functions

Static Public Member Functions

Private Member Functions

Private Attributes

Detailed Description

Member Typedef Documentation

◆ SortTemplate

Constructor & Destructor Documentation

◆ SortManager() [1/3]

◆ SortManager() [2/3]

◆ SortManager() [3/3]

◆ ~SortManager()

Member Function Documentation

◆ addInterpretedMapping()

◆ addInterpretedSort() [1/2]

◆ addInterpretedSort() [2/2]

◆ addSort() [1/2]

◆ addSort() [2/2]

◆ addSortContent()

◆ checkIndices()

◆ clear()

◆ declare()

◆ define()

◆ exportDefinitions()

◆ get_name()

◆ getArity()

◆ getContent()

◆ getIndices()

◆ getInstance()

◆ getInterpreted()

◆ getParameters()

◆ getSort() [1/5]

◆ getSort() [2/5]

◆ getSort() [3/5]

◆ getSort() [4/5]

◆ getSort() [5/5]

◆ getType()

◆ index()

◆ isInterpreted()

◆ isSymbolFree()

◆ makeSortIndexable()

◆ operator=() [1/2]

◆ operator=() [2/2]

◆ print()

◆ replace()

Field Documentation

◆ mDeclarations

◆ mDefinitions

◆ mIndexable

◆ mInterpreted

◆ mSortMap

◆ mSorts

◆ mSortTypes

◆ Singleton< SortManager >