Z3返回不同的答案WITH和WITHOUT使用推/流行？

當檢查使用Z3以下問題，我包裹或不通過對push/popZ3返回不同的答案WITH和WITHOUT使用推/流行？

(declare-fun sz_53() Int) 
(declare-fun x() Int) 
(declare-fun u() Int) 
(declare-fun y() Int) 
(assert (> u 0)) 
(assert (= (+ y (- 0 0)) 0)) 
(assert (or (= (- x u) 0) (> x 0))) 
(assert (<= (* (- 0 1) sz_53) 0)) 
(assert (or (= (- x u) 0) (not (= (- x u) 0)))) 
(assert (not (and (and (and (and (exists ((sz_64 Int)) (and (= sz_64 0) (exists ((sz_62 Int)) (and (exists ((sz_55 Int)) (and (<= (* (- 0 1) sz_55) 0) (= (+ sz_53 (- sz_62 sz_55)) 0))) (= (+ sz_62 (- (- 0 1) sz_64)) 0))))) (>= y 0)) (or (= (+ x (* (- 0 1) y)) 0) (> x 0))) (not (= (+ u (* (- 0 1) y)) 0))) (not (= (+ u (* (- 0 1) y)) 0))))) 
(assert (not false)) 
(check-sat)

特別包裹它，當接收不同的答案，直接（未通過push/pop包裝）檢查時，Z3返回unsat （這裏是網上鍊接：http://rise4fun.com/Z3/cDt3）

然而，push/pop包裹時，Z3返回unknown （http://rise4fun.com/Z3/epyh0）

有沒有人知道爲什麼Z3的行爲如此？

非常感謝！

來源

2015-07-01 Trung Ta

這個問題包含通用量詞（不是......（存在...）），當Z3認爲它不能解決問題時，Z3會放棄這些問題（這就是爲什麼你會得到unknown）。根據使用哪種策略/策略/解算器，它可能決定放棄更早或更晚。在這種特殊情況下，它使用不支持推/拉的解算器，添加它們會導致它回落到使其放棄的不同解算器（或參數設置）上。

有就這個問題和相關問題在計算器上多個問題，例如，z3 produces unknown for assertions without quantifiers，Different check-sat answers when asserting same property in between，Why does Z3 return 「unknown」 on this simple input?

來源

2015-07-01 12:21:52

感謝您的完整的答案！我已閱讀您提到的相關問題和答案，但對於這種情況沒有任何好的解決方案。我覺得在這種情況下，Z3很快就會放棄。希望它在未來的版本中會有所改進。 –

Z3返回不同的答案WITH和WITHOUT使用推/流行？

回答

相關問題