aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2020-09-11 16:10:47 +0200
committerPierre-Marie Pédrot2020-09-17 16:12:33 +0200
commit60a55b1525cd02eb8fccae82d8dc2c2cd231664d (patch)
tree626f1e372a666aec2e9fa5c4c41cbf23f16d4931
parent1be09366e6d2dcf8b1257348c928727a66928760 (diff)
Be more efficient when generating the merge of ltle maps in AcyclicGraph.
We try to avoid reallocating the map in two different ways. - We only add a value when actually needed. - We compute the union of maps with the first element as a starting point.
-rw-r--r--lib/acyclicGraph.ml11
1 files changed, 7 insertions, 4 deletions
diff --git a/lib/acyclicGraph.ml b/lib/acyclicGraph.ml
index 82accd4c99..8da09dc98a 100644
--- a/lib/acyclicGraph.ml
+++ b/lib/acyclicGraph.ml
@@ -359,13 +359,16 @@ module Make (Point:Point) = struct
let ltle =
let fold acc n =
let fold u strict acc =
- if strict then PMap.add u strict acc
- else if PMap.mem u acc then acc
- else PMap.add u false acc
+ match PMap.find u acc with
+ | true -> acc
+ | false -> if strict then PMap.add u true acc else acc
+ | exception Not_found -> PMap.add u strict acc
in
PMap.fold fold n.ltle acc
in
- List.fold_left fold PMap.empty to_merge
+ match to_merge with
+ | [] -> assert false
+ | hd :: tl -> List.fold_left fold hd.ltle tl
in
let ltle, _ = clean_ltle g ltle in
let fold accu a =