2

我正在使用 API 中的 Z3，并且正在寻找一种方法来调试我的约束。我的代码编译并且 Z3 在我的约束上运行，但是我的约束有问题。我希望查看我给 Z3 的约束以确定什么是错误或缺失的，但我不确定如何以一种非常易读的方式执行此操作。问题是使用 SMTLIB_DUMP_ASSERTIONS 之类的工具不会在任何 let 绑定变量中提供有意义的名称。由于我多次重复使用相同的表达式，因此几乎所有内容都与生成的变量绑定。

有没有办法转储输入约束的文件，其中让绑定变量具有我指定的名称？我并不特别关心格式是什么，但 SMTLIB 1 或 2 会很好。

4

1 回答 1

1

不，您不能提供名称让 Z3 AST 打印机自动创建变量。一种可能的解决方案是编写自己的 AST 打印机。在 Z3 发行版中，我们有一个示例应用程序examples/c/test_capi.c。它包含以下功能：

void display_ast(Z3_context c, FILE * out, Z3_ast v)

它展示了如何实现一个简单的 AST 打印机。这个例子很简单，但它是一个起点。

于 2011-10-04T14:55:16.347 回答