Z3 4.3.1 C-API parse_smtlib2_string: Where to get

问题:

unfortunately I do not have enough reputation to comment answers of other questions. So I have to start a new question.

Essentially I have the same problem as described here. I want to use Z3 for incremental solving. For getting the constraints into Z3, I use smtlib2 strings. Everything works fine for the first set of constraints, where I can put the declarations of variables etc. directly into the smtlib2 string. When adding additional constraints incrementally, Z3_parse_smtlib2_string needs to receive the number of previous declarations (unsigned num_decls), the declarations (Z3_func_decl const decls[] ), and the names thereof (Z3_symbol const decl_names[]). For smtlib strings, the Parser interface offers functions to retrieve this information, e.g., "Z3_get_smtlib_num_decls" and "Z3_get_smtlib_decl". However, they do not work for smtlib2 strings.

There was a workaround using models. For this workaround, Z3 must return models including each declared variable ("full models"), which seems not to be the case by default. A solution for this problem has been described here (for Z3 4.0). Unfortunately, this does not work any more for Z3 4.3.

Has somebody an idea how I can get full models from Z3 that is not so much depending on the used version? Or even better: Are there more direct ways to retrieve the declarations in the meantime? About one year ago, Leonardo de Moura mentioned that there will be "Parser" objects in the future that will have support for retrieving decls, formulas, etc. (see Z3 4.0: get complete model). Is there anything new here that I have not yet discovered in the documentation?

Many thanks!

Elisabeth

回答1:

You can walk the sub-expressions to collect the auxiliary sort and function declarations. The following extended example contains code that parses SMTLIB2 and it has to traverse returned expressions for collecting sort and function declarations. You can browse it here

It uses the C++ API. The function collect_decls traverses the expression and collects uninterepreted sorts and functions (this function assumes there are no user-defined algebraic data-types and does not attempt to extract those).