Kind

Every Term has an associated kind. This kind distinguishes if the Term is a value, constant, variable or operator, and what kind of each. For example, a bit-vector value has kind CONST_BITVECTOR , a free constant symbol has kind CONSTANT , an equality over terms of any sort has kind EQUAL , and a universally quantified formula has kind FORALL .

enum cvc5 :: Kind

The kind of a cvc5 Term .

Values:

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

enumerator UNDEFINED_KIND

Undefined kind.

Note

Should never be exposed or created via the API.

enumerator NULL_TERM

Null kind.

The kind of a null term ( Term::Term() ).

Note

May not be explicitly created via API functions other than Term::Term() .

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

enumerator EQUAL

Equality, chainable.

enumerator DISTINCT

Disequality.

enumerator CONSTANT

Free constant symbol.

  • Create Term of this Kind with:

    • Solver::mkConst(const Sort&, const std::string&) const

    • Solver::mkConst(const Sort&) const

Note

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

enumerator VARIABLE

(Bound) variable.

  • Create Term of this Kind with:

    • Solver::mkVar(const Sort&, const std::string&) const

Note

Only permitted in bindings and in lambda and quantifier bodies.

enumerator SEXPR

Symbolic expression.

Warning

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

enumerator LAMBDA

Lambda expression.

enumerator WITNESS

Witness.

The syntax of a witness term is similar to a quantified formula except that only one variable is allowed. For example, the term 

(witness ((x S)) F)

returns an element \(x\) of Sort \(S\) and asserts formula \(F\) .

The witness operator behaves like the description operator (see https://planetmath.org/hilbertsvarepsilonoperator ) if there is no \(x\) that satisfies \(F\) . But if such \(x\) exists, the witness operator does not enforce the following axiom which ensures uniqueness up to logical equivalence:

\[\forall x. F \equiv G \Rightarrow witness~x. F = witness~x. G\]

For example, if there are two elements of Sort \(S\) that satisfy formula \(F\) , then the following formula is satisfiable: 

(distinct
   (witness ((x Int)) F)
   (witness ((x Int)) F))

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\) .

enumerator CONST_BOOLEAN

Boolean constant.

enumerator NOT

Logical negation.

enumerator AND

Logical conjunction.

enumerator IMPLIES

Logical implication.

enumerator OR

Logical disjunction.

enumerator XOR

Logical exclusive disjunction, left associative.

enumerator ITE

If-then-else.

enumerator APPLY_UF

Application of an uninterpreted function.

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

Warning

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

enumerator HO_APPLY

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

enumerator ADD

Arithmetic addition.

enumerator MULT

Arithmetic multiplication.

enumerator IAND

Integer and.

Operator for bit-wise AND over integers, parameterized by a (positive) bit-width \(k\) . 

((_ iand k) i_1 i_2)

is equivalent to 

((_ iand k) i_1 i_2)
(bv2int (bvand ((_ int2bv k) i_1) ((_ int2bv k) i_2)))

for all integers i_1 , i_2 .

  • Arity: 2

    • 1..2: Terms of Sort Int

  • Indices: 1

    • 1: Bit-width \(k\)

enumerator POW2

Power of two.

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

enumerator SUB

Arithmetic subtraction, left associative.

enumerator NEG

Arithmetic negation.

enumerator DIVISION

Real division, division by 0 undefined, left associative.

enumerator INTS_DIVISION

Integer division, division by 0 undefined, left associative.

enumerator INTS_MODULUS

Integer modulus, modulus by 0 undefined.

enumerator ABS

Absolute value.

enumerator POW

Arithmetic power.

enumerator EXPONENTIAL

Exponential function.

enumerator SINE

Sine function.

enumerator COSINE

Cosine function.

enumerator TANGENT

Tangent function.

enumerator COSECANT

Cosecant function.

enumerator SECANT

Secant function.

enumerator COTANGENT

Cotangent function.

enumerator ARCSINE

Arc sine function.

enumerator ARCCOSINE

Arc cosine function.

enumerator ARCTANGENT

Arc tangent function.

enumerator ARCCOSECANT

Arc cosecant function.

enumerator ARCSECANT

Arc secant function.

enumerator ARCCOTANGENT

Arc cotangent function.

enumerator SQRT

Square root.

enumerator DIVISIBLE

Operator for the divisibility-by- \(k\) predicate.

  • Arity: 1

    • 1: Term of Sort Int

  • Indices: 1

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

enumerator CONST_RATIONAL

Arbitrary-precision rational constant.

enumerator CONST_INTEGER

Arbitrary-precision integer constant.

enumerator LT

Less than, chainable.

enumerator LEQ

Less than or equal, chainable.

enumerator GT

Greater than, chainable.

enumerator GEQ

Greater than or equal, chainable.

enumerator IS_INTEGER

Is-integer predicate.

enumerator TO_INTEGER

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

enumerator TO_REAL

Convert Term of Sort Int or Real to Real.

enumerator PI

Pi constant.

Note

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

enumerator CONST_BITVECTOR

Fixed-size bit-vector constant.

enumerator BITVECTOR_CONCAT

Concatenation of two or more bit-vectors.

enumerator BITVECTOR_AND

Bit-wise and.

enumerator BITVECTOR_OR

Bit-wise or.

enumerator BITVECTOR_XOR

Bit-wise xor.

enumerator BITVECTOR_NOT

Bit-wise negation.

enumerator BITVECTOR_NAND

Bit-wise nand.

enumerator BITVECTOR_NOR

Bit-wise nor.

enumerator BITVECTOR_XNOR

Bit-wise xnor, left associative.

enumerator BITVECTOR_COMP

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

enumerator BITVECTOR_MULT

Multiplication of two or more bit-vectors.

enumerator BITVECTOR_ADD

Addition of two or more bit-vectors.

enumerator BITVECTOR_SUB

Subtraction of two bit-vectors.

enumerator BITVECTOR_NEG

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

enumerator BITVECTOR_UDIV

Unsigned bit-vector division.

Truncates towards 0 . If the divisor is zero, the result is all ones.

enumerator BITVECTOR_UREM

Unsigned bit-vector remainder.

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

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

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

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

enumerator BITVECTOR_SHL

Bit-vector shift left.

enumerator BITVECTOR_LSHR

Bit-vector logical shift right.

enumerator BITVECTOR_ASHR

Bit-vector arithmetic shift right.

enumerator BITVECTOR_ULT

Bit-vector unsigned less than.

enumerator BITVECTOR_ULE

Bit-vector unsigned less than or equal.

enumerator BITVECTOR_UGT

Bit-vector unsigned greater than.

enumerator BITVECTOR_UGE

Bit-vector unsigned greater than or equal.

enumerator BITVECTOR_SLT

Bit-vector signed less than.

enumerator BITVECTOR_SLE

Bit-vector signed less than or equal.

enumerator BITVECTOR_SGT

Bit-vector signed greater than.

enumerator BITVECTOR_SGE

Bit-vector signed greater than or equal.

enumerator BITVECTOR_ULTBV

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

enumerator BITVECTOR_SLTBV

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

enumerator BITVECTOR_ITE

Bit-vector if-then-else.

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

enumerator BITVECTOR_REDOR

Bit-vector redor.

enumerator BITVECTOR_REDAND

Bit-vector redand.

enumerator BITVECTOR_UADDO

Unsigned addition overflow detection.

enumerator BITVECTOR_SADDO

Signed addition overflow detection.

enumerator BITVECTOR_UMULO

Unsigned multiplication overflow detection.

enumerator BITVECTOR_SMULO

Signed multiplication overflow detection.

enumerator BITVECTOR_USUBO

Unsigned subtraction overflow detection.

enumerator BITVECTOR_SSUBO

Signed subtraction overflow detection.

enumerator BITVECTOR_SDIVO

Signed division overflow detection.

enumerator BITVECTOR_EXTRACT

Bit-vector extract.

enumerator BITVECTOR_REPEAT

Bit-vector repeat.

enumerator BITVECTOR_ZERO_EXTEND

Bit-vector zero extension.

enumerator BITVECTOR_SIGN_EXTEND

Bit-vector sign extension.

enumerator BITVECTOR_ROTATE_LEFT

Bit-vector rotate left.

enumerator BITVECTOR_ROTATE_RIGHT

Bit-vector rotate right.

enumerator INT_TO_BITVECTOR

Conversion from Int to bit-vector.

enumerator BITVECTOR_TO_NAT

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

enumerator CONST_FINITE_FIELD

Finite field constant.

enumerator FINITE_FIELD_NEG

Negation of a finite field element (additive inverse).

enumerator FINITE_FIELD_ADD

Addition of two or more finite field elements.

enumerator FINITE_FIELD_MULT

Multiplication of two or more finite field elements.

enumerator 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(uint32_t, uint32_t, Term) const

enumerator CONST_ROUNDINGMODE

RoundingMode constant.

enumerator FLOATINGPOINT_FP

Create floating-point literal from bit-vector triple.

enumerator FLOATINGPOINT_EQ

Floating-point equality.

enumerator FLOATINGPOINT_ABS

Floating-point absolute value.

enumerator FLOATINGPOINT_NEG

Floating-point negation.

enumerator FLOATINGPOINT_ADD

Floating-point addition.

enumerator FLOATINGPOINT_SUB

Floating-point sutraction.

enumerator FLOATINGPOINT_MULT

Floating-point multiply.

enumerator FLOATINGPOINT_DIV

Floating-point division.

enumerator FLOATINGPOINT_FMA

Floating-point fused multiply and add.

enumerator FLOATINGPOINT_SQRT

Floating-point square root.

enumerator FLOATINGPOINT_REM

Floating-point remainder.

enumerator FLOATINGPOINT_RTI

Floating-point round to integral.

enumerator FLOATINGPOINT_MIN

Floating-point minimum.

enumerator FLOATINGPOINT_MAX

Floating-point maximum.

enumerator FLOATINGPOINT_LEQ

Floating-point less than or equal.

enumerator FLOATINGPOINT_LT

Floating-point less than.

enumerator FLOATINGPOINT_GEQ

Floating-point greater than or equal.

enumerator FLOATINGPOINT_GT

Floating-point greater than.

enumerator FLOATINGPOINT_IS_NORMAL

Floating-point is normal tester.

enumerator FLOATINGPOINT_IS_SUBNORMAL

Floating-point is sub-normal tester.

enumerator FLOATINGPOINT_IS_ZERO

Floating-point is zero tester.

enumerator FLOATINGPOINT_IS_INF

Floating-point is infinite tester.

enumerator FLOATINGPOINT_IS_NAN

Floating-point is NaN tester.

enumerator FLOATINGPOINT_IS_NEG

Floating-point is negative tester.

enumerator FLOATINGPOINT_IS_POS

Floating-point is positive tester.

enumerator FLOATINGPOINT_TO_FP_FROM_IEEE_BV

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

enumerator FLOATINGPOINT_TO_FP_FROM_FP

Conversion to floating-point from floating-point.

enumerator FLOATINGPOINT_TO_FP_FROM_REAL

Conversion to floating-point from Real.

enumerator FLOATINGPOINT_TO_FP_FROM_SBV

Conversion to floating-point from signed bit-vector.

enumerator FLOATINGPOINT_TO_FP_FROM_UBV

Conversion to floating-point from unsigned bit-vector.

enumerator FLOATINGPOINT_TO_UBV

Conversion to unsigned bit-vector from floating-point.

enumerator FLOATINGPOINT_TO_SBV

Conversion to signed bit-vector from floating-point.

enumerator FLOATINGPOINT_TO_REAL

Conversion to Real from floating-point.

enumerator SELECT

Array select.

enumerator STORE

Array store.

enumerator CONST_ARRAY

Constant array.

enumerator EQ_RANGE

Equality over arrays \(a\) and \(b\) over a given range \([i,j]\) , i.e.,

\[\forall k . i \leq k \leq j \Rightarrow a[k] = b[k]\]

Note

We currently support the creation of array equalities over index Sorts bit-vector, floating-point, Int and Real. Requires to enable option arrays-exp .

Warning

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

enumerator APPLY_CONSTRUCTOR

Datatype constructor application.

enumerator APPLY_SELECTOR

Datatype selector application.

Note

Undefined if misapplied.

enumerator APPLY_TESTER

Datatype tester application.

enumerator APPLY_UPDATER

Datatype update application.

Note

Does not change the datatype argument if misapplied.

enumerator 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 

(match l (((cons h t) h) (nil 0)))

is represented by the AST 

(MATCH l
    (MATCH_BIND_CASE (VARIABLE_LIST h t) (cons h t) h)
    (MATCH_CASE nil 0))

Terms of kind MATCH_CASE are constant case expressions, which are used for nullary constructors. 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.

enumerator 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)

enumerator 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)

enumerator TUPLE_PROJECT

Tuple projection.

This operator takes a tuple as an argument and returns a tuple obtained by concatenating components of its argument at the provided indices.

For example, 

((_ tuple.project 1 2 2 3 1) (tuple 10 20 30 40))
yields 

(tuple 20 30 30 40 20)

enumerator SEP_NIL

Separation logic nil.

Warning

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

enumerator SEP_EMP

Separation logic empty heap.

Warning

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

enumerator SEP_PTO

Separation logic points-to relation.

Warning

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

enumerator SEP_STAR

Separation logic star.

Warning

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

enumerator SEP_WAND

Separation logic magic wand.

Warning

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

enumerator SET_EMPTY

Empty set.

enumerator SET_UNION

Set union.

enumerator SET_INTER

Set intersection.

enumerator SET_MINUS

Set subtraction.

enumerator SET_SUBSET

Subset predicate.

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

enumerator SET_MEMBER

Set membership predicate.

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

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

enumerator SET_INSERT

The set obtained by inserting elements;

enumerator SET_CARD

Set cardinality.

enumerator SET_COMPLEMENT

Set complement with respect to finite universe.

enumerator SET_UNIVERSE

Finite universe set.

All set variables must be interpreted as subsets of it.

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 .

enumerator SET_COMPREHENSION

Set comprehension

A set comprehension is specified by a variable list \(x_1 ... x_n\) , a predicate \(P[x_1...x_n]\) , and a term \(t[x_1...x_n]\) . A comprehension \(C\) with the above form has members given by the following semantics:

\[\forall y. ( \exists x_1...x_n. P[x_1...x_n] \wedge t[x_1...x_n] = y ) \Leftrightarrow (set.member \; y \; C)\]

where \(y\) ranges over the element Sort of the (set) Sort of the comprehension. If \(t[x_1..x_n]\) is not provided, it is equivalent to \(y\) in the above formula.

  • Arity: 3

    • 1: Term of Kind VARIABLE_LIST

    • 2: Term of sort Bool (the predicate of the comprehension)

    • 3: (optional) Term denoting the generator for the comprehension

Warning

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

enumerator 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\) .

Warning

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

enumerator SET_IS_SINGLETON

Set is singleton tester.

Warning

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

enumerator 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\) )

Warning

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

enumerator 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\) )

Warning

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

enumerator 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\) )

Warning

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

enumerator RELATION_JOIN

Relation join.

enumerator RELATION_PRODUCT

Relation cartesian product.

enumerator RELATION_TRANSPOSE

Relation transpose.

enumerator RELATION_TCLOSURE

Relation transitive closure.

enumerator RELATION_JOIN_IMAGE

Relation join image.

Warning

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

enumerator RELATION_IDEN

Relation identity.

Warning

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

enumerator 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

Warning

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

enumerator 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

Warning

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

enumerator RELATION_PROJECT

Relation projection operator extends tuple projection operator to sets.

Warning

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

enumerator BAG_EMPTY

Empty bag.

enumerator BAG_UNION_MAX

Bag max union.

enumerator BAG_UNION_DISJOINT

Bag disjoint union (sum).

enumerator BAG_INTER_MIN

Bag intersection (min).

enumerator BAG_DIFFERENCE_SUBTRACT

Bag difference subtract.

Subtracts multiplicities of the second from the first.

enumerator BAG_DIFFERENCE_REMOVE

Bag difference remove.

Removes shared elements in the two bags.

enumerator BAG_SUBBAG

Bag inclusion predicate.

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

enumerator BAG_COUNT

Bag element multiplicity.

enumerator BAG_MEMBER

Bag membership predicate.

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

Warning

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

enumerator BAG_MAKE

Bag make.

Construct a bag with the given element and given multiplicity.

enumerator BAG_CARD

Bag cardinality.

Warning

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

enumerator 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\) .

Warning

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

enumerator BAG_IS_SINGLETON

Bag is singleton tester.

Warning

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

enumerator BAG_FROM_SET

Conversion from set to bag.

Warning

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

enumerator BAG_TO_SET

Conversion from bag to set.

Warning

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

enumerator 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\) )

Warning

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

enumerator 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\) )

Warning

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

enumerator 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\) )

Warning

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

enumerator 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\) )

Warning

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

enumerator TABLE_PRODUCT

Table cross product.

Warning

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

enumerator TABLE_PROJECT

Table projection operator extends tuple projection operator to tables.

Warning

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

enumerator 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

Warning

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

enumerator 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

Warning

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

enumerator 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

Warning

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

enumerator STRING_CONCAT

String concat.

enumerator STRING_IN_REGEXP

String membership.

enumerator STRING_LENGTH

String length.

enumerator 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\) )

enumerator 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\) )

enumerator 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\) )

enumerator 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\) )

enumerator 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\) )

enumerator 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\) )

enumerator 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\) )

enumerator 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\) )

enumerator 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\) )

enumerator 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\) )

enumerator STRING_TO_LOWER

String to lower case.

enumerator STRING_TO_UPPER

String to upper case.

enumerator STRING_REV

String reverse.

enumerator STRING_TO_CODE

String to code.

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

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

enumerator 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\) )

enumerator 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\) )

enumerator 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\) )

enumerator 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\) )

enumerator STRING_IS_DIGIT

String is-digit.

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

enumerator STRING_FROM_INT

Conversion from Int to String.

If the integer is negative this operator returns the empty string.

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

enumerator CONST_STRING

Constant string.

enumerator STRING_TO_REGEXP

Conversion from string to regexp.

enumerator REGEXP_CONCAT

Regular expression concatenation.

enumerator REGEXP_UNION

Regular expression union.

enumerator REGEXP_INTER

Regular expression intersection.

enumerator REGEXP_DIFF

Regular expression difference.

enumerator REGEXP_STAR

Regular expression *.

enumerator REGEXP_PLUS

Regular expression +.

enumerator REGEXP_OPT

Regular expression ?.

enumerator REGEXP_RANGE

Regular expression range.

enumerator REGEXP_REPEAT

Operator for regular expression repeat.

enumerator REGEXP_LOOP

Regular expression loop.

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

enumerator REGEXP_NONE

Regular expression none.

enumerator REGEXP_ALL

Regular expression all.

enumerator REGEXP_ALLCHAR

Regular expression all characters.

enumerator REGEXP_COMPLEMENT

Regular expression complement.

enumerator SEQ_CONCAT

Sequence concat.

enumerator SEQ_LENGTH

Sequence length.

enumerator 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\) )

enumerator 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\) )

enumerator 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\) )

enumerator 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\) )

enumerator 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\) )

enumerator 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\) )

enumerator 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\) )

enumerator SEQ_REV

Sequence reverse.

enumerator 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\) )

enumerator 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\) )

enumerator CONST_SEQUENCE

Constant sequence.

A constant sequence is a term that is equivalent to: 

(seq.++ (seq.unit c1) ... (seq.unit cn))

where \(n \leq 0\) and \(c_1, ..., c_n\) are constants of some sort. The elements can be extracted with Term::getSequenceValue().

enumerator SEQ_UNIT

Sequence unit.

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

enumerator 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\) )

enumerator FORALL

Universally quantified formula.

enumerator EXISTS

Existentially quantified formula.

enumerator VARIABLE_LIST

Variable list.

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

enumerator INST_PATTERN

Instantiation pattern.

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

Note

Should only be used as a child of INST_PATTERN_LIST .

enumerator INST_NO_PATTERN

Instantiation no-pattern.

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

Note

Should only be used as a child of INST_PATTERN_LIST .

enumerator INST_POOL

Instantiation pool annotation.

Specifies an annotation for pool based instantiation.

In detail, pool symbols can be declared via the method

A pool symbol represents a set of terms of a given sort. An instantiation pool annotation should either: (1) have child sets matching the types of the quantified formula, (2) have a child set of tuple type whose component types match the types of the quantified formula.

For an example of (1), for a quantified formula: 

(FORALL (VARIABLE_LIST x y) F (INST_PATTERN_LIST (INST_POOL p q)))

if \(x\) and \(y\) have Sorts \(S_1\) and \(S_2\) , then pool symbols \(p\) and \(q\) should have Sorts (Set \(S_1\) ) and (Set \(S_2\) ), respectively. This annotation specifies that the quantified formula above should be instantiated with the product of all terms that occur in the sets \(p\) and \(q\) .

Alternatively, as an example of (2), for a quantified formula: 

(FORALL (VARIABLE_LIST x y) F (INST_PATTERN_LIST (INST_POOL s)))

\(s\) should have Sort (Set (Tuple \(S_1\) \(S_2\) )). This annotation specifies that the quantified formula above should be instantiated with the pairs of values in \(s\) .

  • Arity: n > 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, const std::vector<Term>&) const

    • Solver::mkTerm(const Op&, const std::vector<Term>&) const

  • Create Op of this kind with:

    • Solver::mkOp(Kind, const std::vector<uint32_t>&) const

verbatim embed:rst:leading-asterisk .. warning:: This kind is experimental and may be changed or removed in

future versions.

Note

Should only be used as a child of INST_PATTERN_LIST .

enumerator 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: 

(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\) .

Note

Should only be used as a child of INST_PATTERN_LIST .

Warning

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

enumerator 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: 

(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\) .

Note

Should only be used as a child of INST_PATTERN_LIST .

Warning

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

enumerator INST_ATTRIBUTE

Instantiation attribute.

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

Note

Should only be used as a child of INST_PATTERN_LIST .

enumerator INST_PATTERN_LIST

A list of instantiation patterns, attributes or annotations.

enumerator LAST_KIND

Marks the upper-bound of this enumeration.

template < >
struct hash < cvc5 :: Kind >

Hash function for Kinds.

Public Functions

size_t operator () ( cvc5 :: Kind k ) const

Hashes a Kind to a size_t.