Cvc5Term

The Cvc5Term struct represents an arbitrary expression of any of the supported sorts. The list of all supported kinds of terms is given by the Cvc5Kind enum. The Cvc5Term struct provides functions for general inspection (e.g., comparison, retrieving the kind and sort, accessing sub-terms), but also functions for retrieving constant values for the supported theories (i.e., cvc5_term_is_*_value() and cvc5_term_get_*_value(), which returns the constant values in the best type standard C++ offers).

Additionally, a :cpp:tyep:`Cvc5Term` can be hashed (using cvc5_term_hash()) and represented as string (via cvc5_term_to_string()).

Cvc5Term instances are created via factory functions associated with a Cvc5TermManager instance, e.g., cvc5_mk_term() for generic terms of a specific kind and cvc5_mk_<type>() for constants, variables and values of a given type.

typedef struct cvc5_term_t *Cvc5Term

A cvc5 term.

Cvc5Term cvc5_term_copy(Cvc5Term term)

Make copy of term, increases reference counter of term.

Note

This step is optional and allows users to manage resources in a more fine-grained manner.

Parameters:

term – The term to copy.

Returns:

The same term with its reference count increased by one.

void cvc5_term_release(Cvc5Term term)

Release copy of term, decrements reference counter of term.

Note

This step is optional and allows users to release resources in a more fine-grained manner. Further, any API function that returns a copy that is owned by the callee of the function and thus, can be released.

Parameters:

term – The term to release.

bool cvc5_term_is_equal(Cvc5Term a, Cvc5Term b)

Compare two terms for syntactic equality.

Parameters:

• a – The first term.

• b – The second term.

Returns:

True if both term are syntactically identical.

bool cvc5_term_is_disequal(Cvc5Term a, Cvc5Term b)

Compare two terms for syntactic disequality.

Parameters:

• a – The first term.

• b – The second term.

Returns:

True if both term are syntactically disequal.

int64_t cvc5_term_compare(Cvc5Term a, Cvc5Term b)

Compare two terms for ordering.

Parameters:

• a – The first term.

• b – The second term.

Returns:

An integer value indicating the ordering: 0 if both terms are equal, -1 if a < b, and 1 if b > a.

size_t cvc5_term_get_num_children(Cvc5Term term)

Get the number of children of a given term.

Parameters:

term – The term.

Returns:

The number of children of this term.

Cvc5Term cvc5_term_get_child(Cvc5Term term, size_t index)

Get the child term of a given term at a given index.

Parameters:

• term – The term.

• index – The index of the child.

Returns:

The child term at the given index.

uint64_t cvc5_term_get_id(Cvc5Term term)

Get the id of a given term.

Parameters:

term – The term.

Returns:

The id of the term.

Cvc5Kind cvc5_term_get_kind(Cvc5Term term)

Get the kind of a given term.

Parameters:

term – The term.

Returns:

The kind of the term.

Cvc5Sort cvc5_term_get_sort(Cvc5Term term)

Get the sort of a given term.

Parameters:

term – The term.

Returns:

The sort of the term.

Cvc5Term cvc5_term_substitute_term(Cvc5Term term, Cvc5Term t, Cvc5Term replacement)

Replace a given term t with term replacement in a given term.

Note

This replacement is applied during a pre-order traversal and only once (it is not run until fixed point).

Parameters:

• term – The term.

• t – The term to replace.

• replacement – The term to replace it with.

Returns:

The result of replacing term with replacement in the term.

Cvc5Term cvc5_term_substitute_terms(Cvc5Term term, size_t size, const Cvc5Term terms[], const Cvc5Term replacements[])

Simultaneously replace given terms terms with terms replacements in a given term.

In the case that terms contains duplicates, the replacement earliest in the vector takes priority. For example, calling substitute on f(x,y) with terms = { x, z }, replacements = { g(z), w } results in the term f(g(z),y).

Note

Requires that terms and replacements are of equal size (they are interpreted as 1 : 1 mapping).

Note

This replacement is applied during a pre-order traversal and only once (it is not run until fixed point).

Parameters:

• term – The term.

• size – The size of terms and replacements.

• terms – The terms to replace.

• replacements – The replacement terms.

Returns:

The result of simultaneously replacing terms with replacements in the given term.

bool cvc5_term_has_op(Cvc5Term term)

Determine if a given term has an operator.

Parameters:

term – The term.

Returns:

True iff the term has an operator.

Cvc5Op cvc5_term_get_op(Cvc5Term term)

Get the operator of a term with an operator.

Note

Requires that the term has an operator (see cvc5_term_has_op()).

Parameters:

term – The term.

Returns:

The Op used to create the term.

bool cvc5_term_has_symbol(Cvc5Term term)

Determine if a given term has a symbol (a name).

For example, free constants and variables have symbols.

Parameters:

term – The term.

Returns:

True if the term has a symbol.

const char *cvc5_term_get_symbol(Cvc5Term term)

Get the symbol of a given term with a symbol.

The symbol of the term is the string that was provided when constructing it via cvc5_mk_const() or cvc5_mk_var().

Note

Requires that the term has a symbol (see cvc5_term_has_symbol()).

Note

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

Parameters:

term – The term.

Returns:

The raw symbol of the term.

const char *cvc5_term_to_string(Cvc5Term term)

Get a string representation of a given term.

Note

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

Parameters:

term – The term.

Returns:

A string representation of the term.

int32_t cvc5_term_get_real_or_integer_value_sign(Cvc5Term term)

Get the sign of a given integer or real value.

Note

Requires that given term is an integer or real value.

Parameters:

term – The value term.

Returns:

0 if the term is zero, -1 if the term is a negative real or integer value, 1 if the term is a positive real or integer value.

bool cvc5_term_is_int32_value(Cvc5Term term)

Determine if a given term is an int32 value.

Note

This will return true for integer constants and real constants that have integer value.

Parameters:

term – The term.

Returns:

True if the term is an integer value that fits within int32_t.

int32_t cvc5_term_get_int32_value(Cvc5Term term)

Get the int32_t representation of a given integral value.

Note

Requires that the term is an int32 value (see cvc5_term_is_int32_value()).

Parameters:

term – The term.

Returns:

The given term as int32_t value.

bool cvc5_term_is_uint32_value(Cvc5Term term)

Determine if a given term is an uint32 value.

Note

This will return true for integer constants and real constants that have integral value.

Returns:

True if the term is an integral value and fits within uint32_t.

uint32_t cvc5_term_get_uint32_value(Cvc5Term term)

Get the uint32_t representation of a given integral value.

Note

Requires that the term is an uint32 value (see cvc5_term_is_uint32_value()).

Parameters:

term – The term.

Returns:

The term as uint32_t value.

bool cvc5_term_is_int64_value(Cvc5Term term)

Determine if a given term is an int64 value.

Note

This will return true for integer constants and real constants that have integral value.

Parameters:

term – The term.

Returns:

True if the term is an integral value that fits within int64_t.

int64_t cvc5_term_get_int64_value(Cvc5Term term)

Get the int64_t representation of a given integral value.

Note

Requires that the term is an int64 value (see cvc5_term_is_int64_value()).

Parameters:

term – The term.

Returns:

The term as int64_t value.

bool cvc5_term_is_uint64_value(Cvc5Term term)

Determine if a given term is an uint64 value.

Note

This will return true for integer constants and real constants that have integral value.

Parameters:

term – The term.

Returns:

True if the term is an integral value that fits within uint64_t.

uint64_t cvc5_term_get_uint64_value(Cvc5Term term)

Get the uint64_t representation of a given integral value.

Note

Requires that the term is an uint64 value (see cvc5_term_is_uint64_value()).

Parameters:

term – The term.

Returns:

The term as uint64_t value.

bool cvc5_term_is_integer_value(Cvc5Term term)

Determine if a given term is an integral value.

Parameters:

term – The term.

Returns:

True if the term is an integer constant or a real constant that has an integral value.

const char *cvc5_term_get_integer_value(Cvc5Term term)

Get a string representation of a given integral value.

Note

Requires that the term is an integral value (see cvc5_term_is_integer_value()).

Note

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

Parameters:

term – The term.

Returns:

The integral term in (decimal) string representation.

bool cvc5_term_is_string_value(Cvc5Term term)

Determine if a given term is a string value.

Parameters:

term – The term.

Returns:

True if the term is a string value.

const wchar_t *cvc5_term_get_string_value(Cvc5Term term)

Get the native string representation of a string value.

Note

Requires that the term is a string value (see cvc5_term_is_string_value()).

Note

This is not to be confused with cvc5_term_to_string(), which returns some string representation of the term, whatever data it may hold.

Parameters:

term – The term.

Returns:

The string term as a native string value.

bool cvc5_term_is_real32_value(Cvc5Term term)

Determine if a given term is a rational value whose numerator fits into an int32 value and its denominator fits into a uint32 value.

Parameters:

term – The term.

Returns:

True if the term is a rational and its numerator and denominator fit into 32 bit integer values.

void cvc5_term_get_real32_value(Cvc5Term term, int32_t *num, uint32_t *den)

Get the 32 bit integer representations of the numerator and denominator of a rational value.

Note

Requires that the term is a rational value and its numerator and denominator fit into 32 bit integer values (see cvc5_term_is_real32_value()).

Parameters:

• term – The term.

• num – The resulting int32_t representation of the numerator.

• den – The resulting uint32_t representation of the denominator.

bool cvc5_term_is_real64_value(Cvc5Term term)

Determine if a given term is a rational value whose numerator fits into an int64 value and its denominator fits into a uint64 value.

Parameters:

term – The term.

Returns:

True if the term is a rational value whose numerator and denominator fit within int64_t and uint64_t, respectively.

void cvc5_term_get_real64_value(Cvc5Term term, int64_t *num, uint64_t *den)

Get the 64 bit integer representations of the numerator and denominator of a rational value.

Note

Requires that the term is a rational value and its numerator and denominator fit into 64 bit integer values (see cvc5_term_is_real64_value()).

Parameters:

• term – The term.

• num – The resulting int64_t representation of the numerator.

• den – The resulting uint64_t representation of the denominator.

bool cvc5_term_is_real_value(Cvc5Term term)

Determine if a given term is a rational value.

Note

A term of kind PI is not considered to be a real value.

Parameters:

term – The term.

Returns:

True if the term is a rational value.

const char *cvc5_term_get_real_value(Cvc5Term term)

Get a string representation of a given rational value.

Note

Requires that the term is a rational value (see cvc5_term_is_real_value()).

Note

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

Parameters:

term – The term.

Returns:

The representation of a rational value as a (rational) string.

bool cvc5_term_is_const_array(Cvc5Term term)

Determine if a given term is a constant array.

Parameters:

term – The term.

Returns:

True if the term is a constant array.

Cvc5Term cvc5_term_get_const_array_base(Cvc5Term term)

Determine the base (element stored at all indices) of a constant array.

Note

Requires that the term is a constant array (see isConstArray()).

Parameters:

term – The term.

Returns:

The base term.

bool cvc5_term_is_boolean_value(Cvc5Term term)

Determine if a given term is a Boolean value.

Parameters:

term – The term.

Returns:

True if the term is a Boolean value.

bool cvc5_term_get_boolean_value(Cvc5Term term)

Get the value of a Boolean term as a native Boolean value.

Note

Asserts cvc5_term_is_boolean_value().

Parameters:

term – The term.

Returns:

The representation of a Boolean value as a native Boolean value.

bool cvc5_term_is_bv_value(Cvc5Term term)

Determine if a given term is a bit-vector value.

Parameters:

term – The term.

Returns:

True if the term is a bit-vector value.

const char *cvc5_term_get_bv_value(Cvc5Term term, uint32_t base)

Get the string representation of a bit-vector value.

Note

Asserts cvc5_term_is_bv_value().

Note

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

Parameters:

• term – The term.

• base – 2 for binary, 10 for decimal, and 16 for hexadecimal.

Returns:

The string representation of a bit-vector value.

bool cvc5_term_is_ff_value(Cvc5Term term)

Determine if a given term is a finite field value.

Parameters:

term – The term.

Returns:

True if the term is a finite field value.

const char *cvc5_term_get_ff_value(Cvc5Term term)

Get the string representation of a finite field value (base 10).

Note

Asserts cvc5_term_is_ff_value().

Note

Uses the integer representative of smallest absolute value.

Note

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

Parameters:

term – The term.

Returns:

The string representation of the integer representation of the finite field value.

bool cvc5_term_is_uninterpreted_sort_value(Cvc5Term term)

Determine if a given term is an uninterpreted sort value.

Parameters:

term – The term.

Returns:

True if the term is an abstract value.

const char *cvc5_term_get_uninterpreted_sort_value(Cvc5Term term)

Get a string representation of an uninterpreted sort value.

Note

Asserts cvc5_term_is_uninterpreted_sort_value().

Note

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

Parameters:

term – The term.

Returns:

The representation of an uninterpreted sort value as a string.

bool cvc5_term_is_tuple_value(Cvc5Term term)

Determine if a given term is a tuple value.

Parameters:

term – The term.

Returns:

True if the term is a tuple value.

const Cvc5Term *cvc5_term_get_tuple_value(Cvc5Term term, size_t *size)

Get a tuple value as an array of terms.

Note

Asserts cvc5_term_is_tuple_value().

Parameters:

• term – The term.

• size – The size of the resulting array.

Returns:

The representation of a tuple value as an array of terms.

bool cvc5_term_is_rm_value(Cvc5Term term)

Determine if a given term is a floating-point rounding mode value.

Parameters:

term – The term.

Returns:

True if the term is a rounding mode value.

Cvc5RoundingMode cvc5_term_get_rm_value(Cvc5Term term)

Get the Cvc5RoundingMode value of a given rounding-mode value term.

Note

Asserts cvc5_term_is_rounding_mode_value().

Parameters:

term – The term.

Returns:

The floating-point rounding mode value of the term.

bool cvc5_term_is_fp_pos_zero(Cvc5Term term)

Determine if a given term is a floating-point positive zero value (+zero).

Parameters:

term – The term.

Returns:

True if the term is the floating-point value for positive zero.

bool cvc5_term_is_fp_neg_zero(Cvc5Term term)

Determine if a given term is a floating-point negative zero value (-zero).

Parameters:

term – The term.

Returns:

True if the term is the floating-point value for negative zero.

bool cvc5_term_is_fp_pos_inf(Cvc5Term term)

Determine if a given term is a floating-point positive infinity value (+oo).

Parameters:

term – The term.

Returns:

True if the term is the floating-point value for positive. infinity.

bool cvc5_term_is_fp_neg_inf(Cvc5Term term)

Determine if a given term is a floating-point negative infinity value (-oo).

Parameters:

term – The term.

Returns:

True if the term is the floating-point value for negative. infinity.

bool cvc5_term_is_fp_nan(Cvc5Term term)

Determine if a given term is a floating-point NaN value.

Parameters:

term – The term.

Returns:

True if the term is the floating-point value for not a number.

bool cvc5_term_is_fp_value(Cvc5Term term)

Determine if a given term is a floating-point value.

Parameters:

term – The term.

Returns:

True if the term is a floating-point value.

void cvc5_term_get_fp_value(Cvc5Term term, uint32_t *ew, uint32_t *sw, Cvc5Term *val)

Get the representation of a floating-point value as its exponent width, significand width and a bit-vector value term.

Note

Asserts cvc5_term_is_fp_value().

Parameters:

• term – The term.

• ew – The resulting exponent width.

• sw – The resulting significand width.

• val – The resulting bit-vector value term.

bool cvc5_term_is_set_value(Cvc5Term term)

Determine if a given term is a set value.

A term is a set value if it is considered to be a (canonical) constant set value. A canonical set value is one whose AST is:

(union (singleton c1) ... (union (singleton c_{n-1}) (singleton c_n))))

where \(c_1 ... c_n\) are values ordered by id such that \(c_1 > ... > c_n\).

Note

A universe set term (kind CVC5_KIND_SET_UNIVERSE) is not considered to be a set value.

Parameters:

term – The term.

Returns:

True if the term is a set value.

const Cvc5Term *cvc5_term_get_set_value(Cvc5Term term, size_t *size)

Get a set value as an array of terms.

Note

Asserts cvc5_term_is_set_value().

Parameters:

• term – The term.

• size – The size of the resulting array.

Returns:

The representation of a set value as an array of terms.

bool cvc5_term_is_sequence_value(Cvc5Term term)

Determine if a given term is a sequence value.

A term is a sequence value if it has kind #CONST_SEQUENCE. In contrast to values for the set sort (as described in isSetValue()), a sequence value is represented as a Term with no children.

Semantically, a sequence value is a concatenation of unit sequences whose elements are themselves values. For example:

(seq.++ (seq.unit 0) (seq.unit 1))

The above term has two representations in Term. One is as the sequence concatenation term:

(SEQ_CONCAT (SEQ_UNIT 0) (SEQ_UNIT 1))

where 0 and 1 are the terms corresponding to the integer constants 0 and 1.

Alternatively, the above term is represented as the constant sequence value:

CONST_SEQUENCE_{0,1}

where calling getSequenceValue() on the latter returns the vector {0, 1}.

The former term is not a sequence value, but the latter term is.

Constant sequences cannot be constructed directly via the API. They are returned in response to API calls such cvc5_get_value() and cvc5_simplify().

Parameters:

term – The term.

Returns:

True if the term is a sequence value.

const Cvc5Term *cvc5_term_get_sequence_value(Cvc5Term term, size_t *size)

Get a sequence value as an array of terms.

Note

Asserts cvc5_term_is_sequence_value().

Parameters:

• term – The term.

• size – The size of the resulting array.

Returns:

The representation of a sequence value as a vector of terms.

bool cvc5_term_is_cardinality_constraint(Cvc5Term term)

Determine if a given term is a cardinality constraint.

Parameters:

term – The term.

Returns:

True if the term is a cardinality constraint.

void cvc5_term_get_cardinality_constraint(Cvc5Term term, Cvc5Sort *sort, uint32_t *upper)

Get a cardinality constraint as a pair of its sort and upper bound.

Note

Asserts cvc5_term_is_cardinality_constraint().

Parameters:

• term – The term.

• sort – The resulting sort.

• upper – The resulting upper bound.

Returns:

The sort the cardinality constraint is for and its upper bound.

bool cvc5_term_is_real_algebraic_number(Cvc5Term term)

Determine if a given term is a real algebraic number.

Parameters:

term – The term.

Returns:

True if the term is a real algebraic number.

Cvc5Term cvc5_term_get_real_algebraic_number_defining_polynomial(Cvc5Term term, Cvc5Term v)

Get the defining polynomial for a real algebraic number term, expressed in terms of the given variable.

Note

Asserts cvc5_term_is_real_algebraic_number().

Parameters:

• term – The real algebraic number term.

• v – The variable over which to express the polynomial.

Returns:

The defining polynomial.

Cvc5Term cvc5_term_get_real_algebraic_number_lower_bound(Cvc5Term term)

Get the lower bound for a real algebraic number value.

Note

Asserts cvc5_term_is_real_algebraic_number().

Parameters:

term – The real algebraic number value.

Returns:

The lower bound.

Cvc5Term cvc5_term_get_real_algebraic_number_upper_bound(Cvc5Term term)

Get the upper bound for a real algebraic number value.

Note

Asserts cvc5_term_is_real_algebraic_number().

Parameters:

term – The real algebraic number value.

Returns:

The upper bound.

bool cvc5_term_is_skolem(Cvc5Term term)

Is the given term a skolem?

Warning

This function is experimental and may change in future versions.

Parameters:

term – The skolem.

Returns:

True if the term is a skolem function.

Cvc5SkolemId cvc5_term_get_skolem_id(Cvc5Term term)

Get skolem identifier of a term.

Note

Asserts isSkolem().

Warning

This function is experimental and may change in future versions.

Parameters:

term – The skolem.

Returns:

The skolem identifier of the term.

const Cvc5Term *cvc5_term_get_skolem_indices(Cvc5Term term, size_t *size)

Get the skolem indices of a term.

Note

Asserts isSkolem().

Warning

This function is experimental and may change in future versions.

Parameters:

• term – The skolem.

• size – The size of the resulting array.

Returns:

The skolem indices of the term. This is list of terms that the skolem function is indexed by. For example, the array diff skolem Cvc5SkolemId::ARRAY_DEQ_DIFF is indexed by two arrays.

size_t cvc5_term_hash(Cvc5Term term)

Compute the hash value of a term.

Parameters:

term – The term.

Returns:

The hash value of the term.