如何让Z3返回最小模型？

如果我给Z3一个像p | q，我会期望Z3返回p = true，q =不关心（或者用p和q切换），但是它似乎坚持给p和q赋值（即使我没有完成转身在拨打时）。除了对此感到惊讶之外，我的问题是如果p和q不是简单的道具。变量，但昂贵的表达式，我知道，通常p或q将是真实的。有没有一种简单的方法可以让Z3返回一个“最小”模型，而不是浪费时间来同时满足p和q？我已经试过MkITE但这没什么区别。或者我必须使用某种策略来执行此操作？如何让Z3返回最小模型？

的感谢！ 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))

来源

2013-04-30 S.N.

Z3具有称为相关性传播的特征。它在this article中描述。它做你想要的。请注意，在大多数情况下，相关性传播会对性能产生负面影响。在我们的实验中，它只对包含量词的问题有用（量词推理如此昂贵以至于付出代价）。默认情况下，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()

来源

2013-05-01 00:25:52

注：这里给出的例子并不在最新版本的Z3的工作，但它在使用SimpleSolver（）而不是Solver（）时工作。另见这里：http://stackoverflow.com/questions/28289410/z3-eliminate-dont-care-variables/28302963 – 2015-02-03 15:44:22

如何让Z3返回最小模型？

回答

相关问题