#[repr(u32)]pub enum DeclKind {
Show 279 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,
ToReal = 526,
ToInt = 527,
IsInt = 528,
Power = 529,
Abs = 530,
Store = 768,
Select = 769,
ConstArray = 770,
ArrayMap = 771,
ArrayDefault = 772,
SetUnion = 773,
SetIntersect = 774,
SetDifference = 775,
SetComplement = 776,
SetSubset = 777,
AsArray = 778,
ArrayExt = 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,
SignExt = 1_057,
ZeroExt = 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,
RotateLeft = 1_067,
RotateRight = 1_068,
ExtRotateLeft = 1_069,
ExtRotateRight = 1_070,
Bit2bool = 1_071,
Int2bv = 1_072,
Bv2int = 1_073,
Sbv2int = 1_074,
Carry = 1_075,
Xor3 = 1_076,
BsmulNoOvfl = 1_077,
BumulNoOvfl = 1_078,
BsmulNoUdfl = 1_079,
BsdivI = 1_080,
BudivI = 1_081,
BsremI = 1_082,
BuremI = 1_083,
BsmodI = 1_084,
PrUndef = 1_280,
PrTrue = 1_281,
PrAsserted = 1_282,
PrGoal = 1_283,
PrModusPonens = 1_284,
PrReflexivity = 1_285,
PrSymmetry = 1_286,
PrTransitivity = 1_287,
PrTransitivityStar = 1_288,
PrMonotonicity = 1_289,
PrQuantIntro = 1_290,
PrBind = 1_291,
PrDistributivity = 1_292,
PrAndElim = 1_293,
PrNotOrElim = 1_294,
PrRewrite = 1_295,
PrRewriteStar = 1_296,
PrPullQuant = 1_297,
PrPushQuant = 1_298,
PrElimUnusedVars = 1_299,
PrDer = 1_300,
PrQuantInst = 1_301,
PrHypothesis = 1_302,
PrLemma = 1_303,
PrUnitResolution = 1_304,
PrIffTrue = 1_305,
PrIffFalse = 1_306,
PrCommutativity = 1_307,
PrDefAxiom = 1_308,
PrAssumptionAdd = 1_309,
PrLemmaAdd = 1_310,
PrRedundantDel = 1_311,
PrClauseTrail = 1_312,
PrDefIntro = 1_313,
PrApplyDef = 1_314,
PrIffOeq = 1_315,
PrNnfPos = 1_316,
PrNnfNeg = 1_317,
PrSkolemize = 1_318,
PrModusPonensOeq = 1_319,
PrThLemma = 1_320,
PrHyperResolve = 1_321,
RaStore = 1_536,
RaEmpty = 1_537,
RaIsEmpty = 1_538,
RaJoin = 1_539,
RaUnion = 1_540,
RaWiden = 1_541,
RaProject = 1_542,
RaFilter = 1_543,
RaNegationFilter = 1_544,
RaRename = 1_545,
RaComplement = 1_546,
RaSelect = 1_547,
RaClone = 1_548,
FdConstant = 1_549,
FdLt = 1_550,
SeqUnit = 1_551,
SeqEmpty = 1_552,
SeqConcat = 1_553,
SeqPrefix = 1_554,
SeqSuffix = 1_555,
SeqContains = 1_556,
SeqExtract = 1_557,
SeqReplace = 1_558,
SeqReplaceRe = 1_559,
SeqReplaceReAll = 1_560,
SeqReplaceAll = 1_561,
SeqAt = 1_562,
SeqNth = 1_563,
SeqLength = 1_564,
SeqIndex = 1_565,
SeqLastIndex = 1_566,
SeqToRe = 1_567,
SeqInRe = 1_568,
SeqMap = 1_569,
SeqMapi = 1_570,
SeqFoldl = 1_571,
SeqFoldli = 1_572,
StrToInt = 1_573,
IntToStr = 1_574,
UbvToStr = 1_575,
SbvToStr = 1_576,
StrToCode = 1_577,
StrFromCode = 1_578,
StringLt = 1_579,
StringLe = 1_580,
RePlus = 1_581,
ReStar = 1_582,
ReOption = 1_583,
ReConcat = 1_584,
ReUnion = 1_585,
ReRange = 1_586,
ReDiff = 1_587,
ReIntersect = 1_588,
ReLoop = 1_589,
RePower = 1_590,
ReComplement = 1_591,
ReEmptySet = 1_592,
ReFullSet = 1_593,
ReFullCharSet = 1_594,
ReOfPred = 1_595,
ReReverse = 1_596,
ReDerivative = 1_597,
CharConst = 1_598,
CharLe = 1_599,
CharToInt = 1_600,
CharToBv = 1_601,
CharFromBv = 1_602,
CharIsDigit = 1_603,
Label = 1_792,
LabelLit = 1_793,
DtConstructor = 2_048,
DtRecogniser = 2_049,
DtIs = 2_050,
DtAccessor = 2_051,
DtUpdateField = 2_052,
PbAtMost = 2_304,
PbAtLeast = 2_305,
PbLe = 2_306,
PbGe = 2_307,
PbEq = 2_308,
SpecialRelationLo = 40_960,
SpecialRelationPo = 40_961,
SpecialRelationPlo = 40_962,
SpecialRelationTo = 40_963,
SpecialRelationTc = 40_964,
SpecialRelationTrc = 40_965,
FpaRmNearestTiesToEven = 45_056,
FpaRmNearestTiesToAway = 45_057,
FpaRmTowardPositive = 45_058,
FpaRmTowardNegative = 45_059,
FpaRmTowardZero = 45_060,
FpaNum = 45_061,
FpaPlusInf = 45_062,
FpaMinusInf = 45_063,
FpaNan = 45_064,
FpaPlusZero = 45_065,
FpaMinusZero = 45_066,
FpaAdd = 45_067,
FpaSub = 45_068,
FpaNeg = 45_069,
FpaMul = 45_070,
FpaDiv = 45_071,
FpaRem = 45_072,
FpaAbs = 45_073,
FpaMin = 45_074,
FpaMax = 45_075,
FpaFma = 45_076,
FpaSqrt = 45_077,
FpaRoundToIntegral = 45_078,
FpaEq = 45_079,
FpaLt = 45_080,
FpaGt = 45_081,
FpaLe = 45_082,
FpaGe = 45_083,
FpaIsNan = 45_084,
FpaIsInf = 45_085,
FpaIsZero = 45_086,
FpaIsNormal = 45_087,
FpaIsSubnormal = 45_088,
FpaIsNegative = 45_089,
FpaIsPositive = 45_090,
FpaFp = 45_091,
FpaToFp = 45_092,
FpaToFpUnsigned = 45_093,
FpaToUbv = 45_094,
FpaToSbv = 45_095,
FpaToReal = 45_096,
FpaToIeeeBv = 45_097,
FpaBvwrap = 45_098,
FpaBv2rm = 45_099,
Internal = 45_100,
Recursive = 45_101,
Uninterpreted = 45_102,
}Expand description
The different kinds of interpreted function kinds.
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.
ToReal = 526
Coercion of integer to real - Unary.
ToInt = 527
Coercion of real to integer - Unary.
IsInt = 528
Check if real is also an integer - Unary.
Power = 529
Power operator x^y.
Abs = 530
Corresponds to Z3_OP_ABS in the C API.
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.
ConstArray = 770
The constant array. For example, select(const(v),i) = v holds for every v and i. The function is unary.
ArrayMap = 771
Array map operator. It satisfies map[f](a1,..,a_n)[i] = f(a1[i],…,a_n[i]) for every i.
ArrayDefault = 772
Default value of arrays. For example default(const(v)) = v. The function is unary.
SetUnion = 773
Set union between two Boolean arrays (two arrays whose range type is Boolean). The function is binary.
SetIntersect = 774
Set intersection between two Boolean arrays. The function is binary.
SetDifference = 775
Set difference between two Boolean arrays. The function is binary.
SetComplement = 776
Set complement of a Boolean array. The function is unary.
SetSubset = 777
Subset predicate between two Boolean arrays. The relation is binary.
AsArray = 778
An array value that behaves as the function graph of the function passed as parameter.
ArrayExt = 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.
SignExt = 1_057
Bit-vector sign extension.
ZeroExt = 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.
RotateLeft = 1_067
Left rotation.
RotateRight = 1_068
Right rotation.
ExtRotateLeft = 1_069
(extended) Left rotation. Similar to Z3_OP_ROTATE_LEFT, but it is a binary operator instead of a parametric one.
ExtRotateRight = 1_070
(extended) Right rotation. Similar to Z3_OP_ROTATE_RIGHT, but it is a binary operator instead of a parametric one.
Bit2bool = 1_071
Corresponds to Z3_OP_BIT2BOOL in the C API.
Int2bv = 1_072
Coerce integer to bit-vector.
Bv2int = 1_073
Coerce bit-vector to integer.
Sbv2int = 1_074
Coerce signed bit-vector to integer.
Carry = 1_075
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_076
Compute ternary XOR. The meaning is given by the equivalence (xor3 l1 l2 l3) <=> (xor (xor l1 l2) l3)
BsmulNoOvfl = 1_077
a predicate to 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. \sa Z3_mk_bvmul_no_overflow.
BumulNoOvfl = 1_078
check that bit-wise unsigned multiplication does not overflow. Unsigned multiplication overflows if the result does not fit within the available bits.
§See also
BsmulNoUdfl = 1_079
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. Z3_mk_bvmul_no_underflow.
BsdivI = 1_080
Binary signed division. It has the same semantics as Z3_OP_BSDIV, but created in a context where the second operand can be assumed to be non-zero.
BudivI = 1_081
Binary unsigned division. It has the same semantics as Z3_OP_BUDIV, but created in a context where the second operand can be assumed to be non-zero.
BsremI = 1_082
Binary signed remainder. It has the same semantics as Z3_OP_BSREM, but created in a context where the second operand can be assumed to be non-zero.
BuremI = 1_083
Binary unsigned remainder. It has the same semantics as Z3_OP_BUREM, but created in a context where the second operand can be assumed to be non-zero.
BsmodI = 1_084
Binary signed modulus. It has the same semantics as Z3_OP_BSMOD, but created in a context where the second operand can be assumed to be non-zero.
PrUndef = 1_280
Undef/Null proof object.
PrTrue = 1_281
Proof for the expression ‘true’.
PrAsserted = 1_282
Proof for a fact asserted by the user.
PrGoal = 1_283
Proof for a fact (tagged as goal) asserted by the user.
PrModusPonens = 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]: q
The second antecedents may also be a proof for (iff p q).
PrReflexivity = 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’.
PrSymmetry = 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.
PrTransitivity = 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)PrTransitivityStar = 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.
PrMonotonicity = 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.
PrQuantIntro = 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))
PrBind = 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) f
PrDistributivity = 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.
PrAndElim = 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_i
PrNotOrElim = 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)
PrRewrite = 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)PrRewriteStar = 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 proof rule is used in a few cases. The cases are:
- When applying contextual simplification (CONTEXT_SIMPLIFIER=true)
- When converting bit-vectors to Booleans (BIT2BOOL=true)
PrPullQuant = 1_297
A proof for (iff (f (forall (x) q(x)) r) (forall (x) (f (q x) r))). This proof object has no antecedents.
PrPushQuant = 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.
PrElimUnusedVars = 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.
PrDer = 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.
PrQuantInst = 1_301
A proof of (or (not (forall (x) (P x))) (P a))
PrHypothesis = 1_302
Mark a hypothesis in a natural deduction style proof.
PrLemma = 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.
PrUnitResolution = 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')PrIffTrue = 1_305
T1: p
[iff-true T1]: (iff p true)PrIffFalse = 1_306
T1: (not p)
[iff-false T1]: (iff p false)PrCommutativity = 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.
PrDefAxiom = 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).
PrAssumptionAdd = 1_309
Clausal proof adding axiom
PrLemmaAdd = 1_310
Clausal proof lemma addition
PrRedundantDel = 1_311
Clausal proof lemma deletion
PrClauseTrail = 1_312
, Clausal proof trail of additions and deletions
PrDefIntro = 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)
PrApplyDef = 1_314
[apply-def T1]: F ~ n
F is ‘equivalent’ to n, given that T1 is a proof that n is a name for F.
PrIffOeq = 1_315
T1: (iff p q) [iff~ T1]: (~ p q)
PrNnfPos = 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: (a) 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))
(b) When recursively creating NNF over Boolean formulas, where the top-level connective is changed during NNF conversion. The relevant Boolean connectives for NNF_POS are ‘implies’, ‘iff’, ‘xor’, ‘ite’. NNF_NEG furthermore handles the case where negation is pushed over Boolean connectives ‘and’ and ‘or’.
PrNnfNeg = 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’)))
PrSkolemize = 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.
PrModusPonensOeq = 1_319
Modus ponens style rule for equi-satisfiability.
T1: p T2: (~ p q) [mp~ T1 T2]: q
PrThLemma = 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.
PrHyperResolve = 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.
RaStore = 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.
RaEmpty = 1_537
Creates the empty relation.
RaIsEmpty = 1_538
Tests if the relation is empty.
RaJoin = 1_539
Create the relational join.
RaUnion = 1_540
Create the union or convex hull of two relations. The function takes two arguments.
RaWiden = 1_541
Widen two relations. The function takes two arguments.
RaProject = 1_542
Project the columns (provided as numbers in the parameters). The function takes one argument.
RaFilter = 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.
RaNegationFilter = 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.
RaRename = 1_545
rename columns in the relation. The function takes one argument. The parameters contain the renaming as a cycle.
RaComplement = 1_546
Complement the relation.
RaSelect = 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.
RaClone = 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 Z3_OP_RA_UNION to perform destructive updates to the first argument.
FdConstant = 1_549
Corresponds to Z3_OP_FD_CONSTANT in the C API.
FdLt = 1_550
A less than predicate over the finite domain Z3_FINITE_DOMAIN_SORT.
SeqUnit = 1_551
Corresponds to Z3_OP_SEQ_UNIT in the C API.
SeqEmpty = 1_552
Corresponds to Z3_OP_SEQ_EMPTY in the C API.
SeqConcat = 1_553
Corresponds to Z3_OP_SEQ_CONCAT in the C API.
SeqPrefix = 1_554
Corresponds to Z3_OP_SEQ_PREFIX in the C API.
SeqSuffix = 1_555
Corresponds to Z3_OP_SEQ_SUFFIX in the C API.
SeqContains = 1_556
Corresponds to Z3_OP_SEQ_CONTAINS in the C API.
SeqExtract = 1_557
Corresponds to Z3_OP_SEQ_EXTRACT in the C API.
SeqReplace = 1_558
Corresponds to Z3_OP_SEQ_REPLACE in the C API.
SeqReplaceRe = 1_559
Corresponds to Z3_OP_SEQ_REPLACE_RE in the C API.
SeqReplaceReAll = 1_560
Corresponds to Z3_OP_SEQ_REPLACE_RE_ALL in the C API.
SeqReplaceAll = 1_561
Corresponds to Z3_OP_SEQ_REPLACE_ALL in the C API.
SeqAt = 1_562
Corresponds to Z3_OP_SEQ_AT in the C API.
SeqNth = 1_563
Corresponds to Z3_OP_SEQ_NTH in the C API.
SeqLength = 1_564
Corresponds to Z3_OP_SEQ_LENGTH in the C API.
SeqIndex = 1_565
Corresponds to Z3_OP_SEQ_INDEX in the C API.
SeqLastIndex = 1_566
Corresponds to Z3_OP_SEQ_LAST_INDEX in the C API.
SeqToRe = 1_567
Corresponds to Z3_OP_SEQ_TO_RE in the C API.
SeqInRe = 1_568
Corresponds to Z3_OP_SEQ_IN_RE in the C API.
SeqMap = 1_569
Corresponds to Z3_OP_SEQ_MAP in the C API.
SeqMapi = 1_570
Corresponds to Z3_OP_SEQ_MAPI in the C API.
SeqFoldl = 1_571
Corresponds to Z3_OP_SEQ_FOLDL in the C API.
SeqFoldli = 1_572
Corresponds to Z3_OP_SEQ_FOLDLI in the C API.
StrToInt = 1_573
Corresponds to Z3_OP_STR_TO_INT in the C API.
IntToStr = 1_574
Corresponds to Z3_OP_INT_TO_STR in the C API.
UbvToStr = 1_575
Corresponds to Z3_OP_UBV_TO_STR in the C API.
SbvToStr = 1_576
Corresponds to Z3_OP_SBV_TO_STR in the C API.
StrToCode = 1_577
Corresponds to Z3_OP_STR_TO_CODE in the C API.
StrFromCode = 1_578
Corresponds to Z3_OP_STR_FROM_CODE in the C API.
StringLt = 1_579
Corresponds to Z3_OP_STRING_LT in the C API.
StringLe = 1_580
Corresponds to Z3_OP_STRING_LE in the C API.
RePlus = 1_581
Corresponds to Z3_OP_RE_PLUS in the C API.
ReStar = 1_582
Corresponds to Z3_OP_RE_STAR in the C API.
ReOption = 1_583
Corresponds to Z3_OP_RE_OPTION in the C API.
ReConcat = 1_584
Corresponds to Z3_OP_RE_CONCAT in the C API.
ReUnion = 1_585
Corresponds to Z3_OP_RE_UNION in the C API.
ReRange = 1_586
Corresponds to Z3_OP_RE_RANGE in the C API.
ReDiff = 1_587
Corresponds to Z3_OP_RE_DIFF in the C API.
ReIntersect = 1_588
Corresponds to Z3_OP_RE_INTERSECT in the C API.
ReLoop = 1_589
Corresponds to Z3_OP_RE_LOOP in the C API.
RePower = 1_590
Corresponds to Z3_OP_RE_POWER in the C API.
ReComplement = 1_591
Corresponds to Z3_OP_RE_COMPLEMENT in the C API.
ReEmptySet = 1_592
Corresponds to Z3_OP_RE_EMPTY_SET in the C API.
ReFullSet = 1_593
Corresponds to Z3_OP_RE_FULL_SET in the C API.
ReFullCharSet = 1_594
Corresponds to Z3_OP_RE_FULL_CHAR_SET in the C API.
ReOfPred = 1_595
Corresponds to Z3_OP_RE_OF_PRED in the C API.
ReReverse = 1_596
Corresponds to Z3_OP_RE_REVERSE in the C API.
ReDerivative = 1_597
Corresponds to Z3_OP_RE_DERIVATIVE in the C API.
CharConst = 1_598
Corresponds to Z3_OP_CHAR_CONST in the C API.
CharLe = 1_599
Corresponds to Z3_OP_CHAR_LE in the C API.
CharToInt = 1_600
Corresponds to Z3_OP_CHAR_TO_INT in the C API.
CharToBv = 1_601
Corresponds to Z3_OP_CHAR_TO_BV in the C API.
CharFromBv = 1_602
Corresponds to Z3_OP_CHAR_FROM_BV in the C API.
CharIsDigit = 1_603
Corresponds to Z3_OP_CHAR_IS_DIGIT in the C API.
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.
LabelLit = 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.
DtConstructor = 2_048
datatype constructor.
DtRecogniser = 2_049
datatype recognizer.
DtIs = 2_050
datatype recognizer.
DtAccessor = 2_051
datatype accessor.
DtUpdateField = 2_052
datatype field update.
PbAtMost = 2_304
Cardinality constraint. E.g., x + y + z <= 2
PbAtLeast = 2_305
Cardinality constraint. E.g., x + y + z >= 2
PbLe = 2_306
Generalized Pseudo-Boolean cardinality constraint. Example 2x + 3y <= 4
PbGe = 2_307
Generalized Pseudo-Boolean cardinality constraint. Example 2x + 3y + 2*z >= 4
PbEq = 2_308
Generalized Pseudo-Boolean equality constraint. Example 2x + 1y + 2z + 1u = 4
SpecialRelationLo = 40_960
A relation that is a total linear order
SpecialRelationPo = 40_961
A relation that is a partial order
SpecialRelationPlo = 40_962
A relation that is a piecewise linear order
SpecialRelationTo = 40_963
A relation that is a tree order
SpecialRelationTc = 40_964
Transitive closure of a relation
SpecialRelationTrc = 40_965
Transitive reflexive closure of a relation
FpaRmNearestTiesToEven = 45_056
Floating-point rounding mode RNE
FpaRmNearestTiesToAway = 45_057
Floating-point rounding mode RNA
FpaRmTowardPositive = 45_058
Floating-point rounding mode RTP
FpaRmTowardNegative = 45_059
Floating-point rounding mode RTN
FpaRmTowardZero = 45_060
Floating-point rounding mode RTZ
FpaNum = 45_061
Floating-point value
FpaPlusInf = 45_062
Floating-point +oo
FpaMinusInf = 45_063
Floating-point -oo
FpaNan = 45_064
Floating-point NaN
FpaPlusZero = 45_065
Floating-point +zero
FpaMinusZero = 45_066
Floating-point -zero
FpaAdd = 45_067
Floating-point addition
FpaSub = 45_068
Floating-point subtraction
FpaNeg = 45_069
Floating-point negation
FpaMul = 45_070
Floating-point multiplication
FpaDiv = 45_071
Floating-point division
FpaRem = 45_072
Floating-point remainder
FpaAbs = 45_073
Floating-point absolute value
FpaMin = 45_074
Floating-point minimum
FpaMax = 45_075
Floating-point maximum
FpaFma = 45_076
Floating-point fused multiply-add
FpaSqrt = 45_077
Floating-point square root
FpaRoundToIntegral = 45_078
Floating-point round to integral
FpaEq = 45_079
Floating-point equality
FpaLt = 45_080
Floating-point less than
FpaGt = 45_081
Floating-point greater than
FpaLe = 45_082
Floating-point less than or equal
FpaGe = 45_083
Floating-point greater than or equal
FpaIsNan = 45_084
Floating-point isNaN
FpaIsInf = 45_085
Floating-point isInfinite
FpaIsZero = 45_086
Floating-point isZero
FpaIsNormal = 45_087
Floating-point isNormal
FpaIsSubnormal = 45_088
Floating-point isSubnormal
FpaIsNegative = 45_089
Floating-point isNegative
FpaIsPositive = 45_090
Floating-point isPositive
FpaFp = 45_091
Floating-point constructor from 3 bit-vectors
FpaToFp = 45_092
Floating-point conversion (various)
FpaToFpUnsigned = 45_093
Floating-point conversion from unsigned bit-vector
FpaToUbv = 45_094
Floating-point conversion to unsigned bit-vector
FpaToSbv = 45_095
Floating-point conversion to signed bit-vector
FpaToReal = 45_096
Floating-point conversion to real number
FpaToIeeeBv = 45_097
Floating-point conversion to IEEE-754 bit-vector
FpaBvwrap = 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)
FpaBv2rm = 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 = Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN, 1 = 001 = Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY, 2 = 010 = Z3_OP_FPA_RM_TOWARD_POSITIVE, 3 = 011 = Z3_OP_FPA_RM_TOWARD_NEGATIVE, 4 = 100 = Z3_OP_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.
Recursive = 45_101
function declared as recursive
Uninterpreted = 45_102
kind used for uninterpreted symbols.