CODEWITHSUNDEEP
z3smtz3py
Guo Xian HO
Guo Xian HO

Reputation: 89

z3 conversion from int to float and vice versa for any expression

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

Upvotes: 1

Views: 1334

Answers (1)

alias
alias

Reputation: 30428

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.

Upvotes: 2

Related Questions