"SAT/SMT by Example": hacking/tinkering plan
This should be added to my book, but I forgot.
Where can you start hacking?
- CBMC examples. CBMC is easy to install. Examples are in pure C, so anybody can hack them without additional training. CBMC exists for Windows.
- KLEE examples. Also in pure C, but KLEE is trickier to install, via docker... No Windows supports, AFAIR.
- Z3Py examples. These are for Z3 Python API. Only Python knowledge is required. Grep for "from z3 import *" in *.py files, these are for Z3Py.
- SMT-LIB 2.x examples. Lispy language, way less handy than Python, C++, C#, etc... But this language is distilled,
and not contaminated by Python's (or C++'s) specific features, operator overloading, etc, so there you can see a clear border between SMT API and API's implementation in specific PL.
- SAT examples. Low-level. Like assembly language -- hard to understand, hard to use, but the most efficient way of using SAT solvers.
So grab the source code for my book and start tinkering...
List of my other blog posts.