Cvc5SymbolManager 

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

typedef struct Cvc5SymbolManager Cvc5SymbolManager 

Symbol manager. Internally, the symbol manager 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 cvc5_cmd_invoke() .

A symbol manager can be provided when constructing a Cvc5InputParser, in which case that input parser has symbols of this symbol manager preloaded.

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

Cvc5SymbolManager * cvc5_symbol_manager_new ( Cvc5TermManager * tm ) 

Construct a new instance of a cvc5 symbol manager.

Parameters :

tm – The associated term manager instance.

Returns :

The cvc5 symbol manager instance.

void cvc5_symbol_manager_delete ( Cvc5SymbolManager * sm ) 

Delete a cvc5 symbol manager instance.

Parameters :

sm – The symbol manager instance.

bool cvc5_sm_is_logic_set ( Cvc5SymbolManager * sm ) 

Determine if the logic of a given symbol manager has been set.

Parameters :

sm – The symbol manager instance.

Returns :

True if the logic has been set.

const char * cvc5_sm_get_logic ( Cvc5SymbolManager * sm ) 

Get the logic configured for a given symbol manager.

Note

Asserts cvc5_sm_is_logic_set() .

Note

The returned char* pointer is only valid until the next call to this function.

Parameters :

sm – The symbol manager instance.

Returns :

The configured logic.

const Cvc5Sort * cvc5_sm_get_declared_sorts ( Cvc5SymbolManager * sm , size_t * size ) 

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.

Parameters :

• sm – The symbol manager instance.

• size – The size of the resulting sorts array.

Returns :

The declared sorts.

const Cvc5Term * cvc5_sm_get_declared_terms ( Cvc5SymbolManager * sm , size_t * size ) 

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.

Parameters :

• sm – The symbol manager instance.

• size – The size of the resulting sorts array.

Returns :

The declared terms.terms