如果我给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))
注:这里给出的例子并不在最新版本的Z3的工作,但它在使用SimpleSolver()而不是Solver()时工作。另见这里:http://stackoverflow.com/questions/28289410/z3-eliminate-dont-care-variables/28302963 – 2015-02-03 15:44:22