draperlaboratory / VIBES

Verified, Incremental, Binary Editing with Synthesis
MIT License
51 stars 1 forks source link

Enable user defined extra-constraints to inject into minizinc #166

Closed philzook58 closed 2 years ago

philzook58 commented 2 years ago

This puts an extra field into the patch config "extra-constraints"which will inject verbatim the string given to the tail of the minizinc model on a per patch basis. This feature might supersede the excluded registers features and preassignment

The huge caveat is that currently minizinc receives non user friendly names. This can be somewhat ameliorated by using forall sometimes. You also need to have knowledge of how the model works to use this feature. Both require expert use. Only for the brave and true atm. We could work on maintaining good names and a library of helper predicates if this is a desirable feature.

I have removed most vestiges of s-expressions from the minizinc serialization. It was convenient but also horrible to debug. I added a new parameter to mzn_params hvars_temps which maps from high level variables names to temporaries that make up this high level variable name. With this, there are user friendly names available for building extra-constraints

As a side note, i had to move some data types to Data.ml to resolve a dependency ordering issue and removed exception throwing from Linear_ssa.orig_name instead using an option