0

我正在摆弄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 检查是不可判定的，因此，没有程序可以证明所有正确的陈述。但是，这似乎是一个非常简单的案例，所以我想我误解了一些东西。

4

1 回答 1

1

正如您所指出的，量词使逻辑半可判定，而 SMT 求解器通常不能很好地处理此类问题。然而，在这种特殊情况下，--fmf-bound选项似乎是有效的。（运行cvc4 --fmf-bound，你会看到它回复sat）。此参数启用基于有限整数边界的有限实例化，这恰好解决了这种情况。请注意，它可能适用于也可能不适用于其他问题。

您可以通过在脚本中添加以下行来实现相同的目的：

OPTION "fmf-bound";

详情见本文：https ://cvc4.cs.stanford.edu/papers/CADE24-2013/qi_for_fmf_reynolds_cade24.pdf

于 2021-12-07T19:39:22.327 回答