Terms
The API provides constructors for terms defined in the Yices language. There are no special constructs for formulas; formulas are terms of Boolean type. The semantics and typechecking rules of the language are explained in the manual.
All term constructors return an object of type term_t
. They
check their arguments, perform type checking, and return
NULL_TERM
if there’s an error. The functions listed in Section
Error Reporting can then be used to diagnose the error or print
an error message.
If there’s no error, the constructors apply rewriting and simplification procedures, then return an index in the global term table maintained within Yices. This index uniquely identifies the resulting term. Since Yices uses hash consing, two terms that are syntactically identical (after rewriting and simplification) are represented by the same index.
Warning
Some functions take an array of terms as argument. If this
array is not declared as const term_t a[]
then the
function may modify the array.
Common error reports
All functions in this section may report the following errors.
When a parameter to the functions is not a valid term, the error report is set as follow:
– error code:
INVALID_TERM
– term1 := the invalid term
If a type parameter is invalid:
– error code:
INVALID_TYPE
– type1 := the invalid type
When a parameter t to a function does not match a type tau, the type error is reported as follows:
– error code:
TYPE_MISMATCH
– term1 := t
– type1 := tau (i.e., the expected type)
Some functions expect arguments of compatible types. In particular, many bitvector constructors require bitvector arguments of the same size (i.e., the same number of bits). If two arguments t1 and t2 do not have compatible types the error report is:
– error code:
INCOMPATIBLE_TYPES
– term1 := t1
– type1 := t1 ‘s type
– term2 := t2
– type2 := t2 ‘s type
If an integer parameter that must be positive is given the value zero:
– error code:
POS_INT_REQUIRED
– badval := 0
The arithmetic constructors expect arguments of type integer or real. If they are given a term t of a different type, they report the following error:
– error code:
ARITHTERM_REQUIRED
– term1 := t
Several constructors have a parameter that specifies a bitvector size (i.e., number of bits). This number n must be positive and no more than
YICES_MAX_BVSIZE
. If n is more than this limit, the following error is reported:– error code:
MAX_BVSIZE_EXCEEDED
– badval := n
When a bitvector constructor is given a term t that’s not a bitvector:
– error code:
BITVECTOR_REQUIRED
– term1 := t
Other error reports may be produced by the term constructors. They are indicated after the function signature.
General Constructors

term_t
yices_new_uninterpreted_term
(type_t tau) Returns a new uninterpreted term of type tau.
An uninterpreted term is like a global variable of type tau. If tau is a function type, the resulting term is an uninterpreted function of type tau.
Optionally, you can give a name to new uninterpreted terms. using the functions defined in Names. This makes pretty printing nicer and it is useful if you want to construct terms using the parsing functions (see Parsing).

term_t
yices_new_variable
(type_t tau) Returns a fresh variable of type tau.
Variables are different from uninterpreted terms and are reserved for use in quantifiers and lambda terms. They can also be used to define term substitutions.

term_t
yices_constant
(type_t tau, int32_t i) Returns the constant of type tau and index i.
Parameters
tau must be either a scalar type or an uninterpreted type
i must be nonnegative and, if tau is scalar, i must be less than tau’s cardinality
Error report
If tau is not scalar or uninterpreted
– error code:
SCALAR_OR_UTYPE_REQUIRED
– type1 := tau
If i is negative or too large for type tau
– error code:
INVALID_CONSTANT_INDEX
– type1 := tau
– badval := i
This function creates constants of uninterpreted or scalar types. Within each such type, the constants are identified by a nonnegative index i. Two constants with distinct indices are semantically distinct terms.
A scalar type tau has finite cardinality so the number of constants of type tau is limited. There is no such restriction if tau is an uninterpreted type.

term_t
yices_ite
(term_t c, term_t t1, term_t t2) Returns the term (ite c t1 t2) which means if c then t1 else t2.
Parameters
c must be a Boolean term
t1 and t2 must be two terms of compatible types

term_t
yices_eq
(term_t t1, term_t t2) Returns the Boolean term (= t1 t2).
The terms t1 and t2 must have compatible types

term_t
yices_neq
(term_t t1, term_t t2) Returns the Boolean term (/= t1 t2).
The terms t1 and t2 must have compatible types

term_t
yices_distinct
(uint32_t n, term_t arg[]) Returns the term (distinct arg[0] … arg[n1]).
Parameters
n is the size of array arg. It must be positive and no more than
YICES_MAX_ARITY
.arg is an array of n terms. All elements of arg must have compatible types.
If n is 1, this function returns true.
Error report
If n is more than
YICES_MAX_ARITY
:– error code:
TOO_MANY_ARGUMENTS
– badval: n
Warning
Array arg may be modified.

term_t
yices_application
(term_t fun, uint32_t n, const term_t arg[]) Constructs the term (fun arg[0] … arg[n1]).
This applies function fun to the arguments arg[0] … arg[n1], where fun can be any term of function type. For example, fun may be an uninterpreted function constructed using
yices_new_uninterpreted_term
or a lambda term created usingyices_lambda
.If fun is a lambda term, then this constructor applies beta reduction.
Parameters
fun: term of function type
n: number of arguments
arg[0] … arg[n1]: arguments
The parameter n must be equal to the arity of function fun, and the arguments arg[0] … arg[n1] must have types that match the function signature. More precisely, if fun has type (> τ_{1} … τ_{n} σ) then arg[i]’s type must be a subtype of τ_{i+1}.
Error report
If fun does not have function type
– error code:
FUNCTION_REQUIRED
– term1 := fun
If n is different from fun’s arity
– error code:
WRONG_NUMBER_OF_ARGUMENTS
– badval := n

term_t
yices_application1
(term_t fun, term_t arg1) Returns the term (fun arg1).
This function applies a unary function fun to term arg1.
It is equivalent to
yices_application
with n=1.

term_t
yices_application2
(term_t fun, term_t arg1, term_t arg2) Returns the term (fun arg1 arg2).
This function applies binary function fun to the terms arg1 and arg2.
It is equivalent to
yices_application
with n=2.

term_t
yices_application3
(term_t fun, term_t arg1, term_t arg2, term_t arg3) Returns the term (fun arg1 arg2 arg3).
This function applies ternary function fun to arg1, arg2, and arg3.
It is equivalent to
yices_application
with n=3.

term_t
yices_tuple
(uint32_t n, const term_t arg[]) Returns the tuple term (mktuple arg[0] … arg[n1]).
Parameters
n is the number of components. It must be positive and no more than
YICES_MAX_ARITY
arg: array of n terms
Error report
If n is more than
YICES_MAX_ARITY
– error code:
TOO_MANY_ARGUMENTS
– badval := n

term_t
yices_pair
(term_t t1, term_t t2) Returns the pair (mktuple t1 t2).
This function is equivalent to
yices_tuple
with n=2.

term_t
yices_triple
(term_t t1, term_t t2, term_t t3) Returns the triple (mktuple t1 t2 t3).
This function is equivalent to
yices_tuple
with n=3.

term_t
yices_select
(uint32_t i, term_t t) Returns the term (select t i).
This function extracts the ith component of a tuple t.
Parameters
i must be an index between 1 and N (where N is the number of components of t)
t must be a term of tuple type
Error report
If t is does not have tuple type
– error code:
TUPLE_REQUIRED
– term1 := t
If i is zero or larger than N:
– error code:
INVALID_TUPLE_INDEX
– type1 := type of t
– badval := i

term_t
yices_tuple_update
(term_t t, uint32_t i, term_t v) Creates the term (tupleupdate t i v).
The result is the tuple obtained by replacing the ith component of tuple t by v.
Parameters
t must be a term of tuple type
i must be an index between 1 and N, where N is the number of components in t
If t’s type is (tuple τ_{1} … τ_{i} … τ_{n} ) then v’s type must be a subtype of τ_{i}
Error report
If t does not have a tuple type
– error code:
TUPLE_REQUIRED
– term1 := t
If i is zero or larger than N:
– error code:
INVALID_TUPLE_INDEX
– type1 := type of t
– badval := i
If v’s type is incorrect, the error code is
TYPE_MISMATCH

term_t
yices_update
(term_t fun, uint32_t n, const term_t arg[], term_t v) Creates the function update (update fun (arg[0] … arg[n1]) v).
The result is the function that has the same value as fun at all points in its domain, except at point (arg[0] … arg[n1]). At this point, the function returns v.
Parameters
fun must be a term of function type
n is the size of array arg; it must be positive and equal to the arity of fun
arg is an array of n terms
v is a term (the new value)
As in
yices_application
, the arguments arg[0] … arg[n1] must have types that match the signature of fun. In addition, v’s type must be a subtype of the function range.Error report
If fun does not have function type
– error code:
FUNCTION_REQUIRED
– term1 := fun
If n is different from fun’s arity
– error code:
WRONG_NUMBER_OF_ARGUMENTS
– badval := n
This constructor is often used to encode the operation of writing into an array. Yices does not have special types for arrays and an array is the same as a function. Under this interpretation, the function fun above is an array with n dimensions, and the update operation writes the value v at the index (arg[0] … arg[n1]). The result is a new array.

term_t
yices_update1
(term_t fun, term_t arg1, term_t v) Creates the function update (update fun (arg1) v).
This constructor is equivalent to
yices_update
for functions of arity n=1 (or singledimensional arrays).

term_t
yices_update2
(term_t fun, term_t arg1, term_t arg2, term_t v) Creates the function update (update fun (arg1 arg2) v).
This constructor is equivalent to
yices_update
for functions of arity n=2 (or twodimensional arrays).

term_t
yices_update3
(term_t fun, term_t arg1, term_t arg2, term_t arg3, term_t v) Creates the function update (update fun (arg1 arg2 arg3) v).
This constructor is equivalent to
yices_update
for functions of arity n=3 (or threedimensional arrays).

term_t
yices_forall
(uint32_t n, term_t var[], term_t body) Creates the quantified term: (forall (var[0] … var[n1]) body).
Parameters
n is the number of variables
var must be an array of n variables
body must be a Boolean term
Parameter n must be positive and no more than
YICES_MAX_VARS
.All the elements in array var must be constructed with function
yices_new_variable
, and the array must not contain duplicate elements.Error report
If n is more than
YICES_MAX_VARS
:– error code:
TOO_MANY_VARS
– badval := n
If one var[i] is not a variable:
– error code:
VARIABLE_REQUIRED
– term1 := var[i]
If a variable x occurs twice in array var:
– error code:
DUPLICATE_VARIABLE
– term1 := x
Warning
Array var may be modified.

term_t
yices_exists
(uint32_t n, term_t var[], term_t body) Creates the quantified term (exists (var[0] … var[n1]) body).
This function is similar to
yices_forall
. The parameters must satisfy the same constraints, and the possible error reports are the same.Warning
Array var may be modified.

term_t
yices_lambda
(uint32_t n, const term_t var[], term_t body) Creates the lambda term (lambda (var[0] … var[n1]) body).
Parameters
n is the number of variables.
var is an array of n variables.
body can be any term
The parameter n must be positive and no more than
YICES_MAX_VARS
As in constructors
yices_forall
andyices_exists
, all the elements in array var must be constructed with functionyices_new_variable
, and the array must not contain duplicate elements.Error report
If n is more than
YICES_MAX_VARS
:– error code:
TOO_MANY_VARS
– badval := n
If one var[i] is not a variable:
– error code:
VARIABLE_REQUIRED
– term1 := var[i]
If a variable x occurs twice in array var:
– error code:
DUPLICATE_VARIABLE
– term1 := x
Boolean Terms

term_t
yices_true
(void) Returns the Boolean constant true.

term_t
yices_false
(void) Returns the Boolean constant false.

term_t
yices_and
(uint32_t n, term_t arg[]) Constructs the conjunction (and arg[0] … arg[n1]).
Parameters
n is the number of arguments. It must be positive and no more than
YICES_MAX_ARITY
.arg must be an array of n Boolean terms
Error report
If n is more than
YICES_MAX_ARITY
:– error code:
TOO_MANY_ARGUMENTS
– badval: n
Warning
Array arg may be modified.

term_t
yices_and2
(term_t t1, term_t t2) Constructs the term (and t1 t2).
This function is equivalent to
yices_and
with n=2.Parameters
t1 and t2 must be Boolean terms

term_t
yices_and3
(term_t t1, term_t t2, term_t t3) Constructs the term (and t1 t2 t3).
This function is equivalent to
yices_and
with n=3.Parameters
t1, t2, and t3 must be Boolean terms

term_t
yices_or
(uint32_t n, term_t arg[]) Constructs the disjunction (or arg[0] … arg[n1]).
Parameters
n is the number of arguments. It must be positive and no more than
YICES_MAX_ARITY
.arg must be an array of n Boolean terms
Error report
If n is more than
YICES_MAX_ARITY
:– error code:
TOO_MANY_ARGUMENTS
– badval: n
Warning
Array arg may be modified.

term_t
yices_or2
(term_t t1, term_t t2) Constructs the term (or t1 t2).
This function is equivalent to
yices_or
with n=2.Parameters
t1 and t2 must be Boolean terms

term_t
yices_or3
(term_t t1, term_t t2, term_t t3) Constructs the term (or t1 t2 t3).
This function is equivalent to
yices_or
with n=3.Parameters
t1, t2, and t3 must be Boolean terms

term_t
yices_xor
(uint32_t n, term_t arg[]) Constructs the exclusive or (xor arg[0] … arg[n1]).
Parameters
n is the number of arguments. It must be positive and no more than
YICES_MAX_ARITY
.arg must be an array of n Boolean terms
Error report
If n is more than
YICES_MAX_ARITY
:– error code:
TOO_MANY_ARGUMENTS
– badval: n
Warning
Array arg may be modified.

term_t
yices_xor2
(term_t t1, term_t t2) Constructs the term (xor t1 t2).
This function is equivalent to
yices_xor
with n=2.Parameters
t1 and t2 must be Boolean terms

term_t
yices_xor3
(term_t t1, term_t t2, term_t t3) Constructs the term (xor t1 t2 t3).
This function is equivalent to
yices_xor
with n=3.Parameters
t1, t2, and t3 must be Boolean terms
Arithmetic Terms

term_t
yices_zero
(void) Returns the integer constant 0.

term_t
yices_int32
(int32_t val) Converts val to a constant integer term.

term_t
yices_int64
(int64_t val) Converts val to a constant integer term.

term_t
yices_rational32
(int32_t num, uint32_t den) Creates the rational constant num/den.
The parameter den must be positive.
Error report
If den is zero:
– error code:
DIVISION_BY_ZERO

term_t
yices_rational64
(int64_t num, uint64_t den) Creates the rational constant num/den.
The parameter den must be positive.
Error report
If den is zero:
– error code:
DIVISION_BY_ZERO

term_t
yices_mpz
(const mpz_t z) Converts the GMP integer z into a constant integer term.
Note
This function is not declared unless you include
gmp.h
beforeyices.h
in your code:#include <gmp.h> #include <yices.h>

term_t
yices_mpq
(const mpq_t q) Converts the GMP rational q into a constant rational term.
The parameter q must be in canonical form (cf. the GMP documentation).
Like the previous function, you must include
gmp.h
beforeyices.h
to ensure that this function is declared.

term_t
yices_parse_rational
(const char *s) Converts string s into a rational or integer term.
Parameter
The string s must be in the following format:
<sign> <digits>/<digits> or <sign> <digits>
– the
<sign>
can be either+
or
or nothing– and
<digits>
must be a sequence of decimal digits.For example,
"+1230/8939"
,"1/4"
, and"10000"
are in this format.
Error report
If s is not in the right format:
– error code:
INVALID_RATIONAL_FORMAT
If the denominator is zero:
– error code:
DIVISION_BY_ZERO

term_t
yices_parse_float
(const char *s) Converts string s into a rational or integer term.
Parameter
The string s must be in the following floatingpoint format:
<sign><digits>.<digits> or <sign><digits><exp><sign><digits> or <sign><digits>.<digits><exp><sign><digits>
– the
<sign>
can be either+
or
or nothing– the
<exp>
can be eithere
orE
For example,
"+1.04e5"
or"4E3"
are valid input for this function.
The string is converted to a rational or integer constant. Yices does not use floating point numbers internally.
Error report
If s is not in the right format:
– error code:
INVALID_FLOAT_FORMAT

term_t
yices_mul
(term_t t1, term_t t2) Returns the product (* t1 t2).
Error report
If the result has degree n that’s more than
YICES_MAX_DEGREE
– error code:
DEGREE_OVERFLOW
– badval := n

term_t
yices_square
(term_t t1) Returns the square of t1.
If the result has degree n that’s more than
YICES_MAX_DEGREE
– error code:
DEGREE_OVERFLOW
– badval := n

term_t
yices_power
(term_t t1, uint32_t d) Raises t1 to power d.
When d is zero, this function returns the constant 1 even if t1 is zero.
Error report
If the result has degree n that’s more than
YICES_MAX_DEGREE
– error code:
DEGREE_OVERFLOW
– badval := n

term_t
yices_division
(term_t t1, term_t t2) Constructs the quotient (/ t1 t2).
Parameters
t1 amd t2 must be arithmetic terms
Until version 2.5.0, Yices supported only division by nonzero constants. Division by arbitrary arithmetic terms is now supported (and can be handled by Yices’s solver for nonlinear arithmetic).

term_t
yices_sum
(uint32_t n, const term_t t[]) Constructs the sum (+ t[0] … t[n1]).
Parameters
n is the size of array t
t must be an array of n arithmetic terms
This generalizes function
yices_add
to n arguments. The array may be empty (i.e., n may be zero), in which case the function returns 0.

term_t
yices_product
(uint32_t n, const term_t t[]) Constructs the product (* t[0] … t[n1]).
Parameters
n is the size of array t
t must be an array of n arithmetic terms
This generalizes function
yices_mul
to n arguments. If n is zero, the function returns 1.

term_t
yices_poly_int32
(uint32_t n, const int32_t a[], const term_t t[]) Creates the linear polynomial (+ (* a[0] t[0]) … (* a[n1] t[n1)).
Parameters
n is the number of terms in the sum
a must be an array of n integer coefficients (of 32bits)
t must be an array of n arithmetic terms

term_t
yices_poly_int64
(uint32_t n, const int64_t a[], const term_t t[]) Creates the linear polynomial (+ (* a[0] t[0]) … (* a[n1] t[n1)).
Parameters
n is the number of terms in the sum
a must be an array of n integer coefficients (of 64bits)
t must be an array of n arithmetic terms

term_t
yices_poly_rational32
(uint32_t n, const int32_t num[], const uint32_t den[], const term_t t[]) Creates the linear polynomial (+ (* a[0] t[0]) … (* a[n1] t[n1)),
where coefficient a[i] is given by num[i]/den[i].
Parameters
n is the number of terms in the sum
num and den must be two arrays of n integers (of 32bits)
t must be an array of n arithmetic terms
No element of array den can be zero
Error report
If a denominator den[i] is zero:
– error code:
DIVISION_BY_ZERO

term_t
yices_poly_rational64
(uint32_t n, const int64_t num[], const uint64_t den[], const term_t t[]) Creates the linear polynomial (+ (* a[0] t[0]) … (* a[n1] t[n1)),
where coefficient a[i] is given by num[i]/den[i].
Parameters
n is the number of terms in the sum
num and den must be two arrays of n integers (of 64bits)
t must be an array of n arithmetic terms
No element of array den can be zero
Error report
If a denominator den[i] is zero:
– error code:
DIVISION_BY_ZERO

term_t
yices_poly_mpz
(uint32_t n, const mpz_t z[], const term_t t[]) Creates the linear polynomial (+ (* z[0] t[0]) … (* z[n1] t[n1]),
where the coefficients z[i] are GMP integers.
Parameters
n is the number of terms in the sum
z must be an array of n GMP integers
t must be an array of n arithmetic terms
This function is not declared unless you include
gmp.h
beforeyices.h
in your code. Seeyices_mpz
.

term_t
yices_poly_mpq
(uint32_t n, const mpq_t q[], const term_t t[]) Creates the linear polynomial (+ (* q[0] t[0]) … (* q[n1] t[n1])
where the coefficients q[i] are GMP rationals.
Parameters
n is the number of terms in the sum
q must be an array of n GMP rationals
t must be an array of n arithmetic terms
All the elements of q must be canonicalized
Like the previous function, you must include the header
gmp.h
before includingyices.h
to ensure that this function is declared.

term_t
yices_floor
(term_t t) Floor: (floor t)
Parameter
t must be an arithmetic term
The resulting term has integer type. It denotes the largest integer that’s smaller than or equal to t.

term_t
yices_ceil
(term_t t) Ceiling: (ceil t)
Parameter
t must be an arithmetic term
The resulting term has integer type. It denotes the smallest integer that’s larger than or equal to t.

term_t
yices_idiv
(term_t t1, term_t t2) Integer division (div t1 t2)
Parameters
t1 and t2 msut be arithmetic terms
The resulting term has type integer.
If t2 is positive, then (div t1 t2) is equal to (floor (/ t1 t2)).
If t2 is negative, then (div t1 t2) is equal to (ceil (/ t1 t2)).
Until version 2.5.0, Yices supported only division by nonzero constants. Division by arbitrary arithmetic terms is now supported (and can be handled by Yices’s solver for nonlinear arithmetic).

term_t
yices_imod
(term_t t1, term_t t2) Modulo: (mod t1 t2)
Parameters
t1 and t2 must be arithmetic terms
The resulting term is equal to ( t1 (* t2 (div t1 t2))).
Note
Until version 2.5.0, Yices supported only division by nonzero constants. Division by arbitrary arithmetic terms is now supported (and can be handled by Yices’s solver for nonlinear arithmetic).

term_t
yices_divides_atom
(term_t t1, term_t t2) Divisibility test: (divides t1 t2)
Parameters
t1 must be an arithmetic constant
t2 must be an arithmetic term
This constructs the Boolean term (divides t1 t2), which is true iff t2 is of the form n.t2 for some integer n.
Error report
if t1 is not an arithmetic constant:
– error code:
ARITHCONSTANT_REQUIRED
Bitvector Terms

term_t
yices_bvconst_uint32
(uint32_t n, uint32_t x) Converts unsigned 32bit integer x into a bitvector constant.
Parameters
n is the number of bits in the constant.
x is the value.
The parameter n must be positive and no more than
YICES_MAX_BVSIZE
.If n is less than 32, then the value x is truncated to n bits (i.e., the result is formed by taking the n least significant bits of x).
If n is more than 32, then the value x is zeroextended to n bits.

term_t
yices_bvconst_uint64
(uint32_t n, uint64_t x) Converts unsigned 64bit integer x into a bitvector constant.
Parameters
n is the number of bits in the constant.
x is the value.
The parameter n must be positive and no more than
YICES_MAX_BVSIZE
.If n is less than 64, then the value x is truncated to n bits (i.e., the result is formed by taking the n least significant bits of x).
If n is more than 64, then the value x is zeroextended to n bits.

term_t
yices_bvconst_int32
(uint32_t n, int32_t x) Converts signed 32bit integer x into a bitvector constant.
Parameters
n is the number of bits in the constant.
x is the value.
The parameter n must be positive and no more than
YICES_MAX_BVSIZE
.If n is less than 32, then the value x is truncated to n bits (i.e., the result is formed by taking the n least significant bits of x).
If n is more than 32, then the value x is signextended to n bits.

term_t
yices_bvconst_int64
(uint32_t n, int64_t x) Converts signed 64bit integer x into a bitvector constant.
Parameters
n is the number of bits in the constant.
x is the value.
The parameter n must be positive and no more than
YICES_MAX_BVSIZE
.If n is less than 64, then the value x is truncated to n bits (i.e., the result is formed by taking the n least significant bits of x).
If n is more than 64, then the value x is signextended to n bits.

term_t
yices_bvconst_mpz
(uint32_t n, const mpz_t x) Converts GMP integer x into a bitvector constant.
Parameters
n is the number of bits.
x is the value.
The number n must be positive and no more than
YICES_MAX_BVSIZE
.The GMP integer x is interpreted as a signed number in 2’s complement.
If x has fewer than n bits, then the value is signextended.
If x has more than n bits, then the result is formed by taking the n least significant bits of x.
This function is not declared unless you include
gmp.h
beforeyices.h
in your code. Seeyices_mpz
.

term_t
yices_bvconst_zero
(uint32_t n) Constructs the zero bitvector of n bits.
All bits of the results are set to 0.
Parameter
n is the number of bits.
It must be positive and no more than
YICES_MAX_BVSIZE

term_t
yices_bvconst_one
(uint32_t n) Constructs the bitvector constant 1.
The least significant bit of the result is 1 and all other bits are 0.
Parameter
n is the number of bits.
It must be positive and no more than
YICES_MAX_BVSIZE

term_t
yices_bvconst_minus_one
(uint32_t n) Constructs the bitvector constant equal to 1 in 2’s complement representation.
All the bits in the result are set to 1.
Parameter
n is the number of bits.
It must be positive and no more than
YICES_MAX_BVSIZE

term_t
yices_bvconst_from_array
(uint32_t n, const int32_t a[]) Constructs a bitvector constant from an array of integers.
Parameters
n is the number of bits
a must be an array of n integers
Parameter n must be positive and no more than
YICES_MAX_BVSIZE
.The bits are indexed from 0 (least significant bit) to n1 (most significant bit), and the result is defined as follows:
bit i of the result is 0 if a[i] is 0.
bit i of the result is 1 if a[i] is not 0.

term_t
yices_parse_bvbin
(const char *s) Constructs a bitvector constant from a string in binary format.
Parameter
s must be a
'\0'
terminated string that contains only the characters'0'
and'1'
.
The first character of s is the mostsignificant bit in the result, and the last character is the leastsignificant bit.
The size of the result (number of bits) is the same as the length of string s.
For example,
yices_parse_bvbin("00001")
returns the same term asyices_bvconst_one(5)
.Error report
If s is empty or contains characters other than
'0'
or'1'
:– error code:
INVALID_BVBIN_FORMAT
If s is too long (more than
YICES_MAX_BVSIZE
characters):– error code:
MAX_BVSIZE_EXCEEDED
– badval := length of s

term_t
yices_parse_bvhex
(const char *s) Constructs a bitvector constant from a string in hexadecimal format.
Parameter
s must be a
'\0'
terminated string that contains only the characters'0'
to'9'
or'a'
to'f'
or'A'
to'F'
.
If s is a string of length n, then the result is a bitvector of 4*n bits.
The first character of s defines the four most significant bits of the result, and the last character gives the four least significant bits.
For example,
yices_parse_bvhex("A7")
returns the same term asyices_parse_bvbin("10100111")
.Error report
If s is empty or contains nonhexadecimal characters:
– error code:
INVALID_BVHEX_FORMAT
If s is too long (more than
YICES_MAX_BVSIZE
/4 characters):– error code:
MAX_BVSIZE_EXCEEDED
– badval := 4 * (length of s)

term_t
yices_bvadd
(term_t t1, term_t t2) Returns the bitvector sum (bvadd t1 t2).
Parameters
t1 and t2 must be bitvector terms of the same type.

term_t
yices_bvsub
(term_t t1, term_t t2) Returns the bitvector difference (bvsub t1 t2).
Parameters
t1 and t2 must be bitvector terms of the same type.

term_t
yices_bvmul
(term_t t1, term_t t2) Returns the bitvector product (bvmul t1 t2).
Parameters
t1 and t2 must be bitvector terms of the same type.
Error report
If (degree of t1 + degree of t2) is more than
YICES_MAX_DEGREE
– error code :=
DEGREE_OVERFLOW
– badval := degree of t1 + degree of t2

term_t
yices_bvsquare
(term_t t1) Returns the product (bvmul t1 t1).
Error report
If (2 × degree of t1) is more than
YICES_MAX_DEGREE
– error code :=
DEGREE_OVERFLOW
– badval := twice the degree of t1

term_t
yices_bvpower
(term_t t1, uint32_t d) Bitvector exponentiation: raises t1 to power d.
If d is 0, the result is 0b0…01, even if t1 is the zero constant.
Error report
If (d × degree of t1) is more than
YICES_MAX_DEGREE
– error code :=
DEGREE_OVERFLOW
– badval := (d × degree of t1)

term_t
yices_bvsum
(uint32_t n, const term_t t[]) Returns the bitvector sum (bvadd t[0] … t[n1]).
This function generalizes
yices_bvadd
to an arbitrary number of arguments.Parameters
n is the number of arguments. It must be positive.
t must be an array of n bitvector terms. All the elements of t must have the same type (i.e., the same number of bits).
If n=1, this function returns t[0], otherwise, it builds a sum.

term_t
yices_bvproduct
(uint32_t n, const term_t t[]) Returns the bitvector product (bvmul t[0] … t[n1]).
This function generalizes
yices_bvmul
to an arbitrary number of arguments.Parameters
n is the number of arguments. It must be positive.
t must be an array of n bitvector terms. All the elements of t must have the same type (i.e., the same number of bits).
If n=1, this function returns t[0], otherwise, it builds a product.
Error report
If the degree is too large:
– error code:
DEGREE_OVERFLOW
– badval := degree

term_t
yices_bvdiv
(term_t t1, term_t t2) Quotient in the unsigned bitvector division.
Parameters
t1 and t2 must be bitvector terms of the same type.
The two vectors are interpreted as unsigned integers (represented with n bits) and the results is the largest integer that can be represented with n bits, and is less than or equal to t1/t2.
For division by zero, Yices uses the following convention:
(bvdiv t1 0b00...0) = 0b11...1

term_t
yices_bvrem
(term_t t1, term_t t2) Remainder in the unsigned division.
Parameters
t1 and t2 must be bitvector terms of the same type.
The remainder satisfies the following equality:
(bvrem t1 t2) = (bvsub t1 (bvmul (bvdiv t1 t2) t2))
If t2 is zero, this gives:
(bvrem t1 0b00...0) = t1

term_t
yices_bvsdiv
(term_t t1, term_t t2) Quotient in the signed bitvector division.
Parameters
t1 and t2 must be bitvector terms of the same type.
The two bitvectors t1 and t2 are interpreted as signed integers of n bits in 2’s complement representation. This signed division rounds the quotient toward zero.
If t1/t2 is positive and t2 isn’t zero, then (bvsdiv t1 t2) is positive. It is the largest integer that can be represented using n bits and is less than or equal to t1/t2.
If t1/t2 is negative and t2 isn’t zero, then (bvsdiv t1 t2) is negative. It is the smallest integer that can be represented using n bits and is more than or equal to t1/t2.
When t2 is zero, Yices uses the following convention:
If t1 is negative then
(bvsdiv t1 0b00...00) = 0b00...01
If t1 is positive or zero
(bvsdiv t1 0b00...00) = 0b11...11

term_t
yices_bvsrem
(term_t t1, term_t t2) Remainder in the signed division.
Parameters
t1 and t2 must be bitvector terms of the same type.
The remainder satisfies the following equality:
(bvsrem t1 t2) = (bvsub t1 (bvmul (bvsdiv t1 t2) t2))
If t2 is zero, this gives:
(bvsrem t1 0b00...0) = t1

term_t
yices_bvsmod
(term_t t1, term_t t2) Remainder in the floor division.
Parameters
t1 and t2 must be bitvector terms of the same type.
The two bitvectors t1 and t2 are interpreted as signed integers of n bits in 2’s complement representation. This function returns the remainder in the signed division of t1 by t2 with rounding to minus infinity.
If t2 is nonzero, the quotient q in this division is the largest signed integer that can be represented with n bits and is less than or equal to t1/t2.
Then (bvsmod t1 t2) is defined by
(bvsmod t1 t2) = (bvsub t1 (bvmul q t2))
If t2 is zero, this gives
(bvsrem t1 0b00...0) = t1

term_t
yices_bvand
(uint32_t n, const term_t t[]) Returns the bitwise and (bvand t[0] … t[n1]).
Parameters
n is the number of arguments. It must be positive.
t must be an array of n bitvector terms. All the elements of t must have the same type (i.e., the same number of bits).

term_t
yices_bvand2
(term_t t1, term_t t2) Returns the bitwise and (bvand t1 t2).
Parameters
t1 and t2 must be bitvector terms of the same type.
This function is equivalent to
yices_bvand
with n=2.

term_t
yices_bvand3
(term_t t1, term_t t2, term_t t3) Returns the bitwise and (bvand t1 t2 t3).
Parameters
t1, t2, and t3 must be bitvector terms of the same type.
This function is equivalent to
yices_bvand
with n=3.

term_t
yices_bvor
(uint32_t n, const term_t t[]) Returns the bitwise or (bvor t[0] … t[n1]).
Parameters
n is the number of arguments. It must be positive.
t must be an array of n bitvector terms. All the elements of t must have the same type (i.e., the same number of bits).

term_t
yices_bvor2
(term_t t1, term_t t2) Returns the bitwise or (bvor t1 t2).
Parameters
t1 and t2 must be bitvector terms of the same type.
This function is equivalent to
yices_bvor
with n=2.

term_t
yices_bvor3
(term_t t1, term_t t2, term_t t3) Returns the bitwise or (bvor t1 t2 t3).
Parameters
t1, t2, and t3 must be bitvector terms of the same type.
This function is equivalent to
yices_bvor
with n=3.

term_t
yices_bvxor
(uint32_t n, const term_t t[]) Returns the bitwise exclusive or (bvxor t[0] … t[n1]).
Parameters
n is the number of arguments. It must be positive.
t must be an array of n bitvector terms. All the elements of t must have the same type (i.e., the same number of bits).

term_t
yices_bvxor2
(term_t t1, term_t t2) Returns the bitwise exclusive or (bvxor t1 t2).
Parameters
t1 and t2 must be bitvector terms of the same type.
This function is equivalent to
yices_bvxor
with n=2.

term_t
yices_bvxor3
(term_t t1, term_t t2, term_t t3) Returns the bitwise exclusive or (bvxor t1 t2 t3).
Parameters
t1, t2, and t3 must be bitvector terms of the same type.
This function is equivalent to
yices_bvxor
with n=3.

term_t
yices_bvnand
(term_t t1, term_t t2) Returns the bitwise NAND of t1 and t2.
Parameters
t1 and t2 must be bitvector terms of the same type.
The result is the bitwise negation of (bvand t1 t2).

term_t
yices_bvnor
(term_t t1, term_t t2) Returns the bitwise NOR of t1 and t2.
Parameters
t1 and t2 must be bitvector terms of the same type.
The result is the bitwise negation of (bvor t1 t2).

term_t
yices_bvxnor
(term_t t1, term_t t2) Returns the bitwise XNOR of t1 and t2.
Parameters
t1 and t2 must be bitvector terms of the same type.
The result is the bitwise negation of (bvxor t1 t2).

term_t
yices_shift_left0
(term_t t, uint32_t n) Bitvector shift left by a constant, padding with 0.
This shifts bitvector t by n bits to the left, and sets the least significant bits to 0.
Parameters
If t is a bitvector of m bits then parameter n must be between 0 and m.
Examples
t
n
result
0b11111
0
0b11111
0b11111
2
0b11100
0b11111
5
0b00000
Error report
If n is more than the number of bits in t:
– error code:
INVALID_BITSHIFT
– badval := n

term_t
yices_shift_left1
(term_t t, uint32_t n) Bitvector shift left by a constant, padding with 1.
This shifts bitvector t by n bits to the left, and sets the least significant bits to 1.
Parameters
If t is a bitvector of m bits then parameter n must be between 0 and m.
Examples
t
n
result
0b00000
0
0b00000
0b00000
2
0b00011
0b00000
5
0111111
Error report
If n is more than the number of bits in t:
– error code:
INVALID_BITSHIFT
– badval := n

term_t
yices_shift_right0
(term_t t, uint32_t n) Bitvector shift right by a constant, padding with 0.
This shifts bitvector t by n bits to the right, and sets the most significant bits to 0.
Parameters
If t is a bitvector of m bits then parameter n must be between 0 and m.
Examples
t
n
result
0b11111
0
0b11111
0b11111
2
0b00111
0b11111
5
0b00000
Error report
If n is more than the number of bits in t:
– error code:
INVALID_BITSHIFT
– badval := n

term_t
yices_shift_right1
(term_t t, uint32_t n) Bitvector shift right by a constant, padding with 1.
This shifts bitvector t by n bits to the right, and sets the most significant bits to 1.
Parameters
If t is a bitvector of m bits then parameter n must be between 0 and m.
Examples
t
n
result
0b00000
0
0b00000
0b00000
2
0b11000
0b00000
5
0111111
Error report
If n is more than the number of bits in t:
– error code:
INVALID_BITSHIFT
– badval := n

term_t
yices_ashift_right
(term_t t, uint32_t n) Bitvector arithmetic shift right by a constant.
This shifts bitvector t by n bits to the right, and sets the most significant bits of the result to the same value as t’s sign bit (i.e., the most significant bit of t).
Parameters
If t is a bitvector of m bits then parameter n must be between 0 and m.
Examples
t
n
result
0b01111
2
0b00011
0b01111
5
0b00000
0b10111
2
0b11101
0b10111
5
0b11111
Error report
If n is more than the number of bits in t:
– error code:
INVALID_BITSHIFT
– badval := n

term_t
yices_rotate_left
(term_t t, uint32_t n) Bitvector rotate left by a constant.
This rotates bitvector t to the left by n bits.
Parameters
If t is a bitvector of m bits then parameter n must be between 0 and m.
Examples
If n is either 0 or m, the result is equal to t.
t
n
result
0b01010
0
0b01010
0b01010
1
0b10100
0b01010
2
0b01001
Error report
If n is more than the number of bits in t:
– error code:
INVALID_BITSHIFT
– badval := n

term_t
yices_rotate_right
(term_t t, uint32_t n) Bitvector rotate right by a constant.
This rotates bitvector t to the right by n bits.
Parameters
If t is a bitvector of m bits then parameter n must be between 0 and m.
If n is either 0 or m, the result is equal to t.
Examples
t
n
result
0b01010
0
0b01010
0b01010
1
0b00101
0b01010
2
0b10010
Error report
If n is more than the number of bits in t:
– error code:
INVALID_BITSHIFT
– badval := n

term_t
yices_bvshl
(term_t t1, term_t t2) Bitvector shift left.
This shifts bitvector t1 to the left by the amount specified by t2. The least significant bits of the result are set to 0.
Parameters
t1 and t2 must be two bitvectors of the same type
If n is the number of bits in both t1 and t2, then bitvector t2 is interpreted as an unsigned integer of n bits that specifies the shift amount. If t2’s value is more than n1, then the result is the bitvector
0b00...00
.

term_t
yices_bvlshr
(term_t t1, term_t t2) Bitvector logical shift right.
This shifts bitvector t1 to the right by the amount specified by t2. The most significant bits of the result are set to 0.
Parameters
t1 and t2 must be two bitvectors of the same type
If n is the number of bits in both t1 and t2, then bitvector t2 is interpreted as an unsigned integer of n bits that specifies the shift amount. If t2’s value is more than n1, then the result is the bitvector
0b00...00
.

term_t
yices_bvashr
(term_t t1, term_t t2) Bitvector arithmetic shift right.
This shifts bitvector t1 to the right by the amount specified by t2. The most significant bits of the result are equal to t1’s sign bit (i.e., the most significant bit of t1).
Parameters
t1 and t2 must be two bitvectors of the same type
If n is the number of bits in both t1 and t2, then bitvector t2 is interpreted as an unsigned integer of n bits that specifies the shift amount. If t2’s value is more than n1, then the result is either the bitvector
0b11...11
if t1 is negative, or the bitvector0b00...00
if t1 is positive or null.

term_t
yices_bvextract
(term_t t, uint32_t i, uint32_t j) Extracts a subvector from bitvector t.
Parameters
t must be a bitvector term
i and j must satisfy the constraint i ≤ j ≤ n1 where n is the number of bits in t
The result is a bitvector of 1 + j  i bits, formed by taking bits i to j of t. The least significant bit of the result is the ith bit of t, and the most significant bit is the jth bit of t.
Examples
t
i
j
result
0b10010
0
2
0b010
0b10010
2
4
0b100
0b10010
1
4
0b1001
Error report
If the constraint i ≤ j ≤ n1 does not hold
– error code:
INVALID_BVEXTRACT

term_t
yices_bitextract
(term_t t, uint32_t i) Extracts the ith bit of bitvector t.
Parameters
i must be an index between 0 and n1, where n is the number of bits of t.
The result is a Boolean term.
Error report
If i is too large:
– error code:
INVALID_BITEXTRACT

term_t
yices_bvconcat
(uint32_t n, const term_t t[]) Bitvector concatenation: (bvconcat t[0] … t[n1])
Parameters
n is the number of arguments
t must be an array of n bitvector terms
Parameter n must be positive.
The array t lists the elements to concatenate from left to right: the most significant bits of the result are given by t[0] and the least significant bits are formed by t[n1]. For example, if we have n=3 and t[0] = 0b000, t[1] = 0b111, and t[2] = 0b01, then the result is 0b00011101.
Error report
If the size of the result would be more than
YICES_MAX_BVSIZE
– error code:
MAX_BVSIZE_EXCEEDED
– badval := sum of the sizes of the vectors t[i]

term_t
yices_bvconcat2
(term_t t1, term_t t2) Concatenation of t1 and t2.
This function is equivalent to
yices_bvconcat
with n=2.The left part (most significant bits) is t1 and the right part (least significant bits) is t2.

term_t
yices_bvrepeat
(term_t t, uint32_t n) Repeated concatenation.
This concatenates t with itself n times.
The result is a bitvector of n*m bits, where m is the number of bits in t. If n=1 the result is
t
; if n=2, it is the same asyices_bvconcat2(t, t)
, and so forth.Parameters
The integer n must be positive
Error report
If n * (number of bits of t) is more than
YICES_MAX_BVSIZE
– error code:
MAX_BVSIZE_EXCEEDED
– badval := n * (number of bits of t)

term_t
yices_sign_extend
(term_t t, uint32_t n) Sign extension.
This adds n copies of t’s sign bit to the left of t.
Error report
If n + (number of bits of t) is more than
YICES_MAX_BVSIZE
– error code:
MAX_BVSIZE_EXCEEDED
– badval := n + (number of bits of t)

term_t
yices_zero_extend
(term_t t, uint32_t n) Zero extension.
This adds n zero bits to the left of t.
Error report
If n + (number of bits of t) is more than
YICES_MAX_BVSIZE
– error code:
MAX_BVSIZE_EXCEEDED
– badval := n + (number of bits of t)

term_t
yices_redand
(term_t t) And reduction.
This returns a bitvector of one bit equal to the conjunction of all bits of t.
If we denote by b[n1] … b[0] the n bits of b, then bit 0 of the result is (and b[0] … b[n1]).

term_t
yices_redor
(term_t t) Or reduction.
This returns a bitvector of one bit equal to the disjunction of all bits of t.
If we denote by b[n1] … b[0] the n bits of b, then bit 0 of the result is (or b[0] … b[n1]).

term_t
yices_redcomp
(term_t t1, term_t t2) Bitwise equality reduction.
This function returns (bvredand (bvxnor t1 t2)).
The result is a bitvector of one bit equal to 1 if t1 and t2 are equal, and to 0 otherwise.
Parameters
t1 and t2 must be two bitvectors of the same size.

term_t
yices_bvarray
(uint32_t n, const term_t arg[]) Converts an array of Boolean terms into a bitvector.
Parameters
n is the number of bits in the result
arg must be an array of n Boolean terms
Parameter n must be positive and no more than
YICES_MAX_BVSIZE
. The least significant bit is arg[0] and the most significant bit is arg[n1].Error report
If n is too large:
– error code:
MAX_BVSIZE_EXCEEDED
– badval := n

term_t
yices_bveq_atom
(term_t t1, term_t t2) Bivector equality.
This returns the Boolean term (= t1 t2).
Parameters
t1 and t2 must be bitvector of the same type

term_t
yices_bvneq_atom
(term_t t1, term_t t2) Bivector disequality.
This returns the Boolean term (/= t1 t2).
Parameters
t1 and t2 must be bitvector of the same type

term_t
yices_bvge_atom
(term_t t1, term_t t2) Bitvector unsigned inequality: t1 greater than or equal to t2.
Parameters
t1 and t2 must be bitvector of the same type
Both bitvectors are interpreted as unsigned integers of n bits and the result is the atom (>= t1 t2).

term_t
yices_bvgt_atom
(term_t t1, term_t t2) Bitvector unsigned inequality: t1 greater than t2.
Parameters
t1 and t2 must be bitvector of the same type
Both bitvectors are interpreted as unsigned integers of n bits and the result is the atom (> t1 t2).

term_t
yices_bvle_atom
(term_t t1, term_t t2) Bitvector unsigned inequality: t1 less than or equal to t2.
Parameters
t1 and t2 must be bitvector of the same type
Both bitvectors are interpreted as unsigned integers of n bits and the result is the atom (<= t1 t2).

term_t
yices_bvlt_atom
(term_t t1, term_t t2) Bitvector unsigned inequality: t1 less than t2.
Parameters
t1 and t2 must be bitvector of the same type
Both bitvectors are interpreted as unsigned integers of n bits and the result is the atom (< t1 t2).

term_t
yices_bvsge_atom
(term_t t1, term_t t2) Bitvector signed inequality: t1 greater than or equal to t2.
Parameters
t1 and t2 must be bitvector of the same type
Both bitvectors are interpreted as signed integers of n bits in 2’s complement representation and the result is the atom (>= t1 t2).

term_t
yices_bvsgt_atom
(term_t t1, term_t t2) Bitvector signed inequality: t1 greater than t2.
Parameters
t1 and t2 must be bitvector of the same type
Both bitvectors are interpreted as signed integers of n bits in 2’s complement representation and the result is the atom (> t1 t2).
Term Properties

type_t
yices_type_of_term
(term_t t) Returns the type of term t.
This function returns
NULL_TYPE
if t is not a valid term.

int32_t
yices_term_is_bool
(term_t t) Checks whether t is a Boolean term.
This function returns 1 for true and 0 for false. It also returns 0 if t is not a valid term and sets the error report.

int32_t
yices_term_is_int
(term_t t) Checks whether t has type integer.
This function returns 1 for true and 0 for false. It also returns 0 if t is not a valid term and sets the error report.

int32_t
yices_term_is_real
(term_t t) Checks whether t has type real.
This function returns 1 for true and 0 for false. It also returns 0 if t is not a valid term and sets the error report.
This function checks the actual type of t and does not take subtyping into account. It returns false if t has integer type.

int32_t
yices_term_is_arithmetic
(term_t t) Checks whether t is an arithmetic term.
This function returns 1 (for true) if t has either integer or real type. It returns 0 otherwise. If t is not a valid term, the function returns 0 and sets the error report.

int32_t
yices_term_is_bitvector
(term_t t) Checks whether t has a bitvector type.
This function returns 1 for true and 0 for false. It also returns 0 if t is not a valid term and sets the error report.

int32_t
yices_term_is_scalar
(term_t t) Checks whether t has a scalar or uninterpreted type.
This function returns 1 for true and 0 for false. It also returns 0 if t is not a valid term and sets the error report.

int32_t
yices_term_is_tuple
(term_t t) Checks whether t has a tuple type.
This function returns 1 for true and 0 for false. It also returns 0 if t is not a valid term and sets the error report.

int32_t
yices_term_is_function
(term_t t) Checks whether t has a function type.
This function returns 1 for true and 0 for false. It also returns 0 if t is not a valid term and sets the error report.

uint32_t
yices_term_bitsize
(term_t t) Returns the number of bits of term t.
This function returns 0 if there’s an error, either because t is not valid or does not have bitvector type.

int32_t
yices_term_is_ground
(term_t t) Checks whether term t is ground.
Returns 1 if t does not contain free variables, 0 otherwise. It also returns 0 if t is not a valid term and sets the error report.
Access to Term Components
The internal term representation distinguishes between the following classes of terms:
Atomic terms include constants of Boolean, bitvector, arithmetic, scalar, and uninterpreted types, and variables and uninterpreted terms.
Composite terms are terms represented by an operator tag and a list of children. For example an ifthenelse term (ite c t1 t2) is composite. Its tag is the termconstructor
YICES_ITE_TERM
and its three children are the terms c, t1, and t2.Projections represent tuple projection and extraction of a bit from a bitvector, which are constructed by functions
yices_select
andyices_bitextract
, respectively. Internally, such terms consists of an integer index and a term (either a tuple or a bitvector term).Arithmetic sums are used to build arithmetic polynomials. An arithmetic sum is of the form
a_{0} t_{0} + … + a_{n} t_{n}
where the coefficients a_{0} … a_{n} are rational constants and the terms t_{0} … t_{n} are all arithmetic terms.
Term t_{0} may be equal to
NULL_TERM
. In such a case, the product a_{0} t_{0} is replaced by the constant a_{0}, and the sum isa_{0} + a_{1} t_{1} + … + a_{n} t_{n}.
Bitvector sums are used to build bitvector polynomials. A bitvector sum is similar to an arithmetic sum but the coefficients are bitvector constants. It is of the form
a_{0} t_{0} + … + a_{n} t_{n}
where the coefficients a_{0} … a_{n} are bitvector constants and the terms t_{0} … t_{n} are bitvector terms. All the coefficients and terms have the same number of bits.
As previously, t_{0} may be equal to
NULL_TERM
to encode the sum:a_{0} + a_{1} t_{1} + … + a_{n} t_{n}.
Products are also used to build arithmetic and bitvector polynomials. A product is of the form
t_{0}^d_{0} × … × t_{n}^d_{n}
where the exponents d_{0} … d_{n} are positive integers, and the terms t_{0} … t_{n} are either all arithmetic terms or all bitvector terms of the same type.
The number of terms in a sum or product is always positive, but it may be equal to one. For example, the expression (− u) is represented internally as an arithmetic sum with a single monomial ( 1 ) × u.
Every term has a label of type term_constructor_t
that
identifies the class of the term and its constructor. Section Yices Terms
lists all the constructors and explains their roles.
Atomic Terms
Atomic terms are labeled with the following constructors.
Constructor
Term
Boolean constant
Arithmetic constant
Bitvector constant
Scalar/unint constant
Variable
Uninterpreted term
The API provides functions to obtain the value of a constant. For
arithmetic constant, the value is given as a GMP rational. For a
bitvector constant, the value is an array of 0/1 integers; the number
of bits in this array is given by yices_term_bitsize
. The
value of a constant of scalar or uninterpreted type is an integer
index (cf. yices_constant
).
Structure of Composite Terms
The following table lists the constructors of composite terms.
Constructor
Term
(ite c t1 t2)
(apply f t1 … tn)
(update f t1 … tn v)
(tuple t1 … tn)
(eq t1 t2)
(distinct t1 … tn)
(forall v1 … vn t)
(lambda v1 … vn t)
(not t)
(or t1 … tn)
(xor t1 … tn)
(bvarray t1 … tn)
(bvdiv t1 t2)
(bvrem t1 t2)
(bvsdiv t1 t2)
(bvsrem t1 t2)
(bvsmod t1 t2)
(bvshl t1 t2)
(bvlshr t1 t2)
(bvashr t1 t2)
(bvge t1 t2)
(bvsge t1 t2)
(>= t1 t2)
see below
(abs t)
(ceil t)
(floor t)
(/ t1 t2)
(div t1 t2)
(mod t1 t2)
(isint t)
(divides t1 t2)
Notes
The children of a composite term are indexed starting from 0. The indexing corresponds to the lefttoright order in the above table. For example an ifthenelse term has three children indexed from 0 to 2. The first child is the condition c, the next child is the then part t1, and the last child is the else part t2.
The first child in a function application is the function, the other children are the arguments. The first child of a function update is the function, the next n children are the arguments, and the last child is the new value v.
For forall and lambda terms, the first n children are the variables and the last child is the body t.
In the construct (bvarray t1 … tn), the n children are Boolean terms listed in littleendian form. The first child t1 is the least significant bit and the last child tn is the most significant bit.
Arithmetic Root Atoms
Arithmetic root atoms are used internally by the MCSAT solver. Such a term represents an atomic constraint of the form:
x r (kth root of p)
where x and p are both arithmetic terms, r denotes a relational operator (e.g., ≤ or >), and k is an integer index. The term p is always a polynomial. This term is treated like a composite term of two children. The first child is x and the second child is p.
Projection Terms
There are two types of projection terms to represent projection of a tuple and extraction of a bit from a bitvector.
Constructor
Term
(select t i)
(bit i t)
For a term of the form (select t i), the child t is a tuple and i is
an index. If the t has type (tuple τ_{1} … τ_{n})
then the index is between 1 and n. See yices_select
.
For a term of the form (bit i t), the child t is a bitvector and i is
an index. If t is a bitvector of n bits, then i is between 0 and n1.
Index 0 refers to the least significant bit of t and index n1 refers to
the most significant bit. See yices_bitextract
.
Polynomials
Sums and power products have the following constructors.
Constructor
Term
Arithmetic sum
Bitvector sum
Power product
Functions are available to extract the monomials of a sum (as pairs (coefficient × term)) and the factors of a product (as pairs (term, exponent)).
Functions
The following functions give access to the class, constructors,
children, and other components of a term. As usual, these functions
set the error report to INVALID_TERM
if the argument is not
a valid term.

int32_t
yices_term_is_atomic
(term_t t) Checks whether a term is atomic.
This function returns 1 for true and 0 for false. If t is not a valid term, the function returns 0 and sets the error report.

int32_t
yices_term_is_composite
(term_t t) Checks whether a term is composite.
This function returns 1 for true and 0 for false. If t is not a valid term, the function returns 0 and sets the error report.

int32_t
yices_term_is_projection
(term_t t) Checks whether a term is a projection.
This function returns 1 for true and 0 for false. If t is not a valid term, the function returns 0 and sets the error report.

int32_t
yices_term_is_sum
(term_t t) Checks whether a term is an arithmetic sum.
This function returns 1 for true and 0 for false. If t is not a valid term, the function returns 0 and sets the error report.

int32_t
yices_term_is_bvsum
(term_t t) Checks whether a term is a bitvector sum.
This function returns 1 for true and 0 for false. If t is not a valid term, the function returns 0 and sets the error report.

int32_t
yices_term_is_product
(term_t t) Checks whether a term is a product.
This function returns 1 for true and 0 for false. If t is not a valid term, the function returns 0 and sets the error report.

term_constructor_t
yices_term_constructor
(term_t t) Constructor of a term.
This function returns the constructor of term t. If t is not a valid term, it returns
YICES_CONSTRUCTOR_ERROR
.

int32_t
yices_term_num_children
(term_t t) Number of children of a term.
if t is atomic, this function returns 0.
if t is composite, it returns the number of children.
if t is a projection, the function returns 1.
if t is a sum, the function returns the number of summands.
if t is a product, the function returns the number of factors in the product.
otherwise, t is not valid; the function returns 1.

term_t
yices_term_child
(term_t t, int32_t i) Child of a composite term.
The function returns the ith child of composite term t or
NULL_TERM
if there’s an error.Parameters
t must be a composite term
i must be an index between 0 and n1, where n is the number of children of t
Error report
if t is not a composite term or i is not a valid index for term t
– error code:
INVALID_TERM_OP

int32_t
yices_proj_index
(term_t t) Index of a projection term.
Term t must either be a tuple select (select u i) or a bit extract (bit i u). This function returns the index i or 1 if there’s an error.
Error report
if t is not a projection
– error code:
INVALID_TERM_OP

term_t
yices_proj_arg
(term_t t) Child of a projection term.
Term t must either be a tuple select (select u i) or a bit extract (bit i u). This function returns the child u or
NULL_TERM
if there’s an error.Error report
if t is not a projection
– error code:
INVALID_TERM_OP

int32_t
yices_bool_const_value
(term_t t, int32_t *val) Value of a Boolean constant.
This function returns 1 and leaves *val unchanged if t is not a Boolean constant. Otherwise, it stores the value of t in variable *val (0 means false and 1 means true), and returns 0.
Error report
if t is not a Boolean constant
– error code:
INVALID_TERM_OP

int32_t
yices_bv_const_value
(term_t t, int32_t val[]) Value of a bitvector constant.
This function stores the value of t in array val. If t is a bitvector of n bits, then val must be large enough to store n integers. The n bits of t are stored in array val. Element val[i] is either 0 or 1. The least significant bit is stored in val[0] and the most significant bit is stored in val[n1].
The function returns 1 and leaves val unchanged if there’s an error. It returns 0 if t is a bitvector constant.
Error report
if t is not a bitvector constant
– error code:
INVALID_TERM_OP

int32_t
yices_scalar_const_value
(term_t t, int32_t *val) Index of a constant of scalar or uninterpreted type.
Constants of scalar and uninterpreted types are identified by an integer index (cf.
yices_constant
). This function stores the index of constant t in *val.The function returns 1 if there’s an error and leaves *val unchanged. Otherwise, it returns 0.
Error report
if t’s constructor is not
YICES_SCALAR_CONSTANT
– error code:
INVALID_TERM_OP

int32_t
yices_rational_const_value
(term_t t, mpq_t q) Value of a rational constant.
This function copies the value of rational constant t in the GMP rational q. The GMP rational q must be initialized (check the GMP documentation).
If t is not a rational constant, the function returns 1 and leaves q unchanged. Otherwise it returns 0.
Error report
if t’s constructor is not
YICES_ARITH_CONSTANT
– error code:
INVALID_TERM_OP
Note
To make sure that this function is declared, you must include
gmp.h
beforeyices.h
in your code (seeyices_mpz
).

int32_t
yices_sum_component
(term_t t, int32_t i, mpq_t coeff, term_t *term) Component of an arithmetic sum.
An arithmetic sum t is of the form a_{0} t_{0} + … + a_{n} t_{n}. This function copies the coefficient a_{i} in the GMP rational coeff and it copies t_{i} in variable *term.
As a special case, the returned *term may be equal to
NULL_TERM
. This may happen for i=0. In such a case, the sum is of the form a_{0} + a_{1} t_{1} + … + a_{n} t_{n}.This function returns 1 if t is not an arithmetic sum or if the index i is too large. It returns 0 otherwise.
Error report
if t’s constructor is not
YICES_ARITH_SUM
or if i is too large– error code:
INVALID_TERM_OP
Note
To make sure that this function is declared, you must include
gmp.h
beforeyices.h
in your code (seeyices_mpz
).

int32_t
yices_bvsum_component
(term_t t, int32_t i, int32_t val[], term_t *term) Component of a bitvector sum.
A bitvector sum t is of the form a_{0} t_{0} + … + a_{n} t_{n}. This function copies the coefficient a_{i} in array val and it copies t_{i} in *term.
If t is a bitvector term of m bits, then array val must be large enough to store m integers. The m bits of coefficients a_{i} are copied in val[0] … val[m1]; val[0] is the least significant bit and val[m1] is the most significant bit of a_{i}.
As a special case, the returned *term may be equal to
NULL_TERM
. This may happen for i=0. In such a case, the sum is of the form a_{0} + a_{1} t_{1} + … + a_{n} t_{n}.This function returns 1 if t is not an arithmetic sum or if the index i is too large. It returns 0 otherwise.
Error report
if t’s constructor is not
YICES_BV_SUM
or if i is too large– error code:
INVALID_TERM_OP

int32_t
yices_product_component
(term_t t, int32_t i, term_t *term, uint32_t *exp) Component of a power product.
A product t is of the form t_{0}^d_{0} × … × t_{n}^d_{n}. This function stores the term t_{i} into *term and the exponent d_{i} into *exp.
The function returns 1 if t is not a product or if the index i is too large. It returns 0 otherwise.
Error report
if t’s constructor is not
YICES_POWER_PRODUCT
or if i is too large– error code:
INVALID_TERM_OP