From: Kim Nguyễn <kn@lri.fr>
Date: Sat, 27 Jul 2013 14:32:26 +0000 (+0200)
Subject: Lowlevel optimizations in the Ptset module, replace some function
X-Git-Tag: v0.1~51
X-Git-Url: http://git.nguyen.vg/gitweb/?p=tatoo.git;a=commitdiff_plain;h=cd25399e8ac95c48630a18000e797062db66be05

Lowlevel optimizations in the Ptset module, replace some function
calls by a field access, use bit twidling hack to compute the
largest power of two inferior to a given value (was previously done
with log(WORDSIZE * 8) branching + table lookup).
---

diff --git a/src/misc.ml b/src/misc.ml
index dc14fdd..743dda8 100644
--- a/src/misc.ml
+++ b/src/misc.ml
@@ -25,7 +25,7 @@ struct
   type t = data T.t
   let create = T.create
   let add h v = T.add h v v
-  let find = T.find
+  let find h v = T.find h v
   let remove = T.remove
   let find_all = T.find_all
   let clear = T.clear
diff --git a/src/ptset.ml b/src/ptset.ml
index 9d415f8..87ca2a5 100644
--- a/src/ptset.ml
+++ b/src/ptset.ml
@@ -61,7 +61,7 @@ struct
 
   let empty = Node.make Empty
 
-  let is_empty s = (Node.node s) == Empty
+  let is_empty s = s.Node.node == Empty
 
   let branch p m l r = Node.make (Branch(p,m,l,r))
 
@@ -75,117 +75,111 @@ struct
 
                             (******** from here on, only use the smart constructors ************)
 
-  let zero_bit k m = (k land m) == 0
-
   let singleton k = leaf k
 
   let is_singleton n =
-    match Node.node n with
+    match n.Node.node with
       | Leaf _ -> true
       | Branch _ | Empty -> false
 
   let mem (k:elt) n =
-    let kid = Uid.to_int (H.uid k) in
-    let rec loop n = match Node.node n with
+    let kid = (H.uid k :> int) in
+    let rec loop n = match n.Node.node with
     | Empty -> false
     | Leaf j ->  k == j
-    | Branch (p, _, l, r) -> if kid <= p then loop l else loop r
+    | Branch (p, _, l, r) -> loop (if kid <= p then l else r)
     in loop n
 
-  let rec min_elt n = match Node.node n with
+  let rec min_elt n = match n.Node.node with
   | Empty -> raise Not_found
   | Leaf k -> k
   | Branch (_,_,s,_) -> min_elt s
 
-  let rec max_elt n = match Node.node n with
+  let rec max_elt n = match n.Node.node with
   | Empty -> raise Not_found
   | Leaf k -> k
   | Branch (_,_,_,t) -> max_elt t
 
   let elements s =
-    let rec elements_aux acc n = match Node.node n with
+    let rec elements_aux acc n = match n.Node.node with
     | Empty -> acc
     | Leaf k -> k :: acc
     | Branch (_,_,l,r) -> elements_aux (elements_aux acc r) l
     in
     elements_aux [] s
 
+
+  let zero_bit k m = (k land m) == 0
+
   let mask k m  = (k lor (m-1)) land (lnot m)
 
-  let naive_highest_bit x =
-    assert (x < 256);
-    let rec loop i =
-      if i = 0 then 1 else if x lsr i = 1 then 1 lsl i else loop (i-1)
-    in
-    loop 7
-
-  let hbit = Array.init 256 naive_highest_bit
-  (*
-    external clz : int -> int = "caml_clz" "noalloc"
-    external leading_bit : int -> int = "caml_leading_bit" "noalloc"
-  *)
-  let highest_bit x =
-    try
-      let n = (x) lsr 24 in
-      if n != 0 then  hbit.(n) lsl 24
-      else let n = (x) lsr 16 in if n != 0 then hbit.(n) lsl 16
-        else let n = (x) lsr 8 in if n != 0 then hbit.(n) lsl 8
-          else hbit.(x)
-    with
-      _ -> raise (Invalid_argument ("highest_bit " ^ (string_of_int x)))
-
-  let highest_bit64 x =
-    let n = x lsr 32 in if n != 0 then highest_bit n lsl 32
-      else highest_bit x
-
-  let branching_bit p0 p1 = highest_bit64 (p0 lxor p1)
+  external int_of_bool : bool -> int = "%identity"
+
+  let hb32 v0 =
+    let v = v0 lor (v0 lsr 1) in
+    let v = v lor (v lsr 2) in
+    let v = v lor (v lsr 4) in
+    let v = v lor (v lsr 8) in
+    let v = v lor (v lsr 16) in
+    ((v + 1) lsr 1) + (int_of_bool (v0 == 0))
+
+  let hb64 v0 =
+    let v = v0 lor (v0 lsr 1) in
+    let v = v lor (v lsr 2) in
+    let v = v lor (v lsr 4) in
+    let v = v lor (v lsr 8) in
+    let v = v lor (v lsr 16) in
+    let v = v lor (v lsr 32) in
+    ((v + 1) lsr 1) + (int_of_bool (v0 == 0))
+
+
+  let branching_bit p0 p1 = hb64 (p0 lxor p1)
 
   let join p0 t0 p1 t1 =
     let m = branching_bit p0 p1  in
     let msk = mask p0 m in
     if zero_bit p0 m then
-    branch_ne msk m t0 t1
+      branch_ne msk m t0 t1
     else
-    branch_ne msk m t1 t0
+      branch_ne msk m t1 t0
 
   let match_prefix k p m = (mask k m) == p
 
   let add k t =
     let kid = Uid.to_int (H.uid k) in
-    assert (kid >=0);
-    let rec ins n = match Node.node n with
+    let rec ins n = match n.Node.node with
     | Empty -> leaf k
     | Leaf j ->  if j == k then n else join kid (leaf k) (Uid.to_int (H.uid j)) n
     | Branch (p,m,t0,t1)  ->
         if match_prefix kid p m then
-        if zero_bit kid m then
-        branch_ne p m (ins t0) t1
+          if zero_bit kid m then
+            branch_ne p m (ins t0) t1
+          else
+            branch_ne p m t0 (ins t1)
         else
-        branch_ne p m t0 (ins t1)
-        else
-        join kid (leaf k)  p n
+          join kid (leaf k)  p n
     in
     ins t
 
   let remove k t =
-    let kid = Uid.to_int(H.uid k) in
-    let rec rmv n = match Node.node n with
+    let kid = (H.uid k :> int) in
+    let rec rmv n = match n.Node.node with
     | Empty -> empty
     | Leaf j  -> if  k == j then empty else n
     | Branch (p,m,t0,t1) ->
         if match_prefix kid p m then
-        if zero_bit kid m then
-        branch_ne p m (rmv t0) t1
-        else
-        branch_ne p m t0 (rmv t1)
+          if zero_bit kid m then
+            branch_ne p m (rmv t0) t1
+          else
+            branch_ne p m t0 (rmv t1)
         else
-        n
+          n
     in
     rmv t
 
   (* should run in O(1) thanks to hash consing *)
 
-  let equal a b = Node.equal a b
+  let equal a b = a == b
 
   let compare a b = (Uid.to_int (Node.uid a)) - (Uid.to_int (Node.uid b))
 
@@ -193,47 +187,47 @@ struct
     if equal s t (* This is cheap thanks to hash-consing *)
     then s
     else
-    match Node.node s, Node.node t with
-    | Empty, _  -> t
-    | _, Empty  -> s
-    | Leaf k, _ -> add k t
-    | _, Leaf k -> add k s
-    | Branch (p,m,s0,s1), Branch (q,n,t0,t1) ->
-        if m == n && match_prefix q p m then
-        branch p  m  (merge s0 t0) (merge s1 t1)
-        else if m > n && match_prefix q p m then
-        if zero_bit q m then
-        branch_ne p m (merge s0 t) s1
-        else
-        branch_ne p m s0 (merge s1 t)
-        else if m < n && match_prefix p q n then
-        if zero_bit p n then
-        branch_ne q n (merge s t0) t1
-        else
-        branch_ne q n t0 (merge s t1)
-        else
-                                  (* The prefixes disagree. *)
-        join p s q t
+      match s.Node.node, t.Node.node with
+      | Empty, _  -> t
+      | _, Empty  -> s
+      | Leaf k, _ -> add k t
+      | _, Leaf k -> add k s
+      | Branch (p,m,s0,s1), Branch (q,n,t0,t1) ->
+          if m == n && match_prefix q p m then
+            branch p  m  (merge s0 t0) (merge s1 t1)
+          else if m > n && match_prefix q p m then
+            if zero_bit q m then
+              branch_ne p m (merge s0 t) s1
+            else
+              branch_ne p m s0 (merge s1 t)
+          else if m < n && match_prefix p q n then
+            if zero_bit p n then
+              branch_ne q n (merge s t0) t1
+            else
+              branch_ne q n t0 (merge s t1)
+          else
+        (* The prefixes disagree. *)
+            join p s q t
 
 
 
 
   let rec subset s1 s2 = (equal s1 s2) ||
-    match (Node.node s1,Node.node s2) with
+    match s1.Node.node, s2.Node.node with
     | Empty, _ -> true
     | _, Empty -> false
     | Leaf k1, _ -> mem k1 s2
     | Branch _, Leaf _ -> false
     | Branch (p1,m1,l1,r1), Branch (p2,m2,l2,r2) ->
         if m1 == m2 && p1 == p2 then
-        subset l1 l2 && subset r1 r2
+          subset l1 l2 && subset r1 r2
         else if m1 < m2 && match_prefix p1 p2 m2 then
-        if zero_bit p1 m2 then
-        subset l1 l2 && subset r1 l2
+          if zero_bit p1 m2 then
+            subset l1 l2 && subset r1 l2
+          else
+            subset l1 r2 && subset r1 r2
         else
-        subset l1 r2 && subset r1 r2
-        else
-        false
+          false
 
 
   let union s1 s2 = merge s1 s2
@@ -243,88 +237,90 @@ struct
     if equal s1 s2
     then s1
     else
-    match (Node.node s1,Node.node s2) with
-    | Empty, _ -> empty
-    | _, Empty -> empty
-    | Leaf k1, _ -> if mem k1 s2 then s1 else empty
-    | _, Leaf k2 -> if mem k2 s1 then s2 else empty
-    | Branch (p1,m1,l1,r1), Branch (p2,m2,l2,r2) ->
-        if m1 == m2 && p1 == p2 then
-        merge (inter l1 l2)  (inter r1 r2)
-        else if m1 > m2 && match_prefix p2 p1 m1 then
-        inter (if zero_bit p2 m1 then l1 else r1) s2
-        else if m1 < m2 && match_prefix p1 p2 m2 then
-        inter s1 (if zero_bit p1 m2 then l2 else r2)
-        else
-        empty
+      match s1.Node.node, s2.Node.node with
+      | Empty, _ -> empty
+      | _, Empty -> empty
+      | Leaf k1, _ -> if mem k1 s2 then s1 else empty
+      | _, Leaf k2 -> if mem k2 s1 then s2 else empty
+      | Branch (p1,m1,l1,r1), Branch (p2,m2,l2,r2) ->
+          if m1 == m2 && p1 == p2 then
+            merge (inter l1 l2)  (inter r1 r2)
+          else if m1 > m2 && match_prefix p2 p1 m1 then
+            inter (if zero_bit p2 m1 then l1 else r1) s2
+          else if m1 < m2 && match_prefix p1 p2 m2 then
+            inter s1 (if zero_bit p1 m2 then l2 else r2)
+          else
+            empty
 
   let rec diff s1 s2 =
     if equal s1 s2
     then empty
     else
-    match (Node.node s1,Node.node s2) with
-    | Empty, _ -> empty
-    | _, Empty -> s1
-    | Leaf k1, _ -> if mem k1 s2 then empty else s1
-    | _, Leaf k2 -> remove k2 s1
-    | Branch (p1,m1,l1,r1), Branch (p2,m2,l2,r2) ->
-        if m1 == m2 && p1 == p2 then
-        merge (diff l1 l2) (diff r1 r2)
-        else if m1 > m2 && match_prefix p2 p1 m1 then
-        if zero_bit p2 m1 then
-        merge (diff l1 s2) r1
-        else
-        merge l1 (diff r1 s2)
-        else if m1 < m2 && match_prefix p1 p2 m2 then
-        if zero_bit p1 m2 then diff s1 l2 else diff s1 r2
-        else
-        s1
+      match s1.Node.node, s2.Node.node with
+      | Empty, _ -> empty
+      | _, Empty -> s1
+      | Leaf k1, _ -> if mem k1 s2 then empty else s1
+      | _, Leaf k2 -> remove k2 s1
+      | Branch (p1,m1,l1,r1), Branch (p2,m2,l2,r2) ->
+          if m1 == m2 && p1 == p2 then
+            merge (diff l1 l2) (diff r1 r2)
+          else if m1 > m2 && match_prefix p2 p1 m1 then
+            if zero_bit p2 m1 then
+              merge (diff l1 s2) r1
+            else
+              merge l1 (diff r1 s2)
+          else if m1 < m2 && match_prefix p1 p2 m2 then
+            if zero_bit p1 m2 then diff s1 l2 else diff s1 r2
+          else
+            s1
 
 
   (*s All the following operations ([cardinal], [iter], [fold], [for_all],
     [exists], [filter], [partition], [choose], [elements]) are
     implemented as for any other kind of binary trees. *)
 
-  let rec cardinal n = match Node.node n with
+  let rec cardinal n = match n.Node.node with
   | Empty -> 0
   | Leaf _ -> 1
   | Branch (_,_,t0,t1) -> cardinal t0 + cardinal t1
 
-  let rec iter f n = match Node.node n with
+  let rec iter f n = match n.Node.node with
   | Empty -> ()
   | Leaf k -> f k
   | Branch (_,_,t0,t1) -> iter f t0; iter f t1
 
-  let rec fold f s accu = match Node.node s with
+  let rec fold f s accu = match s.Node.node with
   | Empty -> accu
   | Leaf k -> f k accu
-  | Branch (_,_,t0,t1) -> fold f t0 (fold f t1 accu)
+  | Branch (_,_,t0,t1) -> fold f t1 (fold f t0 accu)
 
 
-  let rec for_all p n = match Node.node n with
+  let rec for_all p n = match n.Node.node with
   | Empty -> true
   | Leaf k -> p k
   | Branch (_,_,t0,t1) -> for_all p t0 && for_all p t1
 
-  let rec exists p n = match Node.node n with
+  let rec exists p n = match n.Node.node with
   | Empty -> false
   | Leaf k -> p k
   | Branch (_,_,t0,t1) -> exists p t0 || exists p t1
 
-  let rec filter pr n = match Node.node n with
+  let rec filter pr n = match n.Node.node with
   | Empty -> empty
   | Leaf k -> if pr k then n else empty
-  | Branch (p,m,t0,t1) -> branch_ne p m (filter pr t0) (filter pr t1)
+  | Branch (p,m,t0,t1) -> let n0 = filter pr t0 in
+                          let n1 = filter pr t1 in
+                          branch_ne p m n0 n1
 
   let partition p s =
-    let rec part (t,f as acc) n = match Node.node n with
+    let rec part (t,f as acc) n = match n.Node.node with
     | Empty -> acc
     | Leaf k -> if p k then (add k t, f) else (t, add k f)
     | Branch (_,_,t0,t1) -> part (part acc t0) t1
     in
     part (empty, empty) s
 
-  let rec choose n = match Node.node n with
+  let rec choose n = match n.Node.node with
   | Empty -> raise Not_found
   | Leaf k -> k
   | Branch (_, _,t0,_) -> choose t0   (* we know that [t0] is non-empty *)
@@ -341,20 +337,20 @@ struct
   (*s Additional functions w.r.t to [Set.S]. *)
 
   let rec intersect s1 s2 = (equal s1 s2) ||
-    match (Node.node s1,Node.node s2) with
+    match  s1.Node.node, s2.Node.node with
     | Empty, _ -> false
     | _, Empty -> false
     | Leaf k1, _ -> mem k1 s2
     | _, Leaf k2 -> mem k2 s1
     | Branch (p1,m1,l1,r1), Branch (p2,m2,l2,r2) ->
         if m1 == m2 && p1 == p2 then
-        intersect l1 l2 || intersect r1 r2
+          intersect l1 l2 || intersect r1 r2
         else if m1 > m2 && match_prefix p2 p1 m1 then
-        intersect (if zero_bit p2 m1 then l1 else r1) s2
+          intersect (if zero_bit p2 m1 then l1 else r1) s2
         else if m1 < m2 && match_prefix p1 p2 m2 then
-        intersect s1 (if zero_bit p1 m2 then l2 else r2)
+          intersect s1 (if zero_bit p1 m2 then l2 else r2)
         else
-        false
+          false
 
 
   let from_list l = List.fold_left (fun acc e -> add e acc) empty l
diff --git a/src/run.ml b/src/run.ml
index 9c8203b..bd60264 100644
--- a/src/run.ml
+++ b/src/run.ml
@@ -299,7 +299,7 @@ DEFINE AND_(t1,t2) =
     let cache2 = run.cache2 in
     let cache5 = run.cache5 in
     let unstable = run.unstable in
-    let init_todo = StateSet.diff  (Ata.get_states auto)  (Ata.get_starting_states auto) in
+    let init_todo = StateSet.diff (Ata.get_states auto) (Ata.get_starting_states auto) in
     let rec loop node =
       let node_id = T.preorder tree node in
       if node == T.nil || not (Bitvector.get unstable node_id) then false else begin
@@ -459,9 +459,9 @@ DEFINE AND_(t1,t2) =
           cache.(T.preorder tree node).NodeStatus.node.sat
     in
     loop (T.root tree);
-    StateSet.fold
-      (fun q acc -> (q, Hashtbl.find res_mapper q)::acc)
-      (Ata.get_selecting_states auto) []
+    List.rev (StateSet.fold
+                (fun q acc -> (q, Hashtbl.find res_mapper q)::acc)
+                (Ata.get_selecting_states auto) [])
 
   let prepare_run run list =
     let tree = run.tree in