Hash-conses each node configuration.

[tatoo.git] / src / ata.ml

diff --git a/src/ata.ml b/src/ata.ml
index 4d43441..919dced 100644 (file)
--- 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-18 18:37:45 CEST by Kim Nguyen>
 *)
 
 INCLUDE "utils.ml"
@@ -304,18 +304,24 @@ let eval_trans auto ltrs fcs nss ps ss is_left is_right has_left has_right kind
   loop ltrs ss
 
 
-
-
 type config = {
   sat : StateSet.t;
   unsat : StateSet.t;
   todo : TransList.t;
 }
 
-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.sat == d.sat && c.unsat == d.unsat && c.todo == d.todo
+  let hash c =
+    HASHINT3((c.sat.StateSet.id :> int),
+             (c.unsat.StateSet.id :> int),
+             (c.todo.TransList.id :> int))
+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)
@@ -348,9 +354,9 @@ 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 is_left is_right has_left has_right kind =
   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 } = old_config.Config.node in
     let sat, unsat, removed, kept, todo =
       TransList.fold
         (fun trs acc ->
@@ -376,7 +382,7 @@ let eval_trans2 auto fcs nss ps ss is_left is_right has_left has_right kind =
     let unsat = StateSet.union unsat (StateSet.diff removed kept) in
   (* 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 } in
     if sat == old_sat && unsat == old_unsat && todo == old_todo then new_config
     else loop new_config
   in