INTERPOLANT_ACCEPTANCE_THRESHOLD not defined for each MultiTrackTraceAbstractionRefinementStrategy individually

[Heizmann]

Currently, all refinement strategies give up after the first sequence of interpolants was computed. Whether the sequence is perfect or not is irrelevant.

I would prefer that this threshold is defined by each MultiTrackTraceAbstractionRefinementStrategy individually.

PENGUIN and WALRUS should aim for finding loop invariants and have a high threshold (maybe infinity).
CAMEL and WOLF should aim for good overall performance in e.g., the SV-COMP and should not risk getting timeouts in additonal interpolant computations.

By the way, it would be great if someone could find out why we are so often successful with non-perfect interpolant sequences.

[schillic]

I must admit that I did not know this.
I totally agree that the strategy should have control over this threshold.

I can implement it (maybe at the weekend) if you want.

[danieldietsch]

To be more precise: there is a variable that controls after how many imperfect sequences we don't try to find new ones and just go with it. The variable is currently set to 1. And separately, if we get one perfect sequence, we also go with that.
The implementation is rather easy. But it is unclear what a good value for this variable is.
We could use the SVCOMP preruns to compare different settings, but I am unsure if there will be enough.
Regardless, I will benchmark on a subset and report back.

For benchmarking, it would be nice to have a slightly different implementation: One setting for all strategies that sets the variable. This is obviously not nice from the user's point of view, but its easier to benchmark.

[schillic]

For benchmarking, it would be nice to have a slightly different implementation: One setting for all strategies that sets the variable.

This would be the current implementation, right?
All the better, then I just do nothing - I'm really good at this 😃

[danieldietsch]

No, the current implementation makes it a variable. It should be a setting, where the default value is the current one.

[Heizmann]

No, please not another setting! The strategy should define the threshold.
You can then compare different strategies.
By the way, the different strategy should be the only difference between PENGUIN and CAMEL and the only difference between WOLF and WALRUS.

[danieldietsch]

I will remove the setting after benchmarking.

[danieldietsch]

Alternative: I duplicate the stategies.

[Heizmann]

I would prefer the duplication of the strategies.
(Reason: the benchmarking will never end and I would like to have the setting that I need next week)

[danieldietsch]

Ok. Then I would say for, e.g., Camel there will be

• Camel (threshold=default)
• Camel1 (threshold=1),
• Camel2 (threshold=2)

All other strategies analogously up to the maximal setting that makes sense.

[Heizmann]

Please do whatever you think is appropriate for your evaluation.

[schillic]

By the way, the different strategy should be the only difference between PENGUIN and CAMEL and the only difference between WOLF and WALRUS.

@Heizmann:

1. Currently the difference is
   SMTINTERPOL_TREE_INTERPOLANTS -- Z3_FPBP -- CVC4_FPBP (🐧)*
   vs.
   SMTINTERPOL_TREE_INTERPOLANTS -- Z3_FP (🐫)
   and
   MATHSAT_FPBP/CVC4_FPBP -- Z3_FP (🐺)
   vs.
   MATHSAT_FPBP/CVC4_FPBP -- Z3_FPBP (WALRUS)**.
   Should I really remove these differences?

* 🐧 also has a commented line to use MATHSAT_FPBP initially.
** In the future we should use animals with an emoticon on Github.

2. Currently every 🐫 is a 🐧.
   I would either drop this inheritance if you want to keep the above differences - because nothing is shared between the classes at the moment - or also use inheritance for the other two.
   In the second case: Should WALRUS inherit from 🐺 or the other way around?

[schillic]

I implemented the version with inheritance.
Currently the old behavior wrt. the solvers is retained (see my previous comment).
Every 🐺 is a WALRUS (which is analogous to 🐫 and 🐧 because 🐫 is the efficient version of 🐧).

@Heizmann: Please check if this is what you wanted.

[danieldietsch]

@schillic: I forgot to push a commit from Friday (31d7526) and screwed up while combining with your commits.
After realising this, I basically reverted your inheritance-based solution, because such deep inheritance with strategies makes it tough to understand what a strategy is actually doing.

I still need to duplicate the strategies for benchmarking; I will get to it next week.

[schillic]

@danieldietsch: Alright... basically my change was super simple, so I let you handle it.

[Heizmann]

What Christian implemented exactly the what I wanted to have.
Differences in the solver order should be removed by now (take the order of 🐧 and WALRUS) but we might want to have them back again in the future if necessary.

@danieldietsch I am fine with any other implementation but it should have the same effect and it should be flexible enough for changes that we want to make in the future. (this includes e.g., different solver orders or different solver settings like timeouts).