SymbolManager 

This class manages a symbol table and other meta-information pertaining to SMT-LIB v2 inputs (e.g., named assertions, declared functions, etc.).

class SymbolManager 

Symbol manager. Internally, this class manages a symbol table and other meta-information pertaining to SMT2 file inputs (e.g. named assertions, declared functions, etc.).

A symbol manager can be modified by invoking commands, see Command::invoke .

A symbol manager can be provided when constructing an InputParser , in which case that InputParser has symbols of this symbol manager preloaded.

The symbol manager’s interface is otherwise not publicly available.

Public Functions

SymbolManager ( cvc5 :: TermManager & tm ) 

Constructor.

Parameters :

tm – The associated term manager instance.

SymbolManager ( cvc5 :: Solver * slv ) 

Constructor.

Warning

This constructor is deprecated and replaced by SymbolManager::SymbolManager(TermManager&) . It will be removed in a future release.

Parameters :

slv – The solver instance.

~SymbolManager ( ) 

Destructor.

bool isLogicSet ( ) const 

Determine if the logic of this symbol manager has been set.

Returns :

True if the logic has been set.

const std :: string & getLogic ( ) const 

Get the logic configured for this symbol manager.

Note

Asserts isLogicSet() .

Returns :

The configured logic.

std :: vector < Sort > getDeclaredSorts ( ) const 

Get the list of sorts that have been declared via declare-sort commands. These are the sorts that are printed as part of a response to a get-model command.

Returns :

The declared sorts.

std :: vector < Term > getDeclaredTerms ( ) const 

Get the list of terms that have been declared via declare-fun and declare-const . These are the terms that are printed in response to a get-model command.

Returns :

The declared terms.

Friends

friend class internal::InteractiveShell

friend class main::CommandExecutor