Package io.github.cvc5

Enum Kind

java.lang.Object

java.lang.Enum<Kind>

io.github.cvc5.Kind

All Implemented Interfaces:

java.io.Serializable, java.lang.Comparable<Kind>

public enum Kind
extends java.lang.Enum<Kind>

Enum Constant Summary

Enum Constants

Enum Constant	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_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_DUPLICATE_REMOVAL	Bag duplicate removal.
BAG_EMPTY	Empty bag.
BAG_FILTER	Bag filter.
BAG_FOLD	Bag fold.
BAG_FROM_SET	Conversion from set to bag.
BAG_INTER_MIN	Bag intersection (min).
BAG_IS_SINGLETON	Bag is singleton tester.
BAG_MAKE	Bag make.
BAG_MAP	Bag map.
BAG_MEMBER	Bag membership predicate.
BAG_PARTITION	Bag partition.
BAG_SUBBAG	Bag inclusion predicate.
BAG_TO_SET	Conversion from bag to set.
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_COMP	Equality comparison (returns bit-vector of size 1).
BITVECTOR_CONCAT	Concatenation of two or more bit-vectors.
BITVECTOR_EXTRACT	Bit-vector extract.
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_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_SDIV	Signed bit-vector division.
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_SREM	Signed bit-vector remainder (sign follows dividend).
BITVECTOR_SUB	Subtraction of two bit-vectors.
BITVECTOR_TO_NAT	Bit-vector conversion to (non-negative) 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_UREM	Unsigned bit-vector remainder.
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_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.
EQ_RANGE	Equality over arrays a and b over a given range [i,j], i.e., ..
EQUAL	Equality, chainable.
EXISTS	Existentially quantified formula.
EXPONENTIAL	Exponential function.
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_MODULUS	Integer modulus, modulus by 0 undefined.
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.
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 ... 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).
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_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_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 ... x_n, a predicate P[x_1...x_n], and a term t[x_1...x_n].
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_SINGLETON	Set is singleton tester.
SET_MAP	Set map.
SET_MEMBER	Set membership predicate.
SET_MINUS	Set subtraction.
SET_SINGLETON	Singleton set.
SET_SUBSET	Subset predicate.
SET_UNION	Set union.
SET_UNIVERSE	Finite universe set.
SEXPR	Symbolic expression.
SINE	Sine function.
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 ... 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).
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.

Method Summary

Modifier and Type	Method	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.

Methods inherited from class java.lang.Enum

clone, compareTo, equals, finalize, getDeclaringClass, hashCode, name, ordinal, toString, valueOf

Methods inherited from class java.lang.Object

getClass, notify, notifyAll, wait, wait, wait

Enum Constant Detail

INTERNAL_KIND

public static final Kind 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

public static final Kind UNDEFINED_KIND

Undefined kind.

Note:

Should never be exposed or created via the API.

NULL_TERM

public static final Kind NULL_TERM

Null kind. The kind of a null term (Solver.getNullTerm()).

Note:

May not be explicitly created via API functions other than Solver.getNullTerm().

UNINTERPRETED_SORT_VALUE

public static final Kind 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

public static final Kind EQUAL

Equality, chainable.

• Arity: n > 1
  • 1..n: Terms of the same 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[])

DISTINCT

public static final Kind DISTINCT

Disequality.

• Arity: n > 1
  • 1..n: Terms of the same 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[])

CONSTANT

public static final Kind CONSTANT

Free constant symbol.

• Create Term of this Kind with:
  • Solver.mkConst(Sort, String)
  • Solver.mkConst(Sort)

Note:

Not permitted in bindings (e.g., FORALL, EXISTS).

VARIABLE

public static final Kind VARIABLE

(Bound) variable.

• Create Term of this Kind with:
  • Solver.mkVar(Sort, String)

Note:

Only permitted in bindings and in lambda and quantifier bodies.

SEXPR

public static final Kind SEXPR

Symbolic expression.

• Arity: n > 0
  • 1..n: Terms with same sorts

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

Note:

This kind is experimental and may be changed or removed in future versions.

LAMBDA

public static final Kind LAMBDA

Lambda expression.

• Arity: 2
  • 1: Term of kind VARIABLE_LIST
  • 2: Term of any Sort (the body of the lambda)

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

WITNESS

public static final Kind 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: .. math. \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: 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

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

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.

CONST_BOOLEAN

public static final Kind CONST_BOOLEAN

Boolean constant.

• Create Term of this Kind with:
  • Solver.mkTrue()
  • Solver.mkFalse()
  • Solver.mkBoolean(boolean)

NOT

public static final Kind NOT

Logical negation.

• Arity: 1
  • 1: Term of Sort Bool

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

AND

public static final Kind AND

Logical conjunction.

• Arity: n > 1
  • 1..n: Terms of Sort Bool

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

IMPLIES

public static final Kind IMPLIES

Logical implication.

• Arity: n > 1
  • 1..n: Terms of Sort Bool

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

OR

public static final Kind OR

Logical disjunction.

• Arity: n > 1
  • 1..n: Terms of Sort Bool

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

XOR

public static final Kind XOR

Logical exclusive disjunction, left associative.

• Arity: n > 1
  • 1..n: Terms of Sort Bool

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

ITE

public static final Kind ITE

If-then-else.

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

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

APPLY_UF

public static final Kind APPLY_UF

Application of an uninterpreted function.

• Arity: n > 1
  • 1: Function Term
  • 2..n: Function argument instantiation Terms of any first-class 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[])

CARDINALITY_CONSTRAINT

public static final Kind 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:
  • Solver.mkCardinalityConstraint(Sort, int)

Note:

This kind is experimental and may be changed or removed in future versions.

HO_APPLY

public static final Kind HO_APPLY

Higher-order applicative encoding of function application, left associative.

• Arity: n = 2
  • 1: Function Term
  • 2: Argument Term of the domain Sort of the function

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

ADD

public static final Kind ADD

Arithmetic addition.

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

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

MULT

public static final Kind MULT

Arithmetic multiplication.

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

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

IAND

public static final Kind IAND

Integer and. Operator for bit-wise 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.

• Arity: 2
  • 1..2: Terms of Sort Int
  • Indices: 1
  • 1: Bit-width k

• Create Term of this Kind with:
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

POW2

public static final Kind POW2

Power of two. Operator for raising 2 to a non-negative integer power.

• Arity: 1
  • 1: Term of Sort Int

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

SUB

public static final Kind SUB

Arithmetic subtraction, left associative.

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

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

NEG

public static final Kind NEG

Arithmetic negation.

• Arity: 1
  • 1: Term of Sort Int or Real

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

DIVISION

public static final Kind DIVISION

Real division, division by 0 undefined, left associative.

• Arity: n > 1
  • 1..n: Terms of Sort Real

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

INTS_DIVISION

public static final Kind INTS_DIVISION

Integer division, division by 0 undefined, left associative.

• Arity: n > 1
  • 1..n: Terms of Sort Int

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

INTS_MODULUS

public static final Kind INTS_MODULUS

Integer modulus, modulus by 0 undefined.

• Arity: 2
  • 1: Term of Sort Int
  • 2: Term of Sort Int

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

ABS

public static final Kind ABS

Absolute value.

• Arity: 1
  • 1: Term of Sort Int or Real

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

POW

public static final Kind POW

Arithmetic power.

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

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

EXPONENTIAL

public static final Kind EXPONENTIAL

Exponential function.

• Arity: 1
  • 1: Term of Sort Real

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

SINE

public static final Kind SINE

Sine function.

• Arity: 1
  • 1: Term of Sort Real

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

COSINE

public static final Kind COSINE

Cosine function.

• Arity: 1
  • 1: Term of Sort Real

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

TANGENT

public static final Kind TANGENT

Tangent function.

• Arity: 1
  • 1: Term of Sort Real

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

COSECANT

public static final Kind COSECANT

Cosecant function.

• Arity: 1
  • 1: Term of Sort Real

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

SECANT

public static final Kind SECANT

Secant function.

• Arity: 1
  • 1: Term of Sort Real

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

COTANGENT

public static final Kind COTANGENT

Cotangent function.

• Arity: 1
  • 1: Term of Sort Real

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

ARCSINE

public static final Kind ARCSINE

Arc sine function.

• Arity: 1
  • 1: Term of Sort Real

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

ARCCOSINE

public static final Kind ARCCOSINE

Arc cosine function.

• Arity: 1
  • 1: Term of Sort Real

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

ARCTANGENT

public static final Kind ARCTANGENT

Arc tangent function.

• Arity: 1
  • 1: Term of Sort Real

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

ARCCOSECANT

public static final Kind ARCCOSECANT

Arc cosecant function.

• Arity: 1
  • 1: Term of Sort Real

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

ARCSECANT

public static final Kind ARCSECANT

Arc secant function.

• Arity: 1
  • 1: Term of Sort Real

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

ARCCOTANGENT

public static final Kind ARCCOTANGENT

Arc cotangent function.

• Arity: 1
  • 1: Term of Sort Real

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

SQRT

public static final Kind SQRT

Square root.

• Arity: 1
  • 1: Term of Sort Real

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

DIVISIBLE

public static final Kind DIVISIBLE

Operator for the divisibility-by-k predicate.

• Arity: 1
  • 1: Term of Sort Int
  • Indices: 1
  • 1: The integer k to divide by.

• Create Term of this Kind with:
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

CONST_RATIONAL

public static final Kind CONST_RATIONAL

Arbitrary-precision rational constant.

• Create Term of this Kind with:
  • Solver.mkReal(String)
  • Solver.mkReal(long)
  • Solver.mkReal(long, long)

CONST_INTEGER

public static final Kind CONST_INTEGER

Arbitrary-precision integer constant.

• Create Term of this Kind with:
  • Solver.mkInteger(String)
  • Solver.mkInteger(long)

LT

public static final Kind LT

Less than, chainable.

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

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

LEQ

public static final Kind LEQ

Less than or equal, chainable.

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

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

GT

public static final Kind GT

Greater than, chainable.

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

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

GEQ

public static final Kind GEQ

Greater than or equal, chainable.

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

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

IS_INTEGER

public static final Kind IS_INTEGER

Is-integer predicate.

• Arity: 1
  • 1: Term of Sort Int or Real

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

TO_INTEGER

public static final Kind TO_INTEGER

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

• Arity: 1
  • 1: Term of Sort Int or Real

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

TO_REAL

public static final Kind TO_REAL

Convert Term of Sort Int or Real to Real.

• Arity: 1
  • 1: Term of Sort Int or Real

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

PI

public static final Kind PI

Pi constant.

• Create Term of this Kind with:
  • Solver.mkPi()

Note:

PI is considered a special symbol of Sort Real, but is not a Real value, i.e., Term.isRealValue() will return false.

CONST_BITVECTOR

public static final Kind CONST_BITVECTOR

Fixed-size bit-vector constant.

• Create Term of this Kind with:
  • Solver.mkBitVector(int, long)
  • Solver.mkBitVector(int, String, int)

BITVECTOR_CONCAT

public static final Kind BITVECTOR_CONCAT

Concatenation of two or more bit-vectors.

• Arity: n > 1
  • 1..n: Terms of bit-vector Sort (sorts must match)

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

BITVECTOR_AND

public static final Kind BITVECTOR_AND

Bit-wise and.

• Arity: n > 1
  • 1..n: Terms of bit-vector Sort (sorts must match)

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

BITVECTOR_OR

public static final Kind BITVECTOR_OR

Bit-wise or.

• Arity: n > 1
  • 1..n: Terms of bit-vector Sort (sorts must match)

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

BITVECTOR_XOR

public static final Kind BITVECTOR_XOR

Bit-wise xor.

• Arity: n > 1
  • 1..n: Terms of bit-vector Sort (sorts must match)

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

BITVECTOR_NOT

public static final Kind BITVECTOR_NOT

Bit-wise negation.

• Arity: 1
  • 1: Term of bit-vector 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[])

BITVECTOR_NAND

public static final Kind BITVECTOR_NAND

Bit-wise nand.

• Arity: 2
  • 1..2: Terms of bit-vector Sort (sorts must match)

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

BITVECTOR_NOR

public static final Kind BITVECTOR_NOR

Bit-wise nor.

• Arity: 2
  • 1..2: Terms of bit-vector Sort (sorts must match)

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

BITVECTOR_XNOR

public static final Kind BITVECTOR_XNOR

Bit-wise xnor, left associative.

• Arity: 2
  • 1..2: Terms of bit-vector Sort (sorts must match)

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

BITVECTOR_COMP

public static final Kind BITVECTOR_COMP

Equality comparison (returns bit-vector of size 1).

• Arity: 2
  • 1..2: Terms of bit-vector Sort (sorts must match)

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

BITVECTOR_MULT

public static final Kind BITVECTOR_MULT

Multiplication of two or more bit-vectors.

• Arity: n > 1
  • 1..n: Terms of bit-vector Sort (sorts must match)

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

BITVECTOR_ADD

public static final Kind BITVECTOR_ADD

Addition of two or more bit-vectors.

• Arity: n > 1
  • 1..n: Terms of bit-vector Sort (sorts must match)

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

BITVECTOR_SUB

public static final Kind BITVECTOR_SUB

Subtraction of two bit-vectors.

• Arity: n > 1
  • 1..n: Terms of bit-vector Sort (sorts must match)

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

BITVECTOR_NEG

public static final Kind BITVECTOR_NEG

Negation of a bit-vector (two's complement).

• Arity: 1
  • 1: Term of bit-vector 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[])

BITVECTOR_UDIV

public static final Kind BITVECTOR_UDIV

Unsigned bit-vector division. Truncates towards 0. If the divisor is zero, the result is all ones.

• Arity: 2
  • 1..2: Terms of bit-vector Sort (sorts must match)

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

BITVECTOR_UREM

public static final Kind BITVECTOR_UREM

Unsigned bit-vector remainder. Remainder from unsigned bit-vector division. If the modulus is zero, the result is the dividend.

• Arity: 2
  • 1..2: Terms of bit-vector Sort (sorts must match)

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

BITVECTOR_SDIV

public static final Kind 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: 2
  • 1..2: Terms of bit-vector Sort (sorts must match)

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

BITVECTOR_SREM

public static final Kind 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: 2
  • 1..2: Terms of bit-vector Sort (sorts must match)

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

BITVECTOR_SMOD

public static final Kind 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: 2
  • 1..2: Terms of bit-vector Sort (sorts must match)

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

BITVECTOR_SHL

public static final Kind BITVECTOR_SHL

Bit-vector shift left.

• Arity: 2
  • 1..2: Terms of bit-vector Sort (sorts must match)

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

BITVECTOR_LSHR

public static final Kind BITVECTOR_LSHR

Bit-vector logical shift right.

• Arity: 2
  • 1..2: Terms of bit-vector Sort (sorts must match)

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

BITVECTOR_ASHR

public static final Kind BITVECTOR_ASHR

Bit-vector arithmetic shift right.

• Arity: 2
  • 1..2: Terms of bit-vector Sort (sorts must match)

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

BITVECTOR_ULT

public static final Kind BITVECTOR_ULT

Bit-vector unsigned less than.

• Arity: 2
  • 1..2: Terms of bit-vector Sort (sorts must match)

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

BITVECTOR_ULE

public static final Kind BITVECTOR_ULE

Bit-vector unsigned less than or equal.

• Arity: 2
  • 1..2: Terms of bit-vector Sort (sorts must match)

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

BITVECTOR_UGT

public static final Kind BITVECTOR_UGT

Bit-vector unsigned greater than.

• Arity: 2
  • 1..2: Terms of bit-vector Sort (sorts must match)

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

BITVECTOR_UGE

public static final Kind BITVECTOR_UGE

Bit-vector unsigned greater than or equal.

• Arity: 2
  • 1..2: Terms of bit-vector Sort (sorts must match)

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

BITVECTOR_SLT

public static final Kind BITVECTOR_SLT

Bit-vector signed less than.

• Arity: 2
  • 1..2: Terms of bit-vector Sort (sorts must match)

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

BITVECTOR_SLE

public static final Kind BITVECTOR_SLE

Bit-vector signed less than or equal.

• Arity: 2
  • 1..2: Terms of bit-vector Sort (sorts must match)

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

BITVECTOR_SGT

public static final Kind BITVECTOR_SGT

Bit-vector signed greater than.

• Arity: 2
  • 1..2: Terms of bit-vector Sort (sorts must match)

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

BITVECTOR_SGE

public static final Kind BITVECTOR_SGE

Bit-vector signed greater than or equal.

• Arity: 2
  • 1..2: Terms of bit-vector Sort (sorts must match)

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

BITVECTOR_ULTBV

public static final Kind BITVECTOR_ULTBV

Bit-vector unsigned less than returning a bit-vector of size 1.

• Arity: 2
  • 1..2: Terms of bit-vector Sort (sorts must match)

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

BITVECTOR_SLTBV

public static final Kind BITVECTOR_SLTBV

Bit-vector signed less than returning a bit-vector of size 1.

• Arity: 2
  • 1..2: Terms of bit-vector Sort (sorts must match)

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

BITVECTOR_ITE

public static final Kind BITVECTOR_ITE

Bit-vector if-then-else. Same semantics as regular ITE, but condition is bit-vector of size 1.

• Arity: 3
  • 1: Term of bit-vector Sort of size `1`
  • 1..3: Terms of bit-vector sort (sorts must match)

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

BITVECTOR_REDOR

public static final Kind BITVECTOR_REDOR

Bit-vector redor.

• Arity: 1
  • 1: Term of bit-vector 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[])

BITVECTOR_REDAND

public static final Kind BITVECTOR_REDAND

Bit-vector redand.

• Arity: 1
  • 1: Term of bit-vector 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[])

BITVECTOR_EXTRACT

public static final Kind BITVECTOR_EXTRACT

Bit-vector extract.

• Arity: 1
  • 1: Term of bit-vector Sort
  • Indices: 2
  • 1: The upper bit index.
  • 2: The lower bit index.

• Create Term of this Kind with:
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

BITVECTOR_REPEAT

public static final Kind BITVECTOR_REPEAT

Bit-vector repeat.

• Arity: 1
  • 1: Term of bit-vector Sort
  • Indices: 1
  • 1: The number of times to repeat the given term.

• Create Term of this Kind with:
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

BITVECTOR_ZERO_EXTEND

public static final Kind BITVECTOR_ZERO_EXTEND

Bit-vector zero extension.

• Arity: 1
  • 1: Term of bit-vector Sort
  • Indices: 1
  • 1: The number of zeroes to extend the given term with.

• Create Term of this Kind with:
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

BITVECTOR_SIGN_EXTEND

public static final Kind BITVECTOR_SIGN_EXTEND

Bit-vector sign extension.

• Arity: 1
  • 1: Term of bit-vector Sort
  • Indices: 1
  • 1: The number of bits (of the value of the sign bit) to extend the given term with.

• Create Term of this Kind with:
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

BITVECTOR_ROTATE_LEFT

public static final Kind BITVECTOR_ROTATE_LEFT

Bit-vector rotate left.

• Arity: 1
  • 1: Term of bit-vector Sort
  • Indices: 1
  • 1: The number of bits to rotate the given term left.

• Create Term of this Kind with:
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

BITVECTOR_ROTATE_RIGHT

public static final Kind BITVECTOR_ROTATE_RIGHT

Bit-vector rotate right.

• Arity: 1
  • 1: Term of bit-vector Sort
  • Indices: 1
  • 1: The number of bits to rotate the given term right.

• Create Term of this Kind with:
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

INT_TO_BITVECTOR

public static final Kind INT_TO_BITVECTOR

Conversion from Int to bit-vector.

• Arity: 1
  • 1: Term of Sort Int
  • Indices: 1
  • 1: The size of the bit-vector to convert to.

• Create Term of this Kind with:
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

BITVECTOR_TO_NAT

public static final Kind BITVECTOR_TO_NAT

Bit-vector conversion to (non-negative) integer.

• Arity: 1
  • 1: Term of bit-vector 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[])

CONST_FLOATINGPOINT

public static final Kind CONST_FLOATINGPOINT

Floating-point constant, created from IEEE-754 bit-vector representation of the floating-point value.

• Create Term of this Kind with:
  • Solver.mkFloatingPoint(int, int, Term)

CONST_ROUNDINGMODE

public static final Kind CONST_ROUNDINGMODE

RoundingMode constant.

• Create Term of this Kind with:
  • Solver.mkRoundingMode(RoundingMode)

FLOATINGPOINT_FP

public static final Kind FLOATINGPOINT_FP

Create floating-point literal from bit-vector triple.

• Arity: 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)

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

FLOATINGPOINT_EQ

public static final Kind FLOATINGPOINT_EQ

Floating-point equality.

• Arity: 2
  • 1..2: Terms of floating-point Sort (sorts must match)

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

FLOATINGPOINT_ABS

public static final Kind FLOATINGPOINT_ABS

Floating-point absolute value.

• Arity: 1
  • 1: Term of floating-point 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[])

FLOATINGPOINT_NEG

public static final Kind FLOATINGPOINT_NEG

Floating-point negation.

• Arity: 1
  • 1: Term of floating-point 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[])

FLOATINGPOINT_ADD

public static final Kind FLOATINGPOINT_ADD

Floating-point addition.

• Arity: 3
  • 1: Term of Sort RoundingMode
  • 2..3: Terms of floating-point Sort (sorts must match)

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

FLOATINGPOINT_SUB

public static final Kind FLOATINGPOINT_SUB

Floating-point sutraction.

• Arity: 3
  • 1: Term of Sort RoundingMode
  • 2..3: Terms of floating-point Sort (sorts must match)

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

FLOATINGPOINT_MULT

public static final Kind FLOATINGPOINT_MULT

Floating-point multiply.

• Arity: 3
  • 1: Term of Sort RoundingMode
  • 2..3: Terms of floating-point Sort (sorts must match)

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

FLOATINGPOINT_DIV

public static final Kind FLOATINGPOINT_DIV

Floating-point division.

• Arity: 3
  • 1: Term of Sort RoundingMode
  • 2..3: Terms of floating-point Sort (sorts must match)

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

FLOATINGPOINT_FMA

public static final Kind FLOATINGPOINT_FMA

Floating-point fused multiply and add.

• Arity: 4
  • 1: Term of Sort RoundingMode
  • 2..4: Terms of floating-point Sort (sorts must match)

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

FLOATINGPOINT_SQRT

public static final Kind FLOATINGPOINT_SQRT

Floating-point square root.

• Arity: 2
  • 1: Term of Sort RoundingMode
  • 2: Term of floating-point 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[])

FLOATINGPOINT_REM

public static final Kind FLOATINGPOINT_REM

Floating-point remainder.

• Arity: 2
  • 1..2: Terms of floating-point Sort (sorts must match)

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

FLOATINGPOINT_RTI

public static final Kind FLOATINGPOINT_RTI

Floating-point round to integral.

• Arity: 2
  • 1..2: Terms of floating-point Sort (sorts must match)

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

FLOATINGPOINT_MIN

public static final Kind FLOATINGPOINT_MIN

Floating-point minimum.

• Arity: 2
  • 1..2: Terms of floating-point Sort (sorts must match)

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

FLOATINGPOINT_MAX

public static final Kind FLOATINGPOINT_MAX

Floating-point maximum.

• Arity: 2
  • 1..2: Terms of floating-point Sort (sorts must match)

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

FLOATINGPOINT_LEQ

public static final Kind FLOATINGPOINT_LEQ

Floating-point less than or equal.

• Arity: 2
  • 1..2: Terms of floating-point Sort (sorts must match)

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

FLOATINGPOINT_LT

public static final Kind FLOATINGPOINT_LT

Floating-point less than.

• Arity: 2
  • 1..2: Terms of floating-point Sort (sorts must match)

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

FLOATINGPOINT_GEQ

public static final Kind FLOATINGPOINT_GEQ

Floating-point greater than or equal.

• Arity: 2
  • 1..2: Terms of floating-point Sort (sorts must match)

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

FLOATINGPOINT_GT

public static final Kind FLOATINGPOINT_GT

Floating-point greater than.

• Arity: 2
  • 1..2: Terms of floating-point Sort (sorts must match)

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

FLOATINGPOINT_IS_NORMAL

public static final Kind FLOATINGPOINT_IS_NORMAL

Floating-point is normal tester.

• Arity: 1
  • 1: Term of floating-point 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[])

FLOATINGPOINT_IS_SUBNORMAL

public static final Kind FLOATINGPOINT_IS_SUBNORMAL

Floating-point is sub-normal tester.

• Arity: 1
  • 1: Term of floating-point 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[])

FLOATINGPOINT_IS_ZERO

public static final Kind FLOATINGPOINT_IS_ZERO

Floating-point is zero tester.

• Arity: 1
  • 1: Term of floating-point 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[])

FLOATINGPOINT_IS_INF

public static final Kind FLOATINGPOINT_IS_INF

Floating-point is infinite tester.

• Arity: 1
  • 1: Term of floating-point 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[])

FLOATINGPOINT_IS_NAN

public static final Kind FLOATINGPOINT_IS_NAN

Floating-point is NaN tester.

• Arity: 1
  • 1: Term of floating-point 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[])

FLOATINGPOINT_IS_NEG

public static final Kind FLOATINGPOINT_IS_NEG

Floating-point is negative tester.

• Arity: 1
  • 1: Term of floating-point 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[])

FLOATINGPOINT_IS_POS

public static final Kind FLOATINGPOINT_IS_POS

Floating-point is positive tester.

• Arity: 1
  • 1: Term of floating-point 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[])

FLOATINGPOINT_TO_FP_FROM_IEEE_BV

public static final Kind FLOATINGPOINT_TO_FP_FROM_IEEE_BV

Conversion to floating-point from IEEE-754 bit-vector.

• Arity: 1
  • 1: Term of bit-vector Sort
  • Indices: 2
  • 1: The exponent size
  • 2: The significand size

• Create Term of this Kind with:
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

FLOATINGPOINT_TO_FP_FROM_FP

public static final Kind FLOATINGPOINT_TO_FP_FROM_FP

Conversion to floating-point from floating-point.

• Arity: 2
  • 1: Term of Sort RoundingMode
  • 2: Term of floating-point Sort
  • Indices: 2
  • 1: The exponent size
  • 2: The significand size

• Create Term of this Kind with:
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

FLOATINGPOINT_TO_FP_FROM_REAL

public static final Kind FLOATINGPOINT_TO_FP_FROM_REAL

Conversion to floating-point from Real.

• Arity: 2
  • 1: Term of Sort RoundingMode
  • 2: Term of Sort Real
  • Indices: 2
  • 1: The exponent size
  • 2: The significand size

• Create Term of this Kind with:
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

FLOATINGPOINT_TO_FP_FROM_SBV

public static final Kind FLOATINGPOINT_TO_FP_FROM_SBV

Conversion to floating-point from signed bit-vector.

• Arity: 2
  • 1: Term of Sort RoundingMode
  • 2: Term of bit-vector Sort
  • Indices: 2
  • 1: The exponent size
  • 2: The significand size

• Create Term of this Kind with:
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

FLOATINGPOINT_TO_FP_FROM_UBV

public static final Kind FLOATINGPOINT_TO_FP_FROM_UBV

Conversion to floating-point from unsigned bit-vector.

• Arity: 2
  • 1: Term of Sort RoundingMode
  • 2: Term of bit-vector Sort
  • Indices: 2
  • 1: The exponent size
  • 2: The significand size

• Create Term of this Kind with:
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

FLOATINGPOINT_TO_UBV

public static final Kind FLOATINGPOINT_TO_UBV

Conversion to unsigned bit-vector from floating-point.

• Arity: 1
  • 1: Term of floating-point Sort
  • Indices: 1
  • 1: The size of the bit-vector to convert to.

• Create Term of this Kind with:
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

FLOATINGPOINT_TO_SBV

public static final Kind FLOATINGPOINT_TO_SBV

Conversion to signed bit-vector from floating-point.

• Arity: 1
  • 1: Term of floating-point Sort
  • Indices: 1
  • 1: The size of the bit-vector to convert to.

• Create Term of this Kind with:
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

FLOATINGPOINT_TO_REAL

public static final Kind FLOATINGPOINT_TO_REAL

Conversion to Real from floating-point.

• Arity: 1
  • 1: Term of Sort Real

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

SELECT

public static final Kind SELECT

Array select.

• Arity: 2
  • 1: Term of array Sort
  • 2: Term of array index 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[])

STORE

public static final Kind STORE

Array store.

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

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

CONST_ARRAY

public static final Kind CONST_ARRAY

Constant array.

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

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

EQ_RANGE

public static final Kind EQ_RANGE

Equality over arrays a and b over a given range [i,j], i.e., .. math. \forall k . i \leq k \leq j \Rightarrow a[k] = b[k]

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

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

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>`.

APPLY_CONSTRUCTOR

public static final Kind APPLY_CONSTRUCTOR

Datatype constructor application.

• Arity: 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)

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

APPLY_SELECTOR

public static final Kind APPLY_SELECTOR

Datatype selector application.

• Arity: 2
  • 1: DatatypeSelector Term (see DatatypeSelector.getTerm() )
  • 2: Term of the codomain Sort of the selector

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

Note:

Undefined if misapplied.

APPLY_TESTER

public static final Kind APPLY_TESTER

Datatype tester application.

• Arity: 2
  • 1: Datatype tester Term (see DatatypeConstructor.getTesterTerm() )
  • 2: Term of Datatype Sort (DatatypeConstructor must belong to this Datatype 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[])

APPLY_UPDATER

public static final Kind APPLY_UPDATER

Datatype update application.

• Arity: 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)

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

Note:

Does not change the datatype argument if misapplied.

MATCH

public static final Kind MATCH

Match expression. This kind is primarily used in the parser to support the SMT-LIBv2 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.

• Arity: n > 1
  • 1..n: Terms of kind MATCH_CASE and MATCH_BIND_CASE

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

MATCH_CASE

public static final Kind MATCH_CASE

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

• Arity: 2
  • 1: 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:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

MATCH_BIND_CASE

public static final Kind 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 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:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

TUPLE_PROJECT

public static final Kind 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: 1
  • 1: Term of tuple Sort
  • Indices: n
  • 1..n: The tuple indices to project

• Create Term of this Kind with:
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

SEP_NIL

public static final Kind SEP_NIL

Separation logic nil.

• Create Term of this Kind with:
  • Solver.mkSepNil(Sort)

Note:

This kind is experimental and may be changed or removed in future versions.

SEP_EMP

public static final Kind SEP_EMP

Separation logic empty heap.

• Create Term of this Kind with:
  • Solver.mkSepEmp()

Note:

This kind is experimental and may be changed or removed in future versions.

SEP_PTO

public static final Kind SEP_PTO

Separation logic points-to relation.

• Arity: 2
  • 1: Term denoting the location of the points-to constraint
  • 2: Term denoting the data of the points-to constraint

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

Note:

This kind is experimental and may be changed or removed in future versions.

SEP_STAR

public static final Kind SEP_STAR

Separation logic star.

• Arity: n > 1
  • 1..n: Terms of sort Bool (the child constraints that hold in

disjoint (separated) heaps)

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

Note:

This kind is experimental and may be changed or removed in future versions.

SEP_WAND

public static final Kind SEP_WAND

Separation logic magic wand.

• Arity: 2
  • 1: Terms of Sort Bool (the antecendant of the magic wand constraint)
  • 2: Terms of Sort Bool (conclusion of the magic wand constraint,

which is asserted to hold in all heaps that are disjoint extensions of the antecedent)

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

Note:

This kind is experimental and may be changed or removed in future versions.

SET_EMPTY

public static final Kind SET_EMPTY

Empty set.

• Create Term of this Kind with:
  • Solver.mkEmptySet(Sort)

SET_UNION

public static final Kind SET_UNION

Set union.

• Arity: 2
  • 1..2: Terms 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

public static final Kind SET_INTER

Set intersection.

• Arity: 2
  • 1..2: Terms 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_MINUS

public static final Kind SET_MINUS

Set subtraction.

• Arity: 2
  • 1..2: Terms 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_SUBSET

public static final Kind SET_SUBSET

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

• Arity: 2
  • 1..2: Terms of set Sort

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

SET_MEMBER

public static final Kind SET_MEMBER

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

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

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

SET_SINGLETON

public static final Kind SET_SINGLETON

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

• Arity: 1
  • 1: Term of any Sort (the set element)

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

SET_INSERT

public static final Kind 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_CARD

public static final Kind SET_CARD

Set cardinality.

• Arity: 1
  • 1: 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_COMPLEMENT

public static final Kind SET_COMPLEMENT

Set complement with respect to finite universe.

• Arity: 1
  • 1: 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_UNIVERSE

public static final Kind SET_UNIVERSE

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

• Create Term of this Kind with:
  • Solver.mkUniverseSet(Sort)

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 return false.

SET_COMPREHENSION

public static final Kind 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: 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

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

Note:

This kind is experimental and may be changed or removed in future versions.

SET_CHOOSE

public static final Kind SET_CHOOSE

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

• Arity: 1
  • 1: Term of set Sort

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

Note:

This kind is experimental and may be changed or removed in future versions.

SET_IS_SINGLETON

public static final Kind SET_IS_SINGLETON

Set is singleton tester.

• Arity: 1
  • 1: 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[])

Note:

This kind is experimental and may be changed or removed in future versions.

SET_MAP

public static final Kind SET_MAP

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

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

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

Note:

This kind is experimental and may be changed or removed in future versions.

SET_FILTER

public static final Kind SET_FILTER

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

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

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

Note:

This kind is experimental and may be changed or removed in future versions.

SET_FOLD

public static final Kind SET_FOLD

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

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

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

Note:

This kind is experimental and may be changed or removed in future versions.

RELATION_JOIN

public static final Kind RELATION_JOIN

Relation join.

• Arity: 2
  • 1..2: Terms of relation 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[])

RELATION_PRODUCT

public static final Kind RELATION_PRODUCT

Relation cartesian product.

• Arity: 2
  • 1..2: Terms of relation 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[])

RELATION_TRANSPOSE

public static final Kind RELATION_TRANSPOSE

Relation transpose.

• Arity: 1
  • 1: Term of relation 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[])

RELATION_TCLOSURE

public static final Kind RELATION_TCLOSURE

Relation transitive closure.

• Arity: 1
  • 1: Term of relation 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[])

RELATION_JOIN_IMAGE

public static final Kind RELATION_JOIN_IMAGE

Relation join image.

• Arity: 2
  • 1..2: Terms of relation 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[])

Note:

This kind is experimental and may be changed or removed in future versions.

RELATION_IDEN

public static final Kind RELATION_IDEN

Relation identity.

• Arity: 1
  • 1: Term of relation 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[])

Note:

This kind is experimental and may be changed or removed in future versions.

RELATION_GROUP

public static final Kind RELATION_GROUP

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

• Arity: 1
  • 1: Term of relation sort
  • Indices: n
  • 1..n: Indices of the projection

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

Note:

This kind is experimental and may be changed or removed in future versions.

RELATION_AGGREGATE

public static final Kind RELATION_AGGREGATE

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

• Arity: 3
  • 1: Term of sort (\rightarrow (Tuple \; T_1 \; ... \; T_j)\; T \; T)
  • 2: Term of Sort T
  • 3: Term of relation sort Relation T_1 ... T_j
  • Indices: n
  • 1..n: Indices of the projection

• Create Term of this Kind with:
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

Note:

This kind is experimental and may be changed or removed in future versions.

RELATION_PROJECT

public static final Kind RELATION_PROJECT

Relation projection operator extends tuple projection operator to sets.

• Arity: 1
  • 1: Term of relation Sort
  • Indices: n
  • 1..n: Indices of the projection

• Create Term of this Kind with:
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

Note:

This kind is experimental and may be changed or removed in future versions.

BAG_EMPTY

public static final Kind BAG_EMPTY

Empty bag.

• Create Term of this Kind with:
  • Solver.mkEmptyBag(Sort)

BAG_UNION_MAX

public static final Kind BAG_UNION_MAX

Bag max union.

• Arity: 2
  • 1..2: Terms of bag 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[])

BAG_UNION_DISJOINT

public static final Kind BAG_UNION_DISJOINT

Bag disjoint union (sum).

• Arity: 2
  • 1..2: Terms of bag 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[])

BAG_INTER_MIN

public static final Kind BAG_INTER_MIN

Bag intersection (min).

• Arity: 2
  • 1..2: Terms of bag 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[])

BAG_DIFFERENCE_SUBTRACT

public static final Kind BAG_DIFFERENCE_SUBTRACT

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

• Arity: 2
  • 1..2: Terms of bag Sort

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

BAG_DIFFERENCE_REMOVE

public static final Kind BAG_DIFFERENCE_REMOVE

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

• Arity: 2
  • 1..2: Terms of bag Sort

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

BAG_SUBBAG

public static final Kind BAG_SUBBAG

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

• Arity: 2
  • 1..2: Terms of bag Sort

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

BAG_COUNT

public static final Kind BAG_COUNT

Bag element multiplicity.

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term, Term)
  • Solver.mkTerm(Kind, Term[])

BAG_MEMBER

public static final Kind BAG_MEMBER

Bag membership predicate.

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

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

BAG_DUPLICATE_REMOVAL

public static final Kind BAG_DUPLICATE_REMOVAL

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

• Arity: 1
  • 1: Term of bag Sort

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

Note:

This kind is experimental and may be changed or removed in future versions.

BAG_MAKE

public static final Kind BAG_MAKE

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

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

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

BAG_CARD

public static final Kind BAG_CARD

Bag cardinality.

• Arity: 1
  • 1: Term of bag 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[])

Note:

This kind is experimental and may be changed or removed in future versions.

BAG_CHOOSE

public static final Kind BAG_CHOOSE

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

• Arity: 1
  • 1: Term of bag Sort

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

Note:

This kind is experimental and may be changed or removed in future versions.

BAG_IS_SINGLETON

public static final Kind BAG_IS_SINGLETON

Bag is singleton tester.

• Arity: 1
  • 1: Term of bag 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[])

Note:

This kind is experimental and may be changed or removed in future versions.

BAG_FROM_SET

public static final Kind BAG_FROM_SET

Conversion from set to bag.

• Arity: 1
  • 1: 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[])

Note:

This kind is experimental and may be changed or removed in future versions.

BAG_TO_SET

public static final Kind BAG_TO_SET

Conversion from bag to set.

• Arity: 1
  • 1: Term of bag 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[])

Note:

This kind is experimental and may be changed or removed in future versions.

BAG_MAP

public static final Kind BAG_MAP

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

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

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

Note:

This kind is experimental and may be changed or removed in future versions.

BAG_FILTER

public static final Kind BAG_FILTER

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

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

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

Note:

This kind is experimental and may be changed or removed in future versions.

BAG_FOLD

public static final Kind BAG_FOLD

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

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

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

Note:

This kind is experimental and may be changed or removed in future versions.

BAG_PARTITION

public static final Kind BAG_PARTITION

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

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

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

Note:

This kind is experimental and may be changed or removed in future versions.

TABLE_PRODUCT

public static final Kind TABLE_PRODUCT

Table cross product.

• Arity: 2
  • 1..2: Terms of table 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[])

Note:

This kind is experimental and may be changed or removed in future versions.

TABLE_PROJECT

public static final Kind TABLE_PROJECT

Table projection operator extends tuple projection operator to tables.

• Arity: 1
  • 1: Term of table Sort
  • Indices: n
  • 1..n: Indices of the projection

• Create Term of this Kind with:
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

Note:

This kind is experimental and may be changed or removed in future versions.

TABLE_AGGREGATE

public static final Kind TABLE_AGGREGATE

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

• Arity: 3
  • 1: Term of sort (\rightarrow (Tuple \; T_1 \; ... \; T_j)\; T \; T)
  • 2: Term of Sort T
  • 3: Term of table sort Table T_1 ... T_j
  • Indices: n
  • 1..n: Indices of the projection

• Create Term of this Kind with:
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

Note:

This kind is experimental and may be changed or removed in future versions.

TABLE_JOIN

public static final Kind TABLE_JOIN

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

• Arity: 2
  • 1: Term of table Sort
  • 2: Term of table Sort
  • Indices: n
  • 1..n: Indices of the projection

• Create Term of this Kind with:
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

Note:

This kind is experimental and may be changed or removed in future versions.

TABLE_GROUP

public static final Kind TABLE_GROUP

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

• Arity: 1
  • 1: Term of table sort
  • Indices: n
  • 1..n: Indices of the projection

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

Note:

This kind is experimental and may be changed or removed in future versions.

STRING_CONCAT

public static final Kind STRING_CONCAT

String concat.

• Arity: n > 1
  • 1..n: Terms of Sort String

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

STRING_IN_REGEXP

public static final Kind STRING_IN_REGEXP

String membership.

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

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

STRING_LENGTH

public static final Kind STRING_LENGTH

String length.

• Arity: 1
  • 1: Term of Sort String

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

STRING_SUBSTR

public static final Kind STRING_SUBSTR

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

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

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

STRING_UPDATE

public static final Kind STRING_UPDATE

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

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

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

STRING_CHARAT

public static final Kind STRING_CHARAT

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

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

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

STRING_CONTAINS

public static final Kind STRING_CONTAINS

String contains. Determines whether a string s_1 contains another string s_2. If s_2 is empty, the result is always true.

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

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

STRING_INDEXOF

public static final Kind 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: 2
  • 1: Term of Sort String (substring s_1)
  • 2: Term of Sort String (substring s_2)
  • 3: Term of Sort Int (index i)

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

STRING_INDEXOF_RE

public static final Kind 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: 3
  • 1: Term of Sort String (string s)
  • 2: Term of Sort RegLan (regular expression r)
  • 3: Term of Sort Int (index i)

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

STRING_REPLACE

public static final Kind STRING_REPLACE

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

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

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

STRING_REPLACE_ALL

public static final Kind STRING_REPLACE_ALL

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

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

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

STRING_REPLACE_RE

public static final Kind STRING_REPLACE_RE

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

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

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

STRING_REPLACE_RE_ALL

public static final Kind STRING_REPLACE_RE_ALL

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

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

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

STRING_TO_LOWER

public static final Kind STRING_TO_LOWER

String to lower case.

• Arity: 1
  • 1: Term of Sort String

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

STRING_TO_UPPER

public static final Kind STRING_TO_UPPER

String to upper case.

• Arity: 1
  • 1: Term of Sort String

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

STRING_REV

public static final Kind STRING_REV

String reverse.

• Arity: 1
  • 1: Term of Sort String

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

STRING_TO_CODE

public static final Kind STRING_TO_CODE

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

• Arity: 1
  • 1: Term of Sort String

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

STRING_FROM_CODE

public static final Kind 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: 1
  • 1: Term of Sort Int

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

STRING_LT

public static final Kind STRING_LT

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

• Arity: 2
  • 1: Term of Sort String (s_1)
  • 2: Term of Sort String (s_2)

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

STRING_LEQ

public static final Kind STRING_LEQ

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

• Arity: 2
  • 1: Term of Sort String (s_1)
  • 2: Term of Sort String (s_2)

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

STRING_PREFIX

public static final Kind 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 returns true.

• Arity: 2
  • 1: Term of Sort String (s_1)
  • 2: Term of Sort String (s_2)

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

STRING_SUFFIX

public static final Kind 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 returns true.

• Arity: 2
  • 1: Term of Sort String (s_1)
  • 2: Term of Sort String (s_2)

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

STRING_IS_DIGIT

public static final Kind STRING_IS_DIGIT

String is-digit. Returns true if given string is a digit (it is one of "0", ..., "9").

• Arity: 1
  • 1: Term of Sort String

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

STRING_FROM_INT

public static final Kind STRING_FROM_INT

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

• Arity: 1
  • 1: Term of Sort Int

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

STRING_TO_INT

public static final Kind STRING_TO_INT

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

• Arity: 1
  • 1: Term of Sort Int

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

CONST_STRING

public static final Kind CONST_STRING

Constant string.

• Create Term of this Kind with:
  • Solver.mkString(String, boolean)

STRING_TO_REGEXP

public static final Kind STRING_TO_REGEXP

Conversion from string to regexp.

• Arity: 1
  • 1: Term of Sort String

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

REGEXP_CONCAT

public static final Kind REGEXP_CONCAT

Regular expression concatenation.

• Arity: 2
  • 1..2: Terms of Sort RegLan

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

REGEXP_UNION

public static final Kind REGEXP_UNION

Regular expression union.

• Arity: 2
  • 1..2: Terms of Sort RegLan

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

REGEXP_INTER

public static final Kind REGEXP_INTER

Regular expression intersection.

• Arity: 2
  • 1..2: Terms of Sort RegLan

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

REGEXP_DIFF

public static final Kind REGEXP_DIFF

Regular expression difference.

• Arity: 2
  • 1..2: Terms of Sort RegLan

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

REGEXP_STAR

public static final Kind REGEXP_STAR

Regular expression \*.

• Arity: 1
  • 1: Term of Sort RegLan

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

REGEXP_PLUS

public static final Kind REGEXP_PLUS

Regular expression +.

• Arity: 1
  • 1: Term of Sort RegLan

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

REGEXP_OPT

public static final Kind REGEXP_OPT

Regular expression ?.

• Arity: 1
  • 1: Term of Sort RegLan

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

REGEXP_RANGE

public static final Kind REGEXP_RANGE

Regular expression range.

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

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

REGEXP_REPEAT

public static final Kind REGEXP_REPEAT

Operator for regular expression repeat.

• Arity: 1
  • 1: Term of Sort RegLan
  • Indices: 1
  • 1: The number of repetitions

• Create Term of this Kind with:
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

REGEXP_LOOP

public static final Kind REGEXP_LOOP

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

• Arity: 1
  • 1: Term of Sort RegLan
  • Indices: 1
  • 1: The lower bound
  • 2: The upper bound

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

REGEXP_NONE

public static final Kind REGEXP_NONE

Regular expression none.

• Create Term of this Kind with:
  • Solver.mkRegexpNone()

REGEXP_ALL

public static final Kind REGEXP_ALL

Regular expression all.

• Create Term of this Kind with:
  • Solver.mkRegexpAll()

REGEXP_ALLCHAR

public static final Kind REGEXP_ALLCHAR

Regular expression all characters.

• Create Term of this Kind with:
  • Solver.mkRegexpAllchar()

REGEXP_COMPLEMENT

public static final Kind REGEXP_COMPLEMENT

Regular expression complement.

• Arity: 1
  • 1: Term of Sort RegLan

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

SEQ_CONCAT

public static final Kind SEQ_CONCAT

Sequence concat.

• Arity: n > 1
  • 1..n: Terms of sequence 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[])

SEQ_LENGTH

public static final Kind SEQ_LENGTH

Sequence length.

• Arity: 1
  • 1: Term of sequence 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[])

SEQ_EXTRACT

public static final Kind SEQ_EXTRACT

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

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

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

SEQ_UPDATE

public static final Kind SEQ_UPDATE

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

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

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

SEQ_AT

public static final Kind SEQ_AT

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

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

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

SEQ_CONTAINS

public static final Kind SEQ_CONTAINS

Sequence contains. Checks whether a sequence s_1 contains another sequence s_2. If s_2 is empty, the result is always true.

• Arity: 2
  • 1: Term of sequence Sort (s_1)
  • 2: Term of sequence Sort (s_2)

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

SEQ_INDEXOF

public static final Kind 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: 3
  • 1: Term of sequence Sort (s_1)
  • 2: Term of sequence Sort (s_2)
  • 3: Term of Sort Int (i)

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

SEQ_REPLACE

public static final Kind SEQ_REPLACE

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

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

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

SEQ_REPLACE_ALL

public static final Kind SEQ_REPLACE_ALL

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

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

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

SEQ_REV

public static final Kind SEQ_REV

Sequence reverse.

• Arity: 1
  • 1: Term of sequence 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[])

SEQ_PREFIX

public static final Kind 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 returns true.

• Arity: 1
  • 1: Term of sequence Sort (s_1)
  • 2: Term of sequence Sort (s_2)

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

SEQ_SUFFIX

public static final Kind 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 returns true.

• Arity: 1
  • 1: Term of sequence Sort (s_1)
  • 2: Term of sequence Sort (s_2)

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

CONST_SEQUENCE

public static final Kind 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 with Term.getSequenceValue().

• Create Term of this Kind with:
  • Solver.mkEmptySequence(Sort)

SEQ_UNIT

public static final Kind SEQ_UNIT

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

• Arity: 1
  • 1: Term of any Sort (the element term)

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

SEQ_NTH

public static final Kind SEQ_NTH

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

• Arity: 2
  • 1: Term of sequence Sort
  • 2: Term of Sort Int (n)

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

FORALL

public static final Kind FORALL

Universally quantified formula.

• Arity: 3
  • 1: Term of Kind VARIABLE_LIST
  • 2: Term of Sort Bool (the quantifier body)
  • 3: (optional) Term of Kind INST_PATTERN

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

EXISTS

public static final Kind EXISTS

Existentially quantified formula.

• Arity: 3
  • 1: Term of Kind VARIABLE_LIST
  • 2: Term of Sort Bool (the quantifier body)
  • 3: (optional) Term of Kind INST_PATTERN

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

VARIABLE_LIST

public static final Kind VARIABLE_LIST

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

• Arity: n > 0
  • 1..n: Terms of Kind VARIABLE

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

INST_PATTERN

public static final Kind INST_PATTERN

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

• Arity: n > 0
  • 1..n: Terms of any Sort

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

Note:

Should only be used as a child of INST_PATTERN_LIST.

INST_NO_PATTERN

public static final Kind INST_NO_PATTERN

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

• Arity: n > 0
  • 1..n: Terms of any Sort

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

Note:

Should only be used as a child of INST_PATTERN_LIST.

INST_POOL

public static final Kind INST_POOL

Instantiation pool annotation. Specifies an annotation for pool based instantiation. In detail, pool symbols can be declared via the method

• Solver.declarePool(String, Sort, Term[])

A pool symbol represents a set of terms of a given sort. An instantiation pool annotation should match the types of the quantified formula. For example, for a quantified formula: .. 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.

• Arity: n > 0
  • 1..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:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

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.

INST_ADD_TO_POOL

public static final Kind 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: 2
  • 1: The Term whose free variables are bound by the quantified formula.
  • 2: The pool to add to, whose Sort should be a set of elements that match the Sort of the first argument.

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

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.

SKOLEM_ADD_TO_POOL

public static final Kind 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: 2
  • 1: The Term whose free variables are bound by the quantified formula.
  • 2: The pool to add to, whose Sort should be a set of elements that match the Sort of the first argument.

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

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.

INST_ATTRIBUTE

public static final Kind INST_ATTRIBUTE

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

• Arity: n > 0
  • 1: Term of Kind CONST_STRING (the keyword of the attribute)
  • 2...n: Terms representing the values of the attribute

• Create Term of this Kind with:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

Note:

Should only be used as a child of INST_PATTERN_LIST.

INST_PATTERN_LIST

public static final Kind INST_PATTERN_LIST

A list of instantiation patterns, attributes or annotations.

• Arity: n > 1
  • 1..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:
  • Solver.mkTerm(Kind, Term[])
  • Solver.mkTerm(Op, Term[])

• Create Op of this kind with:
  • Solver.mkOp(Kind, int[])

LAST_KIND

public static final Kind LAST_KIND

Marks the upper-bound of this enumeration.

Method Detail

values

public static Kind[] values()

Returns an array containing the constants of this enum type, in the order they are declared. This method may be used to iterate over the constants as follows:

for (Kind c : Kind.values())
    System.out.println(c);

Returns:

an array containing the constants of this enum type, in the order they are declared

valueOf

public static Kind valueOf(java.lang.String name)

Returns the enum constant of this type with the specified name. The string must match exactly an identifier used to declare an enum constant in this type. (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:

java.lang.IllegalArgumentException - if this enum type has no constant with the specified name

java.lang.NullPointerException - if the argument is null

fromInt

public static Kind fromInt(int value)
                    throws CVC5ApiException

Throws:

CVC5ApiException

getValue

public int getValue()