时间戳

首页 > 解决方案 > 新变量未显示在找到的模型中

z3 - 新变量未显示在找到的模型中

问题描述

我正在使用 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 中改变它？

标签： z3smtz3py

解决方案

FreshInt/FreshReal等旨在创建用户不可见的内部变量。您应该改为使用Int('name')andReal('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 就像你所说的那样，它应该可以解决问题。

推荐阅读