I would like to see how Z3 (in Python) solves the "same"/"similar" sentence in different decidable first-order theories. The original sentence is the following:
Exists x,y :: forAll (x > -1000) -> (y < x)
So, for integers it would be as follows:
x, y = Ints('x y')
vars = [x,y]
l_1 = (-1000 < x)
l_2 = (y <= x)
phi = Implies(l_1, l_2)
Exists(vars, phi)
Now, I would like to test a very similar sentence, but for linear rationals, thus, I modify the original one to support them:
Exists x,y :: forAll (x > -1000.5) -> (y < x)
This can be encoded as follows:
x, y = Reals('x y')
vars = [x,y]
l_1 = (-1000.5 < x)
l_2 = (y <= x)
phi = Implies(l_1, l_2)
Exists(vars, phi)
Note I use the Reals since, for the linear fragment, rationals and reals are elementarily the same.
Also, to represent a similar problem in nonlinear reals, I just add an exponent to x in one of the literals (and eliminate the minus, since we cannot handle imaginary numbers).
Exists x,y :: forAll (x*x > 1000.5) -> (y < x)
Also easily encoded:
x, y = Reals('x y')
vars = [x,y]
l_1 = (1000.5 < x*x)
l_2 = (y <= x)
phi = Implies(l_1, l_2)
Exists(vars, phi)
My problem comes now. Imagine I want to explicitly imitate a similar problem in (linear) naturals and (nonlinear) complex numbers.
For the first one, I can simply remove the minus and get the following:
Exists x,y :: forAll (x > 1000) -> (y < x)
Encoded as follows:
x, y = Ints('x y')
vars = [x,y]
l_1 = (1000 < x)
l_2 = (y <= x)
phi = Implies(l_1, l_2)
Exists(vars, phi)
However, I can only encode this with Ints. Can I do it with Nats? I would like to use a type Nat, so that the sentence forall X, x>=0 is true. Do i have to add it as an axiom every time or what?
As for the second one, I added the minus to the nonlinearity to get a complex equation:
Exists x,y :: forAll (x*x > -1000.5) -> (y < x)
To encode this, I used the representation of complex numbers offered in https://leodemoura.github.io/blog/2013/01/26/complex.html You can see it below:
x = Complex('x')
y = Complex('y')
vars = [x,y]
l_1 = (-1000.5 < x*x)
l_2 = (y <= x)
phi = Implies(l_1, l_2)
Exists(vars, phi)
However, as I expected, looks I cannot compare two complex numbers (and raises the error '<' not supported between instances of 'float' and 'ComplexExpr'). How can I solve this sentence, then?
I hope my problem is understood more or less. You can see the summary below:
| Theory | State |
|---|---|
| Linear Natural arithmetic | ????? |
| Linear Integer arithmetic | Achieved |
| Linear Rational/real arithmetic | Achieved |
| Nonlinear real arithmetic | Achieved |
| Nonlinear complex arithmetic | ????? |
You've a few different questions here, which gets buried in the narrative; it's usually better to ask one-question at a time. But here's what seems to be the crux of what you're asking:
SMTLib does not support naturals; there's no native type to do so. Unfortunately, it's hard to reuse the Int type for this purpose, since you have to keep asserting values are >= 0 all the time, and with each operation you have to make sure the results remain naturals. (Subtraction being the obvious source of issue here.) In general, the kind of typing you want to do here is called predicate-subtyping, and that's beyond the capabilities of SMT solvers. Your best option is to model them like the complex numbers that Leonardo did, defining all the operations and stick to using them. Cumbersome, but doable.
Your second question regarding comparing complex numbers: Indeed you cannot use the built-in <, > etc. In Leonardo's blog that you linked, you need to define a custom function for what it means to be less-than/greater-than, and call those functions separately. Note that you can overload the internal __lt__, __le__, __gt__, __ge__, __eq__ and __ne__ methods; and thus take advantage of using the same symbol. To start with, I recommend using explicit methods; as overloading can trip you up if you're not careful. (Due to extremely weakly typed nature of the Python bindings.)