Love it! I was trying to use python as a dsl frontend to Z3 in a different way https://github.com/philzook58/knuckledragger/blob/ecac7a568a... (it probably has to be done syntactically rather than by overloading in order to make `if` `and` etc work). Still not sure if it is ultimately a good idea. I think it's really neat how you're abusing `,` and `:` in these examples

In some parallel world, Python is the perfect tool for language-oriented programming. Any decorated function is compiled by its own DSL compiler into the internal representation of the corresponding solver, and functions communicate with each other using rich Python data structures :)