A user recently asked me if Z3 had support for Complex numbers. Unfortunately, it does not. This is on my TODO list, but it is has very low priority at this moment. Internally, Z3 already has a lot of machinery for supporting Complex numbers, but there is a lot of “plumbing” missing, such as extending the parsers, simplifiers, models, and root isolation procedures. Most of this work is not really fun.

In the meantime, we can encode Complex numbers on top of the Real numbers provided by Z3. The basic idea is to represent a Complex number as a pair of Real numbers. This is not the most efficient way of implementing a decision procedure for the theory of Complex numbers, but it is simple and allows us to handle problems that mix Real and Complex number reasoning. Moreover, we can decide the resulting problem using the new nonlinear arithmetic solver nlsat that is available in Z3.

We can represent a complex number

\[ a + b i \]

as a pair of real numbers

\[ (a, b) \]

Then the operations on Complex numbers can be easily encode on top of the operations on Real numbers provided by Z3. Here is the encoding of the main operations.

\begin{eqnarray*}
(a_1, b_1) + (a_2, b_2) & = & (a_1 + a_2,\, b_1 + b_2) \\
(a_1, b_1) - (a_2, b_2) & = & (a_1 - a_2,\, b_1 - b_2) \\
(a_1, b_1) \times (a_2, b_2) & = & (a_1 a_2 - b_1 b_2,\, a_1 b_2 + b_1 a_2) \\
(a, b)^{-1} & = & (\frac{a}{a^2 + b^2}, -\frac{b}{a^2 + b^2}) \mbox { if } a \neq 0 \vee b \neq 0 \\
(a_1, b_1) \div (a_2, b_2) & = & (a_1, b_1) \times (a_2, b_2)^{-1} \mbox { if } a \neq 0 \vee b \neq 0 \\
\end{eqnarray*}

The definition of the multiplicative inverse follows from basic algebraic manipulation

\[
\frac{1}{a + b i} = \frac{a - b i}{(a + b i)(a - b i)} = \frac{a - b i}{a^2 + b^2} = \frac{a}{a^2 + b^2} - \frac{b}{a^2 + b^2} i
\]

It is straightforward to implement the operations above using the Z3 Python API. We can even create a class `ComplexExpr`

to wrap the pair of Z3 real expressions and overload the usual operators `+`

, `-`

, `*`

, `/`

. This class has two
fields `.r`

(the real part) and `.i`

(the imaginary part). The auxiliary function `_to_complex`

is used to convert `a`

into a
Z3 “Complex” number if it is not already one.

The function `Complex(a)`

creates a new “Complex” variable. Actually, it creates two real variables named `a.r`

and `a.i`

.
The constant `I`

is just an alias for the pair `(0, 1)`

.

The function `evaluate_cexpr`

“retrieves” the value of a Complex expression `e`

in the model `m`

.

Now, we have all the pieces we need to solve our first problem. Find a root of `x*x + 2`

.

In the example above, I used `Tactic('qfnra-nlsat').solver()`

to create a solver based on nlsat.
Note that, the problem above is unsatisfiable on the Reals.
We can try this example online at rise4fun.