vehicle-lang / vehicle

A toolkit for enforcing logical specifications on neural networks
https://vehicle-lang.readthedocs.io/
Other
80 stars 7 forks source link

Let-insertion is unstable #127

Closed MatthewDaggitt closed 2 years ago

MatthewDaggitt commented 2 years ago

Just changed the Builtin type in 1565374eef162549529886204d347aec7dd1609b, and it's changing the hash of the expressions and therefore the ordering of the inserted lets in the lifting of the network applications. Consequently it switches the variable names in the final code for monotonicity.vcl generated for Marabou.

It would be good if we could stabilise it. Perhaps we could keep track of the order of insertions in the IntMap we use to store the subexpressions?

MatthewDaggitt commented 2 years ago

Possible solution: https://hackage.haskell.org/package/linkedhashmap-0.4.0.0/docs/Data-LinkedHashMap.html