From 67121f5969c723a6cdb7a638fae344dc14f20751 Mon Sep 17 00:00:00 2001 From: =?utf8?q?Kim=20Nguy=E1=BB=85n?= Date: Fri, 19 Apr 2013 01:23:40 +0200 Subject: [PATCH] Hash-conses each node configuration. --- src/ata.ml | 24 +++++++++++++++--------- src/ata.mli | 13 ++++--------- src/eval.ml | 46 ++++++++++++++++++++++++++++------------------ 3 files changed, 47 insertions(+), 36 deletions(-) diff --git a/src/ata.ml b/src/ata.ml index 4d43441..919dced 100644 --- a/src/ata.ml +++ b/src/ata.ml @@ -14,7 +14,7 @@ (***********************************************************************) (* - Time-stamp: + Time-stamp: *) INCLUDE "utils.ml" @@ -304,18 +304,24 @@ 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; } -let eq_config c1 c2 = - c1.sat == c2.sat && c1.unsat == c2.unsat && c1.todo == c2.todo +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 = +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) @@ -348,9 +354,9 @@ let eval_form2 phi fcs nss ps ss is_left is_right has_left has_right kind = -let eval_trans2 auto 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 rec loop old_config = - let { sat = old_sat; unsat = old_unsat; todo = old_todo } = old_config in + 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 -> @@ -376,7 +382,7 @@ let eval_trans2 auto fcs nss ps ss is_left is_right has_left has_right kind = 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 + 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 diff --git a/src/ata.mli b/src/ata.mli index 374beb2..0b52462 100644 --- a/src/ata.mli +++ b/src/ata.mli @@ -14,7 +14,7 @@ (***********************************************************************) (* - Time-stamp: + Time-stamp: *) type predicate = @@ -81,22 +81,17 @@ val create : StateSet.t -> StateSet.t -> t val reset : t -> unit val get_trans : t -> QNameSet.elt -> StateSet.t -> TransList.t -val eval_trans : t -> TransList.t - -> StateSet.t -> StateSet.t -> StateSet.t -> StateSet.t - -> bool -> bool -> bool -> bool -> Tree.NodeKind.t - -> TransList.t*StateSet.t - type config = { sat : StateSet.t; unsat : StateSet.t; todo : TransList.t; } -val eq_config : config -> config -> bool +module Config : Hcons.S with type data = config -val eval_trans2 : t -> config -> config -> config -> config +val eval_trans : t -> Config.t -> Config.t -> Config.t -> Config.t -> bool -> bool -> bool -> bool -> Tree.NodeKind.t - -> config + -> Config.t val add_trans : t -> State.t -> QNameSet.t -> SFormula.t -> unit diff --git a/src/eval.ml b/src/eval.ml index 8f8652e..59ebc03 100644 --- a/src/eval.ml +++ b/src/eval.ml @@ -14,7 +14,7 @@ (***********************************************************************) (* - Time-stamp: + Time-stamp: *) INCLUDE "utils.ml" @@ -53,12 +53,15 @@ END let config0 = let c = get cache tree node in if c == Cache.N1.dummy cache then - { c with Ata.todo = Ata.get_trans auto tag auto.Ata.states } + Ata.Config.make + { c.Ata.Config.node with Ata.todo = Ata.get_trans auto tag auto.Ata.states } else c in let () = - TRACE(Html.trace (T.preorder tree node) _i "Config0
sat: %a
unsat: %a
todo: %a
" + 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) @@ -74,49 +77,55 @@ END and kind = T.kind tree node in let config1 = - Ata.eval_trans2 auto fcs nss ps config0 + Ata.eval_trans auto fcs nss ps config0 is_left is_right has_left has_right kind in let () = - TRACE(Html.trace (T.preorder tree node) _i "Config1
sat: %a
unsat: %a
todo: %a
" + 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 - if not (Ata.eq_config config0 config1) then set cache tree node config1; + if config0 != config1 then set cache tree node config1; let () = loop fc in let fcs1 = get cache tree fc in let config2 = - Ata.eval_trans2 auto + Ata.eval_trans auto fcs1 nss ps config1 is_left is_right has_left has_right kind in let () = - TRACE(Html.trace (T.preorder tree node) _i "Config2
sat: %a
unsat: %a
todo: %a
" + 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 - if not (Ata.eq_config config1 config2) then set cache tree node config2; + if config1 != config2 then set cache tree node config2; let () = loop ns in let config3 = - Ata.eval_trans2 auto + Ata.eval_trans auto fcs1 (get cache tree ns) ps config2 is_left is_right has_left has_right kind in let () = - TRACE(Html.trace (T.preorder tree node) _i "Config3
sat: %a
unsat: %a
todo: %a
" + 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 - if not (Ata.eq_config config2 config3) then set cache tree node config3; + 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.todo) (* no more transition to check *) - || (Ata.eq_config config0 config3) (* did not gain any new information *) + || (Ata.TransList.nil == config3.Ata.Config.node.Ata.todo) (* no more transition to check *) + || (config0 == config3) (* did not gain any new information *) ) then redo := true end @@ -131,7 +140,7 @@ END let acc0 = loop (T.next_sibling tree node) acc in let acc1 = loop (T.first_child tree node) acc0 in - if StateSet.intersect (get cache tree node).Ata.sat auto.Ata.selection_states then + if StateSet.intersect (get cache tree node).Ata.Config.node.Ata.sat auto.Ata.selection_states then node::acc1 else acc1 @@ -139,9 +148,10 @@ END loop node [] let eval auto tree node = - let cache = Cache.N1.create { Ata.sat = StateSet.empty; - Ata.unsat = StateSet.empty; - Ata.todo = Ata.TransList.nil } + let cache = Cache.N1.create + (Ata.Config.make { Ata.sat = StateSet.empty; + Ata.unsat = StateSet.empty; + Ata.todo = Ata.TransList.nil }) in let redo = ref true in let iter = ref 0 in -- 2.17.1