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