Commit 79692dfc authored by Sylvain Dailler's avatar Sylvain Dailler

transformation: add trivial_true (from SPARK); change strategy split_vc

The strategy split_VC now tries to apply trivial_true on generated goals
so that they do not appear unproved.
parent 8e6dbce8
......@@ -362,7 +362,7 @@ let generate_auto_strategies env =
if b then print_info " Prover %a will be used in Auto level >= %d@."
Whyconf.print_prover p lev) env.prover_auto_levels;
(* Split VCs *)
let code = "t split_vc exit" in
let code = "t split_vc next\nnext: \nt trivial_true\n exit" in
let split = {
strategy_name = "Split_VC";
strategy_desc = "Split@ the@ VC@ into@ subgoals";
......
......@@ -243,3 +243,33 @@ let fmla_cond_subst filter f =
fmla_unflatten conj f subf
| _ -> t_map aux f in
aux f
let rec is_trivial fml =
(* Check wether the formula is trivial. *)
match fml.t_node with
| Ttrue -> true
| Tquant (_,tq) ->
let _,_,t = t_open_quant tq in
is_trivial t
| Tlet (_,tb) ->
let _, t = t_open_bound tb in
is_trivial t
| Tbinop (Timplies,_,t2) ->
is_trivial t2
| Tcase (_,tbl) ->
List.for_all (fun b ->
let _, t = t_open_branch b in
is_trivial t) tbl
| _ -> false
let is_trivial_trans =
Trans.goal_l (fun pr t ->
if is_trivial t then
[] (* Goal is proved *)
else
[[Decl.create_prop_decl Pgoal pr t]])
let () = Trans.register_transform_l ~desc:"Prove goals whose positive part is just [true]"
"trivial_true"
is_trivial_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