Arithmetic
Z3 supports the theory of arithmetic described in the following places.
Basics
Z3 has built-in support for integer and real constants. These two types should not be confused with machine integers (32-bit or 64-bit) and floating point numbers. These two types (sorts) represent the mathematical integers and reals. The command declare-const is used to declare integer and real constants.
After constants are declared, the user can assert formulas containing that use these constants and arithmetic operators such as +, -, *, etc. The check-sat command instructs Z3 to try to find an interpretation for the declared constants that makes all formulas true. The interpretation is basically assigning a number to each constant. If such interpretation exists, we say it is a model for the asserted formulas. The command get-model displays the model built by Z3.
Real constants should contain a decimal point. Unlike most programming languages, Z3 will not convert automatically integers into reals and vice-versa. The function to-real can be used to convert an integer expression into a real one.
Some operators are chainable. This includes comparison operators such as < and <=.
We can use mixed constraints to ask questions on how reals behave under rounding.
The following query considers when the sum of two integers, x, y are above a constant a,
while the sum of two reals are below a. At the same time the integers x, y are within unit distance
to the integers.
Difference Arithmetic
Many problem classes use only limited set of arithmetical constraints. One such class is job-shop scheduling constraints. Simpler instances can be encoded and solved using SMT, while advanced uses of job shop scheduling problems do not have efficient encodings directly into arithmetic. For job-shop problems tasks have start time, duration and constraints specifying whether tasks should not overlap and ordering. To specify ordering and overlap constraints require comparing just two time points separated by a constant offset. Comparisons of this form fall within the class of difference arithmetic constraints.
In the example we model three jobs, each job has two tasks
to be completed by two workers. Thus, there are six variables for every task/worker combination.
The start time of job 1 on worker 2 is given by t12. It has duration 1, so has to start at least one unit before
the completion deadline 8. It follows task t11 which has duration 2 and cannot overlap with other tasks on work station 2.
Non-linear arithmetic
We say a formula is nonlinear if it contains expressions of the form (* t s) where t and s are not numbers. Nonlinear real arithmetic is very expensive, and Z3 is not complete for this kind of formula. The command check-sat may return unknown or loop. Nonlinear integer arithmetic is undecidable there is no procedure that is correct and terminates (for every input) with a sat or unsat answer. Yes, it is impossible to build such procedure. Note that, this does not prevent Z3 from returning an answer for many nonlinear problems. The real limit is that there will always be a nonlinear integer arithmetic formula that it will fail produce an answer.
Transcendental Arithmetic
Transcendental reasoning is incomplete and is not covered by the complete
polynomial real-arithmetic procedure described above. Solver selection matters:
in Z3 5.3.1 the default QF_NTA route can return sat for an assertion
(<= (exp x) 0.0), although the assertion is mathematically false.
The smt tactic refutes this example, but that is not a guarantee that it
decides other transcendental problems correctly or completely.
The examples in this section are non-interactive because the guide's embedded solver uses Z3 5.0. Run them with Z3 5.3 or later, taking the version-specific limitations into account.
Z3 5.3 adds the following real-valued operators and extends reasoning for transcendental functions.
| Operation | Mathematical meaning |
|---|---|
(exp x) | Natural exponential of the real argument x |
(log x) or (ln x) | Natural logarithm; use a positive argument |
(atan2 y x) or (arctan2 y x) | Two-argument arctangent, with the vertical argument y first |
These are Z3 extensions, not operators of the SMT-LIB polynomial real-arithmetic
theory. They complement the existing trigonometric, inverse-trigonometric,
hyperbolic, and inverse-hyperbolic operators. The logic name QF_NTA selects
quantifier-free nonlinear transcendental arithmetic in Z3; the operators are
also available with logic ALL or without a set-logic command.
Constrain arguments to the mathematical domains needed by your application,
such as x > 0 for log, and do not rely on out-of-domain values.
The exponential is always positive. The following query explicitly uses the
smt tactic to refute its negation:
(set-logic QF_NTA)
(declare-const x Real)
(assert (<= (exp x) 0.0))
(check-sat-using smt)
The result is unsat in Z3 5.3.1. Replacing the final command by ordinary
check-sat takes a different solver route and exhibits the issue noted above.
Do not treat a result from one route as validation of another.
The nonlinear solver combines theory lemmas and bounds with numerical checking
of candidate assignments. :smt.arith.nl.transcendental controls these
transcendental checks, and :smt.arith.nl.transcendental_tolerance controls their
numerical tolerance (default 0.0000001). These controls do not provide an
exact, complete decision procedure, and changing the tolerance is not a way to
obtain a proof of exact satisfiability. A query may return unknown or exhaust
its resource budget. Keep this support separate from exact polynomial NRA
solving and from floating-point arithmetic.
Division
Z3 also has support for division, integer division, modulo and remainder operators. Internally, they are all mapped to multiplication.
In Z3, division by zero is allowed, but the result is not specified. Division is not a partial function. Actually, in Z3 all functions are total, although the result may be under-specified in some cases like division by zero.
We say that an interpreted function (such as /) is under-specified when the meaning of the function is not fixed on all values
of arguments. The division, modulus and remainder functions are under-specified when the second argument is 0. Constraints that
allow the second arguments to these functions to be 0 can still be satisfiable when there are interpretations of the functions
at 0 that satisfy the constraints.
If you are not happy with this behavior, you may use the ite (if-then-else) operator to guard every division, and assign whatever interpretation you like to the division by zero. This example uses define-fun constructor to create a new operator mydiv. This is essentially a macro, and Z3 will expand its definition for every application of mydiv.
Algorithmic Fragments of Arithmetic
Z3 contains a combination of several engines for solving arithmetic formulas. The engines are invoked based on the shape of arithmetic formulas. For linear real arithmetic formulas it uses dual simplex to determine feasibility. For linear integer arithmetic formulas it uses techniques from integer programming: cuts and branch and bound. There are specialized solvers for different arithmetic fragments and, finally, for non-linear arithmetic constraints z3 contains several small hammers that integrate Grobner basis simplifications, bounds propagation, non-linear cylindric algebraic decomposition and reducing non-linear constraints to linear form by sampling at tangent points.
| Logic | Fragment | Solver | Example |
|---|---|---|---|
| LRA | Linear Real Arithmetic | Dual Simplex | |
| LIA | Linear Integer Arithmetic | CutSat | |
| LIRA | Mixed Real/Integer | Cuts + Branch | |
| IDL | Integer Difference Logic | Floyd-Warshall | |
| RDL | Real Difference Logic | Bellman-Ford | |
| UTVPI | Unit two-variable per inequality | ||
| NRA | Polynomial Real Arithmetic | Model based CAD, Incremental Linearization |