(** Types and default values **)
(*****************************************************************************)
+
type universe = int * UriManager.uri option
let eq u1 u2 =
print_endline ("Aggiusto " ^ (string_of_universe u) ^
"e ottengo questa chiusura\n " ^ (string_of_node ru))
-and adjust_fast_aux u m =
+and adjust_fast_aux adjusted u m =
+ if SOF.mem u adjusted then m, adjusted else
+ let adjusted = SOF.add u adjusted in
let ru = repr u m in
let gt_c = closure_gt_fast ru m in
let ge_c = closure_ge_fast ru m in
(not (are_set_eq ge_c ru.ge_closure))
in
if ((not changed_gegt) && (not changed_eq)) then
- m
+ m, adjusted
else
begin
let ru' = {
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_aux x m)
- (SOF.union ru'.eq_closure ru'.in_gegt_of) m
- (* TESI:
- ru'.in_gegt_of m
- *)
+ let m, adjusted =
+ SOF.fold (fun x (m,adjusted) -> MAL.add x ru' m, SOF.add x adjusted)
+ (SOF.diff ru'.eq_closure adjusted)
+ (m,adjusted)
+ in
+ let m, adjusted =
+ SOF.fold (fun x (m,adjusted) -> adjust_fast_aux adjusted x m)
+ (SOF.diff ru'.in_gegt_of adjusted)
+ (m,adjusted)
in
- m (*adjust_fast u m*)
+ m, adjusted
end
(*
and profiler_adj = HExtlib.profile "CicUniv.adjust_fast"
and adjust_fast x y = profiler_adj.HExtlib.profile (adjust_fast_aux x) y
*)
-and adjust_fast x y = adjust_fast_aux x y
+and adjust_fast x y =
+ fst(adjust_fast_aux SOF.empty x y)
and add_gt_arc_fast u v m =
let ru = repr u m in