为什么CVC4 SMT解算器返回未知(不完全)？

Question

我在摆弄CVC4 SMT解算器在线版本 (用lang = cvc4)。

我使用的不是标准SMT-LIB格式，而是由CVC4实现的本地语言，因为它要简单得多。然而，我不能证明我的发言非常直截了当和明显。例如，第一个CHECKSAT给我sat (可满足)，这是正确的，但第二个CHECKSAT给我不知道。

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检查是不可判定的，因此，没有程序可以证明所有正确的语句。不过，这似乎是一个很简单的例子，所以我想我是误会了。

Answer 1

正如您所提到的，量词使逻辑半可判定，SMT求解器通常不能很好地处理这些问题。然而，在这种情况下，--fmf-bound选项似乎是有效的。(运行cvc4 --fmf-bound，您将看到它响应于sat)。该参数允许基于有限整数界的有限实例化，这恰好解决了这种情况。注意，它可能对其他问题起作用，也可能不起作用。

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

OPTION "fmf-bound";

有关详细信息，请参阅本文：cade24.pdf