feat: add a parameter to adjust SMT encoding of literals

emina / rosette

The Rosette solver-aided host language, sample solver-aided DSLs, and demos

Other

638 stars 74 forks source link

Closed sorawee closed 8 months ago

sorawee commented 8 months ago

Fixes #268

The performance doesn't seem to be negatively affected (the GHA running time is about the same).

Submitting this PR for discussion, but it should not be merged yet because there is no documentation of the new module.

sorawee commented 8 months ago

I discussed this with Emina, and we agree that this approach is too hacky, so I will abandon it.