2
C++ APIを使ってZ3を段階的に解決したいと思います。Z3 smtlib2式から宣言を得るには？
これについていくつかの古い質問、2012年、すでにあります。私は新しいZ3バージョンと解決策があるかどうかを知りたい
Z3 4.0 Z3_parse_smtlib2_string
Z3 4.3.1 C-API parse_smtlib2_string: Where to get declarations from?
は、 、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が実装されますか？
ありがとうございます。