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