Z3 python模型比较
Z3 python模型比较
提问于 2019-01-09 12:55:19
拥有一组公式并使用z3py创建两个模型old_model = solver.model()和new_model。如何获得在两个模型中具有不同赋值的变量名列表？
需要一个考虑公式集中所有自由变量的通用解决方案。如果可能，存在由var = Int('varname')m定义变量且仅在公式ForAll(var, ...)中使用的情况，当开始比较模型时，不需要考虑变量var。
这个想法是在调试期间使用比较，并查看是否存在定义模型之间差异的任何意外变量，或者变量不应出现在模型中。
回答 1
Stack Overflow用户
回答已采纳
发布于 2019-01-09 16:09:57
不清楚您在问什么；但是当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不在那里；我认为正如您所希望的那样。如果您有多个模型，您可以简单地分别查询它们，并查找差异并执行您想要的任何编程。这就是你要找的吗？
页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/54110662
复制相关文章
相似问题
添加站长 进交流群
领取专属 10元无门槛券
AI混元助手 在线答疑
关注 腾讯云开发者公众号
洞察 腾讯核心技术
剖析业界实践案例
社区富文本编辑器全新改版！诚邀体验～
全新交互，全新视觉，新增快捷键、悬浮工具栏、高亮块等功能并同时优化现有功能，全面提升创作效率和体验
腾讯云开发者
