+ redo_ge_closure (SOF.remove u todo) m s
+ end
+
+(*
+ calculates the closures of u and adjusts the in_*_of of v, then
+ starts redo_*_closure to adjust the colure of nodew thet have
+ (clusure u) in theyr closures
+*)
+let add_ge_arc u v m =
+ let ru = repr u m in
+ let rv = repr v m in
+ let ru' = {
+ eq_closure = ru.eq_closure;
+ ge_closure = SOF.add v
+ (SOF.union ru.ge_closure
+ (SOF.union rv.eq_closure rv.ge_closure));
+ gt_closure = ru.gt_closure;
+ in_eq_of = ru.in_eq_of;
+ in_ge_of = ru.in_ge_of;
+ in_gt_of = ru.in_gt_of;
+ one_s_eq = ru.one_s_eq;
+ one_s_ge = SOF.add v ru.one_s_ge;
+ one_s_gt = ru.one_s_gt;
+ } in
+ let rv' = { rv with in_gt_of = SOF.add u rv.in_ge_of } in
+ let m' = MAL.add u ru' m in
+ let m'' = MAL.add v rv' m' in
+ let m''',td = redo_ge_closure ru'.in_ge_of m'' SOF.empty in
+ (* closing ge may provoke aome changes in gt-closures *)
+ redo_gt_closure (SOF.union ru'.in_gt_of
+ (SOF.fold (fun u s -> SOF.union s ((repr u m''').in_gt_of))
+ td SOF.empty )) m''' SOF.empty
+
+(*
+ given the 2 nodes plus the current bag, adds the arc, recomputes the
+ closures and returns the new map
+*)
+let add_ge u v b =
+ let m,l = b in
+ let m' = add_ge_arc u v m in
+ let l' = (GE,u,v)::l in
+ (m',l')
+
+(******************************************************************************)
+(** Real stuff EQ **)
+(******************************************************************************)
+
+let rec redo_eq_closure todo m s =
+ if SOF.is_empty todo then m,s
+ else begin
+ let u = SOF.choose todo in
+ if not (SOF.mem u s) then
+ begin
+ let ru = repr u m in
+ let eq_closure = merge_closures
+ (fun x -> x.eq_closure) ru.one_s_eq m in
+ let ru' = {ru with eq_closure = eq_closure
+ ; in_eq_of = eq_closure ; one_s_eq = eq_closure } in
+ let m' = MAL.add u ru' m in
+ let s' = SOF.add u s in
+ redo_eq_closure (SOF.union (SOF.remove u todo) ru'.in_eq_of) m' s'
+ end
+ else
+ redo_eq_closure (SOF.remove u todo) m s
+ end
+
+(*
+ calculates the closures of u and adjusts the in_*_of of v, then
+ starts redo_*_closure to adjust the colure of nodew thet have
+ (clusure u) in theyr closures
+*)
+let add_eq_arc u v m =
+ let ru = repr u m in
+ let rv = repr v m in
+ (* since eq is symmetric we have to chage more *)
+ let eq_closure = SOF.add u (SOF.add v
+ (SOF.union ru.eq_closure rv.eq_closure)) in
+ let ru' = {
+ eq_closure = eq_closure;
+ ge_closure = SOF.union ru.ge_closure rv.ge_closure;
+ gt_closure = SOF.union ru.gt_closure rv.gt_closure;
+ in_eq_of = eq_closure;
+ in_ge_of = SOF.union ru.in_ge_of rv.in_ge_of;
+ in_gt_of = SOF.union ru.in_gt_of rv.in_gt_of;
+ one_s_eq = eq_closure;
+ one_s_ge = SOF.union ru.one_s_ge rv.one_s_ge;
+ one_s_gt = SOF.union ru.one_s_gt rv.one_s_gt;
+ } in
+ (* this is a collapse *)
+ let rv' = ru' in
+ let m' = MAL.add u ru' m in
+ let m'' = MAL.add v rv' m' in
+ let m''',td = redo_eq_closure ru'.in_eq_of m'' SOF.empty in
+ (* redoing a eq may change some ge and some gt *)
+ let m'''',td' = redo_ge_closure
+ (SOF.union ru'.in_ge_of
+ (SOF.fold (fun u s -> SOF.union s ((repr u m''').in_ge_of))
+ td SOF.empty)) m''' SOF.empty in
+ redo_gt_closure (SOF.union ru'.in_gt_of
+ (SOF.fold (fun u s -> SOF.union s ((repr u m'''').in_gt_of))
+ td' SOF.empty)) m'''' SOF.empty
+
+(*
+ given the 2 nodes plus the current bag, adds the arc, recomputes the
+ closures and returns the new map
+*)
+let add_eq u v b =
+ let m,l = b in
+ let m' = add_eq_arc u v m in
+ let l' = (EQ,u,v)::l in
+ (m',l')
+
+(******************************************************************************)
+(** Oyther real code **)
+(******************************************************************************)
+
+exception UniverseInconsistency of string
+
+let error arc node1 closure_type node2 closure =
+ let s = " ===== Universe Inconsistency detected =====\n\n" ^
+ "\tUnable to add ("^ (string_of_arc arc) ^ ") cause " ^
+ (string_of_universe node1) ^ " is in the " ^
+ (string_of_arc_type closure_type) ^ " closure {" ^
+ (string_of_universe_set closure) ^ "} of " ^
+ (string_of_universe node2) ^ "\n\n" ^
+ " ===== Universe Inconsistency detected =====\n" in
+ prerr_endline s;
+ raise (UniverseInconsistency s)
+
+(*
+ we merge the env_bag with b
+*)
+let qed b =
+ let m,l = b in
+ let m',l' = !env_bag in
+ let m'' = ref m' in
+ MAL.iter (fun k v -> m'':= MAL.add k v !m'') m;
+ let l'' = l @ l' in
+ env_bag := (!m'',l'')
+
+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
+ 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 u v b
+ end
+
+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 u v b
+
+let add_gt 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 (GT,u,v) u GT v rv.gt_closure
+ else
+ begin
+ if SOF.mem u rv.ge_closure then
+ error (GT,u,v) u GE v rv.ge_closure