z3 - z3 从 int 到 float 的转换，反之亦然，适用于任何表达式

Question

说一个python表达式，例如

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

我如何将其转换为 z3 表达式？使用明显的ToReal(x + 1 * 2)不起作用。在旁注中，我已经使用z3.ToReal并且我什至无法获得简单的示例来坐下，但是ToInt按预期工作。例如

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

标签： z3smtz3py

Answer 1

我不知道你为什么这么说it doesn't work。它似乎按预期工作：

>>> 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]

事实上，对于整数值x = -1，你想要的平等确实成立。

您必须更清楚您的预期是什么，以及 z3 做了什么（或没有做什么！）。