From e8132686a926c6be4599c7c2496d8e6a5b42a243 Mon Sep 17 00:00:00 2001 From: =?utf8?q?Kim=20Nguy=E1=BB=85n?= Date: Mon, 22 Apr 2013 14:48:11 +0200 Subject: [PATCH] Store a summary of the node (kind, topology) in the Ata.Config.t type. --- src/ata.ml | 76 +++++++++++++++++++++++++++++++++---------- src/ata.mli | 11 ++++--- src/eval.ml | 94 ++++++++++++++++++++--------------------------------- 3 files changed, 100 insertions(+), 81 deletions(-) diff --git a/src/ata.ml b/src/ata.ml index 919dced..62be713 100644 --- a/src/ata.ml +++ b/src/ata.ml @@ -14,7 +14,7 @@ (***********************************************************************) (* - Time-stamp: + Time-stamp: *) INCLUDE "utils.ml" @@ -303,21 +303,61 @@ 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.sat == d.sat && c.unsat == d.unsat && c.todo == d.todo + c == d || + c.sat == d.sat && + c.unsat == d.unsat && + c.todo == d.todo && + c.summary == d.summary + let hash c = - HASHINT3((c.sat.StateSet.id :> int), + HASHINT4((c.sat.StateSet.id :> int), (c.unsat.StateSet.id :> int), - (c.todo.TransList.id :> int)) + (c.todo.TransList.id :> int), + c.summary) end ) @@ -329,7 +369,7 @@ let simplify_atom atom pos q { Config.node=config; _ } = else atom -let eval_form2 phi fcs nss ps ss is_left is_right has_left has_right kind = +let eval_form2 phi fcs nss ps ss summary = let rec loop phi = begin match SFormula.expr phi with Formula.True | Formula.False -> phi @@ -340,11 +380,11 @@ let eval_form2 phi fcs nss ps ss is_left is_right has_left has_right kind = | 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) + | 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) @@ -354,9 +394,13 @@ let eval_form2 phi 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 eval_trans auto fcs nss ps ss = let rec loop old_config = - let { sat = old_sat; unsat = old_unsat; todo = old_todo } = old_config.Config.node in + 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 -> @@ -364,9 +408,7 @@ let eval_trans auto fcs nss ps ss is_left is_right has_left has_right kind = 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 + 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 @@ -380,9 +422,9 @@ let eval_trans auto fcs nss ps ss is_left is_right has_left has_right kind = (* 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 *) + (* 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 + 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 diff --git a/src/ata.mli b/src/ata.mli index 0b52462..e2bf7e3 100644 --- a/src/ata.mli +++ b/src/ata.mli @@ -14,7 +14,7 @@ (***********************************************************************) (* - Time-stamp: + Time-stamp: *) type predicate = @@ -81,18 +81,19 @@ val create : StateSet.t -> StateSet.t -> t val reset : t -> unit val get_trans : t -> QNameSet.elt -> StateSet.t -> TransList.t +type node_summary = private int +val node_summary : bool -> bool -> bool -> bool -> Tree.NodeKind.t -> node_summary +val dummy_summary : node_summary type config = { sat : StateSet.t; unsat : StateSet.t; todo : TransList.t; + summary : node_summary; } module Config : Hcons.S with type data = config -val eval_trans : t -> Config.t -> Config.t -> Config.t -> Config.t - -> bool -> bool -> bool -> bool -> Tree.NodeKind.t - -> Config.t - +val eval_trans : t -> Config.t -> Config.t -> Config.t -> Config.t -> Config.t val add_trans : t -> State.t -> QNameSet.t -> SFormula.t -> unit val print : Format.formatter -> t -> unit diff --git a/src/eval.ml b/src/eval.ml index 59ebc03..b48d129 100644 --- a/src/eval.ml +++ b/src/eval.ml @@ -14,7 +14,7 @@ (***********************************************************************) (* - Time-stamp: + Time-stamp: *) INCLUDE "utils.ml" @@ -34,6 +34,14 @@ DEFINE TRACE(e) = (e) DEFINE TRACE(e) = () END + let html tree node i config msg = + let config = config.Ata.Config.node in + Html.trace (T.preorder tree node) i + "%s
sat: %a
unsat: %a
todo: %a
" + msg + StateSet.print config.Ata.sat + StateSet.print config.Ata.unsat + (Ata.TransList.print ~sep:"
") config.Ata.todo type cache = StateSet.t Cache.N1.t @@ -54,79 +62,45 @@ END let c = get cache tree node in if c == Cache.N1.dummy cache then Ata.Config.make - { c.Ata.Config.node with Ata.todo = Ata.get_trans auto tag auto.Ata.states } + { c.Ata.Config.node with Ata.todo = Ata.get_trans auto tag auto.Ata.states; + summary = Ata.node_summary + (node == T.first_child tree parent) (* is_left *) + (node == T.next_sibling tree parent) (* is_right *) + (fc != T.nil) (* has_left *) + (ns != T.nil) (* has_right *) + (T.kind tree node) (* kind *) + } else c in - let () = - TRACE( - let config0 = config0.Ata.node in - Html.trace (T.preorder tree node) _i "Config0
sat: %a
unsat: %a
todo: %a
" - StateSet.print config0.Ata.sat - StateSet.print config0.Ata.unsat - (Ata.TransList.print ~sep:"
") config0.Ata.todo) - in + TRACE(html tree node _i config0 "Entering node"); let ps = get cache tree parent in let fcs = get cache tree fc in let nss = get cache tree ns in - let is_left = node == T.first_child tree parent - and is_right = node == T.next_sibling tree parent - and has_left = fc != T.nil - and has_right = ns != T.nil - and kind = T.kind tree node - in - let config1 = - Ata.eval_trans auto fcs nss ps config0 - is_left is_right has_left has_right kind - in - let () = - TRACE( - let config1 = config1.Ata.node in - Html.trace (T.preorder tree node) _i "Config1
sat: %a
unsat: %a
todo: %a
" - StateSet.print config1.Ata.sat - StateSet.print config1.Ata.unsat - (Ata.TransList.print ~sep:"
") config1.Ata.todo) - in + let config1 = Ata.eval_trans auto fcs nss ps config0 in + + TRACE(html tree node _i config1 "Updating transitions"); + if config0 != config1 then set cache tree node config1; let () = loop fc in let fcs1 = get cache tree fc in - let config2 = - Ata.eval_trans auto - fcs1 nss ps config1 - is_left is_right has_left has_right kind - in - let () = - TRACE( - let config2 = config2.Ata.node in - Html.trace (T.preorder tree node) _i "Config2
sat: %a
unsat: %a
todo: %a
" - StateSet.print config2.Ata.sat - StateSet.print config2.Ata.unsat - (Ata.TransList.print ~sep:"
") config2.Ata.todo) - in + let config2 = Ata.eval_trans auto fcs1 nss ps config1 in + + TRACE(html tree node _i config2 "Updating transitions (after first-child)"); if config1 != config2 then set cache tree node config2; let () = loop ns in - let config3 = - Ata.eval_trans auto - fcs1 (get cache tree ns) ps config2 - is_left is_right has_left has_right kind - in - let () = - TRACE( - let config3 = config3.Ata.node in - Html.trace (T.preorder tree node) _i "Config3
sat: %a
unsat: %a
todo: %a
" - StateSet.print config3.Ata.sat - StateSet.print config3.Ata.unsat - (Ata.TransList.print ~sep:"
") config3.Ata.todo) - in + let config3 = Ata.eval_trans auto fcs1 (get cache tree ns) ps config2 in + + TRACE(html tree node _i config3 "Updating transitions (after next-sibling)"); + if config2 != config3 then set cache tree node config3; (* We do set the redo flat if : *) if not ( - !redo (* already set *) - || (Ata.TransList.nil == config3.Ata.Config.node.Ata.todo) (* no more transition to check *) - || (config0 == config3) (* did not gain any new information *) - ) + config0 == config3 (* did not gain any new information *) + || !redo (* already set *) + || Ata.TransList.nil == config3.Ata.Config.node.Ata.todo ) (* no more transition to check *) then redo := true end in @@ -151,7 +125,9 @@ END let cache = Cache.N1.create (Ata.Config.make { Ata.sat = StateSet.empty; Ata.unsat = StateSet.empty; - Ata.todo = Ata.TransList.nil }) + Ata.todo = Ata.TransList.nil; + Ata.summary = Ata.dummy_summary; + }) in let redo = ref true in let iter = ref 0 in -- 2.17.1