Display declarations parsed from an SMT-LIB2 file

问题:

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  

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?

Thanks.

回答1:

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?