2

如果我给 Z3 一个公式，比如 p | q，我希望 Z3 返回 p=true, q=don't care（或切换 p 和 q），但它似乎坚持为 p 和 q 分配值（即使我没有完成转通话时开启Eval()）。除了对此感到惊讶之外，我的问题是如果 p 和 q 不是简单的道具怎么办。vars 但昂贵的表达式，我知道通常 p 或 q 都是正确的。有没有一种简单的方法可以让 Z3 返回一个“最小”模型，而不是浪费时间尝试同时满足 p 和 q？我已经尝试过MkITE了，但这没有什么区别。还是我必须使用某种策略来执行此操作？

谢谢！PS。我想补充一点，我已关闭 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))
4

1 回答 1

3

Z3 有一个称为相关性传播的功能。它在这篇文章中有所描述。它做你想做的事。请注意，在大多数情况下，相关性传播会对性能产生负面影响。在我们的实验中，它只对包含量词的问题有用（量词推理非常昂贵，以至于得到了回报）。默认情况下，Z3 将在包含量词的问题中使用相关性传播。否则，它不会使用它。这是一个在问题没有量词时如何打开它的示例（该示例也可在此处在线获得）

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()
于 2013-05-01T00:25:52.527 回答