let string_of_bag b =
string_of_mal b
-(*****************************************************************************)
-(** Helpers **)
-(*****************************************************************************)
-
-(* find the repr *)
-let repr u m =
- try
- MAL.find u m
- with
- Not_found -> empty_entry
-
-(* FIXME: May be faster if we make it by hand *)
-let merge_closures f nodes m =
- SOF.fold (fun x i -> SOF.union (f (repr x m)) i ) nodes SOF.empty
-
(*****************************************************************************)
(** Benchmarking **)
(*****************************************************************************)
partial := 0.0;
time_spent := !time_spent +. interval
;;
-
+
+
+(*****************************************************************************)
+(** Helpers **)
+(*****************************************************************************)
+
+(* find the repr *)
+let repr u m =
+ try
+ MAL.find u m
+ with
+ Not_found -> empty_entry
+
+(* FIXME: May be faster if we make it by hand *)
+let merge_closures f nodes m =
+ SOF.fold (fun x i -> SOF.union (f (repr x m)) i ) nodes SOF.empty
+
\f
(*****************************************************************************)
(** _fats implementation **)
raise (UniverseInconsistency s)
-let fill_empty_nodes_with_uri g l uri =
+let fill_empty_nodes_with_uri (g, already_contained) 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',l'
+ (m', already_contained),l'
(*****************************************************************************)
(** World interface **)
(*****************************************************************************)
-type universe_graph = bag
+type universe_graph = bag * UriManager.UriSet.t
+(* the graph , the cache of already merged ugraphs *)
-let empty_ugraph = empty_bag
+let empty_ugraph = empty_bag, UriManager.UriSet.empty
let current_index_anon = ref (-1)
let current_index_named = ref (-1)
| (i, None) -> (i, Some uri)
| _ -> u
-let print_ugraph g =
+let print_ugraph (g, _) =
prerr_endline (string_of_bag g)
let add_eq ?(fast=(!fast_implementation)) u v b =
(** START: Decomment this for performance comparisons **)
(*****************************************************************************)
-let add_eq ?(fast=(!fast_implementation)) u v b =
+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
+ end_spending ();
+ rc,already_contained
-let add_ge ?(fast=(!fast_implementation)) u v b =
+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
+ end_spending ();
+ rc,already_contained
-let add_gt ?(fast=(!fast_implementation)) u v b =
+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
+ end_spending ();
+ rc,already_contained
+
+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) ()
(*****************************************************************************)
(** END: Decomment this for performance comparisons **)
(*****************************************************************************)
-let merge_ugraphs u v =
- (* this sucks *)
- let merge_brutal u v =
- if u = empty_bag then v
- else if v = empty_bag then u
- else
- let m1 = u in
- let m2 = v in
- MAL.fold (
- fun k v x ->
- (SOF.fold (
- fun u x ->
- let m = add_gt k u x in m)
- (SOF.union v.one_s_gt v.gt_closure)
- (SOF.fold (
- fun u x ->
- let m = add_ge k u x in m)
- (SOF.union v.one_s_ge v.ge_closure)
- (SOF.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
+let merge_ugraphs ~base_ugraph ~increment:(increment, uri_of_increment) =
+ let merge_brutal (u,_) v =
+ let m1 = u in
+ let m2 = v in
+ MAL.fold (
+ fun k v x ->
+ (SOF.fold (
+ fun u x ->
+ let m = add_gt k u x in m)
+ (SOF.union v.one_s_gt v.gt_closure)
+ (SOF.fold (
+ fun u x ->
+ let m = add_ge k u x in m)
+ (SOF.union v.one_s_ge v.ge_closure)
+ (SOF.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
in
- merge_brutal v u
+ let base, already_contained = base_ugraph in
+ if MAL.is_empty base then
+ increment
+ else if
+ MAL.is_empty (fst increment) ||
+ 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"
+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";
let univno = fst
-let rec clean_ugraph m 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 ->
k::l end else l) m'' []
in
if e_l != [] then
- clean_ugraph m'' (fun u -> (f u) && not (List.mem u e_l))
+ clean_ugraph
+ (m'', already_contained) (fun u -> (f u) && not (List.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
+ m'' MAL.empty,
+ already_contained
let clean_ugraph g l =
clean_ugraph g (fun u -> List.mem u l)
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, !result_list
+ (!result_map,UriManager.UriSet.empty), !result_list
\f
(*****************************************************************************)
one_s_gt = recons_set entry.one_s_gt;
}
-let recons_graph graph =
+let recons_graph (graph,uriset) =
MAL.fold
(fun universe entry map ->
MAL.add (recons_univ universe) (recons_entry entry) map)
- graph MAL.empty
+ graph
+ MAL.empty,
+ UriManager.UriSet.fold
+ (fun u acc ->
+ UriManager.UriSet.add
+ (UriManager.uri_of_string (UriManager.string_of_uri u)) acc)
+ uriset UriManager.UriSet.empty
let assert_univ u =
match u with
| (_,None) -> raise (UniverseInconsistency "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