Commit 785df505 authored by MARCHE Claude's avatar MARCHE Claude

adding strategy auto 0, same as level 1 but without split

parent 5878d5a1
......@@ -343,7 +343,7 @@ let generate_auto_strategies config =
strategy_shortcut = "i";
strategy_code = code }
in
(* Auto level 1 *)
(* Auto level 0 and 1 *)
let provers_level1 =
Hprover.fold
(fun p (lev,b) acc ->
......@@ -354,6 +354,14 @@ let generate_auto_strategies config =
in name :: acc
else acc) prover_auto_levels []
in
List.iter (fun s -> fprintf str_formatter "c %s 1 1000@\n" s) provers_level1;
let code = flush_str_formatter () in
let auto0 = {
strategy_name = "Auto level 0";
strategy_desc = "Automatic@ run@ of@ main@ provers";
strategy_shortcut = "0";
strategy_code = code }
in
fprintf str_formatter "start:@\n";
List.iter (fun s -> fprintf str_formatter "c %s 1 1000@\n" s) provers_level1;
fprintf str_formatter "t split_goal_wp start@\n";
......@@ -397,7 +405,10 @@ let generate_auto_strategies config =
in
add_strategy
(add_strategy
(add_strategy (add_strategy config inline) split) auto1) auto2
(add_strategy
(add_strategy
(add_strategy config inline)
split) auto0) auto1) auto2
let detect_exec env data acc exec_name =
let s = ask_prover_version env exec_name data.version_switch in
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment