SymbolManager

This class manages a symbol table and other meta-information pertaining to SMT2 file 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::Solver *s)

~SymbolManager()

bool isLogicSet() const

Returns:

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

const std::string &getLogic() const

Note

Asserts isLogicSet().

Returns:

the logic used by this symbol manager

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