显示从 SMT-LIB2 文件解析的声明

【问题标题】：Display declarations parsed from an SMT-LIB2 file显示从 SMT-LIB2 文件解析的声明
【发布时间】：2014-05-12 23:37:14
【问题描述】：

我正在使用带有 Java API 的 Z3。在我的 SMT-LIB2 文件中，有几个变量：

(declare-fun x0 () Int)
(declare-fun x1 () Bool)
; alot more

我想获取所有这些变量，并将它们存储在Expr 的数组中。从与 z3 一起分发的示例中，我发现 API SMTLIBDecls 可以从 SMT-LIB1 文件中解析声明，但 SMT-LIB2 没有类似的 API。如何获得声明？

谢谢。

【问题讨论】：

标签： java z3

【解决方案1】：

目前没有用于此目的的函数，但是通过遍历表达式很容易得到声明。以前有人问过 C/C++，但答案也适用于 Java：Z3 4.3.1 C-API parse_smtlib2_string: Where to get declarations from?

【讨论】：

谢谢。在“从何处获取声明”的答案中，有一个示例链接：z3.codeplex.com/SourceControl/latest#examples/tptp/tptp5.cpp，但该链接已失效。你能帮我检查一下吗？
啊！看起来这些链接不包含有关文件所在分支的信息。在这种情况下，examples/tptp/tptp5.cpp 位于不稳定分支中，但在主分支中不可用（目前）。