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.

std::map<Term, std::string> getNamedTerms() const

Get a mapping from terms to names that have been given to them via the :named attribute.

Returns:

A map of the named terms to their names.

Friends

friend class internal::InteractiveShell
friend class main::CommandExecutor