我嘗試了好幾種SMT求解器（CVC3，CVC4和Z3）以下看似瑣碎基準：SMT中量化算術的推理有什麼限制？
(set-logic LIA)
(set-info :smt-lib-version 2.0)
(assert (forall ((x Int)) (forall ((y Int)) (= y x))))
(check-sat)
(exit)
求解器都還不得而知。我知道這是一個不可判斷的片段（非線性），但我期待會有一些簡單的實例化啓發式方法來解決它。我也嘗試添加一些額外的常量的斷言，但它沒有幫助。
有沒有辦法來解決這些問題以及SMT中量化算術的推理有什麼限制？
您的示例屬於線性整數算術（LIA）類別。
LIA即Presburger Arithmetic承認量詞消除（qe），儘管qe過程的時間複雜度過高。
我不知道該CVC3和CVC4支持量詞消去了LIA，但Z3你可以做
(set-logic LIA)
(set-info :smt-lib-version 2.0)
(assert (forall ((x Int)) (forall ((y Int)) (= y x))))
(check-sat-using (then qe smt))
從Rise4Fun execution，我有unsat結果。
這裏的qe策略是在應用最終遊戲策略smt之前的預處理步驟。
Pad是正確的，qe預處理器可能會非常昂貴。而且，對於來自軟件驗證工具的公式，如VCC,Poirot,Dafny,VeriFast,Why3和ESCJava2，這些公式並不有效。這是不有效的，因爲這些應用程序產生的公式還包含未解釋的函數，數組等。
正如Pad的答案所示，Z3是一個引擎集合。它提供了API和命令，允許用戶選擇使用哪個引擎（或引擎組合）來解決問題。當用戶只是說(check-sat)是試圖猜測什麼是解決輸入公式的最佳引擎。猜測基於用戶提供的輸入公式和註釋的結構（例如：set-logic命令）。我們不斷擴展自動檢測到的碎片集以及我們提供的一系列引擎。
這就是說，Z3錯過了一個片段，如LIA，並沒有自動將qe過程應用於它，這是令人尷尬的。對於LIA公式，qe通常是最佳選擇。基於E匹配或MBQI的替代方法無效，因爲它們是用於完全不同的片段。
我只是committed code檢測到LIA（即使沒有使用set-logic）。該更改已在unstable（正在運行）分支中提供。它將在明天的夜間版本和下一個正式版本中提供。