From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Mon, 14 Apr 2008 09:00:52 +0000 (+0000)
Subject: added little optimization to not add twice the same arc
X-Git-Tag: make_still_working~5347
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7149d50a94090ffa72df8105a9d45eb9c9b6abf6;p=helm.git

added little optimization to not add twice the same arc
---

diff --git a/helm/software/components/cic/cicUniv.ml b/helm/software/components/cic/cicUniv.ml
index fd0f696d9..d3ae5c960 100644
--- a/helm/software/components/cic/cicUniv.ml
+++ b/helm/software/components/cic/cicUniv.ml
@@ -227,7 +227,7 @@ 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 u m =
+and adjust_fast_aux u m =
   let ru = repr u m in
   let gt_c = closure_gt_fast ru m in
   let ge_c = closure_ge_fast ru m in
@@ -252,7 +252,7 @@ and adjust_fast u m =
         in
         let m = MAL.add u ru' m in
         let m =
-            SOF.fold (fun x m -> adjust_fast  x 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 
@@ -260,9 +260,16 @@ and adjust_fast u m =
         in
           m (*adjust_fast  u m*)
       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 add_gt_arc_fast u v m =
   let ru = repr u m in
+  if SOF.mem v ru.gt_closure then m else
   let ru' = {ru with one_s_gt = SOF.add v ru.one_s_gt} in
   let m' = MAL.add u ru' m in
   let rv = repr v m' in
@@ -272,6 +279,7 @@ and add_gt_arc_fast u v m =
       
 and add_ge_arc_fast u v m =
   let ru = repr u m in
+  if SOF.mem v ru.ge_closure then m else
   let ru' = { ru with one_s_ge = SOF.add v ru.one_s_ge} in
   let m' = MAL.add u ru' m in
   let rv = repr v m' in
@@ -281,6 +289,7 @@ and add_ge_arc_fast u v m =
 
 and add_eq_arc_fast u v m =
   let ru = repr u m in
+  if SOF.mem v ru.eq_closure then m else
   let rv = repr v m in 
   let ru' = {ru  with one_s_eq = SOF.add v ru.one_s_eq} in
   (*TESI: let ru' = {ru' with in_gegt_of = SOF.add v ru.in_gegt_of} in *)
@@ -570,7 +579,7 @@ let add_gt ?(fast=(!fast_implementation)) u v (b,already_contained,oblivion) =
   end_spending ();
     rc,already_contained,false)
     
-(* profiling code
+(* profiling code 
 let profiler_eq = HExtlib.profile "CicUniv.add_eq"
 let profiler_ge = HExtlib.profile "CicUniv.add_ge"
 let profiler_gt = HExtlib.profile "CicUniv.add_gt"
@@ -670,7 +679,7 @@ let merge_ugraphs ~base_ugraph ~increment:(increment, uri_of_increment(*,l*)) =
     (UriManager.UriSet.add uri_of_increment already_contained), false
 
 (* profiling code; WARNING: the time spent during profiling can be
-   greater than the profiled time
+   greater than the profiled time 
 let profiler_merge = HExtlib.profile "CicUniv.merge_ugraphs"
 let merge_ugraphs ~base_ugraph ~increment =
   profiler_merge.HExtlib.profile