如果我给 Z3 一个像 p | 这样的公式q，我希望 Z3 返回 p=true, q=dont care （或者 p 和 q 切换），但它似乎坚持为 p 和 q 赋值（即使我没有完成转换）通话时亮起Eval()）。除了对此感到惊讶之外，我的问题是如果 p 和 q 不是简单的道具怎么办？ vars 但昂贵的表达式，我知道通常 p 或 q 将为真。有没有一种简单的方法可以要求 Z3 返回“最小”模型，而不是浪费时间尝试同时满足 p 和 q？我已经尝试过了MkITE但这没有什么区别。或者我必须使用某种策略来强制执行此操作？
谢谢！
附言。我想补充一点，我已经关闭了 AUTO_CONFIG，但 Z3 正在尝试为 or 的两个分支中的常量赋值：例如，在下面的代码片段中，我希望它分配给 path2_2 和 path2_1 或分配给 path2R_2 和 path2R_1，但不能同时分配给两者
(or (and (select a!5 path2_2) a!6 (select a!5 path2_1) a!7)
(and (select a!5 path2R_2) a!8 (select a!5 path2R_1) a!9))
Z3有一个称为相关性传播的功能。它描述于本文。它做你想做的事。请注意，在大多数情况下，相关性传播会对性能产生负面影响。在我们的实验中，它仅对包含量词的问题有用（量词推理的成本如此之高，以至于它是值得的）。默认情况下，Z3 将在包含量词的问题中使用相关性传播。否则，它不会使用它。
这是一个关于如何在问题没有量词时打开它的示例（该示例也可以在线获取）here)
x, y = Bools('x y')
s = Solver()
s.set(auto_config=False, relevancy=2)
s.add(Or(x, y))
print s.check()
print s.model()
本文内容由网友自发贡献，版权归原作者所有，本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容，请联系:hwhale#tublm.com(使用前将#替换为@)
