Do not stupidely recompute a constant set of states for each node

[tatoo.git] / src / run.ml

diff --git a/src/run.ml b/src/run.ml
index 726a483..9c8203b 100644 (file)
--- a/src/run.ml
+++ b/src/run.ml
@@ -250,7 +250,7 @@ DEFINE AND_(t1,t2) =
          loop phi
 
 
          loop phi
 
 

-   let eval_trans_aux auto cache2 cache4 tag fcs nss ps old_status =
+   let eval_trans_aux auto cache2 tag fcs nss ps old_status =

      let { sat = old_sat;
            todo = old_todo;
            summary = old_summary } as os_node = old_status.NodeStatus.node
      let { sat = old_sat;
            todo = old_todo;
            summary = old_summary } as os_node = old_status.NodeStatus.node


@@ -273,26 +273,22 @@ DEFINE AND_(t1,t2) =
 
 
    let eval_trans auto cache2 cache5 tag fcs nss ps ss =
 
 
    let eval_trans auto cache2 cache5 tag fcs nss ps ss =

+     let rec loop old_status =
+       let new_status =
+         eval_trans_aux auto cache2 tag fcs nss ps old_status
+       in
+       if new_status == old_status then old_status else loop new_status
+     in

      let fcsid = (fcs.NodeStatus.id :> int) in
      let nssid = (nss.NodeStatus.id :> int) in
      let psid = (ps.NodeStatus.id :> int) in
      let fcsid = (fcs.NodeStatus.id :> int) in
      let nssid = (nss.NodeStatus.id :> int) in
      let psid = (ps.NodeStatus.id :> int) in

+     let ssid = (ss.NodeStatus.id :> int) in

      let tagid = (tag.QName.id :> int) in
      let tagid = (tag.QName.id :> int) in

-     let rec loop old_status =
-       let oid = (old_status.NodeStatus.id :> int) in
-       let res =
-         let res = Cache.N5.find cache5 tagid oid fcsid nssid psid in
-         if res != dummy_status then res
-         else
-           let new_status =
-             eval_trans_aux auto cache2 cache5 tag fcs nss ps old_status
-           in
-           Cache.N5.add cache5 tagid oid fcsid nssid psid new_status;
-           new_status
-       in
-       if res == old_status then res else loop res
-     in
-     loop ss
-
+     let res = Cache.N5.find cache5 tagid ssid fcsid nssid psid in
+     if res != dummy_status then res
+     else let new_status = loop ss in
+          Cache.N5.add cache5 tagid ssid fcsid nssid psid new_status;
+          new_status

 
 
 
 
 
 


@@ -303,6 +299,7 @@ DEFINE AND_(t1,t2) =
     let cache2 = run.cache2 in
     let cache5 = run.cache5 in
     let unstable = run.unstable in
     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 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
     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


@@ -320,9 +317,7 @@ DEFINE AND_(t1,t2) =
             (* first time we visit the node *)
             NodeStatus.make
               { sat = StateSet.empty;
             (* first time we visit the node *)
             NodeStatus.make
               { sat = StateSet.empty;

-                todo = StateSet.diff
-                  (Ata.get_states auto)
-                  (Ata.get_starting_states auto);
+                todo = init_todo;

                 summary = NodeSummary.make
                   (node == T.first_child tree parent) (* is_left *)
                   (node == T.next_sibling tree parent) (* is_right *)
                 summary = NodeSummary.make
                   (node == T.first_child tree parent) (* is_left *)
                   (node == T.next_sibling tree parent) (* is_right *)