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