z3 4.3.2未能找到Why3生成（可滿足）目標的模型

我試圖使用Why3的Z3後端爲了檢索模型，然後可以用於派生測試案例展示程序中的錯誤。但是，對於任何Why3目標而言，Z3 4.3.2版似乎無法回答sat。它看起來像Why3使用的某些公理化定義混淆了Z3。例如，下面的例子（其是什麼Why3產生一小部分）z3 4.3.2未能找到Why3生成（可滿足）目標的模型

(declare-fun abs1 (Int) Int) 

;; abs_def 
    (assert 
    (forall ((x Int)) (ite (<= 0 x) (= (abs1 x) x) (= (abs1 x) (- x))))) 

(check-sat)

導致timeout使用下面的命令行：

z3 -smt2 model.partial=true file.smt2 -T:10

在另一方面，改變定義

(declare-fun abs1 (Int) Int) 

;; abs_def 
    (assert 
    (forall ((x Int)) (=> (<= 0 x) (= (abs1 x) x)))) 

    (assert 
    (forall ((x Int)) (=> (> 0 x) (= (abs1 x) (- x)))))

會得到我的模型（這看起來很合理）

(model 
    (define-fun abs1 ((x!1 Int)) Int 
    (ite (>= x!1 0) x!1 (* (- 1) x!1))) 
)

但如果我嘗試添加下一個公理存在於原始的Why3文件，即

;; Abs_pos 
(assert (forall ((x Int)) (<= 0 (abs1 x))))

再次Z3回答timeout。

在Z3的配置中是否存在缺少的東西？此外，在以前的Why3版本中，有一個選項MODEL_ON_TIMEOUT，允許在這種情況下檢索模型。儘管無法保證這是真正的模型，因爲Z3無法完成檢查，實際上，這些模型通常包含我需要的所有信息。但是，我在4.3.2中沒有找到類似的選項。它還存在嗎？

更新最後公理Abs_pos是錯的（我玩弄了一下與Why3的輸出在這裏發帖之前，結束了粘貼問題的版本不正確）。這現在已經修復。

來源

2015-02-23 Virgile

附加公理

（斷言（未（forall的（（X智力））（< = 0（ABS1 X）））））

使得問題不可滿足，因爲ABS1總是返回一個非負整數，並且在附加公理中，對於某個x，您需要存在abs1的負結果。網絡版Z3返回的結果不如預期，請參閱here。

來源

2015-02-24 09:43:20

糟糕，我意識到我粘貼了我試圖玩弄Why3的輸出的錯誤部分。 Why3提供的真正公理當然是（assert（forall（（x Int））（<= 0（abs1 x））））'。我會相應地編輯我的問題，對於噪音感到抱歉。 – Virgile 2015-02-24 09:51:44

z3 4.3.2未能找到Why3生成（可滿足）目標的模型

回答

相關問題