(* $Id$ *)
-(*****************************************************************************)
-(** switch implementation **)
-(*****************************************************************************)
-
-let fast_implementation = ref true ;;
-
(*****************************************************************************)
(** open **)
(*****************************************************************************)
(** Types and default values **)
(*****************************************************************************)
+
type universe = int * UriManager.uri option
-
+
+let eq u1 u2 =
+ match u1,u2 with
+ | (id1, Some uri1),(id2, Some uri2) ->
+ id1 = id2 && UriManager.eq uri1 uri2
+ | (id1, None),(id2, None) -> id1 = id2
+ | _ -> false
+
+let compare (id1, uri1) (id2, uri2) =
+ let cmp = id1 - id2 in
+ if cmp = 0 then
+ match uri1,uri2 with
+ | None, None -> 0
+ | Some _, None -> 1
+ | None, Some _ -> ~-1
+ | Some uri1, Some uri2 -> UriManager.compare uri1 uri2
+ else
+ cmp
+
module UniverseType = struct
type t = universe
- let compare = Pervasives.compare
+ let compare = compare
end
module SOF = Set.Make(UniverseType)
let string_of_bag b =
string_of_mal b
-(*****************************************************************************)
-(** Benchmarking **)
-(*****************************************************************************)
-let time_spent = ref 0.0;;
-let partial = ref 0.0 ;;
-
-let reset_spent_time () = time_spent := 0.0;;
-let get_spent_time () = !time_spent ;;
-let begin_spending () =
- (*assert (!partial = 0.0);*)
- partial := Unix.gettimeofday ()
-;;
-
-let end_spending () =
- assert (!partial > 0.0);
- let interval = (Unix.gettimeofday ()) -. !partial in
- partial := 0.0;
- time_spent := !time_spent +. interval
-;;
-
-
(*****************************************************************************)
(** Helpers **)
(*****************************************************************************)
print_endline ("Aggiusto " ^ (string_of_universe u) ^
"e ottengo questa chiusura\n " ^ (string_of_node ru))
-and adjust_fast 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 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 =
+ fst(adjust_fast_aux SOF.empty x y)
and add_gt_arc_fast u v m =
let ru = repr u m in
+ if SOF.mem v ru.gt_closure then m else
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
and add_ge_arc_fast u v m =
let ru = repr u m in
+ if SOF.mem v ru.ge_closure then m else
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
and add_eq_arc_fast u v m =
let ru = repr u m in
+ if SOF.mem v ru.eq_closure then m else
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 *)
;;
\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
+exception UniverseInconsistency of string Lazy.t
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;
+ let s =
+ lazy
+ ("\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 (Lazy.force s); *)
raise (UniverseInconsistency s)
-let fill_empty_nodes_with_uri (g, already_contained) l uri =
+let fill_empty_nodes_with_uri (g, already_contained,o) l uri =
let fill_empty_universe u =
match u with
(i,None) -> (i,Some uri)
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', already_contained),l'
+ (m', already_contained,o),l'
(*****************************************************************************)
(** World interface **)
(*****************************************************************************)
-type universe_graph = bag * UriManager.UriSet.t
-(* the graph , the cache of already merged ugraphs *)
+type universe_graph = bag * UriManager.UriSet.t * bool
+(* the graph , the cache of already merged ugraphs, oblivion? *)
-let empty_ugraph = empty_bag, UriManager.UriSet.empty
+let empty_ugraph = empty_bag, UriManager.UriSet.empty, false
+let oblivion_ugraph = empty_bag, UriManager.UriSet.empty, true
+(* FG: default choice for a ugraph ??? *)
+let default_ugraph = oblivion_ugraph
let current_index_anon = ref (-1)
let current_index_named = ref (-1)
let name_universe u uri =
match u with
| (i, None) -> (i, Some uri)
- | _ -> u
+ | u -> u
+;;
-let print_ugraph (g, _) =
+let print_ugraph (g, _, o) =
+ if o then prerr_endline "oblivion universe" else
prerr_endline (string_of_bag g)
-let add_eq ?(fast=(!fast_implementation)) u v b =
+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 u rv.gt_closure then
error ("EQ",u,v) u "GT" v rv.gt_closure
else
- add_eq fast u v b
+ add_eq_arc_fast u v b
end
-let add_ge ?(fast=(!fast_implementation)) u v b =
+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 fast u v b
+ add_ge_arc_fast u v b
-let add_gt ?(fast=(!fast_implementation)) u v b =
+let add_gt 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
if SOF.mem u rv.eq_closure then
error ("GT",u,v) u "EQ" v rv.eq_closure
else*)
- add_gt fast u v b
+ add_gt_arc_fast u v b
(* end
end*)
(** START: Decomment this for performance comparisons **)
(*****************************************************************************)
-let add_eq ?(fast=(!fast_implementation)) u v (b,already_contained) =
- (*prerr_endline "add_eq";*)
- begin_spending ();
- let rc = add_eq ~fast u v b in
- end_spending ();
- rc,already_contained
-
-let add_ge ?(fast=(!fast_implementation)) u v (b,already_contained) =
-(* prerr_endline "add_ge"; *)
- begin_spending ();
- let rc = add_ge ~fast u v b in
- end_spending ();
- rc,already_contained
+let add_eq u v (b,already_contained,oblivion) =
+ if oblivion then (b,already_contained,oblivion) else
+ let rc = add_eq u v b in
+ rc,already_contained,false
+
+let add_ge u v (b,already_contained,oblivion) =
+ if oblivion then (b,already_contained,oblivion) else
+ let rc = add_ge u v b in
+ rc,already_contained,false
-let add_gt ?(fast=(!fast_implementation)) u v (b,already_contained) =
-(* prerr_endline "add_gt"; *)
- begin_spending ();
- let rc = add_gt ~fast u v b in
- end_spending ();
- rc,already_contained
+let add_gt u v (b,already_contained,oblivion) =
+ if oblivion then (b,already_contained,oblivion) else
+ let rc = add_gt u v b in
+ rc,already_contained,false
+(* profiling code *)
let profiler_eq = HExtlib.profile "CicUniv.add_eq"
let profiler_ge = HExtlib.profile "CicUniv.add_ge"
let profiler_gt = HExtlib.profile "CicUniv.add_gt"
-let add_gt ?fast u v b =
- profiler_gt.HExtlib.profile (fun _ -> add_gt ?fast u v b) ()
-let add_ge ?fast u v b =
- profiler_ge.HExtlib.profile (fun _ -> add_ge ?fast u v b) ()
-let add_eq ?fast u v b =
- profiler_eq.HExtlib.profile (fun _ -> add_eq ?fast u v b) ()
+let add_gt u v b =
+ profiler_gt.HExtlib.profile (fun _ -> add_gt u v b) ()
+let add_ge u v b =
+ profiler_ge.HExtlib.profile (fun _ -> add_ge u v b) ()
+let add_eq u v b =
+ profiler_eq.HExtlib.profile (fun _ -> add_eq u v b) ()
+
+
+(* ugly *)
+let rank = ref MAL.empty;;
+
+let do_rank (b,_,_) =
+ let keys =
+ MAL.fold
+ (fun k v acc ->
+ SOF.union acc (SOF.union (SOF.singleton k)
+ (SOF.union v.eq_closure (SOF.union v.gt_closure v.ge_closure))))
+ b SOF.empty
+ in
+ let keys = SOF.elements keys in
+ let rec aux cache l =
+ match l with
+ | [] -> -1,cache
+ | x::tl when List.mem_assoc x cache ->
+ let height = List.assoc x cache in
+ let rest, cache = aux cache tl in
+ max rest height, cache
+ | x::tl ->
+ let sons = SOF.elements (repr x b).gt_closure in
+ let height,cache = aux cache sons in
+ let height = height + 1 in
+ let cache = (x,height) :: cache in
+ let rest, cache = aux cache tl in
+ max height rest, cache
+ in
+ let _, cache = aux [] keys in
+ rank := List.fold_left (fun m (k,v) -> MAL.add k v m) MAL.empty cache;
+ let res = ref [] in
+ let resk = ref [] in
+ MAL.iter
+ (fun k v ->
+ if not (List.mem v !res) then res := v::!res;
+ resk := k :: !resk) !rank;
+ !res, !resk
+;;
+
+let get_rank u =
+ try MAL.find u !rank
+ with Not_found -> 0
+ (* if the universe is not in the graph it means there are
+ * no contraints on it! thus it can be freely set to Type0 *)
+;;
(*****************************************************************************)
(** END: Decomment this for performance comparisons **)
(*****************************************************************************)
-let merge_ugraphs ~base_ugraph ~increment:(increment, uri_of_increment) =
- let merge_brutal (u,_) v =
+(* TODO: uncomment l to gain a small speedup *)
+let merge_ugraphs ~base_ugraph ~increment:(increment, uri_of_increment(*,l*)) =
+ let merge_brutal (u,a,_) v =
+(* prerr_endline ("merging graph: "^UriManager.string_of_uri
+ * uri_of_increment); *)
let m1 = u in
let m2 = v in
MAL.fold (
fun u x ->
let m = add_eq k u x in m)
(SOF.union v.one_s_eq v.eq_closure) x)))
- ) m1 m2
+ ) m1 m2
in
- let base, already_contained = base_ugraph in
- if MAL.is_empty base then
+ let base, already_contained, oblivion = base_ugraph in
+ let inc,_,oblivion2 = increment in
+ if oblivion then
+ base_ugraph
+ else if oblivion2 then
+ increment
+ else if MAL.is_empty base then
increment
else if
- MAL.is_empty (fst increment) ||
+ MAL.is_empty inc ||
UriManager.UriSet.mem uri_of_increment already_contained
then
base_ugraph
- else
- fst (merge_brutal increment base_ugraph),
- UriManager.UriSet.add uri_of_increment already_contained
-
-let profiler_merge = HExtlib.profile "CicUniv.merge_graphs"
+ else
+ (fun (x,_,_) -> x) (merge_brutal increment base_ugraph),
+(*
+ List.fold_right UriManager.UriSet.add
+ (List.map (fun (_,x) -> HExtlib.unopt x) l)
+*)
+ (UriManager.UriSet.add uri_of_increment already_contained), false
+
+(* profiling code; WARNING: the time spent during profiling can be
+ greater than the profiled time
+let profiler_merge = HExtlib.profile "CicUniv.merge_ugraphs"
let merge_ugraphs ~base_ugraph ~increment =
profiler_merge.HExtlib.profile
(fun _ -> merge_ugraphs ~base_ugraph ~increment) ()
+*)
(*****************************************************************************)
(** Xml sesialization and parsing **)
let content = xml_of_entry_content e in
ent content
-let write_xml_of_ugraph filename (m,_) l =
+let write_xml_of_ugraph filename (m,_,_) l =
let tokens =
[<
Xml.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n";
Xml.pp ~gzip:true tokens (Some filename)
let univno = fst
+let univuri = function
+ | _,None -> UriManager.uri_of_string "cic:/fake.con"
+ | _,Some u -> u
-let rec clean_ugraph (m,already_contained) f =
+let rec clean_ugraph m already_contained f =
let m' =
MAL.fold (fun k v x -> if (f k) then MAL.add k v x else x ) m MAL.empty in
let m'' = MAL.fold (fun k v x ->
let e_l =
MAL.fold (fun k v l -> if v = empty_entry && not(f k) then
begin
- k::l end else l) m'' []
+ SOF.add k l end else l) m'' SOF.empty
in
- if e_l != [] then
+ if not (SOF.is_empty e_l) then
clean_ugraph
- (m'', already_contained) (fun u -> (f u) && not (List.mem u e_l))
+ m'' already_contained (fun u -> (f u) && not (SOF.mem u e_l))
else
MAL.fold
(fun k v x -> if v <> empty_entry then MAL.add k v x else x)
m'' MAL.empty,
already_contained
-let clean_ugraph g l =
- clean_ugraph g (fun u -> List.mem u l)
+let clean_ugraph (m,a,o) l =
+ assert(not o);
+ let l = List.fold_right SOF.add l SOF.empty in
+ let m, a = clean_ugraph m a (fun u -> SOF.mem u l) in
+ m, a, o
let assigner_of =
function
let xml_source = `Gzip_file filename in
(try XPP.parse xml_parser xml_source
with (XPP.Parse_error err) as exn -> raise exn);
- (!result_map,UriManager.UriSet.empty), !result_list
+ (!result_map,UriManager.UriSet.empty,false), !result_list
\f
(*****************************************************************************)
one_s_gt = recons_set entry.one_s_gt;
}
-let recons_graph (graph,uriset) =
+let recons_graph (graph,uriset,o) =
MAL.fold
(fun universe entry map ->
MAL.add (recons_univ universe) (recons_entry entry) map)
(fun u acc ->
UriManager.UriSet.add
(UriManager.uri_of_string (UriManager.string_of_uri u)) acc)
- uriset UriManager.UriSet.empty
+ uriset UriManager.UriSet.empty, o
let assert_univ u =
match u with
- | (_,None) -> raise (UniverseInconsistency "This universe graph has a hole")
+ | (_,None) ->
+ raise (UniverseInconsistency (lazy "This universe graph has a hole"))
| _ -> ()
-let assert_univs_have_uri (graph,_) univlist =
+let assert_univs_have_uri (graph,_,_) univlist =
let assert_set s =
SOF.iter (fun u -> assert_univ u) s
in
MAL.iter (fun k v -> assert_univ k; assert_entry v)graph;
List.iter assert_univ univlist
-let eq u1 u2 =
- match u1,u2 with
- | (id1, Some uri1),(id2, Some uri2) ->
- id1 = id2 && UriManager.eq uri1 uri2
- | (id1, None),(id2, None) -> id1 = id2
- | _ -> false
-
-let compare (id1, uri1) (id2, uri2) =
- let cmp = id1 - id2 in
- if cmp = 0 then
- match uri1,uri2 with
- | None, None -> 0
- | Some _, None -> 1
- | None, Some _ -> ~-1
- | Some uri1, Some uri2 -> UriManager.compare uri1 uri2
- else
- cmp
+let is_anon = function (_,None) -> true | _ -> false
(* EOF *)
projects / helm.git / blobdiff