3 ms·
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.
by sevensor 1y 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.
- doctorpangloss 1y agoThis post is the programming joke about Python, "import solution; solution()".
- sevensor 1y agoBarely a joke, this is literally what using the Python Z3 bindings feels like.
- ndr 1y agoI did write a shockingly similar solution few months ago: https://gist.github.com/enigma/98ea0392471fa70211251daa16ce8b2c https://gist.github.com/enigma/98ea0392471fa70211251daa16ce8...
- Recursing 1y agoNote that CVC5 has basically the same Python API ( https://cvc5.github.io/docs/cvc5-1.1.2/api/python/python.html https://cvc5.github.io/docs/cvc5-1.1.2/api/python/python.htm... ) and is often much faster
- sevensor 1y agoNice, I’ll try it out!