Package io.github.cvc5
Enum Class Kind
- All Implemented Interfaces:
Serializable,Comparable<Kind>,Constable
Enum representing the set of possible values for Kind.
-
Nested Class Summary
Nested classes/interfaces inherited from class java.lang.Enum
Enum.EnumDesc<E extends Enum<E>> -
Enum Constant Summary
Enum ConstantsEnum ConstantDescriptionAbsolute value.Arithmetic addition.Logical conjunction.Datatype constructor application.Datatype selector application.Datatype tester application.Application of an uninterpreted function.Datatype update application.Arc cosecant function.Arc cosine function.Arc cotangent function.Arc secant function.Arc sine function.Arc tangent function.Bag all.Bag cardinality.Bag choose.Bag element multiplicity.Bag difference remove.Bag difference subtract.Empty bag.Bag filter.Bag fold.Bag intersection (min).Bag make.Bag map.Bag membership predicate.Bag partition.Bag setof.Bag some.Bag inclusion predicate.Bag disjoint union (sum).Bag max union.Addition of two or more bit-vectors.Bit-wise and.Bit-vector arithmetic shift right.Retrieves the bit at the given index from a bit-vector as a Bool term.Equality comparison (returns bit-vector of size1).Concatenation of two or more bit-vectors.Bit-vector extract.Converts a list of Bool terms to a bit-vector.Bit-vector if-then-else.Bit-vector logical shift right.Multiplication of two or more bit-vectors.Bit-wise nand.Negation of a bit-vector (two's complement).Bit-vector negation overflow detection.Bit-wise nor.Bit-wise negation.Bit-wise or.Bit-vector redand.Bit-vector redor.Bit-vector repeat.Bit-vector rotate left.Bit-vector rotate right.Bit-vector signed addition overflow detection.Bit-vector conversion, signed bit-vector to integer.Signed bit-vector division.Bit-vector signed division overflow detection.Bit-vector signed greater than or equal.Bit-vector signed greater than.Bit-vector shift left.Bit-vector sign extension.Bit-vector signed less than or equal.Bit-vector signed less than.Bit-vector signed less than returning a bit-vector of size1.Signed bit-vector remainder (sign follows divisor).Bit-vector signed multiplication overflow detection.Signed bit-vector remainder (sign follows dividend).Bit-vector signed subtraction overflow detection.Subtraction of two bit-vectors.Bit-vector conversion to (non-negative) integer.Bit-vector unsigned addition overflow detection.Bit-vector conversion, unsigned bit-vector to integer.Unsigned bit-vector division.Bit-vector unsigned greater than or equal.Bit-vector unsigned greater than.Bit-vector unsigned less than or equal.Bit-vector unsigned less than.Bit-vector unsigned less than returning a bit-vector of size 1.Bit-vector unsigned multiplication overflow detection.Unsigned bit-vector remainder.Bit-vector unsigned subtraction overflow detection.Bit-wise xnor, left associative.Bit-wise xor.Bit-vector zero extension.Cardinality constraint on uninterpreted sort.Constant array.Fixed-size bit-vector constant.Boolean constant.Finite field constant.Floating-point constant, created from IEEE-754 bit-vector representation of the floating-point value.Arbitrary-precision integer constant.Arbitrary-precision rational constant.RoundingMode constant.Constant sequence.Constant string.Free constant symbol.Cosecant function.Cosine function.Cotangent function.Disequality.Operator for the divisibility-by-\(k\) predicate.Real division, division by 0 undefined, left associative.Real division, division by 0 defined to be 0, left associative.Equality over arrays \(a\) and \(b\) over a given range \([i,j]\), i.e., \[ \forall k .Equality, chainable.Existentially quantified formula.Exponential function.Addition of two or more finite field elements.Bitsum of two or more finite field elements: x + 2y + 4z + ...Multiplication of two or more finite field elements.Negation of a finite field element (additive inverse).Floating-point absolute value.Floating-point addition.Floating-point division.Floating-point equality.Floating-point fused multiply and add.Create floating-point literal from bit-vector triple.Floating-point greater than or equal.Floating-point greater than.Floating-point is infinite tester.Floating-point is NaN tester.Floating-point is negative tester.Floating-point is normal tester.Floating-point is positive tester.Floating-point is sub-normal tester.Floating-point is zero tester.Floating-point less than or equal.Floating-point less than.Floating-point maximum.Floating-point minimum.Floating-point multiply.Floating-point negation.Floating-point remainder.Floating-point round to integral.Floating-point square root.Floating-point sutraction.Conversion to floating-point from floating-point.Conversion to floating-point from IEEE-754 bit-vector.Conversion to floating-point from Real.Conversion to floating-point from signed bit-vector.Conversion to floating-point from unsigned bit-vector.Conversion to Real from floating-point.Conversion to signed bit-vector from floating-point.Conversion to unsigned bit-vector from floating-point.Universally quantified formula.Greater than or equal, chainable.Greater than, chainable.Higher-order applicative encoding of function application, left associative.Integer and.Logical implication.A instantantiation-add-to-pool annotation.Instantiation attribute.Instantiation no-pattern.Instantiation pattern.A list of instantiation patterns, attributes or annotations.Instantiation pool annotation.Conversion from Int to bit-vector.Internal kind.Integer division, division by 0 undefined, left associative.Integer division, division by 0 defined to be 0, left associative.Integer modulus, modulus by 0 undefined.Integer modulus, t modulus by 0 defined to be t.Is-integer predicate.If-then-else.Lambda expression.Marks the upper-bound of this enumeration.Less than or equal, chainable.Less than, chainable.Match expression.Match case with binders, for constructors with selectors and variable patterns.Match case for nullary constructors.Arithmetic multiplication.Arithmetic negation.Logical negation.Null kind.Lifting operator for nullable terms.Logical disjunction.Pi constant.Arithmetic power.Power of two.Regular expression all.Regular expression all characters.Regular expression complement.Regular expression concatenation.Regular expression difference.Regular expression intersection.Regular expression loop.Regular expression none.Regular expression ?.Regular expression +.Regular expression range.Operator for regular expression repeat.Regular expression \*.Regular expression union.Relation aggregate operator has the form \(((\_ \; rel.aggr \; n_1 ...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 identity.Relation join.Relation join image.Relation cartesian product.Relation projection operator extends tuple projection operator to sets.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 transitive closure.Relation transpose.Secant function.Array select.Separation logic empty heap.Separation logic nil.Separation logic points-to relation.Separation logic star.Separation logic magic wand.Sequence element at.Sequence concat.Sequence contains.Sequence extract.Sequence index-of.Sequence length.Sequence nth.Sequence prefix-of.Sequence replace.Sequence replace all.Sequence reverse.Sequence suffix-of.Sequence unit.Sequence update.Set all.Set cardinality.Set choose.Set complement with respect to finite universe.Set comprehension A set comprehension is specified by a variable list \(x_1 ...Empty set.Set filter.Set fold.The set obtained by inserting elements; Arity:n > 01..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:TermManager.mkTerm(Kind, Term[])TermManager.mkTerm(Op, Term[])Create Op of this kind with:TermManager.mkOp(Kind, int[])Set intersection.Set is empty tester.Set is singleton tester.Set map.Set membership predicate.Set subtraction.Singleton set.Set some.Subset predicate.Set union.Finite universe set.Symbolic expression.Sine function.A Skolem.A skolemization-add-to-pool annotation.Square root.Array store.String character at.String concat.String contains.String from code.Conversion from Int to String.String membership.String index-of.String index-of regular expression match.String is-digit.String length.String less than or equal.String less than.String prefix-of.String replace.String replace all.String replace regular expression match.String replace all regular expression matches.String reverse.String substring.String suffix-of.String to code.String to integer (total function).String to lower case.Conversion from string to regexp.String to upper case.String update.Arithmetic subtraction, left associative.Table aggregate operator has the form \(((\_ \; table.aggr \; n_1 ...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 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 cross product.Table projection operator extends tuple projection operator to tables.Tangent function.Convert Term of sort Int or Real to Int via the floor function.Convert Term of Sort Int or Real to Real.Tuple projection.Undefined kind.The value of an uninterpreted constant.(Bound) variable.Variable list.Witness.Logical exclusive disjunction, left associative. -
Method Summary
Modifier and TypeMethodDescriptionstatic KindfromInt(int value) Converts an integer value to the corresponding enum constant.intgetValue()Get the integer value associated with this enum constant.static KindReturns the enum constant of this class with the specified name.static Kind[]values()Returns an array containing the constants of this enum class, in the order they are declared.
-
Enum Constant Details
-
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.
-
UNDEFINED_KIND
Undefined kind.- Note:
- Should never be exposed or created via the API.
-
NULL_TERM
Null kind. The kind of a null term (Term()).- Note:
- May not be explicitly created via API functions other than
Term().
-
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.
-
EQUAL
Equality, chainable.- Arity:
n > 11..n:Terms of the same Sort
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
DISTINCT
Disequality.- Arity:
n > 11..n:Terms of the same Sort
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
CONSTANT
Free constant symbol.- Create Term of this Kind with:
- Note:
- Not permitted in bindings (e.g., FORALL, EXISTS).
-
VARIABLE
(Bound) variable.- Create Term of this Kind with:
- Note:
- Only permitted in bindings and in lambda and quantifier bodies.
-
SKOLEM
A Skolem.- Note:
- Represents an internally generated term. Information on the skolem is available via the calls Term.getSkolemId and Term.getSkolemIndices.
-
SEXPR
Symbolic expression.- Arity:
n > 01..n:Terms with same sorts
- Create Term of this Kind with:
- Create Op of this kind with:
- Note:
- This kind is experimental and may be changed or removed in future versions.
- Arity:
-
LAMBDA
Lambda expression.- Arity:
21:Term of kind VARIABLE_LIST2:Term of any Sort (the body of the lambda)
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
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 .. code. smtlib (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: .. code. smtlib (distinct (witness ((x Int)) F) (witness ((x Int)) F))- Arity:
31:Term of kind VARIABLE_LIST2:Term of Sort Bool (the body of the witness)3:(optional) Term of kind INST_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 non-linear 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\).
- Arity:
-
CONST_BOOLEAN
Boolean constant.- Create Term of this Kind with:
-
NOT
Logical negation.- Arity:
11:Term of Sort Bool
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
AND
Logical conjunction.- Arity:
n > 11..n:Terms of Sort Bool
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
IMPLIES
Logical implication.- Arity:
n > 11..n:Terms of Sort Bool
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
OR
Logical disjunction.- Arity:
n > 11..n:Terms of Sort Bool
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
XOR
Logical exclusive disjunction, left associative.- Arity:
n > 11..n:Terms of Sort Bool
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
ITE
If-then-else.- Arity:
31:Term of Sort Bool2:The 'then' term, Term of any Sort3:The 'else' term, Term of the same sort as second argument
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
APPLY_UF
Application of an uninterpreted function.- Arity:
n > 11:Function Term2..n:Function argument instantiation Terms of any first-class Sort
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
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:
-
HO_APPLY
Higher-order applicative encoding of function application, left associative.- Arity:
n = 21:Function Term2:Argument Term of the domain Sort of the function
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
ADD
Arithmetic addition.- Arity:
n > 11..n:Terms of Sort Int or Real (sorts must match)
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
MULT
Arithmetic multiplication.- Arity:
n > 11..n:Terms of Sort Int or Real (sorts must match)
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
IAND
Integer and. Operator for bit-wiseANDover integers, parameterized by a (positive) bit-width \(k\). .. code. smtlib ((_ iand k) i_1 i_2) is equivalent to .. code. smtlib (ubv_to_int (bvand ((_ int_to_bv k) i_1) ((_ int_to_bv k) i_2))) for all integersi_1,i_2.- Arity:
21..2:Terms of Sort Int
- Indices:
11:Bit-width \(k\)
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
POW2
Power of two. Operator for raising2to a non-negative integer power.- Arity:
11:Term of Sort Int
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
SUB
Arithmetic subtraction, left associative.- Arity:
n > 11..n:Terms of Sort Int or Real (sorts must match)
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
NEG
Arithmetic negation.- Arity:
11:Term of Sort Int or Real
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
DIVISION
Real division, division by 0 undefined, left associative.- Arity:
n > 11..n:Terms of Sort Real
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
DIVISION_TOTAL
Real division, division by 0 defined to be 0, left associative.- Arity:
n > 11..n:Terms of Sort Real
- Create Term of this Kind with:
- Create Op of this kind with:
- Note:
- This kind is experimental and may be changed or removed in future versions.
- Arity:
-
INTS_DIVISION
Integer division, division by 0 undefined, left associative.- Arity:
n > 11..n:Terms of Sort Int
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
INTS_DIVISION_TOTAL
Integer division, division by 0 defined to be 0, left associative.- Arity:
n > 11..n:Terms of Sort Int
- Create Term of this Kind with:
- Create Op of this kind with:
- Note:
- This kind is experimental and may be changed or removed in future versions.
- Arity:
-
INTS_MODULUS
Integer modulus, modulus by 0 undefined.- Arity:
21:Term of Sort Int2:Term of Sort Int
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
INTS_MODULUS_TOTAL
Integer modulus, t modulus by 0 defined to be t.- Arity:
21:Term of Sort Int2:Term of Sort Int
- Create Term of this Kind with:
- Create Op of this kind with:
- Note:
- This kind is experimental and may be changed or removed in future versions.
- Arity:
-
ABS
Absolute value.- Arity:
11:Term of Sort Int or Real
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
POW
Arithmetic power.- Arity:
21..2:Term of Sort Int or Real (sorts must match)
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
EXPONENTIAL
Exponential function.- Arity:
11:Term of Sort Real
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
SINE
Sine function.- Arity:
11:Term of Sort Real
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
COSINE
Cosine function.- Arity:
11:Term of Sort Real
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
TANGENT
Tangent function.- Arity:
11:Term of Sort Real
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
COSECANT
Cosecant function.- Arity:
11:Term of Sort Real
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
SECANT
Secant function.- Arity:
11:Term of Sort Real
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
COTANGENT
Cotangent function.- Arity:
11:Term of Sort Real
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
ARCSINE
Arc sine function.- Arity:
11:Term of Sort Real
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
ARCCOSINE
Arc cosine function.- Arity:
11:Term of Sort Real
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
ARCTANGENT
Arc tangent function.- Arity:
11:Term of Sort Real
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
ARCCOSECANT
Arc cosecant function.- Arity:
11:Term of Sort Real
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
ARCSECANT
Arc secant function.- Arity:
11:Term of Sort Real
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
ARCCOTANGENT
Arc cotangent function.- Arity:
11:Term of Sort Real
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
SQRT
Square root. If the argument `x` is non-negative, then this returns a non-negative value `y` such that `y * y = x`.- Arity:
11:Term of Sort Real
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
DIVISIBLE
Operator for the divisibility-by-\(k\) predicate.- Arity:
11:Term of Sort Int
- Indices:
11:The integer \(k\) to divide by.
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
CONST_RATIONAL
Arbitrary-precision rational constant.- Create Term of this Kind with:
-
CONST_INTEGER
Arbitrary-precision integer constant.- Create Term of this Kind with:
-
LT
Less than, chainable.- Arity:
n > 11..n:Terms of Sort Int or Real (sorts must match)
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
LEQ
Less than or equal, chainable.- Arity:
n > 11..n:Terms of Sort Int or Real (sorts must match)
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
GT
Greater than, chainable.- Arity:
n > 11..n:Terms of Sort Int or Real (sorts must match)
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
GEQ
Greater than or equal, chainable.- Arity:
n > 11..n:Terms of Sort Int or Real (sorts must match)
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
IS_INTEGER
Is-integer predicate.- Arity:
11:Term of Sort Int or Real
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
TO_INTEGER
Convert Term of sort Int or Real to Int via the floor function.- Arity:
11:Term of Sort Int or Real
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
TO_REAL
Convert Term of Sort Int or Real to Real.- Arity:
11:Term of Sort Int or Real
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
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.
-
CONST_BITVECTOR
Fixed-size bit-vector constant.- Create Term of this Kind with:
-
BITVECTOR_CONCAT
Concatenation of two or more bit-vectors.- Arity:
n > 11..n:Terms of bit-vector Sort (sorts must match)
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
BITVECTOR_AND
Bit-wise and.- Arity:
n > 11..n:Terms of bit-vector Sort (sorts must match)
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
BITVECTOR_OR
Bit-wise or.- Arity:
n > 11..n:Terms of bit-vector Sort (sorts must match)
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
BITVECTOR_XOR
Bit-wise xor.- Arity:
n > 11..n:Terms of bit-vector Sort (sorts must match)
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
BITVECTOR_NOT
Bit-wise negation.- Arity:
11:Term of bit-vector Sort
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
BITVECTOR_NAND
Bit-wise nand.- Arity:
21..2:Terms of bit-vector Sort (sorts must match)
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
BITVECTOR_NOR
Bit-wise nor.- Arity:
21..2:Terms of bit-vector Sort (sorts must match)
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
BITVECTOR_XNOR
Bit-wise xnor, left associative.- Arity:
21..2:Terms of bit-vector Sort (sorts must match)
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
BITVECTOR_COMP
Equality comparison (returns bit-vector of size1).- Arity:
21..2:Terms of bit-vector Sort (sorts must match)
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
BITVECTOR_MULT
Multiplication of two or more bit-vectors.- Arity:
n > 11..n:Terms of bit-vector Sort (sorts must match)
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
BITVECTOR_ADD
Addition of two or more bit-vectors.- Arity:
n > 11..n:Terms of bit-vector Sort (sorts must match)
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
BITVECTOR_SUB
Subtraction of two bit-vectors.- Arity:
n > 11..n:Terms of bit-vector Sort (sorts must match)
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
BITVECTOR_NEG
Negation of a bit-vector (two's complement).- Arity:
11:Term of bit-vector Sort
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
BITVECTOR_UDIV
Unsigned bit-vector division. Truncates towards0. If the divisor is zero, the result is all ones.- Arity:
21..2:Terms of bit-vector Sort (sorts must match)
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
BITVECTOR_UREM
Unsigned bit-vector remainder. Remainder from unsigned bit-vector division. If the modulus is zero, the result is the dividend.- Arity:
21..2:Terms of bit-vector Sort (sorts must match)
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
BITVECTOR_SDIV
Signed bit-vector division. Two's complement signed division of two bit-vectors. 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:
21..2:Terms of bit-vector Sort (sorts must match)
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
BITVECTOR_SREM
Signed bit-vector remainder (sign follows dividend). Two's complement signed remainder of two bit-vectors where the sign follows the dividend. If the modulus is zero, the result is the dividend.- Arity:
21..2:Terms of bit-vector Sort (sorts must match)
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
BITVECTOR_SMOD
Signed bit-vector 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:
21..2:Terms of bit-vector Sort (sorts must match)
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
BITVECTOR_SHL
Bit-vector shift left.- Arity:
21..2:Terms of bit-vector Sort (sorts must match)
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
BITVECTOR_LSHR
Bit-vector logical shift right.- Arity:
21..2:Terms of bit-vector Sort (sorts must match)
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
BITVECTOR_ASHR
Bit-vector arithmetic shift right.- Arity:
21..2:Terms of bit-vector Sort (sorts must match)
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
BITVECTOR_ULT
Bit-vector unsigned less than.- Arity:
21..2:Terms of bit-vector Sort (sorts must match)
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
BITVECTOR_ULE
Bit-vector unsigned less than or equal.- Arity:
21..2:Terms of bit-vector Sort (sorts must match)
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
BITVECTOR_UGT
Bit-vector unsigned greater than.- Arity:
21..2:Terms of bit-vector Sort (sorts must match)
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
BITVECTOR_UGE
Bit-vector unsigned greater than or equal.- Arity:
21..2:Terms of bit-vector Sort (sorts must match)
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
BITVECTOR_SLT
Bit-vector signed less than.- Arity:
21..2:Terms of bit-vector Sort (sorts must match)
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
BITVECTOR_SLE
Bit-vector signed less than or equal.- Arity:
21..2:Terms of bit-vector Sort (sorts must match)
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
BITVECTOR_SGT
Bit-vector signed greater than.- Arity:
21..2:Terms of bit-vector Sort (sorts must match)
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
BITVECTOR_SGE
Bit-vector signed greater than or equal.- Arity:
21..2:Terms of bit-vector Sort (sorts must match)
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
BITVECTOR_ULTBV
Bit-vector unsigned less than returning a bit-vector of size 1.- Arity:
21..2:Terms of bit-vector Sort (sorts must match)
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
BITVECTOR_SLTBV
Bit-vector signed less than returning a bit-vector of size1.- Arity:
21..2:Terms of bit-vector Sort (sorts must match)
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
BITVECTOR_ITE
Bit-vector if-then-else. Same semantics as regular ITE, but condition is bit-vector of size1.- Arity:
31:Term of bit-vector Sort of size `1`1..3:Terms of bit-vector sort (sorts must match)
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
BITVECTOR_REDOR
Bit-vector redor.- Arity:
11:Term of bit-vector Sort
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
BITVECTOR_REDAND
Bit-vector redand.- Arity:
11:Term of bit-vector Sort
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
BITVECTOR_NEGO
Bit-vector negation overflow detection.- Arity:
11:Term of bit-vector Sort
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
BITVECTOR_UADDO
Bit-vector unsigned addition overflow detection.- Arity:
21..2:Terms of bit-vector Sort (sorts must match)
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
BITVECTOR_SADDO
Bit-vector signed addition overflow detection.- Arity:
21..2:Terms of bit-vector Sort (sorts must match)
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
BITVECTOR_UMULO
Bit-vector unsigned multiplication overflow detection.- Arity:
21..2:Terms of bit-vector Sort (sorts must match)
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
BITVECTOR_SMULO
Bit-vector signed multiplication overflow detection.- Arity:
21..2:Terms of bit-vector Sort (sorts must match)
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
BITVECTOR_USUBO
Bit-vector unsigned subtraction overflow detection.- Arity:
21..2:Terms of bit-vector Sort (sorts must match)
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
BITVECTOR_SSUBO
Bit-vector signed subtraction overflow detection.- Arity:
21..2:Terms of bit-vector Sort (sorts must match)
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
BITVECTOR_SDIVO
Bit-vector signed division overflow detection.- Arity:
21..2:Terms of bit-vector Sort (sorts must match)
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
BITVECTOR_EXTRACT
Bit-vector extract.- Arity:
11:Term of bit-vector Sort
- Indices:
21:The upper bit index.2:The lower bit index.
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
BITVECTOR_REPEAT
Bit-vector repeat.- Arity:
11:Term of bit-vector Sort
- Indices:
11:The number of times to repeat the given term.
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
BITVECTOR_ZERO_EXTEND
Bit-vector zero extension.- Arity:
11:Term of bit-vector Sort
- Indices:
11:The number of zeroes to extend the given term with.
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
BITVECTOR_SIGN_EXTEND
Bit-vector sign extension.- Arity:
11:Term of bit-vector Sort
- Indices:
11: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:
- Arity:
-
BITVECTOR_ROTATE_LEFT
Bit-vector rotate left.- Arity:
11:Term of bit-vector Sort
- Indices:
11:The number of bits to rotate the given term left.
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
BITVECTOR_ROTATE_RIGHT
Bit-vector rotate right.- Arity:
11:Term of bit-vector Sort
- Indices:
11:The number of bits to rotate the given term right.
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
INT_TO_BITVECTOR
Conversion from Int to bit-vector.- Arity:
11:Term of Sort Int
- Indices:
11:The size of the bit-vector to convert to.
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
BITVECTOR_TO_NAT
Bit-vector conversion to (non-negative) integer.- Arity:
11:Term of bit-vector Sort
- Create Term of this Kind with:
- Create Op of this kind with:
- Note:
- This kind is deprecated and replaced by `BITVECTOR_UBV_TO_INT`. It will be removed in a future release.
- Arity:
-
BITVECTOR_UBV_TO_INT
Bit-vector conversion, unsigned bit-vector to integer.- Arity:
11:Term of bit-vector Sort
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
BITVECTOR_SBV_TO_INT
Bit-vector conversion, signed bit-vector to integer.- Arity:
11:Term of bit-vector Sort
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
BITVECTOR_FROM_BOOLS
Converts a list of Bool terms to a bit-vector.- Arity:
n > 01..n:Terms of Sort Bool
- 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.
- Arity:
-
BITVECTOR_BIT
Retrieves the bit at the given index from a bit-vector as a Bool term.- Arity:
11:Term of bit-vector Sort
- Indices:
11:The bit index
- 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.
- Arity:
-
CONST_FINITE_FIELD
Finite field constant.- Create Term of this Kind with:
-
FINITE_FIELD_NEG
Negation of a finite field element (additive inverse).- Arity:
11:Term of finite field Sort
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
FINITE_FIELD_ADD
Addition of two or more finite field elements.- Arity:
n > 11..n:Terms of finite field Sort (sorts must match)
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
FINITE_FIELD_BITSUM
Bitsum of two or more finite field elements: x + 2y + 4z + ...- Arity:
n > 11..n:Terms of finite field Sort (sorts must match)
- Create Term of this Kind with:
- Arity:
-
FINITE_FIELD_MULT
Multiplication of two or more finite field elements.- Arity:
n > 11..n:Terms of finite field Sort (sorts must match)
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
CONST_FLOATINGPOINT
Floating-point constant, created from IEEE-754 bit-vector representation of the floating-point value.- Create Term of this Kind with:
-
CONST_ROUNDINGMODE
RoundingMode constant.- Create Term of this Kind with:
-
FLOATINGPOINT_FP
Create floating-point literal from bit-vector triple.- Arity:
31: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)
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
FLOATINGPOINT_EQ
Floating-point equality.- Arity:
21..2:Terms of floating-point Sort (sorts must match)
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
FLOATINGPOINT_ABS
Floating-point absolute value.- Arity:
11:Term of floating-point Sort
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
FLOATINGPOINT_NEG
Floating-point negation.- Arity:
11:Term of floating-point Sort
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
FLOATINGPOINT_ADD
Floating-point addition.- Arity:
31:Term of Sort RoundingMode2..3:Terms of floating-point Sort (sorts must match)
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
FLOATINGPOINT_SUB
Floating-point sutraction.- Arity:
31:Term of Sort RoundingMode2..3:Terms of floating-point Sort (sorts must match)
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
FLOATINGPOINT_MULT
Floating-point multiply.- Arity:
31:Term of Sort RoundingMode2..3:Terms of floating-point Sort (sorts must match)
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
FLOATINGPOINT_DIV
Floating-point division.- Arity:
31:Term of Sort RoundingMode2..3:Terms of floating-point Sort (sorts must match)
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
FLOATINGPOINT_FMA
Floating-point fused multiply and add.- Arity:
41:Term of Sort RoundingMode2..4:Terms of floating-point Sort (sorts must match)
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
FLOATINGPOINT_SQRT
Floating-point square root.- Arity:
21:Term of Sort RoundingMode2:Term of floating-point Sort
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
FLOATINGPOINT_REM
Floating-point remainder.- Arity:
21..2:Terms of floating-point Sort (sorts must match)
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
FLOATINGPOINT_RTI
Floating-point round to integral.- Arity:
21..2:Terms of floating-point Sort (sorts must match)
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
FLOATINGPOINT_MIN
Floating-point minimum.- Arity:
21:Term of Sort RoundingMode2:Term of floating-point Sort
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
FLOATINGPOINT_MAX
Floating-point maximum.- Arity:
21..2:Terms of floating-point Sort (sorts must match)
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
FLOATINGPOINT_LEQ
Floating-point less than or equal.- Arity:
21..2:Terms of floating-point Sort (sorts must match)
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
FLOATINGPOINT_LT
Floating-point less than.- Arity:
21..2:Terms of floating-point Sort (sorts must match)
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
FLOATINGPOINT_GEQ
Floating-point greater than or equal.- Arity:
21..2:Terms of floating-point Sort (sorts must match)
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
FLOATINGPOINT_GT
Floating-point greater than.- Arity:
21..2:Terms of floating-point Sort (sorts must match)
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
FLOATINGPOINT_IS_NORMAL
Floating-point is normal tester.- Arity:
11:Term of floating-point Sort
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
FLOATINGPOINT_IS_SUBNORMAL
Floating-point is sub-normal tester.- Arity:
11:Term of floating-point Sort
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
FLOATINGPOINT_IS_ZERO
Floating-point is zero tester.- Arity:
11:Term of floating-point Sort
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
FLOATINGPOINT_IS_INF
Floating-point is infinite tester.- Arity:
11:Term of floating-point Sort
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
FLOATINGPOINT_IS_NAN
Floating-point is NaN tester.- Arity:
11:Term of floating-point Sort
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
FLOATINGPOINT_IS_NEG
Floating-point is negative tester.- Arity:
11:Term of floating-point Sort
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
FLOATINGPOINT_IS_POS
Floating-point is positive tester.- Arity:
11:Term of floating-point Sort
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
FLOATINGPOINT_TO_FP_FROM_IEEE_BV
Conversion to floating-point from IEEE-754 bit-vector.- Arity:
11:Term of bit-vector Sort
- Indices:
21:The exponent size2:The significand size
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
FLOATINGPOINT_TO_FP_FROM_FP
Conversion to floating-point from floating-point.- Arity:
21:Term of Sort RoundingMode2:Term of floating-point Sort
- Indices:
21:The exponent size2:The significand size
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
FLOATINGPOINT_TO_FP_FROM_REAL
Conversion to floating-point from Real.- Arity:
21:Term of Sort RoundingMode2:Term of Sort Real
- Indices:
21:The exponent size2:The significand size
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
FLOATINGPOINT_TO_FP_FROM_SBV
Conversion to floating-point from signed bit-vector.- Arity:
21:Term of Sort RoundingMode2:Term of bit-vector Sort
- Indices:
21:The exponent size2:The significand size
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
FLOATINGPOINT_TO_FP_FROM_UBV
Conversion to floating-point from unsigned bit-vector.- Arity:
21:Term of Sort RoundingMode2:Term of bit-vector Sort
- Indices:
21:The exponent size2:The significand size
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
FLOATINGPOINT_TO_UBV
Conversion to unsigned bit-vector from floating-point.- Arity:
21:Term of Sort RoundingMode2:Term of floating-point Sort
- Indices:
11:The size of the bit-vector to convert to.
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
FLOATINGPOINT_TO_SBV
Conversion to signed bit-vector from floating-point.- Arity:
21:Term of Sort RoundingMode2:Term of floating-point Sort
- Indices:
11:The size of the bit-vector to convert to.
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
FLOATINGPOINT_TO_REAL
Conversion to Real from floating-point.- Arity:
11:Term of Sort Real
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
SELECT
Array select.- Arity:
21:Term of array Sort2:Term of array index Sort
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
STORE
Array store.- Arity:
31:Term of array Sort2:Term of array index Sort3:Term of array element Sort
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
CONST_ARRAY
Constant array.- Arity:
21:Term of array Sort2:Term of array element Sort (value)
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
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:
41: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:
- Note:
- This kind is experimental and may be changed or removed in future versions., We currently support the creation of array equalities over index Sorts bit-vector, floating-point, Int and Real. Requires to enable option :ref:`arrays-exp<lbl-option-arrays-exp>`.
- Arity:
-
APPLY_CONSTRUCTOR
Datatype constructor application.- Arity:
n > 01: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:
- Arity:
-
APPLY_SELECTOR
Datatype selector application.- Arity:
21: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.
- Arity:
-
APPLY_TESTER
Datatype tester application.- Arity:
21: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:
- Arity:
-
APPLY_UPDATER
Datatype update application.- Arity:
31: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.
- Arity:
-
MATCH
Match expression. This kind is primarily used in the parser to support the SMT-LIBv2matchexpression. 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.- Arity:
n > 11..n:Terms of kind MATCH_CASE and MATCH_BIND_CASE
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
MATCH_CASE
Match case for nullary constructors. A (constant) case expression to be used within a match expression.- Arity:
21:Term of kind APPLY_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:
- Arity:
-
MATCH_BIND_CASE
Match case with binders, for constructors with selectors and variable patterns. A (non-constant) case expression to be used within a match expression.- Arity:
3- For variable patterns:
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)
- For variable patterns:
- For constructors with selectors:
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)
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
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, .. code. smtlib ((_ tuple.project 1 2 2 3 1) (tuple 10 20 30 40)) yields .. code. smtlib (tuple 20 30 30 40 20)- Arity:
11:Term of tuple Sort
- Indices:
n1..n:The tuple indices to project
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
NULLABLE_LIFT
Lifting operator for nullable terms. This operator lifts a built-in operator or a user-defined function to nullable terms. For built-in kinds use mkNullableLift. For user-defined functions use mkTerm.- Arity:
n > 1 1..n:Terms of nullable sort- Create Term of this Kind with:
- Arity:
-
SEP_NIL
Separation logic nil.- Create Term of this Kind with:
- Note:
- This kind is experimental and may be changed or removed in future versions.
-
SEP_EMP
Separation logic empty heap.- Create Term of this Kind with:
- Note:
- This kind is experimental and may be changed or removed in future versions.
-
SEP_PTO
Separation logic points-to relation.- Arity:
21:Term denoting the location of the points-to constraint2:Term denoting the data of the points-to constraint
- Create Term of this Kind with:
- Create Op of this kind with:
- Note:
- This kind is experimental and may be changed or removed in future versions.
- Arity:
-
SEP_STAR
Separation logic star.- Arity:
n > 11..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:
- Note:
- This kind is experimental and may be changed or removed in future versions.
- Arity:
-
SEP_WAND
Separation logic magic wand.- Arity:
21: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:
- Note:
- This kind is experimental and may be changed or removed in future versions.
- Arity:
-
SET_EMPTY
Empty set.- Create Term of this Kind with:
-
SET_UNION
Set union.- Arity:
21..2:Terms of set Sort
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
SET_INTER
Set intersection.- Arity:
21..2:Terms of set Sort
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
SET_MINUS
Set subtraction.- Arity:
21..2:Terms of set Sort
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
SET_SUBSET
Subset predicate. Determines if the first set is a subset of the second set.- Arity:
21..2:Terms of set Sort
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
SET_MEMBER
Set membership predicate. Determines if the given set element is a member of the second set.- Arity:
21: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:
- Arity:
-
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:
11:Term of any Sort (the set element)
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
SET_INSERT
The set obtained by inserting elements;- Arity:
n > 01..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:
- Create Op of this kind with:
- Arity:
-
SET_CARD
Set cardinality.- Arity:
11:Term of set Sort
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
SET_COMPLEMENT
Set complement with respect to finite universe.- Arity:
11:Term of set Sort
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
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.
-
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: .. math. \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:
31:Term of Kind VARIABLE_LIST2: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:
- Note:
- This kind is experimental and may be changed or removed in future versions.
- Arity:
-
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:
11:Term of set Sort
- Create Term of this Kind with:
- Create Op of this kind with:
- Note:
- This kind is experimental and may be changed or removed in future versions.
- Arity:
-
SET_IS_EMPTY
Set is empty tester.- Arity:
11:Term of set Sort
- Create Term of this Kind with:
- Create Op of this kind with:
- Note:
- This kind is experimental and may be changed or removed in future versions.
- Arity:
-
SET_IS_SINGLETON
Set is singleton tester.- Arity:
11:Term of set Sort
- Create Term of this Kind with:
- Create Op of this kind with:
- Note:
- This kind is experimental and may be changed or removed in future versions.
- Arity:
-
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:
21: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:
- Note:
- This kind is experimental and may be changed or removed in future versions.
- Arity:
-
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:
21:Term of function Sort \((\rightarrow T \; Bool)\)2:Term of bag Sort (Set \(T\))
- Create Term of this Kind with:
- Note:
- This kind is experimental and may be changed or removed in future versions.
- Arity:
-
SET_ALL
Set all. This operator checks whether all elements of a set satisfy a predicate. (set.all \(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 true iff all elements of \(A\) satisfy predicate \(p\).- Arity:
21:Term of function Sort \((\rightarrow T \; Bool)\)2:Term of set Sort (Set \(T\))
- Create Term of this Kind with:
- Note:
- This kind is experimental and may be changed or removed in future versions.
- Arity:
-
SET_SOME
Set some. This operator checks whether at least one element of a set satisfies a predicate. (set.some \(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 true iff at least one element of \(A\) satisfies predicate \(p\).- Arity:
21:Term of function Sort \((\rightarrow T \; Bool)\)2:Term of set Sort (Set \(T\))
- Create Term of this Kind with:
- Note:
- This kind is experimental and may be changed or removed in future versions.
- Arity:
-
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:
21: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:
- Note:
- This kind is experimental and may be changed or removed in future versions.
- Arity:
-
RELATION_JOIN
Relation join.- Arity:
21..2:Terms of relation Sort
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
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. This operator filters the product of two sets based on the equality of projected tuples using indices \(m_1, \dots, m_k\) in relation \(A\), and indices \(n_1, \dots, n_k\) in relation \(B\).- Arity:
21:Term of relation Sort2:Term of relation Sort
- Indices:
n1..n:Indices of the projection
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
RELATION_PRODUCT
Relation cartesian product.- Arity:
21..2:Terms of relation Sort
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
RELATION_TRANSPOSE
Relation transpose.- Arity:
11:Term of relation Sort
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
RELATION_TCLOSURE
Relation transitive closure.- Arity:
11:Term of relation Sort
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
RELATION_JOIN_IMAGE
Relation join image.- Arity:
21..2:Terms of relation Sort
- Create Term of this Kind with:
- Create Op of this kind with:
- Note:
- This kind is experimental and may be changed or removed in future versions.
- Arity:
-
RELATION_IDEN
Relation identity.- Arity:
11:Term of relation Sort
- Create Term of this Kind with:
- Create Op of this kind with:
- Note:
- This kind is experimental and may be changed or removed in future versions.
- Arity:
-
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:
11:Term of relation sort
- Indices:
n1..n:Indices of the projection
- Create Term of this Kind with:
- Note:
- This kind is experimental and may be changed or removed in future versions.
- Arity:
-
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:
31: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:
n1..n:Indices of the projection
- Create Term of this Kind with:
- Create Op of this kind with:
- Note:
- This kind is experimental and may be changed or removed in future versions.
- Arity:
-
RELATION_PROJECT
Relation projection operator extends tuple projection operator to sets.- Arity:
11:Term of relation Sort
- Indices:
n1..n:Indices of the projection
- Create Term of this Kind with:
- Create Op of this kind with:
- Note:
- This kind is experimental and may be changed or removed in future versions.
- Arity:
-
BAG_EMPTY
Empty bag.- Create Term of this Kind with:
-
BAG_UNION_MAX
Bag max union.- Arity:
21..2:Terms of bag Sort
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
BAG_UNION_DISJOINT
Bag disjoint union (sum).- Arity:
21..2:Terms of bag Sort
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
BAG_INTER_MIN
Bag intersection (min).- Arity:
21..2:Terms of bag Sort
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
BAG_DIFFERENCE_SUBTRACT
Bag difference subtract. Subtracts multiplicities of the second from the first.- Arity:
21..2:Terms of bag Sort
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
BAG_DIFFERENCE_REMOVE
Bag difference remove. Removes shared elements in the two bags.- Arity:
21..2:Terms of bag Sort
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
BAG_SUBBAG
Bag inclusion predicate. Determine if multiplicities of the first bag are less than or equal to multiplicities of the second bag.- Arity:
21..2:Terms of bag Sort
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
BAG_COUNT
Bag element multiplicity.- Create Term of this Kind with:
-
BAG_MEMBER
Bag membership predicate.- Arity:
21: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:
- Arity:
-
BAG_SETOF
Bag setof. Eliminate duplicates in a given bag. The returned bag contains exactly the same elements in the given bag, but with multiplicity one.- Arity:
11:Term of bag Sort
- Create Term of this Kind with:
- Create Op of this kind with:
- Note:
- This kind is experimental and may be changed or removed in future versions.
- Arity:
-
BAG_MAKE
Bag make. Construct a bag with the given element and given multiplicity.- Arity:
21: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:
- Arity:
-
BAG_CARD
Bag cardinality.- Arity:
11:Term of bag Sort
- Create Term of this Kind with:
- Create Op of this kind with:
- Note:
- This kind is experimental and may be changed or removed in future versions.
- Arity:
-
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:
11:Term of bag Sort
- Create Term of this Kind with:
- Create Op of this kind with:
- Note:
- This kind is experimental and may be changed or removed in future versions.
- Arity:
-
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:
21: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:
- Note:
- This kind is experimental and may be changed or removed in future versions.
- Arity:
-
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:
21:Term of function Sort \((\rightarrow T \; Bool)\)2:Term of bag Sort (Bag \(T\))
- Create Term of this Kind with:
- Note:
- This kind is experimental and may be changed or removed in future versions.
- Arity:
-
BAG_ALL
Bag all. This operator checks whether all elements of a bag satisfy a predicate. (bag.all \(p \; A\)) takes a predicate \(p\) of Sort \((\rightarrow T \; Bool)\) as a first argument, and a bag \(A\) of Sort (Bag \(T\)) as a second argument, and returns true iff all elements of \(A\) satisfy predicate \(p\).- Arity:
21:Term of function Sort \((\rightarrow T \; Bool)\)2:Term of bag Sort (Bag \(T\))
- Create Term of this Kind with:
- Note:
- This kind is experimental and may be changed or removed in future versions.
- Arity:
-
BAG_SOME
Bag some. This operator checks whether at least one element of a bag satisfies a predicate. (bag.some \(p \; A\)) takes a predicate \(p\) of Sort \((\rightarrow T \; Bool)\) as a first argument, and a bag \(A\) of Sort (Bag \(T\)) as a second argument, and returns true iff at least one element of \(A\) satisfies predicate \(p\).- Arity:
21:Term of function Sort \((\rightarrow T \; Bool)\)2:Term of bag Sort (Bag \(T\))
- Create Term of this Kind with:
- Note:
- This kind is experimental and may be changed or removed in future versions.
- Arity:
-
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:
21: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:
- Note:
- This kind is experimental and may be changed or removed in future versions.
- Arity:
-
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:
21:Term of function Sort \((\rightarrow \; E \; E \; Bool)\)2:Term of bag Sort (Bag \(E\))
- Create Term of this Kind with:
- Note:
- This kind is experimental and may be changed or removed in future versions.
- Arity:
-
TABLE_PRODUCT
Table cross product.- Arity:
21..2:Terms of table Sort
- Create Term of this Kind with:
- Create Op of this kind with:
- Note:
- This kind is experimental and may be changed or removed in future versions.
- Arity:
-
TABLE_PROJECT
Table projection operator extends tuple projection operator to tables.- Arity:
11:Term of table Sort
- Indices:
n1..n:Indices of the projection
- Create Term of this Kind with:
- Create Op of this kind with:
- Note:
- This kind is experimental and may be changed or removed in future versions.
- Arity:
-
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:
31: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:
n1..n:Indices of the projection
- Create Term of this Kind with:
- Create Op of this kind with:
- Note:
- This kind is experimental and may be changed or removed in future versions.
- Arity:
-
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:
21:Term of table Sort2:Term of table Sort
- Indices:
n1..n:Indices of the projection
- Create Term of this Kind with:
- Create Op of this kind with:
- Note:
- This kind is experimental and may be changed or removed in future versions.
- Arity:
-
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:
11:Term of table sort
- Indices:
n1..n:Indices of the projection
- Create Term of this Kind with:
- Note:
- This kind is experimental and may be changed or removed in future versions.
- Arity:
-
STRING_CONCAT
String concat.- Arity:
n > 11..n:Terms of Sort String
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
STRING_IN_REGEXP
String membership.- Arity:
21:Term of Sort String2:Term of Sort RegLan
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
STRING_LENGTH
String length.- Arity:
11:Term of Sort String
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
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:
31:Term of Sort String2: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:
- Arity:
-
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:
31:Term of Sort String2: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:
- Arity:
-
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:
21: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:
- Arity:
-
STRING_CONTAINS
String contains. Determines whether a string \(s_1\) contains another string \(s_2\). If \(s_2\) is empty, the result is alwaystrue.- Arity:
21: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:
- Arity:
-
STRING_INDEXOF
String index-of. 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:
21: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:
- Arity:
-
STRING_INDEXOF_RE
String index-of 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:
31: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:
- Arity:
-
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:
31: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:
- Arity:
-
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:
31: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:
- Arity:
-
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:
31:Term of Sort String (\(s_1\))2:Term of Sort RegLan3:Term of Sort String (\(s_2\))
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
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:
31:Term of Sort String (\(s_1\))2:Term of Sort RegLan3:Term of Sort String (\(s_2\))
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
STRING_TO_LOWER
String to lower case.- Arity:
11:Term of Sort String
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
STRING_TO_UPPER
String to upper case.- Arity:
11:Term of Sort String
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
STRING_REV
String reverse.- Arity:
11:Term of Sort String
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
STRING_TO_CODE
String to code. Returns the code point of a string if it has length one, or returns `-1` otherwise.- Arity:
11:Term of Sort String
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
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 out-of-bounds.- Arity:
11:Term of Sort Int
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
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:
21: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:
- Arity:
-
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:
21: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:
- Arity:
-
STRING_PREFIX
String prefix-of. Determines whether a string \(s_1\) is a prefix of string \(s_2\). If string s1 is empty, this operator returnstrue.- Arity:
21: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:
- Arity:
-
STRING_SUFFIX
String suffix-of. Determines whether a string \(s_1\) is a suffix of the second string. If string \(s_1\) is empty, this operator returnstrue.- Arity:
21: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:
- Arity:
-
STRING_IS_DIGIT
String is-digit. Returns true if given string is a digit (it is one of"0", ...,"9").- Arity:
11:Term of Sort String
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
STRING_FROM_INT
Conversion from Int to String. If the integer is negative this operator returns the empty string.- Arity:
11:Term of Sort Int
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
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:
11:Term of Sort Int
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
CONST_STRING
Constant string.- Create Term of this Kind with:
-
STRING_TO_REGEXP
Conversion from string to regexp.- Arity:
11:Term of Sort String
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
REGEXP_CONCAT
Regular expression concatenation.- Arity:
21..2:Terms of Sort RegLan
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
REGEXP_UNION
Regular expression union.- Arity:
21..2:Terms of Sort RegLan
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
REGEXP_INTER
Regular expression intersection.- Arity:
21..2:Terms of Sort RegLan
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
REGEXP_DIFF
Regular expression difference.- Arity:
21..2:Terms of Sort RegLan
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
REGEXP_STAR
Regular expression \*.- Arity:
11:Term of Sort RegLan
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
REGEXP_PLUS
Regular expression +.- Arity:
11:Term of Sort RegLan
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
REGEXP_OPT
Regular expression ?.- Arity:
11:Term of Sort RegLan
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
REGEXP_RANGE
Regular expression range.- Arity:
21: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:
- Arity:
-
REGEXP_REPEAT
Operator for regular expression repeat.- Arity:
11:Term of Sort RegLan
- Indices:
11:The number of repetitions
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
REGEXP_LOOP
Regular expression loop. Regular expression loop from lower bound to upper bound number of repetitions.- Arity:
11:Term of Sort RegLan
- Indices:
11:The lower bound2:The upper bound
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
REGEXP_NONE
Regular expression none.- Create Term 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:
11:Term of Sort RegLan
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
SEQ_CONCAT
Sequence concat.- Arity:
n > 11..n:Terms of sequence Sort
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
SEQ_LENGTH
Sequence length.- Arity:
11:Term of sequence Sort
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
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:
31:Term of sequence Sort2: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:
- Arity:
-
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:
31:Term of sequence Sort2: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:
- Arity:
-
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 length1.- Arity:
21:Term of sequence Sort2:Term of Sort Int (index \(i\))
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
SEQ_CONTAINS
Sequence contains. Checks whether a sequence \(s_1\) contains another sequence \(s_2\). If \(s_2\) is empty, the result is alwaystrue.- Arity:
21: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:
- Arity:
-
SEQ_INDEXOF
Sequence index-of. 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:
31: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:
- Arity:
-
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:
31: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:
- Arity:
-
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:
31: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:
- Arity:
-
SEQ_REV
Sequence reverse.- Arity:
11:Term of sequence Sort
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
SEQ_PREFIX
Sequence prefix-of. Checks whether a sequence \(s_1\) is a prefix of sequence \(s_2\). If sequence \(s_1\) is empty, this operator returnstrue.- Arity:
11: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:
- Arity:
-
SEQ_SUFFIX
Sequence suffix-of. Checks whether a sequence \(s_1\) is a suffix of sequence \(s_2\). If sequence \(s_1\) is empty, this operator returnstrue.- Arity:
11: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:
- Arity:
-
CONST_SEQUENCE
Constant sequence. A constant sequence is a term that is equivalent to: .. code. smtlib (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 withTerm.getSequenceValue().- Create Term of this Kind with:
-
SEQ_UNIT
Sequence unit. Corresponds to a sequence of length one with the given term.- Arity:
11:Term of any Sort (the element term)
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
SEQ_NTH
Sequence nth. Corresponds to the nth element of a sequence.- Arity:
21:Term of sequence Sort2:Term of Sort Int (\(n\))
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
FORALL
Universally quantified formula.- Arity:
31:Term of Kind VARIABLE_LIST2:Term of Sort Bool (the quantifier body)3:(optional) Term of Kind INST_PATTERN
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
EXISTS
Existentially quantified formula.- Arity:
31:Term of Kind VARIABLE_LIST2:Term of Sort Bool (the quantifier body)3:(optional) Term of Kind INST_PATTERN
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
VARIABLE_LIST
Variable list. A list of variables (used to bind variables under a quantifier)- Arity:
n > 01..n:Terms of Kind VARIABLE
- Create Term of this Kind with:
- Create Op of this kind with:
- Arity:
-
INST_PATTERN
Instantiation pattern. Specifies a (list of) terms to be used as a pattern for quantifier instantiation.- Arity:
n > 01..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.
- Arity:
-
INST_NO_PATTERN
Instantiation no-pattern. Specifies a (list of) terms that should not be used as a pattern for quantifier instantiation.- Arity:
n > 01..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.
- Arity:
-
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 either: (1) have child sets matching the types of the quantified formula, (2) have a child set of tuple type whose component types match the types of the quantified formula. For an example of (1), for a quantified formula: .. code. lisp (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\). Alternatively, as an example of (2), for a quantified formula: .. code. lisp (FORALL (VARIABLE_LIST x y) F (INST_PATTERN_LIST (INST_POOL s))) \(s\) should have Sort (Set (Tuple \(S_1\) \(S_2\))). This annotation specifies that the quantified formula above should be instantiated with the pairs of values in \(s\).- Arity:
n > 01..n:Terms that comprise the pools, which are one-to-one with the variables of the quantified formula to be instantiated
- Create Term of this Kind with:
- Create Op of this kind with:
- Note:
- This kind is experimental and may be changed or removed in future versions., Should only be used as a child of INST_PATTERN_LIST.
- Arity:
-
INST_ADD_TO_POOL
A instantantiation-add-to-pool annotation. An instantantiation-add-to-pool 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: .. code. lisp (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:
21: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:
- Note:
- This kind is experimental and may be changed or removed in future versions., Should only be used as a child of INST_PATTERN_LIST.
- Arity:
-
SKOLEM_ADD_TO_POOL
A skolemization-add-to-pool annotation. An skolemization-add-to-pool 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: .. code. lisp (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:
21: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:
- Note:
- This kind is experimental and may be changed or removed in future versions., Should only be used as a child of INST_PATTERN_LIST.
- Arity:
-
INST_ATTRIBUTE
Instantiation attribute. Specifies a custom property for a quantified formula given by a term that is ascribed a user attribute.- Arity:
n > 01:Term of Kind CONST_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.
- Arity:
-
INST_PATTERN_LIST
A list of instantiation patterns, attributes or annotations.- Arity:
n > 11..n:Terms of Kind INST_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:
- Arity:
-
LAST_KIND
Marks the upper-bound of this enumeration.
-
-
Method Details
-
values
Returns an array containing the constants of this enum class, in the order they are declared.- Returns:
- an array containing the constants of this enum class, in the order they are declared
-
valueOf
Returns the enum constant of this class with the specified name. The string must match exactly an identifier used to declare an enum constant in this class. (Extraneous whitespace characters are not permitted.)- Parameters:
name- the name of the enum constant to be returned.- Returns:
- the enum constant with the specified name
- Throws:
IllegalArgumentException- if this enum class has no constant with the specified nameNullPointerException- if the argument is null
-
fromInt
Converts an integer value to the corresponding enum constant.- Parameters:
value- the integer representation of the enum constant.- Returns:
- the corresponding enum constant for the given integer value.
- Throws:
CVC5ApiException- if the value is outside the valid range, or if no corresponding enum constant exists.
-
getValue
public int getValue()Get the integer value associated with this enum constant.- Returns:
- the integer representation of the enum constant.
-