1

I have been searching on whether z3 supports complex numbers and have found the following: https://leodemoura.github.io/blog/2013/01/26/complex.html

The author states that (1) Complex numbers are not yet implemented in Z3 as a built-in (this was written in 2013), and (2) that Complex numbers can be encoded on top of the Real numbers provided by Z3.

The basic idea is to represent a Complex number as a pair of Real numbers. He defines the basic imaginary number with I=(0,1), that is: I means the real part equals 0 and the imaginary part equals 1.

He offers the encoding (I mean, we can test it on our machines), where we can solve the equation x^2+2=0. I received the following result:

sat
x = (-1.4142135623?)*I

The sat result does make sense, since this equation is solvable in the simulation of the theory of complex numbers (as a result of the theory of algebraically closed fields) we have just made. However, the root result does not make sense to me. I mean: what about (1.4142135623?)*I?

I would understand to receive the two roots, but, if only one received, I do not understand why I get the negated solution.

Maybe I misread something or I missed something.

Also, I would like to say if complex numbers have already been implemented built in Z3. I mean, with a standard:

x = Complex("x")

And with tactics of kind of a NCA (from nonlinear complex arithmetic).

I have not seen any reference to this theory in SMT-LIB either.

Theo Deep
  • 666
  • 4
  • 15
  • 1
    There's nothing stopping you from taking Leo's code and using it as is. Does it not work for you for some reason? (Also note that Leo is the original author/developer of z3; so you can trust his code!) – alias Nov 16 '21 at 15:04
  • Nothing, just looking for the most 'standardised' frameworks to solve problems with the complex numbers. – Theo Deep Nov 16 '21 at 15:10

1 Answers1

2

AFAIK there is no plan to add complex numbers to SMT-LIB. There's a Google group for SMT-LIB and it might make sense to send a post there to see if there is any interest there.

Note, that particular blog post says "find a root"; this is just satisfiability, i.e. it finds one solution, not all of them. (But you can ask for another one by adding an assertion that says x should be different from the first result.)

Christoph Wintersteiger
  • 8,234
  • 1
  • 16
  • 30
  • How can I add that assertion? I guess I have it to the `s`, but do not know how. – Theo Deep Nov 16 '21 at 15:17
  • 2
    See https://stackoverflow.com/questions/11867611/z3py-checking-all-solutions-for-equation for how to get "all solutions," which essentially tells you how to add blocking clauses to get different solutions iteratively. – alias Nov 16 '21 at 16:14
  • 1
    Another source for the same: http://theory.stanford.edu/%7Enikolaj/programmingz3.html#sec-blocking-evaluations – alias Nov 16 '21 at 16:15