2

I'm trying to debug a program that is using the Z3 API, and I'm wondering if there's a way, either from within the API or by giving Z3 a command, to print the current logical context, hopefully as if it had been read in an SMT-LIB file.

This question from 7 years ago seemed to indicate that there would be a way to do this, but I couldn't find it in the API docs.

Part of my motivation is that I'm trying to debug whether my program is slow because it's creating an SMT problem that's hard to solve, or whether the slowdown is elsewhere. Being able to view the current context as an SMT-LIB file, and run it in Z3 on the command line, would make this easier.

jmite
  • 8,171
  • 6
  • 40
  • 81

1 Answers1

1

It's not quite clear what you mean by "logical context." If you mean all the assertions the user has given to the solver, then the command:

(get-assertions)

will return it as an S-expression like list; see Section 4.2.4 of http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf

But this doesn't sound useful for your purposes; after all it is going to return precisely everything you yourself have asserted.

If you're looking for a dump of all the learned-lemmas, internal assertions the solver created etc; I'm afraid there's no way to do that from SMTLib. You probably can't even do that using the programmatic API either. (Though this needs to be checked.) That would only be possible by actually modifying the source code of z3 itself (which is open-source), and putting in relevant debug traces. But that would require a lot of study of the internals of z3 and would unlikely to help unless you're intimately knowledgeable about z3 code base itself.

I find that running z3 -v:10 can sometimes provide diagnostic info; if you see it repeatedly printing something, it's a good indication that something has gone wrong in that area. But again, what it prints and what it exactly means is guess work unless you study the source code itself.

alias
  • 28,120
  • 2
  • 23
  • 40
  • For logical context, I'm thinking the assertions, but also any function or constant declarations. Basically, an SMT-LIB file that's equivalent to the series of API calls I've made. – jmite Jul 18 '19 at 04:15
  • The API exposes more than SMT-Lib; so if you've done more than what SMT-Lib allows, then you're out of luck. But otherwise, `(get-assertions)` is your friend. The corresponding C-api function is here: https://z3prover.github.io/api/html/group__capi.html#ga3b3d6d8c5bafd5be707cda2d144073db – alias Jul 18 '19 at 06:06