问题标签 [cvc4]

QF_NRA 中是否包含除以零？

SMT-LIB 标准在这件事上令人困惑。定义标准的论文根本没有讨论这一点，实际上 NRA 和 QF_NRA 并没有出现在该文档的任何地方。标准网站上提供了一些信息。实数定义为包括：

当涉及常数值时，这明确地将零从分母中排除。但是，后来，除法被定义为：

紧随其后的是一条注释：

这似乎是矛盾的，因为第一个引用说这(/ m 0)不是 QV_NRA 中的数字，但后一个引用说这/是一个(= t1 (/ t2 0))可以满足任何t1和的函数t2。

事实上，除以零似乎包含在 SMT-LIB 中，尽管声明只有非零时才是(/ m n)实数。n这与我之前的一个问题有关：y=1/x, x=0 在实数中是否可以满足？

SMT-LIB 中的 QF_NRA 逻辑是否可判定？

我知道塔斯基证明了非线性算术是可判定的，即实数中的多项式系统是可判定的。但是，QF_NRA 是否属于这一范畴并不明显，因为 QF_NRA 包含除法。所以第一个问题是 QF_NRA 中的除法是否包括分母可能为零的变量除法。 我将其作为一个单独的问题发布，因为事实证明，仅靠自己回答这个问题就足够困难了。

如果除以零不是 QF_NRA 的一部分，那么 QF_NRA 中的除法可以转换为乘法，并且问题将是可判定的，如 Tarski 所证明的。如果除法实际上包含在 QF_NRA 中，那么我就不太确定了。我的感觉是，问题仍然可以按情况分解，为发生被零除的情况引入新变量。在这种情况下，QF_NRA 仍然是可判定的。

我尝试使用 C++ API 在 cvc4 中旋转位向量，但是当涉及到运算符表达式时，该 API 有点令人困惑。

使用以下代码（摘录）：

执行此产生：

有人知道如何处理 cvc4 的运算符构造吗？

我想知道人们如何在 SMT 求解器中实现浮点算术结构的位爆破。是否有任何现有的库或设施可以做到这一点（VHDL，...），或者它们是从头开始实现的？这代表了多少行（C？C++？）代码？

提前致谢。

使用 smtlib 我想使用 QF_UFNRA 进行模运算。这使我无法使用 mod、to_int、to_real 之类的东西。

最后我想在下面的代码中得到 z 的小数部分：

当然，正如我在这里提出的这个问题，暗示它没有成功。

有人知道如何使用逻辑 QF_UFNRA 将 z 的小数部分转换为 z1 吗？

我正在按照他们的教程尝试Why3 ，但我收到了Unknown logical symbol map.Map.const多个证明者的消息。以下是我试图证明的理论的内容：

以下是各种证明者的结果：

z3：

cvc4:

光伏：

这是我的why3版本信息：

错误消息中提到的 .drv 文件上的时间戳与我的 why3 可执行文件上的时间戳相匹配。

我的理论或我的安装有问题吗？

编辑添加：在教程本身中，它说用来why3 demo_logic.why证明理论，但是当我尝试得到这个结果时：

相反，如果我只是这样做why3 prove demo_logic.why，则结果只是（大约）该理论的回声：

SMT-LIB 版本 2.6的草案指定了一个(declare-datatypes)声明。在此功能的原始公告中提到，建议的语法与当时 Z3 和 CVC4 支持的语法不同。

是否有任何具有 SMT-LIB 支持的 SMT 求解器当前支持 SMT-LIB 2.6 草案中的建议语法，或者是否有补丁为求解器添加了对建议语法的支持？

我感兴趣的逻辑是 QF_ABV 加上简单 n 元组的数据类型。我不需要高级数据类型功能，例如递归数据类型或参数数据类型。

我正在尝试使用 CVC4 进行一些实验。

当我使用 CVC4 运行它时，我得到以下输出

我对这个输出的这种行为感到困惑。如果我断言 x 和 y 不应该相等，它们的值必须不同，对吗？不同断言的情况也是如此。CVC4 是否将 x 和 y 视为两个不同的“对象”并因此给出它给出的输出？

在 SMT-LIB 语言 1.2 之前的版本中，允许重载用户定义的符号。自标准 2.0 版以来，重载仅限于理论符号。

尽管如此，一些 SMT 求解器仍然允许重载用户定义的符号，这恰好对我的用例很方便：证明义务很容易通过重载自动生成，而不是没有......我想将 cvc4 添加到我的投资组合中的 SMT 求解器，但我发现它会在重载的用户符号上产生解析错误。

我知道这是符合 SMT-LIB 标准的正确方法，但我想知道以下内容：CVC4 是否有一个选项可以禁用此类检查以及解析器能够消除重载用户符号的歧义？

以下 SMT 公式通过 Z3 约束求解，而 CVC4 标记解析错误：“符号‘无’以前声明为变量”。我已经在 Windows 上同时使用 CVC4 1.4 和 CVC 1.5 进行了测试。有什么建议或想法吗？