Comment by sevensor
3 days ago
SMT is so much fun. The Z3 Python api lets you write your problem very directly and then gives you fast answers, even for quite large problems.
3 days ago
SMT is so much fun. The Z3 Python api lets you write your problem very directly and then gives you fast answers, even for quite large problems.
Note that CVC5 has basically the same Python API ( https://cvc5.github.io/docs/cvc5-1.1.2/api/python/python.htm... ) and is often much faster
Nice, I’ll try it out!
I did write a shockingly similar solution few months ago:
https://gist.github.com/enigma/98ea0392471fa70211251daa16ce8...
This post is the programming joke about Python, "import solution; solution()".
Barely a joke, this is literally what using the Python Z3 bindings feels like.