Z3中的Horn子句

Question

如果要分析的程序的語義是作爲Horn子句給出的，則Z3現在支持求解歸納不變量（意味着期望的屬性）。

但z3.codeplex.com上的Z3源代碼的master分支中的版本不支持此功能。由於Z3通過使用內插的PDR算法解決了這些Horn子句問題，因此我編譯爲interp分支（d8b31773b809），它支持(set-logic HORN)。

據我所知，Horn-clause問題是用未知的謂詞來表示不變量，並且X×Y上的謂詞只是一個從X×Y到Bool的函數。到現在爲止還挺好。

我試過的第一個例子只是一個推斷for(int i=0; i<=10; i++)循環的歸納不變量的問題。

(set-logic HORN) 
(declare-fun inv (Int) Bool) 
(assert (inv 0)) 
(assert (forall ((I Int)) (or (> I 10) (not (inv I)) (inv (+ I 1))))) 
(check-sat) 

到目前爲止好，得到了sat。現在剛剛添加(assert (not (inv 15))，我得到了unsat。我然後嘗試

(set-logic HORN) 
(declare-fun inv (Int) Bool) 
(assert (inv 0)) 
(assert (not (inv 15))) 
(check-sat) 

並得到unsat。

我在做什麼錯？

Answer 1

使用「不穩定」分支。 「interp」分支用於內部開發，此分支的狀態可能會波動。 我在第二個問題上得到了答案「sat」。

稍微更有趣的第一個問題的版本是：

(set-logic HORN) 
(declare-fun inv (Int) Bool) 
(assert (inv 0)) 
(assert (forall ((I Int)) (or (> I 10) (not (inv I)) (inv (+ I 1))))) 
(assert (forall ((I Int)) (=> (inv I) (<= I 11)))) 
(check-sat) 
(get-model) 

它產生明顯的電感不變。 如果通過

(assert (forall ((I Int)) (=> (inv I) (<= I 10)))) 

替換最後斷言相反，你得到一個（難以閱讀）的證明。