]> matita.cs.unibo.it Git - helm.git/commitdiff
speedup in fixing the graph closures
authorEnrico Tassi <enrico.tassi@inria.fr>
Tue, 29 Apr 2008 10:18:56 +0000 (10:18 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Tue, 29 Apr 2008 10:18:56 +0000 (10:18 +0000)
helm/software/components/cic/cicUniv.ml

index 8570c0c15c28f4a11f7818fca9d78a0076251538..a936c16bf9fb688e399cb5e30c63fe6813323644 100644 (file)
@@ -46,6 +46,7 @@ open Printf
 (** Types and default values                                                **)
 (*****************************************************************************)
 
+
 type universe = int * UriManager.uri option 
 
 let eq u1 u2 = 
@@ -216,7 +217,9 @@ and print_rec_status u ru =
   print_endline ("Aggiusto " ^ (string_of_universe u) ^ 
                  "e ottengo questa chiusura\n " ^ (string_of_node ru))
 
-and adjust_fast_aux u m =
+and adjust_fast_aux adjusted u m =
+  if SOF.mem u adjusted then m, adjusted else
+  let adjusted = SOF.add u adjusted in
   let ru = repr u m in
   let gt_c = closure_gt_fast ru m in
   let ge_c = closure_ge_fast ru m in
@@ -227,7 +230,7 @@ and adjust_fast_aux u m =
     (not (are_set_eq ge_c ru.ge_closure))
   in
     if ((not changed_gegt) &&  (not changed_eq)) then
-      m
+      m, adjusted
     else
       begin
         let ru' = {
@@ -240,21 +243,25 @@ and adjust_fast_aux u m =
           one_s_gt = ru.one_s_gt}
         in
         let m = MAL.add u ru' m in
-        let m =
-            SOF.fold (fun x m -> adjust_fast_aux  x m) 
-              (SOF.union ru'.eq_closure ru'.in_gegt_of) m
-              (* TESI: 
-                   ru'.in_gegt_of m 
-              *)
+        let m, adjusted  =
+          SOF.fold (fun x (m,adjusted) -> MAL.add x ru' m, SOF.add x adjusted) 
+            (SOF.diff ru'.eq_closure adjusted) 
+            (m,adjusted)
+        in
+        let m, adjusted  =
+            SOF.fold (fun x (m,adjusted) -> adjust_fast_aux adjusted x m) 
+              (SOF.diff ru'.in_gegt_of adjusted) 
+              (m,adjusted)
         in
-          m (*adjust_fast  u m*)
+          m, adjusted 
       end
 
 (*
 and profiler_adj = HExtlib.profile "CicUniv.adjust_fast"
 and adjust_fast x y = profiler_adj.HExtlib.profile (adjust_fast_aux x) y
 *)
-and adjust_fast x y = adjust_fast_aux x y
+and adjust_fast x y = 
+  fst(adjust_fast_aux SOF.empty x y)
         
 and add_gt_arc_fast u v m =
   let ru = repr u m in