Kind ¶
Every
Term
has a kind which represents its type, for
example whether it is an equality (
Equal
), a
conjunction (
And
), or a bitvector addtion
(
BVAdd
).
The kinds below directly correspond to the enum values of the C++
Kind
enum.
 class cvc5. Kind ( value ) ¶

The Kind enum
 ABS ¶

Absolute value.

Arity:
1

1:
Term of Sort Int or Real


Create Term of this Kind with:

Create Op of this kind with:

 ADD ¶

Arithmetic addition.

Arity:
n > 1

1..n:
Terms of Sort Int or Real (sorts must match)


Create Term of this Kind with:

Create Op of this kind with:

 AND ¶

Logical conjunction.

Arity:
n > 1

1..n:
Terms of Sort Bool


Create Term of this Kind with:

Create Op of this kind with:

 APPLY_CONSTRUCTOR ¶

Datatype constructor application.

Arity:
n > 0

1:
DatatypeConstructor Term (seeDatatypeConstructor.getTerm()
) 
2..n:
Terms of the Sorts of the selectors of the constructor (the arguments to the constructor)


Create Term of this Kind with:

Create Op of this kind with:

 APPLY_SELECTOR ¶

Datatype selector application.

Arity:
2

1:
DatatypeSelector Term (seeDatatypeSelector.getTerm()
) 
2:
Term of the codomain Sort of the selector


Create Term of this Kind with:

Create Op of this kind with:
Note
Undefined if misapplied.

 APPLY_TESTER ¶

Datatype tester application.

Arity:
2

1:
Datatype tester Term (seeDatatypeConstructor.getTesterTerm()
) 
2:
Term of Datatype Sort (DatatypeConstructor must belong to this Datatype Sort)


Create Term of this Kind with:

Create Op of this kind with:

 APPLY_UF ¶

Application of an uninterpreted function.

Arity:
n > 1

1:
Function Term 
2..n:
Function argument instantiation Terms of any firstclass Sort


Create Term of this Kind with:

Create Op of this kind with:

 APPLY_UPDATER ¶

Datatype update application.

Arity:
3

1:
Datatype updater Term (seeDatatypeSelector.getUpdaterTerm()
) 
2:
Term of Datatype Sort (DatatypeSelector of the updater must belong to a constructor of this Datatype Sort) 
3:
Term of the codomain Sort of the selector (the Term to update the field of the datatype term with)


Create Term of this Kind with:

Create Op of this kind with:
Note
Does not change the datatype argument if misapplied.

 ARCCOSECANT ¶

Arc cosecant function.

Arity:
1

1:
Term of Sort Real


Create Term of this Kind with:

Create Op of this kind with:

 ARCCOSINE ¶

Arc cosine function.

Arity:
1

1:
Term of Sort Real


Create Term of this Kind with:

Create Op of this kind with:

 ARCCOTANGENT ¶

Arc cotangent function.

Arity:
1

1:
Term of Sort Real


Create Term of this Kind with:

Create Op of this kind with:

 ARCSECANT ¶

Arc secant function.

Arity:
1

1:
Term of Sort Real


Create Term of this Kind with:

Create Op of this kind with:

 ARCSINE ¶

Arc sine function.

Arity:
1

1:
Term of Sort Real


Create Term of this Kind with:

Create Op of this kind with:

 ARCTANGENT ¶

Arc tangent function.

Arity:
1

1:
Term of Sort Real


Create Term of this Kind with:

Create Op of this kind with:

 BAG_CARD ¶

Bag cardinality.

Arity:
1

1:
Term of bag Sort


Create Term of this Kind with:

Create Op of this kind with:
Warning
This kind is experimental and may be changed or removed in future versions.

 BAG_CHOOSE ¶

Bag choose.
Select an element from a given bag.
For a bag \(A = \{(x,n)\}\) where \(n\) is the multiplicity, then the term (choose \(A\) ) is equivalent to the term \(x\) . For an empty bag, then it is an arbitrary value. For a bag that contains distinct elements, it will deterministically return an element in \(A\) .

Arity:
1

1:
Term of bag Sort


Create Term of this Kind with:

Create Op of this kind with:
Warning
This kind is experimental and may be changed or removed in future versions.

 BAG_COUNT ¶

Bag element multiplicity.

Create Term of this Kind with:

 BAG_DIFFERENCE_REMOVE ¶

Bag difference remove.
Removes shared elements in the two bags.

Arity:
2

1..2:
Terms of bag Sort


Create Term of this Kind with:

Create Op of this kind with:

 BAG_DIFFERENCE_SUBTRACT ¶

Bag difference subtract.
Subtracts multiplicities of the second from the first.

Arity:
2

1..2:
Terms of bag Sort


Create Term of this Kind with:

Create Op of this kind with:

 BAG_DUPLICATE_REMOVAL ¶

Bag duplicate removal.
Eliminate duplicates in a given bag. The returned bag contains exactly the same elements in the given bag, but with multiplicity one.

Arity:
1

1:
Term of bag Sort


Create Term of this Kind with:

Create Op of this kind with:
Warning
This kind is experimental and may be changed or removed in future versions.

 BAG_EMPTY ¶

Empty bag.

Create Term of this Kind with:

 BAG_FILTER ¶

Bag filter.
This operator filters the elements of a bag. (bag.filter \(p \; B\) ) takes a predicate \(p\) of Sort \((\rightarrow T \; Bool)\) as a first argument, and a bag \(B\) of Sort (Bag \(T\) ) as a second argument, and returns a subbag of Sort (Bag \(T\) ) that includes all elements of \(B\) that satisfy \(p\) with the same multiplicity.

Arity:
2

1:
Term of function Sort \((\rightarrow T \; Bool)\) 
2:
Term of bag Sort (Bag \(T\) )


Create Term of this Kind with:
Warning
This kind is experimental and may be changed or removed in future versions.

 BAG_FOLD ¶

Bag fold.
This operator combines elements of a bag into a single value. (bag.fold \(f \; t \; B\) ) folds the elements of bag \(B\) starting with Term \(t\) and using the combining function \(f\) .

Arity:
2

1:
Term of function Sort \((\rightarrow S_1 \; S_2 \; S_2)\) 
2:
Term of Sort \(S_2\) (the initial value) 
3:
Term of bag Sort (Bag \(S_1\) )


Create Term of this Kind with:
Warning
This kind is experimental and may be changed or removed in future versions.

 BAG_FROM_SET ¶

Conversion from set to bag.

Arity:
1

1:
Term of set Sort


Create Term of this Kind with:

Create Op of this kind with:
Warning
This kind is experimental and may be changed or removed in future versions.

 BAG_INTER_MIN ¶

Bag intersection (min).

Arity:
2

1..2:
Terms of bag Sort


Create Term of this Kind with:

Create Op of this kind with:

 BAG_IS_SINGLETON ¶

Bag is singleton tester.

Arity:
1

1:
Term of bag Sort


Create Term of this Kind with:

Create Op of this kind with:
Warning
This kind is experimental and may be changed or removed in future versions.

 BAG_MAKE ¶

Bag make.
Construct a bag with the given element and given multiplicity.

Arity:
2

1:
Term of any Sort (the bag element) 
2:
Term of Sort Int (the multiplicity of the element)


Create Term of this Kind with:

Create Op of this kind with:

 BAG_MAP ¶

Bag map.
This operator applies the first argument, a function of Sort \((\rightarrow S_1 \; S_2)\) , to every element of the second argument, a set of Sort (Bag \(S_1\) ), and returns a set of Sort (Bag \(S_2\) ).

Arity:
2

1:
Term of function Sort \((\rightarrow S_1 \; S_2)\) 
2:
Term of bag Sort (Bag \(S_1\) )


Create Term of this Kind with:

Create Op of this kind with:
Warning
This kind is experimental and may be changed or removed in future versions.

 BAG_MEMBER ¶

Bag membership predicate.

Arity:
2

1:
Term of any Sort (must match the element Sort of the given bag Term) 
2:
Terms of bag Sort


Create Term of this Kind with:

Create Op of this kind with:

 BAG_PARTITION ¶

Bag partition.
This operator partitions of a bag of elements into disjoint bags. (bag.partition \(r \; B\) ) partitions the elements of bag \(B\) of type \((Bag \; E)\) based on the equivalence relations \(r\) of type \((\rightarrow \; E \; E \; Bool)\) . It returns a bag of bags of type \((Bag \; (Bag \; E))\) .

Arity:
2

1:
Term of function Sort \((\rightarrow \; E \; E \; Bool)\) 
2:
Term of bag Sort (Bag \(E\) )


Create Term of this Kind with:
Warning
This kind is experimental and may be changed or removed in future versions.

 BAG_SUBBAG ¶

Bag inclusion predicate.
Determine if multiplicities of the first bag are less than or equal to multiplicities of the second bag.

Arity:
2

1..2:
Terms of bag Sort


Create Term of this Kind with:

Create Op of this kind with:

 BAG_TO_SET ¶

Conversion from bag to set.

Arity:
1

1:
Term of bag Sort


Create Term of this Kind with:

Create Op of this kind with:
Warning
This kind is experimental and may be changed or removed in future versions.

 BAG_UNION_DISJOINT ¶

Bag disjoint union (sum).

Arity:
2

1..2:
Terms of bag Sort


Create Term of this Kind with:

Create Op of this kind with:

 BAG_UNION_MAX ¶

Bag max union.

Arity:
2

1..2:
Terms of bag Sort


Create Term of this Kind with:

Create Op of this kind with:

 BITVECTOR_ADD ¶

Addition of two or more bitvectors.

Arity:
n > 1

1..n:
Terms of bitvector Sort (sorts must match)


Create Term of this Kind with:

Create Op of this kind with:

 BITVECTOR_AND ¶

Bitwise and.

Arity:
n > 1

1..n:
Terms of bitvector Sort (sorts must match)


Create Term of this Kind with:

Create Op of this kind with:

 BITVECTOR_ASHR ¶

Bitvector arithmetic shift right.

Arity:
2

1..2:
Terms of bitvector Sort (sorts must match)


Create Term of this Kind with:

Create Op of this kind with:

 BITVECTOR_COMP ¶

Equality comparison (returns bitvector of size
1
).
Arity:
2

1..2:
Terms of bitvector Sort (sorts must match)


Create Term of this Kind with:

Create Op of this kind with:

 BITVECTOR_CONCAT ¶

Concatenation of two or more bitvectors.

Arity:
n > 1

1..n:
Terms of bitvector Sort (sorts must match)


Create Term of this Kind with:

Create Op of this kind with:

 BITVECTOR_EXTRACT ¶

Bitvector extract.

Arity:
1

1:
Term of bitvector Sort


Indices:
2

1:
The upper bit index. 
2:
The lower bit index.


Create Term of this Kind with:

Create Op of this kind with:

 BITVECTOR_ITE ¶

Bitvector ifthenelse.
Same semantics as regular ITE, but condition is bitvector of size
1
.
Arity:
3

1:
Term of bitvector Sort of size 1 
1..3:
Terms of bitvector sort (sorts must match)


Create Term of this Kind with:

Create Op of this kind with:

 BITVECTOR_LSHR ¶

Bitvector logical shift right.

Arity:
2

1..2:
Terms of bitvector Sort (sorts must match)


Create Term of this Kind with:

Create Op of this kind with:

 BITVECTOR_MULT ¶

Multiplication of two or more bitvectors.

Arity:
n > 1

1..n:
Terms of bitvector Sort (sorts must match)


Create Term of this Kind with:

Create Op of this kind with:

 BITVECTOR_NAND ¶

Bitwise nand.

Arity:
2

1..2:
Terms of bitvector Sort (sorts must match)


Create Term of this Kind with:

Create Op of this kind with:

 BITVECTOR_NEG ¶

Negation of a bitvector (two’s complement).

Arity:
1

1:
Term of bitvector Sort


Create Term of this Kind with:

Create Op of this kind with:

 BITVECTOR_NOR ¶

Bitwise nor.

Arity:
2

1..2:
Terms of bitvector Sort (sorts must match)


Create Term of this Kind with:

Create Op of this kind with:

 BITVECTOR_NOT ¶

Bitwise negation.

Arity:
1

1:
Term of bitvector Sort


Create Term of this Kind with:

Create Op of this kind with:

 BITVECTOR_OR ¶

Bitwise or.

Arity:
n > 1

1..n:
Terms of bitvector Sort (sorts must match)


Create Term of this Kind with:

Create Op of this kind with:

 BITVECTOR_REDAND ¶

Bitvector redand.

Arity:
1

1:
Term of bitvector Sort


Create Term of this Kind with:

Create Op of this kind with:

 BITVECTOR_REDOR ¶

Bitvector redor.

Arity:
1

1:
Term of bitvector Sort


Create Term of this Kind with:

Create Op of this kind with:

 BITVECTOR_REPEAT ¶

Bitvector repeat.

Arity:
1

1:
Term of bitvector Sort


Indices:
1

1:
The number of times to repeat the given term.


Create Term of this Kind with:

Create Op of this kind with:

 BITVECTOR_ROTATE_LEFT ¶

Bitvector rotate left.

Arity:
1

1:
Term of bitvector Sort


Indices:
1

1:
The number of bits to rotate the given term left.


Create Term of this Kind with:

Create Op of this kind with:

 BITVECTOR_ROTATE_RIGHT ¶

Bitvector rotate right.

Arity:
1

1:
Term of bitvector Sort


Indices:
1

1:
The number of bits to rotate the given term right.


Create Term of this Kind with:

Create Op of this kind with:

 BITVECTOR_SDIV ¶

Signed bitvector division.
Two’s complement signed division of two bitvectors. If the divisor is zero and the dividend is positive, the result is all ones. If the divisor is zero and the dividend is negative, the result is one.

Arity:
2

1..2:
Terms of bitvector Sort (sorts must match)


Create Term of this Kind with:

Create Op of this kind with:

 BITVECTOR_SGE ¶

Bitvector signed greater than or equal.

Arity:
2

1..2:
Terms of bitvector Sort (sorts must match)


Create Term of this Kind with:

Create Op of this kind with:

 BITVECTOR_SGT ¶

Bitvector signed greater than.

Arity:
2

1..2:
Terms of bitvector Sort (sorts must match)


Create Term of this Kind with:

Create Op of this kind with:

 BITVECTOR_SHL ¶

Bitvector shift left.

Arity:
2

1..2:
Terms of bitvector Sort (sorts must match)


Create Term of this Kind with:

Create Op of this kind with:

 BITVECTOR_SIGN_EXTEND ¶

Bitvector sign extension.

Arity:
1

1:
Term of bitvector Sort


Indices:
1

1:
The number of bits (of the value of the sign bit) to extend the given term with.


Create Term of this Kind with:

Create Op of this kind with:

 BITVECTOR_SLE ¶

Bitvector signed less than or equal.

Arity:
2

1..2:
Terms of bitvector Sort (sorts must match)


Create Term of this Kind with:

Create Op of this kind with:

 BITVECTOR_SLT ¶

Bitvector signed less than.

Arity:
2

1..2:
Terms of bitvector Sort (sorts must match)


Create Term of this Kind with:

Create Op of this kind with:

 BITVECTOR_SLTBV ¶

Bitvector signed less than returning a bitvector of size
1
.
Arity:
2

1..2:
Terms of bitvector Sort (sorts must match)


Create Term of this Kind with:

Create Op of this kind with:

 BITVECTOR_SMOD ¶

Signed bitvector remainder (sign follows divisor).
Two’s complement signed remainder where the sign follows the divisor. If the modulus is zero, the result is the dividend.

Arity:
2

1..2:
Terms of bitvector Sort (sorts must match)


Create Term of this Kind with:

Create Op of this kind with:

 BITVECTOR_SREM ¶

Signed bitvector remainder (sign follows dividend).
Two’s complement signed remainder of two bitvectors where the sign follows the dividend. If the modulus is zero, the result is the dividend.

Arity:
2

1..2:
Terms of bitvector Sort (sorts must match)


Create Term of this Kind with:

Create Op of this kind with:

 BITVECTOR_SUB ¶

Subtraction of two bitvectors.

Arity:
n > 1

1..n:
Terms of bitvector Sort (sorts must match)


Create Term of this Kind with:

Create Op of this kind with:

 BITVECTOR_TO_NAT ¶

Bitvector conversion to (nonnegative) integer.

Arity:
1

1:
Term of bitvector Sort


Create Term of this Kind with:

Create Op of this kind with:

 BITVECTOR_UDIV ¶

Unsigned bitvector division.
Truncates towards
0
. If the divisor is zero, the result is all ones.
Arity:
2

1..2:
Terms of bitvector Sort (sorts must match)


Create Term of this Kind with:

Create Op of this kind with:

 BITVECTOR_UGE ¶

Bitvector unsigned greater than or equal.

Arity:
2

1..2:
Terms of bitvector Sort (sorts must match)


Create Term of this Kind with:

Create Op of this kind with:

 BITVECTOR_UGT ¶

Bitvector unsigned greater than.

Arity:
2

1..2:
Terms of bitvector Sort (sorts must match)


Create Term of this Kind with:

Create Op of this kind with:

 BITVECTOR_ULE ¶

Bitvector unsigned less than or equal.

Arity:
2

1..2:
Terms of bitvector Sort (sorts must match)


Create Term of this Kind with:

Create Op of this kind with:

 BITVECTOR_ULT ¶

Bitvector unsigned less than.

Arity:
2

1..2:
Terms of bitvector Sort (sorts must match)


Create Term of this Kind with:

Create Op of this kind with:

 BITVECTOR_ULTBV ¶

Bitvector unsigned less than returning a bitvector of size 1.

Arity:
2

1..2:
Terms of bitvector Sort (sorts must match)


Create Term of this Kind with:

Create Op of this kind with:

 BITVECTOR_UREM ¶

Unsigned bitvector remainder.
Remainder from unsigned bitvector division. If the modulus is zero, the result is the dividend.

Arity:
2

1..2:
Terms of bitvector Sort (sorts must match)


Create Term of this Kind with:

Create Op of this kind with:

 BITVECTOR_XNOR ¶

Bitwise xnor, left associative.

Arity:
2

1..2:
Terms of bitvector Sort (sorts must match)


Create Term of this Kind with:

Create Op of this kind with:

 BITVECTOR_XOR ¶

Bitwise xor.

Arity:
n > 1

1..n:
Terms of bitvector Sort (sorts must match)


Create Term of this Kind with:

Create Op of this kind with:

 BITVECTOR_ZERO_EXTEND ¶

Bitvector zero extension.

Arity:
1

1:
Term of bitvector Sort


Indices:
1

1:
The number of zeroes to extend the given term with.


Create Term of this Kind with:

Create Op of this kind with:

 CARDINALITY_CONSTRAINT ¶

Cardinality constraint on uninterpreted sort.
Interpreted as a predicate that is true when the cardinality of uinterpreted Sort \(S\) is less than or equal to an upper bound.

Create Term of this Kind with:
Warning
This kind is experimental and may be changed or removed in future versions.

 CONSTANT ¶

Free constant symbol.

Create Term of this Kind with:

 CONST_ARRAY ¶

Constant array.

Arity:
2

1:
Term of array Sort 
2:
Term of array element Sort (value)


Create Term of this Kind with:

Create Op of this kind with:

 CONST_BITVECTOR ¶

Fixedsize bitvector constant.

Create Term of this Kind with:

 CONST_BOOLEAN ¶

Boolean constant.

Create Term of this Kind with:

 CONST_FLOATINGPOINT ¶

Floatingpoint constant, created from IEEE754 bitvector representation of the floatingpoint value.

Create Term of this Kind with:

 CONST_INTEGER ¶

Arbitraryprecision integer constant.

Create Term of this Kind with:

 CONST_RATIONAL ¶

Arbitraryprecision rational constant.

Create Term of this Kind with:

 CONST_ROUNDINGMODE ¶

RoundingMode constant.

Create Term of this Kind with:

 CONST_SEQUENCE ¶

Constant sequence.
A constant sequence is a term that is equivalent to:
(seq.++ (seq.unit c1) ... (seq.unit cn))
where \(n \leq 0\) and \(c_1, ..., c_n\) are constants of some sort. The elements can be extracted with
Term.getSequenceValue()
.
Create Term of this Kind with:

 CONST_STRING ¶

Constant string.

Create Term of this Kind with:

 COSECANT ¶

Cosecant function.

Arity:
1

1:
Term of Sort Real


Create Term of this Kind with:

Create Op of this kind with:

 COSINE ¶

Cosine function.

Arity:
1

1:
Term of Sort Real


Create Term of this Kind with:

Create Op of this kind with:

 COTANGENT ¶

Cotangent function.

Arity:
1

1:
Term of Sort Real


Create Term of this Kind with:

Create Op of this kind with:

 DISTINCT ¶

Disequality.

Arity:
n > 1

1..n:
Terms of the same Sort


Create Term of this Kind with:

Create Op of this kind with:

 DIVISIBLE ¶

Operator for the divisibilityby \(k\) predicate.

Arity:
1

1:
Term of Sort Int


Indices:
1

1:
The integer \(k\) to divide by.


Create Term of this Kind with:

Create Op of this kind with:

 DIVISION ¶

Real division, division by 0 undefined, left associative.

Arity:
n > 1

1..n:
Terms of Sort Real


Create Term of this Kind with:

Create Op of this kind with:

 EQUAL ¶

Equality, chainable.

Arity:
n > 1

1..n:
Terms of the same Sort


Create Term of this Kind with:

Create Op of this kind with:

 EQ_RANGE ¶

Equality over arrays \(a\) and \(b\) over a given range \([i,j]\) , i.e.,
\[\forall k . i \leq k \leq j \Rightarrow a[k] = b[k]\]
Arity:
4

1:
Term of array Sort (first array) 
2:
Term of array Sort (second array) 
3:
Term of array index Sort (lower bound of range, inclusive) 
4:
Term of array index Sort (upper bound of range, inclusive)


Create Term of this Kind with:

Create Op of this kind with:
Warning
This kind is experimental and may be changed or removed in future versions.
Note
We currently support the creation of array equalities over index Sorts bitvector, floatingpoint, Int and Real. Requires to enable option arraysexp .

 EXISTS ¶

Existentially quantified formula.

Arity:
3

1:
Term of KindVARIABLE_LIST

2:
Term of Sort Bool (the quantifier body) 
3:
(optional) Term of KindINST_PATTERN


Create Term of this Kind with:

Create Op of this kind with:

 EXPONENTIAL ¶

Exponential function.

Arity:
1

1:
Term of Sort Real


Create Term of this Kind with:

Create Op of this kind with:

 FLOATINGPOINT_ABS ¶

Floatingpoint absolute value.

Arity:
1

1:
Term of floatingpoint Sort


Create Term of this Kind with:

Create Op of this kind with:

 FLOATINGPOINT_ADD ¶

Floatingpoint addition.

Arity:
3

1:
Term of Sort RoundingMode 
2..3:
Terms of floatingpoint Sort (sorts must match)


Create Term of this Kind with:

Create Op of this kind with:

 FLOATINGPOINT_DIV ¶

Floatingpoint division.

Arity:
3

1:
Term of Sort RoundingMode 
2..3:
Terms of floatingpoint Sort (sorts must match)


Create Term of this Kind with:

Create Op of this kind with:

 FLOATINGPOINT_EQ ¶

Floatingpoint equality.

Arity:
2

1..2:
Terms of floatingpoint Sort (sorts must match)


Create Term of this Kind with:

Create Op of this kind with:

 FLOATINGPOINT_FMA ¶

Floatingpoint fused multiply and add.

Arity:
4

1:
Term of Sort RoundingMode 
2..4:
Terms of floatingpoint Sort (sorts must match)


Create Term of this Kind with:

Create Op of this kind with:

 FLOATINGPOINT_FP ¶

Create floatingpoint literal from bitvector triple.

Arity:
3

1:
Term of bitvector Sort of size 1 (sign bit) 
2:
Term of bitvector Sort of exponent size (exponent) 
3:
Term of bitvector Sort of significand size  1 (significand without hidden bit)


Create Term of this Kind with:

Create Op of this kind with:

 FLOATINGPOINT_GEQ ¶

Floatingpoint greater than or equal.

Arity:
2

1..2:
Terms of floatingpoint Sort (sorts must match)


Create Term of this Kind with:

Create Op of this kind with:

 FLOATINGPOINT_GT ¶

Floatingpoint greater than.

Arity:
2

1..2:
Terms of floatingpoint Sort (sorts must match)


Create Term of this Kind with:

Create Op of this kind with:

 FLOATINGPOINT_IS_INF ¶

Floatingpoint is infinite tester.

Arity:
1

1:
Term of floatingpoint Sort


Create Term of this Kind with:

Create Op of this kind with:

 FLOATINGPOINT_IS_NAN ¶

Floatingpoint is NaN tester.

Arity:
1

1:
Term of floatingpoint Sort


Create Term of this Kind with:

Create Op of this kind with:

 FLOATINGPOINT_IS_NEG ¶

Floatingpoint is negative tester.

Arity:
1

1:
Term of floatingpoint Sort


Create Term of this Kind with:

Create Op of this kind with:

 FLOATINGPOINT_IS_NORMAL ¶

Floatingpoint is normal tester.

Arity:
1

1:
Term of floatingpoint Sort


Create Term of this Kind with:

Create Op of this kind with:

 FLOATINGPOINT_IS_POS ¶

Floatingpoint is positive tester.

Arity:
1

1:
Term of floatingpoint Sort


Create Term of this Kind with:

Create Op of this kind with:

 FLOATINGPOINT_IS_SUBNORMAL ¶

Floatingpoint is subnormal tester.

Arity:
1

1:
Term of floatingpoint Sort


Create Term of this Kind with:

Create Op of this kind with:

 FLOATINGPOINT_IS_ZERO ¶

Floatingpoint is zero tester.

Arity:
1

1:
Term of floatingpoint Sort


Create Term of this Kind with:

Create Op of this kind with:

 FLOATINGPOINT_LEQ ¶

Floatingpoint less than or equal.

Arity:
2

1..2:
Terms of floatingpoint Sort (sorts must match)


Create Term of this Kind with:

Create Op of this kind with:

 FLOATINGPOINT_LT ¶

Floatingpoint less than.

Arity:
2

1..2:
Terms of floatingpoint Sort (sorts must match)


Create Term of this Kind with:

Create Op of this kind with:

 FLOATINGPOINT_MAX ¶

Floatingpoint maximum.

Arity:
2

1..2:
Terms of floatingpoint Sort (sorts must match)


Create Term of this Kind with:

Create Op of this kind with:

 FLOATINGPOINT_MIN ¶

Floatingpoint minimum.

Arity:
2

1..2:
Terms of floatingpoint Sort (sorts must match)


Create Term of this Kind with:

Create Op of this kind with:

 FLOATINGPOINT_MULT ¶

Floatingpoint multiply.

Arity:
3

1:
Term of Sort RoundingMode 
2..3:
Terms of floatingpoint Sort (sorts must match)


Create Term of this Kind with:

Create Op of this kind with:

 FLOATINGPOINT_NEG ¶

Floatingpoint negation.

Arity:
1

1:
Term of floatingpoint Sort


Create Term of this Kind with:

Create Op of this kind with:

 FLOATINGPOINT_REM ¶

Floatingpoint remainder.

Arity:
2

1..2:
Terms of floatingpoint Sort (sorts must match)


Create Term of this Kind with:

Create Op of this kind with:

 FLOATINGPOINT_RTI ¶

Floatingpoint round to integral.

Arity:
2

1..2:
Terms of floatingpoint Sort (sorts must match)


Create Term of this Kind with:

Create Op of this kind with:

 FLOATINGPOINT_SQRT ¶

Floatingpoint square root.

Arity:
2

1:
Term of Sort RoundingMode 
2:
Term of floatingpoint Sort


Create Term of this Kind with:

Create Op of this kind with:

 FLOATINGPOINT_SUB ¶

Floatingpoint sutraction.

Arity:
3

1:
Term of Sort RoundingMode 
2..3:
Terms of floatingpoint Sort (sorts must match)


Create Term of this Kind with:

Create Op of this kind with:

 FLOATINGPOINT_TO_FP_FROM_FP ¶

Conversion to floatingpoint from floatingpoint.

Arity:
2

1:
Term of Sort RoundingMode 
2:
Term of floatingpoint Sort


Indices:
2

1:
The exponent size 
2:
The significand size


Create Term of this Kind with:

Create Op of this kind with:

 FLOATINGPOINT_TO_FP_FROM_IEEE_BV ¶

Conversion to floatingpoint from IEEE754 bitvector.

Arity:
1

1:
Term of bitvector Sort


Indices:
2

1:
The exponent size 
2:
The significand size


Create Term of this Kind with:

Create Op of this kind with:

 FLOATINGPOINT_TO_FP_FROM_REAL ¶

Conversion to floatingpoint from Real.

Arity:
2

1:
Term of Sort RoundingMode 
2:
Term of Sort Real


Indices:
2

1:
The exponent size 
2:
The significand size


Create Term of this Kind with:

Create Op of this kind with:

 FLOATINGPOINT_TO_FP_FROM_SBV ¶

Conversion to floatingpoint from signed bitvector.

Arity:
2

1:
Term of Sort RoundingMode 
2:
Term of bitvector Sort


Indices:
2

1:
The exponent size 
2:
The significand size


Create Term of this Kind with:

Create Op of this kind with:

 FLOATINGPOINT_TO_FP_FROM_UBV ¶

Conversion to floatingpoint from unsigned bitvector.

Arity:
2

1:
Term of Sort RoundingMode 
2:
Term of bitvector Sort


Indices:
2

1:
The exponent size 
2:
The significand size


Create Term of this Kind with:

Create Op of this kind with:

 FLOATINGPOINT_TO_REAL ¶

Conversion to Real from floatingpoint.

Arity:
1

1:
Term of Sort Real


Create Term of this Kind with:

Create Op of this kind with:

 FLOATINGPOINT_TO_SBV ¶

Conversion to signed bitvector from floatingpoint.

Arity:
1

1:
Term of floatingpoint Sort


Indices:
1

1:
The size of the bitvector to convert to.


Create Term of this Kind with:

Create Op of this kind with:

 FLOATINGPOINT_TO_UBV ¶

Conversion to unsigned bitvector from floatingpoint.

Arity:
1

1:
Term of floatingpoint Sort


Indices:
1

1:
The size of the bitvector to convert to.


Create Term of this Kind with:

Create Op of this kind with:

 FORALL ¶

Universally quantified formula.

Arity:
3

1:
Term of KindVARIABLE_LIST

2:
Term of Sort Bool (the quantifier body) 
3:
(optional) Term of KindINST_PATTERN


Create Term of this Kind with:

Create Op of this kind with:

 GEQ ¶

Greater than or equal, chainable.

Arity:
n > 1

1..n:
Terms of Sort Int or Real (sorts must match)


Create Term of this Kind with:

Create Op of this kind with:

 GT ¶

Greater than, chainable.

Arity:
n > 1

1..n:
Terms of Sort Int or Real (sorts must match)


Create Term of this Kind with:

Create Op of this kind with:

 HO_APPLY ¶

Higherorder applicative encoding of function application, left associative.

Arity:
n = 2

1:
Function Term 
2:
Argument Term of the domain Sort of the function


Create Term of this Kind with:

Create Op of this kind with:

 IAND ¶

Integer and.
Operator for bitwise
AND
over integers, parameterized by a (positive) bitwidth \(k\) .((_ iand k) i_1 i_2)
is equivalent to
((_ iand k) i_1 i_2) (bv2int (bvand ((_ int2bv k) i_1) ((_ int2bv k) i_2)))
for all integers
i_1
,i_2
.
Arity:
2

1..2:
Terms of Sort Int


Indices:
1

1:
Bitwidth \(k\)


Create Term of this Kind with:

Create Op of this kind with:

 IMPLIES ¶

Logical implication.

Arity:
n > 1

1..n:
Terms of Sort Bool


Create Term of this Kind with:

Create Op of this kind with:

 INST_ADD_TO_POOL ¶

A instantantiationaddtopool annotation.
An instantantiationaddtopool annotation indicates that when a quantified formula is instantiated, the instantiated version of a term should be added to the given pool.
For example, consider a quantified formula:
(FORALL (VARIABLE_LIST x) F (INST_PATTERN_LIST (INST_ADD_TO_POOL (ADD x 1) p)))
where assume that \(x\) has type Int. When this quantified formula is instantiated with, e.g., the term \(t\) , the term
(ADD t 1)
is added to pool \(p\) .
Arity:
2

1:
The Term whose free variables are bound by the quantified formula. 
2:
The pool to add to, whose Sort should be a set of elements that match the Sort of the first argument.


Create Term of this Kind with:

Create Op of this kind with:
Warning
This kind is experimental and may be changed or removed in future versions.
Note
Should only be used as a child of
INST_PATTERN_LIST
. 
 INST_ATTRIBUTE ¶

Instantiation attribute.
Specifies a custom property for a quantified formula given by a term that is ascribed a user attribute.

Arity:
n > 0

1:
Term of KindCONST_STRING
(the keyword of the attribute) 
2...n:
Terms representing the values of the attribute


Create Term of this Kind with:

Create Op of this kind with:
Note
Should only be used as a child of
INST_PATTERN_LIST
. 
 INST_NO_PATTERN ¶

Instantiation nopattern.
Specifies a (list of) terms that should not be used as a pattern for quantifier instantiation.

Arity:
n > 0

1..n:
Terms of any Sort


Create Term of this Kind with:

Create Op of this kind with:
Note
Should only be used as a child of
INST_PATTERN_LIST
. 
 INST_PATTERN ¶

Instantiation pattern.
Specifies a (list of) terms to be used as a pattern for quantifier instantiation.

Arity:
n > 0

1..n:
Terms of any Sort


Create Term of this Kind with:

Create Op of this kind with:
Note
Should only be used as a child of
INST_PATTERN_LIST
. 
 INST_PATTERN_LIST ¶

A list of instantiation patterns, attributes or annotations.

Arity:
n > 1

1..n:
Terms of KindINST_PATTERN
,INST_NO_PATTERN
,INST_POOL
,INST_ADD_TO_POOL
,SKOLEM_ADD_TO_POOL
,INST_ATTRIBUTE


Create Term of this Kind with:

Create Op of this kind with:

 INST_POOL ¶

Instantiation pool annotation.
Specifies an annotation for pool based instantiation.
 In detail, pool symbols can be declared via the method
A pool symbol represents a set of terms of a given sort. An instantiation pool annotation should match the types of the quantified formula.
For example, for a quantified formula:
(FORALL (VARIABLE_LIST x y) F (INST_PATTERN_LIST (INST_POOL p q)))
if \(x\) and \(y\) have Sorts \(S_1\) and \(S_2\) , then pool symbols \(p\) and \(q\) should have Sorts (Set \(S_1\) ) and (Set \(S_2\) ), respectively. This annotation specifies that the quantified formula above should be instantiated with the product of all terms that occur in the sets \(p\) and \(q\) .

Arity:
n > 0

1..n:
Terms that comprise the pools, which are onetoone with the variables of the quantified formula to be instantiated


Create Term of this Kind with:

Create Op of this kind with:
Warning
This kind is experimental and may be changed or removed in future versions.
Note
Should only be used as a child of
INST_PATTERN_LIST
.
 INTERNAL_KIND ¶

Internal kind.
This kind serves as an abstraction for internal kinds that are not exposed via the API but may appear in terms returned by API functions, e.g., when querying the simplified form of a term.
Note
Should never be created via the API.
 INTS_DIVISION ¶

Integer division, division by 0 undefined, left associative.

Arity:
n > 1

1..n:
Terms of Sort Int


Create Term of this Kind with:

Create Op of this kind with:

 INTS_MODULUS ¶

Integer modulus, modulus by 0 undefined.

Arity:
2

1:
Term of Sort Int 
2:
Term of Sort Int


Create Term of this Kind with:

Create Op of this kind with:

 INT_TO_BITVECTOR ¶

Conversion from Int to bitvector.

Arity:
1

1:
Term of Sort Int


Indices:
1

1:
The size of the bitvector to convert to.


Create Term of this Kind with:

Create Op of this kind with:

 IS_INTEGER ¶

Isinteger predicate.

Arity:
1

1:
Term of Sort Int or Real


Create Term of this Kind with:

Create Op of this kind with:

 ITE ¶

Ifthenelse.

Arity:
3

1:
Term of Sort Bool 
2:
The ‘then’ term, Term of any Sort 
3:
The ‘else’ term, Term of the same sort as second argument


Create Term of this Kind with:

Create Op of this kind with:

 LAMBDA ¶

Lambda expression.

Arity:
2

1:
Term of kindVARIABLE_LIST

2:
Term of any Sort (the body of the lambda)


Create Term of this Kind with:

Create Op of this kind with:

 LAST_KIND ¶

Marks the upperbound of this enumeration.
 LEQ ¶

Less than or equal, chainable.

Arity:
n > 1

1..n:
Terms of Sort Int or Real (sorts must match)


Create Term of this Kind with:

Create Op of this kind with:

 LT ¶

Less than, chainable.

Arity:
n > 1

1..n:
Terms of Sort Int or Real (sorts must match)


Create Term of this Kind with:

Create Op of this kind with:

 MATCH ¶

Match expression.
This kind is primarily used in the parser to support the SMTLIBv2
match
expression.For example, the SMTLIBv2 syntax for the following match term
(match l (((cons h t) h) (nil 0)))
is represented by the AST
(MATCH l (MATCH_BIND_CASE (VARIABLE_LIST h t) (cons h t) h) (MATCH_CASE nil 0))
Terms of kind
MATCH_CASE
are constant case expressions, which are used for nullary constructors. KindMATCH_BIND_CASE
is used for constructors with selectors and variable match patterns. If not all constructors are covered, at least one catchall variable pattern must be included.
Arity:
n > 1

1..n:
Terms of kindMATCH_CASE
andMATCH_BIND_CASE


Create Term of this Kind with:

Create Op of this kind with:

 MATCH_BIND_CASE ¶

Match case with binders, for constructors with selectors and variable patterns.
A (nonconstant) case expression to be used within a match expression.

Arity:
3

For variable patterns:

1:
Term of kindVARIABLE_LIST
(containing the free variable of the case) 
2:
Term of kindVARIABLE
(the pattern expression, the free variable of the case) 
3:
Term of any Sort (the term the pattern evaluates to)


For constructors with selectors:

1:
Term of kindVARIABLE_LIST
(containing the free variable of the case) 
2:
Term of kindAPPLY_CONSTRUCTOR
(the pattern expression, applying the set of variables to the constructor) 
3:
Term of any Sort (the term the match term evaluates to)



Create Term of this Kind with:

Create Op of this kind with:

 MATCH_CASE ¶

Match case for nullary constructors.
A (constant) case expression to be used within a match expression.

Arity:
2

1:
Term of kindAPPLY_CONSTRUCTOR
(the pattern to match against) 
2:
Term of any Sort (the term the match term evaluates to)


Create Term of this Kind with:

Create Op of this kind with:

 MULT ¶

Arithmetic multiplication.

Arity:
n > 1

1..n:
Terms of Sort Int or Real (sorts must match)


Create Term of this Kind with:

Create Op of this kind with:

 NEG ¶

Arithmetic negation.

Arity:
1

1:
Term of Sort Int or Real


Create Term of this Kind with:

Create Op of this kind with:

 NOT ¶

Logical negation.

Arity:
1

1:
Term of Sort Bool


Create Term of this Kind with:

Create Op of this kind with:

 NULL_TERM ¶

Null kind.
The kind of a null term (
Term.Term()
).Note
May not be explicitly created via API functions other than
Term.Term()
.
 OR ¶

Logical disjunction.

Arity:
n > 1

1..n:
Terms of Sort Bool


Create Term of this Kind with:

Create Op of this kind with:

 PI ¶

Pi constant.

Create Term of this Kind with:
Note
PI
is considered a special symbol of Sort Real, but is not a Real value, i.e.,Term.isRealValue()
will returnfalse
. 
 POW ¶

Arithmetic power.

Arity:
2

1..2:
Term of Sort Int or Real (sorts must match)


Create Term of this Kind with:

Create Op of this kind with:

 POW2 ¶

Power of two.
Operator for raising
2
to a nonnegative integer power.
Arity:
1

1:
Term of Sort Int


Create Term of this Kind with:

Create Op of this kind with:

 REGEXP_ALL ¶

Regular expression all.

Create Term of this Kind with:

 REGEXP_ALLCHAR ¶

Regular expression all characters.

Create Term of this Kind with:

 REGEXP_COMPLEMENT ¶

Regular expression complement.

Arity:
1

1:
Term of Sort RegLan


Create Term of this Kind with:

Create Op of this kind with:

 REGEXP_CONCAT ¶

Regular expression concatenation.

Arity:
2

1..2:
Terms of Sort RegLan


Create Term of this Kind with:

Create Op of this kind with:

 REGEXP_DIFF ¶

Regular expression difference.

Arity:
2

1..2:
Terms of Sort RegLan


Create Term of this Kind with:

Create Op of this kind with:

 REGEXP_INTER ¶

Regular expression intersection.

Arity:
2

1..2:
Terms of Sort RegLan


Create Term of this Kind with:

Create Op of this kind with:

 REGEXP_LOOP ¶

Regular expression loop.
Regular expression loop from lower bound to upper bound number of repetitions.

Arity:
1

1:
Term of Sort RegLan


Indices:
1

1:
The lower bound 
2:
The upper bound


Create Term of this Kind with:

Create Op of this kind with:

 REGEXP_NONE ¶

Regular expression none.

Create Term of this Kind with:

 REGEXP_OPT ¶

Regular expression ?.

Arity:
1

1:
Term of Sort RegLan


Create Term of this Kind with:

Create Op of this kind with:

 REGEXP_PLUS ¶

Regular expression +.

Arity:
1

1:
Term of Sort RegLan


Create Term of this Kind with:

Create Op of this kind with:

 REGEXP_RANGE ¶

Regular expression range.

Arity:
2

1:
Term of Sort String (lower bound character for the range) 
2:
Term of Sort String (upper bound character for the range)


Create Term of this Kind with:

Create Op of this kind with:

 REGEXP_REPEAT ¶

Operator for regular expression repeat.

Arity:
1

1:
Term of Sort RegLan


Indices:
1

1:
The number of repetitions


Create Term of this Kind with:

Create Op of this kind with:

 REGEXP_STAR ¶

Regular expression *.

Arity:
1

1:
Term of Sort RegLan


Create Term of this Kind with:

Create Op of this kind with:

 REGEXP_UNION ¶

Regular expression union.

Arity:
2

1..2:
Terms of Sort RegLan


Create Term of this Kind with:

Create Op of this kind with:

 RELATION_AGGREGATE ¶

Relation aggregate operator has the form \(((\_ \; rel.aggr \; n_1 ... n_k) \; f \; i \; A)\) where \(n_1, ..., n_k\) are natural numbers, \(f\) is a function of type \((\rightarrow (Tuple \; T_1 \; ... \; T_j)\; T \; T)\) , \(i\) has the type \(T\) , and \(A\) has type \((Relation \; T_1 \; ... \; T_j)\) . The returned type is \((Set \; T)\) .
This operator aggregates elements in A that have the same tuple projection with indices n_1, …, n_k using the combining function \(f\) , and initial value \(i\) .

Arity:
3

1:
Term of sort \((\rightarrow (Tuple \; T_1 \; ... \; T_j)\; T \; T)\) 
2:
Term of Sort \(T\) 
3:
Term of relation sort \(Relation T_1 ... T_j\)


Indices:
n
1..n:
Indices of the projection 
Create Term of this Kind with: 
Solver.mkTerm()

Create Op of this kind with: 
Solver.mkOp()
Warning
This kind is experimental and may be changed or removed in future versions.

 RELATION_GROUP ¶

Relation group
\(((\_ \; rel.group \; n_1 \; \dots \; n_k) \; A)\) partitions tuples of relation \(A\) such that tuples that have the same projection with indices \(n_1 \; \dots \; n_k\) are in the same part. It returns a set of relations of type \((Set \; T)\) where \(T\) is the type of \(A\) .

Arity:
1

1:
Term of relation sort


Indices:
n

1..n:
Indices of the projection


Create Term of this Kind with:
Warning
This kind is experimental and may be changed or removed in future versions.

 RELATION_IDEN ¶

Relation identity.

Arity:
1

1:
Term of relation Sort


Create Term of this Kind with:

Create Op of this kind with:
Warning
This kind is experimental and may be changed or removed in future versions.

 RELATION_JOIN ¶

Relation join.

Arity:
2

1..2:
Terms of relation Sort


Create Term of this Kind with:

Create Op of this kind with:

 RELATION_JOIN_IMAGE ¶

Relation join image.

Arity:
2

1..2:
Terms of relation Sort


Create Term of this Kind with:

Create Op of this kind with:
Warning
This kind is experimental and may be changed or removed in future versions.

 RELATION_PRODUCT ¶

Relation cartesian product.

Arity:
2

1..2:
Terms of relation Sort


Create Term of this Kind with:

Create Op of this kind with:

 RELATION_PROJECT ¶

Relation projection operator extends tuple projection operator to sets.

Arity:
1
1:
Term of relation Sort 
Indices:
n
1..n:
Indices of the projection 
Create Term of this Kind with: 
Solver.mkTerm()

Create Op of this kind with: 
Solver.mkOp()
Warning
This kind is experimental and may be changed or removed in future versions.

 RELATION_TCLOSURE ¶

Relation transitive closure.

Arity:
1

1:
Term of relation Sort


Create Term of this Kind with:

Create Op of this kind with:

 RELATION_TRANSPOSE ¶

Relation transpose.

Arity:
1

1:
Term of relation Sort


Create Term of this Kind with:

Create Op of this kind with:

 SECANT ¶

Secant function.

Arity:
1

1:
Term of Sort Real


Create Term of this Kind with:

Create Op of this kind with:

 SELECT ¶

Array select.

Arity:
2

1:
Term of array Sort 
2:
Term of array index Sort


Create Term of this Kind with:

Create Op of this kind with:

 SEP_EMP ¶

Separation logic empty heap.

Create Term of this Kind with:
Warning
This kind is experimental and may be changed or removed in future versions.

 SEP_NIL ¶

Separation logic nil.

Create Term of this Kind with:
Warning
This kind is experimental and may be changed or removed in future versions.

 SEP_PTO ¶

Separation logic pointsto relation.

Arity:
2

1:
Term denoting the location of the pointsto constraint 
2:
Term denoting the data of the pointsto constraint


Create Term of this Kind with:

Create Op of this kind with:
Warning
This kind is experimental and may be changed or removed in future versions.

 SEP_STAR ¶

Separation logic star.

Arity:
n > 1


1..n:
Terms of sort Bool (the child constraints that hold in 
disjoint (separated) heaps)



Create Term of this Kind with:

Create Op of this kind with:
Warning
This kind is experimental and may be changed or removed in future versions.

 SEP_WAND ¶

Separation logic magic wand.

Arity:
2

1:
Terms of Sort Bool (the antecendant of the magic wand constraint) 

2:
Terms of Sort Bool (conclusion of the magic wand constraint, 
which is asserted to hold in all heaps that are disjoint extensions of the antecedent)



Create Term of this Kind with:

Create Op of this kind with:
Warning
This kind is experimental and may be changed or removed in future versions.

 SEQ_AT ¶

Sequence element at.
Returns the element at index \(i\) from a sequence \(s\) . If the index is negative or the index is greater or equal to the length of the sequence, the result is the empty sequence. Otherwise the result is a sequence of length
1
.
Arity:
2

1:
Term of sequence Sort 
2:
Term of Sort Int (index \(i\) )


Create Term of this Kind with:

Create Op of this kind with:

 SEQ_CONCAT ¶

Sequence concat.

Arity:
n > 1

1..n:
Terms of sequence Sort


Create Term of this Kind with:

Create Op of this kind with:

 SEQ_CONTAINS ¶

Sequence contains.
Checks whether a sequence \(s_1\) contains another sequence \(s_2\) . If \(s_2\) is empty, the result is always
true
.
Arity:
2

1:
Term of sequence Sort ( \(s_1\) ) 
2:
Term of sequence Sort ( \(s_2\) )


Create Term of this Kind with:

Create Op of this kind with:

 SEQ_EXTRACT ¶

Sequence extract.
Extracts a subsequence, starting at index \(i\) and of length \(l\) , from a sequence \(s\) . If the start index is negative, the start index is greater than the length of the sequence, or the length is negative, the result is the empty sequence.

Arity:
3

1:
Term of sequence Sort 
2:
Term of Sort Int (index \(i\) ) 
3:
Term of Sort Int (length \(l\) )


Create Term of this Kind with:

Create Op of this kind with:

 SEQ_INDEXOF ¶

Sequence indexof.
Returns the index of a subsequence \(s_2\) in a sequence \(s_1\) starting at index \(i\) . If the index is negative or greater than the length of sequence \(s_1\) or the subsequence \(s_2\) does not appear in sequence \(s_1\) after index \(i\) , the result is 1.

Arity:
3

1:
Term of sequence Sort ( \(s_1\) ) 
2:
Term of sequence Sort ( \(s_2\) ) 
3:
Term of Sort Int ( \(i\) )


Create Term of this Kind with:

Create Op of this kind with:

 SEQ_LENGTH ¶

Sequence length.

Arity:
1

1:
Term of sequence Sort


Create Term of this Kind with:

Create Op of this kind with:

 SEQ_NTH ¶

Sequence nth.
Corresponds to the nth element of a sequence.

Arity:
2

1:
Term of sequence Sort 
2:
Term of Sort Int ( \(n\) )


Create Term of this Kind with:

Create Op of this kind with:

 SEQ_PREFIX ¶

Sequence prefixof.
Checks whether a sequence \(s_1\) is a prefix of sequence \(s_2\) . If sequence \(s_1\) is empty, this operator returns
true
.
Arity:
1

1:
Term of sequence Sort ( \(s_1\) ) 
2:
Term of sequence Sort ( \(s_2\) )


Create Term of this Kind with:

Create Op of this kind with:

 SEQ_REPLACE ¶

Sequence replace.
Replaces the first occurrence of a sequence \(s_2\) in a sequence \(s_1\) with sequence \(s_3\) . If \(s_2\) does not appear in \(s_1\) , \(s_1\) is returned unmodified.

Arity:
3

1:
Term of sequence Sort ( \(s_1\) ) 
2:
Term of sequence Sort ( \(s_2\) ) 
3:
Term of sequence Sort ( \(s_3\) )


Create Term of this Kind with:

Create Op of this kind with:

 SEQ_REPLACE_ALL ¶

Sequence replace all.
Replaces all occurrences of a sequence \(s_2\) in a sequence \(s_1\) with sequence \(s_3\) . If \(s_2\) does not appear in \(s_1\) , sequence \(s_1\) is returned unmodified.

Arity:
3

1:
Term of sequence Sort ( \(s_1\) ) 
2:
Term of sequence Sort ( \(s_2\) ) 
3:
Term of sequence Sort ( \(s_3\) )


Create Term of this Kind with:

Create Op of this kind with:

 SEQ_REV ¶

Sequence reverse.

Arity:
1

1:
Term of sequence Sort


Create Term of this Kind with:

Create Op of this kind with:

 SEQ_SUFFIX ¶

Sequence suffixof.
Checks whether a sequence \(s_1\) is a suffix of sequence \(s_2\) . If sequence \(s_1\) is empty, this operator returns
true
.
Arity:
1

1:
Term of sequence Sort ( \(s_1\) ) 
2:
Term of sequence Sort ( \(s_2\) )


Create Term of this Kind with:

Create Op of this kind with:

 SEQ_UNIT ¶

Sequence unit.
Corresponds to a sequence of length one with the given term.

Arity:
1

1:
Term of any Sort (the element term)


Create Term of this Kind with:

Create Op of this kind with:

 SEQ_UPDATE ¶

Sequence update.
Updates a sequence \(s\) by replacing its context starting at an index with string \(t\) . If the start index is negative, the start index is greater than the length of the sequence, the result is \(s\) . Otherwise, the length of the original sequence is preserved.

Arity:
3

1:
Term of sequence Sort 
2:
Term of Sort Int (index \(i\) ) 
3:
Term of sequence Sort (replacement sequence \(t\) )


Create Term of this Kind with:

Create Op of this kind with:

 SET_CARD ¶

Set cardinality.

Arity:
1

1:
Term of set Sort


Create Term of this Kind with:

Create Op of this kind with:

 SET_CHOOSE ¶

Set choose.
Select an element from a given set. For a set \(A = \{x\}\) , the term (set.choose \(A\) ) is equivalent to the term \(x_1\) . For an empty set, it is an arbitrary value. For a set with cardinality > 1, it will deterministically return an element in \(A\) .

Arity:
1

1:
Term of set Sort


Create Term of this Kind with:

Create Op of this kind with:
Warning
This kind is experimental and may be changed or removed in future versions.

 SET_COMPLEMENT ¶

Set complement with respect to finite universe.

Arity:
1

1:
Term of set Sort


Create Term of this Kind with:

Create Op of this kind with:

 SET_COMPREHENSION ¶

Set comprehension
A set comprehension is specified by a variable list \(x_1 ... x_n\) , a predicate \(P[x_1...x_n]\) , and a term \(t[x_1...x_n]\) . A comprehension \(C\) with the above form has members given by the following semantics:
\[\forall y. ( \exists x_1...x_n. P[x_1...x_n] \wedge t[x_1...x_n] = y ) \Leftrightarrow (set.member \; y \; C)\]where \(y\) ranges over the element Sort of the (set) Sort of the comprehension. If \(t[x_1..x_n]\) is not provided, it is equivalent to \(y\) in the above formula.

Arity:
3

1:
Term of KindVARIABLE_LIST

2:
Term of sort Bool (the predicate of the comprehension) 
3:
(optional) Term denoting the generator for the comprehension


Create Term of this Kind with:

Create Op of this kind with:
Warning
This kind is experimental and may be changed or removed in future versions.

 SET_EMPTY ¶

Empty set.

Create Term of this Kind with:

 SET_FILTER ¶

Set filter.
This operator filters the elements of a set. (set.filter \(p \; A\) ) takes a predicate \(p\) of Sort \((\rightarrow T \; Bool)\) as a first argument, and a set \(A\) of Sort (Set \(T\) ) as a second argument, and returns a subset of Sort (Set \(T\) ) that includes all elements of \(A\) that satisfy \(p\) .

Arity:
2

1:
Term of function Sort \((\rightarrow T \; Bool)\) 
2:
Term of bag Sort (Set \(T\) )


Create Term of this Kind with:
Warning
This kind is experimental and may be changed or removed in future versions.

 SET_FOLD ¶

Set fold.
This operator combines elements of a set into a single value. (set.fold \(f \; t \; A\) ) folds the elements of set \(A\) starting with Term \(t\) and using the combining function \(f\) .

Arity:
2

1:
Term of function Sort \((\rightarrow S_1 \; S_2 \; S_2)\) 
2:
Term of Sort \(S_2\) (the initial value) 
3:
Term of bag Sort (Set \(S_1\) )


Create Term of this Kind with:
Warning
This kind is experimental and may be changed or removed in future versions.

 SET_INSERT ¶

The set obtained by inserting elements;

Arity:
n > 0

1..n1:
Terms of any Sort (must match the element sort of the given set Term) 
n:
Term of set Sort


Create Term of this Kind with:

Create Op of this kind with:

 SET_INTER ¶

Set intersection.

Arity:
2

1..2:
Terms of set Sort


Create Term of this Kind with:

Create Op of this kind with:

 SET_IS_SINGLETON ¶

Set is singleton tester.

Arity:
1

1:
Term of set Sort


Create Term of this Kind with:

Create Op of this kind with:
Warning
This kind is experimental and may be changed or removed in future versions.

 SET_MAP ¶

Set map.
This operator applies the first argument, a function of Sort \((\rightarrow S_1 \; S_2)\) , to every element of the second argument, a set of Sort (Set \(S_1\) ), and returns a set of Sort (Set \(S_2\) ).

Arity:
2

1:
Term of function Sort \((\rightarrow S_1 \; S_2)\) 
2:
Term of set Sort (Set \(S_1\) )


Create Term of this Kind with:

Create Op of this kind with:
Warning
This kind is experimental and may be changed or removed in future versions.

 SET_MEMBER ¶

Set membership predicate.
Determines if the given set element is a member of the second set.

Arity:
2

1:
Term of any Sort (must match the element Sort of the given set Term) 
2:
Term of set Sort


Create Term of this Kind with:

Create Op of this kind with:

 SET_MINUS ¶

Set subtraction.

Arity:
2

1..2:
Terms of set Sort


Create Term of this Kind with:

Create Op of this kind with:

 SET_SINGLETON ¶

Singleton set.
Construct a singleton set from an element given as a parameter. The returned set has the same Sort as the element.

Arity:
1

1:
Term of any Sort (the set element)


Create Term of this Kind with:

Create Op of this kind with:

 SET_SUBSET ¶

Subset predicate.
Determines if the first set is a subset of the second set.

Arity:
2

1..2:
Terms of set Sort


Create Term of this Kind with:

Create Op of this kind with:

 SET_UNION ¶

Set union.

Arity:
2

1..2:
Terms of set Sort


Create Term of this Kind with:

Create Op of this kind with:

 SET_UNIVERSE ¶

Finite universe set.
All set variables must be interpreted as subsets of it.

Create Term of this Kind with:
Note
SET_UNIVERSE
is considered a special symbol of the theory of sets and is not considered as a set value, i.e.,Term.isSetValue()
will returnfalse
. 
 SEXPR ¶

Symbolic expression.

Arity:
n > 0

1..n:
Terms with same sorts


Create Term of this Kind with:

Create Op of this kind with:
Warning
This kind is experimental and may be changed or removed in future versions.

 SINE ¶

Sine function.

Arity:
1

1:
Term of Sort Real


Create Term of this Kind with:

Create Op of this kind with:

 SKOLEM_ADD_TO_POOL ¶

A skolemizationaddtopool annotation.
An skolemizationaddtopool annotation indicates that when a quantified formula is skolemized, the skolemized version of a term should be added to the given pool.
For example, consider a quantified formula:
(FORALL (VARIABLE_LIST x) F (INST_PATTERN_LIST (SKOLEM_ADD_TO_POOL (ADD x 1) p)))
where assume that \(x\) has type Int. When this quantified formula is skolemized, e.g., with \(k\) of type Int, then the term
(ADD k 1)
is added to the pool \(p\) .
Arity:
2

1:
The Term whose free variables are bound by the quantified formula. 
2:
The pool to add to, whose Sort should be a set of elements that match the Sort of the first argument.


Create Term of this Kind with:

Create Op of this kind with:
Warning
This kind is experimental and may be changed or removed in future versions.
Note
Should only be used as a child of
INST_PATTERN_LIST
. 
 SQRT ¶

Square root.

Arity:
1

1:
Term of Sort Real


Create Term of this Kind with:

Create Op of this kind with:

 STORE ¶

Array store.

Arity:
3

1:
Term of array Sort 
2:
Term of array index Sort 
3:
Term of array element Sort


Create Term of this Kind with:

Create Op of this kind with:

 STRING_CHARAT ¶

String character at.
Returns the character at index \(i\) from a string \(s\) . If the index is negative or the index is greater than the length of the string, the result is the empty string. Otherwise the result is a string of length 1.

Arity:
2

1:
Term of Sort String (string \(s\) ) 
2:
Term of Sort Int (index \(i\) )


Create Term of this Kind with:

Create Op of this kind with:

 STRING_CONCAT ¶

String concat.

Arity:
n > 1

1..n:
Terms of Sort String


Create Term of this Kind with:

Create Op of this kind with:

 STRING_CONTAINS ¶

String contains.
Determines whether a string \(s_1\) contains another string \(s_2\) . If \(s_2\) is empty, the result is always
true
.
Arity:
2

1:
Term of Sort String (the string \(s_1\) ) 
2:
Term of Sort String (the string \(s_2\) )


Create Term of this Kind with:

Create Op of this kind with:

 STRING_FROM_CODE ¶

String from code.
Returns a string containing a single character whose code point matches the argument to this function, or the empty string if the argument is outofbounds.

Arity:
1

1:
Term of Sort Int


Create Term of this Kind with:

Create Op of this kind with:

 STRING_FROM_INT ¶

Conversion from Int to String.
If the integer is negative this operator returns the empty string.

Arity:
1

1:
Term of Sort Int


Create Term of this Kind with:

Create Op of this kind with:

 STRING_INDEXOF ¶

String indexof.
Returns the index of a substring \(s_2\) in a string \(s_1\) starting at index \(i\) . If the index is negative or greater than the length of string \(s_1\) or the substring \(s_2\) does not appear in string \(s_1\) after index \(i\) , the result is 1.

Arity:
2

1:
Term of Sort String (substring \(s_1\) ) 
2:
Term of Sort String (substring \(s_2\) ) 
3:
Term of Sort Int (index \(i\) )


Create Term of this Kind with:

Create Op of this kind with:

 STRING_INDEXOF_RE ¶

String indexof regular expression match.
Returns the first match of a regular expression \(r\) in a string \(s\) . If the index is negative or greater than the length of string \(s_1\) , or \(r\) does not match a substring in \(s\) after index \(i\) , the result is 1.

Arity:
3

1:
Term of Sort String (string \(s\) ) 
2:
Term of Sort RegLan (regular expression \(r\) ) 
3:
Term of Sort Int (index \(i\) )


Create Term of this Kind with:

Create Op of this kind with:

 STRING_IN_REGEXP ¶

String membership.

Arity:
2

1:
Term of Sort String 
2:
Term of Sort RegLan


Create Term of this Kind with:

Create Op of this kind with:

 STRING_IS_DIGIT ¶

String isdigit.
Returns true if given string is a digit (it is one of
"0"
, …,"9"
).
Arity:
1

1:
Term of Sort String


Create Term of this Kind with:

Create Op of this kind with:

 STRING_LENGTH ¶

String length.

Arity:
1

1:
Term of Sort String


Create Term of this Kind with:

Create Op of this kind with:

 STRING_LEQ ¶

String less than or equal.
Returns true if string \(s_1\) is less than or equal to \(s_2\) based on a lexiographic ordering over code points.

Arity:
2

1:
Term of Sort String ( \(s_1\) ) 
2:
Term of Sort String ( \(s_2\) )


Create Term of this Kind with:

Create Op of this kind with:

 STRING_LT ¶

String less than.
Returns true if string \(s_1\) is (strictly) less than \(s_2\) based on a lexiographic ordering over code points.

Arity:
2

1:
Term of Sort String ( \(s_1\) ) 
2:
Term of Sort String ( \(s_2\) )


Create Term of this Kind with:

Create Op of this kind with:

 STRING_PREFIX ¶

String prefixof.
Determines whether a string \(s_1\) is a prefix of string \(s_2\) . If string s1 is empty, this operator returns
true
.
Arity:
2

1:
Term of Sort String ( \(s_1\) ) 
2:
Term of Sort String ( \(s_2\) )


Create Term of this Kind with:

Create Op of this kind with:

 STRING_REPLACE ¶

String replace.
Replaces a string \(s_2\) in a string \(s_1\) with string \(s_3\) . If \(s_2\) does not appear in \(s_1\) , \(s_1\) is returned unmodified.

Arity:
3

1:
Term of Sort String (string \(s_1\) ) 
2:
Term of Sort String (string \(s_2\) ) 
3:
Term of Sort String (string \(s_3\) )


Create Term of this Kind with:

Create Op of this kind with:

 STRING_REPLACE_ALL ¶

String replace all.
Replaces all occurrences of a string \(s_2\) in a string \(s_1\) with string \(s_3\) . If \(s_2\) does not appear in \(s_1\) , \(s_1\) is returned unmodified.

Arity:
3

1:
Term of Sort String ( \(s_1\) ) 
2:
Term of Sort String ( \(s_2\) ) 
3:
Term of Sort String ( \(s_3\) )


Create Term of this Kind with:

Create Op of this kind with:

 STRING_REPLACE_RE ¶

String replace regular expression match.
Replaces the first match of a regular expression \(r\) in string \(s_1\) with string \(s_2\) . If \(r\) does not match a substring of \(s_1\) , \(s_1\) is returned unmodified.

Arity:
3

1:
Term of Sort String ( \(s_1\) ) 
2:
Term of Sort RegLan 
3:
Term of Sort String ( \(s_2\) )


Create Term of this Kind with:

Create Op of this kind with:

 STRING_REPLACE_RE_ALL ¶

String replace all regular expression matches.
Replaces all matches of a regular expression \(r\) in string \(s_1\) with string \(s_2\) . If \(r\) does not match a substring of \(s_1\) , string \(s_1\) is returned unmodified.

Arity:
3

1:
Term of Sort String ( \(s_1\) ) 
2:
Term of Sort RegLan 
3:
Term of Sort String ( \(s_2\) )


Create Term of this Kind with:

Create Op of this kind with:

 STRING_REV ¶

String reverse.

Arity:
1

1:
Term of Sort String


Create Term of this Kind with:

Create Op of this kind with:

 STRING_SUBSTR ¶

String substring.
Extracts a substring, starting at index \(i\) and of length \(l\) , from a string \(s\) . If the start index is negative, the start index is greater than the length of the string, or the length is negative, the result is the empty string.

Arity:
3

1:
Term of Sort String 
2:
Term of Sort Int (index \(i\) ) 
3:
Term of Sort Int (length \(l\) )


Create Term of this Kind with:

Create Op of this kind with:

 STRING_SUFFIX ¶

String suffixof.
Determines whether a string \(s_1\) is a suffix of the second string. If string \(s_1\) is empty, this operator returns
true
.
Arity:
2

1:
Term of Sort String ( \(s_1\) ) 
2:
Term of Sort String ( \(s_2\) )


Create Term of this Kind with:

Create Op of this kind with:

 STRING_TO_CODE ¶

String to code.
Returns the code point of a string if it has length one, or returns 1 otherwise.

Arity:
1

1:
Term of Sort String


Create Term of this Kind with:

Create Op of this kind with:

 STRING_TO_INT ¶

String to integer (total function).
If the string does not contain an integer or the integer is negative, the operator returns 1 .

Arity:
1

1:
Term of Sort Int


Create Term of this Kind with:

Create Op of this kind with:

 STRING_TO_LOWER ¶

String to lower case.

Arity:
1

1:
Term of Sort String


Create Term of this Kind with:

Create Op of this kind with:

 STRING_TO_REGEXP ¶

Conversion from string to regexp.

Arity:
1

1:
Term of Sort String


Create Term of this Kind with:

Create Op of this kind with:

 STRING_TO_UPPER ¶

String to upper case.

Arity:
1

1:
Term of Sort String


Create Term of this Kind with:

Create Op of this kind with:

 STRING_UPDATE ¶

String update.
Updates a string \(s\) by replacing its context starting at an index with string \(t\) . If the start index is negative, the start index is greater than the length of the string, the result is \(s\) . Otherwise, the length of the original string is preserved.

Arity:
3

1:
Term of Sort String 
2:
Term of Sort Int (index \(i\) ) 
3:
Term of Sort Strong (replacement string \(t\) )


Create Term of this Kind with:

Create Op of this kind with:

 SUB ¶

Arithmetic subtraction, left associative.

Arity:
n > 1

1..n:
Terms of Sort Int or Real (sorts must match)


Create Term of this Kind with:

Create Op of this kind with:

 TABLE_AGGREGATE ¶

Table aggregate operator has the form \(((\_ \; table.aggr \; n_1 ... n_k) \; f \; i \; A)\) where \(n_1, ..., n_k\) are natural numbers, \(f\) is a function of type \((\rightarrow (Tuple \; T_1 \; ... \; T_j)\; T \; T)\) , \(i\) has the type \(T\) , and \(A\) has type \((Table \; T_1 \; ... \; T_j)\) . The returned type is \((Bag \; T)\) .
This operator aggregates elements in A that have the same tuple projection with indices n_1, …, n_k using the combining function \(f\) , and initial value \(i\) .

Arity:
3

1:
Term of sort \((\rightarrow (Tuple \; T_1 \; ... \; T_j)\; T \; T)\) 
2:
Term of Sort \(T\) 
3:
Term of table sort \(Table T_1 ... T_j\)


Indices:
n
1..n:
Indices of the projection 
Create Term of this Kind with: 
Solver.mkTerm()

Create Op of this kind with: 
Solver.mkOp()
Warning
This kind is experimental and may be changed or removed in future versions.

 TABLE_GROUP ¶

Table group
\(((\_ \; table.group \; n_1 \; \dots \; n_k) \; A)\) partitions tuples of table \(A\) such that tuples that have the same projection with indices \(n_1 \; \dots \; n_k\) are in the same part. It returns a bag of tables of type \((Bag \; T)\) where \(T\) is the type of \(A\) .

Arity:
1

1:
Term of table sort


Indices:
n

1..n:
Indices of the projection


Create Term of this Kind with:
Warning
This kind is experimental and may be changed or removed in future versions.

 TABLE_JOIN ¶

 Table join operator has the form

\(((\_ \; table.join \; m_1 \; n_1 \; \dots \; m_k \; n_k) \; A \; B)\) where \(m_1 \; n_1 \; \dots \; m_k \; n_k\) are natural numbers, and \(A, B\) are tables. This operator filters the product of two bags based on the equality of projected tuples using indices \(m_1, \dots, m_k\) in table \(A\) , and indices \(n_1, \dots, n_k\) in table \(B\) .

Arity:
2

1:
Term of table Sort 
2:
Term of table Sort


Indices:
n
1..n:
Indices of the projection 
Create Term of this Kind with: 
Solver.mkTerm()

Create Op of this kind with: 
Solver.mkOp()
Warning
This kind is experimental and may be changed or removed in future versions.
 TABLE_PRODUCT ¶

Table cross product.

Arity:
2

1..2:
Terms of table Sort


Create Term of this Kind with:

Create Op of this kind with:
Warning
This kind is experimental and may be changed or removed in future versions.

 TABLE_PROJECT ¶

Table projection operator extends tuple projection operator to tables.

Arity:
1
1:
Term of table Sort 
Indices:
n
1..n:
Indices of the projection 
Create Term of this Kind with: 
Solver.mkTerm()

Create Op of this kind with: 
Solver.mkOp()
Warning
This kind is experimental and may be changed or removed in future versions.

 TANGENT ¶

Tangent function.

Arity:
1

1:
Term of Sort Real


Create Term of this Kind with:

Create Op of this kind with:

 TO_INTEGER ¶

Convert Term of sort Int or Real to Int via the floor function.

Arity:
1

1:
Term of Sort Int or Real


Create Term of this Kind with:

Create Op of this kind with:

 TO_REAL ¶

Convert Term of Sort Int or Real to Real.

Arity:
1

1:
Term of Sort Int or Real


Create Term of this Kind with:

Create Op of this kind with:

 TUPLE_PROJECT ¶

Tuple projection.
This operator takes a tuple as an argument and returns a tuple obtained by concatenating components of its argument at the provided indices.
For example,
((_ tuple.project 1 2 2 3 1) (tuple 10 20 30 40))
yields
(tuple 20 30 30 40 20)

Arity:
1

1:
Term of tuple Sort


Indices:
n

1..n:
The tuple indices to project


Create Term of this Kind with:

Create Op of this kind with:

 UNDEFINED_KIND ¶

Undefined kind.
Note
Should never be exposed or created via the API.
 UNINTERPRETED_SORT_VALUE ¶

The value of an uninterpreted constant.
Note
May be returned as the result of an API call, but terms of this kind may not be created explicitly via the API and may not appear in assertions.
 VARIABLE ¶

(Bound) variable.

Create Term of this Kind with:
Note
Only permitted in bindings and in lambda and quantifier bodies.

 VARIABLE_LIST ¶

Variable list.
A list of variables (used to bind variables under a quantifier)

Arity:
n > 0

1..n:
Terms of KindVARIABLE


Create Term of this Kind with:

Create Op of this kind with:

 WITNESS ¶

Witness.
The syntax of a witness term is similar to a quantified formula except that only one variable is allowed. For example, the term
(witness ((x S)) F)
returns an element \(x\) of Sort \(S\) and asserts formula \(F\) .
The witness operator behaves like the description operator (see https: no \(x\) that satisfies \(F\) . But if such \(x\) exists, the witness operator does not enforce the following axiom which ensures uniqueness up to logical equivalence:
\[\forall x. F \equiv G \Rightarrow witness~x. F = witness~x. G\]For example, if there are two elements of Sort \(S\) that satisfy formula \(F\) , then the following formula is satisfiable:
(distinct (witness ((x Int)) F) (witness ((x Int)) F))

Arity:
3

1:
Term of kindVARIABLE_LIST

2:
Term of Sort Bool (the body of the witness) 
3:
(optional) Term of kindINST_PATTERN_LIST


Create Term of this Kind with:

Create Op of this kind with:
Note
This kind is primarily used internally, but may be returned in models (e.g., for arithmetic terms in nonlinear queries). However, it is not supported by the parser. Moreover, the user of the API should be cautious when using this operator. In general, all witness terms
(witness ((x Int)) F)
should be such that(exists ((x Int)) F)
is a valid formula. If this is not the case, then the semantics in formulas that use witness terms may be unintuitive. For example, the following formula is unsatisfiable:(or (= (witness ((x Int)) false) 0) (not (= (witness ((x Int)) false) 0))
, whereas notice that(or (= z 0) (not (= z 0)))
is true for any \(z\) . 
 XOR ¶

Logical exclusive disjunction, left associative.

Arity:
n > 1

1..n:
Terms of Sort Bool


Create Term of this Kind with:

Create Op of this kind with:
