antoinemine / apron

Apron Numerical Abstract Domain Library
Other
114 stars 33 forks source link

Fix the variable permutation performed at the end of level 1 fold. #90

Closed antoinemine closed 1 year ago

antoinemine commented 1 year ago

Level 0 fold operation requires the indice of folded variables to be sorted. However, level 1 fold takes as argument a list of variable names, which does not necessarily give a sorted list of variable indices. Hence, level 1 fold applis the level 0 fold on the sorted variable indices, and then corrects the result by permuting variable indices until the fist variable in the argument list (i.e., the destination) contains the result of the fold (instead of the variable with the lowest index).

Previously, the code performed a rotation to the right, which was not correct and provided wrong results in some cases. A rotation to the left is actually needed, instead. This PR fixes the rotation.

rmonat commented 1 year ago

This fixes the issue I encountered, thank you @antoinemine!