Cvc5Kind

Every Cvc5Term has an associated kind, represented as enum Cvc5Kind. 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 CVC5_KIND_CONST_BITVECTOR, a free constant symbol has kind CVC5_KIND_CONSTANT, an equality over terms of any sort has kind CVC5_KIND_EQUAL, and a universally quantified formula has kind CVC5_KIND_FORALL.

enum Cvc5Kind

The kind of a cvc5 Term.

Values:

enumerator CVC5_KIND_INTERNAL_KIND

Internal kind.

This kind serves as an abstraction for internal kinds that are not exposed via the API but may appear in terms returned by API functions, e.g., when querying the simplified form of a term.

Note

Should never be created via the API.

enumerator CVC5_KIND_UNDEFINED_KIND: Undefined kind.

Note

Should never be exposed or created via the API.

enumerator CVC5_KIND_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 CVC5_KIND_UNINTERPRETED_SORT_VALUE: The value of an uninterpreted constant.

Note

May be returned as the result of an API call, but terms of this kind may not be created explicitly via the API and may not appear in assertions.

enumerator CVC5_KIND_EQUAL

Equality, chainable.

Arity: n > 1
- 1..n: Terms of the same Sort
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

enumerator CVC5_KIND_DISTINCT

Disequality.

Arity: n > 1
- 1..n: Terms of the same Sort
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

enumerator CVC5_KIND_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 CVC5_KIND_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 CVC5_KIND_SKOLEM

A Skolem.

skolem is available via the calls Solver::getSkolemId and Solver::getSkolemIndices.

Note

Represents an internally generated term. Information on the

enumerator CVC5_KIND_SEXPR

Symbolic expression.

Arity: n > 0
- 1..n: Terms with same sorts
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

Warning

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

enumerator CVC5_KIND_LAMBDA

Lambda expression.

Arity: 2
- 1: Term of kind :cpp:enumerator:VARIABLE_LIST
- 2: Term of any Sort (the body of the lambda)
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

enumerator CVC5_KIND_WITNESS

Witness.

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

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

Arity: 3
- 1: Term of kind :cpp:enumerator:VARIABLE_LIST
- 2: Term of Sort Bool (the body of the witness)
- 3: (optional) Term of kind :cpp:enumerator:INST_PATTERN_LIST
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

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 CVC5_KIND_CONST_BOOLEAN

Boolean constant.

Create Term of this Kind with:
- Solver::mkTrue() const
- Solver::mkFalse() const
- Solver::mkBoolean(bool) const

enumerator CVC5_KIND_NOT

Logical negation.

Arity: 1
- 1: Term of Sort Bool
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

enumerator CVC5_KIND_AND

Logical conjunction.

Arity: n > 1
- 1..n: Terms of Sort Bool
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

enumerator CVC5_KIND_IMPLIES

Logical implication.

Arity: n > 1
- 1..n: Terms of Sort Bool
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

enumerator CVC5_KIND_OR

Logical disjunction.

Arity: n > 1
- 1..n: Terms of Sort Bool
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

enumerator CVC5_KIND_XOR

Logical exclusive disjunction, left associative.

Arity: n > 1
- 1..n: Terms of Sort Bool
Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_ITE

If-then-else.

Arity: 3
- 1: Term of Sort Bool
- 2: The ‘then’ term, Term of any Sort
- 3: The ‘else’ term, Term of the same sort as second argument
Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_APPLY_UF

Application of an uninterpreted function.

Arity: n > 1
- 1: Function Term
- 2..n: Function argument instantiation Terms of any first-class Sort
Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_CARDINALITY_CONSTRAINT

Cardinality constraint on uninterpreted sort.

Interpreted as a predicate that is true when the cardinality of uinterpreted Sort \(S\) is less than or equal to an upper bound.

Create Term of this Kind with:
- Solver::mkCardinalityConstraint(const Sort&, uint32_t) const

Warning

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

enumerator CVC5_KIND_HO_APPLY

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

Arity: n = 2
- 1: Function Term
- 2: Argument Term of the domain Sort of the function
Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_ADD

Arithmetic addition.

Arity: n > 1
- 1..n: Terms of Sort Int or Real (sorts must match)
Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_MULT

Arithmetic multiplication.

Arity: n > 1
- 1..n: Terms of Sort Int or Real (sorts must match)
Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

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

Create Term of this Kind with:
- Solver::mkTerm(const Op&, const std::vector<Term>&) const
Create Op of this kind with:
- Solver::mkOp(Kind, const std::vector<uint32_t>&) const

enumerator CVC5_KIND_POW2

Power of two.

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

Arity: 1
- 1: Term of Sort Int
Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_SUB

Arithmetic subtraction, left associative.

Arity: n > 1
- 1..n: Terms of Sort Int or Real (sorts must match)
Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_NEG

Arithmetic negation.

Arity: 1
- 1: Term of Sort Int or Real
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

enumerator CVC5_KIND_DIVISION

Real division, division by 0 undefined, left associative.

Arity: n > 1
- 1..n: Terms of Sort Real
Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_DIVISION_TOTAL

Real division, division by 0 defined to be 0, left associative.

Arity: n > 1
- 1..n: Terms of Sort Real
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

Warning

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

enumerator CVC5_KIND_INTS_DIVISION

Integer division, division by 0 undefined, left associative.

Arity: n > 1
- 1..n: Terms of Sort Int
Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_INTS_DIVISION_TOTAL

Integer division, division by 0 defined to be 0, left associative.

Arity: n > 1
- 1..n: Terms of Sort Int
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

Warning

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

enumerator CVC5_KIND_INTS_MODULUS

Integer modulus, modulus by 0 undefined.

Arity: 2
- 1: Term of Sort Int
- 2: Term of Sort Int
Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_INTS_MODULUS_TOTAL

Integer modulus, t modulus by 0 defined to be t.

Arity: 2
- 1: Term of Sort Int
- 2: Term of Sort Int
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

Warning

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

enumerator CVC5_KIND_ABS

Absolute value.

Arity: 1
- 1: Term of Sort Int or Real
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

enumerator CVC5_KIND_POW

Arithmetic power.

Arity: 2
- 1..2: Term of Sort Int or Real (sorts must match)
Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_EXPONENTIAL

Exponential function.

Arity: 1
- 1: Term of Sort Real
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

enumerator CVC5_KIND_SINE

Sine function.

Arity: 1
- 1: Term of Sort Real
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

enumerator CVC5_KIND_COSINE

Cosine function.

Arity: 1
- 1: Term of Sort Real
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

enumerator CVC5_KIND_TANGENT

Tangent function.

Arity: 1
- 1: Term of Sort Real
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

enumerator CVC5_KIND_COSECANT

Cosecant function.

Arity: 1
- 1: Term of Sort Real
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

enumerator CVC5_KIND_SECANT

Secant function.

Arity: 1
- 1: Term of Sort Real
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

enumerator CVC5_KIND_COTANGENT

Cotangent function.

Arity: 1
- 1: Term of Sort Real
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

enumerator CVC5_KIND_ARCSINE

Arc sine function.

Arity: 1
- 1: Term of Sort Real
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

enumerator CVC5_KIND_ARCCOSINE

Arc cosine function.

Arity: 1
- 1: Term of Sort Real
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

enumerator CVC5_KIND_ARCTANGENT

Arc tangent function.

Arity: 1
- 1: Term of Sort Real
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

enumerator CVC5_KIND_ARCCOSECANT

Arc cosecant function.

Arity: 1
- 1: Term of Sort Real
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

enumerator CVC5_KIND_ARCSECANT

Arc secant function.

Arity: 1
- 1: Term of Sort Real
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

enumerator CVC5_KIND_ARCCOTANGENT

Arc cotangent function.

Arity: 1
- 1: Term of Sort Real
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

enumerator CVC5_KIND_SQRT

Square root.

If the argument x is non-negative, then this returns a non-negative value y such that y * y = x.

Arity: 1
- 1: Term of Sort Real
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

enumerator CVC5_KIND_DIVISIBLE

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

Arity: 1
- 1: Term of Sort Int
Indices: 1
- 1: The integer \(k\) to divide by.

Create Term of this Kind with:
- Solver::mkTerm(const Op&, const std::vector<Term>&) const
Create Op of this kind with:
- Solver::mkOp(Kind, const std::vector<uint32_t>&) const

enumerator CVC5_KIND_CONST_RATIONAL

Arbitrary-precision rational constant.

Create Term of this Kind with:
- Solver::mkReal(const std::string&) const
- Solver::mkReal(int64_t) const
- Solver::mkReal(int64_t, int64_t) const

enumerator CVC5_KIND_CONST_INTEGER

Arbitrary-precision integer constant.

Create Term of this Kind with:
- Solver::mkInteger(const std::string&) const
- Solver::mkInteger(int64_t) const

enumerator CVC5_KIND_LT

Less than, chainable.

Arity: n > 1
- 1..n: Terms of Sort Int or Real (sorts must match)
Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_LEQ

Less than or equal, chainable.

Arity: n > 1
- 1..n: Terms of Sort Int or Real (sorts must match)
Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_GT

Greater than, chainable.

Arity: n > 1
- 1..n: Terms of Sort Int or Real (sorts must match)
Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_GEQ

Greater than or equal, chainable.

Arity: n > 1
- 1..n: Terms of Sort Int or Real (sorts must match)
Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_IS_INTEGER

Is-integer predicate.

Arity: 1
- 1: Term of Sort Int or Real
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

enumerator CVC5_KIND_TO_INTEGER

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

Arity: 1
- 1: Term of Sort Int or Real
Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_TO_REAL

Convert Term of Sort Int or Real to Real.

Arity: 1
- 1: Term of Sort Int or Real
Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_PI

Pi constant.

Create Term of this Kind with:
- Solver::mkPi() const

Note

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

enumerator CVC5_KIND_CONST_BITVECTOR

Fixed-size bit-vector constant.

Create Term of this Kind with:
- Solver::mkBitVector(uint32_t, uint64_t) const
- Solver::mkBitVector(uint32_t, const std::string&, uint32_t) const

enumerator CVC5_KIND_BITVECTOR_CONCAT

Concatenation of two or more bit-vectors.

Arity: n > 1
- 1..n: Terms of bit-vector Sort (sorts must match)
Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_BITVECTOR_AND

Bit-wise and.

Arity: n > 1
- 1..n: Terms of bit-vector Sort (sorts must match)
Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_BITVECTOR_OR

Bit-wise or.

Arity: n > 1
- 1..n: Terms of bit-vector Sort (sorts must match)
Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_BITVECTOR_XOR

Bit-wise xor.

Arity: n > 1
- 1..n: Terms of bit-vector Sort (sorts must match)
Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_BITVECTOR_NOT

Bit-wise negation.

Arity: 1
- 1: Term of bit-vector Sort
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

enumerator CVC5_KIND_BITVECTOR_NAND

Bit-wise nand.

Arity: 2
- 1..2: Terms of bit-vector Sort (sorts must match)
Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_BITVECTOR_NOR

Bit-wise nor.

Arity: 2
- 1..2: Terms of bit-vector Sort (sorts must match)
Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_BITVECTOR_XNOR

Bit-wise xnor, left associative.

Arity: 2
- 1..2: Terms of bit-vector Sort (sorts must match)
Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_BITVECTOR_COMP

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

Arity: 2
- 1..2: Terms of bit-vector Sort (sorts must match)
Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_BITVECTOR_MULT

Multiplication of two or more bit-vectors.

Arity: n > 1
- 1..n: Terms of bit-vector Sort (sorts must match)
Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_BITVECTOR_ADD

Addition of two or more bit-vectors.

Arity: n > 1
- 1..n: Terms of bit-vector Sort (sorts must match)
Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_BITVECTOR_SUB

Subtraction of two bit-vectors.

Arity: n > 1
- 1..n: Terms of bit-vector Sort (sorts must match)
Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_BITVECTOR_NEG

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

Arity: 1
- 1: Term of bit-vector Sort
Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_BITVECTOR_UDIV

Unsigned bit-vector division.

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

Arity: 2
- 1..2: Terms of bit-vector Sort (sorts must match)
Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_BITVECTOR_UREM

Unsigned bit-vector remainder.

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

Arity: 2
- 1..2: Terms of bit-vector Sort (sorts must match)
Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_BITVECTOR_SDIV

Signed bit-vector division.

Two’s complement signed division of two bit-vectors. If the divisor is zero and the dividend is positive, the result is all ones. If the divisor is zero and the dividend is negative, the result is one.

Arity: 2
- 1..2: Terms of bit-vector Sort (sorts must match)
Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_BITVECTOR_SREM

Signed bit-vector remainder (sign follows dividend).

Two’s complement signed remainder of two bit-vectors where the sign follows the dividend. If the modulus is zero, the result is the dividend.

Arity: 2
- 1..2: Terms of bit-vector Sort (sorts must match)
Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_BITVECTOR_SMOD

Signed bit-vector remainder (sign follows divisor).

Two’s complement signed remainder where the sign follows the divisor. If the modulus is zero, the result is the dividend.

Arity: 2
- 1..2: Terms of bit-vector Sort (sorts must match)
Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_BITVECTOR_SHL

Bit-vector shift left.

Arity: 2
- 1..2: Terms of bit-vector Sort (sorts must match)
Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_BITVECTOR_LSHR

Bit-vector logical shift right.

Arity: 2
- 1..2: Terms of bit-vector Sort (sorts must match)
Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_BITVECTOR_ASHR

Bit-vector arithmetic shift right.

Arity: 2
- 1..2: Terms of bit-vector Sort (sorts must match)
Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_BITVECTOR_ULT

Bit-vector unsigned less than.

Arity: 2
- 1..2: Terms of bit-vector Sort (sorts must match)
Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_BITVECTOR_ULE

Bit-vector unsigned less than or equal.

Arity: 2
- 1..2: Terms of bit-vector Sort (sorts must match)
Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_BITVECTOR_UGT

Bit-vector unsigned greater than.

Arity: 2
- 1..2: Terms of bit-vector Sort (sorts must match)
Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_BITVECTOR_UGE

Bit-vector unsigned greater than or equal.

Arity: 2
- 1..2: Terms of bit-vector Sort (sorts must match)
Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_BITVECTOR_SLT

Bit-vector signed less than.

Arity: 2
- 1..2: Terms of bit-vector Sort (sorts must match)
Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_BITVECTOR_SLE

Bit-vector signed less than or equal.

Arity: 2
- 1..2: Terms of bit-vector Sort (sorts must match)
Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_BITVECTOR_SGT

Bit-vector signed greater than.

Arity: 2
- 1..2: Terms of bit-vector Sort (sorts must match)
Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_BITVECTOR_SGE

Bit-vector signed greater than or equal.

Arity: 2
- 1..2: Terms of bit-vector Sort (sorts must match)
Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_BITVECTOR_ULTBV

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

Arity: 2
- 1..2: Terms of bit-vector Sort (sorts must match)
Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_BITVECTOR_SLTBV

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

Arity: 2
- 1..2: Terms of bit-vector Sort (sorts must match)
Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_BITVECTOR_ITE

Bit-vector if-then-else.

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

Arity: 3
- 1: Term of bit-vector Sort of size 1
- 1..3: Terms of bit-vector sort (sorts must match)
Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_BITVECTOR_REDOR

Bit-vector redor.

Arity: 1
- 1: Term of bit-vector Sort
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

enumerator CVC5_KIND_BITVECTOR_REDAND

Bit-vector redand.

Arity: 1
- 1: Term of bit-vector Sort
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

enumerator CVC5_KIND_BITVECTOR_NEGO

Bit-vector negation overflow detection.

Arity: 1
- 1: Term of bit-vector Sort
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

enumerator CVC5_KIND_BITVECTOR_UADDO

Bit-vector unsigned addition overflow detection.

Arity: 2
- 1..2: Terms of bit-vector Sort (sorts must match)
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

enumerator CVC5_KIND_BITVECTOR_SADDO

Bit-vector signed addition overflow detection.

Arity: 2
- 1..2: Terms of bit-vector Sort (sorts must match)
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

enumerator CVC5_KIND_BITVECTOR_UMULO

Bit-vector unsigned multiplication overflow detection.

Arity: 2
- 1..2: Terms of bit-vector Sort (sorts must match)
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

enumerator CVC5_KIND_BITVECTOR_SMULO

Bit-vector signed multiplication overflow detection.

Arity: 2
- 1..2: Terms of bit-vector Sort (sorts must match)
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

enumerator CVC5_KIND_BITVECTOR_USUBO

Bit-vector unsigned subtraction overflow detection.

Arity: 2
- 1..2: Terms of bit-vector Sort (sorts must match)
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

enumerator CVC5_KIND_BITVECTOR_SSUBO

Bit-vector signed subtraction overflow detection.

Arity: 2
- 1..2: Terms of bit-vector Sort (sorts must match)
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

enumerator CVC5_KIND_BITVECTOR_SDIVO

Bit-vector signed division overflow detection.

Arity: 2
- 1..2: Terms of bit-vector Sort (sorts must match)
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

enumerator CVC5_KIND_BITVECTOR_EXTRACT

Bit-vector extract.

Arity: 1
- 1: Term of bit-vector Sort
Indices: 2
- 1: The upper bit index.
- 2: The lower bit index.
Create Term of this Kind with:
- Solver::mkTerm(const Op&, const std::vector<Term>&) const
Create Op of this kind with:
- Solver::mkOp(Kind, const std::vector<uint32_t>&) const

enumerator CVC5_KIND_BITVECTOR_REPEAT

Bit-vector repeat.

Arity: 1
- 1: Term of bit-vector Sort
Indices: 1
- 1: The number of times to repeat the given term.
Create Term of this Kind with:
- Solver::mkTerm(const Op&, const std::vector<Term>&) const
Create Op of this kind with:
- Solver::mkOp(Kind, const std::vector<uint32_t>&) const

enumerator CVC5_KIND_BITVECTOR_ZERO_EXTEND

Bit-vector zero extension.

Arity: 1
- 1: Term of bit-vector Sort
Indices: 1
- 1: The number of zeroes to extend the given term with.
Create Term of this Kind with:
- Solver::mkTerm(const Op&, const std::vector<Term>&) const
Create Op of this kind with:
- Solver::mkOp(Kind, const std::vector<uint32_t>&) const

enumerator CVC5_KIND_BITVECTOR_SIGN_EXTEND

Bit-vector sign extension.

Arity: 1
- 1: Term of bit-vector Sort
Indices: 1
- 1: The number of bits (of the value of the sign bit) to extend the given term with.
Create Term of this Kind with:
- Solver::mkTerm(const Op&, const std::vector<Term>&) const
Create Op of this kind with:
- Solver::mkOp(Kind, const std::vector<uint32_t>&) const

enumerator CVC5_KIND_BITVECTOR_ROTATE_LEFT

Bit-vector rotate left.

Arity: 1
- 1: Term of bit-vector Sort
Indices: 1
- 1: The number of bits to rotate the given term left.
Create Term of this Kind with:
- Solver::mkTerm(const Op&, const std::vector<Term>&) const
Create Op of this kind with:
- Solver::mkOp(Kind, const std::vector<uint32_t>&) const

enumerator CVC5_KIND_BITVECTOR_ROTATE_RIGHT

Bit-vector rotate right.

Arity: 1
- 1: Term of bit-vector Sort
Indices: 1
- 1: The number of bits to rotate the given term right.
Create Term of this Kind with:
- Solver::mkTerm(const Op&, const std::vector<Term>&) const
Create Op of this kind with:
- Solver::mkOp(Kind, const std::vector<uint32_t>&) const

enumerator CVC5_KIND_INT_TO_BITVECTOR

Conversion from Int to bit-vector.

Arity: 1
- 1: Term of Sort Int
Indices: 1
- 1: The size of the bit-vector to convert to.
Create Term of this Kind with:
- Solver::mkTerm(const Op&, const std::vector<Term>&) const
Create Op of this kind with:
- Solver::mkOp(Kind, const std::vector<uint32_t>&) const

enumerator CVC5_KIND_BITVECTOR_TO_NAT

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

Arity: 1
- 1: Term of bit-vector Sort
Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_BITVECTOR_FROM_BOOLS

Converts a list of Bool terms to a bit-vector.

Arity: n > 0
- 1..n: Terms of Sort Bool

Note

May be returned as the result of an API call, but terms of this kind may not be created explicitly via the API and may not appear in assertions.

enumerator CVC5_KIND_BITVECTOR_BIT

Retrieves the bit at the given index from a bit-vector as a Bool term.

Arity: 1
- 1: Term of bit-vector Sort
Indices: 1
- 1: The bit index

Note

May be returned as the result of an API call, but terms of this kind may not be created explicitly via the API and may not appear in assertions.

enumerator CVC5_KIND_CONST_FINITE_FIELD

Finite field constant.

Create Term of this Kind with:
- Solver::mkFiniteFieldElem(const std::string&, const Sort&, uint32_t base) const

enumerator CVC5_KIND_FINITE_FIELD_NEG

Negation of a finite field element (additive inverse).

Arity: 1
- 1: Term of finite field Sort
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

enumerator CVC5_KIND_FINITE_FIELD_ADD

Addition of two or more finite field elements.

Arity: n > 1
- 1..n: Terms of finite field Sort (sorts must match)
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

enumerator CVC5_KIND_FINITE_FIELD_BITSUM

Bitsum of two or more finite field elements: x + 2y + 4z + …

Arity: n > 1
- 1..n: Terms of finite field Sort (sorts must match)
Create Term of this Kind with:
- Solver::mkTerm(Kind, const std::vector<Term>&) const
- Solver::mkTerm(const Op&, const std::vector<Term>&) const

enumerator CVC5_KIND_FINITE_FIELD_MULT

Multiplication of two or more finite field elements.

Arity: n > 1
- 1..n: Terms of finite field Sort (sorts must match)
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

enumerator CVC5_KIND_CONST_FLOATINGPOINT

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

Create Term of this Kind with:
- Solver::mkFloatingPoint(uint32_t, uint32_t, Term) const

enumerator CVC5_KIND_CONST_ROUNDINGMODE

RoundingMode constant.

Create Term of this Kind with:
- Solver::mkRoundingMode(RoundingMode) const

enumerator CVC5_KIND_FLOATINGPOINT_FP

Create floating-point literal from bit-vector triple.

Arity: 3
- 1: Term of bit-vector Sort of size 1 (sign bit)
- 2: Term of bit-vector Sort of exponent size (exponent)
- 3: Term of bit-vector Sort of significand size - 1 (significand without hidden bit)
Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_FLOATINGPOINT_EQ

Floating-point equality.

Arity: 2
- 1..2: Terms of floating-point Sort (sorts must match)
Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_FLOATINGPOINT_ABS

Floating-point absolute value.

Arity: 1
- 1: Term of floating-point Sort
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

enumerator CVC5_KIND_FLOATINGPOINT_NEG

Floating-point negation.

Arity: 1
- 1: Term of floating-point Sort
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

enumerator CVC5_KIND_FLOATINGPOINT_ADD

Floating-point addition.

Arity: 3
- 1: Term of Sort RoundingMode
- 2..3: Terms of floating-point Sort (sorts must match)
Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_FLOATINGPOINT_SUB

Floating-point sutraction.

Arity: 3
- 1: Term of Sort RoundingMode
- 2..3: Terms of floating-point Sort (sorts must match)
Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_FLOATINGPOINT_MULT

Floating-point multiply.

Arity: 3
- 1: Term of Sort RoundingMode
- 2..3: Terms of floating-point Sort (sorts must match)
Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_FLOATINGPOINT_DIV

Floating-point division.

Arity: 3
- 1: Term of Sort RoundingMode
- 2..3: Terms of floating-point Sort (sorts must match)
Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_FLOATINGPOINT_FMA

Floating-point fused multiply and add.

Arity: 4
- 1: Term of Sort RoundingMode
- 2..4: Terms of floating-point Sort (sorts must match)
Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_FLOATINGPOINT_SQRT

Floating-point square root.

Arity: 2
- 1: Term of Sort RoundingMode
- 2: Term of floating-point Sort
Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_FLOATINGPOINT_REM

Floating-point remainder.

Arity: 2
- 1..2: Terms of floating-point Sort (sorts must match)
Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_FLOATINGPOINT_RTI

Floating-point round to integral.

Arity: 2
- 1..2: Terms of floating-point Sort (sorts must match)
Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_FLOATINGPOINT_MIN

Floating-point minimum.

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

enumerator CVC5_KIND_FLOATINGPOINT_MAX

Floating-point maximum.

Arity: 2
- 1..2: Terms of floating-point Sort (sorts must match)
Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_FLOATINGPOINT_LEQ

Floating-point less than or equal.

Arity: 2
- 1..2: Terms of floating-point Sort (sorts must match)
Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_FLOATINGPOINT_LT

Floating-point less than.

Arity: 2
- 1..2: Terms of floating-point Sort (sorts must match)
Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_FLOATINGPOINT_GEQ

Floating-point greater than or equal.

Arity: 2
- 1..2: Terms of floating-point Sort (sorts must match)
Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_FLOATINGPOINT_GT

Floating-point greater than.

Arity: 2
- 1..2: Terms of floating-point Sort (sorts must match)
Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_FLOATINGPOINT_IS_NORMAL

Floating-point is normal tester.

Arity: 1
- 1: Term of floating-point Sort
Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_FLOATINGPOINT_IS_SUBNORMAL

Floating-point is sub-normal tester.

Arity: 1
- 1: Term of floating-point Sort
Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_FLOATINGPOINT_IS_ZERO

Floating-point is zero tester.

Arity: 1
- 1: Term of floating-point Sort
Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_FLOATINGPOINT_IS_INF

Floating-point is infinite tester.

Arity: 1
- 1: Term of floating-point Sort
Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_FLOATINGPOINT_IS_NAN

Floating-point is NaN tester.

Arity: 1
- 1: Term of floating-point Sort
Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_FLOATINGPOINT_IS_NEG

Floating-point is negative tester.

Arity: 1
- 1: Term of floating-point Sort
Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_FLOATINGPOINT_IS_POS

Floating-point is positive tester.

Arity: 1
- 1: Term of floating-point Sort
Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_FLOATINGPOINT_TO_FP_FROM_IEEE_BV

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

Arity: 1
- 1: Term of bit-vector Sort
Indices: 2
- 1: The exponent size
- 2: The significand size
Create Term of this Kind with:
- Solver::mkTerm(const Op&, const std::vector<Term>&) const
Create Op of this kind with:
- Solver::mkOp(Kind, const std::vector<uint32_t>&) const

enumerator CVC5_KIND_FLOATINGPOINT_TO_FP_FROM_FP

Conversion to floating-point from floating-point.

Arity: 2
- 1: Term of Sort RoundingMode
- 2: Term of floating-point Sort
Indices: 2
- 1: The exponent size
- 2: The significand size
Create Term of this Kind with:
- Solver::mkTerm(const Op&, const std::vector<Term>&) const
Create Op of this kind with:
- Solver::mkOp(Kind, const std::vector<uint32_t>&) const

enumerator CVC5_KIND_FLOATINGPOINT_TO_FP_FROM_REAL

Conversion to floating-point from Real.

Arity: 2
- 1: Term of Sort RoundingMode
- 2: Term of Sort Real
Indices: 2
- 1: The exponent size
- 2: The significand size
Create Term of this Kind with:
- Solver::mkTerm(const Op&, const std::vector<Term>&) const
Create Op of this kind with:
- Solver::mkOp(Kind, const std::vector<uint32_t>&) const

enumerator CVC5_KIND_FLOATINGPOINT_TO_FP_FROM_SBV

Conversion to floating-point from signed bit-vector.

Arity: 2
- 1: Term of Sort RoundingMode
- 2: Term of bit-vector Sort
Indices: 2
- 1: The exponent size
- 2: The significand size
Create Term of this Kind with:
- Solver::mkTerm(const Op&, const std::vector<Term>&) const
Create Op of this kind with:
- Solver::mkOp(Kind, const std::vector<uint32_t>&) const

enumerator CVC5_KIND_FLOATINGPOINT_TO_FP_FROM_UBV

Conversion to floating-point from unsigned bit-vector.

Arity: 2
- 1: Term of Sort RoundingMode
- 2: Term of bit-vector Sort
Indices: 2
- 1: The exponent size
- 2: The significand size
Create Term of this Kind with:
- Solver::mkTerm(const Op&, const std::vector<Term>&) const
Create Op of this kind with:
- Solver::mkOp(Kind, const std::vector<uint32_t>&) const

enumerator CVC5_KIND_FLOATINGPOINT_TO_UBV

Conversion to unsigned bit-vector from floating-point.

Arity: 2
- 1: Term of Sort RoundingMode
- 2: Term of floating-point Sort
Indices: 1
- 1: The size of the bit-vector to convert to.
Create Term of this Kind with:
- Solver::mkTerm(const Op&, const std::vector<Term>&) const
Create Op of this kind with:
- Solver::mkOp(Kind, const std::vector<uint32_t>&) const

enumerator CVC5_KIND_FLOATINGPOINT_TO_SBV

Conversion to signed bit-vector from floating-point.

Arity: 2
- 1: Term of Sort RoundingMode
- 2: Term of floating-point Sort
Indices: 1
- 1: The size of the bit-vector to convert to.
Create Term of this Kind with:
- Solver::mkTerm(const Op&, const std::vector<Term>&) const
Create Op of this kind with:
- Solver::mkOp(Kind, const std::vector<uint32_t>&) const

enumerator CVC5_KIND_FLOATINGPOINT_TO_REAL

Conversion to Real from floating-point.

Arity: 1
- 1: Term of Sort Real
Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_SELECT

Array select.

Arity: 2
- 1: Term of array Sort
- 2: Term of array index Sort
Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_STORE

Array store.

Arity: 3
- 1: Term of array Sort
- 2: Term of array index Sort
- 3: Term of array element Sort
Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_CONST_ARRAY

Constant array.

Arity: 2
- 1: Term of array Sort
- 2: Term of array element Sort (value)
Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_EQ_RANGE

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

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

Arity: 4
- 1: Term of array Sort (first array)
- 2: Term of array Sort (second array)
- 3: Term of array index Sort (lower bound of range, inclusive)
- 4: Term of array index Sort (upper bound of range, inclusive)
Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

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

enumerator CVC5_KIND_APPLY_SELECTOR

Datatype selector application.

Arity: 2
- 1: DatatypeSelector Term (see DatatypeSelector::getTerm() const)
- 2: Term of the codomain Sort of the selector
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

Note

Undefined if misapplied.

enumerator CVC5_KIND_APPLY_TESTER

Datatype tester application.

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

enumerator CVC5_KIND_APPLY_UPDATER

Datatype update application.

Arity: 3
- 1: Datatype updater Term (see DatatypeSelector::getUpdaterTerm() const)
- 2: Term of Datatype Sort (DatatypeSelector of the updater must belong to a constructor of this Datatype Sort)
- 3: Term of the codomain Sort of the selector (the Term to update the field of the datatype term with)
Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

Note

Does not change the datatype argument if misapplied.

enumerator CVC5_KIND_MATCH

Match expression.

This kind is primarily used in the parser to support the SMT-LIBv2 match expression.

For example, the SMT-LIBv2 syntax for the following match term

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

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

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

enumerator CVC5_KIND_MATCH_CASE

Match case for nullary constructors.

A (constant) case expression to be used within a match expression.

Arity: 2
- 1: Term of kind APPLY_CONSTRUCTOR (the pattern to match against)
- 2: Term of any Sort (the term the match term evaluates to)

Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_MATCH_BIND_CASE

Match case with binders, for constructors with selectors and variable patterns.

A (non-constant) case expression to be used within a match expression.

Arity: 3
- For variable patterns:
  - 1: Term of kind VARIABLE_LIST (containing the free variable of the case)
  - 2: Term of kind VARIABLE (the pattern expression, the free variable of the case)
  - 3: Term of any Sort (the term the pattern evaluates to)
- For constructors with selectors:
  - 1: Term of kind VARIABLE_LIST (containing the free variable of the case)
  - 2: Term of kind APPLY_CONSTRUCTOR (the pattern expression, applying the set of variables to the constructor)
  - 3: Term of any Sort (the term the match term evaluates to)

Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_TUPLE_PROJECT

Tuple projection.

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

For example,

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

yields

(tuple 20 30 30 40 20)

Arity: 1
- 1: Term of tuple Sort
Indices: n
- 1..n: The tuple indices to project
Create Term of this Kind with:
- Solver::mkTerm(const Op&, const std::vector<Term>&) const
Create Op of this kind with:
- Solver::mkOp(Kind, const std::vector<uint32_t>&) const

enumerator CVC5_KIND_NULLABLE_LIFT

Lifting operator for nullable terms. This operator lifts a built-in operator or a user-defined function to nullable terms. For built-in kinds use mkNullableLift. For user-defined functions use mkTerm.

Arity: n > 1
1..n: Terms of nullable sort
Create Term of this Kind with:
- Solver::mkNullableLift(Kind, const std::vector<Term>&) const
- Solver::mkTerm(Kind, const std::vector<Term>&) const

enumerator CVC5_KIND_SEP_NIL

Separation logic nil.

Create Term of this Kind with:
- Solver::mkSepNil(const Sort&) const

Warning

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

enumerator CVC5_KIND_SEP_EMP

Separation logic empty heap.

Create Term of this Kind with:
- Solver::mkSepEmp() const

Warning

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

enumerator CVC5_KIND_SEP_PTO

Separation logic points-to relation.

Arity: 2
- 1: Term denoting the location of the points-to constraint
- 2: Term denoting the data of the points-to constraint
Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

Warning

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

enumerator CVC5_KIND_SEP_STAR

Separation logic star.

Arity: n > 1
- 1..n: Terms of sort Bool (the child constraints that hold in disjoint (separated) heaps)
Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

Warning

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

enumerator CVC5_KIND_SEP_WAND

Separation logic magic wand.

Arity: 2
- 1: Terms of Sort Bool (the antecendant of the magic wand constraint)
- 2: Terms of Sort Bool (conclusion of the magic wand constraint, which is asserted to hold in all heaps that are disjoint extensions of the antecedent)
Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

Warning

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

enumerator CVC5_KIND_SET_EMPTY

Empty set.

Create Term of this Kind with:
- Solver::mkEmptySet(const Sort&) const

enumerator CVC5_KIND_SET_UNION

Set union.

Arity: 2
- 1..2: Terms of set Sort
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

enumerator CVC5_KIND_SET_INTER

Set intersection.

Arity: 2
- 1..2: Terms of set Sort
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

enumerator CVC5_KIND_SET_MINUS

Set subtraction.

Arity: 2
- 1..2: Terms of set Sort
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

enumerator CVC5_KIND_SET_SUBSET

Subset predicate.

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

Arity: 2
- 1..2: Terms of set Sort
Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_SET_MEMBER

Set membership predicate.

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

Arity: 2
- 1: Term of any Sort (must match the element Sort of the given set Term)
- 2: Term of set Sort
Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_SET_SINGLETON

Singleton set.

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

Arity: 1
- 1: Term of any Sort (the set element)
Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_SET_INSERT

The set obtained by inserting elements;

Arity: n > 0
- 1..n-1: Terms of any Sort (must match the element sort of the given set Term)
- n: Term of set Sort
Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_SET_CARD

Set cardinality.

Arity: 1
- 1: Term of set Sort
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

enumerator CVC5_KIND_SET_COMPLEMENT

Set complement with respect to finite universe.

Arity: 1
- 1: Term of set Sort
Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_SET_UNIVERSE

Finite universe set.

All set variables must be interpreted as subsets of it.

Create Term of this Kind with:
- Solver::mkUniverseSet(const Sort&) const

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 CVC5_KIND_SET_COMPREHENSION

Set comprehension

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

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

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

Arity: 3
- 1: Term of Kind VARIABLE_LIST
- 2: Term of sort Bool (the predicate of the comprehension)
- 3: (optional) Term denoting the generator for the comprehension

Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

Warning

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

enumerator CVC5_KIND_SET_CHOOSE

Set choose.

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

Arity: 1
- 1: Term of set Sort
Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

Warning

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

enumerator CVC5_KIND_SET_IS_EMPTY

Set is empty tester.

Arity: 1
- 1: Term of set Sort
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

Warning

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

enumerator CVC5_KIND_SET_IS_SINGLETON

Set is singleton tester.

Arity: 1
- 1: Term of set Sort
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

Warning

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

enumerator CVC5_KIND_SET_MAP

Set map.

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

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

Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

Warning

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

enumerator CVC5_KIND_SET_FILTER

Set filter.

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

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

Create Term of this Kind with:
- Solver::mkTerm(Kind, const std::vector<Term>&) const
- Solver::mkTerm(const Op&, const std::vector<Term>&) const

Warning

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

enumerator CVC5_KIND_SET_ALL

Set all.

This operator checks whether all elements of a set satisfy a predicate. (set.all \(p \; A\)) takes a predicate \(p\) of Sort \((\rightarrow T \; Bool)\) as a first argument, and a set \(A\) of Sort (Set \(T\)) as a second argument, and returns true iff all elements of \(A\) satisfy predicate \(p\).

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

Create Term of this Kind with:
- Solver::mkTerm(Kind, const std::vector<Term>&) const
- Solver::mkTerm(const Op&, const std::vector<Term>&) const

Warning

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

enumerator CVC5_KIND_SET_SOME

Set some.

This operator checks whether at least one element of a set satisfies a predicate. (set.some \(p \; A\)) takes a predicate \(p\) of Sort \((\rightarrow T \; Bool)\) as a first argument, and a set \(A\) of Sort (Set \(T\)) as a second argument, and returns true iff at least one element of \(A\) satisfies predicate \(p\).

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

Create Term of this Kind with:
- Solver::mkTerm(Kind, const std::vector<Term>&) const
- Solver::mkTerm(const Op&, const std::vector<Term>&) const

Warning

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

enumerator CVC5_KIND_SET_FOLD

Set fold.

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

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

Create Term of this Kind with:
- Solver::mkTerm(Kind, const std::vector<Term>&) const
- Solver::mkTerm(const Op&, const std::vector<Term>&) const

Warning

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

enumerator CVC5_KIND_RELATION_JOIN

Relation join.

Arity: 2
- 1..2: Terms of relation Sort
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

enumerator CVC5_KIND_RELATION_TABLE_JOIN

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

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

Create Term of this Kind with:
- Solver::mkTerm(const Op&, const std::vector<Term>&) const
Create Op of this kind with:
- Solver::mkOp(Kind, const std::vector<uint32_t>&) const

Warning

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

enumerator CVC5_KIND_RELATION_PRODUCT

Relation cartesian product.

Arity: 2
- 1..2: Terms of relation Sort
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

enumerator CVC5_KIND_RELATION_TRANSPOSE

Relation transpose.

Arity: 1
- 1: Term of relation Sort
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

enumerator CVC5_KIND_RELATION_TCLOSURE

Relation transitive closure.

Arity: 1
- 1: Term of relation Sort
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

enumerator CVC5_KIND_RELATION_JOIN_IMAGE

Relation join image.

Arity: 2
- 1..2: Terms of relation Sort
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

Warning

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

enumerator CVC5_KIND_RELATION_IDEN

Relation identity.

Arity: 1
- 1: Term of relation Sort
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

Warning

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

enumerator CVC5_KIND_RELATION_GROUP

Relation group

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

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

Create Term of this Kind with:
- Solver::mkTerm(Kind, const std::vector<Term>&) const
- Solver::mkTerm(const Op&, const std::vector<Term>&) const

Warning

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

enumerator CVC5_KIND_RELATION_AGGREGATE

Relation aggregate operator has the form \(((\_ \; rel.aggr \; n_1 ... n_k) \; f \; i \; A)\) where \(n_1, ..., n_k\) are natural numbers, \(f\) is a function of type \((\rightarrow (Tuple \; T_1 \; ... \; T_j)\; T \; T)\), \(i\) has the type \(T\), and \(A\) has type \((Relation \; T_1 \; ... \; T_j)\). The returned type is \((Set \; T)\).

This operator aggregates elements in A that have the same tuple projection with indices n_1, …, n_k using the combining function \(f\), and initial value \(i\).

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

Create Term of this Kind with:
- Solver::mkTerm(const Op&, const std::vector<Term>&) const
Create Op of this kind with:
- Solver::mkOp(Kind, const std::vector<uint32_t>&) const

Warning

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

enumerator CVC5_KIND_RELATION_PROJECT

Relation projection operator extends tuple projection operator to sets.

Arity: 1
- 1: Term of relation Sort
Indices: n
- 1..n: Indices of the projection
Create Term of this Kind with:
- Solver::mkTerm(const Op&, const std::vector<Term>&) const
Create Op of this kind with:
- Solver::mkOp(Kind, const std::vector<uint32_t>&) const

Warning

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

enumerator CVC5_KIND_BAG_EMPTY

Empty bag.

Create Term of this Kind with:
- Solver::mkEmptyBag(const Sort&) const

enumerator CVC5_KIND_BAG_UNION_MAX

Bag max union.

Arity: 2
- 1..2: Terms of bag Sort
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

enumerator CVC5_KIND_BAG_UNION_DISJOINT

Bag disjoint union (sum).

Arity: 2
- 1..2: Terms of bag Sort
Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_BAG_INTER_MIN

Bag intersection (min).

Arity: 2
- 1..2: Terms of bag Sort
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

enumerator CVC5_KIND_BAG_DIFFERENCE_SUBTRACT

Bag difference subtract.

Subtracts multiplicities of the second from the first.

Arity: 2
- 1..2: Terms of bag Sort
Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_BAG_DIFFERENCE_REMOVE

Bag difference remove.

Removes shared elements in the two bags.

Arity: 2
- 1..2: Terms of bag Sort
Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_BAG_SUBBAG

Bag inclusion predicate.

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

Arity: 2
- 1..2: Terms of bag Sort
Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_BAG_COUNT

Bag element multiplicity.

Create Term of this Kind with:
- Solver::mkTerm(Kind, const Term&, const Term&) const
- Solver::mkTerm(Kind, const std::vector<Term>&) const

enumerator CVC5_KIND_BAG_MEMBER

Bag membership predicate.

Arity: 2
- 1: Term of any Sort (must match the element Sort of the given bag Term)
- 2: Terms of bag Sort
Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_BAG_SETOF

Bag setof.

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

Arity: 1
- 1: Term of bag Sort
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

Warning

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

enumerator CVC5_KIND_BAG_MAKE

Bag make.

Construct a bag with the given element and given multiplicity.

Arity: 2
- 1: Term of any Sort (the bag element)
- 2: Term of Sort Int (the multiplicity of the element)
Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_BAG_CARD

Bag cardinality.

Arity: 1
- 1: Term of bag Sort
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

Warning

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

enumerator CVC5_KIND_BAG_CHOOSE

Bag choose.

Select an element from a given bag.

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

Arity: 1
- 1: Term of bag Sort
Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

Warning

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

enumerator CVC5_KIND_BAG_MAP

Bag map.

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

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

Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

Warning

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

enumerator CVC5_KIND_BAG_FILTER

Bag filter.

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

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

Create Term of this Kind with:
- Solver::mkTerm(Kind, const std::vector<Term>&) const
- Solver::mkTerm(const Op&, const std::vector<Term>&) const

Warning

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

enumerator CVC5_KIND_BAG_FOLD

Bag fold.

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

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

Create Term of this Kind with:
- Solver::mkTerm(Kind, const std::vector<Term>&) const
- Solver::mkTerm(const Op&, const std::vector<Term>&) const

Warning

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

enumerator CVC5_KIND_BAG_PARTITION

Bag partition.

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

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

Create Term of this Kind with:
- Solver::mkTerm(Kind, const std::vector<Term>&) const
- Solver::mkTerm(const Op&, const std::vector<Term>&) const

Warning

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

enumerator CVC5_KIND_TABLE_PRODUCT

Table cross product.

Arity: 2
- 1..2: Terms of table Sort
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

Warning

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

enumerator CVC5_KIND_TABLE_PROJECT

Table projection operator extends tuple projection operator to tables.

Arity: 1
- 1: Term of table Sort
Indices: n
- 1..n: Indices of the projection
Create Term of this Kind with:
- Solver::mkTerm(const Op&, const std::vector<Term>&) const
Create Op of this kind with:
- Solver::mkOp(Kind, const std::vector<uint32_t>&) const

Warning

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

enumerator CVC5_KIND_TABLE_AGGREGATE

Table aggregate operator has the form \(((\_ \; table.aggr \; n_1 ... n_k) \; f \; i \; A)\) where \(n_1, ..., n_k\) are natural numbers, \(f\) is a function of type \((\rightarrow (Tuple \; T_1 \; ... \; T_j)\; T \; T)\), \(i\) has the type \(T\), and \(A\) has type \((Table \; T_1 \; ... \; T_j)\). The returned type is \((Bag \; T)\).

This operator aggregates elements in A that have the same tuple projection with indices n_1, …, n_k using the combining function \(f\), and initial value \(i\).

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

Create Term of this Kind with:
- Solver::mkTerm(const Op&, const std::vector<Term>&) const
Create Op of this kind with:
- Solver::mkOp(Kind, const std::vector<uint32_t>&) const

Warning

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

enumerator CVC5_KIND_TABLE_JOIN

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

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

Create Term of this Kind with:
- Solver::mkTerm(const Op&, const std::vector<Term>&) const
Create Op of this kind with:
- Solver::mkOp(Kind, const std::vector<uint32_t>&) const

Warning

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

enumerator CVC5_KIND_TABLE_GROUP

Table group

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

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

Create Term of this Kind with:
- Solver::mkTerm(Kind, const std::vector<Term>&) const
- Solver::mkTerm(const Op&, const std::vector<Term>&) const

Warning

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

enumerator CVC5_KIND_STRING_CONCAT

String concat.

Arity: n > 1
- 1..n: Terms of Sort String
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

enumerator CVC5_KIND_STRING_IN_REGEXP

String membership.

Arity: 2
- 1: Term of Sort String
- 2: Term of Sort RegLan
Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_STRING_LENGTH

String length.

Arity: 1
- 1: Term of Sort String
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

enumerator CVC5_KIND_STRING_SUBSTR

String substring.

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

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

Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_STRING_UPDATE

String update.

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

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

Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_STRING_CHARAT

String character at.

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

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

Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_STRING_CONTAINS

String contains.

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

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

Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_STRING_INDEXOF

String index-of.

Returns the index of a substring \(s_2\) in a string \(s_1\) starting at index \(i\). If the index is negative or greater than the length of string \(s_1\) or the substring \(s_2\) does not appear in string \(s_1\) after index \(i\), the result is -1.

Arity: 2
- 1: Term of Sort String (substring \(s_1\))
- 2: Term of Sort String (substring \(s_2\))
- 3: Term of Sort Int (index \(i\))

Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_STRING_INDEXOF_RE

String index-of regular expression match.

Returns the first match of a regular expression \(r\) in a string \(s\). If the index is negative or greater than the length of string \(s_1\), or \(r\) does not match a substring in \(s\) after index \(i\), the result is -1.

Arity: 3
- 1: Term of Sort String (string \(s\))
- 2: Term of Sort RegLan (regular expression \(r\))
- 3: Term of Sort Int (index \(i\))

Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_STRING_REPLACE

String replace.

Replaces a string \(s_2\) in a string \(s_1\) with string \(s_3\). If \(s_2\) does not appear in \(s_1\), \(s_1\) is returned unmodified.

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

Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_STRING_REPLACE_ALL

String replace all.

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

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

Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_STRING_REPLACE_RE

String replace regular expression match.

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

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

Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_STRING_REPLACE_RE_ALL

String replace all regular expression matches.

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

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

Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_STRING_TO_LOWER

String to lower case.

Arity: 1
- 1: Term of Sort String
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

enumerator CVC5_KIND_STRING_TO_UPPER

String to upper case.

Arity: 1
- 1: Term of Sort String
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

enumerator CVC5_KIND_STRING_REV

String reverse.

Arity: 1
- 1: Term of Sort String
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

enumerator CVC5_KIND_STRING_TO_CODE

String to code.

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

Arity: 1
- 1: Term of Sort String
Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_STRING_FROM_CODE

String from code.

Returns a string containing a single character whose code point matches the argument to this function, or the empty string if the argument is out-of-bounds.

Arity: 1
- 1: Term of Sort Int
Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_STRING_LT

String less than.

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

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

Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_STRING_LEQ

String less than or equal.

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

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

Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_STRING_PREFIX

String prefix-of.

Determines whether a string \(s_1\) is a prefix of string \(s_2\). If string s1 is empty, this operator returns true.

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

Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_STRING_SUFFIX

String suffix-of.

Determines whether a string \(s_1\) is a suffix of the second string. If string \(s_1\) is empty, this operator returns true.

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

Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_STRING_IS_DIGIT

String is-digit.

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

Arity: 1
- 1: Term of Sort String
Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_STRING_FROM_INT

Conversion from Int to String.

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

Arity: 1
- 1: Term of Sort Int
Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_STRING_TO_INT

String to integer (total function).

If the string does not contain an integer or the integer is negative, the operator returns -1.

Arity: 1
- 1: Term of Sort Int
Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_CONST_STRING

Constant string.

Create Term of this Kind with:
- Solver::mkString(const std::string&, bool) const
- Solver::mkString(const std::wstring&) const

enumerator CVC5_KIND_STRING_TO_REGEXP

Conversion from string to regexp.

Arity: 1
- 1: Term of Sort String
Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_REGEXP_CONCAT

Regular expression concatenation.

Arity: 2
- 1..2: Terms of Sort RegLan
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

enumerator CVC5_KIND_REGEXP_UNION

Regular expression union.

Arity: 2
- 1..2: Terms of Sort RegLan
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

enumerator CVC5_KIND_REGEXP_INTER

Regular expression intersection.

Arity: 2
- 1..2: Terms of Sort RegLan
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

enumerator CVC5_KIND_REGEXP_DIFF

Regular expression difference.

Arity: 2
- 1..2: Terms of Sort RegLan
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

enumerator CVC5_KIND_REGEXP_STAR

Regular expression *.

Arity: 1
- 1: Term of Sort RegLan
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

enumerator CVC5_KIND_REGEXP_PLUS

Regular expression +.

Arity: 1
- 1: Term of Sort RegLan
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

enumerator CVC5_KIND_REGEXP_OPT

Regular expression ?.

Arity: 1
- 1: Term of Sort RegLan
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

enumerator CVC5_KIND_REGEXP_RANGE

Regular expression range.

Arity: 2
- 1: Term of Sort String (lower bound character for the range)
- 2: Term of Sort String (upper bound character for the range)
Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_REGEXP_REPEAT

Operator for regular expression repeat.

Arity: 1
- 1: Term of Sort RegLan
Indices: 1
- 1: The number of repetitions
Create Term of this Kind with:
- Solver::mkTerm(const Op&, const std::vector<Term>&) const
Create Op of this kind with:
- Solver::mkOp(Kind, const std::vector<uint32_t>&) const

enumerator CVC5_KIND_REGEXP_LOOP

Regular expression loop.

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

Arity: 1
- 1: Term of Sort RegLan
Indices: 1
- 1: The lower bound
- 2: The upper bound
Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_REGEXP_NONE

Regular expression none.

Create Term of this Kind with:
- Solver::mkRegexpNone() const

enumerator CVC5_KIND_REGEXP_ALL

Regular expression all.

Create Term of this Kind with:
- Solver::mkRegexpAll() const

enumerator CVC5_KIND_REGEXP_ALLCHAR

Regular expression all characters.

Create Term of this Kind with:
- Solver::mkRegexpAllchar() const

enumerator CVC5_KIND_REGEXP_COMPLEMENT

Regular expression complement.

Arity: 1
- 1: Term of Sort RegLan
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

enumerator CVC5_KIND_SEQ_CONCAT

Sequence concat.

Arity: n > 1
- 1..n: Terms of sequence Sort
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

enumerator CVC5_KIND_SEQ_LENGTH

Sequence length.

Arity: 1
- 1: Term of sequence Sort
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

enumerator CVC5_KIND_SEQ_EXTRACT

Sequence extract.

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

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

Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_SEQ_UPDATE

Sequence update.

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

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

Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_SEQ_AT

Sequence element at.

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

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

Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_SEQ_CONTAINS

Sequence contains.

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

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

Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_SEQ_INDEXOF

Sequence index-of.

Returns the index of a subsequence \(s_2\) in a sequence \(s_1\) starting at index \(i\). If the index is negative or greater than the length of sequence \(s_1\) or the subsequence \(s_2\) does not appear in sequence \(s_1\) after index \(i\), the result is -1.

Arity: 3
- 1: Term of sequence Sort (\(s_1\))
- 2: Term of sequence Sort (\(s_2\))
- 3: Term of Sort Int (\(i\))

Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_SEQ_REPLACE

Sequence replace.

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

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

Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_SEQ_REPLACE_ALL

Sequence replace all.

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

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

Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_SEQ_REV

Sequence reverse.

Arity: 1
- 1: Term of sequence Sort
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

enumerator CVC5_KIND_SEQ_PREFIX

Sequence prefix-of.

Checks whether a sequence \(s_1\) is a prefix of sequence \(s_2\). If sequence \(s_1\) is empty, this operator returns true.

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

Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_SEQ_SUFFIX

Sequence suffix-of.

Checks whether a sequence \(s_1\) is a suffix of sequence \(s_2\). If sequence \(s_1\) is empty, this operator returns true.

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

Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_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:
- Solver::mkEmptySequence(const Sort&) const

enumerator CVC5_KIND_SEQ_UNIT

Sequence unit.

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

Arity: 1
- 1: Term of any Sort (the element term)
Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_SEQ_NTH

Sequence nth.

Corresponds to the nth element of a sequence.

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

Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_FORALL

Universally quantified formula.

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

Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_EXISTS

Existentially quantified formula.

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

Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_VARIABLE_LIST

Variable list.

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

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

Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_INST_PATTERN

Instantiation pattern.

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

Arity: n > 0
- 1..n: Terms of any Sort
Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

Note

Should only be used as a child of INST_PATTERN_LIST.

enumerator CVC5_KIND_INST_NO_PATTERN

Instantiation no-pattern.

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

Arity: n > 0
- 1..n: Terms of any Sort
Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

Note

Should only be used as a child of INST_PATTERN_LIST.

enumerator CVC5_KIND_INST_POOL

Instantiation pool annotation.

Specifies an annotation for pool based instantiation.

In detail, pool symbols can be declared via the method

Solver::declarePool(const std::string&, const Sort&, const std::vector<Term>&) const

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

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 CVC5_KIND_INST_ADD_TO_POOL

A instantantiation-add-to-pool annotation.

An instantantiation-add-to-pool annotation indicates that when a quantified formula is instantiated, the instantiated version of a term should be added to the given pool.

For example, consider a quantified formula:

(FORALL (VARIABLE_LIST x) F
        (INST_PATTERN_LIST (INST_ADD_TO_POOL (ADD x 1) p)))

where assume that \(x\) has type Int. When this quantified formula is instantiated with, e.g., the term \(t\), the term (ADD t 1) is added to pool \(p\).

Arity: 2
- 1: The Term whose free variables are bound by the quantified formula.
- 2: The pool to add to, whose Sort should be a set of elements that match the Sort of the first argument.
Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

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 CVC5_KIND_SKOLEM_ADD_TO_POOL

A skolemization-add-to-pool annotation.

An skolemization-add-to-pool annotation indicates that when a quantified formula is skolemized, the skolemized version of a term should be added to the given pool.

For example, consider a quantified formula:

(FORALL (VARIABLE_LIST x) F
        (INST_PATTERN_LIST (SKOLEM_ADD_TO_POOL (ADD x 1) p)))

where assume that \(x\) has type Int. When this quantified formula is skolemized, e.g., with \(k\) of type Int, then the term (ADD k 1) is added to the pool \(p\).

Arity: 2
- 1: The Term whose free variables are bound by the quantified formula.
- 2: The pool to add to, whose Sort should be a set of elements that match the Sort of the first argument.
Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

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 CVC5_KIND_INST_ATTRIBUTE

Instantiation attribute.

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

Arity: n > 0
- 1: Term of Kind :cpp:enumerator:CONST_STRING (the keyword of the attribute)
- 2...n: Terms representing the values of the attribute
Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

Note

Should only be used as a child of INST_PATTERN_LIST.

enumerator CVC5_KIND_INST_PATTERN_LIST

A list of instantiation patterns, attributes or annotations.

Arity: n > 1
- 1..n: Terms of Kind INST_PATTERN, INST_NO_PATTERN, INST_POOL, INST_ADD_TO_POOL, SKOLEM_ADD_TO_POOL, INST_ATTRIBUTE

Create Term of this Kind with:
- Solver::mkTerm(Kind, 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

enumerator CVC5_KIND_LAST_KIND: Marks the upper-bound of this enumeration.

const char *cvc5_kind_to_string(Cvc5Kind kind)

Get a string representation of a Cvc5Kind.

Parameters:: kind – The kind.
Returns:: The string representation.

size_t cvc5_kind_hash(Cvc5Kind kind)

Hash function for Cvc5Kinds.

Parameters:: kind – The kind.
Returns:: The hash value.