我正在擺弄CVC4 SMT 求解器在線版本（使用 lang = cvc4）。
我沒有使用標準的SMT-LIB 格式，而是使用 CVC4 實作的本地語言，因為它簡單得多。但是，我無法證明非常直接和明顯的陳述。例如，第一個 CHECKSAT 給了我sat (satisfiable)，這是正確的，但第二個 CHECKSAT 給了我unknow。
OPTION "incremental";
ASSERT FORALL (k : INT): ((k > 5 AND k < 7) => (k = 6));
CHECKSAT; % this returns sat, okay!
arr: ARRAY INT OF REAL;
ASSERT arr[6] = 123;
ASSERT FORALL (k : INT): ((k > 5 AND k < 7) => (arr[k] = 123));
CHECKSAT; % this returns unknown, why?
為什么CVC4不能證明這么簡單的謂詞邏輯運算式？據我了解，SMT 檢查是不可判定的，因此沒有程式可以證明所有正確的陳述句。然而，這似乎是一個非常簡單的案例，所以我想我誤解了一些東西。
uj5u.com熱心網友回復：
正如您所指出的，量詞使邏輯具有半可判定性，而 SMT 求解器通常不能很好地處理此類問題。然而，在這種特殊情況下，--fmf-bound選項似乎是有效的。（即運行cvc4 --fmf-bound，您會看到它回應sat）。此引數啟用基于有限整數邊界的有限實體化，恰好解決了這種情況。請注意，它可能適用于也可能不適用于其他問題。
您可以通過在腳本中添加以下行來實作相同的效果：
OPTION "fmf-bound";
詳情見這篇論文：https : //cvc4.cs.stanford.edu/papers/CADE24-2013/qi_for_fmf_reynolds_cade24.pdf
轉載請註明出處，本文鏈接：https://www.uj5u.com/shujuku/378580.html