Commit f305152e authored by MARCHE Claude's avatar MARCHE Claude
Browse files

keep former split_goal_wp and introduce a new transformation

parent 6be9b9a8
......@@ -327,22 +327,14 @@ let generate_auto_strategies config =
(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
(* Split VCs *)
let code = "t split_intros_goal_wp exit" in
let split = {
strategy_name = "Split";
strategy_desc = "Split@ the@ goal@ into@ subgoals";
strategy_name = "Split_VC";
strategy_desc = "Split@ the@ VC@ into@ subgoals";
strategy_shortcut = "s";
strategy_code = code }
in
(* Inline *)
let code = "t introduce_premises next next: t inline_goal exit" in
let inline = {
strategy_name = "Inline";
strategy_desc = "Inline@ definitions@ in@ the@ conclusion@ of@ the@ goal";
strategy_shortcut = "i";
strategy_code = code }
in
(* Auto level 0 and 1 *)
let provers_level1 =
Hprover.fold
......@@ -361,7 +353,7 @@ let generate_auto_strategies config =
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";
fprintf str_formatter "t split_all_full 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 = {
......@@ -380,14 +372,14 @@ let generate_auto_strategies config =
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";
fprintf str_formatter "t split_all_full 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 "afterintro:@\n";
fprintf str_formatter "t inline_goal afterinline@\n";
fprintf str_formatter "g trylongertime@\n";
fprintf str_formatter "afterinline:@\n";
fprintf str_formatter "t split_goal_wp start@\n";
fprintf str_formatter "t split_all_full start@\n";
fprintf str_formatter "trylongertime:@\n";
List.iter (fun s -> fprintf str_formatter "c %s 30 4000@\n" s) provers_level2;
let code = flush_str_formatter () in
......@@ -400,9 +392,7 @@ let generate_auto_strategies config =
add_strategy
(add_strategy
(add_strategy
(add_strategy
(add_strategy config inline)
split) auto0) auto1) auto2
(add_strategy config split) auto0) auto1) auto2
let detect_exec env data acc exec_name =
let s = ask_prover_version env exec_name data.version_switch in
......
......@@ -145,6 +145,7 @@ type config_strategy = {
}
(* a default set of strategies *)
(*
let default_strategies =
List.map
(fun (name,desc,shortcut,code) ->
......@@ -161,6 +162,7 @@ let default_strategies =
"Compute", "Compute@ in@ goal", "c",
"t compute_in_goal exit";
]
*)
let get_strategies ?(default=[]) rc =
match get_simple_family rc "strategy" with
......@@ -576,7 +578,7 @@ let get_config (filename,rc) =
let editors = List.fold_left load_editor Meditor.empty editors in
let policy = get_family rc "uninstalled_prover" in
let policy = List.fold_left (load_policy provers) Mprover.empty policy in
let strategies = get_strategies ~default:default_strategies rc in
let strategies = get_strategies ~default:[] rc in
let strategies = List.fold_left load_strategy Mstr.empty strategies in
{ conf_file = filename;
config = rc;
......
......@@ -115,23 +115,26 @@ let () = Trans.register_transform
~desc:"Replace axioms of the form 'exists x. P' by 'constant x axiom P'."
let split_goal_wp =
Trans.compose_l Split_goal.split_goal_right (Trans.singleton introduce_premises)
let simplify_intros =
Trans.compose Simplify_formula.simplify_trivial_quantification introduce_premises
let split_all_wp =
Trans.compose_l Split_goal.split_all_right (Trans.singleton introduce_premises)
let split_intros_goal_wp =
Trans.compose_l Split_goal.split_goal_right (Trans.singleton simplify_intros)
let split_premise_wp =
Trans.compose Split_goal.split_premise_right introduce_premises
let split_intros_all_wp =
Trans.compose_l Split_goal.split_all_right (Trans.singleton simplify_intros)
let split_intros_premise_wp =
Trans.compose Split_goal.split_premise_right simplify_intros
let () = Trans.register_transform_l
"split_goal_wp" split_goal_wp
~desc:"Same@ as@ split_goal_right."
"split_intros_goal_wp" split_intros_goal_wp
~desc:"The@ recommended@ splitting@ transformation@ to@ apply@ on@ VCs@ generated@ by@ WP@ (split_goal_right@ followed@ by@ simplify_trivial_quantifications@ followed@ by@ introduce_premises)."
let () = Trans.register_transform_l
"split_all_wp" split_all_wp
~desc:"Same@ as@ split_goal_wp,@ but@ also@ split@ premises."
"split_intros_intros_all_wp" split_intros_all_wp
~desc:"Same@ as@ split_intros_goal_wp,@ but@ also@ split@ premises."
let () = Trans.register_transform
"split_premise_wp" split_premise_wp
~desc:"Same@ as@ split_all_wp,@ but@ split@ only@ premises."
"split_intros_premise_wp" split_intros_premise_wp
~desc:"Same@ as@ split_intros_all_wp,@ but@ split@ only@ premises."
......@@ -32,9 +32,3 @@ val intros : Decl.prsymbol -> Term.term -> Decl.decl list
premises of [goal G : f] *)
val introduce_premises : Task.task Trans.trans
(* superseded by split_goal_wp
val split_intro : Task.task Trans.tlist
(** [split_intro] is [split_goal_wp] followed by [introduce_premises] *)
*)
......@@ -18,6 +18,8 @@ val fmla_remove_quant : Term.term -> Term.term
(** transforms \exists x. x == y /\ F into F[y/x]
and \forall x. x <> y \/ F into F[y/x] *)
val simplify_trivial_quantification : Task.task Trans.trans
val fmla_cond_subst: (Term.term -> Term.term -> bool) -> Term.term -> Term.term
(** given a formula [f] containing some equality or disequality [t1] ?= [t2]
such that [filter t1 t2] (resp [filter t2 t1]) evaluates to true,
......
......@@ -521,12 +521,15 @@ let prep_premise split = Trans.store (fun t ->
let split_goal_full = prep_goal full_proof
let split_goal_right = prep_goal right_proof
let split_goal_wp = split_goal_right
let split_all_full = prep_all full_proof
let split_all_right = prep_all right_proof
let split_all_wp = split_all_right
let split_premise_full = prep_premise full_proof
let split_premise_right = prep_premise right_proof
let split_premise_wp = split_premise_right
let () = Trans.register_transform_l "split_goal_full" split_goal_full
~desc:"Put@ the@ goal@ in@ a@ conjunctive@ form,@ \
......@@ -545,3 +548,10 @@ let () = Trans.register_transform_l "split_all_right" split_all_right
~desc:"Same@ as@ split_goal_right,@ but@ also@ split@ premises."
let () = Trans.register_transform "split_premise_right" split_premise_right
~desc:"Same@ as@ split_all_right,@ but@ split@ only@ premises."
let () = Trans.register_transform_l "split_goal_wp" split_goal_wp
~desc:"Same@ as@ split_goal_right."
let () = Trans.register_transform_l "split_all_wp" split_all_wp
~desc:"Same@ as@ split_goal_wp,@ but@ also@ split@ premises."
let () = Trans.register_transform "split_premise_wp" split_premise_wp
~desc:"Same@ as@ split_all_wp,@ but@ split@ only@ premises."
......@@ -56,3 +56,8 @@ val split_premise_full : Task.task Trans.trans
val split_goal_right : Task.task Trans.tlist
val split_all_right : Task.task Trans.tlist
val split_premise_right : Task.task Trans.trans
(* deprecated *)
val split_goal_wp : Task.task Trans.tlist
val split_all_wp : Task.task Trans.tlist
val split_premise_wp : Task.task Trans.trans
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