在Z3觸發問題

Question

我最近在Z3中觀察到了幾個關於觸發的行爲，我不明白。不幸的是，這些例子來自大型的Boogie文件，所以我想我現在會抽象地描述它們，只是爲了看看是否有明顯的答案。但是，如果具體文件會更好，我可以附加它們。

基本上有三個問題，雖然第三個可能是第二個的特例。據我的理解，沒有預期的行爲，但也許我錯過了一些東西。任何幫助將不勝感激！

首先：在我的程序瑣碎的等式似乎就觸發關切地被忽略。例如，如果t1是應該匹配的模式進行量化公理，如果我加一條線的形式我的不羈程序

​​

然後t1不不似乎習慣作爲觸發一個術語用於量化的公理。我明確添加了該行，以便提供t1作爲證明者的觸發器，我經常在Boogie程序中執行此操作。

如果不是我引入一個額外的功能，說

function f(x : same_type_as_t1) : bool 
{ true } 

和現在，而不是添加一行

assert f(t1); 

到我的程序，然後t1確實似乎被用來作爲觸發Z3。我已經檢查過前一個程序的Z3翻譯，並且t1上的（平凡的）等式確實存在於布吉翻譯中（即，這不是布吉試圖做一些聰明的事情）。

其次：輔助模式似乎不能正常工作。例如，我有一個計劃，其中一個公理的形式

axiom (forall ... :: {t1,t2} {t3,t4,t5} .....); 

和一種情況，即t3, t4和t5都發生了。該程序未能驗證，顯然是因爲該公理沒有實例化。但是，如果我將公理改寫爲

axiom (forall ... :: {t3,t4,t5} {t1,t2} .....); 

然後程序驗證。在這兩種情況下，運行Boogie的時間大約是3秒，模式生存到Z3輸出。

三：這很可能是第二個問題的症狀，但是我對以下行爲感到驚訝：

我寫形式的公理

​​

，並在發生t2和t3的情況下，第一個公理沒有被實例化（我預料它是，因爲在第二個公理的實例化後，發生了t1）。但是，如果我重寫爲

axiom (forall .. :: {t2,t3} {t1,t2} ....); 

axiom (forall ... :: {t2,t4} {t2,t3} ...some expression involving t1...); 

那麼第一個公理就被實例化了。但是，如果由於某種原因二次模式沒有被普遍使用，那麼這也將解釋這種行爲。

如果明確的例子是有用的，我可以附加很長的例子，並可以嘗試減少它們（但當然，觸發問題有點微妙，所以我可能會失去行爲，如果我舉例說明太小）。

非常感謝您的任何意見！

亞歷夏天

編輯：這裏是部分地示出了上述第二和第三行爲的例子。我附加了Boogie代碼，使其更容易閱讀，但如果它更有用，我也可以複製或通過電子郵件發送Z3輸入。我已經刪除了幾乎所有原始的Boogie代碼，但似乎很難使其更簡單，而不會完全失去行爲。

已經低於代碼我原來的例子巧妙地表現不同，但我認爲這是足夠接近。基本上，下面標記爲（1）的公理未設法使其第二模式集合匹配。如果我將公理（1）註釋掉，而是用（兩個當前註釋的）公理（2）和（3）替換它們，這兩個公理（2）和（3）就是兩個模式集合中的每一個的原始副本，然後程序將進行驗證。事實上，在這個特殊情況下，有足夠的公理（2）。在我原來的代碼中（在我將它裁減之前），公理（1）中的兩個模式集合的順序也是足夠的，但在我的小代碼中似乎不再是這種情況。

type ref; 
type HeapType; 

function vals1(HeapType, ref) returns (ref); 
function vals2(HeapType, ref) returns (ref); 
function vals3(HeapType, ref) returns (ref); 

function heap_trigger(HeapType) returns (bool); 

function trigger1(ref) returns (bool); 
function trigger2(ref) returns (bool); 

axiom (forall Heap: HeapType, this: ref :: {vals1(Heap, this)} (vals1(Heap, this) == vals3(Heap,this))); 

axiom (forall Heap: HeapType, this: ref :: {vals2(Heap, this)} trigger2(this)); 

// (1) 
axiom (forall Heap: HeapType, this: ref :: {vals1(Heap, this)} {trigger1(this), heap_trigger(Heap), trigger2(this)} (vals1(Heap, this) == vals2(Heap, this))); 

// (2) 
// axiom (forall Heap: HeapType, this: ref :: {trigger1(this), heap_trigger(Heap), trigger2(this)} (vals1(Heap, this) == vals2(Heap, this))); 
// (3)  
// axiom (forall Heap: HeapType, this: ref :: {vals1(Heap, this)} (vals1(Heap, this) == vals2(Heap, this))); 

procedure test(Heap:HeapType, this:ref) 
{ 
    assume trigger1(this); assume heap_trigger(Heap); 

    assert (vals2(Heap, this) == vals3(Heap,this)); 
} 

Answer 1

第一個問題：

瑣碎的斷言通過Z3中的預處理步驟簡化。斷言assert t1 == t1簡化爲assert true。因此，術語t1不被E匹配引擎考慮。技巧assert f(t1)是使術語t1可用於Z3的電子匹配的標準技巧。 Z3中的當前預處理器不夠「足夠聰明」以去除不相關的斷言assert f(t1)。當然，Z3的未來版本可能會有更好的預處理器，而且這個技巧不再適用。

對於第二個和第三個問題，這將是不錯的產生描述的行爲（小）Z3腳本。

編輯。 我分析了你的問題中的例子。事實證明這是Z3中的一個錯誤。我修復了這個錯誤，並且修復程序將在Z3 4.1中提供。 感謝您抽出時間縮小示例的大小。對此，我真的非常感激。這將需要「永遠」在更大的實例中發現這個錯誤。 電子匹配引擎缺少一些實例。 該問題影響包含使用函數符號f的多模式的Z3腳本，該函數符號不會出現在任何一元模式中。 多模式應該在地面f應用之前出現。 此外，MBQI引擎必須禁用。默認情況下，Boogie禁用MBQI引擎。 在這種情況下，可能會錯過多模式的實例。 這個bug在E-matching引擎中很長一段時間。我認爲，這是從來沒有的原因有兩個檢測：

1，不影響穩健（Z3不會產生一個錯誤的答案，但「未知」的答案）

2- MBQI引擎「補償」爲任何缺失的實例。

關於爲電子匹配提供附加條款的額外命令，我們可以通過以下方式進行模擬。 命令add_term(t)只是(assert (add_term t))的語法糖。 即使我們實現了一個預處理器來消除只出現正面（或負面）的謂詞符號，它也不會消除保留的謂詞符號add_term。因此，即使我們添加了這個預處理器，這個技巧也會繼續工作。