From: Kim Nguyễn <kn@lri.fr>
Date: Sat, 11 Jan 2014 17:22:16 +0000 (+0100)
Subject: Implement subtree-skipping optimisation (a one liner, really ~_~) that skips a whole... 
X-Git-Tag: v0.1~3
X-Git-Url: http://git.nguyen.vg/gitweb/?p=tatoo.git;a=commitdiff_plain;h=aae9118fbf9d29df5d7fc36efe2afd6eadab11d1

Implement subtree-skipping optimisation (a one liner, really ~_~) that skips a whole subtree during the topdown phase when some states had to be proven but none could.
---

diff --git a/src/run.ml b/src/run.ml
index f9222f1..53f48c3 100644
--- a/src/run.ml
+++ b/src/run.ml
@@ -153,8 +153,8 @@ END
                            match m with
                              `First_child -> fcs
                            | `Next_sibling -> nss
-                           | `Parent | `Previous_sibling ->  ps
-                           | `Stay ->  ss
+                           | `Parent | `Previous_sibling -> ps
+                           | `Stay -> ss
                        )
                      | Is_first_child -> b == is_left summary
                      | Is_next_sibling -> b == is_right summary
@@ -238,6 +238,7 @@ module Make (T : Tree.S) (L : Node_list.S with type node = T.node) =
     let rec loop_td_and_bu node parent parent_sat =
       if node == T.nil then StateSet.empty
       else begin
+        let tag = T.tag tree node in
         let node_id = T.preorder tree node in
         let fc = T.first_child tree node in
         let ns = T.next_sibling tree node in
@@ -247,8 +248,8 @@ module Make (T : Tree.S) (L : Node_list.S with type node = T.node) =
           if  s != 0 then s else
             let s =
               NodeSummary.make
-                (node_id == T.preorder tree (T.first_child tree parent)) (*is_left *)
-                (node_id ==  T.preorder tree (T.next_sibling tree parent))(*is_right *)
+                (node == (T.first_child tree parent)) (*is_left *)
+                (node == (T.next_sibling tree parent))(*is_right *)
                 (fc != T.nil) (* has_left *)
                 (ns != T.nil) (* has_right *)
                 (T.kind tree node) (* kind *)
@@ -258,7 +259,6 @@ module Make (T : Tree.S) (L : Node_list.S with type node = T.node) =
         let status0 = unsafe_get run.sat node_id in
         (* get the node_statuses for the first child, next sibling and parent *)
         (* evaluate the transitions with all this statuses *)
-        let tag = T.tag tree node in
         let status1 =
           eval_trans
             auto run.fetch_trans_cache run.td_cache tag
@@ -268,9 +268,10 @@ module Make (T : Tree.S) (L : Node_list.S with type node = T.node) =
             parent_sat
             status0 td_todo
         in
-
-        (* update the cache if the status of the node changed
-           unsafe_set run.sat node_id status1 status0;*)
+        if status1 == StateSet.empty && status0 != StateSet.empty
+        then StateSet.empty else
+          (* update the cache if the status of the node changed
+             unsafe_set run.sat node_id status1 status0;*)
           if bu_todo == StateSet.empty then begin
             unsafe_set run.sat node_id status1 status0; (* write the td_states *)
             update_res false status1 node;
@@ -295,7 +296,7 @@ module Make (T : Tree.S) (L : Node_list.S with type node = T.node) =
                 status1 bu_todo
             in
             unsafe_set run.sat node_id status2 status0;
-            if last_run then update_res true status2 node;
+            if last_run && status2 != StateSet.empty then update_res true status2 node;
             status2
         end
     in