Autotune: Conditionally activate congruence integer domain #911
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
…on the whole program. Enables congruence domain on whole program when there is enough complexity-'fuel' left
Enabling this option has two effects: (a) The congruence domain is enabled for functions that use modulo, and (b) the congruence domain is globally enabled for programs where there is still some autotuner "fuel" for the program.
michael-schwarz
approved these changes
Nov 17, 2022
By removing the setting, the autotuner will not enable congruences with this configuration.
michael-schwarz
added a commit
to leunam99/analyzer
that referenced
this pull request
Nov 18, 2022
Julian is working on fine-tuning the parameters now. |
|
I started another run with the new optimization. |
|
As this is deactivated by default and the issue we uncovered is not here, I am merging this now. |
Merged
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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.
This PR extends the autotuner to be able to enable the congruence domain for a whole program. Previously, the autotuner only activated the congruence domain for functions that contain the
%-operator (remainder) or were called by such functions.However, the congruence domain may be useful even in some cases when the program does not contain the remainder operator. Therefore the congruence domain is activated on a program when there is still some "autotuner fuel" left for the configuration. This should enable the domain on small programs.
The formulas for computing the
costandvalueoption were chosen as something that seemed sensible, but were not fine-tuned.This PR also adds the
congruenceoption to the autotuner in thesvcomp23.jsonconfiguration. That means that the autotuner may activate thecongruencedomain, on a function level or for a whole program.