Tentative optimization

diff --git a/src/run.ml b/src/run.ml
index cb2ea3b..df9397b 100644 (file)
--- a/src/run.ml
+++ b/src/run.ml
@@ -221,6 +221,51 @@ END
          in
          loop phi
 
          in
          loop phi
 

+   type trivalent = False | True | Unknown
+
+   let or_ t1 t2 = match t1 with
+     False -> t2
+   | True -> True
+   | Unknown -> if t2 == True then True else Unknown
+
+   let and_ t1 t2 = match t1 with
+     False -> False
+   | True -> t2
+   | Unknown -> if t2 == False then False else Unknown
+   let of_bool = function false -> False | true -> True
+
+   let eval_form phi fcs nss ps ss summary =
+     let open Ata in
+         let rec loop phi =
+           begin match Formula.expr phi with
+           | Boolean.False -> False
+           | Boolean.True -> True
+           | Boolean.Atom (a, b) ->
+               begin
+                 let open NodeSummary in
+                     match a.Atom.node with
+                     | Move (m, q) ->
+                         let sum = match m with
+                           `First_child -> fcs
+                         | `Next_sibling -> nss
+                         | `Parent | `Previous_sibling -> ps
+                         | `Stay -> ss
+                         in
+                         if StateSet.mem q sum.NodeStatus.node.sat then of_bool b
+                         else if StateSet.mem q sum.NodeStatus.node.unsat then of_bool (not b)
+                         else Unknown
+                     | Is_first_child -> of_bool (b == is_left summary)
+                     | Is_next_sibling -> of_bool (b == is_right summary)
+                     | Is k -> of_bool (b == (k == kind summary))
+                     | Has_first_child -> of_bool (b == has_left summary)
+                     | Has_next_sibling -> of_bool (b == has_right summary)
+               end
+           | Boolean.And(phi1, phi2) -> and_ (loop phi1) (loop phi2)
+           | Boolean.Or (phi1, phi2) -> or_  (loop phi1) (loop phi2)
+           end
+         in
+         loop phi
+

 
    let eval_trans_aux cache4 fcs nss ps ss old_config =
      let { sat = old_sat;
 
    let eval_trans_aux cache4 fcs nss ps ss old_config =
      let { sat = old_sat;


@@ -234,16 +279,14 @@ END
            let q, lab, phi = Ata.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 q, lab, phi = Ata.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 =
+             let phi_val =

                eval_form phi fcs nss ps old_config old_summary
              in
                eval_form phi fcs nss ps old_config old_summary
              in

-             if Ata.Formula.is_true new_phi then
-               StateSet.add q a_sat, a_unsat, StateSet.add q a_rem, a_kept, a_todo
-             else if Ata.Formula.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 = Ata.Transition.make (q, lab, new_phi) in
-               (a_sat, a_unsat, a_rem, StateSet.add q a_kept, (Ata.TransList.cons new_tr a_todo))
+             match phi_val with
+             | False -> a_sat, StateSet.add q a_unsat, StateSet.add q a_rem, a_kept, a_todo
+             | True ->  StateSet.add q a_sat, a_unsat, StateSet.add q a_rem, a_kept, a_todo
+             | Unknown ->
+                 (a_sat, a_unsat, a_rem, StateSet.add q a_kept, (Ata.TransList.cons trs a_todo))

          ) old_todo (old_sat, old_unsat, StateSet.empty, StateSet.empty, Ata.TransList.nil)
      in
            (* States that have been removed from the todo list and not kept are now
          ) old_todo (old_sat, old_unsat, StateSet.empty, StateSet.empty, Ata.TransList.nil)
      in
            (* States that have been removed from the todo list and not kept are now