Commit 023bcaf8 authored by MARCHE Claude's avatar MARCHE Claude

Autodetection generates default automatic strategies with some available provers

parent 8e2332ec
[ATP alt-ergo]
[ATP alt-ergo-prv]
name = "Alt-Ergo"
exec = "alt-ergo"
exec = "alt-ergo-1.20.prv"
exec = "alt-ergo-1.10.prv"
exec = "alt-ergo-1.01"
exec = "alt-ergo-1.00.prv"
version_switch = "-version"
version_regexp = "^\\([0-9.]+\\(-dev\\|prv\\)?\\)$"
version_ok = "1.20.prv"
version_ok = "1.10.prv"
version_ok = "1.01"
version_ok = "1.00.prv"
command = "%e -timelimit %t %f"
command_steps = "%e -steps-bound %S %f"
driver = "drivers/alt_ergo.drv"
editor = "altgr-ergo"
[ATP alt-ergo]
name = "Alt-Ergo"
exec = "alt-ergo"
exec = "alt-ergo-1.01"
version_switch = "-version"
version_regexp = "^\\([0-9.]+\\)$"
version_ok = "1.01"
command = "%e -timelimit %t %f"
command_steps = "%e -steps-bound %S %f"
driver = "drivers/alt_ergo.drv"
editor = "altgr-ergo"
use_at_auto_level = 1
[ATP alt-ergo]
name = "Alt-Ergo"
exec = "alt-ergo"
......@@ -31,7 +42,7 @@ driver = "drivers/alt_ergo.drv"
editor = "altgr-ergo"
# CVC4 version 1.5-prerelease
[ATP cvc4]
[ATP cvc4-15-pre]
name = "CVC4"
exec = "cvc4"
exec = "cvc4-1.5-prerelease"
......@@ -60,6 +71,7 @@ driver = "drivers/cvc4_14.drv"
# --rlimit=%S : cvc4 1.4 DOES NOT accept -1 as argument
# cvc4 1.4 does not print steps used in --stats anyway
command = "%e --tlimit-per=%t000 --lang=smt2 %f"
use_at_auto_level = 1
# CVC4 version 1.4, not using SMTLIB bitvectors
[ATP cvc4]
......@@ -74,7 +86,7 @@ driver = "drivers/cvc4.drv"
# --random-seed=42 is not needed as soon as --random-freq=0.0 by default
# to try: --inst-when=full-last-call
# --rlimit=%S : cvc4 1.4 DOES NOT accept -1 as argument
# cvc4 .14 does not print steps used in --stats anyway
# cvc4 1.4 does not print steps used in --stats anyway
command = "%e --tlimit-per=%t000 --lang=smt2 %f"
......@@ -328,6 +340,7 @@ version_ok = "4.4.0"
driver = "drivers/z3_440.drv"
command = "%e -smt2 sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 %f"
command_steps = "%e -smt2 sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 memory_max_alloc_count=%S %f"
use_at_auto_level = 1
# Z3 >= 4.4.0, without BV support
[ATP z3]
......
......@@ -70,6 +70,7 @@ type prover_autodetection_data =
prover_driver : string;
prover_editor : string;
prover_in_place : bool;
use_at_auto_level : int;
message : string option;
}
......@@ -79,7 +80,7 @@ let prover_keys =
["name";"compile_time_support";
"exec";"version_switch";"version_regexp";
"version_ok";"version_old";"version_bad";"command"; "command_steps";
"editor";"driver";"in_place";"message";"alternative";]
"editor";"driver";"in_place";"message";"alternative";"use_at_auto_level"]
let load_prover kind (id,section) =
check_exhaustive section prover_keys;
......@@ -101,6 +102,7 @@ let load_prover kind (id,section) =
prover_driver = get_string section ~default:"" "driver";
prover_editor = get_string section ~default:"" "editor";
prover_in_place = get_bool section ~default:false "in_place";
use_at_auto_level = get_int section ~default:0 "use_at_auto_level";
message = get_stringo section "message";
} in
if prover.prover_command != None && prover.prover_driver = "" then
......@@ -308,8 +310,90 @@ let add_prover_shortcuts env prover =
let add_id_prover_shortcut env id prover priority =
match Hstr.find_opt env.prover_shortcuts id with
| Some (p,_) when p >= priority -> ()
| Some _ -> assert false
| _ -> Hstr.replace env.prover_shortcuts id (priority,prover)
let prover_auto_levels = Hprover.create 5
let record_prover_for_auto_mode prover level =
Hprover.replace prover_auto_levels prover (level,false)
let check_prover_auto_level prover =
try
let lev,_ = Hprover.find prover_auto_levels prover in
Hprover.replace prover_auto_levels prover (lev,true)
with Not_found -> ()
let generate_auto_strategies config =
eprintf "Generating strategies:@.";
Hprover.iter
(fun p (lev,b) ->
if b then eprintf " Prover %a will be used in Auto level >= %d@."
Whyconf.print_prover p lev) prover_auto_levels;
(* Split *)
let code = "t split_goal_wp exit" in
let split = {
strategy_name = "Split";
strategy_desc = "Split@ the@ goal@ into@ subgoals";
strategy_shortcut = "s";
strategy_code = code }
in
(* Auto level 1 *)
let provers_level1 =
Hprover.fold
(fun p (lev,b) acc ->
if b && lev = 1 then
let name =
p.Whyconf.prover_name ^ "," ^
p.Whyconf.prover_version ^ "," ^ p.Whyconf.prover_altern
in name :: acc
else acc) prover_auto_levels []
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";
List.iter (fun s -> fprintf str_formatter "c %s 10 4000@\n" s) provers_level1;
let code = flush_str_formatter () in
let auto1 = {
strategy_name = "Auto level 1";
strategy_desc = "Automatic@ run@ of@ main@ provers";
strategy_shortcut = "1";
strategy_code = code }
in
(* Auto level 2 *)
let provers_level2 =
Hprover.fold
(fun p (lev,b) acc ->
if b && lev >= 1 && lev <= 2 then
let name =
p.Whyconf.prover_name ^ "," ^
p.Whyconf.prover_version ^ "," ^ p.Whyconf.prover_altern
in name :: acc
else acc) prover_auto_levels []
in
fprintf str_formatter "start:@\n";
List.iter (fun s -> fprintf str_formatter "c %s 1 1000@\n" s) provers_level2;
fprintf str_formatter "t split_goal_wp start@\n";
List.iter (fun s -> fprintf str_formatter "c %s 5 2000@\n" s) provers_level2;
fprintf str_formatter "t introduce_premises afterintro@\n";
fprintf str_formatter "g inline@\n";
fprintf str_formatter "afterintro:@\n";
fprintf str_formatter "t split_goal_wp start@\n";
fprintf str_formatter "inline:@\n";
fprintf str_formatter "t inline_goal afterinline@\n";
fprintf str_formatter "g longtime@\n";
fprintf str_formatter "afterinline:@\n";
fprintf str_formatter "t split_goal_wp start@\n";
fprintf str_formatter "longtime:@\n";
List.iter (fun s -> fprintf str_formatter "c %s 30 4000@\n" s) provers_level2;
let code = flush_str_formatter () in
let auto2 = {
strategy_name = "Auto level 2";
strategy_desc = "Automatic@ run@ of@ provers@ and@ most@ useful@ transformations";
strategy_shortcut = "2";
strategy_code = code }
in
add_strategy (add_strategy (add_strategy config split) auto1) auto2
let detect_exec env main data acc exec_name =
let s = ask_prover_version env exec_name data.version_switch in
......@@ -413,6 +497,8 @@ let detect_exec env main data acc exec_name =
known_version env exec_name;
add_prover_shortcuts env prover;
add_id_prover_shortcut env data.prover_id prover priority;
let level = data.use_at_auto_level in
if level > 0 then record_prover_for_auto_mode prover level;
add_prover_with_uniq_id prover_config acc
end
else (unknown_version env exec_name data.prover_id prover_config priority;
......@@ -441,7 +527,7 @@ let detect_unknown env detected =
let convert_shortcuts env =
Hstr.fold (fun s (_,p) acc ->
Mstr.add s p acc
check_prover_auto_level p; Mstr.add s p acc
) env.prover_shortcuts Mstr.empty
let run_auto_detection config =
......@@ -456,6 +542,7 @@ let run_auto_detection config =
"%d provers detected and %d provers detected with unsupported version@."
length_detected length_unsupported_version;
let shortcuts = convert_shortcuts env in
let config = generate_auto_strategies config in
let config = set_editors config (read_editors main) in
let config = set_prover_shortcuts config shortcuts in
let config = set_provers config detected in
......
......@@ -133,7 +133,7 @@ type config_editor = {
type config_strategy = {
strategy_name : string;
strategy_desc : Pp.formatted;
strategy_desc : string;
strategy_code : string;
strategy_shortcut : string;
}
......@@ -161,6 +161,18 @@ let get_strategies ?(default=[]) rc =
| [] -> default
| s -> s
let set_strategy _ s family =
let section = empty_section in
let section = set_string section "name" s.strategy_name in
let section = set_string section "desc" s.strategy_desc in
let section = set_string section "shortcut" s.strategy_shortcut in
let section = set_string section "code" s.strategy_code in
section::family
let set_strategies rc strategies =
let family = Mstr.fold set_strategy strategies [] in
set_simple_family rc "strategy" family
(** Main record *)
type main = {
......@@ -489,7 +501,9 @@ let load_strategy strategies section =
try
let name = get_string section "name" in
let desc = get_string section "desc" in
(*
let desc = Scanf.format_from_string desc "" in
*)
let shortcut = get_string ~default:"" section "shortcut" in
let code = get_string section "code" in
Mstr.add
......@@ -800,6 +814,13 @@ let editor_by_id whyconf id =
let get_strategies config = config.strategies
let add_strategy c strat =
let f = get_strategies c in
let strategies = Mstr.add strat.strategy_name strat f in
{ c with strategies = strategies;
config = set_strategies c.config strategies }
(******)
let get_section config name = assert (name <> "main");
......
......@@ -128,7 +128,7 @@ val get_provers : config -> config_prover Mprover.t
keys are the unique ids of the prover (argument of the family) *)
val set_provers : config ->
?shortcuts:Mprover.key Mstr.t -> config_prover Mprover.t -> config
?shortcuts:prover Mstr.t -> config_prover Mprover.t -> config
(** [set_provers config provers] replace all the family prover by the
one given *)
......@@ -184,13 +184,15 @@ val set_policies : config -> prover_upgrade_policy Mprover.t -> config
type config_strategy = {
strategy_name : string;
strategy_desc : Pp.formatted;
strategy_desc : string;
strategy_code : string;
strategy_shortcut : string;
}
val get_strategies : config -> config_strategy Mstr.t
val add_strategy : config -> config_strategy -> config
(** filter prover *)
type filter_prover
......
......@@ -1680,6 +1680,7 @@ let () =
let () =
let iter (name,desc,strat,k) =
let desc = Scanf.format_from_string desc "" in
let b = GButton.button ~packing:strategies_box#add
~label:(sanitize_markup name) ()
in
......@@ -2304,6 +2305,7 @@ let () =
let submenu = tools_factory#add_submenu "Strategies" in
let submenu = new GMenu.factory submenu ~accel_group in
let iter (name,desc,strat,k) =
let desc = Scanf.format_from_string desc "" in
let callback () = apply_strategy_on_selection strat in
let ii = submenu#add_image_item
~label:(sanitize_markup name) ~callback ()
......
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