我正在使用 z3 编写一个静态检查器。我有以下问题：
>>> from z3 import *
>>> s = Solver()
>>> s.add(FreshInt() + FreshInt() > 0)
>>> s.check()
sat
>>> s.model()
[]
如您所见，模型中未显示新变量。我也无法获得它们的价值：
>>> a = FreshInt()
>>> s.add(a > 3)
>>> s.check()
sat
>>> s.model()
[]
>>> s.model()[a]
我查看了文档，但找不到改变这种行为的方法。我可以自己生成唯一的变量，但如果 z3 可以为我处理这个问题，那就太好了。有人可以指出我正确的方向吗？还是不能在 z3py 中更改？
【问题讨论】：
FreshInt;这些可以被认为是“内部的”。使用a = Int('a')，该示例按预期工作。
FreshInt/FreshReal 等用于创建用户不可见的内部变量。您应该改用Int('name') 和Real('name') 创建将在模型中显示的用户级变量。
如果你真的想看值，你可以添加一个observer函数并像这样使用它：
from z3 import *
def observeInt(s, a):
obs = Int('observer')
s.add(obs == a)
# might want to check the following really returns sat!
s.check()
print s.model()[obs]
s = Solver()
a = FreshInt()
s.add(a + FreshInt() > 0)
s.add(a > 12)
print s.check()
observeInt(s, a)
打印出来：
sat
13
这显然并不便宜（因为它涉及到对check 的调用），但它是安全的，只要它用于调试情况下的强臂 z3 就像你所说的那样，它应该可以解决问题。
【讨论】：
Int/Real？这是唯一的区别。 （换句话说，如果你想让 z3 向你展示它们，只需使用 Int/Real，如果你不想自己创建名称，可以使用 Axel 的技巧。）
您可以通过以下方式规避此限制：
freshIntIdx = 0
def myFreshInt():
global freshIntIdx
freshIntIdx += 1;
return Int('fi' + str(freshIntIdx))
a = myFreshInt()
b = myFreshInt()
s = Solver()
s.add(a + b > 5, a > 0, b > 0, a + b < 10)
print(s.check())
m = s.model()
print("a = %s" % m[a])
print("b = %s" % m[b])
【讨论】：