# Arithmetic

info

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.

info

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.

LogicFragmentSolverExample
LRALinear Real ArithmeticDual Simplex$x + \frac{1}{2}y \leq 3$
LIALinear Integer ArithmeticCutSat$a + 3b \leq 3$
LIRAMixed Real/IntegerCuts + Branch$x + a \geq 4$
IDLInteger Difference LogicFloyd-Warshall$a - b \leq 4$
RDLReal Difference LogicBellman-Ford
UTVPIUnit two-variable per inequality$x + y \leq 4$
NRAPolynomial Real ArithmeticModel based CAD, Incremental Linearization$x^2 + y^2 < 1$