- close_ge_aux repr_u.ge []
-
-(* all the nodes we can ifer in the gt list of u,
- we must follow bot gt and ge arcs, but we must put in bag only
- the nodes that have a gt in theys path
-*)
-let close_gt u =
- let repr_u = repr u in
- let rec close_gt_aux bag todo inspected =
- (*print_all bag todo;Unix.sleep 1;*)
- match todo with
- [],[] -> bag
- | [],p::may -> let repr_p = repr p in
- if List.mem repr_p.u inspected then (* avoid loops *)
- close_gt_aux bag ([],may) inspected
- else
- close_gt_aux bag (repr_p.gt,repr_p.ge @ may)
- (repr_p.u::inspected)
- | s::secure,may -> let repr_s = repr s in
- if List.mem repr_s.u inspected then (* avoid loops *)
- if List.mem repr_s bag then
- close_gt_aux bag (secure,may) inspected
- else
- (* even if we ave already inspected the node, now
- it is in the secure list so we want it in the bag
- *)
- close_gt_aux (repr_s::bag) (secure,may) inspected
- else
- close_gt_aux ((repr_s)::bag)
- (repr_s.gt @ repr_s.ge,may) (repr_s.u::inspected)
+ if ((not changed_gegt) && (not changed_eq)) then
+ m
+ else
+ begin
+ let ru' = {
+ 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}
+ in
+ let m = MAL.add u ru' m in
+ let m =
+ SOF.fold (fun x m -> adjust_fast x m)
+ (SOF.union ru'.eq_closure ru'.in_gegt_of) m
+ (* TESI:
+ ru'.in_gegt_of m
+ *)
+ in
+ m (*adjust_fast u m*)
+ end
+
+and add_gt_arc_fast 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
+ let rv = repr v m' in
+ let rv' = {rv with in_gegt_of = SOF.add u rv.in_gegt_of} in
+ let m'' = MAL.add v rv' m' in
+ adjust_fast u m''
+
+and add_ge_arc_fast 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
+ let rv = repr v m' in
+ let rv' = {rv with in_gegt_of = SOF.add u rv.in_gegt_of} in
+ let m'' = MAL.add v rv' m' in
+ adjust_fast u m''
+
+and add_eq_arc_fast 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
+ (*TESI: let ru' = {ru' with in_gegt_of = SOF.add v ru.in_gegt_of} in *)
+ let m' = MAL.add u ru' m in
+ let rv' = {rv with one_s_eq = SOF.add u rv.one_s_eq} in
+ (*TESI: let rv' = {rv' with in_gegt_of = SOF.add u rv.in_gegt_of} in *)
+ let m'' = MAL.add v rv' m' in
+ adjust_fast v (*(adjust_fast u*) 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 **)
+(*****************************************************************************)
+
+exception UniverseInconsistency of string
+
+let error arc node1 closure_type node2 closure =
+ let s = "\n ===== Universe Inconsistency detected =====\n\n" ^
+ " Unable to add\n" ^
+ "\t" ^ (string_of_arc arc) ^ "\n" ^
+ " cause\n" ^
+ "\t" ^ (string_of_universe node1) ^ "\n" ^
+ " is in the " ^ closure_type ^ " closure\n" ^
+ "\t{" ^ (string_of_universe_set closure) ^ "}\n" ^
+ " of\n" ^
+ "\t" ^ (string_of_universe node2) ^ "\n\n" ^
+ " ===== Universe Inconsistency detected =====\n" in
+ prerr_endline s;
+ raise (UniverseInconsistency s)
+
+
+let fill_empty_nodes_with_uri g l uri =
+ let fill_empty_universe u =
+ match u with
+ (i,None) -> (i,Some uri)
+ | (i,Some _) as u -> u
+ in
+ let fill_empty_set s =
+ SOF.fold (fun e s -> SOF.add (fill_empty_universe e) s) s SOF.empty
+ in
+ let fill_empty_entry e = {
+ eq_closure = (fill_empty_set e.eq_closure) ;
+ ge_closure = (fill_empty_set e.ge_closure) ;
+ gt_closure = (fill_empty_set e.gt_closure) ;
+ in_gegt_of = (fill_empty_set e.in_gegt_of) ;
+ one_s_eq = (fill_empty_set e.one_s_eq) ;
+ one_s_ge = (fill_empty_set e.one_s_ge) ;
+ one_s_gt = (fill_empty_set e.one_s_gt) ;
+ } in
+ let m = g in
+ let m' = MAL.fold (
+ fun k v m ->
+ MAL.add (fill_empty_universe k) (fill_empty_entry v) m) m MAL.empty
+ in
+ let l' = List.map fill_empty_universe l in
+ m',l'
+
+
+(*****************************************************************************)
+(** World interface **)
+(*****************************************************************************)
+
+type universe_graph = bag
+
+let empty_ugraph = empty_bag
+
+let current_index_anon = ref (-1)
+let current_index_named = ref (-1)
+
+let restart_numbering () = current_index_named := (-1)
+
+let fresh ?uri ?id () =
+ let i =
+ match uri,id with
+ | None,None ->
+ current_index_anon := !current_index_anon + 1;
+ !current_index_anon
+ | None, Some _ -> assert false
+ | Some _, None ->
+ current_index_named := !current_index_named + 1;
+ !current_index_named
+ | Some _, Some id -> id