Z3DeclKind
public extension Z3DeclKind
-
The constant true.
Declaration
Swift
static let opTrue: Z3_decl_kind
-
The constant false.
Declaration
Swift
static let opFalse: Z3_decl_kind
-
The equality predicate.
Declaration
Swift
static let opEq: Z3_decl_kind
-
The n-ary distinct predicate (every argument is mutually distinct).
Declaration
Swift
static let opDistinct: Z3_decl_kind
-
The ternary if-then-else term.
Declaration
Swift
static let opIte: Z3_decl_kind
-
n-ary conjunction.
Declaration
Swift
static let opAnd: Z3_decl_kind
-
n-ary disjunction.
Declaration
Swift
static let opOr: Z3_decl_kind
-
equivalence (binary).
Declaration
Swift
static let opIff: Z3_decl_kind
-
Exclusive or.
Declaration
Swift
static let opXor: Z3_decl_kind
-
Negation.
Declaration
Swift
static let opNot: Z3_decl_kind
-
Implication.
Declaration
Swift
static let opImplies: Z3_decl_kind
-
Binary equivalence modulo namings. This binary predicate is used in proof terms. It captures equisatisfiability and equivalence modulo renamings.
Declaration
Swift
static let opOeq: Z3_decl_kind
-
Arithmetic numeral.
Declaration
Swift
static let opAnum: Z3_decl_kind
-
Arithmetic algebraic numeral. Algebraic numbers are used to represent irrational numbers in Z3.
Declaration
Swift
static let opAgnum: Z3_decl_kind
-
<=.
Declaration
Swift
static let opLe: Z3_decl_kind
-
=.
Declaration
Swift
static let opGe: Z3_decl_kind
-
<.
Declaration
Swift
static let opLt: Z3_decl_kind
-
.
Declaration
Swift
static let opGt: Z3_decl_kind
-
Addition - Binary.
Declaration
Swift
static let opAdd: Z3_decl_kind
-
Binary subtraction.
Declaration
Swift
static let opSub: Z3_decl_kind
-
Unary minus.
Declaration
Swift
static let opUminus: Z3_decl_kind
-
Multiplication - Binary.
Declaration
Swift
static let opMul: Z3_decl_kind
-
Division - Binary.
Declaration
Swift
static let opDiv: Z3_decl_kind
-
Integer division - Binary.
Declaration
Swift
static let opIdiv: Z3_decl_kind
-
Remainder - Binary.
Declaration
Swift
static let opRem: Z3_decl_kind
-
Modulus - Binary.
Declaration
Swift
static let opMod: Z3_decl_kind
-
Coercion of integer to real - Unary.
Declaration
Swift
static let opToReal: Z3_decl_kind
-
Coercion of real to integer - Unary.
Declaration
Swift
static let opToInt: Z3_decl_kind
-
Check if real is also an integer - Unary.
Declaration
Swift
static let opIsInt: Z3_decl_kind
-
Power operator x^y.
Declaration
Swift
static let opPower: Z3_decl_kind
-
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.
Declaration
Swift
static let opStore: Z3_decl_kind
-
Array select.
Declaration
Swift
static let opSelect: Z3_decl_kind
-
The constant array. For example, select(const(v),i) = v holds for every v and i. The function is unary.
Declaration
Swift
static let opConstArray: Z3_decl_kind
-
Array map operator. It satisfies mapf[i] = f(a1[i],…,a_n[i]) for every i.
Declaration
Swift
static let opArrayMap: Z3_decl_kind
-
Default value of arrays. For example default(const(v)) = v. The function is unary.
Declaration
Swift
static let opArrayDefault: Z3_decl_kind
-
Set union between two Boolean arrays (two arrays whose range type is Boolean). The function is binary.
Declaration
Swift
static let opSetUnion: Z3_decl_kind
-
Set intersection between two Boolean arrays. The function is binary.
Declaration
Swift
static let opSetIntersect: Z3_decl_kind
-
Set difference between two Boolean arrays. The function is binary.
Declaration
Swift
static let opSetDifference: Z3_decl_kind
-
Set complement of a Boolean array. The function is unary.
Declaration
Swift
static let opSetComplement: Z3_decl_kind
-
Subset predicate between two Boolean arrays. The relation is binary.
Declaration
Swift
static let opSetSubset: Z3_decl_kind
-
An array value that behaves as the function graph of the function passed as parameter.
Declaration
Swift
static let opAsArray: Z3_decl_kind
-
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.
Declaration
Swift
static let opArrayExt: Z3_decl_kind
-
Declaration
Swift
static let opSetHasSize: Z3_decl_kind
-
Declaration
Swift
static let opSetCard: Z3_decl_kind
-
Bit-vector numeral.
Declaration
Swift
static let opBnum: Z3_decl_kind
-
One bit bit-vector.
Declaration
Swift
static let opBit1: Z3_decl_kind
-
Zero bit bit-vector.
Declaration
Swift
static let opBit0: Z3_decl_kind
-
Unary minus.
Declaration
Swift
static let opBneg: Z3_decl_kind
-
Binary addition.
Declaration
Swift
static let opBadd: Z3_decl_kind
-
Binary subtraction.
Declaration
Swift
static let opBsub: Z3_decl_kind
-
Binary multiplication.
Declaration
Swift
static let opBmul: Z3_decl_kind
-
Binary signed division.
Declaration
Swift
static let opBsdiv: Z3_decl_kind
-
Binary unsigned division.
Declaration
Swift
static let opBudiv: Z3_decl_kind
-
Binary signed remainder.
Declaration
Swift
static let opBsrem: Z3_decl_kind
-
Binary unsigned remainder.
Declaration
Swift
static let opBurem: Z3_decl_kind
-
Binary signed modulus.
Declaration
Swift
static let opBsmod: Z3_decl_kind
-
Unary function. bsdiv(x,0) is congruent to bsdiv0(x).
Declaration
Swift
static let opBsdiv0: Z3_decl_kind
-
Unary function. budiv(x,0) is congruent to budiv0(x).
Declaration
Swift
static let opBudiv0: Z3_decl_kind
-
Unary function. bsrem(x,0) is congruent to bsrem0(x).
Declaration
Swift
static let opBsrem0: Z3_decl_kind
-
Unary function. burem(x,0) is congruent to burem0(x).
Declaration
Swift
static let opBurem0: Z3_decl_kind
-
Unary function. bsmod(x,0) is congruent to bsmod0(x).
Declaration
Swift
static let opBsmod0: Z3_decl_kind
-
Unsigned bit-vector <= - Binary relation.
Declaration
Swift
static let opUleq: Z3_decl_kind
-
Signed bit-vector <= - Binary relation.
Declaration
Swift
static let opSleq: Z3_decl_kind
-
Unsigned bit-vector >= - Binary relation.
Declaration
Swift
static let opUgeq: Z3_decl_kind
-
Signed bit-vector >= - Binary relation.
Declaration
Swift
static let opSgeq: Z3_decl_kind
-
Unsigned bit-vector < - Binary relation.
Declaration
Swift
static let opUlt: Z3_decl_kind
-
Signed bit-vector < - Binary relation.
Declaration
Swift
static let opSlt: Z3_decl_kind
-
Unsigned bit-vector > - Binary relation.
Declaration
Swift
static let opUgt: Z3_decl_kind
-
Signed bit-vector > - Binary relation.
Declaration
Swift
static let opSgt: Z3_decl_kind
-
Bit-wise and - Binary.
Declaration
Swift
static let opBand: Z3_decl_kind
-
Bit-wise or - Binary.
Declaration
Swift
static let opBor: Z3_decl_kind
-
Bit-wise not - Unary.
Declaration
Swift
static let opBnot: Z3_decl_kind
-
Bit-wise xor - Binary.
Declaration
Swift
static let opBxor: Z3_decl_kind
-
Bit-wise nand - Binary.
Declaration
Swift
static let opBnand: Z3_decl_kind
-
Bit-wise nor - Binary.
Declaration
Swift
static let opBnor: Z3_decl_kind
-
Bit-wise xnor - Binary.
Declaration
Swift
static let opBxnor: Z3_decl_kind
-
Bit-vector concatenation - Binary.
Declaration
Swift
static let opConcat: Z3_decl_kind
-
Bit-vector sign extension.
Declaration
Swift
static let opSignExt: Z3_decl_kind
-
Bit-vector zero extension.
Declaration
Swift
static let opZeroExt: Z3_decl_kind
-
Bit-vector extraction.
Declaration
Swift
static let opExtract: Z3_decl_kind
-
Repeat bit-vector n times.
Declaration
Swift
static let opRepeat: Z3_decl_kind
-
Bit-vector reduce or - Unary.
Declaration
Swift
static let opBredor: Z3_decl_kind
-
Bit-vector reduce and - Unary.
Declaration
Swift
static let opBredand: Z3_decl_kind
-
.
Declaration
Swift
static let opBcomp: Z3_decl_kind
-
Shift left.
Declaration
Swift
static let opBshl: Z3_decl_kind
-
Logical shift right.
Declaration
Swift
static let opBlshr: Z3_decl_kind
-
Arithmetical shift right.
Declaration
Swift
static let opBashr: Z3_decl_kind
-
Left rotation.
Declaration
Swift
static let opRotateLeft: Z3_decl_kind
-
Right rotation.
Declaration
Swift
static let opRotateRight: Z3_decl_kind
-
(extended) Left rotation. Similar to Z3_OP_ROTATE_LEFT, but it is a binary operator instead of a parametric one.
Declaration
Swift
static let opExtRotateLeft: Z3_decl_kind
-
(extended) Right rotation. Similar to Z3_OP_ROTATE_RIGHT, but it is a binary operator instead of a parametric one.
Declaration
Swift
static let opExtRotateRight: Z3_decl_kind
-
Declaration
Swift
static let opBit2bool: Z3_decl_kind
-
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.
Declaration
Swift
static let opInt2bv: Z3_decl_kind
-
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.
Declaration
Swift
static let opBv2int: Z3_decl_kind
-
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)))
Declaration
Swift
static let opCarry: Z3_decl_kind
-
Compute ternary XOR. The meaning is given by the equivalence (xor3 l1 l2 l3) <=> (xor (xor l1 l2) l3)
Declaration
Swift
static let opXor3: Z3_decl_kind
-
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.
Declaration
Swift
static let opBsmulNoOvfl: Z3_decl_kind
-
check that bit-wise unsigned multiplication does not overflow. Unsigned multiplication overflows if the result does not fit within the available bits. \sa Z3_mk_bvmul_no_overflow.
Declaration
Swift
static let opBumulNoOvfl: Z3_decl_kind
-
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.
Declaration
Swift
static let opBsmulNoUdfl: Z3_decl_kind
-
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.
Declaration
Swift
static let opBsdivI: Z3_decl_kind
-
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.
Declaration
Swift
static let opBudivI: Z3_decl_kind
-
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.
Declaration
Swift
static let opBsremI: Z3_decl_kind
-
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.
Declaration
Swift
static let opBuremI: Z3_decl_kind
-
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.
Declaration
Swift
static let opBsmodI: Z3_decl_kind
-
Undef/Null proof object.
Declaration
Swift
static let opPrUndef: Z3_decl_kind
-
Proof for the expression ‘true’.
Declaration
Swift
static let opPrTrue: Z3_decl_kind
-
Proof for a fact asserted by the user.
Declaration
Swift
static let opPrAsserted: Z3_decl_kind
-
Proof for a fact (tagged as goal) asserted by the user.
Declaration
Swift
static let opPrGoal: Z3_decl_kind
-
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).
Declaration
Swift
static let opPrModusPonens: Z3_decl_kind
-
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’.
Declaration
Swift
static let opPrReflexivity: Z3_decl_kind
-
Given an symmetric relation R and a proof for (R t s), produces a proof for (R s t). \nicebox{ T1: (R t s) [symmetry T1]: (R s t) } T1 is the antecedent of this proof object.
Declaration
Swift
static let opPrSymmetry: Z3_decl_kind
-
Given a transitive relation R, and proofs for (R t s) and (R s u), produces a proof for (R t u). \nicebox{ T1: (R t s) T2: (R s u) [trans T1 T2]: (R t u) }
Declaration
Swift
static let opPrTransitivity: Z3_decl_kind
-
Condensed transitivity proof. It combines several symmetry and transitivity proofs. Example: \nicebox{ 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.
Declaration
Swift
static let opPrTransitivityStar: Z3_decl_kind
-
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.
Declaration
Swift
static let opPrMonotonicity: Z3_decl_kind
-
Given a proof for (~ p q), produces a proof for (~ (forall (x) p) (forall (x) q)).
T1: (~ p q)
Declaration
Swift
static let opPrQuantIntro: Z3_decl_kind
-
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
Declaration
Swift
static let opPrBind: Z3_decl_kind
-
Distributivity proof object. Given that f (= or) distributes over g (= and), produces a proof for \nicebox{ (= (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: \nicebox{ (= (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.
Declaration
Swift
static let opPrDistributivity: Z3_decl_kind
-
Given a proof for (and l_1 … l_n), produces a proof for l_i
T1: (and l_1 … l_n)
Declaration
Swift
static let opPrAndElim: Z3_decl_kind
-
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)
Declaration
Swift
static let opPrNotOrElim: Z3_decl_kind
-
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: \nicebox{ (= (+ x 0) x) (= (+ x 1 2) (+ 3 x)) (iff (or x false) x) }
Declaration
Swift
static let opPrRewrite: Z3_decl_kind
-
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)
Declaration
Swift
static let opPrRewriteStar: Z3_decl_kind
-
A proof for (iff (f (forall (x) q(x)) r) (forall (x) (f (q x) r))). This proof object has no antecedents.
Declaration
Swift
static let opPrPullQuant: Z3_decl_kind
-
A proof for: \nicebox{ (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.
Declaration
Swift
static let opPrPushQuant: Z3_decl_kind
-
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.
Declaration
Swift
static let opPrElimUnusedVars: Z3_decl_kind
-
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.
Declaration
Swift
static let opPrDer: Z3_decl_kind
-
A proof of (or (not (forall (x) (P x))) (P a))
Declaration
Swift
static let opPrQuantInst: Z3_decl_kind
-
Mark a hypothesis in a natural deduction style proof.
Declaration
Swift
static let opPrHypothesis: Z3_decl_kind
-
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.
Declaration
Swift
static let opPrLemma: Z3_decl_kind
-
\nicebox{ 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’) }
Declaration
Swift
static let opPrUnitResolution: Z3_decl_kind
-
\nicebox{ T1: p [iff-true T1]: (iff p true) }
Declaration
Swift
static let opPrIffTrue: Z3_decl_kind
-
\nicebox{ T1: (not p) [iff-false T1]: (iff p false) }
Declaration
Swift
static let opPrIffFalse: Z3_decl_kind
-
f is a commutative operator.
This proof object has no antecedents. Remark: if f is bool, then = is iff.
Declaration
Swift
static let opPrCommutativity: Z3_decl_kind
-
Proof object used to justify Tseitin’s like axioms: \nicebox{ (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).
Declaration
Swift
static let opPrDefAxiom: Z3_decl_kind
-
Clausal proof adding axiom
Declaration
Swift
static let opPrAssumptionAdd: Z3_decl_kind
-
Clausal proof lemma addition
Declaration
Swift
static let opPrLemmaAdd: Z3_decl_kind
-
Clausal proof lemma deletion
Declaration
Swift
static let opPrRedundantDel: Z3_decl_kind
-
Declaration
Swift
static let opPrClauseTrail: Z3_decl_kind
-
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:
or:
when e only occurs positively.
When e is of the form (ite cond th el):
Otherwise: def-intro: (= n e)
Declaration
Swift
static let opPrDefIntro: Z3_decl_kind
-
[apply-def T1]: F ~ n
F is ‘equivalent’ to n, given that T1 is a proof that n is a name for F.
Declaration
Swift
static let opPrApplyDef: Z3_decl_kind
-
T1: (iff p q) [iff~ T1]: (~ p q)
Declaration
Swift
static let opPrIffOeq: Z3_decl_kind
-
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’
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’.
Declaration
Swift
static let opPrNnfPos: Z3_decl_kind
-
Proof for a (negative) NNF step. Examples:
T1: (not s_1) ~ r_1 … Tn: (not s_n) ~ r_n
and
T1: (not s_1) ~ r_1 … Tn: (not s_n) ~ 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’
(and (or r_1 r_2) (or r_1' r_2')))
Declaration
Swift
static let opPrNnfNeg: Z3_decl_kind
-
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.
Declaration
Swift
static let opPrSkolemize: Z3_decl_kind
-
Modus ponens style rule for equi-satisfiability.
T1: p T2: (~ p q)
Declaration
Swift
static let opPrModusPonensOeq: Z3_decl_kind
-
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.
Declaration
Swift
static let opPrThLemma: Z3_decl_kind
-
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 \nicebox{ (or l0 l1 l2 .. ln) } or \nicebox{ (=> (and l1 l2 .. ln) l0) } or in the most general (ground) form: \nicebox{ (=> (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:
\nicebox{ (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.
Declaration
Swift
static let opPrHyperResolve: Z3_decl_kind
-
Insert a record into a relation. The function takes
n
+1 arguments, where the first argument is the relation and the remainingn
elements correspond to then
columns of the relation.Declaration
Swift
static let opRaStore: Z3_decl_kind
-
Creates the empty relation.
Declaration
Swift
static let opRaEmpty: Z3_decl_kind
-
Tests if the relation is empty.
Declaration
Swift
static let opRaIsEmpty: Z3_decl_kind
-
Create the relational join.
Declaration
Swift
static let opRaJoin: Z3_decl_kind
-
Create the union or convex hull of two relations. The function takes two arguments.
Declaration
Swift
static let opRaUnion: Z3_decl_kind
-
Widen two relations. The function takes two arguments.
Declaration
Swift
static let opRaWiden: Z3_decl_kind
-
Project the columns (provided as numbers in the parameters). The function takes one argument.
Declaration
Swift
static let opRaProject: Z3_decl_kind
-
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.
Declaration
Swift
static let opRaFilter: Z3_decl_kind
-
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.
Declaration
Swift
static let opRaNegationFilter: Z3_decl_kind
-
rename columns in the relation. The function takes one argument. The parameters contain the renaming as a cycle.
Declaration
Swift
static let opRaRename: Z3_decl_kind
-
Complement the relation.
Declaration
Swift
static let opRaComplement: Z3_decl_kind
-
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 remainingn
arguments correspond to a record.Declaration
Swift
static let opRaSelect: Z3_decl_kind
-
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.
Declaration
Swift
static let opRaClone: Z3_decl_kind
-
Declaration
Swift
static let opFdConstant: Z3_decl_kind
-
A less than predicate over the finite domain Z3_FINITE_DOMAIN_SORT.
Declaration
Swift
static let opFdLt: Z3_decl_kind
-
Declaration
Swift
static let opSeqUnit: Z3_decl_kind
-
Declaration
Swift
static let opSeqEmpty: Z3_decl_kind
-
Declaration
Swift
static let opSeqConcat: Z3_decl_kind
-
Declaration
Swift
static let opSeqPrefix: Z3_decl_kind
-
Declaration
Swift
static let opSeqSuffix: Z3_decl_kind
-
Declaration
Swift
static let opSeqContains: Z3_decl_kind
-
Declaration
Swift
static let opSeqExtract: Z3_decl_kind
-
Declaration
Swift
static let opSeqReplace: Z3_decl_kind
-
Declaration
Swift
static let opSeqReplaceRe: Z3_decl_kind
-
Declaration
Swift
static let opSeqReplaceReAll: Z3_decl_kind
-
Declaration
Swift
static let opSeqReplaceAll: Z3_decl_kind
-
Declaration
Swift
static let opSeqAt: Z3_decl_kind
-
Declaration
Swift
static let opSeqNth: Z3_decl_kind
-
Declaration
Swift
static let opSeqLength: Z3_decl_kind
-
Declaration
Swift
static let opSeqIndex: Z3_decl_kind
-
Declaration
Swift
static let opSeqLastIndex: Z3_decl_kind
-
Declaration
Swift
static let opSeqToRe: Z3_decl_kind
-
Declaration
Swift
static let opSeqInRe: Z3_decl_kind
-
Declaration
Swift
static let opStrToInt: Z3_decl_kind
-
Declaration
Swift
static let opIntToStr: Z3_decl_kind
-
Declaration
Swift
static let opUbvToStr: Z3_decl_kind
-
Declaration
Swift
static let opSbvToStr: Z3_decl_kind
-
Declaration
Swift
static let opStrToCode: Z3_decl_kind
-
Declaration
Swift
static let opStrFromCode: Z3_decl_kind
-
Declaration
Swift
static let opStringLt: Z3_decl_kind
-
Declaration
Swift
static let opStringLe: Z3_decl_kind
-
Declaration
Swift
static let opRePlus: Z3_decl_kind
-
Declaration
Swift
static let opReStar: Z3_decl_kind
-
Declaration
Swift
static let opReOption: Z3_decl_kind
-
Declaration
Swift
static let opReConcat: Z3_decl_kind
-
Declaration
Swift
static let opReUnion: Z3_decl_kind
-
Declaration
Swift
static let opReRange: Z3_decl_kind
-
Declaration
Swift
static let opReDiff: Z3_decl_kind
-
Declaration
Swift
static let opReIntersect: Z3_decl_kind
-
Declaration
Swift
static let opReLoop: Z3_decl_kind
-
Declaration
Swift
static let opRePower: Z3_decl_kind
-
Declaration
Swift
static let opReComplement: Z3_decl_kind
-
Declaration
Swift
static let opReEmptySet: Z3_decl_kind
-
Declaration
Swift
static let opReFullSet: Z3_decl_kind
-
Declaration
Swift
static let opReFullCharSet: Z3_decl_kind
-
Declaration
Swift
static let opReOfPred: Z3_decl_kind
-
Declaration
Swift
static let opReReverse: Z3_decl_kind
-
Declaration
Swift
static let opReDerivative: Z3_decl_kind
-
Declaration
Swift
static let opCharConst: Z3_decl_kind
-
Declaration
Swift
static let opCharLe: Z3_decl_kind
-
Declaration
Swift
static let opCharToInt: Z3_decl_kind
-
Declaration
Swift
static let opCharToBv: Z3_decl_kind
-
Declaration
Swift
static let opCharFromBv: Z3_decl_kind
-
Declaration
Swift
static let opCharIsDigit: Z3_decl_kind
-
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.
Declaration
Swift
static let opLabel: Z3_decl_kind
-
A label literal (used by the Boogie Verification condition generator). A label literal has a set of string parameters. It takes no arguments.
Declaration
Swift
static let opLabelLit: Z3_decl_kind
-
datatype constructor.
Declaration
Swift
static let opDtConstructor: Z3_decl_kind
-
datatype recognizer.
Declaration
Swift
static let opDtRecogniser: Z3_decl_kind
-
datatype recognizer.
Declaration
Swift
static let opDtIs: Z3_decl_kind
-
datatype accessor.
Declaration
Swift
static let opDtAccessor: Z3_decl_kind
-
datatype field update.
Declaration
Swift
static let opDtUpdateField: Z3_decl_kind
-
Cardinality constraint. E.g., x + y + z <= 2
Declaration
Swift
static let opPbAtMost: Z3_decl_kind
-
Cardinality constraint. E.g., x + y + z >= 2
Declaration
Swift
static let opPbAtLeast: Z3_decl_kind
-
Generalized Pseudo-Boolean cardinality constraint. Example 2*x + 3*y <= 4
Declaration
Swift
static let opPbLe: Z3_decl_kind
-
Generalized Pseudo-Boolean cardinality constraint. Example 2*x + 3*y + 2*z >= 4
Declaration
Swift
static let opPbGe: Z3_decl_kind
-
Generalized Pseudo-Boolean equality constraint. Example 2*x + 1*y + 2*z + 1*u = 4
Declaration
Swift
static let opPbEq: Z3_decl_kind
-
A relation that is a total linear order
Declaration
Swift
static let opSpecialRelationLo: Z3_decl_kind
-
A relation that is a partial order
Declaration
Swift
static let opSpecialRelationPo: Z3_decl_kind
-
A relation that is a piecewise linear order
Declaration
Swift
static let opSpecialRelationPlo: Z3_decl_kind
-
A relation that is a tree order
Declaration
Swift
static let opSpecialRelationTo: Z3_decl_kind
-
Transitive closure of a relation
Declaration
Swift
static let opSpecialRelationTc: Z3_decl_kind
-
Transitive reflexive closure of a relation
Declaration
Swift
static let opSpecialRelationTrc: Z3_decl_kind
-
Floating-point rounding mode RNE
Declaration
Swift
static let opFpaRmNearestTiesToEven: Z3_decl_kind
-
Floating-point rounding mode RNA
Declaration
Swift
static let opFpaRmNearestTiesToAway: Z3_decl_kind
-
Floating-point rounding mode RTP
Declaration
Swift
static let opFpaRmTowardPositive: Z3_decl_kind
-
Floating-point rounding mode RTN
Declaration
Swift
static let opFpaRmTowardNegative: Z3_decl_kind
-
Floating-point rounding mode RTZ
Declaration
Swift
static let opFpaRmTowardZero: Z3_decl_kind
-
Floating-point value
Declaration
Swift
static let opFpaNum: Z3_decl_kind
-
Floating-point +oo
Declaration
Swift
static let opFpaPlusInf: Z3_decl_kind
-
Floating-point -oo
Declaration
Swift
static let opFpaMinusInf: Z3_decl_kind
-
Floating-point NaN
Declaration
Swift
static let opFpaNan: Z3_decl_kind
-
Floating-point +zero
Declaration
Swift
static let opFpaPlusZero: Z3_decl_kind
-
Floating-point -zero
Declaration
Swift
static let opFpaMinusZero: Z3_decl_kind
-
Floating-point addition
Declaration
Swift
static let opFpaAdd: Z3_decl_kind
-
Floating-point subtraction
Declaration
Swift
static let opFpaSub: Z3_decl_kind
-
Floating-point negation
Declaration
Swift
static let opFpaNeg: Z3_decl_kind
-
Floating-point multiplication
Declaration
Swift
static let opFpaMul: Z3_decl_kind
-
Floating-point division
Declaration
Swift
static let opFpaDiv: Z3_decl_kind
-
Floating-point remainder
Declaration
Swift
static let opFpaRem: Z3_decl_kind
-
Floating-point absolute value
Declaration
Swift
static let opFpaAbs: Z3_decl_kind
-
Floating-point minimum
Declaration
Swift
static let opFpaMin: Z3_decl_kind
-
Floating-point maximum
Declaration
Swift
static let opFpaMax: Z3_decl_kind
-
Floating-point fused multiply-add
Declaration
Swift
static let opFpaFma: Z3_decl_kind
-
Floating-point square root
Declaration
Swift
static let opFpaSqrt: Z3_decl_kind
-
Floating-point round to integral
Declaration
Swift
static let opFpaRoundToIntegral: Z3_decl_kind
-
Floating-point equality
Declaration
Swift
static let opFpaEq: Z3_decl_kind
-
Floating-point less than
Declaration
Swift
static let opFpaLt: Z3_decl_kind
-
Floating-point greater than
Declaration
Swift
static let opFpaGt: Z3_decl_kind
-
Floating-point less than or equal
Declaration
Swift
static let opFpaLe: Z3_decl_kind
-
Floating-point greater than or equal
Declaration
Swift
static let opFpaGe: Z3_decl_kind
-
Floating-point isNaN
Declaration
Swift
static let opFpaIsNan: Z3_decl_kind
-
Floating-point isInfinite
Declaration
Swift
static let opFpaIsInf: Z3_decl_kind
-
Floating-point isZero
Declaration
Swift
static let opFpaIsZero: Z3_decl_kind
-
Floating-point isNormal
Declaration
Swift
static let opFpaIsNormal: Z3_decl_kind
-
Floating-point isSubnormal
Declaration
Swift
static let opFpaIsSubnormal: Z3_decl_kind
-
Floating-point isNegative
Declaration
Swift
static let opFpaIsNegative: Z3_decl_kind
-
Floating-point isPositive
Declaration
Swift
static let opFpaIsPositive: Z3_decl_kind
-
Floating-point constructor from 3 bit-vectors
Declaration
Swift
static let opFpaFp: Z3_decl_kind
-
Floating-point conversion (various)
Declaration
Swift
static let opFpaToFp: Z3_decl_kind
-
Floating-point conversion from unsigned bit-vector
Declaration
Swift
static let opFpaToFpUnsigned: Z3_decl_kind
-
Floating-point conversion to unsigned bit-vector
Declaration
Swift
static let opFpaToUbv: Z3_decl_kind
-
Floating-point conversion to signed bit-vector
Declaration
Swift
static let opFpaToSbv: Z3_decl_kind
-
Floating-point conversion to real number
Declaration
Swift
static let opFpaToReal: Z3_decl_kind
-
Floating-point conversion to IEEE-754 bit-vector
Declaration
Swift
static let opFpaToIeeeBv: Z3_decl_kind
-
(Implicitly) represents the internal bitvector- representation of a floating-point term (used for the lazy encoding of non-relevant terms in theory_fpa)
Declaration
Swift
static let opFpaBvwrap: Z3_decl_kind
-
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.
Declaration
Swift
static let opFpaBv2rm: Z3_decl_kind
-
internal (often interpreted) symbol, but no additional information is exposed. Tools may use the string representation of the function declaration to obtain more information.
Declaration
Swift
static let opInternal: Z3_decl_kind
-
function declared as recursive
Declaration
Swift
static let opRecursive: Z3_decl_kind
-
kind used for uninterpreted symbols.
Declaration
Swift
static let opUninterpreted: Z3_decl_kind