What is the rationale behind Z3_parse_smtlib2_file's interface?

[delcypher]

The interface of Z3_parse_smtlib2_file() looks like this

    Z3_ast Z3_API Z3_parse_smtlib2_file(Z3_context c, Z3_string file_name,
                                        unsigned num_sorts,
                                        Z3_symbol const sort_names[],
                                        Z3_sort const sorts[],
                                        unsigned num_decls,
                                        Z3_symbol const decl_names[],
                                        Z3_func_decl const decls[]);

There are some oddities here.

• Why do the num_sorts, sort_names, sorts, etc.. arguments exist? At a quick glance I thought they were outputs (i.e. the sorts and declarations from the smtlib2 file) but in fact looking at the implementation these are inputs. They seems to be used to populate the internal Z3 context before parsing the smtlib2 file. What is the reason for this and when is it useful?

• The function returns a single Z3_ast with all assertions conjuncted. Wouldn't a Z3_ast_vector make more sense?

[NikolajBjorner]

The API predates the availability of ast_vectors. The ability to pass auxiliary sort and function declarations allows to parse expressions in a context where functions have been declared. It is almost never used, though so just adds clutter to most users who rely on the C API. For other languages using default arguments / overloading helps.

[delcypher]

@NikolajBjorner

The API predates the availability of ast_vectors. The ability to pass auxiliary sort and function declarations allows to parse expressions in a context where functions have been declared. It is almost never used, though so just adds clutter to most users who rely on the C API. For other languages using default arguments / overloading helps.

Thanks for the reply.

Perhaps it's time to introduce a new API and deprecate this one? One problem with this API is that a single (assert (and ...)) is indistinguishable from a set of assertions

(assert ...)
(assert ...)

even though they are semantically the same thing, syntactically they are not and the user of this API might want to be able to detect the difference.

Another problem is that I have to traverse the ASTs to find all the sorts and variable declarations, even though Z3 already knows about them.

[NikolajBjorner]

Possibly having a parse method on a solver object will do. You can get assertions from solvers already. There is no exposed method for returning declarations on solvers (the pretty-printer uses one such method, though). I wonder about ditching the ability to pass in declarations of functions and sorts.

[delcypher]

@NikolajBjorner I'm not actually using Z3 as a solver. I'm currently using it's API to build a proto-type solver that reuses its parser, expression language and some of its tactics.

That is likely why I'm running into issues. On the positive side this is an excellent way to proto-type because most of Z3's C API is incredibly good. The parser is the one area where the API is a bit clunky and inflexible.

[NikolajBjorner]

Yes, it could be better. I changed the parser in a different branch to return an ast_vector. Unfortunately, I had to also change quite a bit in the interpolation code path. So I would hold off porting this part.

[wintersteiger]

Total agreement from my side as well, the parser interface is not easy enough to use.

One obvious thing that comes up frequently, is how to access the consts, sorts, etc that have been read in by the parser. I think it would be a good idea to make the parser produce a goal + an optional symbol table (in whatever form). The symbol table can then also be used as an optional input, so that users can change it before reading a second file/string, or just set up what they need in advance before parsing a file or string, like the current parser does.

[delcypher]

@wintersteiger I'm not sure about using a goal to contain the ASTs. I recently experienced cases with Z3_goals where Z3 was silently changing how formulas were represented (in a previously undocumented manner) see #1058. This might not be desirable. For example a user might be trying to implement a tool to count the number of asserts in query.

Another thing that needs to be considered is that SMT-LIBv2 files can

• Be incremental, i.e. use push/pop and add additional asserts
• Issue various commands other than check-sat (e.g. setting options).

Do we want to handle these? If so we might want a Z3_parser type that represents a state machine that can be interacted with. For every command in the SMT-LIB file the state machine could return and give the user choice whether or not to actually execute the command (e.g. (check-sat)). The user would also be able to query the current symbol table, known sorts and assertion stack.

This might be overkill. For the non-incremental case we definitely want something simpler but the incremental case probably deserves some thought.

[wintersteiger]

@delcypher Yes, a goal is not the same as an ordered set of SMT commands and I don't think that's what they should be. If we need that sort of granularity, I think we should add a new layer of abstraction in between; at the moment, the SMT commands are never kept anywhere, they are only applied to the cmd_context's state and then forgotten.

As you say, that's probably overkill. Most applications that use SMT2 commands as their interface to Z3 have their own strategy for tracking and updating the state of the solver/goals (many including incrementality) and I expect they want to keep it that way. Of course, it's useful for people who want to implement their own incremental SMT solvers based on Z3, but those users/applications are fairly rare, and they will usually have to understand the relevant parts of the codebase anyways.

[NikolajBjorner]

I added Z3_solver_from_string and from_file. Furthermore, the parse functions return a vector corresponding to asserts.