6 ms·
Looking at some of your SMT-based projects, I'd love to compare your SMT solver notes with my mine from working on https://github.com/pschanely/CrossHair https:
by pschanely 6y ago
Looking at some of your SMT-based projects, I'd love to compare your SMT solver notes with my mine from working on https://github.com/pschanely/CrossHair https://github.com/pschanely/CrossHair
Sadly, there aren't a lot of resources on how to use SMT solvers well.
- fovc 6y agoIs there a place to find your notes?
- pschanely 6y agoSadly, mine largely aren't committed to words yet. I do have a small thing on implementing regular expressions: https://medium.com/@pschanely/modeling-python-regular-expressions-with-z3-fe391b7ee24 https://medium.com/@pschanely/modeling-python-regular-expres... But there is so much to talk about: gotchas with quantifiers, mixing logics, multiplication, float conversions. I'll try to write up some more of my experiences if that's valuable for folks!