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

diff --git a/src/ata.ml b/src/ata.ml
index c01cd50..62be713 100644
--- 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-22 14:46:08 CEST by Kim Nguyen>
 *)
 
 INCLUDE "utils.ml"
@@ -303,9 +303,132 @@ 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 == 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.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 summary =
+  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 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)
+    end
+  in
+  loop phi
+
+
+
+let eval_trans auto fcs nss ps ss =
+  let rec loop old_config =
+    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 ->
+          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 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
+            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 ; summary = old_summary } 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