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

void cvc5_sm_get_named_terms(Cvc5SymbolManager *sm, size_t *size, Cvc5Term *terms[], const char **names[])

Get the named terms that have been given to them via the :named attribute.

Note

The resulting terms and names array pointers are only valid until the next call to this function.

Parameters:

  • sm – The symbol manager instance.

  • size – The resulting size of terms and names.

  • terms – The resulting term that are mapped to the resulting names.

  • names – The resulting names.