goal demodulated with new

[helm.git] / components / tactics / paramodulation / saturation.ml

diff --git a/components/tactics/paramodulation/saturation.ml b/components/tactics/paramodulation/saturation.ml
index f1cec900f1d54eaa100f1a0f8006d490c9bc176b..1cb6d351433f158a52aa5511b51e0c36c32b1bd1 100644 (file)
--- a/components/tactics/paramodulation/saturation.ml
+++ b/components/tactics/paramodulation/saturation.ml
@@ -354,6 +354,50 @@ let infer env current (active_list, active_table) =
         List.filter (fun e -> OrderedEquality.compare e eq <= 0) new_pos
 ;;
 
+let check_for_deep_subsumption env active_table eq =
+  let _,_,(eq_ty, left, right, order),metas,id = Equality.open_equality eq in
+  if id = 14242 then assert false;
+  
+  let check deep l r = 
+    let eqtmp = 
+      Equality.mk_tmp_equality(0,(eq_ty,l,r,Utils.Incomparable),metas)in
+    match Indexing.subsumption env active_table eqtmp with
+    | None -> false
+    | Some (s,eq') -> 
+        prerr_endline 
+          ("\n\n " ^ Equality.string_of_equality ~env eq ^ 
+          "\nis"^(if deep then " CONTEXTUALLY " else " ")^"subsumed by \n " ^ 
+          Equality.string_of_equality ~env eq' ^ "\n\n");
+        true        
+  in 
+  let rec aux b = function
+    | Cic.Rel n, Cic.Rel m -> if n = m then true else false
+    | ((Cic.Appl l) as left),((Cic.Appl l') as right) ->
+        check b left right ||
+        (try 
+          List.for_all2 (fun t t' -> aux true (t,t')) (List.tl l) (List.tl l')
+        with Invalid_argument _ -> false)
+    | (Cic.Meta _),_ 
+    | _,(Cic.Meta _) -> false
+    | _ -> false
+  in
+  aux false (left,right)
+;;
+
+(*
+let check_for_deep env active_table eq =
+  match Indexing.subsumption env active_table eq with
+  | None -> false
+  | Some _ -> true
+;;
+*)
+
+let profiler = HExtlib.profile "check_for_deep";;
+
+let check_for_deep_subsumption env active_table eq = 
+  profiler.HExtlib.profile (check_for_deep_subsumption env active_table) eq
+;;
+
 (* buttare via sign *)
 
 (** simplifies current using active and passive *)
@@ -407,26 +451,35 @@ let forward_simplify env (sign,current) ?passive (active_list, active_table) =
   match res with
   | None -> None
   | Some c ->
-      (* immagino non funzioni piu'... *)
       if Indexing.in_index active_table c then
         None
       else
         match passive_table with
         | None -> 
+            if check_for_deep_subsumption env active_table c then
+              None
+            else 
+              res
+(*
             if Indexing.subsumption env active_table c = None then
               res
             else
               None
+*)
         | Some passive_table ->
             if Indexing.in_index passive_table c then None
             else 
-              if Indexing.subsumption env active_table c = None then
-                if Indexing.subsumption env passive_table c = None then
-                  res 
-                else
-                  None
+              if check_for_deep_subsumption env active_table c then
+                None
+              else 
+(*              if Indexing.subsumption env active_table c = None then*)
+                (match Indexing.subsumption env passive_table c with
+                | None -> res
+                | Some (_,c') -> None (*Some c'*))
+(*
               else
                 None
+*)
 ;;
 
 type fs_time_info_t = {
@@ -525,8 +578,8 @@ let rec simplify_goal env goal ?passive (active_list, active_table) =
     | None -> demodulate active_table goal
     | Some passive_table ->
         let changed, goal = demodulate active_table goal in
-        let changed', goal = demodulate passive_table goal in
-        (changed || changed'), goal
+(*        let changed', goal = demodulate passive_table goal in*)
+        (changed (*|| changed'*)), goal
   in
   changed,
   if not changed then 
@@ -634,15 +687,25 @@ let backward_simplify_passive env new_pos new_table min_weight passive =
   |  _ -> ((pl, ps), passive_table), Some (newp)
 ;;
 
+let build_table equations =
+    List.fold_left
+      (fun (l, t, w) e ->
+         let ew, _, _, _ , _ = Equality.open_equality e in
+         e::l, Indexing.index t e, min ew w)
+      ([], Indexing.empty, 1000000) equations
+;;
+  
 
 let backward_simplify env new' ?passive active =
-  let new_pos, new_table, min_weight =
+  let new_pos, new_table, min_weight = build_table new' in
+(*
     List.fold_left
       (fun (l, t, w) e ->
          let ew, _, _, _ , _ = Equality.open_equality e in
          e::l, Indexing.index t e, min ew w)
       ([], Indexing.empty, 1000000) new'
   in
+*)
   let active, newa =
     backward_simplify_active env new_pos new_table min_weight active in
   match passive with
@@ -1103,6 +1166,11 @@ and given_clause_fullred_aux dbd env goals theorems passive active =
                   simplify (new' @ p @ rp) active passive
             in
             let active, _, new' = simplify new' active passive in
+            let goals = 
+              let a,b,_ = build_table new' in
+              simplify_goals env goals ~passive (a,b)
+            in
+              
 (* pessima prova 
             let new1 = prova env new' active in
             let new' = (fst new') @ (fst new1), (snd new') @ (snd new1) in