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 subterms),
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 finegrained 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 finegrained 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
ifa < b
, and1
ifb > 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 termreplacement
in a given term.Note
This replacement is applied during a preorder 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
withreplacement
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 termsreplacements
in a given term.In the case that
terms
contains duplicates, the replacement earliest in the vector takes priority. For example, calling substitute onf(x,y)
withterms = { x, z }
,replacements = { g(z), w }
results in the termf(g(z),y)
.Note
Requires that
terms
andreplacements
are of equal size (they are interpreted as 1 : 1 mapping).Note
This replacement is applied during a preorder traversal and only once (it is not run until fixed point).
 Parameters :


term – The term.

size – The size of
terms
andreplacements
. 
terms – The terms to replace.

replacements – The replacement terms.

 Returns :

The result of simultaneously replacing
terms
withreplacements
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 bitvector value.
 Parameters :

term – The term.
 Returns :

True if the term is a bitvector value.

const
char
*
cvc5_term_get_bv_value
(
Cvc5Term
term
,
uint32_t
base
)

Get the string representation of a bitvector 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, and16
for hexadecimal.

 Returns :

The string representation of a bitvector 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 floatingpoint 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 roundingmode value term.
Note
Asserts cvc5_term_is_rounding_mode_value().
 Parameters :

term – The term.
 Returns :

The floatingpoint rounding mode value of the term.

bool
cvc5_term_is_fp_pos_zero
(
Cvc5Term
term
)

Determine if a given term is a floatingpoint positive zero value (+zero).
 Parameters :

term – The term.
 Returns :

True if the term is the floatingpoint value for positive zero.

bool
cvc5_term_is_fp_neg_zero
(
Cvc5Term
term
)

Determine if a given term is a floatingpoint negative zero value (zero).
 Parameters :

term – The term.
 Returns :

True if the term is the floatingpoint value for negative zero.

bool
cvc5_term_is_fp_pos_inf
(
Cvc5Term
term
)

Determine if a given term is a floatingpoint positive infinity value (+oo).
 Parameters :

term – The term.
 Returns :

True if the term is the floatingpoint value for positive. infinity.

bool
cvc5_term_is_fp_neg_inf
(
Cvc5Term
term
)

Determine if a given term is a floatingpoint negative infinity value (oo).
 Parameters :

term – The term.
 Returns :

True if the term is the floatingpoint value for negative. infinity.

bool
cvc5_term_is_fp_nan
(
Cvc5Term
term
)

Determine if a given term is a floatingpoint NaN value.
 Parameters :

term – The term.
 Returns :

True if the term is the floatingpoint value for not a number.

bool
cvc5_term_is_fp_value
(
Cvc5Term
term
)

Determine if a given term is a floatingpoint value.
 Parameters :

term – The term.
 Returns :

True if the term is a floatingpoint value.

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

Get the representation of a floatingpoint value as its exponent width, significand width and a bitvector 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 bitvector 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_{n1}) (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.