What changed in Z3 and how one can use it is often very hard to find out

[zimmski]

I think the Z3 project could benefit from better documentation. Making changes discoverable to the user.

We try to stay up to date with Z3 versions to benefit from not just all the bug fixes and performance improvements but also to use new features if we see that we can. So i am literally looking through every commit, issue and discussion with every update that might went into a release.

There are a few things missing for me that would help, a lot:

a. Doing better commit messages that describe what changed, why a change is happening and why I as a user should care.

Every release has a list of commits that went in e.g. https://github.com/Z3Prover/z3/releases/tag/z3-4.8.17 However, most of them are usually not well described. The "what" a commit does is not often that clear, e.g. 98e1c86 is easy but 9cc5f69 starts to get trickier, both use "na" as a commit subject. Others have better messages such as d1f1e4c but it requires one to either dig deep or be familiar with a lot of topics. I am reading lots of papers, know a bit of the Z3 code as well as other SAT and SMT solvers, but to be honest, i still cannot make sense out of all changes that are happening.

b. Adding tests for changes.

Even if one does not understand what a change does, an automated test gives you a great documentation. https://github.com/Z3Prover/z3test exists and i learned a lot from that repository (might be a also worth nothing this repository in the README) but it is not updated with every change, it is hardly updated at all. To be honest i do not even understand when or why it is updated, since it suffers the commit message problem as well.

c. Adding documentation to changes

There are release notes with every release https://github.com/Z3Prover/z3/blob/master/RELEASE_NOTES but they make it hard to follow as a user what changed and how one can use it. E.g. for 4.8.17 i was exited to read initial support for nested algebraic datatypes with sequences but since there is no reference or example i again have to go back to reading commits. I think this is the only commit related to that change 81d97a8, but i cannot be sure. Reading through the code i got less excited and i thought "this is not the way". Adding a little documentation that Z3 now supports X and just one example as a documentation would have helped here.

I hope these explanations make sense. Z3 is a great project. Even though i lost many hairs using it, i still think it is easy to use and integrate. Z3 also has a ton of features and more are added with every release. However, i think it would be really worth it for all users and new users to add some more documentation during the implementation and fixing of bugs.

[chadbrewbaker]

Easiest is to run /usr/bin/time -v on the integration test suite. That should tease out performance improvements/regressions.

As long as an example of each new feature is in the integration test suite it should be easy to diff between commits.

[NikolajBjorner]

regarding sequences and ADT. This was a feature request from a user group.
The agreement was that I added the feature, and the requestor would evaluate it. Issue #6005 tracks evaluation.
Similarly map/fold on sequences is a feature request from Mark Marron. While the feature is available
in Master it is being evaluated. Once found to be in a reasonable state (or not, in which the feature may be removed), it makes better sense to develop adequate documentation. There are many places where more adequate documentation can be developed and the release notes can be made more usable.

[zimmski]

Thanks for the explanation. I agree that it makes sense to work on evaluating a feature like that. My main concern though is not about that particular feature but about how Z3 users are informed about what has changed and how one could use it. I am sometimes jealously looking at the CVC change log and documentation which is pretty great. Such a documentation for Z3 would be extremely cool, especially for Z3 newbies. However, that would be a huge undertaking. For starters it would make following changes of Z3 much easier if commit messages and the changelog could have a little more information.

You asked on Twitter https://twitter.com/BjornerNikolaj/status/1543791329821351936 about how to improve the original rise4fun. I did not have an answer then but now that i thought some more about it: it would be great to make rise4fun the documentation base of Z3. The base would be to document every functionality with examples (that are run-able online) and then go deeper into scenarios. That would make it easier to extend the documentation with new features/changes.

[zimmski]

Just saw the change of the release notes to markdown with more information: https://github.com/Z3Prover/z3/blob/master/RELEASE_NOTES.md coming to 4.9.0. Awesome!

The new release notes also brought me to https://microsoft.github.io/rise4fun which is super cool. Will add it to my reading list :-) One thing that would be good here is to make the connection between that website and Z3 stronger, e.g. make changes there part of the Z3 changelog and link them. I am unsure how other Z3 users see this, but i am always glad to see a new mini-tutorial of a functionality that i did not know before so we can improve our engine.

[zimmski]

About this discussion and #6092, just wanted to say THANKS @NikolajBjorner. I was a little out of the loop with updating our solver version (we are working mostly on product and environments right now) but now that i had some time to geek into what changed with Z3: i am simply blown away by how cooler the changelog got. Hope to do an update of our solver soon and give you some feedback on how it went!