Z3 python模型比较

Question

拥有一组公式并使用z3py创建两个模型old_model = solver.model()和new_model。如何获取在两个模型中具有不同赋值的变量名称列表？

需要一个通用的解决方案来考虑公式集中的所有自由变量。如果可能的话，一个变量由var = Int('varname') m定义，并且只在公式ForAll(var, ...)中使用，当开始比较模型时，var不需要考虑该变量。

这个想法是在调试期间使用比较，并查看是否存在任何定义模型之间差异的意外变量，或者变量不应出现在模型中。

Answer 1

不清楚你在问什么;但是当 z3 给你一个模型时，它只是一个将变量映射到它们的值的字典。你可以在Python中轻松保留它们：

from z3 import *
s = Solver()
x, y, z = Ints('x y z')
s.add(x + y > 5)
s.add(ForAll([z], z > z-1))
s.check()
m = s.model()
print m
# get the variables:
for v in m:
  print v

这将打印：

[y = 0, x = 6]
y
x

正如你所看到的，y和x在那里，z没有;正如你想要的那样。如果您有多个模型，您可以简单地分别查询它们并查找差异并执行您想要的任何编程。这是你要找的吗？