Z3_decl_kind class abstract

\brief The different kinds of interpreted function kinds.

Z3_OP_TRUE The constant true.
Z3_OP_FALSE The constant false.
Z3_OP_EQ The equality predicate.
Z3_OP_DISTINCT The n-ary distinct predicate (every argument is mutually distinct).
Z3_OP_ITE The ternary if-then-else term.
Z3_OP_AND n-ary conjunction.
Z3_OP_OR n-ary disjunction.
Z3_OP_IFF equivalence (binary).
Z3_OP_XOR Exclusive or.
Z3_OP_NOT Negation.
Z3_OP_IMPLIES Implication.
Z3_OP_OEQ Binary equivalence modulo namings. This binary predicate is used in proof terms. It captures equisatisfiability and equivalence modulo renamings.
Z3_OP_ANUM Arithmetic numeral.
Z3_OP_AGNUM Arithmetic algebraic numeral. Algebraic numbers are used to represent irrational numbers in Z3.
Z3_OP_LE <=.
Z3_OP_GE >=.
Z3_OP_LT <.
Z3_OP_GT >.
Z3_OP_ADD Addition - Binary.
Z3_OP_SUB Binary subtraction.
Z3_OP_UMINUS Unary minus.
Z3_OP_MUL Multiplication - Binary.
Z3_OP_DIV Division - Binary.
Z3_OP_IDIV Integer division - Binary.
Z3_OP_REM Remainder - Binary.
Z3_OP_MOD Modulus - Binary.
Z3_OP_TO_REAL Coercion of integer to real - Unary.
Z3_OP_TO_INT Coercion of real to integer - Unary.
Z3_OP_IS_INT Check if real is also an integer - Unary.
Z3_OP_POWER Power operator x^y.
Z3_OP_STORE Array store. It satisfies select(store(a,i,v),j) = if i = j then v else select(a,j). Array store takes at least 3 arguments.
Z3_OP_SELECT Array select.
Z3_OP_CONST_ARRAY The constant array. For example, select(const(v),i) = v holds for every v and i. The function is unary.
Z3_OP_ARRAY_DEFAULT Default value of arrays. For example default(const(v)) = v. The function is unary.
Z3_OP_ARRAY_MAP Array map operator. It satisfies mapfi = f(a1i,...,a_ni) for every i.
Z3_OP_SET_UNION Set union between two Boolean arrays (two arrays whose range type is Boolean). The function is binary.
Z3_OP_SET_INTERSECT Set intersection between two Boolean arrays. The function is binary.
Z3_OP_SET_DIFFERENCE Set difference between two Boolean arrays. The function is binary.
Z3_OP_SET_COMPLEMENT Set complement of a Boolean array. The function is unary.
Z3_OP_SET_SUBSET Subset predicate between two Boolean arrays. The relation is binary.
Z3_OP_AS_ARRAY An array value that behaves as the function graph of the function passed as parameter.
Z3_OP_ARRAY_EXT Array extensionality function. It takes two arrays as arguments and produces an index, such that the arrays are different if they are different on the index.
Z3_OP_BNUM Bit-vector numeral.
Z3_OP_BIT1 One bit bit-vector.
Z3_OP_BIT0 Zero bit bit-vector.
Z3_OP_BNEG Unary minus.
Z3_OP_BADD Binary addition.
Z3_OP_BSUB Binary subtraction.
Z3_OP_BMUL Binary multiplication.
Z3_OP_BSDIV Binary signed division.
Z3_OP_BUDIV Binary unsigned division.
Z3_OP_BSREM Binary signed remainder.
Z3_OP_BUREM Binary unsigned remainder.
Z3_OP_BSMOD Binary signed modulus.
Z3_OP_BSDIV0 Unary function. bsdiv(x,0) is congruent to bsdiv0(x).
Z3_OP_BUDIV0 Unary function. budiv(x,0) is congruent to budiv0(x).
Z3_OP_BSREM0 Unary function. bsrem(x,0) is congruent to bsrem0(x).
Z3_OP_BUREM0 Unary function. burem(x,0) is congruent to burem0(x).
Z3_OP_BSMOD0 Unary function. bsmod(x,0) is congruent to bsmod0(x).
Z3_OP_ULEQ Unsigned bit-vector <= - Binary relation.
Z3_OP_SLEQ Signed bit-vector <= - Binary relation.
Z3_OP_UGEQ Unsigned bit-vector >= - Binary relation.
Z3_OP_SGEQ Signed bit-vector >= - Binary relation.
Z3_OP_ULT Unsigned bit-vector < - Binary relation.
Z3_OP_SLT Signed bit-vector < - Binary relation.
Z3_OP_UGT Unsigned bit-vector > - Binary relation.
Z3_OP_SGT Signed bit-vector > - Binary relation.
Z3_OP_BAND Bit-wise and - Binary.
Z3_OP_BOR Bit-wise or - Binary.
Z3_OP_BNOT Bit-wise not - Unary.
Z3_OP_BXOR Bit-wise xor - Binary.
Z3_OP_BNAND Bit-wise nand - Binary.
Z3_OP_BNOR Bit-wise nor - Binary.
Z3_OP_BXNOR Bit-wise xnor - Binary.
Z3_OP_CONCAT Bit-vector concatenation - Binary.
Z3_OP_SIGN_EXT Bit-vector sign extension.
Z3_OP_ZERO_EXT Bit-vector zero extension.
Z3_OP_EXTRACT Bit-vector extraction.
Z3_OP_REPEAT Repeat bit-vector n times.
Z3_OP_BREDOR Bit-vector reduce or - Unary.
Z3_OP_BREDAND Bit-vector reduce and - Unary.
Z3_OP_BCOMP .
Z3_OP_BSHL Shift left.
Z3_OP_BLSHR Logical shift right.
Z3_OP_BASHR Arithmetical shift right.
Z3_OP_ROTATE_LEFT Left rotation.
Z3_OP_ROTATE_RIGHT Right rotation.
Z3_OP_EXT_ROTATE_LEFT (extended) Left rotation. Similar to Z3_OP_ROTATE_LEFT, but it is a binary operator instead of a parametric one.
Z3_OP_EXT_ROTATE_RIGHT (extended) Right rotation. Similar to Z3_OP_ROTATE_RIGHT, but it is a binary operator instead of a parametric one.
Z3_OP_INT2BV Coerce integer to bit-vector. NB. This function is not supported by the decision procedures. Only the most rudimentary simplification rules are applied to this function.
Z3_OP_BV2INT Coerce bit-vector to integer. NB. This function is not supported by the decision procedures. Only the most rudimentary simplification rules are applied to this function.
Z3_OP_CARRY Compute the carry bit in a full-adder. The meaning is given by the equivalence (carry l1 l2 l3) <=> (or (and l1 l2) (and l1 l3) (and l2 l3)))
Z3_OP_XOR3 Compute ternary XOR. The meaning is given by the equivalence (xor3 l1 l2 l3) <=> (xor (xor l1 l2) l3)
Z3_OP_BSMUL_NO_OVFL: 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.
Z3_OP_BUMUL_NO_OVFL: check that bit-wise unsigned multiplication does not overflow. Unsigned multiplication overflows if the result does not fit within the available bits. \sa Z3_mk_bvmul_no_overflow.
Z3_OP_BSMUL_NO_UDFL: check that bit-wise signed multiplication does not underflow. Signed multiplication underflows if the operands have opposite signs and the result of multiplication does not fit within the available bits. Z3_mk_bvmul_no_underflow.
Z3_OP_BSDIV_I: 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.
Z3_OP_BUDIV_I: 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.
Z3_OP_BSREM_I: 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.
Z3_OP_BUREM_I: 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.
Z3_OP_BSMOD_I: 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.
Z3_OP_PR_UNDEF: Undef/Null proof object.
Z3_OP_PR_TRUE: Proof for the expression 'true'.
Z3_OP_PR_ASSERTED: Proof for a fact asserted by the user.
Z3_OP_PR_GOAL: Proof for a fact (tagged as goal) asserted by the user.
Z3_OP_PR_MODUS_PONENS: Given a proof for p and a proof for (implies p q), produces a proof for q.

T1: p T2: (implies p q) mp T1 T2: q

The second antecedents may also be a proof for (iff p q).

Z3_OP_PR_REFLEXIVITY: A proof for (R t t), where R is a reflexive relation. This proof object has no antecedents. The only reflexive relations that are used are equivalence modulo namings, equality and equivalence. That is, R is either '~', '=' or 'iff'.
Z3_OP_PR_SYMMETRY: 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.
Z3_OP_PR_TRANSITIVITY: 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) }
Z3_OP_PR_TRANSITIVITY_STAR: 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.

Z3_OP_PR_MONOTONICITY: Monotonicity proof object.

T1: (R t_1 s_1) ... Tn: (R t_n s_n) monotonicity T1 ... Tn: (R (f t_1 ... t_n) (f s_1 ... s_n))

Remark: if t_i == s_i, then the antecedent Ti is suppressed. That is, reflexivity proofs are suppressed to save space.

Z3_OP_PR_QUANT_INTRO: Given a proof for (~ p q), produces a proof for (~ (forall (x) p) (forall (x) q)).

T1: (~ p q) quant-intro T1: (~ (forall (x) p) (forall (x) q))

Z3_OP_PR_BIND: Given a proof p, produces a proof of lambda x . p, where x are free variables in p.

T1: f proof-bind T1 forall (x) f

Z3_OP_PR_DISTRIBUTIVITY: 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.

Z3_OP_PR_AND_ELIM: Given a proof for (and l_1 ... l_n), produces a proof for l_i

T1: (and l_1 ... l_n) and-elim T1: l_i

Z3_OP_PR_NOT_OR_ELIM: Given a proof for (not (or l_1 ... l_n)), produces a proof for (not l_i).

T1: (not (or l_1 ... l_n)) not-or-elim T1: (not l_i)

Z3_OP_PR_REWRITE: A proof for a local rewriting step (= t s). The head function symbol of t is interpreted.

This proof object has no antecedents. The conclusion of a rewrite rule is either an equality (= t s), an equivalence (iff t s), or equi-satisfiability (~ t s). Remark: if f is bool, then = is iff. Examples: \nicebox{ (= (+ x 0) x) (= (+ x 1 2) (+ 3 x)) (iff (or x false) x) }

Z3_OP_PR_REWRITE_STAR: A proof for rewriting an expression t into an expression s. This proof object can have n antecedents. The antecedents are proofs for equalities used as substitution rules. The 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)
Z3_OP_PR_PULL_QUANT: A proof for (iff (f (forall (x) q(x)) r) (forall (x) (f (q x) r))). This proof object has no antecedents.
Z3_OP_PR_PUSH_QUANT: A proof for: \nicebox{ (iff (forall (x_1 ... x_m) (and p_1x_1 ... x_m ... p_nx_1 ... x_m)) (and (forall (x_1 ... x_m) p_1x_1 ... x_m) ... (forall (x_1 ... x_m) p_nx_1 ... x_m))) } This proof object has no antecedents.
Z3_OP_PR_ELIM_UNUSED_VARS: A proof for (iff (forall (x_1 ... x_n y_1 ... y_m) px_1 ... x_n) (forall (x_1 ... x_n) px_1 ... x_n))

It is used to justify the elimination of unused variables. This proof object has no antecedents.

Z3_OP_PR_DER: A proof for destructive equality resolution: (iff (forall (x) (or (not (= x t)) Px)) Pt) if x does not occur in t.

This proof object has no antecedents.

Several variables can be eliminated simultaneously.

Z3_OP_PR_QUANT_INST: A proof of (or (not (forall (x) (P x))) (P a))
Z3_OP_PR_HYPOTHESIS: Mark a hypothesis in a natural deduction style proof.
Z3_OP_PR_LEMMA:

T1: false lemma T1: (or (not l_1) ... (not l_n))

This proof object has one antecedent: a hypothetical proof for false. It converts the proof in a proof for (or (not l_1) ... (not l_n)), when T1 contains the open hypotheses: l_1, ..., l_n. The hypotheses are closed after an application of a lemma. Furthermore, there are no other open hypotheses in the subtree covered by the lemma.

Z3_OP_PR_UNIT_RESOLUTION: \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') }
Z3_OP_PR_IFF_TRUE: \nicebox{ T1: p iff-true T1: (iff p true) }
Z3_OP_PR_IFF_FALSE: \nicebox{ T1: (not p) iff-false T1: (iff p false) }
Z3_OP_PR_COMMUTATIVITY:

comm: (= (f a b) (f b a))

f is a commutative operator.

This proof object has no antecedents. Remark: if f is bool, then = is iff.

Z3_OP_PR_DEF_AXIOM: 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).
Z3_OP_PR_ASSUMPTION_ADD Clausal proof adding axiom
Z3_OP_PR_LEMMA_ADD Clausal proof lemma addition
Z3_OP_PR_REDUNDANT_DEL Clausal proof lemma deletion
Z3_OP_PR_CLAUSE_TRAIL, Clausal proof trail of additions and deletions
Z3_OP_PR_DEF_INTRO: Introduces a name for a formula/term. Suppose e is an expression with free variables x, and def-intro introduces the name n(x). The possible cases are:

When e is of Boolean type: def-intro: (and (or n (not e)) (or (not n) e))

or: def-intro: (or (not n) e) when e only occurs positively.

When e is of the form (ite cond th el): def-intro: (and (or (not cond) (= n th)) (or cond (= n el)))

Otherwise: def-intro: (= n e)

Z3_OP_PR_APPLY_DEF:

apply-def T1: F ~ n

F is 'equivalent' to n, given that T1 is a proof that n is a name for F.

Z3_OP_PR_IFF_OEQ:

T1: (iff p q) iff~ T1: (~ p q)

Z3_OP_PR_NNF_POS: Proof for a (positive) NNF step. Example:

T1: (not s_1) ~ r_1 T2: (not s_2) ~ r_2 T3: s_1 ~ r_1' T4: s_2 ~ r_2' nnf-pos T1 T2 T3 T4: (~ (iff s_1 s_2) (and (or r_1 r_2') (or r_1' r_2)))

The negation normal form steps NNF_POS and NNF_NEG are used in the following cases: (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'.

Z3_OP_PR_NNF_NEG: Proof for a (negative) NNF step. Examples:

T1: (not s_1) ~ r_1 ... Tn: (not s_n) ~ r_n nnf-neg T1 ... Tn: (not (and s_1 ... s_n)) ~ (or r_1 ... r_n)

and

T1: (not s_1) ~ r_1 ... Tn: (not s_n) ~ r_n nnf-neg T1 ... Tn: (not (or s_1 ... s_n)) ~ (and r_1 ... r_n)

and

T1: (not s_1) ~ r_1 T2: (not s_2) ~ r_2 T3: s_1 ~ r_1' T4: s_2 ~ r_2' nnf-neg T1 T2 T3 T4: (~ (not (iff s_1 s_2)) (and (or r_1 r_2) (or r_1' r_2')))

Z3_OP_PR_SKOLEMIZE: Proof for:

sk: (~ (not (forall x (p x y))) (not (p (sk y) y))) sk: (~ (exists x (p x y)) (p (sk y) y))

This proof object has no antecedents.

Z3_OP_PR_MODUS_PONENS_OEQ: Modus ponens style rule for equi-satisfiability.

T1: p T2: (~ p q) mp~ T1 T2: q

Z3_OP_PR_TH_LEMMA: Generic proof for theory lemmas. The theory lemma function comes with one or more parameters. The first parameter indicates the name of the theory. For the theory of arithmetic, additional parameters provide hints for checking the theory lemma. The hints for arithmetic are:
farkas - followed by rational coefficients. Multiply the coefficients to the inequalities in the lemma, add the (negated) inequalities and obtain a contradiction.
triangle-eq - Indicates a lemma related to the equivalence:

(iff (= t1 t2) (and (<= t1 t2) (<= t2 t1)))

gcd-test - Indicates an integer linear arithmetic lemma that uses a gcd test.
Z3_OP_PR_HYPER_RESOLVE: Hyper-resolution rule.

The premises of the rules is a sequence of clauses. The first clause argument is the main clause of the rule. with a literal from the first (main) clause.

Premises of the rules are of the form \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.

Z3_OP_RA_STORE: Insert a record into a relation. The function takes \c n+1 arguments, where the first argument is the relation and the remaining \c n elements correspond to the \c n columns of the relation.
Z3_OP_RA_EMPTY: Creates the empty relation.
Z3_OP_RA_IS_EMPTY: Tests if the relation is empty.
Z3_OP_RA_JOIN: Create the relational join.
Z3_OP_RA_UNION: Create the union or convex hull of two relations. The function takes two arguments.
Z3_OP_RA_WIDEN: Widen two relations. The function takes two arguments.
Z3_OP_RA_PROJECT: Project the columns (provided as numbers in the parameters). The function takes one argument.
Z3_OP_RA_FILTER: Filter (restrict) a relation with respect to a predicate. The first argument is a relation. The second argument is a predicate with free de-Bruijn indices corresponding to the columns of the relation. So the first column in the relation has index 0.
Z3_OP_RA_NEGATION_FILTER: Intersect the first relation with respect to negation of the second relation (the function takes two arguments). Logically, the specification can be described by a function

target = filter_by_negation(pos, neg, columns)

where columns are pairs c1, d1, .., cN, dN of columns from pos and neg, such that target are elements in x in pos, such that there is no y in neg that agrees with x on the columns c1, d1, .., cN, dN.

Z3_OP_RA_RENAME: rename columns in the relation. The function takes one argument. The parameters contain the renaming as a cycle.
Z3_OP_RA_COMPLEMENT: Complement the relation.
Z3_OP_RA_SELECT: Check if a record is an element of the relation. The function takes \c n+1 arguments, where the first argument is a relation, and the remaining \c n arguments correspond to a record.
Z3_OP_RA_CLONE: Create a fresh copy (clone) of a relation. The function is logically the identity, but in the context of a register machine allows for #Z3_OP_RA_UNION to perform destructive updates to the first argument.
Z3_OP_FD_LT: A less than predicate over the finite domain Z3_FINITE_DOMAIN_SORT.
Z3_OP_LABEL: A label (used by the Boogie Verification condition generator). The label has two parameters, a string and a Boolean polarity. It takes one argument, a formula.
Z3_OP_LABEL_LIT: A label literal (used by the Boogie Verification condition generator). A label literal has a set of string parameters. It takes no arguments.
Z3_OP_DT_CONSTRUCTOR: datatype constructor.
Z3_OP_DT_RECOGNISER: datatype recognizer.
Z3_OP_DT_IS: datatype recognizer.
Z3_OP_DT_ACCESSOR: datatype accessor.
Z3_OP_DT_UPDATE_FIELD: datatype field update.
Z3_OP_PB_AT_MOST: Cardinality constraint. E.g., x + y + z <= 2
Z3_OP_PB_AT_LEAST: Cardinality constraint. E.g., x + y + z >= 2
Z3_OP_PB_LE: Generalized Pseudo-Boolean cardinality constraint. Example 2x + 3y <= 4
Z3_OP_PB_GE: Generalized Pseudo-Boolean cardinality constraint. Example 2x + 3y + 2*z >= 4
Z3_OP_PB_EQ: Generalized Pseudo-Boolean equality constraint. Example 2x + 1y + 2z + 1u = 4
Z3_OP_SPECIAL_RELATION_LO: A relation that is a total linear order
Z3_OP_SPECIAL_RELATION_PO: A relation that is a partial order
Z3_OP_SPECIAL_RELATION_PLO: A relation that is a piecewise linear order
Z3_OP_SPECIAL_RELATION_TO: A relation that is a tree order
Z3_OP_SPECIAL_RELATION_TC: Transitive closure of a relation
Z3_OP_SPECIAL_RELATION_TRC: Transitive reflexive closure of a relation
Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN: Floating-point rounding mode RNE
Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY: Floating-point rounding mode RNA
Z3_OP_FPA_RM_TOWARD_POSITIVE: Floating-point rounding mode RTP
Z3_OP_FPA_RM_TOWARD_NEGATIVE: Floating-point rounding mode RTN
Z3_OP_FPA_RM_TOWARD_ZERO: Floating-point rounding mode RTZ
Z3_OP_FPA_NUM: Floating-point value
Z3_OP_FPA_PLUS_INF: Floating-point +oo
Z3_OP_FPA_MINUS_INF: Floating-point -oo
Z3_OP_FPA_NAN: Floating-point NaN
Z3_OP_FPA_PLUS_ZERO: Floating-point +zero
Z3_OP_FPA_MINUS_ZERO: Floating-point -zero
Z3_OP_FPA_ADD: Floating-point addition
Z3_OP_FPA_SUB: Floating-point subtraction
Z3_OP_FPA_NEG: Floating-point negation
Z3_OP_FPA_MUL: Floating-point multiplication
Z3_OP_FPA_DIV: Floating-point division
Z3_OP_FPA_REM: Floating-point remainder
Z3_OP_FPA_ABS: Floating-point absolute value
Z3_OP_FPA_MIN: Floating-point minimum
Z3_OP_FPA_MAX: Floating-point maximum
Z3_OP_FPA_FMA: Floating-point fused multiply-add
Z3_OP_FPA_SQRT: Floating-point square root
Z3_OP_FPA_ROUND_TO_INTEGRAL: Floating-point round to integral
Z3_OP_FPA_EQ: Floating-point equality
Z3_OP_FPA_LT: Floating-point less than
Z3_OP_FPA_GT: Floating-point greater than
Z3_OP_FPA_LE: Floating-point less than or equal
Z3_OP_FPA_GE: Floating-point greater than or equal
Z3_OP_FPA_IS_NAN: Floating-point isNaN
Z3_OP_FPA_IS_INF: Floating-point isInfinite
Z3_OP_FPA_IS_ZERO: Floating-point isZero
Z3_OP_FPA_IS_NORMAL: Floating-point isNormal
Z3_OP_FPA_IS_SUBNORMAL: Floating-point isSubnormal
Z3_OP_FPA_IS_NEGATIVE: Floating-point isNegative
Z3_OP_FPA_IS_POSITIVE: Floating-point isPositive
Z3_OP_FPA_FP: Floating-point constructor from 3 bit-vectors
Z3_OP_FPA_TO_FP: Floating-point conversion (various)
Z3_OP_FPA_TO_FP_UNSIGNED: Floating-point conversion from unsigned bit-vector
Z3_OP_FPA_TO_UBV: Floating-point conversion to unsigned bit-vector
Z3_OP_FPA_TO_SBV: Floating-point conversion to signed bit-vector
Z3_OP_FPA_TO_REAL: Floating-point conversion to real number
Z3_OP_FPA_TO_IEEE_BV: Floating-point conversion to IEEE-754 bit-vector
Z3_OP_FPA_BVWRAP: (Implicitly) represents the internal bitvector- representation of a floating-point term (used for the lazy encoding of non-relevant terms in theory_fpa)
Z3_OP_FPA_BV2RM: Conversion of a 3-bit bit-vector term to a floating-point rounding-mode term

The conversion uses the following values: 0 = 000 = 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.

Z3_OP_INTERNAL: internal (often interpreted) symbol, but no additional information is exposed. Tools may use the string representation of the function declaration to obtain more information.
Z3_OP_RECURSIVE: function declared as recursive
Z3_OP_UNINTERPRETED: kind used for uninterpreted symbols.

Constructors

Z3_decl_kind()

Properties

hashCode → int: The hash code for this object.
no setterinherited
runtimeType → Type: A representation of the runtime type of the object.
no setterinherited

Methods

noSuchMethod(Invocation invocation) → dynamic: Invoked when a nonexistent method or property is accessed.
inherited
toString() → String: A string representation of this object.
inherited

Operators

operator ==(Object other) → bool: The equality operator.
inherited

Constants

OP_ADD → const int
OP_AGNUM → const int
OP_AND → const int
OP_ANUM → const int
OP_ARRAY_DEFAULT → const int
OP_ARRAY_EXT → const int
OP_ARRAY_MAP → const int
OP_AS_ARRAY → const int
OP_BADD → const int
OP_BAND → const int
OP_BASHR → const int
OP_BCOMP → const int
OP_BIT0 → const int
OP_BIT1 → const int
OP_BIT2BOOL → const int
OP_BLSHR → const int
OP_BMUL → const int
OP_BNAND → const int
OP_BNEG → const int
OP_BNOR → const int
OP_BNOT → const int
OP_BNUM → const int
OP_BOR → const int
OP_BREDAND → const int
OP_BREDOR → const int
OP_BSDIV → const int
OP_BSDIV0 → const int
OP_BSDIV_I → const int
OP_BSHL → const int
OP_BSMOD → const int
OP_BSMOD0 → const int
OP_BSMOD_I → const int
OP_BSMUL_NO_OVFL → const int
OP_BSMUL_NO_UDFL → const int
OP_BSREM → const int
OP_BSREM0 → const int
OP_BSREM_I → const int
OP_BSUB → const int
OP_BUDIV → const int
OP_BUDIV0 → const int
OP_BUDIV_I → const int
OP_BUMUL_NO_OVFL → const int
OP_BUREM → const int
OP_BUREM0 → const int
OP_BUREM_I → const int
OP_BV2INT → const int
OP_BXNOR → const int
OP_BXOR → const int
OP_CARRY → const int
OP_CHAR_CONST → const int
OP_CHAR_FROM_BV → const int
OP_CHAR_IS_DIGIT → const int
OP_CHAR_LE → const int
OP_CHAR_TO_BV → const int
OP_CHAR_TO_INT → const int
OP_CONCAT → const int
OP_CONST_ARRAY → const int
OP_DISTINCT → const int
OP_DIV → const int
OP_DT_ACCESSOR → const int
OP_DT_CONSTRUCTOR → const int
OP_DT_IS → const int
OP_DT_RECOGNISER → const int
OP_DT_UPDATE_FIELD → const int
OP_EQ → const int
OP_EXT_ROTATE_LEFT → const int
OP_EXT_ROTATE_RIGHT → const int
OP_EXTRACT → const int
OP_FALSE → const int
OP_FD_CONSTANT → const int
OP_FD_LT → const int
OP_FPA_ABS → const int
OP_FPA_ADD → const int
OP_FPA_BV2RM → const int
OP_FPA_BVWRAP → const int
OP_FPA_DIV → const int
OP_FPA_EQ → const int
OP_FPA_FMA → const int
OP_FPA_FP → const int
OP_FPA_GE → const int
OP_FPA_GT → const int
OP_FPA_IS_INF → const int
OP_FPA_IS_NAN → const int
OP_FPA_IS_NEGATIVE → const int
OP_FPA_IS_NORMAL → const int
OP_FPA_IS_POSITIVE → const int
OP_FPA_IS_SUBNORMAL → const int
OP_FPA_IS_ZERO → const int
OP_FPA_LE → const int
OP_FPA_LT → const int
OP_FPA_MAX → const int
OP_FPA_MIN → const int
OP_FPA_MINUS_INF → const int
OP_FPA_MINUS_ZERO → const int
OP_FPA_MUL → const int
OP_FPA_NAN → const int
OP_FPA_NEG → const int
OP_FPA_NUM → const int
OP_FPA_PLUS_INF → const int
OP_FPA_PLUS_ZERO → const int
OP_FPA_REM → const int
OP_FPA_RM_NEAREST_TIES_TO_AWAY → const int
OP_FPA_RM_NEAREST_TIES_TO_EVEN → const int
OP_FPA_RM_TOWARD_NEGATIVE → const int
OP_FPA_RM_TOWARD_POSITIVE → const int
OP_FPA_RM_TOWARD_ZERO → const int
OP_FPA_ROUND_TO_INTEGRAL → const int
OP_FPA_SQRT → const int
OP_FPA_SUB → const int
OP_FPA_TO_FP → const int
OP_FPA_TO_FP_UNSIGNED → const int
OP_FPA_TO_IEEE_BV → const int
OP_FPA_TO_REAL → const int
OP_FPA_TO_SBV → const int
OP_FPA_TO_UBV → const int
OP_GE → const int
OP_GT → const int
OP_IDIV → const int
OP_IFF → const int
OP_IMPLIES → const int
OP_INT2BV → const int
OP_INT_TO_STR → const int
OP_INTERNAL → const int
OP_IS_INT → const int
OP_ITE → const int
OP_LABEL → const int
OP_LABEL_LIT → const int
OP_LE → const int
OP_LT → const int
OP_MOD → const int
OP_MUL → const int
OP_NOT → const int
OP_OEQ → const int
OP_OR → const int
OP_PB_AT_LEAST → const int
OP_PB_AT_MOST → const int
OP_PB_EQ → const int
OP_PB_GE → const int
OP_PB_LE → const int
OP_POWER → const int
OP_PR_AND_ELIM → const int
OP_PR_APPLY_DEF → const int
OP_PR_ASSERTED → const int
OP_PR_ASSUMPTION_ADD → const int
OP_PR_BIND → const int
OP_PR_CLAUSE_TRAIL → const int
OP_PR_COMMUTATIVITY → const int
OP_PR_DEF_AXIOM → const int
OP_PR_DEF_INTRO → const int
OP_PR_DER → const int
OP_PR_DISTRIBUTIVITY → const int
OP_PR_ELIM_UNUSED_VARS → const int
OP_PR_GOAL → const int
OP_PR_HYPER_RESOLVE → const int
OP_PR_HYPOTHESIS → const int
OP_PR_IFF_FALSE → const int
OP_PR_IFF_OEQ → const int
OP_PR_IFF_TRUE → const int
OP_PR_LEMMA → const int
OP_PR_LEMMA_ADD → const int
OP_PR_MODUS_PONENS → const int
OP_PR_MODUS_PONENS_OEQ → const int
OP_PR_MONOTONICITY → const int
OP_PR_NNF_NEG → const int
OP_PR_NNF_POS → const int
OP_PR_NOT_OR_ELIM → const int
OP_PR_PULL_QUANT → const int
OP_PR_PUSH_QUANT → const int
OP_PR_QUANT_INST → const int
OP_PR_QUANT_INTRO → const int
OP_PR_REDUNDANT_DEL → const int
OP_PR_REFLEXIVITY → const int
OP_PR_REWRITE → const int
OP_PR_REWRITE_STAR → const int
OP_PR_SKOLEMIZE → const int
OP_PR_SYMMETRY → const int
OP_PR_TH_LEMMA → const int
OP_PR_TRANSITIVITY → const int
OP_PR_TRANSITIVITY_STAR → const int
OP_PR_TRUE → const int
OP_PR_UNDEF → const int
OP_PR_UNIT_RESOLUTION → const int
OP_RA_CLONE → const int
OP_RA_COMPLEMENT → const int
OP_RA_EMPTY → const int
OP_RA_FILTER → const int
OP_RA_IS_EMPTY → const int
OP_RA_JOIN → const int
OP_RA_NEGATION_FILTER → const int
OP_RA_PROJECT → const int
OP_RA_RENAME → const int
OP_RA_SELECT → const int
OP_RA_STORE → const int
OP_RA_UNION → const int
OP_RA_WIDEN → const int
OP_RE_COMPLEMENT → const int
OP_RE_CONCAT → const int
OP_RE_DERIVATIVE → const int
OP_RE_DIFF → const int
OP_RE_EMPTY_SET → const int
OP_RE_FULL_CHAR_SET → const int
OP_RE_FULL_SET → const int
OP_RE_INTERSECT → const int
OP_RE_LOOP → const int
OP_RE_OF_PRED → const int
OP_RE_OPTION → const int
OP_RE_PLUS → const int
OP_RE_POWER → const int
OP_RE_RANGE → const int
OP_RE_REVERSE → const int
OP_RE_STAR → const int
OP_RE_UNION → const int
OP_RECURSIVE → const int
OP_REM → const int
OP_REPEAT → const int
OP_ROTATE_LEFT → const int
OP_ROTATE_RIGHT → const int
OP_SBV_TO_STR → const int
OP_SELECT → const int
OP_SEQ_AT → const int
OP_SEQ_CONCAT → const int
OP_SEQ_CONTAINS → const int
OP_SEQ_EMPTY → const int
OP_SEQ_EXTRACT → const int
OP_SEQ_IN_RE → const int
OP_SEQ_INDEX → const int
OP_SEQ_LAST_INDEX → const int
OP_SEQ_LENGTH → const int
OP_SEQ_NTH → const int
OP_SEQ_PREFIX → const int
OP_SEQ_REPLACE → const int
OP_SEQ_REPLACE_ALL → const int
OP_SEQ_REPLACE_RE → const int
OP_SEQ_REPLACE_RE_ALL → const int
OP_SEQ_SUFFIX → const int
OP_SEQ_TO_RE → const int
OP_SEQ_UNIT → const int
OP_SET_CARD → const int
OP_SET_COMPLEMENT → const int
OP_SET_DIFFERENCE → const int
OP_SET_HAS_SIZE → const int
OP_SET_INTERSECT → const int
OP_SET_SUBSET → const int
OP_SET_UNION → const int
OP_SGEQ → const int
OP_SGT → const int
OP_SIGN_EXT → const int
OP_SLEQ → const int
OP_SLT → const int
OP_SPECIAL_RELATION_LO → const int
OP_SPECIAL_RELATION_PLO → const int
OP_SPECIAL_RELATION_PO → const int
OP_SPECIAL_RELATION_TC → const int
OP_SPECIAL_RELATION_TO → const int
OP_SPECIAL_RELATION_TRC → const int
OP_STORE → const int
OP_STR_FROM_CODE → const int
OP_STR_TO_CODE → const int
OP_STR_TO_INT → const int
OP_STRING_LE → const int
OP_STRING_LT → const int
OP_SUB → const int
OP_TO_INT → const int
OP_TO_REAL → const int
OP_TRUE → const int
OP_UBV_TO_STR → const int
OP_UGEQ → const int
OP_UGT → const int
OP_ULEQ → const int
OP_ULT → const int
OP_UMINUS → const int
OP_UNINTERPRETED → const int
OP_XOR → const int
OP_XOR3 → const int
OP_ZERO_EXT → const int