Split octagon autotuner to separate octagonAnalysis and octagonVars autotuners
Opened this issue · 1 comments
Turns out when the octagon autotuner says Enabled octagon domain for: ..., it implicitly means "disabling octagon analysis for all other variables, _even if explicitly enabled by the user".
This massively shoot us in the foot for #1394 benchmarks, where explicitly enabling the apron analysis on top of the normal svcomp configuration, which intuitively should only make things more precise, only produced 1 relational invariant. Actually the autotuner more-or-less overrode that, disabling the autotuner gives us 1896 invariants!
We're really selling our novel relational analyses short by disabling them even when explicitly requested. If it's counterintuitive for us, it will definitely be counterintuitive for anyone else evaluating Goblint.
Much less confusing behavior would be to split the autotuner into two:
- octagonAnalysis, which is just in charge of enabling the octagon analysis, but not choosing a subset of the variables.
- octagonVars, which is in charge of choosing the variables, i.e. disabling octagon analysis for all other variables (because that's what it's really doing, not enabling for additional variables).
Yes, that's a good idea! I was aware that this is the behavior of the autotuner, but then I was also the one advising the thesis which cooked up the autotuners.
If this knowledge has not even propagated in the team, then, as you say, any external people trying it will be confused for sure!