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 8f8652e..b48d129 100644 (file)
--- a/src/eval.ml
+++ b/src/eval.ml
@@ -14,7 +14,7 @@
 (***********************************************************************)
 
 (*
-  Time-stamp: <Last modified on 2013-04-18 17:36:06 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
@@ -53,71 +61,46 @@ END
         let config0 =
           let c = get cache tree node in
           if c == Cache.N1.dummy cache then
-            { c with Ata.todo = Ata.get_trans auto tag auto.Ata.states }
+           Ata.Config.make
+             { 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(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_trans2 auto fcs nss ps config0
-            is_left is_right has_left has_right kind
-        in
-        let () =
-          TRACE(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
-        if not (Ata.eq_config config0 config1) then set cache tree node config1;
+        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_trans2 auto
-            fcs1 nss ps config1
-            is_left is_right has_left has_right kind
-        in
-        let () =
-          TRACE(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 not (Ata.eq_config config1 config2) then set cache tree node config2;
+        if config1 != config2 then set cache tree node config2;
         let () = loop ns in
-        let config3 =
-          Ata.eval_trans2 auto
-            fcs1 (get cache tree ns) ps config2
-            is_left is_right has_left has_right kind
-        in
-        let () =
-          TRACE(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
-        if not (Ata.eq_config config2 config3) then set cache tree node config3;
+        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.todo) (* no more transition to check *)
-          || (Ata.eq_config 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
@@ -131,7 +114,7 @@ END
         let acc0 = loop (T.next_sibling tree node) acc in
         let acc1 = loop (T.first_child tree node) acc0 in
 
-        if StateSet.intersect (get cache tree node).Ata.sat auto.Ata.selection_states then
+        if StateSet.intersect (get cache tree node).Ata.Config.node.Ata.sat auto.Ata.selection_states then
           node::acc1
         else
           acc1
@@ -139,9 +122,12 @@ END
     loop node []
 
   let eval auto tree node =
-    let cache = Cache.N1.create { Ata.sat = StateSet.empty;
-                                  Ata.unsat = StateSet.empty;
-                                  Ata.todo = Ata.TransList.nil }
+    let cache = Cache.N1.create
+      (Ata.Config.make { Ata.sat = StateSet.empty;
+                         Ata.unsat = StateSet.empty;
+                         Ata.todo = Ata.TransList.nil;
+                         Ata.summary = Ata.dummy_summary;
+                       })
     in
     let redo = ref true in
     let iter = ref 0 in