量詞和模式（QBF公式）

Question

我想在z3的smt-lib 2語法中編碼QBF。運行在警告

警告Z3結果：未能找到量詞的模式（量詞ID：！k來14）

和滿足性的結果是 「未知」。

的代碼如下：

(declare-fun R (Bool Bool Bool Bool) Bool) 
(assert 
    (forall ((x2 Bool) (x3 Bool)) 
    (exists ((y Bool)) 
     (forall ((x1 Bool)) 
     (R x1 x2 x3 y) 
    ) 
    ) 
) 
) 
(check-sat) 

我被重寫代碼擺脫警告到

(set-option :auto-config false) 
(set-option :mbqi false) 
(declare-fun R (Bool Bool Bool Bool) Bool) 
(declare-fun x1() Bool) 
(declare-fun x2() Bool) 
(declare-fun x3() Bool) 
(declare-fun y() Bool) 
(assert 
    (forall ((x2 Bool) (x3 Bool)) 
    (! 
    (exists ((y Bool)) 
    (! 
     (forall ((x1 Bool)) 
     (! 
     (R x1 x2 x3 y) 
     :pattern((R x1 x2 x3 y))) 
    ) 
    :pattern((R x1 x2 x3 y))) 
    ) 
    :pattern((R x1 x2 x3 y))) 
) 
) 
(check-sat) 

結果爲坐在查詢，但是，仍然是「未知」。

我猜我需要的模式是正確的嗎？如何爲嵌套量詞指定它們？儘管如此，更簡單的量詞實例似乎無需模式註釋即可運行。

不幸的是，對於What is the reason behind the warning message in Z3: "failed to find a pattern for quantifier (quantifier id: k!18) "和z3指南的回答並沒有太多幫助。

Answer 1

該警告信息可以忽略。它只是告訴你，電子匹配引擎將無法處理這個量化的公式。

電子匹配僅用於顯示問題不可滿足。既然你的例子是可以滿足的，那麼電子匹配就不會很有用。也就是說，Z3將不能使用E匹配引擎返回sat。基於模型的量化器實例化（MBQI）是Z3中唯一能夠顯示包含量詞的問題是可滿足的引擎。

對於您的示例，使用默認配置，Z3將返回sat。它返回unknown，因爲您禁用了MBQI模塊。

MBQI引擎保證Z3是許多片段的決定過程（請參閱http://rise4fun.com/Z3/tutorial/guide）。但是，一般情況下它非常昂貴，當快速和近似的答案足夠時應該禁用。在這種情況下，unknown可能會被解讀爲probably sat。驗證工具，如VCC禁用MBQI模塊，因爲它不能決定它們產生的公式。也就是說，由VCC產生的公式不在任何可由MBQI引擎決定的片段中。 我們說片段可以由Z3決定，當片段Z3中的任何公式將返回sat或unsat（即，它不返回unknown）。當然，這個說法假設我們擁有無限的資源。也就是說，當內存耗盡或者用戶指定超時時，Z3也可能失敗（即，返回unknown）用於可判斷片段。

最後，Z3 3.2在MBQI引擎中有一個bug。該錯誤已得到解決，並不會影響您的問題。如果你需要，我可以給你一個Z3 4.0的預發佈版本，其中包含錯誤修復。