Cvc5TermManager

This struct represents a cvc5 term manager instance.

Terms , Sorts and Ops are not tied to a Cvc5 but associated with a Cvc5TermManager instance, which can be shared between solver instances (and thus allows sharing of terms and sorts between solver instances).

Term kinds are defined via enum Cvc5Kind , and sort kinds via enum Cvc5SortKind .

Solver options are configured via cvc5_set_option() and queried via cvc5_get_option() (for more information on configuration options, see Options ). Information about a specific option can be retrieved via cvc5_get_option_info() (see Cvc5OptionInfo ).

typedef struct Cvc5TermManager Cvc5TermManager

A cvc5 term (and sort) manager.

Warning

doxygengroup: Cannot find group “c_cvc5termmanager” in doxygen xml output for project “cvc5_c” from directory: /home/runner/work/cvc5/cvc5/build-shared/docs/api/c/doxygen/xml

Sort Creation

Warning

doxygengroup: Cannot find group “c_sort_creation” in doxygen xml output for project “cvc5_c” from directory: /home/runner/work/cvc5/cvc5/build-shared/docs/api/c/doxygen/xml

Operator Creation

Cvc5Op cvc5_mk_op ( Cvc5TermManager * tm , Cvc5Kind kind , size_t size , const uint32_t idxs [ ] )

Create operator of Kind:

See Cvc5Kind for a description of the parameters.

Note

If idxs is empty, the Cvc5Op simply wraps the Cvc5Kind. The Cvc5Kind can be used in cvc5_mk_term directly without creating a Cvc5Op first.

Parameters :

  • tm – The term manager instance.

  • kind – The kind of the operator.

  • size – The number of indices of the operator.

  • idxs – The indices.

Cvc5Op cvc5_mk_op_from_str ( Cvc5TermManager * tm , Cvc5Kind kind , const char * arg )

Create operator of kind:

See CKind for a description of the parameters.

Parameters :

  • tm – The term manager instance.

  • kind – The kind of the operator.

  • arg – The string argument to this operator.

Term Creation

Warning

doxygengroup: Cannot find group “c_term_creation” in doxygen xml output for project “cvc5_c” from directory: /home/runner/work/cvc5/cvc5/build-shared/docs/api/c/doxygen/xml

Datatype Declaration Creation

Warning

doxygengroup: Cannot find group “c_dt_decl_creation” in doxygen xml output for project “cvc5_c” from directory: /home/runner/work/cvc5/cvc5/build-shared/docs/api/c/doxygen/xml

Datatype Constructor Declaration Creation

Warning

doxygengroup: Cannot find group “c_dt_cons_decl_creation” in doxygen xml output for project “cvc5_c” from directory: /home/runner/work/cvc5/cvc5/build-shared/docs/api/c/doxygen/xml