How to get the declaration from a Z3 smtlib2 formu

Question

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.

Answer 1

Like Nikolaj said in Z3 4.3.1 C-API parse_smtlib2_string: Where to get declarations from?, you'll have to traverse the expressions (assertions) to collect the declarations. The link to the tptp example is broken, but the file comes with Z3 as examples/tptp/tptp5.cpp (see the collect_decls function).

See also: Display declarations parsed from an SMT-LIB2 file