Commit c3dc3f73 authored by Andrei Paskevich's avatar Andrei Paskevich

Term: drop "keep_on_simp" in generic simplifying constructors

Instead, we use more cautious simplification in Vc.
parent 4ee46717
......@@ -1434,10 +1434,6 @@ let t_pred_app_beta lam t = t_pred_app_beta_l lam [t]
(* constructors with propositional simplification *)
let keep_on_simp = create_label "keep_on_simp"
let can_simp t = not (Slab.mem keep_on_simp t.t_label)
let can_simp_left t = can_simp t && not (Slab.mem asym_split t.t_label)
let t_not_simp f = match f.t_node with
| Ttrue -> t_label_copy f t_false
| Tfalse -> t_label_copy f t_true
......@@ -1445,59 +1441,59 @@ let t_not_simp f = match f.t_node with
| _ -> t_not f
let t_and_simp f1 f2 = match f1.t_node, f2.t_node with
| Ttrue, _ when can_simp f1 -> f2
| _, Ttrue when can_simp f2 -> t_label_remove asym_split f1
| Tfalse, _ when can_simp f2 -> t_label_remove asym_split f1
| _, Tfalse when can_simp_left f1 -> f2
| _, _ when t_equal f1 f2 -> f1
| Ttrue, _ -> f2
| _, Ttrue -> t_label_remove asym_split f1
| Tfalse, _ -> t_label_remove asym_split f1
| _, Tfalse -> f2
| _, _ when t_equal f1 f2 -> f1
| _, _ -> t_and f1 f2
let t_and_simp_l l = List.fold_right t_and_simp l t_true
let t_or_simp f1 f2 = match f1.t_node, f2.t_node with
| Ttrue, _ when can_simp f2 -> t_label_remove asym_split f1
| _, Ttrue when can_simp_left f1 -> f2
| Tfalse, _ when can_simp f1 -> f2
| _, Tfalse when can_simp f2 -> t_label_remove asym_split f1
| _, _ when t_equal f1 f2 -> f1
| Ttrue, _ -> t_label_remove asym_split f1
| _, Ttrue -> f2
| Tfalse, _ -> f2
| _, Tfalse -> t_label_remove asym_split f1
| _, _ when t_equal f1 f2 -> f1
| _, _ -> t_or f1 f2
let t_or_simp_l l = List.fold_right t_or_simp l t_false
let t_and_asym_simp f1 f2 = match f1.t_node, f2.t_node with
| Ttrue, _ when can_simp f1 -> f2
| _, Ttrue when can_simp f2 -> t_label_remove asym_split f1
| Tfalse, _ when can_simp f2 -> t_label_remove asym_split f1
(*| _, Tfalse when can_simp f1 -> f2*)
| _, _ when t_equal f1 f2 -> f1
| Ttrue, _ -> f2
| _, Ttrue -> t_label_remove asym_split f1
| Tfalse, _ -> t_label_remove asym_split f1
| _, Tfalse -> f2
| _, _ when t_equal f1 f2 -> f1
| _, _ -> t_and_asym f1 f2
let t_and_asym_simp_l l = List.fold_right t_and_asym_simp l t_true
let t_or_asym_simp f1 f2 = match f1.t_node, f2.t_node with
| Ttrue, _ when can_simp f2 -> t_label_remove asym_split f1
(*| _, Ttrue when can_simp f1 -> f2*)
| Tfalse, _ when can_simp f1 -> f2
| _, Tfalse when can_simp f2 -> t_label_remove asym_split f1
| _, _ when t_equal f1 f2 -> f1
| Ttrue, _ -> t_label_remove asym_split f1
| _, Ttrue -> f2
| Tfalse, _ -> f2
| _, Tfalse -> t_label_remove asym_split f1
| _, _ when t_equal f1 f2 -> f1
| _, _ -> t_or_asym f1 f2
let t_or_asym_simp_l l = List.fold_right t_or_asym_simp l t_false
let t_implies_simp f1 f2 = match f1.t_node, f2.t_node with
| Ttrue, _ when can_simp f1 -> f2
| _, Ttrue when can_simp f1 -> f2
| Tfalse, _ when can_simp f2 -> t_label_copy f1 t_true
| _, Tfalse when can_simp f2 -> t_not_simp f1
| _, _ when t_equal f1 f2 -> t_label_copy f1 t_true
| Ttrue, _ -> f2
| _, Ttrue -> f2
| Tfalse, _ -> t_label_copy f1 t_true
| _, Tfalse -> t_not_simp f1
| _, _ when t_equal f1 f2 -> t_label_copy f1 t_true
| _, _ -> t_implies f1 f2
let t_iff_simp f1 f2 = match f1.t_node, f2.t_node with
| Ttrue, _ when can_simp f1 -> f2
| _, Ttrue when can_simp f2 -> f1
| Tfalse, _ when can_simp f1 -> t_not_simp f2
| _, Tfalse when can_simp f2 -> t_not_simp f1
| _, _ when t_equal f1 f2 -> t_label_copy f1 t_true
| Ttrue, _ -> f2
| _, Ttrue -> f1
| Tfalse, _ -> t_not_simp f2
| _, Tfalse -> t_not_simp f1
| _, _ when t_equal f1 f2 -> t_label_copy f1 t_true
| _, _ -> t_iff f1 f2
let t_binary_simp op = match op with
......@@ -1507,13 +1503,13 @@ let t_binary_simp op = match op with
| Tiff -> t_iff_simp
let t_if_simp f1 f2 f3 = match f1.t_node, f2.t_node, f3.t_node with
| Ttrue, _, _ when can_simp f1 && can_simp f3 -> f2
| Tfalse, _, _ when can_simp f1 && can_simp f2 -> f3
| _, Ttrue, _ when can_simp f2 -> t_implies_simp (t_not_simp f1) f3
| _, Tfalse, _ when can_simp f2 -> t_and_asym_simp (t_not_simp f1) f3
| _, _, Ttrue when can_simp f3 -> t_implies_simp f1 f2
| _, _, Tfalse when can_simp f3 -> t_and_asym_simp f1 f2
| _, _, _ when t_equal f2 f3 && can_simp f1 -> f2
| Ttrue, _, _ -> f2
| Tfalse, _, _ -> f3
| _, Ttrue, _ -> t_implies_simp (t_not_simp f1) f3
| _, Tfalse, _ -> t_and_asym_simp (t_not_simp f1) f3
| _, _, Ttrue -> t_implies_simp f1 f2
| _, _, Tfalse -> t_and_asym_simp f1 f2
| _, _, _ when t_equal f2 f3 -> f2
| _, _, _ -> t_if f1 f2 f3
let small t = match t.t_node with
......@@ -1522,7 +1518,7 @@ let small t = match t.t_node with
let t_let_simp e ((v,b,t) as bt) =
let n = t_v_occurs v t in
if n = 0 && can_simp e then
if n = 0 then
t_subst_unsafe b.bv_subst t else
if n = 1 || small e then begin
vs_check v e;
......@@ -1532,7 +1528,7 @@ let t_let_simp e ((v,b,t) as bt) =
let t_let_close_simp v e t =
let n = t_v_occurs v t in
if n = 0 && can_simp e then t else
if n = 0 then t else
if n = 1 || small e then
t_subst_single v e t
else
......@@ -1547,10 +1543,10 @@ let t_case_simp t bl =
let e0_false = match e0.t_node with
| Tfalse -> true | _ -> false in
let is_e0 (_,_,e) = match e.t_node with
| Ttrue when can_simp e -> e0_true
| Tfalse when can_simp e -> e0_false
| Ttrue -> e0_true
| Tfalse -> e0_false
| _ -> t_equal e e0 in
if can_simp t && t_closed e0 && List.for_all is_e0 tl then e0
if t_closed e0 && List.for_all is_e0 tl then e0
else t_case t bl
let t_case_close_simp t bl =
......@@ -1562,10 +1558,10 @@ let t_case_close_simp t bl =
let e0_false = match e0.t_node with
| Tfalse -> true | _ -> false in
let is_e0 (_,e) = match e.t_node with
| Ttrue when can_simp e -> e0_true
| Tfalse when can_simp e -> e0_false
| Ttrue -> e0_true
| Tfalse -> e0_false
| _ -> t_equal e e0 in
if can_simp t && t_closed e0 && List.for_all is_e0 tl then e0
if t_closed e0 && List.for_all is_e0 tl then e0
else t_case_close t bl
let t_quant_simp q ((vl,_,_,f) as qf) =
......@@ -1598,10 +1594,10 @@ let t_forall_close_simp = t_quant_close_simp Tforall
let t_exists_close_simp = t_quant_close_simp Texists
let t_equ_simp t1 t2 =
if t_equal t1 t2 && can_simp t1 then t_true else t_equ t1 t2
if t_equal t1 t2 then t_true else t_equ t1 t2
let t_neq_simp t1 t2 =
if t_equal t1 t2 && can_simp t1 then t_false else t_neq t1 t2
if t_equal t1 t2 then t_false else t_neq t1 t2
let t_forall_close_merge vs f = match f.t_node with
| Tquant (Tforall, fq) ->
......
......@@ -247,8 +247,6 @@ val t_label_copy : term -> term -> term
(** Constructors with propositional simplification *)
val keep_on_simp : label
val t_if_simp : term -> term -> term -> term
val t_let_simp : term -> term_bound -> term
val t_case_simp : term -> term_branch list -> term
......
......@@ -90,7 +90,6 @@ let split_case_2 kn forig spl pos acc t bl =
let stop f = Slab.mem Term.stop_split f.t_label
let asym f = Slab.mem Term.asym_split f.t_label
let keep f = Slab.mem Term.keep_on_simp f.t_label
let unstop f =
t_label ?loc:f.t_loc (Slab.remove stop_split f.t_label) f
......@@ -104,7 +103,7 @@ type split = {
let rec split_pos ro acc f = match f.t_node with
| _ when ro.stop_label && stop f -> unstop f :: acc
| Ttrue -> if keep f then f::acc else acc
| Ttrue -> acc
| Tfalse -> f::acc
| Tapp _ -> f::acc
| Tbinop (Tand,f1,f2) when ro.respect_as && asym f1 ->
......@@ -150,7 +149,7 @@ let rec split_pos ro acc f = match f.t_node with
and split_neg ro acc f = match f.t_node with
| _ when ro.stop_label && stop f -> unstop f :: acc
| Ttrue -> f::acc
| Tfalse -> if keep f then f::acc else acc
| Tfalse -> acc
| Tapp _ -> f::acc
| Tbinop (Tand,_,_) when ro.right_only -> f::acc
| Tbinop (Tand,f1,f2) ->
......@@ -299,7 +298,7 @@ let split_intro known_map pr f =
let rec split_intro dl acc f =
let rsp = split_intro dl in
match f.t_node with
| Ttrue when not (keep f) -> acc
| Ttrue -> acc
| Tbinop (Tand,f1,f2) when asym f1 ->
rsp (rsp acc (t_implies f1 f2)) f1
| Tbinop (Tand,f1,f2) ->
......
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