问题描述
我正在使用Z3和Java API。在我的SMT-LIB2文件中，有几个变量：
I'm using Z3 with Java API. In my SMT-LIB2 file, there are several variables:
(declare-fun x0 () Int)
(declare-fun x1 () Bool)
; alot more
我想得到所有这些变量，并将它们存储在<$ c $的数组中C> Expr的。从z3随附的示例中，我发现API SMTLIBDecls 获取从SMT-LIB1文件解析的声明，但SMT-LIB2没有类似的API。我怎样才能得到声明？
I want to get all these variables, and store them in an array of Expr. From the example distributed with z3, I find the API SMTLIBDecls that get declarations parsed from an SMT-LIB1 file, but there is no similar API for SMT-LIB2. How can I get the declarations?
谢谢。
推荐答案
那里目前没有用于此目的的函数，但通过遍历表达式很容易获得声明。之前已经要求使用C / C ++，但答案也适用于Java：
There is currently no function for this purpose, but it is easy to get the declarations by traversing the expressions. This has previously been asked for C/C++, but the answer applies to Java as well: Z3 4.3.1 C-API parse_smtlib2_string: Where to get declarations from?
另外，这些帖子也可能是有意义的：
，
Additionally, these posts may be of interest as well:Traversing Z3_ast tree in C/C++, How to find out if a z3_ast corresponds to a clause?
这篇关于显示从SMT-LIB2文件解析的声明的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持！