slow_implementation and some dead code removed

diff --git a/helm/software/components/cic/cicUniv.ml b/helm/software/components/cic/cicUniv.ml
index 2bfbc92a32f999553815ee7f7326ebbe2ee5a3d4..7aac62cff5b77e08ae1537ab2850731b52c9e27b 100644 (file)
--- a/helm/software/components/cic/cicUniv.ml
+++ b/helm/software/components/cic/cicUniv.ml
@@ -36,12 +36,6 @@
 
 (* $Id$ *)
 
-(*****************************************************************************)
-(** switch implementation                                                   **)
-(*****************************************************************************)
-
-let fast_implementation = ref true ;;
-
 (*****************************************************************************)
 (** open                                                                    **)
 (*****************************************************************************)
@@ -135,29 +129,6 @@ let string_of_mal m =
 let string_of_bag b = 
   string_of_mal b
 
-(*****************************************************************************)
-(** Benchmarking                                                            **)
-(*****************************************************************************)
-let time_spent = ref 0.0;;
-let partial = ref 0.0 ;;
-
-let reset_spent_time () = time_spent := 0.0;;
-let get_spent_time () = !time_spent ;;
-let begin_spending () = ()
-  (*assert (!partial = 0.0);*)
-(*   partial := Unix.gettimeofday () *)
-;;
-
-let end_spending () = ()
-(*
-  assert (!partial > 0.0);
-  let interval = (Unix.gettimeofday ()) -. !partial in
-    partial := 0.0;
-    time_spent := !time_spent +. interval
-*)
-;;
-
-
 (*****************************************************************************)
 (** Helpers                                                                 **)
 (*****************************************************************************)
@@ -301,108 +272,6 @@ and add_eq_arc_fast u v m =
 ;;
 
 \f
-(*****************************************************************************)
-(** safe implementation                                                     **)
-(*****************************************************************************)
-
-let closure_of u m =
-  let ru = repr u m in
-  let eq_c =
-    let j = ru.one_s_eq in
-    let _Uj = merge_closures (fun x -> x.eq_closure) j m in
-    let one_step_eq = ru.one_s_eq in
-            (SOF.union one_step_eq _Uj)
-  in
-  let ge_c = 
-    let j = SOF.union ru.one_s_ge (SOF.union ru.one_s_gt ru.one_s_eq) in
-    let _Uj = merge_closures (fun x -> x.ge_closure) j m in
-    let _Ux = j in
-      (SOF.union _Uj _Ux)
-  in
-  let gt_c =
-    let j = ru.one_s_gt in
-    let k = ru.one_s_ge in
-    let l = ru.one_s_eq in
-    let _Uj = merge_closures (fun x -> x.ge_closure) j m in
-    let _Uk = merge_closures (fun x -> x.gt_closure) k m in
-    let _Ul = merge_closures (fun x -> x.gt_closure) l m in
-    let one_step_gt = ru.one_s_gt in
-      (SOF.union (SOF.union (SOF.union _Ul one_step_gt) _Uk) _Uj)
-  in
-    {
-      eq_closure = eq_c;
-      ge_closure = ge_c;
-      gt_closure = gt_c;
-      in_gegt_of = ru.in_gegt_of;
-      one_s_eq = ru.one_s_eq;
-      one_s_ge = ru.one_s_ge;
-      one_s_gt = ru.one_s_gt
-    }
-
-let rec simple_adjust m =
-  let m' = 
-    MAL.mapi (fun x _ -> closure_of x m) m
-  in
-    if not (are_ugraph_eq m  m') then(
-      simple_adjust m')
-    else
-      m'
-
-let add_eq_arc u v m =
-  let ru = repr u m in
-  let rv = repr v m in
-  let ru' = {ru with one_s_eq = SOF.add v ru.one_s_eq} in
-  let m' = MAL.add u ru' m in
-  let rv' = {rv with one_s_eq = SOF.add u rv.one_s_eq} in
-  let m'' = MAL.add v rv' m' in
-    simple_adjust m''
-
-let add_ge_arc u v m =
-  let ru = repr u m in
-  let ru' = { ru with one_s_ge = SOF.add v ru.one_s_ge} in
-  let m' = MAL.add u ru' m in
-    simple_adjust m'
-
-let add_gt_arc u v m =
-  let ru = repr u m in
-  let ru' = {ru with one_s_gt = SOF.add v ru.one_s_gt} in
-  let m' = MAL.add u ru' m in
-    simple_adjust m'
-
-\f
-(*****************************************************************************)
-(** Outhern interface, that chooses between _fast and safe                  **)
-(*****************************************************************************)
-
-(*                                                                            
-    given the 2 nodes plus the current bag, adds the arc, recomputes the 
-    closures and returns the new map
-*) 
-let add_eq fast u v b =
-  if fast then
-    add_eq_arc_fast u v b
-  else
-    add_eq_arc u v b
-
-(*                                                                            
-    given the 2 nodes plus the current bag, adds the arc, recomputes the 
-    closures and returns the new map
-*) 
-let add_ge fast u v b =
-  if fast then
-    add_ge_arc_fast u v b
-  else
-    add_ge_arc u v b
-(*                                                                            
-    given the 2 nodes plus the current bag, adds the arc, recomputes the 
-    closures and returns the new map
-*)                                                                            
-let add_gt fast u v b =
-  if fast then
-    add_gt_arc_fast u v b
-  else
-    add_gt_arc u v b
-
 
 (*****************************************************************************)
 (** Other real code                                                         **)
@@ -500,7 +369,7 @@ let print_ugraph (g, _, o) =
   if o then prerr_endline "oblivion universe" else
   prerr_endline (string_of_bag g)
 
-let add_eq ?(fast=(!fast_implementation)) u v b =
+let add_eq u v b =
   (* should we check to no add twice the same?? *)
   let m = b in
   let ru = repr u m in
@@ -512,19 +381,19 @@ let add_eq ?(fast=(!fast_implementation)) u v b =
     if SOF.mem u rv.gt_closure then
       error ("EQ",u,v) u "GT" v rv.gt_closure
     else
-      add_eq fast u v b
+      add_eq_arc_fast u v b
     end
 
-let add_ge ?(fast=(!fast_implementation)) u v b =
+let add_ge u v b =
   (* should we check to no add twice the same?? *)
   let m = b in
   let rv = repr v m in
   if SOF.mem u rv.gt_closure then
     error ("GE",u,v) u "GT" v rv.gt_closure
   else
-    add_ge fast u v b
+    add_ge_arc_fast u v b
   
-let add_gt ?(fast=(!fast_implementation)) u v b =
+let add_gt u v b =
   (* should we check to no add twice the same?? *)
   (* 
      FIXME : check the thesis... no need to check GT and EQ closure since the 
@@ -548,7 +417,7 @@ let add_gt ?(fast=(!fast_implementation)) u v b =
           if SOF.mem u rv.eq_closure then
             error ("GT",u,v) u "EQ" v rv.eq_closure
           else*)
-            add_gt fast u v b
+            add_gt_arc_fast u v b
 (*        end
     end*)
 
@@ -556,46 +425,37 @@ let add_gt ?(fast=(!fast_implementation)) u v b =
 (** START: Decomment this for performance comparisons                       **)
 (*****************************************************************************)
 
-let add_eq ?(fast=(!fast_implementation))  u v (b,already_contained,oblivion) =
+let add_eq u v (b,already_contained,oblivion) =
         if oblivion then (b,already_contained,oblivion) else
-  (*prerr_endline "add_eq";*)
-  (begin_spending ();
-  let rc = add_eq ~fast u v b in
-  end_spending ();
-    rc,already_contained,false)
+  let rc = add_eq u v b in
+    rc,already_contained,false
 
-let add_ge ?(fast=(!fast_implementation)) u v (b,already_contained,oblivion) =
+let add_ge u v (b,already_contained,oblivion) =
         if oblivion then (b,already_contained,oblivion) else
-(*   prerr_endline "add_ge"; *)
-  (begin_spending ();
-  let rc = add_ge ~fast u v b in
-  end_spending ();
-    rc,already_contained,false)
+  let rc = add_ge u v b in
+    rc,already_contained,false
     
-let add_gt ?(fast=(!fast_implementation)) u v (b,already_contained,oblivion) =
+let add_gt u v (b,already_contained,oblivion) =
         if oblivion then (b,already_contained,oblivion) else
-(*   prerr_endline "add_gt"; *)
-  (begin_spending ();
-  let rc = add_gt ~fast u v b in
-  end_spending ();
-    rc,already_contained,false)
+  let rc = add_gt u v b in
+    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"
-let add_gt ?fast u v b = 
-  profiler_gt.HExtlib.profile (fun _ -> add_gt ?fast u v b) ()
-let add_ge ?fast u v b = 
-  profiler_ge.HExtlib.profile (fun _ -> add_ge ?fast u v b) ()
-let add_eq ?fast u v b = 
-  profiler_eq.HExtlib.profile (fun _ -> add_eq ?fast u v b) ()
-*)
+let add_gt u v b = 
+  profiler_gt.HExtlib.profile (fun _ -> add_gt u v b) ()
+let add_ge u v b = 
+  profiler_ge.HExtlib.profile (fun _ -> add_ge u v b) ()
+let add_eq u v b = 
+  profiler_eq.HExtlib.profile (fun _ -> add_eq u v b) ()
+
 
 (* ugly *)
 let rank = ref MAL.empty;;
 
-let do_rank (b,_,_ as ugraph) =
+let do_rank (b,_,_) =
 (*         print_ugraph ugraph; *)
    let keys = MAL.fold (fun k _ acc -> k::acc) b [] in
    let fall =

diff --git a/helm/software/components/cic/cicUniv.mli b/helm/software/components/cic/cicUniv.mli
index fd501df8c47c4adfa320d90151ebc07b47c89e74..7b422583f53f361da3e247fb5717ac313eb7f70c 100644 (file)
--- a/helm/software/components/cic/cicUniv.mli
+++ b/helm/software/components/cic/cicUniv.mli
@@ -66,11 +66,11 @@ val oblivion_ugraph: universe_graph
   UniverseInconsistency
 *)
 val add_eq: 
-  ?fast:bool -> universe -> universe -> universe_graph -> universe_graph
+  universe -> universe -> universe_graph -> universe_graph
 val add_ge: 
-  ?fast:bool -> universe -> universe -> universe_graph -> universe_graph
+  universe -> universe -> universe_graph -> universe_graph
 val add_gt: 
-  ?fast:bool -> universe -> universe -> universe_graph -> universe_graph
+  universe -> universe -> universe_graph -> universe_graph
 
 val do_rank: universe_graph -> unit
 val get_rank: universe -> int
@@ -152,10 +152,4 @@ val assert_univ: universe -> unit
 val compare: universe -> universe -> int
 val eq: universe -> universe -> bool
 
-(*
-  Benchmarking stuff
-*)
-val get_spent_time: unit -> float
-val reset_spent_time: unit -> unit
-
 val is_anon: universe -> bool