找到的模型中没有显示新变量

Question

我正在使用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中更改此内容？

Answer 1

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，它应该可以解决问题。

Answer 2

您可以按如下方式规避此限制：

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