I would like to do incremental solving with Z3 with the C++ API.
There are already some old questions, 2012, about this:
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?
I would like to know if there is a solution with the new Z3 versions, 4.4.2.
Basically what I want to do it is something like this:
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();
But I don't know how to get the declarations. I tried to use Z3_get_smtlib_num_decls, but it is only working with smtlib1, not with smtlib2.
Is there a way to retrieve the declarations? Will the function Z3_get_smtlib2_num_decls be implemented in the future?
Thank you for your time.
