Comment by richard_shelton
Comment by richard_shelton 3 days ago
Or you can use Python AST + Z3 :) Here is a toy implementation:
https://github.com/true-grue/python-dsls/blob/main/datalog/d...
Comment by richard_shelton 3 days ago
Or you can use Python AST + Z3 :) Here is a toy implementation:
https://github.com/true-grue/python-dsls/blob/main/datalog/d...
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 :)
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