Tutorial needs TLC

[NikolajBjorner]

Hi Bjorner:

We used your tools: Z3 for a final assignment for the graduate-level course: advanced programming language this semester.

First of all, we want to thank you very much for publishing the paper and making the tool available for us to use on the homework. This is an excellent and useful tool that we can use in our homework. It is very reliable that we can use some methods embedded in Z3 to do some modifications to implement our tasks. Thank you very much for your contribution to Z3!

However, while completing the homework on your tool, we find one thing that is not convenient for us, so we want to suggest you. This is the hard-reading tutorial for Z3. People who first use Z3 tools will definitely need to learn the tutorial to get started. However, the current tutorial is too hard to read; it is challenging for us to search/locate what we want to use. So, we think people will suffer from learning and understanding how to use the Z3 tool or take too much time to figure it out. So, we suggest that maybe you can use a better interface, like the tutorial for PyTorch(https://pytorch.org/tutorials/), to let people feel more comfortable getting started quickly.

Thank you again~

[NikolajBjorner]

To offer some additional context.
The message describes using https://theory.stanford.edu/~nikolaj/programmingz3.html as a starting point for graduate students who are being introduced to the area. It wasn't the primal intent of the document to be a basic introduction, but a place to record some of the more advanced tricks of the trade. In this way it doesn't match the target audience in a course.
There is material in jupyter notebooks that could be used as starting points:
https://github.com/Z3Prover/z3/tree/master/examples/python/tutorial/jupyter
It was used for several years as the initial starting point for student scenarios well before programmingz3 was there. Programmingz3 was written as a contributed paper for SETSS spring school after Jonathan Bowen had the boldness to ask for a "small" contribution for the proceedings to follow a spring graduate school.

Tutorial material that uses up-to-date presentation layers is clearly welcome, but I don't have any bandwidth to write one.
What I can suggest at this point is that anybody interested to develop teaching material related to Z3 that is directly accessible from Z3 distributions or github entries to contact me and use this as a starting point to see if there is a way it can be supported in a reasonable way.

[gmCAD]

These are links that I found helpful when trying to figure things out.

https://sat-smt.codes/SAT_SMT_by_example.pdf - Dennis uses a mix of Z3 and other SAT/SMT solvers, but the concepts are solid.
https://stackoverflow.com/questions/26562177/river-crossing-puzzle-in-z3
https://stackoverflow.com/questions/53711168/modelling-a-logic-puzzle
https://www.weinholt.se/articles/design-low-tagging-z3py/
https://github.com/VidhyaTV/AutomatedProtocolSynthesis

[philzook58]

I recently gave a beginner level tutorial. Video and jupyter notebooks which load on click to google colab are available here https://github.com/philzook58/z3_tutorial

It is also easy to make google colab links that go directly to the Z3 repo tutorials above, as it appears the Azure notebook hosting link does not work
https://colab.research.google.com/github/Z3Prover/z3/blob/master/examples/python/tutorial/jupyter/guide.ipynb

[NikolajBjorner]

Some context:

Azure notebook hosting was discontinued. It was a welcome feature as long as it lasted. Our own home-made python hosting service was target of "security researchers" finding ways to hack it and therefore a complete distraction from developing Z3.
I need to deprecate the broken links, yes.

Colab offers corresponding environment so this seems to be a current great way to have shared and reduced installation friction experiences. There is a closed GitHub beta for jupyter, but I have yet to gain access to and try it.