Commit 34aea94e authored by MARCHE Claude's avatar MARCHE Claude

rename split_intros_goal_wp into split_vc

parent 7adf6371
...@@ -328,7 +328,7 @@ let generate_auto_strategies config = ...@@ -328,7 +328,7 @@ let generate_auto_strategies config =
if b then eprintf " Prover %a will be used in Auto level >= %d@." if b then eprintf " Prover %a will be used in Auto level >= %d@."
Whyconf.print_prover p lev) prover_auto_levels; Whyconf.print_prover p lev) prover_auto_levels;
(* Split VCs *) (* Split VCs *)
let code = "t split_intros_goal_wp exit" in let code = "t split_vc exit" in
let split = { let split = {
strategy_name = "Split_VC"; strategy_name = "Split_VC";
strategy_desc = "Split@ the@ VC@ into@ subgoals"; strategy_desc = "Split@ the@ VC@ into@ subgoals";
......
...@@ -105,23 +105,9 @@ let () = Trans.register_transform ...@@ -105,23 +105,9 @@ let () = Trans.register_transform
let simplify_intros = let simplify_intros =
Trans.compose Simplify_formula.simplify_trivial_wp_quantification introduce_premises Trans.compose Simplify_formula.simplify_trivial_wp_quantification introduce_premises
let split_intros_goal_wp = let split_vc =
Trans.compose_l Split_goal.split_goal_right (Trans.singleton simplify_intros) Trans.compose_l Split_goal.split_goal_right (Trans.singleton simplify_intros)
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 let () = Trans.register_transform_l
"split_intros_goal_wp" split_intros_goal_wp "split_vcp" split_vc
~desc:"The@ recommended@ splitting@ transformation@ to@ apply@ on@ VCs@ generated@ by@ WP@ (split_goal_right@ followed@ by@ simplify_trivial_quantifications@ followed@ by@ introduce_premises)." ~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_intros_all_wp" split_intros_all_wp
~desc:"Same@ as@ split_intros_goal_wp,@ but@ also@ split@ premises."
let () = Trans.register_transform
"split_intros_premise_wp" split_intros_premise_wp
~desc:"Same@ as@ split_intros_all_wp,@ but@ split@ only@ premises."
...@@ -56,7 +56,7 @@ let alt_ergo_driver : Driver.driver = ...@@ -56,7 +56,7 @@ let alt_ergo_driver : Driver.driver =
let () = log_time ("Initialising why3 worker: end ") let () = log_time ("Initialising why3 worker: end ")
let split_trans = Trans.lookup_transform_l "split_intros_goal_wp" env let split_trans = Trans.lookup_transform_l "split_vc" env
(* CF gmain.ml ligne 568 et suivante *) (* CF gmain.ml ligne 568 et suivante *)
module W = module W =
......
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