X-Git-Url: http://git.nguyen.vg/gitweb/?p=tatoo.git;a=blobdiff_plain;f=src%2Fata.ml;h=62be713138fd0e884fe95b5bab9bd6ff0311710a;hp=4d4344128db52b72a64b1012a0a326d91b4248bf;hb=e8132686a926c6be4599c7c2496d8e6a5b42a243;hpb=3c87bbf00b98bcf40dab913cd334846b26cdb71d

diff --git a/src/ata.ml b/src/ata.ml
index 4d43441..62be713 100644
--- a/src/ata.ml
+++ b/src/ata.ml
@@ -14,7 +14,7 @@
 (***********************************************************************)
 
 (*
-  Time-stamp: <Last modified on 2013-04-18 17:05:32 CEST by Kim Nguyen>
+  Time-stamp: <Last modified on 2013-04-22 14:46:08 CEST by Kim Nguyen>
 *)
 
 INCLUDE "utils.ml"
@@ -303,6 +303,37 @@ let eval_trans auto ltrs fcs nss ps ss is_left is_right has_left has_right kind
   in
   loop ltrs ss
 
+type node_summary = int
+let dummy_summary = -1
+(*
+4444444444443210
+4 -> kind
+3 -> is_left
+2 -> is_right
+1 -> has_left
+0 -> has_right
+*)
+
+let has_right (s : node_summary) : bool =
+  Obj.magic (s land 1)
+let has_left (s : node_summary) : bool =
+  Obj.magic ((s lsr 1) land 1)
+
+let is_right (s : node_summary) : bool =
+  Obj.magic ((s lsr 2) land 1)
+
+let is_left (s : node_summary) : bool =
+  Obj.magic ((s lsr 3) land 1)
+
+let kind (s : node_summary ) : Tree.NodeKind.t =
+  Obj.magic (s lsr 4)
+
+let node_summary is_left is_right has_left has_right kind =
+  ((Obj.magic kind) lsl 4) lor
+    ((Obj.magic is_left) lsl 3) lor
+    ((Obj.magic is_right) lsl 2) lor
+    ((Obj.magic has_left) lsl 1) lor
+    (Obj.magic has_right)
 
 
 
@@ -310,12 +341,27 @@ type config = {
   sat : StateSet.t;
   unsat : StateSet.t;
   todo : TransList.t;
+  summary : node_summary;
 }
 
-let eq_config c1 c2 =
-  c1.sat == c2.sat && c1.unsat == c2.unsat && c1.todo == c2.todo
+module Config = Hcons.Make(struct
+  type t = config
+  let equal c d =
+    c == d ||
+      c.sat == d.sat &&
+      c.unsat == d.unsat &&
+      c.todo == d.todo &&
+      c.summary == d.summary
+
+  let hash c =
+    HASHINT4((c.sat.StateSet.id :> int),
+             (c.unsat.StateSet.id :> int),
+             (c.todo.TransList.id :> int),
+             c.summary)
+end
+)
 
-let simplify_atom atom pos q config =
+let simplify_atom atom pos q { Config.node=config; _ } =
   if (pos && StateSet.mem q config.sat)
     || ((not pos) && StateSet.mem q config.unsat) then SFormula.true_
   else if (pos && StateSet.mem q config.unsat)
@@ -323,7 +369,7 @@ let simplify_atom atom pos q config =
   else atom
 
 
-let eval_form2 phi fcs nss ps ss is_left is_right has_left has_right kind =
+let eval_form2 phi fcs nss ps ss summary =
   let rec loop phi =
     begin match SFormula.expr phi with
       Formula.True | Formula.False -> phi
@@ -334,11 +380,11 @@ let eval_form2 phi fcs nss ps ss is_left is_right has_left has_right kind =
           | Next_sibling -> simplify_atom phi b q nss
           | Parent | Previous_sibling -> simplify_atom phi b q ps
           | Stay -> simplify_atom phi b q ss
-          | Is_first_child -> SFormula.of_bool (b == is_left)
-          | Is_next_sibling -> SFormula.of_bool (b == is_right)
-          | Is k -> SFormula.of_bool (b == (k == kind))
-          | Has_first_child -> SFormula.of_bool (b == has_left)
-          | Has_next_sibling -> SFormula.of_bool (b == has_right)
+          | Is_first_child -> SFormula.of_bool (b == (is_left summary))
+          | Is_next_sibling -> SFormula.of_bool (b == (is_right summary))
+          | Is k -> SFormula.of_bool (b == (k == (kind summary)))
+          | Has_first_child -> SFormula.of_bool (b == (has_left summary))
+          | Has_next_sibling -> SFormula.of_bool (b == (has_right summary))
         end
     | Formula.And(phi1, phi2) -> SFormula.and_ (loop phi1) (loop phi2)
     | Formula.Or (phi1, phi2) -> SFormula.or_  (loop phi1) (loop phi2)
@@ -348,9 +394,13 @@ let eval_form2 phi fcs nss ps ss is_left is_right has_left has_right kind =
 
 
 
-let eval_trans2 auto fcs nss ps ss is_left is_right has_left has_right kind =
+let eval_trans auto fcs nss ps ss =
   let rec loop old_config =
-    let { sat = old_sat; unsat = old_unsat; todo = old_todo } = old_config in
+    let { sat = old_sat;
+          unsat = old_unsat;
+          todo = old_todo;
+          summary = old_summary } = old_config.Config.node
+    in
     let sat, unsat, removed, kept, todo =
       TransList.fold
         (fun trs acc ->
@@ -358,9 +408,7 @@ let eval_trans2 auto fcs nss ps ss is_left is_right has_left has_right kind =
           let a_sat, a_unsat, a_rem, a_kept, a_todo = acc in
           if StateSet.mem q a_sat || StateSet.mem q a_unsat then acc else
             let new_phi =
-            eval_form2
-              phi fcs nss ps old_config
-              is_left is_right has_left has_right kind
+            eval_form2  phi fcs nss ps old_config old_summary
             in
             if SFormula.is_true new_phi then
               StateSet.add q a_sat, a_unsat, StateSet.add q a_rem, a_kept, a_todo
@@ -374,9 +422,9 @@ let eval_trans2 auto fcs nss ps ss is_left is_right has_left has_right kind =
   (* States that have been removed from the todo list and not kept are now
      unsatisfiable *)
     let unsat = StateSet.union unsat (StateSet.diff removed kept) in
-  (* States that were found once to be satisfiable remain so *)
+    (* States that were found once to be satisfiable remain so *)
     let unsat = StateSet.diff unsat sat in
-    let new_config = { sat; unsat; todo } in
+    let new_config = Config.make { sat; unsat; todo ; summary = old_summary } in
     if sat == old_sat && unsat == old_unsat && todo == old_todo then new_config
     else loop new_config
   in