问题标签 [cvc4]

我有一个可以动态生成 SMT-LIB 格式的表达式的程序，我正在尝试将这些表达式连接到 CVC4 以测试可满足性并获取模型。我想知道是否有一种方便的方法可以通过 CVC4 C++ API 解析这些字符串，或者最好将生成的 SMT-LIB 代码存储在文件中并将输入重定向到 cvc4 可执行文件。

我有一个用 Z3 用 C++ 编写的可满足性问题，我正在尝试将其转换为 SMT-LIB2，然后将其输入 CVC4 来解决。

当我Z3_solver为问题打印（使用Z3_solver_to_string()）时，我相信它是以Z3_PRINT_SMTLIB_FULL表格形式打印的，而不是Z3_PRINT_SMTLIB2_COMPLIANT（CVC4 抛出Parse Error: unexpected token '('）。

我在 API 中看到有一个方法调用Z3_set_ast_print_mode()来以正确的 SMT-LIB 形式获取 AST，但是有没有办法为该Z3_solver类型执行此操作？求解器是否适合在这里打印，或者我应该打印其中一个节点并将其发送到 CVC4？

我正在尝试option使用 Java API 在 CVC4 中定义参数化数据类型。

我的问题是我不知道如何调用None构造函数。我尝试了以下代码：

这会导致以下错误：

当我删除类型归属行时，它不会推断出正确的类型，所以我认为类型归属是必要的。这是我在没有类型说明的情况下得到的错误：

如何使用 Java API 正确创建此数据类型和公式？

我在以下 SMT 输入上执行了 z3 和 CVC4。两者都返回未知。

• 他们无法决定可满足性是否有任何根本原因？

• 哪些选项或其他求解器适合解决此类问题？

我想从 CVC4 生成的 sygus 文件中改变约束的内部表示。

例如 (constraint (and (<= x (fxy)) (<= y (fxy)))) 是来自 small.sl 的约束，我将其提供给 cvc4 qas 输入以合成程序。

我知道 cvc4 使用类 Expr 创建一个内部表示；

cvc4 定义了一个命令 cmd ，它似乎指向 sygus 文件中的每个语句，如下所示：

我担心这两个约束。我想通过围绕运算符交换约束来修改约束，如下所示：

为此，我正在搜索指向在解析后由约束形成的表达式树的对象。

这就是他们声明解析器构建器的方式。

这里定义了指向解析器的指针。

这是指向输入文件中已解析语句的命令。

这是内部表示的类声明。

有谁知道如何获取表达式树的对象？

提前致谢

所以我花了一些时间学习后才开始学习cvc4boolector。有了它，可以仅使用boolector_print_model打印模型。不幸的是，文档页面cvc4目前已关闭，我无法理解如何cvc4在 Java 中做同样的事情。

任何人都可以帮忙吗？

例如，你可以帮我看看这个例子的模型。

编辑：为了清楚起见，对于整个模型，我的意思是模型BV中存在的每个或一般变量的有效值。

一个示例模型可以是：

非常感谢

我正在尝试使用 SMTLIB 格式来表达 Z3 中的集合成员资格：

函数emptyset和member似乎在 CVC4 中按预期解析，但在 Z3 中没有。

通过检查 API（例如，这里：https ://z3prover.github.io/api/html/group__capi.html ），Z3确实以编程方式支持空集和成员资格，但是如何用 SMTLIB 语法表达这些？

我被困在如何在 SMTLIB2 中创建一个声明类似

此属性将检查一个函数，该函数递归地将所有小于 100 的数字加 1：

我通读了关于量词和模式的 Z3 教程，但这似乎并没有让我在任何地方获得太多帮助。

我可以为如下查询获取多个模型吗？

而不仅仅是

我想得到 0, 1, -1, 2, ...

我正在尝试从源代码（http://cvc4.cs.stanford.edu/wiki/Building_CVC4_from_source#Installing_libantlr3c:_ANTLR_parser_generator_C_support_library）构建 CVC4。为此，我需要安装 libantrl3c，但遇到以下错误：

完整的日志/堆栈跟踪，可以在这里找到：https ://pastebin.com/rkVzSaAB