4 ms·

Or you can use Python AST + Z3 :) Here is a toy implementation: https://github.com/true-grue/python-dsls/blob/main/datalog/datalog_test.py https://github.com/t

• philzook 1y ago
  Love it! I was trying to use python as a dsl frontend to Z3 in a different way https://github.com/philzook58/knuckledragger/blob/ecac7a568a85fac5c3eaf4a17f24049244eb4ecc/kdrag/reflect.py#L617 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
  • richard_shelton 1y ago
    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 :)