Home - News ( United States | United Kingdom | Italy | Germany ) - Football scores

Showing content from https://z3prover.github.io/api/html/group__capi.html below:

Z3: C API

Definition at line 339 of file z3_fixedpoint.h.

Definition at line 340 of file z3_fixedpoint.h.

Definition at line 318 of file z3_fixedpoint.h.

The following utilities allows adding user-defined domains.

Definition at line 313 of file z3_fixedpoint.h.

Definition at line 341 of file z3_fixedpoint.h.

Z3 string type. It is just an alias for const char *.

Most of the types in the C API are opaque pointers.

• Z3_config: configuration object used to initialize logical contexts.
• Z3_context: manager of all other Z3 objects, global configuration options, etc.
• Z3_symbol: Lisp-like symbol used to name types, constants, and functions. A symbol can be created using string or integers.
• Z3_ast: abstract syntax tree node. That is, the data-structure used in Z3 to represent terms, formulas and types.
• Z3_sort: kind of AST used to represent types.
• Z3_func_decl: kind of AST used to represent function symbols.
• Z3_app: kind of AST used to represent function applications.
• Z3_pattern: kind of AST used to represent pattern and multi-patterns used to guide quantifier instantiation.
• Z3_constructor: type constructor for a (recursive) datatype.
• Z3_constructor_list: list of constructors for a (recursive) datatype.
• Z3_params: parameter set used to configure many components such as: simplifiers, tactics, solvers, etc.
• Z3_param_descrs: provides a collection of parameter names, their types, default values and documentation strings. Solvers, tactics, and other objects accept different collection of parameters.
• Z3_parser_context: context for incrementally parsing strings. Declarations can be added incrementally to the parser state.
• Z3_model: model for the constraints asserted into the logical context.
• Z3_func_interp: interpretation of a function in a model.
• Z3_func_entry: representation of the value of a Z3_func_interp at a particular point.
• Z3_fixedpoint: context for the recursive predicate solver.
• Z3_optimize: context for solving optimization queries.
• Z3_ast_vector: vector of Z3_ast objects.
• Z3_ast_map: mapping from Z3_ast to Z3_ast objects.
• Z3_goal: set of formulas that can be solved and/or transformed using tactics and solvers.
• Z3_tactic: basic building block for creating custom solvers for specific problem domains.
• Z3_simplifier: basic building block for creating custom pre-processing simplifiers.
• Z3_probe: function/predicate used to inspect a goal and collect information that may be used to decide which solver and/or preprocessing step will be used.
• Z3_apply_result: collection of subgoals resulting from applying of a tactic to a goal.
• Z3_solver: (incremental) solver, possibly specialized by a particular tactic or logic.
• Z3_stats: statistical data for a solver.

Definition at line 53 of file z3_api.h.

The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types.

• Z3_APP_AST: constant and applications
• Z3_NUMERAL_AST: numeral constants
• Z3_VAR_AST: bound variables
• Z3_QUANTIFIER_AST: quantifiers
• Z3_SORT_AST: sort
• Z3_FUNC_DECL_AST: function declaration
• Z3_UNKNOWN_AST: internal

Definition at line 140 of file z3_api.h.

Z3_ast_kind

The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types.

Z3 pretty printing modes (See Z3_set_ast_print_mode).

• Z3_PRINT_SMTLIB_FULL: Print AST nodes in SMTLIB verbose format.
• Z3_PRINT_LOW_LEVEL: Print AST nodes using a low-level format.
• Z3_PRINT_SMTLIB2_COMPLIANT: Print AST nodes in SMTLIB 2.x compliant format.

Definition at line 1324 of file z3_api.h.

Z3_ast_print_mode

Z3 pretty printing modes (See Z3_set_ast_print_mode).

@ Z3_PRINT_SMTLIB2_COMPLIANT

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 mapf[i] = f(a1[i],...,a_n[i]) 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.

  See also

  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.

  See also

  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).

         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).

      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:

         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)
  

• 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

         (= (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.

• 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)

• 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:

         (= (+ 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:

         (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.

• Z3_OP_PR_ELIM_UNUSED_VARS: A proof for (iff (forall (x_1 ... x_n y_1 ... y_m) p[x_1 ... x_n]) (forall (x_1 ... x_n) p[x_1 ... x_n]))

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

• Z3_OP_PR_DER: A proof for destructive equality resolution: (iff (forall (x) (or (not (= x t)) P[x])) P[t]) if x does not occur in t.

  This proof object has no antecedents.

  Several variables can be eliminated simultaneously.

• 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:

         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:

      T1: p
      [iff-true T1]: (iff p true)
      

• Z3_OP_PR_IFF_FALSE:

      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:

         (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:

  or:

  when e only occurs positively.

  When e is of the form (ite cond th 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

  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.

• Z3_OP_RA_STORE: Insert a record into a relation. The function takes n+1 arguments, where the first argument is the relation and the remaining n elements correspond to the n columns of the relation.
• 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 n+1 arguments, where the first argument is a relation, and the remaining 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 2*x + 3*y <= 4
• Z3_OP_PB_GE: Generalized Pseudo-Boolean cardinality constraint. Example 2*x + 3*y + 2*z >= 4
• Z3_OP_PB_EQ: Generalized Pseudo-Boolean equality constraint. Example 2*x + 1*y + 2*z + 1*u = 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.

Definition at line 963 of file z3_api.h.

Z3_decl_kind

The different kinds of interpreted function kinds.

@ Z3_OP_FPA_ROUND_TO_INTEGRAL

@ Z3_OP_PR_UNIT_RESOLUTION

@ Z3_OP_SPECIAL_RELATION_TRC

@ Z3_OP_PR_MODUS_PONENS_OEQ

@ Z3_OP_FPA_RM_TOWARD_NEGATIVE

@ Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN

@ Z3_OP_PR_ELIM_UNUSED_VARS

@ Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY

@ Z3_OP_FPA_RM_TOWARD_ZERO

@ Z3_OP_FPA_RM_TOWARD_POSITIVE

@ Z3_OP_SPECIAL_RELATION_PO

@ Z3_OP_SPECIAL_RELATION_TC

@ Z3_OP_SPECIAL_RELATION_TO

@ Z3_OP_FPA_TO_FP_UNSIGNED

@ Z3_OP_RA_NEGATION_FILTER

@ Z3_OP_SPECIAL_RELATION_PLO

@ Z3_OP_PR_ASSUMPTION_ADD

@ Z3_OP_PR_TRANSITIVITY_STAR

@ Z3_OP_SEQ_REPLACE_RE_ALL

@ Z3_OP_SPECIAL_RELATION_LO

@ Z3_OP_PR_DISTRIBUTIVITY

Z3 error codes (See Z3_get_error_code).

• Z3_OK: No error.
• Z3_SORT_ERROR: User tried to build an invalid (type incorrect) AST.
• Z3_IOB: Index out of bounds.
• Z3_INVALID_ARG: Invalid argument was provided.
• Z3_PARSER_ERROR: An error occurred when parsing a string or file.
• Z3_NO_PARSER: Parser output is not available, that is, user didn't invoke Z3_parse_smtlib2_string or Z3_parse_smtlib2_file.
• Z3_INVALID_PATTERN: Invalid pattern was used to build a quantifier.
• Z3_MEMOUT_FAIL: A memory allocation failure was encountered.
• Z3_FILE_ACCESS_ERROR: A file could not be accessed.
• Z3_INVALID_USAGE: API call is invalid in the current state.
• Z3_INTERNAL_FATAL: An error internal to Z3 occurred.
• Z3_DEC_REF_ERROR: Trying to decrement the reference counter of an AST that was deleted or the reference counter was not initialized with Z3_inc_ref.
• Z3_EXCEPTION: Internal Z3 exception. Additional details can be retrieved using Z3_get_error_msg.

Definition at line 1348 of file z3_api.h.

Z3_error_code

Z3 error codes (See Z3_get_error_code).

Z3 custom error handler (See Z3_set_error_handler).

Definitions for update_api.py

callback functions for user propagator.

A Goal is essentially a set of formulas. Z3 provide APIs for building strategies/tactics for solving and transforming Goals. Some of these transformations apply under/over approximations.

• Z3_GOAL_PRECISE: Approximations/Relaxations were not applied on the goal (sat and unsat answers were preserved).
• Z3_GOAL_UNDER: Goal is the product of a under-approximation (sat answers are preserved).
• Z3_GOAL_OVER: Goal is the product of an over-approximation (unsat answers are preserved).
• Z3_GOAL_UNDER_OVER: Goal is garbage (it is the product of over- and under-approximations, sat and unsat answers are not preserved).

Definition at line 1389 of file z3_api.h.

Z3_goal_prec

Z3 custom error handler (See Z3_set_error_handler).

Lifted Boolean type: false, undefined, true.

Definition at line 60 of file z3_api.h.

Z3_lbool

Lifted Boolean type: false, undefined, true.

The different kinds of parameters that can be associated with parameter sets. (see Z3_mk_params).

• Z3_PK_UINT integer parameters.
• Z3_PK_BOOL boolean parameters.
• Z3_PK_DOUBLE double parameters.
• Z3_PK_SYMBOL symbol parameters.
• Z3_PK_STRING string parameters.
• Z3_PK_OTHER all internal parameter kinds which are not exposed in the API.
• Z3_PK_INVALID invalid parameter.

Definition at line 1307 of file z3_api.h.

Z3_param_kind

The different kinds of parameters that can be associated with parameter sets. (see Z3_mk_params).

The different kinds of parameters that can be associated with function symbols.

See also

Z3_get_decl_num_parameters

Z3_get_decl_parameter_kind

• Z3_PARAMETER_INT is used for integer parameters.
• Z3_PARAMETER_DOUBLE is used for double parameters.
• Z3_PARAMETER_RATIONAL is used for parameters that are rational numbers.
• Z3_PARAMETER_SYMBOL is used for parameters that are symbols.
• Z3_PARAMETER_SORT is used for sort parameters.
• Z3_PARAMETER_AST is used for expression parameters.
• Z3_PARAMETER_FUNC_DECL is used for function declaration parameters.

Definition at line 94 of file z3_api.h.

Z3_parameter_kind

The different kinds of parameters that can be associated with function symbols.

The different kinds of Z3 types (See Z3_get_sort_kind).

Definition at line 108 of file z3_api.h.

Z3_sort_kind

The different kinds of Z3 types (See Z3_get_sort_kind).

The different kinds of symbol. In Z3, a symbol can be represented using integers and strings (See Z3_get_symbol_kind).

See also

Z3_mk_int_symbol

Z3_mk_string_symbol

Definition at line 74 of file z3_api.h.

Z3_symbol_kind

The different kinds of symbol. In Z3, a symbol can be represented using integers and strings (See Z3_...

Create a fresh func_interp object, add it to a model for a specified function. It has reference count 0.

Parameters

c context m model f function declaration default_value default value for function interpretation

Referenced by model::add_func_interp(), and ModelRef::update_value().

Define the body of a recursive function.

Parameters

c logical context. f function declaration. n number of arguments to the function args constants that are used as arguments to the recursive function in the definition. body body of the recursive function

After declaring a recursive function or a collection of mutually recursive functions, use this function to provide the definition for the recursive function.

See also

Z3_mk_rec_func_decl

Referenced by z3py::RecAddDefinition(), and context::recdef().

Return the value a + b.

Precondition

Z3_algebraic_is_value(c, a)

Z3_algebraic_is_value(c, b)

Postcondition

Z3_algebraic_is_value(c, result)

Return the value a / b.

Precondition

Z3_algebraic_is_value(c, a)

Z3_algebraic_is_value(c, b)

!Z3_algebraic_is_zero(c, b)

Postcondition

Z3_algebraic_is_value(c, result)

Return true if a == b, and false otherwise.

Precondition

Z3_algebraic_is_value(c, a)

Z3_algebraic_is_value(c, b)

Given a multivariate polynomial p(x_0, ..., x_{n-1}), return the sign of p(a[0], ..., a[n-1]).

Precondition

p is a Z3 expression that contains only arithmetic terms and free variables.

forall i in [0, n) Z3_algebraic_is_value(c, a[i])

Return true if a >= b, and false otherwise.

Precondition

Z3_algebraic_is_value(c, a)

Z3_algebraic_is_value(c, b)

Return true if a > b, and false otherwise.

Precondition

Z3_algebraic_is_value(c, a)

Z3_algebraic_is_value(c, b)

Return true if a is negative, and false otherwise.

Precondition

Z3_algebraic_is_value(c, a)

Return true if a is positive, and false otherwise.

Precondition

Z3_algebraic_is_value(c, a)

Return true if a can be used as value in the Z3 real algebraic number package.

Return true if a is zero, and false otherwise.

Precondition

Z3_algebraic_is_value(c, a)

Return true if a <= b, and false otherwise.

Precondition

Z3_algebraic_is_value(c, a)

Z3_algebraic_is_value(c, b)

Return true if a < b, and false otherwise.

Precondition

Z3_algebraic_is_value(c, a)

Z3_algebraic_is_value(c, b)

Return the value a * b.

Precondition

Z3_algebraic_is_value(c, a)

Z3_algebraic_is_value(c, b)

Postcondition

Z3_algebraic_is_value(c, result)

Return true if a != b, and false otherwise.

Precondition

Z3_algebraic_is_value(c, a)

Z3_algebraic_is_value(c, b)

Return the a^k.

Precondition

Z3_algebraic_is_value(c, a)

Postcondition

Z3_algebraic_is_value(c, result)

Return the a^(1/k)

Precondition

Z3_algebraic_is_value(c, a)

k is even => !Z3_algebraic_is_neg(c, a)

Postcondition

Z3_algebraic_is_value(c, result)

Given a multivariate polynomial p(x_0, ..., x_{n-1}, x_n), returns the roots of the univariate polynomial p(a[0], ..., a[n-1], x_n).

Precondition

p is a Z3 expression that contains only arithmetic terms and free variables.

forall i in [0, n) Z3_algebraic_is_value(c, a[i])

Postcondition

forall r in result Z3_algebraic_is_value(c, result)

Return 1 if a is positive, 0 if a is zero, and -1 if a is negative.

Precondition

Z3_algebraic_is_value(c, a)

Return the value a - b.

Precondition

Z3_algebraic_is_value(c, a)

Z3_algebraic_is_value(c, b)

Postcondition

Z3_algebraic_is_value(c, result)

Convert a Z3_app into Z3_ast. This is just type casting.

Append user-defined string to interaction log.

The interaction log is opened using Z3_open_log. It contains the formulas that are checked using Z3. You can use this command to append comments, for instance.

See also

Z3_open_log

Z3_close_log

Referenced by z3py::append_log().

Decrement the reference counter of the given AST map.

Referenced by AstMap::__del__().

Return the value associated with the key k.

The procedure invokes the error handler if k is not in the map.

Referenced by AstMap::__getitem__().

Increment the reference counter of the given AST map.

Return the keys stored in the given map.

Referenced by AstMap::keys().

Convert the given benchmark into SMT-LIB formatted string.

Warning

The result buffer is statically allocated by Z3. It will be automatically deallocated when Z3_del_context is invoked. So, the buffer is invalidated in the next call to Z3_benchmark_to_smtlib_string.

Parameters

c - context. name - name of benchmark. The argument is optional. logic - the benchmark logic. status - the status string (sat, unsat, or unknown) attributes - other attributes, such as source, difficulty or category. num_assumptions - number of assumptions. assumptions - auxiliary assumptions. formula - formula to be checked for consistency in conjunction with assumptions.

Referenced by solver::to_smt2(), and Solver::to_smt2().

Retrieve the number of fields of a constructor.

Parameters

c logical context. constr constructor.

Update record field with a value.

This corresponds to the 'with' construct in OCaml. It has the effect of updating a record field with a given value. The remaining fields are left unchanged. It is the record equivalent of an array store (see

See also

Z3_mk_store). If the datatype has more than one constructor, then the update function behaves as identity if there is a mismatch between the accessor and constructor. For example ((_ update-field car) nil 1) is nil, while ((_ update-field car) (cons 2 nil) 1) is (cons 1 nil).

Precondition

Z3_get_sort_kind(Z3_get_sort(c, t)) == Z3_get_domain(c, field_access, 1) == Z3_DATATYPE_SORT

Z3_get_sort(c, value) == Z3_get_range(c, field_access)

use concurrency control for dec-ref. Reference counting decrements are allowed in separate threads from the context. If this setting is not invoked, reference counting decrements are not going to be thread safe.

Parse and evaluate and SMT-LIB2 command sequence. The state from a previous call is saved so the next evaluation builds on top of the previous call.

Returns

output generated from processing commands.

Destroy all allocated resources.

Any pointers previously returned by the API become invalid. Can be used for memory leak detection.

set export callback for lemmas

Add property about the predicate pred. Add a property of predicate pred at level. It gets pushed forward when possible.

Note: level = -1 is treated as the fixedpoint. So passing -1 for the level means that the property is true of the fixed-point unfolding with respect to pred.

Note: this functionality is PDR specific.

Referenced by fixedpoint::add_cover(), and Fixedpoint::add_cover().

Add a Database fact.

Parameters

c - context d - fixed point context r - relation signature for the row. num_args - number of columns for the given row. args - array of the row elements.

The number of arguments num_args should be equal to the number of sorts in the domain of r. Each sort in the domain should be an integral (bit-vector, Boolean or or finite domain sort).

The call has the same effect as adding a rule where r is applied to the arguments.

Referenced by fixedpoint::add_fact().

Add a universal Horn clause as a named rule. The horn_rule should be of the form:

horn_rule ::= (

(bound-vars) horn_rule)

| (=> atoms horn_rule)

| atom

expr forall(expr const &x, expr const &b)

Referenced by fixedpoint::add_rule(), and Fixedpoint::add_rule().

Assert a constraint to the fixedpoint context.

The constraints are used as background axioms when the fixedpoint engine uses the PDR mode. They are ignored for standard Datalog mode.

Referenced by Fixedpoint::assert_exprs().

Retrieve a formula that encodes satisfying answers to the query.

When used in Datalog mode, the returned answer is a disjunction of conjuncts. Each conjunct encodes values of the bound variables of the query that are satisfied. In PDR mode, the returned answer is a single conjunction.

When used in Datalog mode the previous call to Z3_fixedpoint_query must have returned Z3_L_TRUE. When used with the PDR engine, the previous call must have been either Z3_L_TRUE or Z3_L_FALSE.

Referenced by fixedpoint::get_answer(), and Fixedpoint::get_answer().

Retrieve the current cover of pred up to level unfoldings. Return just the delta that is known at level. To obtain the full set of properties of pred one should query at level+1 , level+2 etc, and include level=-1.

Note: this functionality is PDR specific.

Referenced by fixedpoint::get_cover_delta(), and Fixedpoint::get_cover_delta().

Query the PDR engine for the maximal levels properties are known about predicate.

This call retrieves the maximal number of relevant unfoldings of pred with respect to the current exploration state. Note: this functionality is PDR specific.

Referenced by fixedpoint::get_num_levels(), and Fixedpoint::get_num_levels().

Initialize the context with a user-defined state.

Pose a query against the asserted rules.

query ::= (

(bound-vars) query)

| literals

expr exists(expr const &x, expr const &b)

query returns

• Z3_L_FALSE if the query is unsatisfiable.
• Z3_L_TRUE if the query is satisfiable. Obtain the answer by calling Z3_fixedpoint_get_answer.
• Z3_L_UNDEF if the query was interrupted, timed out or otherwise failed.

Referenced by fixedpoint::query(), and Fixedpoint::query().

Pose multiple queries against the asserted rules.

The queries are encoded as relations (function declarations).

query returns

• Z3_L_FALSE if the query is unsatisfiable.
• Z3_L_TRUE if the query is satisfiable. Obtain the answer by calling Z3_fixedpoint_get_answer.
• Z3_L_UNDEF if the query was interrupted, timed out or otherwise failed.

Referenced by fixedpoint::query(), and Fixedpoint::query().

Configure the predicate representation.

It sets the predicate to use a set of domains given by the list of symbols. The domains given by the list of symbols must belong to a set of built-in domains.

Referenced by Fixedpoint::set_predicate_representation().

Register a callback for building terms based on the relational operators.

Register a callback to destructive updates.

Registers are identified with terms encoded as fresh constants,

Retrieves the exponent of a floating-point literal as a bit-vector expression.

Parameters

c logical context t a floating-point numeral biased flag to indicate whether the result is in biased representation

Remarks: This function extracts the exponent in t, without normalization. NaN is an invalid arguments.

Referenced by FPNumRef::exponent_as_bv().

Return the exponent value of a floating-point numeral as a signed 64-bit integer.

Parameters

c logical context t a floating-point numeral n exponent biased flag to indicate whether the result is in biased representation

Returns

true if t corresponds to a floating point numeral, otherwise invokes exception handler or returns false

Remarks: This function extracts the exponent in t, without normalization. NaN is an invalid argument.

Referenced by FPNumRef::exponent_as_long().

Return the exponent value of a floating-point numeral as a string.

Parameters

c logical context t a floating-point numeral biased flag to indicate whether the result is in biased representation

Returns

true if t corresponds to a floating point numeral, otherwise invokes exception handler or returns false

Remarks: This function extracts the exponent in t, without normalization. NaN is an invalid argument.

Referenced by FPNumRef::exponent().

Retrieves the sign of a floating-point literal.

Parameters

c logical context t a floating-point numeral sgn the retrieved sign

Returns

true if t corresponds to a floating point numeral, otherwise invokes exception handler or returns false

Remarks: sets sgn to 0 if ‘t’ is positive and to 1 otherwise, except for NaN, which is an invalid argument.

Referenced by FPNumRef::sign().

Retrieves the sign of a floating-point literal as a bit-vector expression.

Parameters

c logical context t a floating-point numeral

Remarks: NaN is an invalid argument.

Referenced by FPNumRef::sign_as_bv().

Retrieves the significand of a floating-point literal as a bit-vector expression.

Parameters

c logical context t a floating-point numeral

Remarks: NaN is an invalid argument.

Referenced by FPNumRef::significand_as_bv().

Return the significand value of a floating-point numeral as a string.

Parameters

c logical context t a floating-point numeral

Returns

true if t corresponds to a floating point numeral, otherwise invokes exception handler or returns false

Remarks: The significand s is always 0.0 <= s < 2.0; the resulting string is long enough to represent the real significand precisely.

Referenced by FPNumRef::significand().

Return the significand value of a floating-point numeral as a uint64.

Parameters

c logical context t a floating-point numeral n pointer to output uint64

Remarks: This function extracts the significand bits in t, without the hidden bit or normalization. Sets the Z3_INVALID_ARG error code if the significand does not fit into a uint64. NaN is an invalid argument.

Referenced by FPNumRef::significand_as_long().

add a function entry to a function interpretation.

Parameters

c logical context fi a function interpretation to be updated. args list of arguments. They should be constant values (such as integers) and be of the same types as the domain of the function. value value of the function when the parameters match args.

It is assumed that entries added to a function cover disjoint arguments. If an two entries are added with the same arguments, only the second insertion survives and the first inserted entry is removed.

Referenced by func_interp::add_entry(), and ModelRef::update_value().

Return the arity (number of arguments) of the given function interpretation.

Referenced by FuncInterp::arity().

Return the 'else' value of the given function interpretation.

A function interpretation is represented as a finite map and an 'else' value. This procedure returns the 'else' value.

Referenced by func_interp::else_value(), and FuncInterp::else_value().

Return the number of entries in the given function interpretation.

A function interpretation is represented as a finite map and an 'else' value. Each entry in the finite map represents the value of a function given a set of arguments. This procedure return the number of element in the finite map of f.

See also

Z3_func_interp_get_entry

Referenced by func_interp::num_entries(), and FuncInterp::num_entries().

Return the 'else' value of the given function interpretation.

A function interpretation is represented as a finite map and an 'else' value. This procedure can be used to update the 'else' value.

Referenced by func_interp::set_else().

Return a lower bound for the given real algebraic number. The interval isolating the number is smaller than 1/10^precision. The result is a numeral AST of sort Real.

Precondition

Z3_is_algebraic_number(c, a)

Referenced by expr::algebraic_lower().

Return a upper bound for the given real algebraic number. The interval isolating the number is smaller than 1/10^precision. The result is a numeral AST of sort Real.

Precondition

Z3_is_algebraic_number(c, a)

Referenced by expr::algebraic_upper(), and AlgebraicNumRef::approx().

Return a hash code for the given AST. The hash code is structural but two different AST objects can map to the same hash. The result of Z3_get_ast_id returns an identifier that is unique over the set of live AST objects.

Referenced by ast::hash(), and AstRef::hash().

Return Z3_L_TRUE if a is true, Z3_L_FALSE if it is false, and Z3_L_UNDEF otherwise.

Referenced by expr::bool_value().

Return the parameter type associated with a declaration.

Parameters

c the context d the function declaration idx is the index of the named parameter it should be between 0 and the number of parameters.

Referenced by parameter::parameter(), and FuncDeclRef::params().

Return the number of parameters of the given declaration.

See also

Z3_get_arity

Return the estimated allocated memory in bytes.

Store the size of the sort in r. Return false if the call failed. That is, Z3_get_sort_kind(s) == Z3_FINITE_DOMAIN_SORT.

Referenced by FiniteDomainSortRef::size().

Retrieve congruence class representatives for terms.

The function can be used for relying on Z3 to identify equal terms under the current set of assumptions. The array of terms and array of class identifiers should have the same length. The class identifiers are numerals that are assigned to the same value for their corresponding terms if the current context forces the terms to be equal. You cannot deduce that terms corresponding to different numerals must be all different, (especially when using non-convex theories). All implied equalities are returned by this call. This means that two terms map to the same class identifier if and only if the current context implies that they are equal.

A side-effect of the function is a satisfiability check on the assertions on the solver that is passed in. The function return Z3_L_FALSE if the current assertions are not satisfiable.

Return index of de-Bruijn bound variable.

Precondition

Z3_get_ast_kind(a) == Z3_VAR_AST

Referenced by z3py::get_var_index().

Retrieve the string constant stored in s. The string can contain escape sequences. Characters in the range 1 to 255 are literal. Characters in the range 0, and 256 above are escaped.

Precondition

Z3_is_string(c, s)

Referenced by SeqRef::as_string().

Return numeral as a double.

Precondition

Z3_get_ast_kind(c, a) == Z3_NUMERAL_AST || Z3_is_algebraic_number(c, a)

Referenced by expr::is_numeral().

Similar to Z3_get_numeral_string, but only succeeds if the value can fit as a rational number as machine int64_t int. Return true if the call succeeded.

Precondition

Z3_get_ast_kind(c, v) == Z3_NUMERAL_AST

See also

Z3_get_numeral_string

Return numeral value, as a pair of 64 bit numbers if the representation fits.

Parameters

c logical context. a term. num numerator. den denominator.

Return true if the numeral value fits in 64 bit numerals, false otherwise.

Precondition

Z3_get_ast_kind(a) == Z3_NUMERAL_AST

Return i'th ast in pattern.

Return number of terms in pattern.

Return symbol of the i'th bound variable.

Precondition

Z3_get_ast_kind(a) == Z3_QUANTIFIER_AST

Referenced by QuantifierRef::var_name().

Return sort of the i'th bound variable.

Precondition

Z3_get_ast_kind(a) == Z3_QUANTIFIER_AST

Referenced by QuantifierRef::var_sort().

Obtain id of quantifier.

Precondition

Z3_get_ast_kind(a) == Z3_QUANTIFIER_AST

Referenced by QuantifierRef::qid().

Return number of bound variables of quantifier.

Precondition

Z3_get_ast_kind(a) == Z3_QUANTIFIER_AST

Referenced by QuantifierRef::num_vars().

Obtain weight of quantifier.

Precondition

Z3_get_ast_kind(a) == Z3_QUANTIFIER_AST

Referenced by QuantifierRef::weight().

Return the range of the given declaration.

If d is a constant (i.e., has zero arguments), then this function returns the sort of the constant.

Referenced by func_decl::range(), and FuncDeclRef::range().

Return arity of relation.

Precondition

Z3_get_sort_kind(s) == Z3_RELATION_SORT

See also

Z3_get_relation_column

Return sort at i'th column of relation sort.

Precondition

Z3_get_sort_kind(c, s) == Z3_RELATION_SORT

col < Z3_get_relation_arity(c, s)

See also

Z3_get_relation_arity

Return the name of the idx simplifier.

Precondition

i < Z3_get_num_simplifiers(c)

See also

Z3_get_num_simplifiers

Return the sort of an AST node.

The AST node must be a constant, application, numeral, bound variable, or quantifier.

Referenced by z3py::deserialize(), expr::get_sort(), z3py::is_array_sort(), z3py::is_sort(), SeqRef::is_string(), BoolRef::sort(), ArithRef::sort(), BitVecRef::sort(), ArrayRef::sort(), DatatypeRef::sort(), FiniteDomainRef::sort(), FPRef::sort(), and SeqRef::sort().

Return a unique identifier for s.

Referenced by sort::id().

Retrieve the string constant stored in s. Characters outside the basic printable ASCII range are escaped.

Precondition

Z3_is_string(c, s)

Referenced by expr::get_string().

Retrieve the unescaped string constant stored in s.

Precondition

Z3_is_string(c, s)

length contains the number of characters in s

Referenced by expr::get_u32string().

Retrieve the length of the unescaped string constant stored in s.

Precondition

Z3_is_string(c, s)

Referenced by expr::get_u32string().

Return the symbol name.

Precondition

Z3_get_symbol_kind(s) == Z3_STRING_SYMBOL

Warning

The returned buffer is statically allocated by Z3. It will be automatically deallocated when Z3_del_context is invoked. So, the buffer is invalidated in the next call to Z3_get_symbol_string.

See also

Z3_mk_string_symbol

Referenced by symbol::str(), and z3py::to_symbol().

Return the i-th field declaration (i.e., projection function declaration) of the given tuple sort.

Precondition

Z3_get_sort_kind(t) == Z3_DATATYPE_SORT

i < Z3_get_tuple_sort_num_fields(c, t)

See also

Z3_mk_tuple_sort

Z3_get_sort_kind

Set a global (or module) parameter. This setting is shared by all Z3 contexts.

When a Z3 module is initialized it will use the value of these parameters when Z3_params objects are not provided.

The name of parameter can be composed of characters [a-z][A-Z], digits [0-9], '-' and '_'. The character '.' is a delimiter (more later).

The parameter names are case-insensitive. The character '-' should be viewed as an "alias" for '_'. Thus, the following parameter names are considered equivalent: "pp.decimal-precision" and "PP.DECIMAL_PRECISION".

This function can be used to set parameters for a specific Z3 module. This can be done by using <module-name>.<parameter-name>. For example: Z3_global_param_set('pp.decimal', 'true') will set the parameter "decimal" in the module "pp" to true.

See also

Z3_global_param_get

Z3_global_param_reset_all

Referenced by z3py::set_param(), and z3::set_param().

Add a new formula a to the given goal. The formula is split according to the following procedure that is applied until a fixed-point: Conjunctions are split into separate formulas. Negations are distributed over disjunctions, resulting in separate formulas. If the goal is false, adding new formulas is a no-op. If the formula a is true, then nothing is added. If the formula a is false, then the entire goal is replaced by the formula false.

Referenced by goal::add(), and Goal::assert_exprs().

Return the depth of the given goal. It tracks how many transformations were applied to it.

Referenced by goal::depth(), and Goal::depth().

Return true if the goal is empty, and it is precise or the product of a under approximation.

Referenced by goal::is_decided_sat().

Return true if the goal contains false, and it is precise or the product of an over approximation.

Referenced by goal::is_decided_unsat().

Return the number of formulas, subformulas and terms in the given goal.

Referenced by goal::num_exprs().

Return the "precision" of the given goal. Goals can be transformed using over and under approximations. A under approximation is applied when the objective is to find a model for a given goal. An over approximation is applied when the objective is to find a proof for a given goal.

Referenced by Goal::prec(), and goal::precision().

Erase all formulas from the given goal.

Referenced by goal::reset().

Convert a goal into a DIMACS formatted string. The goal must be in CNF. You can convert a goal to CNF by applying the tseitin-cnf tactic. Bit-vectors are not automatically converted to Booleans either, so if the caller intends to preserve satisfiability, it should apply bit-blasting tactics. Quantifiers and theory atoms will not be encoded.

Referenced by goal::dimacs(), and Goal::dimacs().

Copy a goal g from the context source to the context target.

Referenced by Goal::translate().

The (_ as-array f) AST node is a construct for assigning interpretations for arrays in Z3. It is the array such that forall indices i we have that (select (_ as-array f) i) is equal to (f i). This procedure returns true if the a is an as-array AST node.

Z3 current solvers have minimal support for as_array nodes.

See also

Z3_get_as_array_func_decl

Referenced by z3py::is_as_array().

Check if s is a character sort.

Compare terms.

Referenced by z3py::is_real().

Check if s is a regular expression sort.

Check if s is a sequence sort.

Take the absolute value of an integer.

Create an AST node representing args[0] + ... + args[num_args-1].

The array args must have num_args elements. All arguments must have int or real sort.

Referenced by z3py::Sum().

Create an AST node representing args[0] and ... and args[num_args-1].

The array args must have num_args elements. All arguments must have Boolean sort.

Referenced by z3py::And(), and goal::as_expr().

Access the array default value. Produces the default range value, for arrays that can be represented as finite maps with a default range value.

Parameters

c logical context. array array value whose default range value is accessed.

Referenced by ArrayRef::default().

Create array extensionality index given two arrays with the same sort. The meaning is given by the axiom: (=> (= (select A (array-ext A B)) (select B (array-ext A B))) (= A B))

Referenced by z3py::Ext().

Create array with the same interpretation as a function. The array satisfies the property (f x) = (select (_ as-array f) x) for every argument x.

Referenced by z3::as_array().

Return an empty mapping from AST to AST.

Pseudo-Boolean relations.

Encode p1 + p2 + ... + pn >= k

Referenced by z3py::AtLeast().

Pseudo-Boolean relations.

Encode p1 + p2 + ... + pn <= k

Referenced by z3py::AtMost().

Extracts the bit at position i of a bit-vector and yields a boolean.

The node t1 must have a bit-vector sort.

Referenced by expr::bit2bool().

Create a variable.

Variables are intended to be bound by a scope created by a quantifier. So we call them bound variables even if they appear as free variables in the expression produced by Z3_mk_bound.

Bound variables are indexed by de-Bruijn indices. It is perhaps easiest to explain the meaning of de-Bruijn indices by indicating the compilation process from non-de-Bruijn formulas to de-Bruijn format.

abs(forall (x1) phi) = forall (x1) abs1(phi, x1, 0)
abs(forall (x1, x2) phi) = abs(forall (x1) abs(forall (x2) phi))
abs1(x, x, n) = b_n
abs1(y, x, n) = y
abs1(f(t1,...,tn), x, n) = f(abs1(t1,x,n), ..., abs1(tn,x,n))
abs1(forall (x1) phi, x, n) = forall (x1) (abs1(phi, x, n+1))

The last line is significant: the index of a bound variable is different depending on the scope in which it appears. The deeper x appears, the higher is its index.

Parameters

c logical context index de-Bruijn index ty sort of the bound variable

See also

Z3_mk_forall

Z3_mk_exists

Referenced by z3py::Var(), and context::variable().

Create an integer from the bit-vector argument t1. If is_signed is false, then the bit-vector t1 is treated as unsigned. So the result is non-negative and in the range [0..2^N-1], where N are the number of bits in t1. If is_signed is true, t1 is treated as a signed bit-vector.

The node t1 must have a bit-vector sort.

Referenced by z3py::BV2Int().

Create a predicate that checks that the bit-wise addition of t1 and t2 does not overflow.

The nodes t1 and t2 must have the same bit-vector sort. The returned node is of sort Bool.

Referenced by z3py::BVAddNoOverflow().

Create a predicate that checks that the bit-wise signed addition of t1 and t2 does not underflow.

The nodes t1 and t2 must have the same bit-vector sort. The returned node is of sort Bool.

Referenced by z3py::BVAddNoUnderflow().

Arithmetic shift right.

It is like logical shift right except that the most significant bits of the result always copy the most significant bit of the second argument.

The semantics of shift operations varies between environments. This definition does not necessarily capture directly the semantics of the programming language or assembly architecture you are modeling.

The nodes t1 and t2 must have the same bit-vector sort.

Referenced by BitVecRef::__rrshift__(), BitVecRef::__rshift__(), and z3::ashr().

Logical shift right.

It is equivalent to unsigned division by 2^x where x is the value of the third argument.

NB. The semantics of shift operations varies between environments. This definition does not necessarily capture directly the semantics of the programming language or assembly architecture you are modeling.

The nodes t1 and t2 must have the same bit-vector sort.

Referenced by z3py::LShR(), and z3::lshr().

Create a predicate that checks that the bit-wise multiplication of t1 and t2 does not overflow.

The nodes t1 and t2 must have the same bit-vector sort. The returned node is of sort Bool.

Referenced by z3py::BVMulNoOverflow().

Create a predicate that checks that the bit-wise signed multiplication of t1 and t2 does not underflow.

The nodes t1 and t2 must have the same bit-vector sort. The returned node is of sort Bool.

Referenced by z3py::BVMulNoUnderflow().

Bitwise nand.

The nodes t1 and t2 must have the same bit-vector sort.

Standard two's complement unary minus.

The node t1 must have bit-vector sort.

Referenced by BitVecRef::__neg__().

Check that bit-wise negation does not overflow when t1 is interpreted as a signed bit-vector.

The node t1 must have bit-vector sort. The returned node is of sort Bool.

Referenced by z3py::BVSNegNoOverflow().

Bitwise nor.

The nodes t1 and t2 must have the same bit-vector sort.

Take conjunction of bits in vector, return vector of length 1.

The node t1 must have a bit-vector sort.

Referenced by z3py::BVRedAnd().

Take disjunction of bits in vector, return vector of length 1.

The node t1 must have a bit-vector sort.

Referenced by z3py::BVRedOr().

Two's complement signed division.

It is defined in the following way:

• The floor of t1/t2 if t2 is different from zero, and t1*t2 >= 0.
• The ceiling of t1/t2 if t2 is different from zero, and t1*t2 < 0.

If t2 is zero, then the result is undefined.

The nodes t1 and t2 must have the same bit-vector sort.

Referenced by BitVecRef::__div__(), and BitVecRef::__rdiv__().

Create a predicate that checks that the bit-wise signed division of t1 and t2 does not overflow.

The nodes t1 and t2 must have the same bit-vector sort. The returned node is of sort Bool.

Referenced by z3py::BVSDivNoOverflow().

Two's complement signed greater than or equal to.

The nodes t1 and t2 must have the same bit-vector sort.

Referenced by BitVecRef::__ge__(), and z3::sge().

Two's complement signed greater than.

The nodes t1 and t2 must have the same bit-vector sort.

Referenced by BitVecRef::__gt__(), and z3::sgt().

Shift left.

It is equivalent to multiplication by 2^x where x is the value of the third argument.

NB. The semantics of shift operations varies between environments. This definition does not necessarily capture directly the semantics of the programming language or assembly architecture you are modeling.

The nodes t1 and t2 must have the same bit-vector sort.

Referenced by BitVecRef::__lshift__(), BitVecRef::__rlshift__(), and z3::shl().

Two's complement signed less than or equal to.

The nodes t1 and t2 must have the same bit-vector sort.

Referenced by BitVecRef::__le__(), and z3::sle().

Two's complement signed less than.

It abbreviates:

(or (and (= (extract[|m-1|:|m-1|] t1) bit1)

(= (extract[|m-1|:|m-1|] t2) bit0))

(and (= (extract[|m-1|:|m-1|] t1) (extract[|m-1|:|m-1|] t2))

(bvult t1 t2)))

The nodes t1 and t2 must have the same bit-vector sort.

Referenced by BitVecRef::__lt__(), and z3::slt().

Two's complement signed remainder (sign follows dividend).

It is defined as t1 - (t1 /s t2) * t2, where /s represents signed division. The most significant bit (sign) of the result is equal to the most significant bit of t1.

If t2 is zero, then the result is undefined.

The nodes t1 and t2 must have the same bit-vector sort.

See also

Z3_mk_bvsmod

Referenced by z3py::SRem(), and z3::srem().

Create a predicate that checks that the bit-wise signed subtraction of t1 and t2 does not overflow.

The nodes t1 and t2 must have the same bit-vector sort. The returned node is of sort Bool.

Referenced by z3py::BVSubNoOverflow().

Create a predicate that checks that the bit-wise subtraction of t1 and t2 does not underflow.

The nodes t1 and t2 must have the same bit-vector sort. The returned node is of sort Bool.

Referenced by z3py::BVSubNoUnderflow().

Unsigned division.

It is defined as the floor of t1/t2 if t2 is different from zero. If t2 is zero, then the result is undefined.

The nodes t1 and t2 must have the same bit-vector sort.

Referenced by z3py::UDiv(), and z3::udiv().

Unsigned greater than or equal to.

The nodes t1 and t2 must have the same bit-vector sort.

Referenced by z3py::UGE(), and z3::uge().

Unsigned greater than.

The nodes t1 and t2 must have the same bit-vector sort.

Referenced by z3py::UGT(), and z3::ugt().

Unsigned less than or equal to.

The nodes t1 and t2 must have the same bit-vector sort.

Referenced by z3py::ULE(), and z3::ule().

Unsigned less than.

The nodes t1 and t2 must have the same bit-vector sort.

Referenced by z3py::ULT(), and z3::ult().

Unsigned remainder.

It is defined as t1 - (t1 /u t2) * t2, where /u represents unsigned division.

If t2 is zero, then the result is undefined.

The nodes t1 and t2 must have the same bit-vector sort.

Referenced by z3py::URem(), and z3::urem().

Bitwise xnor.

The nodes t1 and t2 must have the same bit-vector sort.

Create less than or equal to between two characters.

Referenced by CharRef::__le__().

Create a sort for unicode characters.

The sort for characters can be changed to ASCII by setting the global parameter encoding to ascii, or alternative to 16 bit characters by setting encoding to bmp.

Referenced by context::char_sort(), and z3py::CharSort().

Concatenate the given bit-vectors.

The nodes t1 and t2 must have (possibly different) bit-vector sorts

The result is a bit-vector of size n1+n2, where n1 (n2) is the size of t1 (t2).

Referenced by z3py::Concat().

Create a configuration object for the Z3 context object.

Configurations are created in order to assign parameters prior to creating contexts for Z3 interaction. For example, if the users wishes to use proof generation, then call:

Z3_set_param_value(cfg, "proof", "true")

The following parameters can be set:

- proof  (Boolean)           Enable proof generation
- debug_ref_count (Boolean)  Enable debug support for Z3_ast reference counting
- trace  (Boolean)           Tracing support for VCC
- trace_file_name (String)   Trace out file for VCC traces
- timeout (unsigned)         default timeout (in milliseconds) used for solvers
- well_sorted_check          type checker
- auto_config                use heuristics to automatically select solver and configure it
- model                      model generation for solvers, this parameter can be overwritten when creating a solver
- model_validate             validate models produced by solvers
- unsat_core                 unsat-core generation for solvers, this parameter can be overwritten when creating a solver
- encoding                   the string encoding used internally (must be either "unicode" - 18 bit, "bmp" - 16 bit or "ascii" - 8 bit)

See also

Z3_set_param_value

Z3_del_config

Referenced by Context::__init__(), and config::config().

Declare and create a constant.

This function is a shorthand for:

Z3_func_decl Z3_API Z3_mk_func_decl(Z3_context c, Z3_symbol s, unsigned domain_size, Z3_sort const domain[], Z3_sort range)

Declare a constant or function.

Z3_ast Z3_API Z3_mk_app(Z3_context c, Z3_func_decl d, unsigned num_args, Z3_ast const args[])

Create a constant or function application.

System.IntPtr Z3_func_decl

See also

Z3_mk_app

Z3_mk_fresh_const

Z3_mk_func_decl

Referenced by z3py::Array(), z3py::BitVec(), z3py::Bool(), z3py::Const(), context::constant(), z3py::FP(), z3py::Int(), z3py::Real(), and z3py::String().

Create the constant array.

The resulting term is an array, such that a select on an arbitrary index produces the value v.

Parameters

c logical context. domain domain sort for the array. v value that the array maps to.

Referenced by z3::const_array(), and z3py::K().

Create a constructor.

Parameters

c logical context. name constructor name. recognizer name of recognizer function. num_fields number of fields in constructor. field_names names of the constructor fields. sorts field sorts, 0 if the field sort refers to a recursive sort. sort_refs reference to datatype sort that is an argument to the constructor; if the corresponding sort reference is 0, then the value in sort_refs should be an index referring to one of the recursive datatypes that is declared.

See also

Z3_del_constructor

Z3_mk_constructor_list

Z3_query_constructor

Referenced by constructors::add(), and z3py::CreateDatatypes().

Create a context using the given configuration.

After a context is created, the configuration cannot be changed, although some parameters can be changed using Z3_update_param_value. All main interaction with Z3 happens in the context of a Z3_context.

In contrast to Z3_mk_context_rc the life time of Z3_ast objects persists with the life time of the context.

Note that all other reference counted objects, including Z3_model, Z3_solver, Z3_func_interp have to be managed by the caller. Their reference counts are not handled by the context.

See also

Z3_del_context

Create a context using the given configuration. This function is similar to Z3_mk_context. However, in the context returned by this function, the user is responsible for managing Z3_ast reference counters. Managing reference counters is a burden and error-prone, but allows the user to use the memory more efficiently. The user must invoke Z3_inc_ref for any Z3_ast returned by Z3, and Z3_dec_ref whenever the Z3_ast is not needed anymore. This idiom is similar to the one used in BDD (binary decision diagrams) packages such as CUDD.

Remarks:

• Z3_sort, Z3_func_decl, Z3_app, Z3_pattern are Z3_ast's.
• After a context is created, the configuration cannot be changed.
• All main interaction with Z3 happens in the context of a Z3_context.
• Z3 uses hash-consing, i.e., when the same Z3_ast is created twice, Z3 will return the same pointer twice.

Create datatype, such as lists, trees, records, enumerations or unions of records. The datatype may be recursive. Return the datatype sort.

Parameters

c logical context. name name of datatype. num_constructors number of constructors passed in. constructors array of constructor containers.

See also

Z3_mk_constructor

Z3_mk_constructor_list

Z3_mk_datatypes

Referenced by context::datatype().

create a forward reference to a recursive datatype being declared. The forward reference can be used in a nested occurrence: the range of an array or as element sort of a sequence. The forward reference should only be used when used in an accessor for a recursive datatype that gets declared.

Forward references can replace the use sort references, that are unsigned integers in the Z3_mk_constructor call

Referenced by context::datatype_sort(), and z3py::DatatypeSort().

Create an AST node representing distinct(args[0], ..., args[num_args-1]).

The distinct construct is used for declaring the arguments pairwise distinct. That is, Forall 0 <= i < j < num_args. not args[i] = args[j].

All arguments must have the same sort.

Referenced by ExprRef::__ne__(), and z3py::Distinct().

Create an AST node representing arg1 div arg2.

The arguments must either both have int type or both have real type. If the arguments have int type, then the result type is an int type, otherwise the the result type is real.

Referenced by ArithRef::__div__(), and ArithRef::__rdiv__().

Create division predicate.

The nodes t1 and t2 must be of integer sort. The predicate is true when t1 divides t2. For the predicate to be part of linear integer arithmetic, the first argument t1 must be a non-zero integer.

Create a enumeration sort.

An enumeration sort with n elements. This function will also declare the functions corresponding to the enumerations.

Parameters

c logical context name name of the enumeration sort. n number of elements in enumeration sort. enum_names names of the enumerated elements. enum_consts constants corresponding to the enumerated elements. enum_testers predicates testing if terms of the enumeration sort correspond to an enumeration.

For example, if this function is called with three symbols A, B, C and the name S, then s is a sort whose name is S, and the function returns three terms corresponding to A, B, C in enum_consts. The array enum_testers has three predicates of type (s -> Bool). The first predicate (corresponding to A) is true when applied to A, and false otherwise. Similarly for the other predicates.

Referenced by context::enumeration_sort(), and z3py::EnumSort().

Create an AST node representing l = r.

The nodes l and r must have the same type.

Referenced by ExprRef::__eq__().

Similar to Z3_mk_forall_const.

Create an existential quantifier using a list of constants that will form the set of bound variables.

Parameters

c logical context. weight quantifiers are associated with weights indicating the importance of using the quantifier during instantiation. By default, pass the weight 0. num_bound number of constants to be abstracted into bound variables. bound array of constants to be abstracted into bound variables. num_patterns number of patterns. patterns array containing the patterns created using Z3_mk_pattern. body the body of the quantifier.

See also

Z3_mk_pattern

Z3_mk_forall_const

Referenced by z3::exists().

Rotate bits of t1 to the left t2 times.

The nodes t1 and t2 must have the same bit-vector sort.

Referenced by z3py::RotateLeft().

Rotate bits of t1 to the right t2 times.

The nodes t1 and t2 must have the same bit-vector sort.

Referenced by z3py::RotateRight().

Extract the bits high down to low from a bit-vector of size m to yield a new bit-vector of size n, where n = high - low + 1.

The node t1 must have a bit-vector sort.

Referenced by z3py::Extract(), and expr::extract().

Create a named finite domain sort.

To create constants that belong to the finite domain, use the APIs for creating numerals and pass a numeric constant together with the sort returned by this call. The numeric constant should be between 0 and the less than the size of the domain.

See also

Z3_get_finite_domain_sort_size

Referenced by z3py::FiniteDomainSort().

Create a forall formula. It takes an expression body that contains bound variables of the same sorts as the sorts listed in the array sorts. The bound variables are de-Bruijn indices created using Z3_mk_bound. The array decl_names contains the names that the quantified formula uses for the bound variables. Z3 applies the convention that the last element in the decl_names and sorts array refers to the variable with index 0, the second to last element of decl_names and sorts refers to the variable with index 1, etc.

Parameters

c logical context. weight quantifiers are associated with weights indicating the importance of using the quantifier during instantiation. By default, pass the weight 0. num_patterns number of patterns. patterns array containing the patterns created using Z3_mk_pattern. num_decls number of variables to be bound. sorts the sorts of the bound variables. decl_names names of the bound variables body the body of the quantifier.

See also

Z3_mk_pattern

Z3_mk_bound

Z3_mk_exists

Create a universal quantifier using a list of constants that will form the set of bound variables.

Parameters

c logical context. weight quantifiers are associated with weights indicating the importance of using the quantifier during instantiation. By default, pass the weight 0. num_bound number of constants to be abstracted into bound variables. bound array of constants to be abstracted into bound variables. num_patterns number of patterns. patterns array containing the patterns created using Z3_mk_pattern. body the body of the quantifier.

See also

Z3_mk_pattern

Z3_mk_exists_const

Referenced by z3::forall().

Floating-point addition.

Parameters

c logical context rm term of RoundingMode sort t1 term of FloatingPoint sort t2 term of FloatingPoint sort

rm must be of RoundingMode sort, t1 and t2 must have the same FloatingPoint sort.

Floating-point division.

Parameters

c logical context rm term of RoundingMode sort t1 term of FloatingPoint sort. t2 term of FloatingPoint sort

The nodes rm must be of RoundingMode sort, t1 and t2 must have the same FloatingPoint sort.

Floating-point equality.

Parameters

c logical context t1 term of FloatingPoint sort t2 term of FloatingPoint sort

Note that this is IEEE 754 equality (as opposed to SMT-LIB =).

t1 and t2 must have the same FloatingPoint sort.

See also

Z3_mk_fpa_geq

Z3_mk_fpa_gt

Z3_mk_fpa_leq

Z3_mk_fpa_lt

Floating-point fused multiply-add.

Parameters

c logical context rm term of RoundingMode sort t1 term of FloatingPoint sort t2 term of FloatingPoint sort t3 term of FloatingPoint sort

The result is round((t1 * t2) + t3).

rm must be of RoundingMode sort, t1, t2, and t3 must have the same FloatingPoint sort.

Maximum of floating-point numbers.

Parameters

c logical context t1 term of FloatingPoint sort t2 term of FloatingPoint sort

t1, t2 must have the same FloatingPoint sort.

See also

Z3_mk_fpa_min

Minimum of floating-point numbers.

Parameters

c logical context t1 term of FloatingPoint sort t2 term of FloatingPoint sort

t1, t2 must have the same FloatingPoint sort.

See also

Z3_mk_fpa_max

Floating-point multiplication.

Parameters

c logical context rm term of RoundingMode sort t1 term of FloatingPoint sort t2 term of FloatingPoint sort

rm must be of RoundingMode sort, t1 and t2 must have the same FloatingPoint sort.

Floating-point remainder.

Parameters

c logical context t1 term of FloatingPoint sort t2 term of FloatingPoint sort

t1 and t2 must have the same FloatingPoint sort.

Floating-point roundToIntegral. Rounds a floating-point number to the closest integer, again represented as a floating-point number.

Parameters

c logical context rm term of RoundingMode sort t term of FloatingPoint sort

t must be of FloatingPoint sort.

Floating-point square root.

Parameters

c logical context rm term of RoundingMode sort t term of FloatingPoint sort

rm must be of RoundingMode sort, t must have FloatingPoint sort.

Floating-point subtraction.

Parameters

c logical context rm term of RoundingMode sort t1 term of FloatingPoint sort t2 term of FloatingPoint sort

rm must be of RoundingMode sort, t1 and t2 must have the same FloatingPoint sort.

Conversion of a single IEEE 754-2008 bit-vector into a floating-point number.

Produces a term that represents the conversion of a bit-vector term bv to a floating-point term of sort s.

Parameters

c logical context bv a bit-vector term s floating-point sort

s must be a FloatingPoint sort, t must be of bit-vector sort, and the bit-vector size of bv must be equal to ebits+sbits of s. The format of the bit-vector is as defined by the IEEE 754-2008 interchange format.

Referenced by z3py::fpBVToFP(), z3py::fpToFP(), and expr::mk_from_ieee_bv().

Conversion of a FloatingPoint term into another term of different FloatingPoint sort.

Produces a term that represents the conversion of a floating-point term t to a floating-point term of sort s. If necessary, the result will be rounded according to rounding mode rm.

Parameters

c logical context rm term of RoundingMode sort t term of FloatingPoint sort s floating-point sort

s must be a FloatingPoint sort, rm must be of RoundingMode sort, t must be of floating-point sort.

Referenced by z3py::fpFPToFP(), and z3py::fpToFP().