#[repr(u32)]pub enum DeclKind {
Show 239 variants
TRUE = 256,
FALSE = 257,
EQ = 258,
DISTINCT = 259,
ITE = 260,
AND = 261,
OR = 262,
IFF = 263,
XOR = 264,
NOT = 265,
IMPLIES = 266,
OEQ = 267,
ANUM = 512,
AGNUM = 513,
LE = 514,
GE = 515,
LT = 516,
GT = 517,
ADD = 518,
SUB = 519,
UMINUS = 520,
MUL = 521,
DIV = 522,
IDIV = 523,
REM = 524,
MOD = 525,
TO_REAL = 526,
TO_INT = 527,
IS_INT = 528,
POWER = 529,
STORE = 768,
SELECT = 769,
CONST_ARRAY = 770,
ARRAY_MAP = 771,
ARRAY_DEFAULT = 772,
SET_UNION = 773,
SET_INTERSECT = 774,
SET_DIFFERENCE = 775,
SET_COMPLEMENT = 776,
SET_SUBSET = 777,
AS_ARRAY = 778,
ARRAY_EXT = 779,
BNUM = 1_024,
BIT1 = 1_025,
BIT0 = 1_026,
BNEG = 1_027,
BADD = 1_028,
BSUB = 1_029,
BMUL = 1_030,
BSDIV = 1_031,
BUDIV = 1_032,
BSREM = 1_033,
BUREM = 1_034,
BSMOD = 1_035,
BSDIV0 = 1_036,
BUDIV0 = 1_037,
BSREM0 = 1_038,
BUREM0 = 1_039,
BSMOD0 = 1_040,
ULEQ = 1_041,
SLEQ = 1_042,
UGEQ = 1_043,
SGEQ = 1_044,
ULT = 1_045,
SLT = 1_046,
UGT = 1_047,
SGT = 1_048,
BAND = 1_049,
BOR = 1_050,
BNOT = 1_051,
BXOR = 1_052,
BNAND = 1_053,
BNOR = 1_054,
BXNOR = 1_055,
CONCAT = 1_056,
SIGN_EXT = 1_057,
ZERO_EXT = 1_058,
EXTRACT = 1_059,
REPEAT = 1_060,
BREDOR = 1_061,
BREDAND = 1_062,
BCOMP = 1_063,
BSHL = 1_064,
BLSHR = 1_065,
BASHR = 1_066,
ROTATE_LEFT = 1_067,
ROTATE_RIGHT = 1_068,
EXT_ROTATE_LEFT = 1_069,
EXT_ROTATE_RIGHT = 1_070,
BIT2BOOL = 1_071,
INT2BV = 1_072,
BV2INT = 1_073,
CARRY = 1_074,
XOR3 = 1_075,
BSMUL_NO_OVFL = 1_076,
BUMUL_NO_OVFL = 1_077,
BSMUL_NO_UDFL = 1_078,
BSDIV_I = 1_079,
BUDIV_I = 1_080,
BSREM_I = 1_081,
BUREM_I = 1_082,
BSMOD_I = 1_083,
PR_UNDEF = 1_280,
PR_TRUE = 1_281,
PR_ASSERTED = 1_282,
PR_GOAL = 1_283,
PR_MODUS_PONENS = 1_284,
PR_REFLEXIVITY = 1_285,
PR_SYMMETRY = 1_286,
PR_TRANSITIVITY = 1_287,
PR_TRANSITIVITY_STAR = 1_288,
PR_MONOTONICITY = 1_289,
PR_QUANT_INTRO = 1_290,
PR_BIND = 1_291,
PR_DISTRIBUTIVITY = 1_292,
PR_AND_ELIM = 1_293,
PR_NOT_OR_ELIM = 1_294,
PR_REWRITE = 1_295,
PR_REWRITE_STAR = 1_296,
PR_PULL_QUANT = 1_297,
PR_PUSH_QUANT = 1_298,
PR_ELIM_UNUSED_VARS = 1_299,
PR_DER = 1_300,
PR_QUANT_INST = 1_301,
PR_HYPOTHESIS = 1_302,
PR_LEMMA = 1_303,
PR_UNIT_RESOLUTION = 1_304,
PR_IFF_TRUE = 1_305,
PR_IFF_FALSE = 1_306,
PR_COMMUTATIVITY = 1_307,
PR_DEF_AXIOM = 1_308,
PR_DEF_INTRO = 1_313,
PR_APPLY_DEF = 1_314,
PR_IFF_OEQ = 1_315,
PR_NNF_POS = 1_316,
PR_NNF_NEG = 1_317,
PR_SKOLEMIZE = 1_318,
PR_MODUS_PONENS_OEQ = 1_319,
PR_TH_LEMMA = 1_320,
PR_HYPER_RESOLVE = 1_321,
RA_STORE = 1_536,
RA_EMPTY = 1_537,
RA_IS_EMPTY = 1_538,
RA_JOIN = 1_539,
RA_UNION = 1_540,
RA_WIDEN = 1_541,
RA_PROJECT = 1_542,
RA_FILTER = 1_543,
RA_NEGATION_FILTER = 1_544,
RA_RENAME = 1_545,
RA_COMPLEMENT = 1_546,
RA_SELECT = 1_547,
RA_CLONE = 1_548,
FD_CONSTANT = 1_549,
FD_LT = 1_550,
SEQ_UNIT = 1_551,
SEQ_EMPTY = 1_552,
SEQ_CONCAT = 1_553,
SEQ_PREFIX = 1_554,
SEQ_SUFFIX = 1_555,
SEQ_CONTAINS = 1_556,
SEQ_EXTRACT = 1_557,
SEQ_REPLACE = 1_558,
SEQ_AT = 1_559,
SEQ_LENGTH = 1_561,
SEQ_INDEX = 1_562,
SEQ_TO_RE = 1_564,
SEQ_IN_RE = 1_565,
STR_TO_INT = 1_566,
INT_TO_STR = 1_567,
RE_PLUS = 1_570,
RE_STAR = 1_571,
RE_OPTION = 1_572,
RE_CONCAT = 1_573,
RE_UNION = 1_574,
RE_RANGE = 1_575,
RE_LOOP = 1_576,
RE_INTERSECT = 1_577,
RE_EMPTY_SET = 1_578,
RE_FULL_SET = 1_579,
RE_COMPLEMENT = 1_580,
LABEL = 1_792,
LABEL_LIT = 1_793,
DT_CONSTRUCTOR = 2_048,
DT_RECOGNISER = 2_049,
DT_IS = 2_050,
DT_ACCESSOR = 2_051,
DT_UPDATE_FIELD = 2_052,
PB_AT_MOST = 2_304,
PB_AT_LEAST = 2_305,
PB_LE = 2_306,
PB_GE = 2_307,
PB_EQ = 2_308,
FPA_RM_NEAREST_TIES_TO_EVEN = 45_056,
FPA_RM_NEAREST_TIES_TO_AWAY = 45_057,
FPA_RM_TOWARD_POSITIVE = 45_058,
FPA_RM_TOWARD_NEGATIVE = 45_059,
FPA_RM_TOWARD_ZERO = 45_060,
FPA_NUM = 45_061,
FPA_PLUS_INF = 45_062,
FPA_MINUS_INF = 45_063,
FPA_NAN = 45_064,
FPA_PLUS_ZERO = 45_065,
FPA_MINUS_ZERO = 45_066,
FPA_ADD = 45_067,
FPA_SUB = 45_068,
FPA_NEG = 45_069,
FPA_MUL = 45_070,
FPA_DIV = 45_071,
FPA_REM = 45_072,
FPA_ABS = 45_073,
FPA_MIN = 45_074,
FPA_MAX = 45_075,
FPA_FMA = 45_076,
FPA_SQRT = 45_077,
FPA_ROUND_TO_INTEGRAL = 45_078,
FPA_EQ = 45_079,
FPA_LT = 45_080,
FPA_GT = 45_081,
FPA_LE = 45_082,
FPA_GE = 45_083,
FPA_IS_NAN = 45_084,
FPA_IS_INF = 45_085,
FPA_IS_ZERO = 45_086,
FPA_IS_NORMAL = 45_087,
FPA_IS_SUBNORMAL = 45_088,
FPA_IS_NEGATIVE = 45_089,
FPA_IS_POSITIVE = 45_090,
FPA_FP = 45_091,
FPA_TO_FP = 45_092,
FPA_TO_FP_UNSIGNED = 45_093,
FPA_TO_UBV = 45_094,
FPA_TO_SBV = 45_095,
FPA_TO_REAL = 45_096,
FPA_TO_IEEE_BV = 45_097,
FPA_BVWRAP = 45_098,
FPA_BV2RM = 45_099,
INTERNAL = 45_100,
UNINTERPRETED = 45_101,
}Expand description
The different kinds of interpreted function kinds.
This corresponds to Z3_decl_kind in the C API.
Variants§
TRUE = 256
The constant true.
FALSE = 257
The constant false.
EQ = 258
The equality predicate.
DISTINCT = 259
The n-ary distinct predicate (every argument is mutually distinct).
ITE = 260
The ternary if-then-else term.
AND = 261
n-ary conjunction.
OR = 262
n-ary disjunction.
IFF = 263
equivalence (binary).
XOR = 264
Exclusive or.
NOT = 265
Negation.
IMPLIES = 266
Implication.
OEQ = 267
Binary equivalence modulo namings. This binary predicate is used in proof terms. It captures equisatisfiability and equivalence modulo renamings.
ANUM = 512
Arithmetic numeral.
AGNUM = 513
Arithmetic algebraic numeral. Algebraic numbers are used to represent irrational numbers in Z3.
LE = 514
<=.
GE = 515
>=.
LT = 516
<.
GT = 517
>.
ADD = 518
Addition - Binary.
SUB = 519
Binary subtraction.
UMINUS = 520
Unary minus.
MUL = 521
Multiplication - Binary.
DIV = 522
Division - Binary.
IDIV = 523
Integer division - Binary.
REM = 524
Remainder - Binary.
MOD = 525
Modulus - Binary.
TO_REAL = 526
Coercion of integer to real - Unary.
TO_INT = 527
Coercion of real to integer - Unary.
IS_INT = 528
Check if real is also an integer - Unary.
POWER = 529
Power operator x^y.
STORE = 768
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 = 769
Array select.
CONST_ARRAY = 770
The constant array. For example, select(const(v),i) = v
holds for every v and i. The function is unary.
ARRAY_MAP = 771
Array map operator.
It satisfies map[f](a1,..,a_n)[i] = f(a1[i],...,a_n[i]) for every i.
ARRAY_DEFAULT = 772
Default value of arrays. For example default(const(v)) = v. The function is unary.
SET_UNION = 773
Set union between two Boolean arrays (two arrays whose range type is Boolean). The function is binary.
SET_INTERSECT = 774
Set intersection between two Boolean arrays. The function is binary.
SET_DIFFERENCE = 775
Set difference between two Boolean arrays. The function is binary.
SET_COMPLEMENT = 776
Set complement of a Boolean array. The function is unary.
SET_SUBSET = 777
Subset predicate between two Boolean arrays. The relation is binary.
AS_ARRAY = 778
An array value that behaves as the function graph of the function passed as parameter.
ARRAY_EXT = 779
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 = 1_024
Bit-vector numeral.
BIT1 = 1_025
One bit bit-vector.
BIT0 = 1_026
Zero bit bit-vector.
BNEG = 1_027
Unary minus.
BADD = 1_028
Binary addition.
BSUB = 1_029
Binary subtraction.
BMUL = 1_030
Binary multiplication.
BSDIV = 1_031
Binary signed division.
BUDIV = 1_032
Binary unsigned division.
BSREM = 1_033
Binary signed remainder.
BUREM = 1_034
Binary unsigned remainder.
BSMOD = 1_035
Binary signed modulus.
BSDIV0 = 1_036
Unary function. bsdiv(x, 0) is congruent to bsdiv0(x).
BUDIV0 = 1_037
Unary function. budiv(x, 0) is congruent to budiv0(x).
BSREM0 = 1_038
Unary function. bsrem(x, 0) is congruent to bsrem0(x).
BUREM0 = 1_039
Unary function. burem(x, 0) is congruent to burem0(x).
BSMOD0 = 1_040
Unary function. bsmod(x, 0) is congruent to bsmod0(x).
ULEQ = 1_041
Unsigned bit-vector <= - Binary relation.
SLEQ = 1_042
Signed bit-vector <= - Binary relation.
UGEQ = 1_043
Unsigned bit-vector >= - Binary relation.
SGEQ = 1_044
Signed bit-vector >= - Binary relation.
ULT = 1_045
Unsigned bit-vector < - Binary relation.
SLT = 1_046
Signed bit-vector < - Binary relation.
UGT = 1_047
Unsigned bit-vector > - Binary relation.
SGT = 1_048
Signed bit-vector > - Binary relation.
BAND = 1_049
Bit-wise and - Binary.
BOR = 1_050
Bit-wise or - Binary.
BNOT = 1_051
Bit-wise not - Unary.
BXOR = 1_052
Bit-wise xor - Binary.
BNAND = 1_053
Bit-wise nand - Binary.
BNOR = 1_054
Bit-wise nor - Binary.
BXNOR = 1_055
Bit-wise xnor - Binary.
CONCAT = 1_056
Bit-vector concatenation - Binary.
SIGN_EXT = 1_057
Bit-vector sign extension.
ZERO_EXT = 1_058
Bit-vector zero extension.
EXTRACT = 1_059
Bit-vector extraction.
REPEAT = 1_060
Repeat bit-vector n times.
BREDOR = 1_061
Bit-vector reduce or - Unary.
BREDAND = 1_062
Bit-vector reduce and - Unary.
BCOMP = 1_063
BSHL = 1_064
Shift left.
BLSHR = 1_065
Logical shift right.
BASHR = 1_066
Arithmetical shift right.
ROTATE_LEFT = 1_067
Left rotation.
ROTATE_RIGHT = 1_068
Right rotation.
EXT_ROTATE_LEFT = 1_069
(extended) Left rotation. Similar to DeclKind::ROTATE_LEFT,
but it is a binary operator instead of a parametric one.
EXT_ROTATE_RIGHT = 1_070
(extended) Right rotation. Similar to DeclKind::ROTATE_RIGHT,
but it is a binary operator instead of a parametric one.
BIT2BOOL = 1_071
INT2BV = 1_072
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 = 1_073
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 = 1_074
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 = 1_075
Compute ternary XOR.
The meaning is given by the equivalence:
(xor3 l1 l2 l3) <=> (xor (xor l1 l2) l3)BSMUL_NO_OVFL = 1_076
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 = 1_077
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 = 1_078
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 = 1_079
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 = 1_080
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 = 1_081
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 = 1_082
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 = 1_083
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 = 1_280
Undef/Null proof object.
PR_TRUE = 1_281
Proof for the expression ‘true’.
PR_ASSERTED = 1_282
Proof for a fact asserted by the user.
PR_GOAL = 1_283
Proof for a fact (tagged as goal) asserted by the user.
PR_MODUS_PONENS = 1_284
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]: qThe second antecedents may also be a proof for (iff p q).
PR_REFLEXIVITY = 1_285
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 = 1_286
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 = 1_287
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 = 1_288
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 = 1_289
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 = 1_290
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 = 1_291
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) fPR_DISTRIBUTIVITY = 1_292
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 = 1_293
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_iPR_NOT_OR_ELIM = 1_294
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 = 1_295
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 = 1_296
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 = 1_297
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 = 1_298
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 = 1_299
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 = 1_300
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 = 1_301
A proof of (or (not (forall (x) (P x))) (P a)).
PR_HYPOTHESIS = 1_302
Mark a hypothesis in a natural deduction style proof.
PR_LEMMA = 1_303
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 = 1_304
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 = 1_305
T1: p
[iff-true T1]: (iff p true)PR_IFF_FALSE = 1_306
T1: (not p)
[iff-false T1]: (iff p false)PR_COMMUTATIVITY = 1_307
[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 = 1_308
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 = 1_313
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 = 1_314
[apply-def T1]: F ~ nF is ‘equivalent’ to n, given that T1 is a proof that
n is a name for F.
PR_IFF_OEQ = 1_315
T1: (iff p q)
[iff~ T1]: (~ p q)PR_NNF_POS = 1_316
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_POSareimplies,iff,xor,ite.NNF_NEGfurthermore handles the case where negation is pushed over Boolean connectivesandandor.
PR_NNF_NEG = 1_317
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 = 1_318
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 = 1_319
Modus ponens style rule for equi-satisfiability.
T1: p
T2: (~ p q)
[mp~ T1 T2]: qPR_TH_LEMMA = 1_320
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 = 1_321
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 = 1_536
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 = 1_537
Creates the empty relation.
RA_IS_EMPTY = 1_538
Tests if the relation is empty.
RA_JOIN = 1_539
Create the relational join.
RA_UNION = 1_540
Create the union or convex hull of two relations.
The function takes two arguments.
RA_WIDEN = 1_541
Widen two relations.
The function takes two arguments.
RA_PROJECT = 1_542
Project the columns (provided as numbers in the parameters).
The function takes one argument.
RA_FILTER = 1_543
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 = 1_544
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 = 1_545
Rename columns in the relation.
The function takes one argument.
The parameters contain the renaming as a cycle.
RA_COMPLEMENT = 1_546
Complement the relation.
RA_SELECT = 1_547
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 = 1_548
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 = 1_549
FD_LT = 1_550
A less than predicate over the finite domain SortKind::FiniteDomain.
SEQ_UNIT = 1_551
SEQ_EMPTY = 1_552
SEQ_CONCAT = 1_553
SEQ_PREFIX = 1_554
SEQ_SUFFIX = 1_555
SEQ_CONTAINS = 1_556
SEQ_EXTRACT = 1_557
SEQ_REPLACE = 1_558
SEQ_AT = 1_559
SEQ_LENGTH = 1_561
SEQ_INDEX = 1_562
SEQ_TO_RE = 1_564
SEQ_IN_RE = 1_565
STR_TO_INT = 1_566
INT_TO_STR = 1_567
RE_PLUS = 1_570
RE_STAR = 1_571
RE_OPTION = 1_572
RE_CONCAT = 1_573
RE_UNION = 1_574
RE_RANGE = 1_575
RE_LOOP = 1_576
RE_INTERSECT = 1_577
RE_EMPTY_SET = 1_578
RE_FULL_SET = 1_579
RE_COMPLEMENT = 1_580
LABEL = 1_792
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 = 1_793
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 = 2_048
Datatype constructor.
DT_RECOGNISER = 2_049
Datatype recognizer.
DT_IS = 2_050
Datatype recognizer.
DT_ACCESSOR = 2_051
Datatype accessor.
DT_UPDATE_FIELD = 2_052
Datatype field update.
PB_AT_MOST = 2_304
Cardinality constraint.
Example: x + y + z <= 2
PB_AT_LEAST = 2_305
Cardinality constraint.
Example: x + y + z >= 2
PB_LE = 2_306
Generalized Pseudo-Boolean cardinality constraint.
Example: 2*x + 3*y <= 4
PB_GE = 2_307
Generalized Pseudo-Boolean cardinality constraint.
Example: 2*x + 3*y + 2*z >= 4
PB_EQ = 2_308
Generalized Pseudo-Boolean equality constraint.
Example: 2*x + 1*y + 2*z + 1*u = 4
FPA_RM_NEAREST_TIES_TO_EVEN = 45_056
Floating-point rounding mode RNE
FPA_RM_NEAREST_TIES_TO_AWAY = 45_057
Floating-point rounding mode RNA
FPA_RM_TOWARD_POSITIVE = 45_058
Floating-point rounding mode RTP
FPA_RM_TOWARD_NEGATIVE = 45_059
Floating-point rounding mode RTN
FPA_RM_TOWARD_ZERO = 45_060
Floating-point rounding mode RTZ
FPA_NUM = 45_061
Floating-point value
FPA_PLUS_INF = 45_062
Floating-point +oo
FPA_MINUS_INF = 45_063
Floating-point -oo
FPA_NAN = 45_064
Floating-point NaN
FPA_PLUS_ZERO = 45_065
Floating-point +zero
FPA_MINUS_ZERO = 45_066
Floating-point -zero
FPA_ADD = 45_067
Floating-point addition
FPA_SUB = 45_068
Floating-point subtraction
FPA_NEG = 45_069
Floating-point negation
FPA_MUL = 45_070
Floating-point multiplication
FPA_DIV = 45_071
Floating-point division
FPA_REM = 45_072
Floating-point remainder
FPA_ABS = 45_073
Floating-point absolute value
FPA_MIN = 45_074
Floating-point minimum
FPA_MAX = 45_075
Floating-point maximum
FPA_FMA = 45_076
Floating-point fused multiply-add
FPA_SQRT = 45_077
Floating-point square root
FPA_ROUND_TO_INTEGRAL = 45_078
Floating-point round to integral
FPA_EQ = 45_079
Floating-point equality
FPA_LT = 45_080
Floating-point less than
FPA_GT = 45_081
Floating-point greater than
FPA_LE = 45_082
Floating-point less than or equal
FPA_GE = 45_083
Floating-point greater than or equal
FPA_IS_NAN = 45_084
Floating-point isNaN
FPA_IS_INF = 45_085
Floating-point isInfinite
FPA_IS_ZERO = 45_086
Floating-point isZero
FPA_IS_NORMAL = 45_087
Floating-point isNormal
FPA_IS_SUBNORMAL = 45_088
Floating-point isSubnormal
FPA_IS_NEGATIVE = 45_089
Floating-point isNegative
FPA_IS_POSITIVE = 45_090
Floating-point isPositive
FPA_FP = 45_091
Floating-point constructor from 3 bit-vectors
FPA_TO_FP = 45_092
Floating-point conversion (various)
FPA_TO_FP_UNSIGNED = 45_093
Floating-point conversion from unsigned bit-vector
FPA_TO_UBV = 45_094
Floating-point conversion to unsigned bit-vector
FPA_TO_SBV = 45_095
Floating-point conversion to signed bit-vector
FPA_TO_REAL = 45_096
Floating-point conversion to real number
FPA_TO_IEEE_BV = 45_097
Floating-point conversion to IEEE-754 bit-vector
FPA_BVWRAP = 45_098
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 = 45_099
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 = 45_100
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 = 45_101
Kind used for uninterpreted symbols.