the function to create on the fly a symmetry step has been moved to equality

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

diff --git a/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml
index b71f5e5b6fbd7002191d354ab996e7b5e8f7da12..02b080147aa2c0ccbafaf1529137840c700c566c 100644 (file)
--- a/helm/software/components/tactics/paramodulation/saturation.ml
+++ b/helm/software/components/tactics/paramodulation/saturation.ml
@@ -404,34 +404,12 @@ let check_for_deep_subsumption env active_table eq =
       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        
+    | Some _ -> true        
   in 
   let rec aux b (ok_so_far, subsumption_used) t1 t2  = 
     match t1,t2 with
       | t1, t2 when not ok_so_far -> ok_so_far, subsumption_used
       | t1, t2 when subsumption_used -> t1 = t2, subsumption_used
-(* VERSIONE ERRATA 
-      | Cic.Appl (h1::l),Cic.Appl (h2::l') when h1 = h2 ->
-          let rc = check_subsumed b t1 t1 in 
-            if rc then 
-              true, true
-            else if h1 = h2 then
-              (try 
-                 List.fold_left2 
-                   (fun (ok_so_far, subsumption_used) t t' -> 
-                      aux true (ok_so_far, subsumption_used) t t')
-                   (ok_so_far, subsumption_used) l l'
-               with Invalid_argument _ -> false,subsumption_used)
-            else
-              false, subsumption_used
-      | _ -> false, subsumption_used *)
       | Cic.Appl (h1::l),Cic.Appl (h2::l') ->
           let rc = check_subsumed b t1 t2 in 
             if rc then 
@@ -450,20 +428,6 @@ let check_for_deep_subsumption env active_table eq =
   fst (aux false (true,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 *)
@@ -479,17 +443,7 @@ let forward_simplify env (sign,current) ?passive (active_list, active_table) =
       Indexing.demodulation_equality !maxmeta env table sign current in
     maxmeta := newmeta;
     if Equality.is_identity env newcurrent then
-(*         debug_print  *)
-(*           (lazy *)
-(*              (Printf.sprintf "\ncurrent was: %s\nnewcurrent is: %s\n" *)
-(*                 (string_of_equality current) *)
-(*                 (string_of_equality newcurrent))); *)
-(*         debug_print *)
-(*           (lazy *)
-(*              (Printf.sprintf "active is: %s" *)
-(*                 (String.concat "\n"  *)
-(*                    (List.map (fun (_, e) -> (string_of_equality e)) active_list)))); *)
-        None
+      None
     else
       Some newcurrent
   in
@@ -541,7 +495,7 @@ let forward_simplify env (sign,current) ?passive (active_list, active_table) =
 (*              if Indexing.subsumption env active_table c = None then*)
                 (match Indexing.subsumption env passive_table c with
                 | None -> res
-                | Some (_,c') -> 
+                | Some (_,c',_) -> 
                     None
                     (*prerr_endline "\n\nPESCO DALLE PASSIVE LA PIU' GENERALE\n\n";
                     Some c'*))
@@ -551,15 +505,6 @@ let forward_simplify env (sign,current) ?passive (active_list, active_table) =
 *)
 ;;
 
-type fs_time_info_t = {
-  mutable build_all: float;
-  mutable demodulate: float;
-  mutable subsumption: float;
-};;
-
-let fs_time_info = { build_all = 0.; demodulate = 0.; subsumption = 0. };;
-
-
 (** simplifies new using active and passive *)
 let forward_simplify_new env new_pos ?passive active =
   if Utils.debug_metas then
@@ -589,8 +534,7 @@ let forward_simplify_new env new_pos ?passive active =
     List.fold_left
       (fun s e ->
          if not (Equality.is_identity env e) then
-(*            if EqualitySet.mem e s then s *)
-           (*else*) EqualitySet.add e s
+           EqualitySet.add e s
          else s)
       EqualitySet.empty new_pos
   in
@@ -604,9 +548,6 @@ let forward_simplify_new env new_pos ?passive active =
         (fun e -> ((Indexing.subsumption env active_table e = None) &&
                          (Indexing.subsumption env passive_table e = None)))
   in
-(*   let t1 = Unix.gettimeofday () in *)
-(*   let t2 = Unix.gettimeofday () in *)
-(*   fs_time_info.subsumption <- fs_time_info.subsumption +. (t2 -. t1); *)
   let is_duplicate =
     match passive_table with
     | None ->
@@ -940,10 +881,12 @@ let print_goals goals =
            in
            Printf.sprintf "%d: %s" d (String.concat "; " gl')) goals))
 ;;
-
+              
 let check_if_goal_is_subsumed ((_,ctx,_) as env) table (goalproof,menv,ty) =
+(*
   let names = names_of_context ctx in
   Printf.eprintf "check_goal_subsumed: %s\n" (CicPp.pp ty names);
+*)
   match ty with
   | Cic.Appl[Cic.MutInd(uri,_,_);eq_ty;left;right] 
     when UriManager.eq uri (LibraryObjects.eq_URI ()) ->
@@ -953,12 +896,18 @@ let check_if_goal_is_subsumed ((_,ctx,_) as env) table (goalproof,menv,ty) =
       in
 (*      match Indexing.subsumption env table goal_equation with*)
        match Indexing.unification env table goal_equation with 
-        | Some (subst, equality ) ->
+        | Some (subst, equality, pos ) ->
             prerr_endline 
               ("GOAL SUBSUMED BY: " ^ Equality.string_of_equality equality);
             prerr_endline ("SUBST:" ^ Subst.ppsubst subst);
             let (_,p,(ty,l,r,_),m,id) = Equality.open_equality equality in
             let cicmenv = Subst.apply_subst_metasenv subst (m @ menv) in
+            let p =
+              if pos = Utils.Left then
+                Equality.symmetric eq_ty l id uri m
+              else
+                p
+            in
             Some (goalproof, p, id, subst, cicmenv)
         | None -> None)
   | _ -> None
@@ -1749,7 +1698,7 @@ let saturate
       given_clause_fullred dbd env goals theorems passive active
 *)
       let goals = make_goal_set goal in
-      let max_iterations = 1000 in
+      let max_iterations = 10000 in
       let max_time = Unix.gettimeofday () +.  300. (* minutes *) in
       given_clause env goals theorems passive active max_iterations max_time 
     in