Parse SMT-LIB2 String using Declarations in Existi

Question

I have an existing Z3 4.1 context created in the .NET API, with many function declarations, sort declarations, assumptions asserted, etc.

What is the cleanest way to parse an SMT-LIB2 string using all the existing declarations in this context? Specifically, is there a way to iterate over all the declarations in a context? I did not see any methods in Context that would allow me to access the declarations.

Currently, I am doing the following:

Context z3 = new Context();

// ... declare sorts, add declarations (parsing other input files), add assertions, to z3 context

List<FuncDecl> decls = new List<FuncDecl>();
List<Symbol> names = new List<Symbol>();
string pstr; // smtlib2 string to be parsed populated elsewhere

// ... populate decls and names by iterating over my internal data structures with references to these declarations

BoolExpr prop = z3.ParseSMTLIB2String(pstr, null, null, names.ToArray(), decls.ToArray());

Is there a way to get all these declarations and symbol names from the z3 context itself? They all have already been declared in the z3 object. I would rather do it this way than iterate over my internal data structures.

I may have missed it, but I didn't see anything that would let me do this in the API. I'm imaging something similar to the array of asserted formulas available via Solver.Assertions.

Answer 1

Your solution looks correct. The decls and names could be collected the first time they occur instead of reconstructing them for each call, which would get rid of the iteration over internal data structures for every call. Note that, if you are making many calls to Z3, using the SMT parser may not be the most efficient solution; If possible, I would recommend constructing Z3 expressions directly instead of strings (in which case a table of symbols would likely be necessary as well).