1

Say for a python expression, e.g.

float(x + 1 * 2) * 2 == 2

how would I convert this to a z3 expression? Using the obvious ToReal(x + 1 * 2) does not work. On a side note, i've used z3.ToReal and I can't get even simple example to sat, but ToInt is working as expected. E.g.

from z3 import *
a = Int("a")
b = Real("b")
s = Solver()
s.add(ToReal(a) == 1.1)
s.check()
>>> unsat
s.reset()
s.add(ToInt(b) + 1.1 == 2)
s.check()
>>> sat
Guo Xian HO
  • 89
  • 7

1 Answers1

2

I'm not sure why you're saying it doesn't work. It seems to work as expected:

>>> from z3 import *
>>> x = Int('x')
>>> s = Solver()
>>> s.add(ToReal(x + 1 * 2) * 2 == 2)
>>> print(s.check())
sat
>>> print(s.model())
[x = -1]

And indeed with the integer value x = -1, the equality you wanted indeed holds.

You'll have to be a bit more clear on what exactly you expected, and what z3 did (or didn't!) do.

alias
  • 28,120
  • 2
  • 23
  • 40
  • It seems like i'll get unsat when `x` is getting a real number. If i do `ToReal(x) / 2 == 3 / 2` it will return model `x = 3` which is expected, but when i do `ToReal(x) == 0.5`, it gave me unsat. – Guo Xian HO Dec 18 '20 at 04:21
  • After refreshing my brain with some good sleep, now i do think that that is expected behavior since `x` is defined as Int. If I want to convert the variable to Real i can just create a new Real variable. – Guo Xian HO Dec 18 '20 at 04:39
  • Another question will be, IIRC ToInt is taking the `floor` value of. Is there any way to take the `ceiling` value? – Guo Xian HO Dec 18 '20 at 04:43
  • Indeed. There's no `x` such that `ToReal(x) == 0.5` would ever hold; as all integers are also reals; i.e., there's a perfect injection. You can prove `ToReal(x) == x` for all x. – alias Dec 18 '20 at 05:19
  • Ceiling/Floor functions, while present, usually are not handled all that well by SMT. solvers. See https://stackoverflow.com/questions/61388141/floor-and-ceiling-function-implementation-in-z3 for an explanation. – alias Dec 18 '20 at 05:33