问题标签 [cvc4]

使用示例 find.c 文件，我可以使用默认的 alt-ergo 证明它没有问题。但是当更改为 cvc4 时，会收到警告消息和语法错误。这里的代码：

运行此命令并获取以下消息： frama-c -wp -wp-prover CVC4 -wp-out out find.c

如何摆脱警告和语法错误？我的 CVC4 是 1.6 版。

我正在尝试从To Mock a Mockingbird建模一个逻辑难题。我正在努力将其翻译成 SMT-LIB。谜题是这样的：

有一个花园，所有的花要么是红色的，要么是黄色的，要么是蓝色的，所有的颜色都被代表了。对于您采摘的任何三朵花，至少一朵是红色的，一朵是黄色的。第三朵花永远是蓝色的吗？

我尝试将花园建模为Array Int Flower，但这不起作用，我相信因为数组的域固定在所有整数的范围内。Z3 很有帮助地告诉我这是无法满足的，CVC4 只是立即返回未知。

这个谜题的唯一解决方案是一个花园，每种颜色只有一朵花，但我如何让解题者告诉我这个？

这是我失败的尝试：

这似乎是根据SMTLIB 标准define-funs-rec可以做什么的严格超集。如果是这样，是否有理由不总是使用，也许除了语法简单之外？define-fundefine-funs-rec

我想知道同一个列表公理的这两种编码有什么区别：

和

对于这个基准：

不知何故，z3 能够推断出第二个版本，但不能推断出第一个版本（它似乎只是永远循环）。

编辑：与 cvc4 相同，第一个版本返回未知。

我正在修改 CVC4 对集合和关系的支持，并希望能够使用product运算符来构建两个集合的笛卡尔积。但是，此运算符仅适用于关系。

这是馈送到 CVC4 的示例输入：

这会导致以下错误消息：

然后我发现 CVC4 期望product运算符适用于元组集。以下处理成功：

CVC4 可以在这里将集合视为具有该集合元素的 1 元组的集合。

• 是否有任何基本问题阻止它发生这种行为？

我将符号执行引擎的符号输出以 SMT-LIB 2 格式传递给 Z3。我需要它来截断整数，就像它们在 C 中一样。所以那(assert (= 1 (/ 3 2)))将是SAT.

这些公式也可能有浮点数，因此并非所有除法都应截断。只是整数的划分。

如何做到这一点？

使用 CVC4 的集合论（版本 1.8-prerelease [git master a90b9e2b]）我定义了一组具有固定基数的整数

CVC4 然后给了我一个正确的模型

有没有办法求集合 A 中的整数之和？

下面的 smt2 代码给出了与类型相关的错误。

错误：

为什么它不知道使用返回类型，有没有办法做到这一点？

一种方法是手动将其设置为(nil (as nil (List Ty)) )解决错误但我不想在程序中的每个 nil 处指定返回类型。还有其他方法吗？或者我需要提到的任何选项 enable ？

我正在尝试使用CVC4对函数执行语法引导合成。首先，我正在关注CVC4 Getting Started，我的example.smt2文件如下所示：

当我cvc4 example.smt2在目录中的命令行运行时，根据上面链接的教程应该没有问题。但是，我收到此错误：

请注意，此错误与文件不存在时不同。例如，当我运行时cvc4 exampl.doesnotexist，会出现以下错误：

这是不同的。我到处查找，但找不到答案。有任何想法吗？

我正在编写一个需要将一些转换Int为BitVec反之亦然的问题的 BV 编码。

在mathsat/optimathsat一个可以使用：

在z3一个可以使用：

在CVC4一个可以使用：

问：

• 有签名z3的功能吗？（看起来没有。）bv2intBitVec
• CVC4有什么功能bv2int吗？（我没有任何线索。）
• 是否有记录这些转换功能的地方？（关于逻辑/理论的 SMT-LIB 网页似乎没有任何关于它们的信息。）

注意：我受限于基于文本的 SMT-LIB 接口（没有 API 解决方案）。