Improved strategies

[xldenis]

I did some analysis of our sessions and concluded that we can significantly tighten up the default strategies.

Based on this I've significantly shortened the bounds on the strategies we have in Why3. My idea is that "Auto Level 0" should handle approximately 75% of the goals, and 100% of the goals should be handled by "Auto Level 3".

However, if we want this to replace the Why3 strategies they need to be added on a per-user basis as from reading the why3 source code it seems like the order is User Config > Auto Config > Extra Config.

[strategy]
code = "t split_vc exit"
desc = "Split@ the@ VC@ into@ subgoals"
name = "Split_VC"
shortcut = "s"

[strategy]
code = "start:
c Alt-Ergo,2.4.2 0.2 1000
c CVC5,1.0.2 0.5 1000
c Z3,4.11.2 0.5 1000
t split_vc start
c Alt-Ergo,2.4.2 2. 2000
c CVC5,1.0.2 2. 2000
c Z3,4.11.2 2. 2000
t introduce_premises afterintro
afterintro:
t inline_goal afterinline
g trylongertime
afterinline:
t split_all_full start
trylongertime:
c Alt-Ergo,2.4.2 10. 4000
c CVC5,1.0.2 10. 4000
c Z3,4.11.2 10. 4000
"
desc = "Automatic@ run@ of@ provers@ and@ most@ useful@ transformations"
name = "Auto_level_3"
shortcut = "3"

[strategy]
code = "start:
c Alt-Ergo,2.4.2 .2 1000
c CVC5,1.0.2 .5 1000
c Z3,4.11.2 .5 1000
t split_vc start
c Alt-Ergo,2.4.2 2. 4000
c CVC5,1.0.2 2. 4000
c Z3,4.11.2 2. 4000
"
desc = "Automatic@ run@ of@ main@ provers and splitting"
name = "Auto_level_2"
shortcut = "2"

[strategy]
code = "c Alt-Ergo,2.4.2 5. 1000
c CVC5,1.0.2 5. 1000
c Z3,4.11.2 5. 1000
"
desc = "Automatic@ run@ of@ main@ provers for longer times"
name = "Auto_level_1"
shortcut = "1"

[strategy]
code = "c Alt-Ergo,2.4.2 0.2 1000
c CVC5,1.0.2 0.5 1000
c Z3,4.11.2 0.5 1000
"
desc = "Automatic@ run@ of@ main@ provers 2020"
name = "Auto_level_0"
shortcut = "0"

[xldenis]

From analyzing CreuSAT:

stats:

I don't know why z3 is so heavily favored over alt-ergo, but it suggests that we can apply a quite similar strategy.

[jhjourdan]

If you want to include such strategies in Creusot, then could we please not specify versions of provers in the strategies?

[sarsko]

I asked about this in the Why3-Zulip a while back, and was not able to find a way to not specify versions (https://why3.zulipchat.com/#narrow/stream/304503-general/topic/Why3.20custom.20strategies/near/307707049)

[xldenis]

In that thread it seems to say that you should be able to run :

I believe you can omit versions in name, say using CVC5,, as a prover name would select a prover whose name is CVC5 is any. Not sure if it works, if it doesn't then I don't see any way to do

Does that not work? Also, does extra-config override pre-existing strategies?

[xldenis]

One thing that's missing in this analysis is reasoning about which transformations were effective. That would help to determine whether running the provers for 2 seconds in the middle of the auto-level 3 strategy is worth it at all.

I'm not sure how to ask that question though, perhaps analysis of the depth of solved goals would be informative here?