Kind
Every
Term
has an associated kind, represented
as enum class
cvc5::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
class
cvc5
::
Kind
:
int32_t
-
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
-
-
-
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.
-
Arity:
n > 0
-
1..n:
Terms with same sorts
-
-
Create Term of this Kind with:
-
Create Op of this kind with:
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
NOT
-
Logical negation.
-
enumerator
AND
-
Logical conjunction.
-
enumerator
IMPLIES
-
Logical implication.
-
enumerator
OR
-
Logical disjunction.
-
enumerator
XOR
-
Logical exclusive disjunction, left associative.
-
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.
-
Create Term of this Kind with:
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
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
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.
-
Create Term of this Kind with:
Note
PI
is considered a special symbol of Sort Real, but is not a Real value, i.e.,Term::isRealValue()
will returnfalse
. -
-
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_NEGO
-
Bit-vector negation overflow detection.
-
enumerator
BITVECTOR_UADDO
-
Bit-vector unsigned addition overflow detection.
-
enumerator
BITVECTOR_SADDO
-
Bit-vector signed addition overflow detection.
-
enumerator
BITVECTOR_UMULO
-
Bit-vector unsigned multiplication overflow detection.
-
enumerator
BITVECTOR_SMULO
-
Bit-vector signed multiplication overflow detection.
-
enumerator
BITVECTOR_USUBO
-
Bit-vector unsigned subtraction overflow detection.
-
enumerator
BITVECTOR_SSUBO
-
Bit-vector signed subtraction overflow detection.
-
enumerator
BITVECTOR_SDIVO
-
Bit-vector 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
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_BITSUM
-
Bitsum of two or more finite field elements: x + 2y + 4z + …
-
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
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.
-
Arity:
n > 0
-
1:
DatatypeConstructor Term (see DatatypeConstructor::getTerm() const ) -
2..n:
Terms of the Sorts of the selectors of the constructor (the arguments to the constructor)
-
-
Create Term of this Kind with:
-
Create Op of this kind with:
-
-
enumerator
APPLY_SELECTOR
-
Datatype selector application.
-
Arity:
2
-
Create Term of this Kind with:
-
Create Op of this kind with:
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. KindMATCH_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 kindMATCH_CASE
andMATCH_BIND_CASE
-
-
-
enumerator
MATCH_CASE
-
Match case for nullary constructors.
A (constant) case expression to be used within a match expression.
-
Arity:
2
-
1:
Term of kindAPPLY_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 kindVARIABLE_LIST
(containing the free variable of the case) -
2:
Term of kindVARIABLE
(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 kindVARIABLE_LIST
(containing the free variable of the case) -
2:
Term of kindAPPLY_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))
(tuple 20 30 30 40 20)
-
enumerator
SEP_NIL
-
Separation logic nil.
-
Create Term of this Kind with:
Warning
This kind is experimental and may be changed or removed in future versions.
-
-
enumerator
SEP_EMP
-
Separation logic empty heap.
-
Create Term of this Kind with:
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.
-
Arity:
n > 1
-
1..n:
Terms of sort Bool (the child constraints that hold in disjoint (separated) heaps)
-
-
Create Term of this Kind with:
-
Create Op of this kind with:
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_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.
-
Create Term of this Kind with:
Note
SET_UNIVERSE
is considered a special symbol of the theory of sets and is not considered as a set value, i.e., Term::isSetValue() will returnfalse
. -
-
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 KindVARIABLE_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\) )
-
-
Create Term of this Kind with:
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\) )
-
-
Create Term of this Kind with:
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
-
-
Create Term of this Kind with:
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.
-
Arity:
1
-
Indices:
n
-
1..n:
Indices of the projection
-
-
Create Term of this Kind with:
-
Create Op of this kind with:
Warning
This kind is experimental and may be changed or removed in future versions.
-
-
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.
-
Create Term of this Kind with:
-
Solver::mkTerm(Kind, const Term&, const Term&) const
-
-
-
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\) )
-
-
Create Term of this Kind with:
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\) )
-
-
Create Term of this Kind with:
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\) )
-
-
Create Term of this Kind with:
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.
-
Arity:
1
-
Indices:
n
-
1..n:
Indices of the projection
-
-
Create Term of this Kind with:
-
Create Op of this kind with:
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
-
-
Create Term of this Kind with:
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
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_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().
-
Create Term of this Kind with:
-
-
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.
-
Arity:
3
-
1:
Term of KindVARIABLE_LIST
-
2:
Term of Sort Bool (the quantifier body) -
3:
(optional) Term of KindINST_PATTERN
-
-
-
enumerator
EXISTS
-
Existentially quantified formula.
-
Arity:
3
-
1:
Term of KindVARIABLE_LIST
-
2:
Term of Sort Bool (the quantifier body) -
3:
(optional) Term of KindINST_PATTERN
-
-
-
enumerator
VARIABLE_LIST
-
Variable list.
A list of variables (used to bind variables under a quantifier)
-
Arity:
n > 0
-
1..n:
Terms of KindVARIABLE
-
-
-
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.
-
Arity:
n > 0
-
1:
Term of Kind :cpp:enumerator:CONST_STRING
(the keyword of the attribute) -
2...n:
Terms representing the values of the attribute
-
-
Create Term of this Kind with:
-
Create Op of this kind with:
Note
Should only be used as a child of
INST_PATTERN_LIST
. -
-
enumerator
INST_PATTERN_LIST
-
A list of instantiation patterns, attributes or annotations.
-
Arity:
n > 1
-
1..n:
Terms of KindINST_PATTERN
,INST_NO_PATTERN
,INST_POOL
,INST_ADD_TO_POOL
,SKOLEM_ADD_TO_POOL
,INST_ATTRIBUTE
-
-
-
enumerator
LAST_KIND
-
Marks the upper-bound of this enumeration.
-
enumerator
INTERNAL_KIND
-
std
::
ostream
&
cvc5
::
operator
<<
(
std
::
ostream
&
out
,
Kind
kind
)
-
Serialize a kind to given stream.
- Parameters :
-
-
out – The output stream.
-
kind – The kind to be serialized to the given output stream.
-
- Returns :
-
The output stream.