#[repr(u32)]
pub enum DeclKind {
Show 239 variants
TRUE,
FALSE,
EQ,
DISTINCT,
ITE,
AND,
OR,
IFF,
XOR,
NOT,
IMPLIES,
OEQ,
ANUM,
AGNUM,
LE,
GE,
LT,
GT,
ADD,
SUB,
UMINUS,
MUL,
DIV,
IDIV,
REM,
MOD,
TO_REAL,
TO_INT,
IS_INT,
POWER,
STORE,
SELECT,
CONST_ARRAY,
ARRAY_MAP,
ARRAY_DEFAULT,
SET_UNION,
SET_INTERSECT,
SET_DIFFERENCE,
SET_COMPLEMENT,
SET_SUBSET,
AS_ARRAY,
ARRAY_EXT,
BNUM,
BIT1,
BIT0,
BNEG,
BADD,
BSUB,
BMUL,
BSDIV,
BUDIV,
BSREM,
BUREM,
BSMOD,
BSDIV0,
BUDIV0,
BSREM0,
BUREM0,
BSMOD0,
ULEQ,
SLEQ,
UGEQ,
SGEQ,
ULT,
SLT,
UGT,
SGT,
BAND,
BOR,
BNOT,
BXOR,
BNAND,
BNOR,
BXNOR,
CONCAT,
SIGN_EXT,
ZERO_EXT,
EXTRACT,
REPEAT,
BREDOR,
BREDAND,
BCOMP,
BSHL,
BLSHR,
BASHR,
ROTATE_LEFT,
ROTATE_RIGHT,
EXT_ROTATE_LEFT,
EXT_ROTATE_RIGHT,
BIT2BOOL,
INT2BV,
BV2INT,
CARRY,
XOR3,
BSMUL_NO_OVFL,
BUMUL_NO_OVFL,
BSMUL_NO_UDFL,
BSDIV_I,
BUDIV_I,
BSREM_I,
BUREM_I,
BSMOD_I,
PR_UNDEF,
PR_TRUE,
PR_ASSERTED,
PR_GOAL,
PR_MODUS_PONENS,
PR_REFLEXIVITY,
PR_SYMMETRY,
PR_TRANSITIVITY,
PR_TRANSITIVITY_STAR,
PR_MONOTONICITY,
PR_QUANT_INTRO,
PR_BIND,
PR_DISTRIBUTIVITY,
PR_AND_ELIM,
PR_NOT_OR_ELIM,
PR_REWRITE,
PR_REWRITE_STAR,
PR_PULL_QUANT,
PR_PUSH_QUANT,
PR_ELIM_UNUSED_VARS,
PR_DER,
PR_QUANT_INST,
PR_HYPOTHESIS,
PR_LEMMA,
PR_UNIT_RESOLUTION,
PR_IFF_TRUE,
PR_IFF_FALSE,
PR_COMMUTATIVITY,
PR_DEF_AXIOM,
PR_DEF_INTRO,
PR_APPLY_DEF,
PR_IFF_OEQ,
PR_NNF_POS,
PR_NNF_NEG,
PR_SKOLEMIZE,
PR_MODUS_PONENS_OEQ,
PR_TH_LEMMA,
PR_HYPER_RESOLVE,
RA_STORE,
RA_EMPTY,
RA_IS_EMPTY,
RA_JOIN,
RA_UNION,
RA_WIDEN,
RA_PROJECT,
RA_FILTER,
RA_NEGATION_FILTER,
RA_RENAME,
RA_COMPLEMENT,
RA_SELECT,
RA_CLONE,
FD_CONSTANT,
FD_LT,
SEQ_UNIT,
SEQ_EMPTY,
SEQ_CONCAT,
SEQ_PREFIX,
SEQ_SUFFIX,
SEQ_CONTAINS,
SEQ_EXTRACT,
SEQ_REPLACE,
SEQ_AT,
SEQ_LENGTH,
SEQ_INDEX,
SEQ_TO_RE,
SEQ_IN_RE,
STR_TO_INT,
INT_TO_STR,
RE_PLUS,
RE_STAR,
RE_OPTION,
RE_CONCAT,
RE_UNION,
RE_RANGE,
RE_LOOP,
RE_INTERSECT,
RE_EMPTY_SET,
RE_FULL_SET,
RE_COMPLEMENT,
LABEL,
LABEL_LIT,
DT_CONSTRUCTOR,
DT_RECOGNISER,
DT_IS,
DT_ACCESSOR,
DT_UPDATE_FIELD,
PB_AT_MOST,
PB_AT_LEAST,
PB_LE,
PB_GE,
PB_EQ,
FPA_RM_NEAREST_TIES_TO_EVEN,
FPA_RM_NEAREST_TIES_TO_AWAY,
FPA_RM_TOWARD_POSITIVE,
FPA_RM_TOWARD_NEGATIVE,
FPA_RM_TOWARD_ZERO,
FPA_NUM,
FPA_PLUS_INF,
FPA_MINUS_INF,
FPA_NAN,
FPA_PLUS_ZERO,
FPA_MINUS_ZERO,
FPA_ADD,
FPA_SUB,
FPA_NEG,
FPA_MUL,
FPA_DIV,
FPA_REM,
FPA_ABS,
FPA_MIN,
FPA_MAX,
FPA_FMA,
FPA_SQRT,
FPA_ROUND_TO_INTEGRAL,
FPA_EQ,
FPA_LT,
FPA_GT,
FPA_LE,
FPA_GE,
FPA_IS_NAN,
FPA_IS_INF,
FPA_IS_ZERO,
FPA_IS_NORMAL,
FPA_IS_SUBNORMAL,
FPA_IS_NEGATIVE,
FPA_IS_POSITIVE,
FPA_FP,
FPA_TO_FP,
FPA_TO_FP_UNSIGNED,
FPA_TO_UBV,
FPA_TO_SBV,
FPA_TO_REAL,
FPA_TO_IEEE_BV,
FPA_BVWRAP,
FPA_BV2RM,
INTERNAL,
UNINTERPRETED,
}
Expand description
The different kinds of interpreted function kinds.
This corresponds to Z3_decl_kind
in the C API.
Variants§
TRUE
The constant true
.
FALSE
The constant false
.
EQ
The equality predicate.
DISTINCT
The n-ary distinct predicate (every argument is mutually distinct).
ITE
The ternary if-then-else term.
AND
n-ary conjunction.
OR
n-ary disjunction.
IFF
equivalence (binary).
XOR
Exclusive or.
NOT
Negation.
IMPLIES
Implication.
OEQ
Binary equivalence modulo namings. This binary predicate is used in proof terms. It captures equisatisfiability and equivalence modulo renamings.
ANUM
Arithmetic numeral.
AGNUM
Arithmetic algebraic numeral. Algebraic numbers are used to represent irrational numbers in Z3.
LE
<=
.
GE
>=
.
LT
<
.
GT
>
.
ADD
Addition - Binary.
SUB
Binary subtraction.
UMINUS
Unary minus.
MUL
Multiplication - Binary.
DIV
Division - Binary.
IDIV
Integer division - Binary.
REM
Remainder - Binary.
MOD
Modulus - Binary.
TO_REAL
Coercion of integer to real - Unary.
TO_INT
Coercion of real to integer - Unary.
IS_INT
Check if real is also an integer - Unary.
POWER
Power operator x^y
.
STORE
Array store. It satisfies select(store(a,i,v),j) = if i = j then v else select(a,j)
.
Array store takes at least 3 arguments.
SELECT
Array select.
CONST_ARRAY
The constant array. For example, select(const(v),i) = v
holds for every v
and i
. The function is unary.
ARRAY_MAP
Array map operator.
It satisfies map[f](a1,..,a_n)[i] = f(a1[i],...,a_n[i])
for every i
.
ARRAY_DEFAULT
Default value of arrays. For example default(const(v)) = v
. The function is unary.
SET_UNION
Set union between two Boolean arrays (two arrays whose range type is Boolean). The function is binary.
SET_INTERSECT
Set intersection between two Boolean arrays. The function is binary.
SET_DIFFERENCE
Set difference between two Boolean arrays. The function is binary.
SET_COMPLEMENT
Set complement of a Boolean array. The function is unary.
SET_SUBSET
Subset predicate between two Boolean arrays. The relation is binary.
AS_ARRAY
An array value that behaves as the function graph of the function passed as parameter.
ARRAY_EXT
Array extensionality function. It takes two arrays as arguments and produces an index, such that the arrays are different if they are different on the index.
BNUM
Bit-vector numeral.
BIT1
One bit bit-vector.
BIT0
Zero bit bit-vector.
BNEG
Unary minus.
BADD
Binary addition.
BSUB
Binary subtraction.
BMUL
Binary multiplication.
BSDIV
Binary signed division.
BUDIV
Binary unsigned division.
BSREM
Binary signed remainder.
BUREM
Binary unsigned remainder.
BSMOD
Binary signed modulus.
BSDIV0
Unary function. bsdiv(x, 0)
is congruent to bsdiv0(x)
.
BUDIV0
Unary function. budiv(x, 0)
is congruent to budiv0(x)
.
BSREM0
Unary function. bsrem(x, 0)
is congruent to bsrem0(x)
.
BUREM0
Unary function. burem(x, 0)
is congruent to burem0(x)
.
BSMOD0
Unary function. bsmod(x, 0)
is congruent to bsmod0(x)
.
ULEQ
Unsigned bit-vector <= - Binary relation.
SLEQ
Signed bit-vector <= - Binary relation.
UGEQ
Unsigned bit-vector >= - Binary relation.
SGEQ
Signed bit-vector >= - Binary relation.
ULT
Unsigned bit-vector < - Binary relation.
SLT
Signed bit-vector < - Binary relation.
UGT
Unsigned bit-vector > - Binary relation.
SGT
Signed bit-vector > - Binary relation.
BAND
Bit-wise and - Binary.
BOR
Bit-wise or - Binary.
BNOT
Bit-wise not - Unary.
BXOR
Bit-wise xor - Binary.
BNAND
Bit-wise nand - Binary.
BNOR
Bit-wise nor - Binary.
BXNOR
Bit-wise xnor - Binary.
CONCAT
Bit-vector concatenation - Binary.
SIGN_EXT
Bit-vector sign extension.
ZERO_EXT
Bit-vector zero extension.
EXTRACT
Bit-vector extraction.
REPEAT
Repeat bit-vector n times.
BREDOR
Bit-vector reduce or - Unary.
BREDAND
Bit-vector reduce and - Unary.
BCOMP
BSHL
Shift left.
BLSHR
Logical shift right.
BASHR
Arithmetical shift right.
ROTATE_LEFT
Left rotation.
ROTATE_RIGHT
Right rotation.
EXT_ROTATE_LEFT
(extended) Left rotation. Similar to DeclKind::ROTATE_LEFT
,
but it is a binary operator instead of a parametric one.
EXT_ROTATE_RIGHT
(extended) Right rotation. Similar to DeclKind::ROTATE_RIGHT
,
but it is a binary operator instead of a parametric one.
BIT2BOOL
INT2BV
Coerce integer to bit-vector.
NB. This function is not supported by the decision procedures. Only the most rudimentary simplification rules are applied to this function.
BV2INT
Coerce bit-vector to integer.
NB. This function is not supported by the decision procedures. Only the most rudimentary simplification rules are applied to this function.
CARRY
Compute the carry bit in a full-adder. The meaning is given by the equivalence:
(carry l1 l2 l3) <=> (or (and l1 l2) (and l1 l3) (and l2 l3)))
XOR3
Compute ternary XOR.
The meaning is given by the equivalence:
(xor3 l1 l2 l3) <=> (xor (xor l1 l2) l3)
BSMUL_NO_OVFL
Check that bit-wise signed multiplication does not overflow.
Signed multiplication overflows if the operands have the same sign and the result of multiplication does not fit within the available bits.
See also:
BUMUL_NO_OVFL
Check that bit-wise unsigned multiplication does not overflow.
Unsigned multiplication overflows if the result does not fit within the available bits.
See also:
BSMUL_NO_UDFL
Check that bit-wise signed multiplication does not underflow.
Signed multiplication underflows if the operands have opposite signs and the result of multiplication does not fit within the available bits.
See also:
BSDIV_I
Binary signed division.
It has the same semantics as DeclKind::BSDIV
, but created in
a context where the second operand can be assumed to be non-zero.
BUDIV_I
Binary unsigned division.
It has the same semantics as DeclKind::BUDIV
, but created in a
context where the second operand can be assumed to be non-zero.
BSREM_I
Binary signed remainder.
It has the same semantics as DeclKind::BSREM
, but created in a
context where the second operand can be assumed to be non-zero.
BUREM_I
Binary unsigned remainder.
It has the same semantics as DeclKind::BUREM
, but created in a
context where the second operand can be assumed to be non-zero.
BSMOD_I
Binary signed modulus.
It has the same semantics as DeclKind::BSMOD
, but created in a
context where the second operand can be assumed to be non-zero.
PR_UNDEF
Undef/Null proof object.
PR_TRUE
Proof for the expression ‘true’.
PR_ASSERTED
Proof for a fact asserted by the user.
PR_GOAL
Proof for a fact (tagged as goal) asserted by the user.
PR_MODUS_PONENS
Given a proof for p and a proof for (implies p q), produces a proof for q.
T1: p
T2: (implies p q)
[mp T1 T2]: q
The second antecedents may also be a proof for (iff p q)
.
PR_REFLEXIVITY
A proof for (R t t)
, where R
is a reflexive relation.
This proof object has no antecedents.
The only reflexive relations that are used are
equivalence modulo namings, equality and equivalence.
That is, R
is either ~
, =
or iff
.
PR_SYMMETRY
Given an symmetric relation R
and a proof for (R t s)
,
produces a proof for (R s t)
.
T1: (R t s)
[symmetry T1]: (R s t)
T1
is the antecedent of this proof object.
PR_TRANSITIVITY
Given a transitive relation R
, and proofs for (R t s)
and
(R s u)
, produces a proof for (R t u)
.
T1: (R t s)
T2: (R s u)
[trans T1 T2]: (R t u)
PR_TRANSITIVITY_STAR
Condensed transitivity proof.
It combines several symmetry and transitivity proofs.
Example:
T1: (R a b)
T2: (R c b)
T3: (R c d)
[trans* T1 T2 T3]: (R a d)
R
must be a symmetric and transitive relation.
Assuming that this proof object is a proof for (R s t)
, then
a proof checker must check if it is possible to prove (R s t)
using the antecedents, symmetry and transitivity. That is,
if there is a path from s
to t
, if we view every
antecedent (R a b)
as an edge between a
and b
.
PR_MONOTONICITY
Monotonicity proof object.
T1: (R t_1 s_1)
...
Tn: (R t_n s_n)
[monotonicity T1 ... Tn]: (R (f t_1 ... t_n) (f s_1 ... s_n))
Remark: if t_i == s_i
, then the antecedent Ti
is suppressed.
That is, reflexivity proofs are suppressed to save space.
PR_QUANT_INTRO
Given a proof for (~ p q)
, produces a proof for
(~ (forall (x) p) (forall (x) q))
.
T1: (~ p q)
[quant-intro T1]: (~ (forall (x) p) (forall (x) q))
PR_BIND
Given a proof p
, produces a proof of lambda x . p
, where x
are free
variables in p
.
T1: f
[proof-bind T1] forall (x) f
PR_DISTRIBUTIVITY
Distributivity proof object.
Given that f (= or)
distributes over g (= and)
, produces a proof for
(= (f a (g c d))
(g (f a c) (f a d)))
If f
and g
are associative, this proof also justifies the following equality:
(= (f (g a b) (g c d))
(g (f a c) (f a d) (f b c) (f b d)))
where each f
and g
can have arbitrary number of arguments.
This proof object has no antecedents.
Remark: This rule is used by the CNF conversion pass and
instantiated by f = or
, and g = and
.
PR_AND_ELIM
Given a proof for (and l_1 ... l_n)
, produces a proof
for l_i
.
T1: (and l_1 ... l_n)
[and-elim T1]: l_i
PR_NOT_OR_ELIM
Given a proof for (not (or l_1 ... l_n))
, produces a
proof for (not l_i)
.
T1: (not (or l_1 ... l_n))
[not-or-elim T1]: (not l_i)
PR_REWRITE
A proof for a local rewriting step (= t s)
.
The head function symbol of t
is interpreted.
This proof object has no antecedents.
The conclusion of a rewrite rule is either an equality (= t s)
,
an equivalence (iff t s)
, or equi-satisfiability (~ t s)
.
Remark: if f
is bool
, then =
is iff
.
Examples:
(= (+ x 0) x)
(= (+ x 1 2) (+ 3 x))
(iff (or x false) x)
PR_REWRITE_STAR
A proof for rewriting an expression t
into an expression s
.
This proof object can have n
antecedents. The antecedents are
proofs for equalities used as substitution rules.
The object is also used in a few cases. The cases are:
- When applying contextual simplification
(CONTEXT_SIMPLIFIER=true)
. - When converting bit-vectors to Booleans
(BIT2BOOL=true)
.
PR_PULL_QUANT
A proof for (iff (f (forall (x) q(x)) r) (forall (x) (f (q x) r)))
.
This proof object has no antecedents.
PR_PUSH_QUANT
A proof for:
(iff (forall (x_1 ... x_m) (and p_1[x_1 ... x_m] ... p_n[x_1 ... x_m]))
(and (forall (x_1 ... x_m) p_1[x_1 ... x_m])
...
(forall (x_1 ... x_m) p_n[x_1 ... x_m])))
This proof object has no antecedents.
PR_ELIM_UNUSED_VARS
A proof for
(iff (forall (x_1 ... x_n y_1 ... y_m) p[x_1 ... x_n])
(forall (x_1 ... x_n) p[x_1 ... x_n]))
It is used to justify the elimination of unused variables.
This proof object has no antecedents.
PR_DER
A proof for destructive equality resolution:
(iff (forall (x) (or (not (= x t)) P[x])) P[t])
if x
does not occur in t
.
This proof object has no antecedents.
Several variables can be eliminated simultaneously.
PR_QUANT_INST
A proof of (or (not (forall (x) (P x))) (P a))
.
PR_HYPOTHESIS
Mark a hypothesis in a natural deduction style proof.
PR_LEMMA
T1: false
[lemma T1]: (or (not l_1) ... (not l_n))
This proof object has one antecedent: a hypothetical proof for false.
It converts the proof in a proof for (or (not l_1) ... (not l_n))
,
when T1
contains the open hypotheses: l_1, ..., l_n
.
The hypotheses are closed after an application of a lemma.
Furthermore, there are no other open hypotheses in the subtree covered by the lemma.
PR_UNIT_RESOLUTION
T1: (or l_1 ... l_n l_1' ... l_m')
T2: (not l_1)
...
T(n+1): (not l_n)
[unit-resolution T1 ... T(n+1)]: (or l_1' ... l_m')
PR_IFF_TRUE
T1: p
[iff-true T1]: (iff p true)
PR_IFF_FALSE
T1: (not p)
[iff-false T1]: (iff p false)
PR_COMMUTATIVITY
[comm]: (= (f a b) (f b a))
f
is a commutative operator.
This proof object has no antecedents.
Remark: if f
is bool
, then =
is iff
.
PR_DEF_AXIOM
Proof object used to justify Tseitin’s like axioms:
(or (not (and p q)) p)
(or (not (and p q)) q)
(or (not (and p q r)) p)
(or (not (and p q r)) q)
(or (not (and p q r)) r)
...
(or (and p q) (not p) (not q))
(or (not (or p q)) p q)
(or (or p q) (not p))
(or (or p q) (not q))
(or (not (iff p q)) (not p) q)
(or (not (iff p q)) p (not q))
(or (iff p q) (not p) (not q))
(or (iff p q) p q)
(or (not (ite a b c)) (not a) b)
(or (not (ite a b c)) a c)
(or (ite a b c) (not a) (not b))
(or (ite a b c) a (not c))
(or (not (not a)) (not a))
(or (not a) a)
This proof object has no antecedents.
Note: all axioms are propositional tautologies.
Note also that and
and or
can take multiple arguments.
You can recover the propositional tautologies by
unfolding the Boolean connectives in the axioms a small
bounded number of steps (=3)
.
PR_DEF_INTRO
Introduces a name for a formula/term.
Suppose e
is an expression with free variables x
, and
def-intro
introduces the name n(x)
. The possible cases are:
When e is of Boolean type:
[def-intro]: (and (or n (not e)) (or (not n) e))
or:
[def-intro]: (or (not n) e)
when e only occurs positively.
When e is of the form (ite cond th el)
:
[def-intro]: (and (or (not cond) (= n th)) (or cond (= n el)))
Otherwise:
[def-intro]: (= n e)
PR_APPLY_DEF
[apply-def T1]: F ~ n
F
is ‘equivalent’ to n
, given that T1
is a proof that
n
is a name for F
.
PR_IFF_OEQ
T1: (iff p q)
[iff~ T1]: (~ p q)
PR_NNF_POS
Proof for a (positive) NNF step. Example:
T1: (not s_1) ~ r_1
T2: (not s_2) ~ r_2
T3: s_1 ~ r_1'
T4: s_2 ~ r_2'
[nnf-pos T1 T2 T3 T4]: (~ (iff s_1 s_2)
(and (or r_1 r_2') (or r_1' r_2)))
The negation normal form steps NNF_POS
and NNF_NEG
are used in the
following cases:
- When creating the NNF of a positive force quantifier.
The quantifier is retained (unless the bound variables are eliminated).
Example:
T1: q ~ q_new [nnf-pos T1]: (~ (forall (x T) q) (forall (x T) q_new))
- When recursively creating NNF over Boolean formulas, where the top-level
connective is changed during NNF conversion. The relevant Boolean connectives
for
NNF_POS
areimplies
,iff
,xor
,ite
.NNF_NEG
furthermore handles the case where negation is pushed over Boolean connectivesand
andor
.
PR_NNF_NEG
Proof for a (negative) NNF step. Examples:
T1: (not s_1) ~ r_1
...
Tn: (not s_n) ~ r_n
[nnf-neg T1 ... Tn]: (not (and s_1 ... s_n)) ~ (or r_1 ... r_n)
and
T1: (not s_1) ~ r_1
...
Tn: (not s_n) ~ r_n
[nnf-neg T1 ... Tn]: (not (or s_1 ... s_n)) ~ (and r_1 ... r_n)
and
T1: (not s_1) ~ r_1
T2: (not s_2) ~ r_2
T3: s_1 ~ r_1'
T4: s_2 ~ r_2'
[nnf-neg T1 T2 T3 T4]: (~ (not (iff s_1 s_2))
(and (or r_1 r_2) (or r_1' r_2')))
PR_SKOLEMIZE
Proof for:
[sk]: (~ (not (forall x (p x y))) (not (p (sk y) y)))
[sk]: (~ (exists x (p x y)) (p (sk y) y))
This proof object has no antecedents.
PR_MODUS_PONENS_OEQ
Modus ponens style rule for equi-satisfiability.
T1: p
T2: (~ p q)
[mp~ T1 T2]: q
PR_TH_LEMMA
Generic proof for theory lemmas.
The theory lemma function comes with one or more parameters.
The first parameter indicates the name of the theory.
For the theory of arithmetic, additional parameters provide hints for checking the theory lemma.
The hints for arithmetic are:
farkas
- followed by rational coefficients. Multiply the coefficients to the inequalities in the lemma, add the (negated) inequalities and obtain a contradiction.triangle-eq
- Indicates a lemma related to the equivalence:(iff (= t1 t2) (and (<= t1 t2) (<= t2 t1)))
gcd-test
- Indicates an integer linear arithmetic lemma that uses a gcd test.
PR_HYPER_RESOLVE
Hyper-resolution rule.
The premises of the rules is a sequence of clauses. The first clause argument is the main clause of the rule. with a literal from the first (main) clause.
Premises of the rules are of the form
(or l0 l1 l2 .. ln)
or
(=> (and l1 l2 .. ln) l0)
or in the most general (ground) form:
(=> (and ln+1 ln+2 .. ln+m) (or l0 l1 .. ln))
In other words we use the following (Prolog style) convention for Horn implications:
- the head of a Horn implication is position 0,
- the first conjunct in the body of an implication is position 1
- the second conjunct in the body of an implication is position 2
For general implications where the head is a disjunction, the first n positions correspond to the n disjuncts in the head. The next m positions correspond to the m conjuncts in the body.
The premises can be universally quantified so that the most general non-ground form is:
(forall (vars) (=> (and ln+1 ln+2 .. ln+m) (or l0 l1 .. ln)))
The hyper-resolution rule takes a sequence of parameters. The parameters are substitutions of bound variables separated by pairs of literal positions from the main clause and side clause.
RA_STORE
Insert a record into a relation.
The function takes n
+1 arguments, where the first argument
is the relation and the remaining n
elements
correspond to the n
columns of the relation.
RA_EMPTY
Creates the empty relation.
RA_IS_EMPTY
Tests if the relation is empty.
RA_JOIN
Create the relational join.
RA_UNION
Create the union or convex hull of two relations.
The function takes two arguments.
RA_WIDEN
Widen two relations.
The function takes two arguments.
RA_PROJECT
Project the columns (provided as numbers in the parameters).
The function takes one argument.
RA_FILTER
Filter (restrict) a relation with respect to a predicate.
The first argument is a relation.
The second argument is a predicate with free de-Bruijn indices corresponding to the columns of the relation.
So the first column in the relation has index 0.
RA_NEGATION_FILTER
Intersect the first relation with respect to negation of the second relation (the function takes two arguments).
Logically, the specification can be described by a function
target = filter_by_negation(pos, neg, columns)
where columns are pairs c1
, d1
, .., cN
, dN
of columns
from pos
and neg
, such that target are elements in x
in pos
,
such that there is no y
in neg
that agrees with
x
on the columns c1
, d1
, .., cN
, dN
.
RA_RENAME
Rename columns in the relation.
The function takes one argument.
The parameters contain the renaming as a cycle.
RA_COMPLEMENT
Complement the relation.
RA_SELECT
Check if a record is an element of the relation.
The function takes n
+1 arguments, where the first argument is a relation,
and the remaining n
arguments correspond to a record.
RA_CLONE
Create a fresh copy (clone) of a relation.
The function is logically the identity, but
in the context of a register machine allows
for DeclKind::RA_UNION
to perform destructive updates to the first argument.
FD_CONSTANT
FD_LT
A less than predicate over the finite domain SortKind::FiniteDomain
.
SEQ_UNIT
SEQ_EMPTY
SEQ_CONCAT
SEQ_PREFIX
SEQ_SUFFIX
SEQ_CONTAINS
SEQ_EXTRACT
SEQ_REPLACE
SEQ_AT
SEQ_LENGTH
SEQ_INDEX
SEQ_TO_RE
SEQ_IN_RE
STR_TO_INT
INT_TO_STR
RE_PLUS
RE_STAR
RE_OPTION
RE_CONCAT
RE_UNION
RE_RANGE
RE_LOOP
RE_INTERSECT
RE_EMPTY_SET
RE_FULL_SET
RE_COMPLEMENT
LABEL
A label (used by the Boogie Verification condition generator).
The label has two parameters, a string and a Boolean polarity.
It takes one argument, a formula.
LABEL_LIT
A label literal (used by the Boogie Verification condition generator).
A label literal has a set of string parameters. It takes no arguments.
DT_CONSTRUCTOR
Datatype constructor.
DT_RECOGNISER
Datatype recognizer.
DT_IS
Datatype recognizer.
DT_ACCESSOR
Datatype accessor.
DT_UPDATE_FIELD
Datatype field update.
PB_AT_MOST
Cardinality constraint.
Example: x + y + z <= 2
PB_AT_LEAST
Cardinality constraint.
Example: x + y + z >= 2
PB_LE
Generalized Pseudo-Boolean cardinality constraint.
Example: 2*x + 3*y <= 4
PB_GE
Generalized Pseudo-Boolean cardinality constraint.
Example: 2*x + 3*y + 2*z >= 4
PB_EQ
Generalized Pseudo-Boolean equality constraint.
Example: 2*x + 1*y + 2*z + 1*u = 4
FPA_RM_NEAREST_TIES_TO_EVEN
Floating-point rounding mode RNE
FPA_RM_NEAREST_TIES_TO_AWAY
Floating-point rounding mode RNA
FPA_RM_TOWARD_POSITIVE
Floating-point rounding mode RTP
FPA_RM_TOWARD_NEGATIVE
Floating-point rounding mode RTN
FPA_RM_TOWARD_ZERO
Floating-point rounding mode RTZ
FPA_NUM
Floating-point value
FPA_PLUS_INF
Floating-point +oo
FPA_MINUS_INF
Floating-point -oo
FPA_NAN
Floating-point NaN
FPA_PLUS_ZERO
Floating-point +zero
FPA_MINUS_ZERO
Floating-point -zero
FPA_ADD
Floating-point addition
FPA_SUB
Floating-point subtraction
FPA_NEG
Floating-point negation
FPA_MUL
Floating-point multiplication
FPA_DIV
Floating-point division
FPA_REM
Floating-point remainder
FPA_ABS
Floating-point absolute value
FPA_MIN
Floating-point minimum
FPA_MAX
Floating-point maximum
FPA_FMA
Floating-point fused multiply-add
FPA_SQRT
Floating-point square root
FPA_ROUND_TO_INTEGRAL
Floating-point round to integral
FPA_EQ
Floating-point equality
FPA_LT
Floating-point less than
FPA_GT
Floating-point greater than
FPA_LE
Floating-point less than or equal
FPA_GE
Floating-point greater than or equal
FPA_IS_NAN
Floating-point isNaN
FPA_IS_INF
Floating-point isInfinite
FPA_IS_ZERO
Floating-point isZero
FPA_IS_NORMAL
Floating-point isNormal
FPA_IS_SUBNORMAL
Floating-point isSubnormal
FPA_IS_NEGATIVE
Floating-point isNegative
FPA_IS_POSITIVE
Floating-point isPositive
FPA_FP
Floating-point constructor from 3 bit-vectors
FPA_TO_FP
Floating-point conversion (various)
FPA_TO_FP_UNSIGNED
Floating-point conversion from unsigned bit-vector
FPA_TO_UBV
Floating-point conversion to unsigned bit-vector
FPA_TO_SBV
Floating-point conversion to signed bit-vector
FPA_TO_REAL
Floating-point conversion to real number
FPA_TO_IEEE_BV
Floating-point conversion to IEEE-754 bit-vector
FPA_BVWRAP
Implicitly) represents the internal bitvector-representation of a floating-point term (used for the lazy encoding of non-relevant terms in theory_fpa)
FPA_BV2RM
Conversion of a 3-bit bit-vector term to a floating-point rounding-mode term.
The conversion uses the following values:
0 = 000 = DeclKind::FPA_RM_NEAREST_TIES_TO_EVEN
,
1 = 001 = DeclKind::FPA_RM_NEAREST_TIES_TO_AWAY
,
2 = 010 = DeclKind::FPA_RM_TOWARD_POSITIVE
,
3 = 011 = DeclKind::FPA_RM_TOWARD_NEGATIVE
,
4 = 100 = DeclKind::FPA_RM_TOWARD_ZERO
.
INTERNAL
Internal (often interpreted) symbol, but no additional information is exposed. Tools may use the string representation of the function declaration to obtain more information.
UNINTERPRETED
Kind used for uninterpreted symbols.