如何讓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返回最小模型？

回答

相關問題