Enum Constant and Description |
---|
ABS
Absolute value.
|
ADD
Arithmetic addition.
|
AND
Logical conjunction.
|
APPLY_CONSTRUCTOR
Datatype constructor application.
|
APPLY_SELECTOR
Datatype selector application.
|
APPLY_TESTER
Datatype tester application.
|
APPLY_UF
Application of an uninterpreted function.
|
APPLY_UPDATER
Datatype update application.
|
ARCCOSECANT
Arc cosecant function.
|
ARCCOSINE
Arc cosine function.
|
ARCCOTANGENT
Arc cotangent function.
|
ARCSECANT
Arc secant function.
|
ARCSINE
Arc sine function.
|
ARCTANGENT
Arc tangent function.
|
BAG_ALL
Bag all.
|
BAG_CARD
Bag cardinality.
|
BAG_CHOOSE
Bag choose.
|
BAG_COUNT
Bag element multiplicity.
|
BAG_DIFFERENCE_REMOVE
Bag difference remove.
|
BAG_DIFFERENCE_SUBTRACT
Bag difference subtract.
|
BAG_EMPTY
Empty bag.
|
BAG_FILTER
Bag filter.
|
BAG_FOLD
Bag fold.
|
BAG_INTER_MIN
Bag intersection (min).
|
BAG_MAKE
Bag make.
|
BAG_MAP
Bag map.
|
BAG_MEMBER
Bag membership predicate.
|
BAG_PARTITION
Bag partition.
|
BAG_SETOF
Bag setof.
|
BAG_SOME
Bag some.
|
BAG_SUBBAG
Bag inclusion predicate.
|
BAG_UNION_DISJOINT
Bag disjoint union (sum).
|
BAG_UNION_MAX
Bag max union.
|
BITVECTOR_ADD
Addition of two or more bit-vectors.
|
BITVECTOR_AND
Bit-wise and.
|
BITVECTOR_ASHR
Bit-vector arithmetic shift right.
|
BITVECTOR_BIT
Retrieves the bit at the given index from a bit-vector as a Bool term.
|
BITVECTOR_COMP
Equality comparison (returns bit-vector of size
1 ). |
BITVECTOR_CONCAT
Concatenation of two or more bit-vectors.
|
BITVECTOR_EXTRACT
Bit-vector extract.
|
BITVECTOR_FROM_BOOLS
Converts a list of Bool terms to a bit-vector.
|
BITVECTOR_ITE
Bit-vector if-then-else.
|
BITVECTOR_LSHR
Bit-vector logical shift right.
|
BITVECTOR_MULT
Multiplication of two or more bit-vectors.
|
BITVECTOR_NAND
Bit-wise nand.
|
BITVECTOR_NEG
Negation of a bit-vector (two's complement).
|
BITVECTOR_NEGO
Bit-vector negation overflow detection.
|
BITVECTOR_NOR
Bit-wise nor.
|
BITVECTOR_NOT
Bit-wise negation.
|
BITVECTOR_OR
Bit-wise or.
|
BITVECTOR_REDAND
Bit-vector redand.
|
BITVECTOR_REDOR
Bit-vector redor.
|
BITVECTOR_REPEAT
Bit-vector repeat.
|
BITVECTOR_ROTATE_LEFT
Bit-vector rotate left.
|
BITVECTOR_ROTATE_RIGHT
Bit-vector rotate right.
|
BITVECTOR_SADDO
Bit-vector signed addition overflow detection.
|
BITVECTOR_SBV_TO_INT
Bit-vector conversion, signed bit-vector to integer.
|
BITVECTOR_SDIV
Signed bit-vector division.
|
BITVECTOR_SDIVO
Bit-vector signed division overflow detection.
|
BITVECTOR_SGE
Bit-vector signed greater than or equal.
|
BITVECTOR_SGT
Bit-vector signed greater than.
|
BITVECTOR_SHL
Bit-vector shift left.
|
BITVECTOR_SIGN_EXTEND
Bit-vector sign extension.
|
BITVECTOR_SLE
Bit-vector signed less than or equal.
|
BITVECTOR_SLT
Bit-vector signed less than.
|
BITVECTOR_SLTBV
Bit-vector signed less than returning a bit-vector of size
1 . |
BITVECTOR_SMOD
Signed bit-vector remainder (sign follows divisor).
|
BITVECTOR_SMULO
Bit-vector signed multiplication overflow detection.
|
BITVECTOR_SREM
Signed bit-vector remainder (sign follows dividend).
|
BITVECTOR_SSUBO
Bit-vector signed subtraction overflow detection.
|
BITVECTOR_SUB
Subtraction of two bit-vectors.
|
BITVECTOR_TO_NAT
Bit-vector conversion to (non-negative) integer.
|
BITVECTOR_UADDO
Bit-vector unsigned addition overflow detection.
|
BITVECTOR_UBV_TO_INT
Bit-vector conversion, unsigned bit-vector to integer.
|
BITVECTOR_UDIV
Unsigned bit-vector division.
|
BITVECTOR_UGE
Bit-vector unsigned greater than or equal.
|
BITVECTOR_UGT
Bit-vector unsigned greater than.
|
BITVECTOR_ULE
Bit-vector unsigned less than or equal.
|
BITVECTOR_ULT
Bit-vector unsigned less than.
|
BITVECTOR_ULTBV
Bit-vector unsigned less than returning a bit-vector of size 1.
|
BITVECTOR_UMULO
Bit-vector unsigned multiplication overflow detection.
|
BITVECTOR_UREM
Unsigned bit-vector remainder.
|
BITVECTOR_USUBO
Bit-vector unsigned subtraction overflow detection.
|
BITVECTOR_XNOR
Bit-wise xnor, left associative.
|
BITVECTOR_XOR
Bit-wise xor.
|
BITVECTOR_ZERO_EXTEND
Bit-vector zero extension.
|
CARDINALITY_CONSTRAINT
Cardinality constraint on uninterpreted sort.
|
CONST_ARRAY
Constant array.
|
CONST_BITVECTOR
Fixed-size bit-vector constant.
|
CONST_BOOLEAN
Boolean constant.
|
CONST_FINITE_FIELD
Finite field constant.
|
CONST_FLOATINGPOINT
Floating-point constant, created from IEEE-754 bit-vector representation
of the floating-point value.
|
CONST_INTEGER
Arbitrary-precision integer constant.
|
CONST_RATIONAL
Arbitrary-precision rational constant.
|
CONST_ROUNDINGMODE
RoundingMode constant.
|
CONST_SEQUENCE
Constant sequence.
|
CONST_STRING
Constant string.
|
CONSTANT
Free constant symbol.
|
COSECANT
Cosecant function.
|
COSINE
Cosine function.
|
COTANGENT
Cotangent function.
|
DISTINCT
Disequality.
|
DIVISIBLE
Operator for the divisibility-by-\(k\) predicate.
|
DIVISION
Real division, division by 0 undefined, left associative.
|
DIVISION_TOTAL
Real division, division by 0 defined to be 0, left associative.
|
EQ_RANGE
Equality over arrays \(a\) and \(b\) over a given range
\([i,j]\), i.e.,
\[
\forall k .
|
EQUAL
Equality, chainable.
|
EXISTS
Existentially quantified formula.
|
EXPONENTIAL
Exponential function.
|
FINITE_FIELD_ADD
Addition of two or more finite field elements.
|
FINITE_FIELD_BITSUM
Bitsum of two or more finite field elements: x + 2y + 4z + ...
|
FINITE_FIELD_MULT
Multiplication of two or more finite field elements.
|
FINITE_FIELD_NEG
Negation of a finite field element (additive inverse).
|
FLOATINGPOINT_ABS
Floating-point absolute value.
|
FLOATINGPOINT_ADD
Floating-point addition.
|
FLOATINGPOINT_DIV
Floating-point division.
|
FLOATINGPOINT_EQ
Floating-point equality.
|
FLOATINGPOINT_FMA
Floating-point fused multiply and add.
|
FLOATINGPOINT_FP
Create floating-point literal from bit-vector triple.
|
FLOATINGPOINT_GEQ
Floating-point greater than or equal.
|
FLOATINGPOINT_GT
Floating-point greater than.
|
FLOATINGPOINT_IS_INF
Floating-point is infinite tester.
|
FLOATINGPOINT_IS_NAN
Floating-point is NaN tester.
|
FLOATINGPOINT_IS_NEG
Floating-point is negative tester.
|
FLOATINGPOINT_IS_NORMAL
Floating-point is normal tester.
|
FLOATINGPOINT_IS_POS
Floating-point is positive tester.
|
FLOATINGPOINT_IS_SUBNORMAL
Floating-point is sub-normal tester.
|
FLOATINGPOINT_IS_ZERO
Floating-point is zero tester.
|
FLOATINGPOINT_LEQ
Floating-point less than or equal.
|
FLOATINGPOINT_LT
Floating-point less than.
|
FLOATINGPOINT_MAX
Floating-point maximum.
|
FLOATINGPOINT_MIN
Floating-point minimum.
|
FLOATINGPOINT_MULT
Floating-point multiply.
|
FLOATINGPOINT_NEG
Floating-point negation.
|
FLOATINGPOINT_REM
Floating-point remainder.
|
FLOATINGPOINT_RTI
Floating-point round to integral.
|
FLOATINGPOINT_SQRT
Floating-point square root.
|
FLOATINGPOINT_SUB
Floating-point sutraction.
|
FLOATINGPOINT_TO_FP_FROM_FP
Conversion to floating-point from floating-point.
|
FLOATINGPOINT_TO_FP_FROM_IEEE_BV
Conversion to floating-point from IEEE-754 bit-vector.
|
FLOATINGPOINT_TO_FP_FROM_REAL
Conversion to floating-point from Real.
|
FLOATINGPOINT_TO_FP_FROM_SBV
Conversion to floating-point from signed bit-vector.
|
FLOATINGPOINT_TO_FP_FROM_UBV
Conversion to floating-point from unsigned bit-vector.
|
FLOATINGPOINT_TO_REAL
Conversion to Real from floating-point.
|
FLOATINGPOINT_TO_SBV
Conversion to signed bit-vector from floating-point.
|
FLOATINGPOINT_TO_UBV
Conversion to unsigned bit-vector from floating-point.
|
FORALL
Universally quantified formula.
|
GEQ
Greater than or equal, chainable.
|
GT
Greater than, chainable.
|
HO_APPLY
Higher-order applicative encoding of function application, left
associative.
|
IAND
Integer and.
|
IMPLIES
Logical implication.
|
INST_ADD_TO_POOL
A instantantiation-add-to-pool annotation.
|
INST_ATTRIBUTE
Instantiation attribute.
|
INST_NO_PATTERN
Instantiation no-pattern.
|
INST_PATTERN
Instantiation pattern.
|
INST_PATTERN_LIST
A list of instantiation patterns, attributes or annotations.
|
INST_POOL
Instantiation pool annotation.
|
INT_TO_BITVECTOR
Conversion from Int to bit-vector.
|
INTERNAL_KIND
Internal kind.
|
INTS_DIVISION
Integer division, division by 0 undefined, left associative.
|
INTS_DIVISION_TOTAL
Integer division, division by 0 defined to be 0, left associative.
|
INTS_MODULUS
Integer modulus, modulus by 0 undefined.
|
INTS_MODULUS_TOTAL
Integer modulus, t modulus by 0 defined to be t.
|
IS_INTEGER
Is-integer predicate.
|
ITE
If-then-else.
|
LAMBDA
Lambda expression.
|
LAST_KIND
Marks the upper-bound of this enumeration.
|
LEQ
Less than or equal, chainable.
|
LT
Less than, chainable.
|
MATCH
Match expression.
|
MATCH_BIND_CASE
Match case with binders, for constructors with selectors and variable
patterns.
|
MATCH_CASE
Match case for nullary constructors.
|
MULT
Arithmetic multiplication.
|
NEG
Arithmetic negation.
|
NOT
Logical negation.
|
NULL_TERM
Null kind.
|
NULLABLE_LIFT
Lifting operator for nullable terms.
|
OR
Logical disjunction.
|
PI
Pi constant.
|
POW
Arithmetic power.
|
POW2
Power of two.
|
REGEXP_ALL
Regular expression all.
|
REGEXP_ALLCHAR
Regular expression all characters.
|
REGEXP_COMPLEMENT
Regular expression complement.
|
REGEXP_CONCAT
Regular expression concatenation.
|
REGEXP_DIFF
Regular expression difference.
|
REGEXP_INTER
Regular expression intersection.
|
REGEXP_LOOP
Regular expression loop.
|
REGEXP_NONE
Regular expression none.
|
REGEXP_OPT
Regular expression ?.
|
REGEXP_PLUS
Regular expression +.
|
REGEXP_RANGE
Regular expression range.
|
REGEXP_REPEAT
Operator for regular expression repeat.
|
REGEXP_STAR
Regular expression \*.
|
REGEXP_UNION
Regular expression union.
|
RELATION_AGGREGATE
Relation aggregate operator has the form
\(((\_ \; rel.aggr \; n_1 ...
|
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.
|
RELATION_IDEN
Relation identity.
|
RELATION_JOIN
Relation join.
|
RELATION_JOIN_IMAGE
Relation join image.
|
RELATION_PRODUCT
Relation cartesian product.
|
RELATION_PROJECT
Relation projection operator extends tuple projection operator to sets.
|
RELATION_TABLE_JOIN
Table join operator for relations has the form
\(((\_ \; rel.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 relations.
|
RELATION_TCLOSURE
Relation transitive closure.
|
RELATION_TRANSPOSE
Relation transpose.
|
SECANT
Secant function.
|
SELECT
Array select.
|
SEP_EMP
Separation logic empty heap.
|
SEP_NIL
Separation logic nil.
|
SEP_PTO
Separation logic points-to relation.
|
SEP_STAR
Separation logic star.
|
SEP_WAND
Separation logic magic wand.
|
SEQ_AT
Sequence element at.
|
SEQ_CONCAT
Sequence concat.
|
SEQ_CONTAINS
Sequence contains.
|
SEQ_EXTRACT
Sequence extract.
|
SEQ_INDEXOF
Sequence index-of.
|
SEQ_LENGTH
Sequence length.
|
SEQ_NTH
Sequence nth.
|
SEQ_PREFIX
Sequence prefix-of.
|
SEQ_REPLACE
Sequence replace.
|
SEQ_REPLACE_ALL
Sequence replace all.
|
SEQ_REV
Sequence reverse.
|
SEQ_SUFFIX
Sequence suffix-of.
|
SEQ_UNIT
Sequence unit.
|
SEQ_UPDATE
Sequence update.
|
SET_ALL
Set all.
|
SET_CARD
Set cardinality.
|
SET_CHOOSE
Set choose.
|
SET_COMPLEMENT
Set complement with respect to finite universe.
|
SET_COMPREHENSION
Set comprehension
A set comprehension is specified by a variable list \(x_1 ...
|
SET_EMPTY
Empty set.
|
SET_FILTER
Set filter.
|
SET_FOLD
Set fold.
|
SET_INSERT
The set obtained by inserting elements;
Arity:
n > 0
1..n-1: 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:
Solver.mkTerm(Kind, Term[])
Solver.mkTerm(Op, Term[])
Create Op of this kind with:
Solver.mkOp(Kind, int[])
|
SET_INTER
Set intersection.
|
SET_IS_EMPTY
Set is empty tester.
|
SET_IS_SINGLETON
Set is singleton tester.
|
SET_MAP
Set map.
|
SET_MEMBER
Set membership predicate.
|
SET_MINUS
Set subtraction.
|
SET_SINGLETON
Singleton set.
|
SET_SOME
Set some.
|
SET_SUBSET
Subset predicate.
|
SET_UNION
Set union.
|
SET_UNIVERSE
Finite universe set.
|
SEXPR
Symbolic expression.
|
SINE
Sine function.
|
SKOLEM
A Skolem.
|
SKOLEM_ADD_TO_POOL
A skolemization-add-to-pool annotation.
|
SQRT
Square root.
|
STORE
Array store.
|
STRING_CHARAT
String character at.
|
STRING_CONCAT
String concat.
|
STRING_CONTAINS
String contains.
|
STRING_FROM_CODE
String from code.
|
STRING_FROM_INT
Conversion from Int to String.
|
STRING_IN_REGEXP
String membership.
|
STRING_INDEXOF
String index-of.
|
STRING_INDEXOF_RE
String index-of regular expression match.
|
STRING_IS_DIGIT
String is-digit.
|
STRING_LENGTH
String length.
|
STRING_LEQ
String less than or equal.
|
STRING_LT
String less than.
|
STRING_PREFIX
String prefix-of.
|
STRING_REPLACE
String replace.
|
STRING_REPLACE_ALL
String replace all.
|
STRING_REPLACE_RE
String replace regular expression match.
|
STRING_REPLACE_RE_ALL
String replace all regular expression matches.
|
STRING_REV
String reverse.
|
STRING_SUBSTR
String substring.
|
STRING_SUFFIX
String suffix-of.
|
STRING_TO_CODE
String to code.
|
STRING_TO_INT
String to integer (total function).
|
STRING_TO_LOWER
String to lower case.
|
STRING_TO_REGEXP
Conversion from string to regexp.
|
STRING_TO_UPPER
String to upper case.
|
STRING_UPDATE
String update.
|
SUB
Arithmetic subtraction, left associative.
|
TABLE_AGGREGATE
Table aggregate operator has the form
\(((\_ \; table.aggr \; n_1 ...
|
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.
|
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.
|
TABLE_PRODUCT
Table cross product.
|
TABLE_PROJECT
Table projection operator extends tuple projection operator to tables.
|
TANGENT
Tangent function.
|
TO_INTEGER
Convert Term of sort Int or Real to Int via the floor function.
|
TO_REAL
Convert Term of Sort Int or Real to Real.
|
TUPLE_PROJECT
Tuple projection.
|
UNDEFINED_KIND
Undefined kind.
|
UNINTERPRETED_SORT_VALUE
The value of an uninterpreted constant.
|
VARIABLE
(Bound) variable.
|
VARIABLE_LIST
Variable list.
|
WITNESS
Witness.
|
XOR
Logical exclusive disjunction, left associative.
|
Modifier and Type | Method and Description |
---|---|
static Kind |
fromInt(int value) |
int |
getValue() |
static Kind |
valueOf(java.lang.String name)
Returns the enum constant of this type with the specified name.
|
static Kind[] |
values()
Returns an array containing the constants of this enum type, in
the order they are declared.
|
public static final Kind INTERNAL_KIND
public static final Kind UNDEFINED_KIND
public static final Kind NULL_TERM
Term()
).Term()
.public static final Kind UNINTERPRETED_SORT_VALUE
public static final Kind EQUAL
n > 1
1..n:
Terms of the same Sort
public static final Kind DISTINCT
n > 1
1..n:
Terms of the same Sort
public static final Kind CONSTANT
public static final Kind VARIABLE
public static final Kind SKOLEM
public static final Kind SEXPR
n > 0
1..n:
Terms with same sorts
public static final Kind LAMBDA
2
1:
Term of kind VARIABLE_LIST
2:
Term of any Sort (the body of the lambda)
public static final Kind WITNESS
3
1:
Term of kind VARIABLE_LIST
2:
Term of Sort Bool (the body of the witness)
3:
(optional) Term of kind INST_PATTERN_LIST
(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\).public static final Kind CONST_BOOLEAN
public static final Kind NOT
1
1:
Term of Sort Bool
public static final Kind AND
n > 1
1..n:
Terms of Sort Bool
public static final Kind IMPLIES
n > 1
1..n:
Terms of Sort Bool
public static final Kind OR
n > 1
1..n:
Terms of Sort Bool
public static final Kind XOR
n > 1
1..n:
Terms of Sort Bool
public static final Kind ITE
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
public static final Kind APPLY_UF
n > 1
1:
Function Term
2..n:
Function argument instantiation Terms of any first-class Sort
public static final Kind CARDINALITY_CONSTRAINT
public static final Kind HO_APPLY
n = 2
1:
Function Term
2:
Argument Term of the domain Sort of the function
public static final Kind ADD
n > 1
1..n:
Terms of Sort Int or Real (sorts must match)
public static final Kind MULT
n > 1
1..n:
Terms of Sort Int or Real (sorts must match)
public static final Kind IAND
AND
over integers, parameterized by a (positive)
bit-width \(k\).
.. code. smtlib
((_ iand k) i_1 i_2)
is equivalent to
.. code. smtlib
((_ iand k) i_1 i_2)
(bv2int (bvand ((_ int2bv k) i_1) ((_ int2bv k) i_2)))
for all integers i_1
, i_2
.
2
1..2:
Terms of Sort Int
1
1:
Bit-width \(k\)
public static final Kind POW2
2
to a non-negative integer power.
1
1:
Term of Sort Int
public static final Kind SUB
n > 1
1..n:
Terms of Sort Int or Real (sorts must match)
public static final Kind NEG
1
1:
Term of Sort Int or Real
public static final Kind DIVISION
n > 1
1..n:
Terms of Sort Real
public static final Kind DIVISION_TOTAL
n > 1
1..n:
Terms of Sort Real
public static final Kind INTS_DIVISION
n > 1
1..n:
Terms of Sort Int
public static final Kind INTS_DIVISION_TOTAL
n > 1
1..n:
Terms of Sort Int
public static final Kind INTS_MODULUS
2
1:
Term of Sort Int
2:
Term of Sort Int
public static final Kind INTS_MODULUS_TOTAL
2
1:
Term of Sort Int
2:
Term of Sort Int
public static final Kind ABS
1
1:
Term of Sort Int or Real
public static final Kind POW
2
1..2:
Term of Sort Int or Real (sorts must match)
public static final Kind EXPONENTIAL
1
1:
Term of Sort Real
public static final Kind SINE
1
1:
Term of Sort Real
public static final Kind COSINE
1
1:
Term of Sort Real
public static final Kind TANGENT
1
1:
Term of Sort Real
public static final Kind COSECANT
1
1:
Term of Sort Real
public static final Kind SECANT
1
1:
Term of Sort Real
public static final Kind COTANGENT
1
1:
Term of Sort Real
public static final Kind ARCSINE
1
1:
Term of Sort Real
public static final Kind ARCCOSINE
1
1:
Term of Sort Real
public static final Kind ARCTANGENT
1
1:
Term of Sort Real
public static final Kind ARCCOSECANT
1
1:
Term of Sort Real
public static final Kind ARCSECANT
1
1:
Term of Sort Real
public static final Kind ARCCOTANGENT
1
1:
Term of Sort Real
public static final Kind SQRT
1
1:
Term of Sort Real
public static final Kind DIVISIBLE
1
1:
Term of Sort Int
1
1:
The integer \(k\) to divide by.
public static final Kind CONST_RATIONAL
public static final Kind CONST_INTEGER
public static final Kind LT
n > 1
1..n:
Terms of Sort Int or Real (sorts must match)
public static final Kind LEQ
n > 1
1..n:
Terms of Sort Int or Real (sorts must match)
public static final Kind GT
n > 1
1..n:
Terms of Sort Int or Real (sorts must match)
public static final Kind GEQ
n > 1
1..n:
Terms of Sort Int or Real (sorts must match)
public static final Kind IS_INTEGER
1
1:
Term of Sort Int or Real
public static final Kind TO_INTEGER
1
1:
Term of Sort Int or Real
public static final Kind TO_REAL
1
1:
Term of Sort Int or Real
public static final Kind PI
Term.isRealValue()
will return false
.public static final Kind CONST_BITVECTOR
public static final Kind BITVECTOR_CONCAT
n > 1
1..n:
Terms of bit-vector Sort (sorts must match)
public static final Kind BITVECTOR_AND
n > 1
1..n:
Terms of bit-vector Sort (sorts must match)
public static final Kind BITVECTOR_OR
n > 1
1..n:
Terms of bit-vector Sort (sorts must match)
public static final Kind BITVECTOR_XOR
n > 1
1..n:
Terms of bit-vector Sort (sorts must match)
public static final Kind BITVECTOR_NOT
1
1:
Term of bit-vector Sort
public static final Kind BITVECTOR_NAND
2
1..2:
Terms of bit-vector Sort (sorts must match)
public static final Kind BITVECTOR_NOR
2
1..2:
Terms of bit-vector Sort (sorts must match)
public static final Kind BITVECTOR_XNOR
2
1..2:
Terms of bit-vector Sort (sorts must match)
public static final Kind BITVECTOR_COMP
1
).
2
1..2:
Terms of bit-vector Sort (sorts must match)
public static final Kind BITVECTOR_MULT
n > 1
1..n:
Terms of bit-vector Sort (sorts must match)
public static final Kind BITVECTOR_ADD
n > 1
1..n:
Terms of bit-vector Sort (sorts must match)
public static final Kind BITVECTOR_SUB
n > 1
1..n:
Terms of bit-vector Sort (sorts must match)
public static final Kind BITVECTOR_NEG
1
1:
Term of bit-vector Sort
public static final Kind BITVECTOR_UDIV
0
. If the divisor is zero, the result is all ones.
2
1..2:
Terms of bit-vector Sort (sorts must match)
public static final Kind BITVECTOR_UREM
2
1..2:
Terms of bit-vector Sort (sorts must match)
public static final Kind BITVECTOR_SDIV
2
1..2:
Terms of bit-vector Sort (sorts must match)
public static final Kind BITVECTOR_SREM
2
1..2:
Terms of bit-vector Sort (sorts must match)
public static final Kind BITVECTOR_SMOD
2
1..2:
Terms of bit-vector Sort (sorts must match)
public static final Kind BITVECTOR_SHL
2
1..2:
Terms of bit-vector Sort (sorts must match)
public static final Kind BITVECTOR_LSHR
2
1..2:
Terms of bit-vector Sort (sorts must match)
public static final Kind BITVECTOR_ASHR
2
1..2:
Terms of bit-vector Sort (sorts must match)
public static final Kind BITVECTOR_ULT
2
1..2:
Terms of bit-vector Sort (sorts must match)
public static final Kind BITVECTOR_ULE
2
1..2:
Terms of bit-vector Sort (sorts must match)
public static final Kind BITVECTOR_UGT
2
1..2:
Terms of bit-vector Sort (sorts must match)
public static final Kind BITVECTOR_UGE
2
1..2:
Terms of bit-vector Sort (sorts must match)
public static final Kind BITVECTOR_SLT
2
1..2:
Terms of bit-vector Sort (sorts must match)
public static final Kind BITVECTOR_SLE
2
1..2:
Terms of bit-vector Sort (sorts must match)
public static final Kind BITVECTOR_SGT
2
1..2:
Terms of bit-vector Sort (sorts must match)
public static final Kind BITVECTOR_SGE
2
1..2:
Terms of bit-vector Sort (sorts must match)
public static final Kind BITVECTOR_ULTBV
2
1..2:
Terms of bit-vector Sort (sorts must match)
public static final Kind BITVECTOR_SLTBV
1
.
2
1..2:
Terms of bit-vector Sort (sorts must match)
public static final Kind BITVECTOR_ITE
1
.
3
1:
Term of bit-vector Sort of size `1`
1..3:
Terms of bit-vector sort (sorts must match)
public static final Kind BITVECTOR_REDOR
1
1:
Term of bit-vector Sort
public static final Kind BITVECTOR_REDAND
1
1:
Term of bit-vector Sort
public static final Kind BITVECTOR_NEGO
1
1:
Term of bit-vector Sort
public static final Kind BITVECTOR_UADDO
2
1..2:
Terms of bit-vector Sort (sorts must match)
public static final Kind BITVECTOR_SADDO
2
1..2:
Terms of bit-vector Sort (sorts must match)
public static final Kind BITVECTOR_UMULO
2
1..2:
Terms of bit-vector Sort (sorts must match)
public static final Kind BITVECTOR_SMULO
2
1..2:
Terms of bit-vector Sort (sorts must match)
public static final Kind BITVECTOR_USUBO
2
1..2:
Terms of bit-vector Sort (sorts must match)
public static final Kind BITVECTOR_SSUBO
2
1..2:
Terms of bit-vector Sort (sorts must match)
public static final Kind BITVECTOR_SDIVO
2
1..2:
Terms of bit-vector Sort (sorts must match)
public static final Kind BITVECTOR_EXTRACT
1
1:
Term of bit-vector Sort
2
1:
The upper bit index.
2:
The lower bit index.
public static final Kind BITVECTOR_REPEAT
1
1:
Term of bit-vector Sort
1
1:
The number of times to repeat the given term.
public static final Kind BITVECTOR_ZERO_EXTEND
1
1:
Term of bit-vector Sort
1
1:
The number of zeroes to extend the given term with.
public static final Kind BITVECTOR_SIGN_EXTEND
1
1:
Term of bit-vector Sort
1
1:
The number of bits (of the value of the sign bit) to extend the given term with.
public static final Kind BITVECTOR_ROTATE_LEFT
1
1:
Term of bit-vector Sort
1
1:
The number of bits to rotate the given term left.
public static final Kind BITVECTOR_ROTATE_RIGHT
1
1:
Term of bit-vector Sort
1
1:
The number of bits to rotate the given term right.
public static final Kind INT_TO_BITVECTOR
1
1:
Term of Sort Int
1
1:
The size of the bit-vector to convert to.
public static final Kind BITVECTOR_TO_NAT
1
1:
Term of bit-vector Sort
public static final Kind BITVECTOR_UBV_TO_INT
1
1:
Term of bit-vector Sort
public static final Kind BITVECTOR_SBV_TO_INT
1
1:
Term of bit-vector Sort
public static final Kind BITVECTOR_FROM_BOOLS
n > 0
1..n:
Terms of Sort Bool
public static final Kind BITVECTOR_BIT
1
1:
Term of bit-vector Sort
1
1:
The bit index
public static final Kind CONST_FINITE_FIELD
public static final Kind FINITE_FIELD_NEG
1
1:
Term of finite field Sort
public static final Kind FINITE_FIELD_ADD
n > 1
1..n:
Terms of finite field Sort (sorts must match)
public static final Kind FINITE_FIELD_BITSUM
n > 1
1..n:
Terms of finite field Sort (sorts must match)
public static final Kind FINITE_FIELD_MULT
n > 1
1..n:
Terms of finite field Sort (sorts must match)
public static final Kind CONST_FLOATINGPOINT
public static final Kind CONST_ROUNDINGMODE
public static final Kind FLOATINGPOINT_FP
3
1:
Term of bit-vector Sort of size `1` (sign bit)
2:
Term of bit-vector Sort of exponent size (exponent)
3:
Term of bit-vector Sort of significand size - 1 (significand without hidden bit)
public static final Kind FLOATINGPOINT_EQ
2
1..2:
Terms of floating-point Sort (sorts must match)
public static final Kind FLOATINGPOINT_ABS
1
1:
Term of floating-point Sort
public static final Kind FLOATINGPOINT_NEG
1
1:
Term of floating-point Sort
public static final Kind FLOATINGPOINT_ADD
3
1:
Term of Sort RoundingMode
2..3:
Terms of floating-point Sort (sorts must match)
public static final Kind FLOATINGPOINT_SUB
3
1:
Term of Sort RoundingMode
2..3:
Terms of floating-point Sort (sorts must match)
public static final Kind FLOATINGPOINT_MULT
3
1:
Term of Sort RoundingMode
2..3:
Terms of floating-point Sort (sorts must match)
public static final Kind FLOATINGPOINT_DIV
3
1:
Term of Sort RoundingMode
2..3:
Terms of floating-point Sort (sorts must match)
public static final Kind FLOATINGPOINT_FMA
4
1:
Term of Sort RoundingMode
2..4:
Terms of floating-point Sort (sorts must match)
public static final Kind FLOATINGPOINT_SQRT
2
1:
Term of Sort RoundingMode
2:
Term of floating-point Sort
public static final Kind FLOATINGPOINT_REM
2
1..2:
Terms of floating-point Sort (sorts must match)
public static final Kind FLOATINGPOINT_RTI
2
1..2:
Terms of floating-point Sort (sorts must match)
public static final Kind FLOATINGPOINT_MIN
2
1:
Term of Sort RoundingMode
2:
Term of floating-point Sort
public static final Kind FLOATINGPOINT_MAX
2
1..2:
Terms of floating-point Sort (sorts must match)
public static final Kind FLOATINGPOINT_LEQ
2
1..2:
Terms of floating-point Sort (sorts must match)
public static final Kind FLOATINGPOINT_LT
2
1..2:
Terms of floating-point Sort (sorts must match)
public static final Kind FLOATINGPOINT_GEQ
2
1..2:
Terms of floating-point Sort (sorts must match)
public static final Kind FLOATINGPOINT_GT
2
1..2:
Terms of floating-point Sort (sorts must match)
public static final Kind FLOATINGPOINT_IS_NORMAL
1
1:
Term of floating-point Sort
public static final Kind FLOATINGPOINT_IS_SUBNORMAL
1
1:
Term of floating-point Sort
public static final Kind FLOATINGPOINT_IS_ZERO
1
1:
Term of floating-point Sort
public static final Kind FLOATINGPOINT_IS_INF
1
1:
Term of floating-point Sort
public static final Kind FLOATINGPOINT_IS_NAN
1
1:
Term of floating-point Sort
public static final Kind FLOATINGPOINT_IS_NEG
1
1:
Term of floating-point Sort
public static final Kind FLOATINGPOINT_IS_POS
1
1:
Term of floating-point Sort
public static final Kind FLOATINGPOINT_TO_FP_FROM_IEEE_BV
1
1:
Term of bit-vector Sort
2
1:
The exponent size
2:
The significand size
public static final Kind FLOATINGPOINT_TO_FP_FROM_FP
2
1:
Term of Sort RoundingMode
2:
Term of floating-point Sort
2
1:
The exponent size
2:
The significand size
public static final Kind FLOATINGPOINT_TO_FP_FROM_REAL
2
1:
Term of Sort RoundingMode
2:
Term of Sort Real
2
1:
The exponent size
2:
The significand size
public static final Kind FLOATINGPOINT_TO_FP_FROM_SBV
2
1:
Term of Sort RoundingMode
2:
Term of bit-vector Sort
2
1:
The exponent size
2:
The significand size
public static final Kind FLOATINGPOINT_TO_FP_FROM_UBV
2
1:
Term of Sort RoundingMode
2:
Term of bit-vector Sort
2
1:
The exponent size
2:
The significand size
public static final Kind FLOATINGPOINT_TO_UBV
2
1:
Term of Sort RoundingMode
2:
Term of floating-point Sort
1
1:
The size of the bit-vector to convert to.
public static final Kind FLOATINGPOINT_TO_SBV
2
1:
Term of Sort RoundingMode
2:
Term of floating-point Sort
1
1:
The size of the bit-vector to convert to.
public static final Kind FLOATINGPOINT_TO_REAL
1
1:
Term of Sort Real
public static final Kind SELECT
2
1:
Term of array Sort
2:
Term of array index Sort
public static final Kind STORE
3
1:
Term of array Sort
2:
Term of array index Sort
3:
Term of array element Sort
public static final Kind CONST_ARRAY
2
1:
Term of array Sort
2:
Term of array element Sort (value)
public static final Kind EQ_RANGE
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)
public static final Kind APPLY_CONSTRUCTOR
n > 0
1:
DatatypeConstructor Term (see DatatypeConstructor.getTerm()
)
2..n:
Terms of the Sorts of the selectors of the constructor (the arguments to the constructor)
public static final Kind APPLY_SELECTOR
2
1:
DatatypeSelector Term (see DatatypeSelector.getTerm()
)
2:
Term of the codomain Sort of the selector
public static final Kind APPLY_TESTER
2
1:
Datatype tester Term (see DatatypeConstructor.getTesterTerm()
)
2:
Term of Datatype Sort (DatatypeConstructor must belong to this Datatype Sort)
public static final Kind APPLY_UPDATER
3
1:
Datatype updater Term (see DatatypeSelector.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)
public static final Kind MATCH
match
expression.
For example, the SMT-LIBv2 syntax for the following match term
.. code. smtlib
(match l (((cons h t) h) (nil 0)))
is represented by the AST
.. code. lisp
(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. Kind
MATCH_BIND_CASE is used for constructors with selectors
and variable match patterns. If not all constructors are covered, at least
one catch-all variable pattern must be included.
n > 1
1..n:
Terms of kind MATCH_CASE and MATCH_BIND_CASE
public static final Kind MATCH_CASE
2
1:
Term of kind APPLY_CONSTRUCTOR (the pattern to match against)
2:
Term of any Sort (the term the match term evaluates to)
public static final Kind MATCH_BIND_CASE
3
1:
Term of kind VARIABLE_LIST (containing the free variable of the case)
2:
Term of kind VARIABLE (the pattern expression, the free variable of the case)
3:
Term of any Sort (the term the pattern evaluates to)
1:
Term of kind VARIABLE_LIST (containing the free variable of the case)
2:
Term of kind APPLY_CONSTRUCTOR (the pattern expression, applying the set of variables to the constructor)
3:
Term of any Sort (the term the match term evaluates to)
public static final Kind TUPLE_PROJECT
1
1:
Term of tuple Sort
n
1..n:
The tuple indices to project
public static final Kind NULLABLE_LIFT
n > 1
1..n:
Terms of nullable sort
public static final Kind SEP_NIL
public static final Kind SEP_EMP
public static final Kind SEP_PTO
2
1:
Term denoting the location of the points-to constraint
2:
Term denoting the data of the points-to constraint
public static final Kind SEP_STAR
n > 1
1..n:
Terms of sort Bool (the child constraints that hold in
disjoint (separated) heaps)
public static final Kind SEP_WAND
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)
public static final Kind SET_EMPTY
public static final Kind SET_UNION
2
1..2:
Terms of set Sort
public static final Kind SET_INTER
2
1..2:
Terms of set Sort
public static final Kind SET_MINUS
2
1..2:
Terms of set Sort
public static final Kind SET_SUBSET
2
1..2:
Terms of set Sort
public static final Kind SET_MEMBER
2
1:
Term of any Sort (must match the element Sort of the given set Term)
2:
Term of set Sort
public static final Kind SET_SINGLETON
1
1:
Term of any Sort (the set element)
public static final Kind SET_INSERT
n > 0
1..n-1:
Terms of any Sort (must match the element sort of the given set Term)
n:
Term of set Sort
public static final Kind SET_CARD
1
1:
Term of set Sort
public static final Kind SET_COMPLEMENT
1
1:
Term of set Sort
public static final Kind SET_UNIVERSE
Term.isSetValue()
will return false
.public static final Kind SET_COMPREHENSION
3
1:
Term of Kind VARIABLE_LIST
2:
Term of sort Bool (the predicate of the comprehension)
3:
(optional) Term denoting the generator for the comprehension
public static final Kind SET_CHOOSE
1
1:
Term of set Sort
public static final Kind SET_IS_EMPTY
1
1:
Term of set Sort
public static final Kind SET_IS_SINGLETON
1
1:
Term of set Sort
public static final Kind SET_MAP
2
1:
Term of function Sort \((\rightarrow S_1 \; S_2)\)
2:
Term of set Sort (Set \(S_1\))
public static final Kind SET_FILTER
2
1:
Term of function Sort \((\rightarrow T \; Bool)\)
2:
Term of bag Sort (Set \(T\))
public static final Kind SET_ALL
2
1:
Term of function Sort \((\rightarrow T \; Bool)\)
2:
Term of set Sort (Set \(T\))
public static final Kind SET_SOME
2
1:
Term of function Sort \((\rightarrow T \; Bool)\)
2:
Term of set Sort (Set \(T\))
public static final Kind SET_FOLD
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\))
public static final Kind RELATION_JOIN
2
1..2:
Terms of relation Sort
public static final Kind RELATION_TABLE_JOIN
2
1:
Term of relation Sort
2:
Term of relation Sort
n
1..n:
Indices of the projection
public static final Kind RELATION_PRODUCT
2
1..2:
Terms of relation Sort
public static final Kind RELATION_TRANSPOSE
1
1:
Term of relation Sort
public static final Kind RELATION_TCLOSURE
1
1:
Term of relation Sort
public static final Kind RELATION_JOIN_IMAGE
2
1..2:
Terms of relation Sort
public static final Kind RELATION_IDEN
1
1:
Term of relation Sort
public static final Kind RELATION_GROUP
1
1:
Term of relation sort
n
1..n:
Indices of the projection
public static final Kind RELATION_AGGREGATE
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\)
n
1..n:
Indices of the projection
public static final Kind RELATION_PROJECT
1
1:
Term of relation Sort
n
1..n:
Indices of the projection
public static final Kind BAG_EMPTY
public static final Kind BAG_UNION_MAX
2
1..2:
Terms of bag Sort
public static final Kind BAG_UNION_DISJOINT
2
1..2:
Terms of bag Sort
public static final Kind BAG_INTER_MIN
2
1..2:
Terms of bag Sort
public static final Kind BAG_DIFFERENCE_SUBTRACT
2
1..2:
Terms of bag Sort
public static final Kind BAG_DIFFERENCE_REMOVE
2
1..2:
Terms of bag Sort
public static final Kind BAG_SUBBAG
2
1..2:
Terms of bag Sort
public static final Kind BAG_COUNT
public static final Kind BAG_MEMBER
2
1:
Term of any Sort (must match the element Sort of the given bag Term)
2:
Terms of bag Sort
public static final Kind BAG_SETOF
1
1:
Term of bag Sort
public static final Kind BAG_MAKE
2
1:
Term of any Sort (the bag element)
2:
Term of Sort Int (the multiplicity of the element)
public static final Kind BAG_CARD
1
1:
Term of bag Sort
public static final Kind BAG_CHOOSE
1
1:
Term of bag Sort
public static final Kind BAG_MAP
2
1:
Term of function Sort \((\rightarrow S_1 \; S_2)\)
2:
Term of bag Sort (Bag \(S_1\))
public static final Kind BAG_FILTER
2
1:
Term of function Sort \((\rightarrow T \; Bool)\)
2:
Term of bag Sort (Bag \(T\))
public static final Kind BAG_ALL
2
1:
Term of function Sort \((\rightarrow T \; Bool)\)
2:
Term of bag Sort (Bag \(T\))
public static final Kind BAG_SOME
2
1:
Term of function Sort \((\rightarrow T \; Bool)\)
2:
Term of bag Sort (Bag \(T\))
public static final Kind BAG_FOLD
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\))
public static final Kind BAG_PARTITION
2
1:
Term of function Sort \((\rightarrow \; E \; E \; Bool)\)
2:
Term of bag Sort (Bag \(E\))
public static final Kind TABLE_PRODUCT
2
1..2:
Terms of table Sort
public static final Kind TABLE_PROJECT
1
1:
Term of table Sort
n
1..n:
Indices of the projection
public static final Kind TABLE_AGGREGATE
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\)
n
1..n:
Indices of the projection
public static final Kind TABLE_JOIN
2
1:
Term of table Sort
2:
Term of table Sort
n
1..n:
Indices of the projection
public static final Kind TABLE_GROUP
1
1:
Term of table sort
n
1..n:
Indices of the projection
public static final Kind STRING_CONCAT
n > 1
1..n:
Terms of Sort String
public static final Kind STRING_IN_REGEXP
2
1:
Term of Sort String
2:
Term of Sort RegLan
public static final Kind STRING_LENGTH
1
1:
Term of Sort String
public static final Kind STRING_SUBSTR
3
1:
Term of Sort String
2:
Term of Sort Int (index \(i\))
3:
Term of Sort Int (length \(l\))
public static final Kind STRING_UPDATE
3
1:
Term of Sort String
2:
Term of Sort Int (index \(i\))
3:
Term of Sort Strong (replacement string \(t\))
public static final Kind STRING_CHARAT
2
1:
Term of Sort String (string \(s\))
2:
Term of Sort Int (index \(i\))
public static final Kind STRING_CONTAINS
true
.
2
1:
Term of Sort String (the string \(s_1\))
2:
Term of Sort String (the string \(s_2\))
public static final Kind STRING_INDEXOF
2
1:
Term of Sort String (substring \(s_1\))
2:
Term of Sort String (substring \(s_2\))
3:
Term of Sort Int (index \(i\))
public static final Kind STRING_INDEXOF_RE
3
1:
Term of Sort String (string \(s\))
2:
Term of Sort RegLan (regular expression \(r\))
3:
Term of Sort Int (index \(i\))
public static final Kind STRING_REPLACE
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\))
public static final Kind STRING_REPLACE_ALL
3
1:
Term of Sort String (\(s_1\))
2:
Term of Sort String (\(s_2\))
3:
Term of Sort String (\(s_3\))
public static final Kind STRING_REPLACE_RE
3
1:
Term of Sort String (\(s_1\))
2:
Term of Sort RegLan
3:
Term of Sort String (\(s_2\))
public static final Kind STRING_REPLACE_RE_ALL
3
1:
Term of Sort String (\(s_1\))
2:
Term of Sort RegLan
3:
Term of Sort String (\(s_2\))
public static final Kind STRING_TO_LOWER
1
1:
Term of Sort String
public static final Kind STRING_TO_UPPER
1
1:
Term of Sort String
public static final Kind STRING_REV
1
1:
Term of Sort String
public static final Kind STRING_TO_CODE
1
1:
Term of Sort String
public static final Kind STRING_FROM_CODE
1
1:
Term of Sort Int
public static final Kind STRING_LT
2
1:
Term of Sort String (\(s_1\))
2:
Term of Sort String (\(s_2\))
public static final Kind STRING_LEQ
2
1:
Term of Sort String (\(s_1\))
2:
Term of Sort String (\(s_2\))
public static final Kind STRING_PREFIX
true
.
2
1:
Term of Sort String (\(s_1\))
2:
Term of Sort String (\(s_2\))
public static final Kind STRING_SUFFIX
true
.
2
1:
Term of Sort String (\(s_1\))
2:
Term of Sort String (\(s_2\))
public static final Kind STRING_IS_DIGIT
"0"
, ...,
"9"
).
1
1:
Term of Sort String
public static final Kind STRING_FROM_INT
1
1:
Term of Sort Int
public static final Kind STRING_TO_INT
1
1:
Term of Sort Int
public static final Kind CONST_STRING
public static final Kind STRING_TO_REGEXP
1
1:
Term of Sort String
public static final Kind REGEXP_CONCAT
2
1..2:
Terms of Sort RegLan
public static final Kind REGEXP_UNION
2
1..2:
Terms of Sort RegLan
public static final Kind REGEXP_INTER
2
1..2:
Terms of Sort RegLan
public static final Kind REGEXP_DIFF
2
1..2:
Terms of Sort RegLan
public static final Kind REGEXP_STAR
1
1:
Term of Sort RegLan
public static final Kind REGEXP_PLUS
1
1:
Term of Sort RegLan
public static final Kind REGEXP_OPT
1
1:
Term of Sort RegLan
public static final Kind REGEXP_RANGE
2
1:
Term of Sort String (lower bound character for the range)
2:
Term of Sort String (upper bound character for the range)
public static final Kind REGEXP_REPEAT
1
1:
Term of Sort RegLan
1
1:
The number of repetitions
public static final Kind REGEXP_LOOP
1
1:
Term of Sort RegLan
1
1:
The lower bound
2:
The upper bound
public static final Kind REGEXP_NONE
public static final Kind REGEXP_ALL
public static final Kind REGEXP_ALLCHAR
public static final Kind REGEXP_COMPLEMENT
1
1:
Term of Sort RegLan
public static final Kind SEQ_CONCAT
n > 1
1..n:
Terms of sequence Sort
public static final Kind SEQ_LENGTH
1
1:
Term of sequence Sort
public static final Kind SEQ_EXTRACT
3
1:
Term of sequence Sort
2:
Term of Sort Int (index \(i\))
3:
Term of Sort Int (length \(l\))
public static final Kind SEQ_UPDATE
3
1:
Term of sequence Sort
2:
Term of Sort Int (index \(i\))
3:
Term of sequence Sort (replacement sequence \(t\))
public static final Kind SEQ_AT
1
.
2
1:
Term of sequence Sort
2:
Term of Sort Int (index \(i\))
public static final Kind SEQ_CONTAINS
true
.
2
1:
Term of sequence Sort (\(s_1\))
2:
Term of sequence Sort (\(s_2\))
public static final Kind SEQ_INDEXOF
3
1:
Term of sequence Sort (\(s_1\))
2:
Term of sequence Sort (\(s_2\))
3:
Term of Sort Int (\(i\))
public static final Kind SEQ_REPLACE
3
1:
Term of sequence Sort (\(s_1\))
2:
Term of sequence Sort (\(s_2\))
3:
Term of sequence Sort (\(s_3\))
public static final Kind SEQ_REPLACE_ALL
3
1:
Term of sequence Sort (\(s_1\))
2:
Term of sequence Sort (\(s_2\))
3:
Term of sequence Sort (\(s_3\))
public static final Kind SEQ_REV
1
1:
Term of sequence Sort
public static final Kind SEQ_PREFIX
true
.
1
1:
Term of sequence Sort (\(s_1\))
2:
Term of sequence Sort (\(s_2\))
public static final Kind SEQ_SUFFIX
true
.
1
1:
Term of sequence Sort (\(s_1\))
2:
Term of sequence Sort (\(s_2\))
public static final Kind CONST_SEQUENCE
Term.getSequenceValue()
.
public static final Kind SEQ_UNIT
1
1:
Term of any Sort (the element term)
public static final Kind SEQ_NTH
2
1:
Term of sequence Sort
2:
Term of Sort Int (\(n\))
public static final Kind FORALL
3
1:
Term of Kind VARIABLE_LIST
2:
Term of Sort Bool (the quantifier body)
3:
(optional) Term of Kind INST_PATTERN
public static final Kind EXISTS
3
1:
Term of Kind VARIABLE_LIST
2:
Term of Sort Bool (the quantifier body)
3:
(optional) Term of Kind INST_PATTERN
public static final Kind VARIABLE_LIST
n > 0
1..n:
Terms of Kind VARIABLE
public static final Kind INST_PATTERN
n > 0
1..n:
Terms of any Sort
public static final Kind INST_NO_PATTERN
n > 0
1..n:
Terms of any Sort
public static final Kind INST_POOL
n > 0
1..n:
Terms that comprise the pools, which are one-to-one with the variables of the quantified formula to be instantiated
public static final Kind INST_ADD_TO_POOL
(ADD t 1)
is
added to pool \(p\).
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.
public static final Kind SKOLEM_ADD_TO_POOL
(ADD k 1)
is added to the pool \(p\).
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.
public static final Kind INST_ATTRIBUTE
n > 0
1:
Term of Kind CONST_STRING (the keyword of the attribute)
2...n:
Terms representing the values of the attribute
public static final Kind INST_PATTERN_LIST
n > 1
1..n:
Terms of Kind INST_PATTERN, INST_NO_PATTERN, INST_POOL, INST_ADD_TO_POOL, SKOLEM_ADD_TO_POOL, INST_ATTRIBUTE
public static final Kind LAST_KIND
public static Kind[] values()
for (Kind c : Kind.values()) System.out.println(c);
public static Kind valueOf(java.lang.String name)
name
- the name of the enum constant to be returned.java.lang.IllegalArgumentException
- if this enum type has no constant with the specified namejava.lang.NullPointerException
- if the argument is nullpublic static Kind fromInt(int value) throws CVC5ApiException
CVC5ApiException
public int getValue()