Z3命名允许绑定在API

Question

我使用Z3从API，我正在寻找一种方法来调试我的约束。我的代码编译和Z3运行在我的约束上，但是我的约束有些问题。我希望看看我给Z3确定什么是错误或缺失的限制，但我不知道如何以一种非常可读的方式做到这一点。问题是使用像SMTLIB_DUMP_ASSERTIONS这样的工具不会在任何绑定变量中提供有意义的名称。由于我有很多重复使用相同的表达式，几乎所有的东西都被一个生成的变量限制了。

是否有任何方法来转储输入约束文件，其中let-bound变量具有我已分配的名称？我不特别在乎格式是什么，但SMTLIB 1或2会很好。

Answer 1

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

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

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