Maintain the set of unsatisfiable states.

[tatoo.git] / src / ata.ml

diff --git a/src/ata.ml b/src/ata.ml
index c01cd50..4d43441 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 17:05:32 CEST by Kim Nguyen>
 *)
 
 INCLUDE "utils.ml"
@@ -306,6 +306,81 @@ let eval_trans auto ltrs fcs nss ps ss is_left is_right has_left has_right kind
 
 
 
+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
+
+let simplify_atom atom pos q 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_trans2 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, 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 = { 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