如何从 Z3 smtlib2 公式中获取声明？答案

【问题标题】：How to get the declaration from a Z3 smtlib2 formula?如何从 Z3 smtlib2 公式中获取声明？
【发布时间】：2016-10-05 20:20:29
【问题描述】：

我想通过 C++ API 使用 Z3 进行增量求解。

已经有一些老问题了，2012，关于这个：

Z3 4.0 Z3_parse_smtlib2_string

Z3 4.0: get complete model

Z3 4.3.1 C-API parse_smtlib2_string: Where to get declarations from?

我想知道新的 Z3 版本 4.4.2 是否有解决方案。

基本上我想做的是这样的：

char *decl = "(declare-const p0 Bool)";
char *assert = "(assert(= p0 true))";

Z3_ast ast = Z3_parse_smtlib2_string(ctx, (Z3_string)decl, 0, 0, 0, 0, 0, 0);
z3::expr eq1(ctx, ast);
solver.add(eq1);

//extract declarations from the solver, ctx or ast
...

//Parse the assert with the previous declarations
Z3_ast ast = Z3_parse_smtlib2_string(ctx, (Z3_string)assert, 0, 0, 0, num_decls, symbols, decl_list);
z3::expr eq2(ctx, ast);
solver.add(eq2);
solver.check();

但我不知道如何获得声明。我尝试使用 Z3_get_smtlib_num_decls，但它仅适用于 smtlib1，不适用于 smtlib2。

有没有办法检索声明？以后会实现Z3_get_smtlib2_num_decls函数吗？

感谢您的宝贵时间。

【问题讨论】：

标签： z3

【解决方案1】：

就像 Nikolaj 在Z3 4.3.1 C-API parse_smtlib2_string: Where to get declarations from? 中所说，您必须遍历表达式（断言）来收集声明。指向 tptp 示例的链接已损坏，但文件附带 Z3 为 examples/tptp/tptp5.cpp（请参阅 collect_decls 函数）。

另见：Display declarations parsed from an SMT-LIB2 file

【讨论】：