问题标签 [cvc4]

对于此示例：http : //pastebin.com/QyebfD1p z3 和 cvc4 作为 check-sat 的结果返回“未知”。两者都不是很详细的原因，有没有办法让 z3 对其执行更详细？

我在以下看似微不足道的基准测试中尝试了几个 SMT 求解器（CVC3、CVC4 和 Z3）：

求解器都返回未知数。我知道这是一个无法确定的片段（非线性），但我期待会有一些简单的实例化启发式方法可以解决它。我还尝试使用常量添加一些额外的断言，但它没有帮助。

有没有办法解决这些问题？ SMT 中量化算术的推理限制是什么？

以下 SMT-LIB 代码在 Z3、MathSat 和 CVC4 中运行没有问题，但在 Alt-Ergo 中没有运行，请告诉我发生了什么，非常感谢：

在之前的一篇文章中，证明了使用 Z3 SMT-LIB 的二面体组 D3 的一个定理。在这篇文章中，我们尝试使用以下 SMT-LIB 代码同时使用 Z3 和 CVC4 来证明这样的定理：

当使用 Z3 或 CVC4 执行此代码时，将获得正确的结果。在此处使用 Z3 在线运行此代码

问题是：

1. 在 Z3 的情况下，unsupported ; :incremental会生成一条消息。这个消息似乎并没有改变结果，为什么？

2. 在 CVC4 的情况下，unknown在 Z3 生成时生成一条消息sat。同样，这条消息似乎并没有改变结果，为什么？

3. 如何使用 Mathsat 执行 SMT-LIB 代码。

以下 SMT-LIB 代码在 Z3、MathSat 和 CVC4 中运行没有问题，但在 Alt-Ergo 中没有运行，请告诉我发生了什么，非常感谢：

在此处在线运行此示例

1. 在 Z3 中，unsupported ; :incremental生成了消息，但这不会改变计算并获得正确的答案。

2. 在 mathsat 中，unsupported会生成一些消息，但会显示正确答案。

3. 在 Cvc4 中，代码执行没有问题并获得正确答案。

4. 在 Alt-Ergo 中，代码在没有消息的情况下执行，但unsat会生成错误答案（正确答案是：）unsat, sat。

SMT2 标准规定调用 get-value 仅在调用 check-sat 并且仅当 check-sat 返回“sat”或“unknown”时才合法。

下面是一个 unsat 问题的简单示例：

由于问题未解决，因此 get-value 命令是非法的。取出任何一个断言，它就会变成 sat 并且 get-value 命令变得合法。所以我的问题是，你如何编写一个 SMT2 脚本来检查 check-sat 的返回值，并且只在它返回 sat 时才调用 get-value？

非法调用 get-value 对我来说是一个问题，因为我在一个流程中运行不同的 smt 求解器并检查程序的返回值，然后解析它们的输出。如果非法调用 get-value，CVC4 会将其返回值更改为错误状态。

我正在尝试从 FreeBSD 上的源代码编译CVC4，但我在配置时遇到了问题 - 找不到 GMP，即使共享对象显然位于公共路径中：

...这是输出./configure：

在那之后，我做了一些谷歌搜索，发现了一篇描述我认为可能相关的 ABI 错误的文章。然后我从源代码编译了 GMP，但仍然没有从配置脚本中找到运气。

什么可能导致此错误？任何创意或帮助将不胜感激。谢谢！

I want to prove a simplification which involves calculating log to the base 2. Is there any function available in z3/cvc4 for calculating it?

我试图弄清楚如何使用 C++ 接口在 CVC4 中编写量词。这是我试图运行但不能运行的示例。

相反，我只是收到一条错误消息：

但我将量词定义为forall. 我做错了什么？

编辑（问https://www.andrew.cmu.edu/user/liminjia/）：

语法错误。我们想知道是否

是真是假。但如果上述公式有效与否，CVC4 则不会，因为 SMT 求解器不是成熟的一阶逻辑定理证明器。

如果您想尝试一些可行的方法，请尝试使用 CVC4 语言：

在 C++ 中，我们有

这是原生 CVC 语言的示例：

我将如何使用 CVC4 的 C++ API 编写它？找不到有关如何执行此操作的任何文档。