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

[tatoo.git] / src / ata.ml

diff --git a/src/ata.ml b/src/ata.ml
index 919dced..62be713 100644 (file)
--- a/src/ata.ml
+++ b/src/ata.ml
@@ -14,7 +14,7 @@
 (***********************************************************************)
 
 (*
-  Time-stamp: <Last modified on 2013-04-18 18:37:45 CEST by Kim Nguyen>
+  Time-stamp: <Last modified on 2013-04-22 14:46:08 CEST by Kim Nguyen>
 *)
 
 INCLUDE "utils.ml"
@@ -303,21 +303,61 @@ 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)
+
+
 
 type config = {
   sat : StateSet.t;
   unsat : StateSet.t;
   todo : TransList.t;
+  summary : node_summary;
 }
 
 module Config = Hcons.Make(struct
   type t = config
   let equal c d =
-    c.sat == d.sat && c.unsat == d.unsat && c.todo == d.todo
+    c == d ||
+      c.sat == d.sat &&
+      c.unsat == d.unsat &&
+      c.todo == d.todo &&
+      c.summary == d.summary
+
   let hash c =
-    HASHINT3((c.sat.StateSet.id :> int),
+    HASHINT4((c.sat.StateSet.id :> int),
              (c.unsat.StateSet.id :> int),
-             (c.todo.TransList.id :> int))
+             (c.todo.TransList.id :> int),
+             c.summary)
 end
 )
 
@@ -329,7 +369,7 @@ let simplify_atom atom pos q { Config.node=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
@@ -340,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)
@@ -354,9 +394,13 @@ let eval_form2 phi fcs nss ps ss is_left is_right has_left has_right kind =
 
 
 
-let eval_trans 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.Config.node 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 ->
@@ -364,9 +408,7 @@ let eval_trans 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
@@ -380,9 +422,9 @@ let eval_trans 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 = Config.make { 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