+ 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 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
+ m'
+
+
+(*****************************************************************************)
+(** 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 () =
+ let i =
+ match uri with
+ | None ->
+ current_index_anon := !current_index_anon + 1;
+ !current_index_anon
+ | Some _ ->
+ current_index_named := !current_index_named + 1;
+ !current_index_named
+ in
+ (i,uri)
+
+let print_ugraph g =
+ prerr_endline (string_of_bag g)
+
+let add_eq ?(fast=(!fast_implementation)) u v b =
+ (* should we check to no add twice the same?? *)
+ let m = b in
+ let ru = repr u m in
+ if SOF.mem v ru.gt_closure then
+ error ("EQ",u,v) v "GT" u ru.gt_closure
+ else
+ begin
+ let rv = repr v m in
+ 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
+ end
+
+let add_ge ?(fast=(!fast_implementation)) 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
+
+let add_gt ?(fast=(!fast_implementation)) 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
+ GE is a superset of both
+ *)
+ let m = b in
+ let rv = repr v m in
+
+ if u = v then
+ error ("GT",u,v) u "==" v SOF.empty
+ else