Parsing SMTLIB using the Z3 C API without losing `push`, `pop` and `check-sat` commands

Question

I'm using the Z3_parse_smtlib2_string function from the Z3 C API (via Haskell's Z3 lib) to parse an SMTLIB file and apply some tactics to simplify its content, however I notice that any push, pop and check-sat commands appear to be swallowed by this function and do not appear in the resulting AST.

Is there anyway that I can parse this without losing these commands (and then apply the required tactics, once again without losing them)?

Answer 1

I don't think it's possible to do this with Z3_parse_smtlib2_string. As you can see in the documentation "It returns a formula comprising of the conjunction of assertions in the scope (up to push/pop) at the end of the string." See: https://z3prover.github.io/api/html/group__capi.html#ga7905ebec9289b9fe5debcad965f6267e

Note that the reason for this is not just mere "not-implemented" or "buggy." Look at the return type of the function you're using. It returns a Z3_ast_vector, and Z3_ast only captures "expressions" in the SMTLib language. But push/pop etc. are not considered expressions by Z3, but rather commands; i.e., they are internally represented differently. (Whether this was a conscious choice or historical is something I'm not sure about.)

I don't think there's a function to do what you're asking; i.e., can return both expressions and commands. You can ask at https://github.com/Z3Prover/z3/discussions to see if the developers can provide an alternative API, or if they already have something exposed to the users that achieves this.