显示从SMT-LIB2文件解析的声明 [英] Display declarations parsed from an SMT-LIB2 file

问题描述

我正在使用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： Z3 4.3.1 C-API parse_smtlib2_string：从哪里获取声明？

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?

另外，这些帖子也可能是有意义的：
在C /中遍历Z3_ast树C ++ ，如何确定z3_ast是否与条款相对应？

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文件解析的声明的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！