From 2ed731db1107673f11de9b56a376bee41b4cf0be Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sat, 19 Apr 2008 16:27:28 +0000 Subject: [PATCH] ranking function fixed: when graphs are collapsed one step links are not updated (nor serialized to disk) thus you can not rely on them, just use the closures! --- helm/software/components/cic/cicUniv.ml | 21 +++++++++++---------- 1 file changed, 11 insertions(+), 10 deletions(-) diff --git a/helm/software/components/cic/cicUniv.ml b/helm/software/components/cic/cicUniv.ml index 699af7847..2bfbc92a3 100644 --- a/helm/software/components/cic/cicUniv.ml +++ b/helm/software/components/cic/cicUniv.ml @@ -595,26 +595,27 @@ let add_eq ?fast u v b = (* ugly *) let rank = ref MAL.empty;; -let do_rank (b,_,_) = - +let do_rank (b,_,_ as ugraph) = +(* print_ugraph ugraph; *) let keys = MAL.fold (fun k _ acc -> k::acc) b [] in let fall = List.fold_left (fun acc u -> - let rec aux seen = function + let rec aux k seen = function | [] -> 0, seen - | x::tl when SOF.mem x seen -> aux seen tl + | x::tl when SOF.mem x seen -> aux k seen tl | x::tl -> +(* prerr_endline (String.make k '.' ^ string_of_universe x); *) let seen = SOF.add x seen in - let t1, seen = aux seen (SOF.elements (repr x b).one_s_eq) in - let t2, seen = aux seen (SOF.elements (repr x b).one_s_ge) in - let t3, seen = aux seen (SOF.elements (repr x b).one_s_gt) in - let t4, seen = aux seen tl in + let t1, seen = aux (k+1) seen (SOF.elements (repr x b).eq_closure) in + let t3, seen = aux (k+1) seen (SOF.elements (repr x b).gt_closure) in + let t2, seen = aux (k+1) seen (SOF.elements (repr x b).ge_closure) in + let t4, seen = aux k seen tl in max (max t1 t2) - (max (if SOF.is_empty (repr x b).one_s_gt then 0 else t3+1) t4), + (max (if SOF.is_empty (repr x b).gt_closure then 0 else t3+1) t4), seen in - let rank, _ = aux SOF.empty [u] in + let rank, _ = aux 0 SOF.empty [u] in MAL.add u rank acc) MAL.empty in -- 2.39.2