Store a summary of the node (kind, topology) in the Ata.Config.t type.

[tatoo.git] / src / eval.ml

diff --git a/src/eval.ml b/src/eval.ml
index 59ebc03..b48d129 100644 (file)
--- a/src/eval.ml
+++ b/src/eval.ml
@@ -14,7 +14,7 @@
 (***********************************************************************)
 
 (*
-  Time-stamp: <Last modified on 2013-04-19 01:13:47 CEST by Kim Nguyen>
+  Time-stamp: <Last modified on 2013-04-22 14:47:46 CEST by Kim Nguyen>
 *)
 
 INCLUDE "utils.ml"
@@ -34,6 +34,14 @@ DEFINE TRACE(e) = (e)
 DEFINE TRACE(e) = ()
 END
 
+   let html tree node i config msg =
+     let config = config.Ata.Config.node in
+     Html.trace (T.preorder tree node) i
+       "%s<br/>sat: %a<br/>unsat: %a<br/>todo: %a<br/>"
+       msg
+       StateSet.print config.Ata.sat
+       StateSet.print config.Ata.unsat
+       (Ata.TransList.print ~sep:"<br/>") config.Ata.todo
 
 
   type cache = StateSet.t Cache.N1.t
@@ -54,79 +62,45 @@ END
           let c = get cache tree node in
           if c == Cache.N1.dummy cache then
            Ata.Config.make
-             { c.Ata.Config.node with Ata.todo = Ata.get_trans auto tag auto.Ata.states }
+             { c.Ata.Config.node with Ata.todo = Ata.get_trans auto tag auto.Ata.states;
+               summary = Ata.node_summary
+                 (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 *)
+             }
           else c
         in
 
-        let () =
-          TRACE(
-            let config0 = config0.Ata.node in
-            Html.trace (T.preorder tree node) _i "Config0<br/>sat: %a<br/>unsat: %a<br/>todo: %a<br/>"
-                  StateSet.print config0.Ata.sat
-                  StateSet.print config0.Ata.unsat
-                  (Ata.TransList.print ~sep:"<br/>") config0.Ata.todo)
-        in
+        TRACE(html tree node _i config0 "Entering node");
 
         let ps = get cache tree parent in
         let fcs = get cache tree fc in
         let nss = get cache tree ns in
-        let is_left = node == T.first_child tree parent
-        and is_right = node == T.next_sibling tree parent
-        and has_left = fc != T.nil
-        and has_right = ns != T.nil
-        and kind = T.kind tree node
-        in
-        let config1 =
-          Ata.eval_trans auto fcs nss ps config0
-            is_left is_right has_left has_right kind
-        in
-        let () =
-          TRACE(
-            let config1 = config1.Ata.node in
-            Html.trace (T.preorder tree node) _i "Config1<br/>sat: %a<br/>unsat: %a<br/>todo: %a<br/>"
-                  StateSet.print config1.Ata.sat
-                  StateSet.print config1.Ata.unsat
-                  (Ata.TransList.print ~sep:"<br/>") config1.Ata.todo)
-        in
+        let config1 = Ata.eval_trans auto fcs nss ps config0 in
+
+        TRACE(html tree node _i config1 "Updating transitions");
+
         if config0 != config1 then set cache tree node config1;
         let () = loop fc in
         let fcs1 = get cache tree fc in
-        let config2 =
-          Ata.eval_trans auto
-            fcs1 nss ps config1
-            is_left is_right has_left has_right kind
-        in
-        let () =
-          TRACE(
-            let config2 = config2.Ata.node in
-            Html.trace (T.preorder tree node) _i "Config2<br/>sat: %a<br/>unsat: %a<br/>todo: %a<br/>"
-                  StateSet.print config2.Ata.sat
-                  StateSet.print config2.Ata.unsat
-                  (Ata.TransList.print ~sep:"<br/>") config2.Ata.todo)
-        in
+        let config2 = Ata.eval_trans auto fcs1 nss ps config1 in
+
+        TRACE(html tree node _i config2 "Updating transitions (after first-child)");
 
         if config1 != config2 then set cache tree node config2;
         let () = loop ns in
-        let config3 =
-          Ata.eval_trans auto
-            fcs1 (get cache tree ns) ps config2
-            is_left is_right has_left has_right kind
-        in
-        let () =
-          TRACE(
-            let config3 = config3.Ata.node in
-            Html.trace (T.preorder tree node) _i "Config3<br/>sat: %a<br/>unsat: %a<br/>todo: %a<br/>"
-                  StateSet.print config3.Ata.sat
-                  StateSet.print config3.Ata.unsat
-                  (Ata.TransList.print ~sep:"<br/>") config3.Ata.todo)
-        in
+        let config3 = Ata.eval_trans auto fcs1 (get cache tree ns) ps config2 in
+
+        TRACE(html tree node _i config3 "Updating transitions (after next-sibling)");
+
         if config2 != config3 then set cache tree node config3;
         (* We do set the redo flat if : *)
         if not (
-          !redo (* already set *)
-          || (Ata.TransList.nil == config3.Ata.Config.node.Ata.todo) (* no more transition to check *)
-          || (config0 == config3) (* did not gain any new information *)
-        )
+          config0 == config3 (* did not gain any new information *)
+          || !redo (* already set *)
+          || Ata.TransList.nil == config3.Ata.Config.node.Ata.todo ) (* no more transition to check *)
         then redo := true
       end
     in
@@ -151,7 +125,9 @@ END
     let cache = Cache.N1.create
       (Ata.Config.make { Ata.sat = StateSet.empty;
                          Ata.unsat = StateSet.empty;
-                         Ata.todo = Ata.TransList.nil })
+                         Ata.todo = Ata.TransList.nil;
+                         Ata.summary = Ata.dummy_summary;
+                       })
     in
     let redo = ref true in
     let iter = ref 0 in