From 1be09366e6d2dcf8b1257348c928727a66928760 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 11 Sep 2020 15:33:52 +0200
Subject: Do not allocate intermediate sets in universe refreshing.

A set was created only to be folded over. Since the list is ensured to
be duplicate-free, there is no point in creating the former, we just
fold over the list directly.
---
 lib/acyclicGraph.ml | 33 ++++++++++++++-------------------
 1 file changed, 14 insertions(+), 19 deletions(-)

(limited to 'lib')

diff --git a/lib/acyclicGraph.ml b/lib/acyclicGraph.ml
index dc5241b89e..82accd4c99 100644
--- a/lib/acyclicGraph.ml
+++ b/lib/acyclicGraph.ml
@@ -356,12 +356,8 @@ module Make (Point:Point) = struct
 
   let get_new_edges g to_merge =
     (* Computing edge sets. *)
-    let to_merge_lvl =
-      List.fold_left (fun acc u -> PMap.add u.canon u acc)
-        PMap.empty to_merge
-    in
     let ltle =
-      let fold _ n acc =
+      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
@@ -369,26 +365,25 @@ module Make (Point:Point) = struct
         in
         PMap.fold fold n.ltle acc
       in
-      PMap.fold fold to_merge_lvl PMap.empty
+      List.fold_left fold PMap.empty to_merge
     in
     let ltle, _ = clean_ltle g ltle in
-    let ltle =
-      PMap.merge (fun _ a strict ->
-          match a, strict with
-          | Some _, Some true ->
-            (* There is a lt edge inside the new component. This is a
-                "bad cycle". *)
-            raise CycleDetected
-          | Some _, Some false -> None
-          | _, _ -> strict
-        ) to_merge_lvl ltle
+    let fold accu a =
+      match PMap.find a.canon ltle with
+      | true ->
+        (* There is a lt edge inside the new component. This is a
+            "bad cycle". *)
+        raise CycleDetected
+      | false -> PMap.remove a.canon accu
+      | exception Not_found -> accu
     in
+    let ltle = List.fold_left fold ltle to_merge in
     let gtge =
-      PMap.fold (fun _ n acc -> PSet.union acc n.gtge)
-        to_merge_lvl PSet.empty
+      List.fold_left (fun acc n -> PSet.union acc n.gtge)
+        PSet.empty to_merge
     in
     let gtge, _ = clean_gtge g gtge in
-    let gtge = PSet.diff gtge (PMap.domain to_merge_lvl) in
+    let gtge = List.fold_left (fun acc n -> PSet.remove n.canon acc) gtge to_merge in
     (ltle, gtge)
 
 
-- 
cgit v1.2.3


From 60a55b1525cd02eb8fccae82d8dc2c2cd231664d Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 11 Sep 2020 16:10:47 +0200
Subject: 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.
---
 lib/acyclicGraph.ml | 11 +++++++----
 1 file changed, 7 insertions(+), 4 deletions(-)

(limited to 'lib')

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 =
-- 
cgit v1.2.3