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 cvc5.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.

Wrapper class for the C++ class cvc5::parser::SymbolManager.

getDeclaredSorts()

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

Returns:

The declared sorts.

getDeclaredTerms()

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.

getLogic()

Note

Asserts isLogicSet().

Returns:

The logic used by this symbol manager.

getNamedTerms()

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.

isLogicSet()

Returns:

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