Hash-conses each node configuration.

[tatoo.git] / src / ata.ml

diff --git a/src/ata.ml b/src/ata.ml
index c01cd50..919dced 100644 (file)
--- a/src/ata.ml
+++ b/src/ata.ml
@@ -14,7 +14,7 @@
 (***********************************************************************)
 
 (*
-  Time-stamp: <Last modified on 2013-04-04 21:16:04 CEST by Kim Nguyen>
+  Time-stamp: <Last modified on 2013-04-18 18:37:45 CEST by Kim Nguyen>
 *)
 
 INCLUDE "utils.ml"
@@ -304,9 +304,90 @@ 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;
+}
+
+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.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)
+      || ((not pos) && StateSet.mem q config.sat) then SFormula.false_
+  else atom
+
+
+let eval_form2 phi fcs nss ps ss is_left is_right has_left has_right kind =
+  let rec loop phi =
+    begin match SFormula.expr phi with
+      Formula.True | Formula.False -> phi
+    | Formula.Atom a ->
+        let p, b, q = Atom.node a in begin
+          match p with
+          | First_child -> simplify_atom phi b q fcs
+          | 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)
+        end
+    | Formula.And(phi1, phi2) -> SFormula.and_ (loop phi1) (loop phi2)
+    | Formula.Or (phi1, phi2) -> SFormula.or_  (loop phi1) (loop phi2)
+    end
+  in
+  loop phi
 
 
 
+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.Config.node in
+    let sat, unsat, removed, kept, todo =
+      TransList.fold
+        (fun trs acc ->
+          let q, lab, phi = Transition.node trs in
+          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
+            in
+            if SFormula.is_true new_phi then
+              StateSet.add q a_sat, a_unsat, StateSet.add q a_rem, a_kept, a_todo
+            else if SFormula.is_false new_phi then
+              a_sat, StateSet.add q a_unsat, StateSet.add q a_rem, a_kept, a_todo
+            else
+              let new_tr = Transition.make (q, lab, new_phi) in
+              (a_sat, a_unsat, a_rem, StateSet.add q a_kept, (TransList.cons new_tr a_todo))
+        ) old_todo (old_sat, old_unsat, StateSet.empty, StateSet.empty, TransList.nil)
+    in
+  (* 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 *)
+    let unsat = StateSet.diff unsat sat 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
+  loop ss
+
 (*
   [add_trans a q labels f] adds a transition [(q,labels) -> f] to the
   automaton [a] but ensures that transitions remains pairwise disjoint