呼叫`eval`超時

Question

Leonardo：感謝您的快速回復！非常感激。

如果我喂下面的腳本Z3：

(set-option :MBQI true) 
(set-option :produce-models true) 
(declare-fun s1 ((_ BitVec 16)) (_ BitVec 16)) 
(assert (forall ((s0 (_ BitVec 16))) (bvuge s0 (s1 s0)))) 
(check-sat) 
(get-model) 
(eval (s1 #x0000)) 

Z3成功構建模型，其中s1給出確定身份的功能。但是，對eval的調用會導致Z3超時。有沒有我需要設置的特定選項？

另外，我注意到，如果我刪除行：

(set-option :MBQI true) 

然後Z3響應unknown。由於QBVF是可以確定的，這有點令人驚訝，我需要設置一個選項。我們是否應該在所有QBVF問題中將MBQI設置爲true，或者是否存在關於此實例的特殊情況？

謝謝..

Answer 1

Z3具有處理量詞幾個引擎：E-匹配，MBQI，疊加等 雖然QBVF是判定片斷，只有MBQI引擎可以決定。 電子匹配模塊僅在顯示公式不可滿足時纔有效。 對於可滿足的實例，它總是會失敗（返回未知）。 疊加模塊在純（無理論）一階邏輯公式中有效。

在某些版本的Z3中，默認情況下MBQI模塊未啓用，因爲它非常昂貴。 某些應用程序（如VCC和Spec＃）使用非常複雜的量化公式，它們不在任何可由MBQI支持的可判定片段中。 因此，MBQI模塊只是這些應用程序的開銷。 在Z3 3.1（可在Z3網站下載）中，默認情況下啓用MBQI。

在即將到來的Z3 3.2中，邏輯UFBV將被正式支持。 UBBV是QBVF的SMT-LIB名稱。 因此，您將可以使用(set-logic UFBV)，Z3會自動爲此邏輯配置自身。

關於eval命令，這是一個錯誤，我會解決它。該修復程序將在Z3 3.2中提供。