Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
The manual inspection of not enabling vs enabling
loopUnrolling
showed that the stats for the current unrolling are (broadly) the following:Looking into the semantics of the tasks where unrolling helped us verify (Unknown -> True), however, revealed that
Regardless of the semantics of the program, I also tried to find the minimum amount of unrollings necessary for solving the task. This showed that:
For all loops with a nondet bound that I found by inspection, the sufficient (minimum) times of unrollings needed for solving the task is at max 2.
As revealed by some intermediate runs, unrolling fixed loops with the bound up to 100 makes us timeout in many of the instances (including on some of the regression tests; see #1516 (comment)). For the maximum bound of loop unrolling, which was 25 previously, the actual semantics were that the loop has to be unrolled by a minimum of 19 times (the syntax can determine that) for us to solve the task. Thus, I have changed the heuristic of
if totalLoops < 17 && AutoTune0.isActivated "forceLoopUnrollForFewLoops" then 10 else 0 in
to| Some i when i <= 20 -> i
, i.e., if a fixed loop iteration of 20 or less is found, we will unroll the loop the found amount of times.(The next old unroll maximum would be 16, where the semantics is nondet, and 1 unroll is sufficient, and further from that, the new max is 12, which cases semantics I have not looked into too thoroughly yet.)
Otherwise, if the found loop iterations are 20+, we will default to the median of the previous unrolling (4), which, in many cases, is the sufficient amount of unrolling needed to solve a task - so, we would default to unrolling 4 times instead of the complicated heuristic of calculating some (weird) bound based on the number of statements in the loop:
max unroll_min (targetInstructions / loopStats.instructions)
. According to a run with these settings, we do not lose too many tasks but gain a bit in performance (e.g. instead of the "random" unrolling of 12 times in many cases, where 2 times would be sufficient, we now only unroll 4 times).We made a run with these new defaults, and I investigated some of the tasks (edge cases) where we could not solve the task because the iterations found by the new heuristics were too small. Some PRs will follow this PR to again handle these lost cases in addition to some new tasks that we can further solve due to some (new) improvements to the unrolling.