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

Friends

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