显示从SMT-LIB2文件解析的声明
我正在使用Z3和Java API。 在我的SMT-LIB2文件中，有几个变量：
(declare-fun x0 () Int) (declare-fun x1 () Bool) ; alot more 我想得到所有这些变量，并将它们存储在Expr数组中。 从z3 SMTLIBDecls的示例中，我找到了API SMTLIBDecls ，它们从SMT-LIB1文件中解析出声明，但SMT-LIB2没有类似的API。 我怎样才能得到声明？
谢谢。
目前没有用于此目的的函数，但通过遍历表达式很容易获得声明。 之前已经要求使用C / C ++，但答案也适用于Java： Z3 4.3.1 C-API parse_smtlib2_string：从哪里获取声明？
另外，这些post也可能是有意义的： 在C / C ++中遍历Z3_ast树 ， 如何找出z3_ast是否对应于一个子句？