From: Kim Nguyễn Date: Mon, 22 Apr 2013 13:34:39 +0000 (+0200) Subject: Merge branch 'feature/precise-sat' X-Git-Tag: v0.1~94 X-Git-Url: http://git.nguyen.vg/gitweb/?p=tatoo.git;a=commitdiff_plain;h=f71defc62c481fe8a3a161d904790f3ca117a8cb;hp=8c060c29b8d82c703065395349782b93fe7a9fd8 Merge branch 'feature/precise-sat' --- diff --git a/.gitignore b/.gitignore index 62417ef..d7eda5a 100644 --- a/.gitignore +++ b/.gitignore @@ -1,4 +1,5 @@ -_build +*.cm* +*.o *.native *.byte tests/*.results/*_tatoo* @@ -13,4 +14,3 @@ autom4te.cache config.log remake .remake - diff --git a/src/ata.ml b/src/ata.ml index c01cd50..d6aeaec 100644 --- a/src/ata.ml +++ b/src/ata.ml @@ -14,7 +14,7 @@ (***********************************************************************) (* - Time-stamp: + Time-stamp: *) INCLUDE "utils.ml" @@ -159,13 +159,72 @@ end = end + +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 +) + type t = { id : Uid.t; mutable states : StateSet.t; mutable selection_states: StateSet.t; transitions: (State.t, (QNameSet.t*SFormula.t) list) Hashtbl.t; mutable cache2 : TransList.t Cache.N2.t; - mutable cache6 : (TransList.t*StateSet.t) Cache.N6.t; + mutable cache4 : Config.t Cache.N4.t; } let next = Uid.make_maker () @@ -174,7 +233,13 @@ let dummy2 = TransList.cons (Transition.make (State.dummy,QNameSet.empty, SFormula.false_)) TransList.nil -let dummy6 = (dummy2, StateSet.empty) + + +let dummy_config = Config.make { sat = StateSet.empty; + unsat = StateSet.empty; + todo = TransList.nil; + summary = dummy_summary + } let create s ss = @@ -183,27 +248,27 @@ let create s ss = selection_states = ss; transitions = Hashtbl.create 17; cache2 = Cache.N2.create dummy2; - cache6 = Cache.N6.create dummy6; + cache4 = Cache.N4.create dummy_config; } in at_exit (fun () -> - let n6 = ref 0 in + let n4 = ref 0 in let n2 = ref 0 in Cache.N2.iteri (fun _ _ _ b -> if b then incr n2) auto.cache2; - Cache.N6.iteri (fun _ _ _ _ _ _ _ b -> if b then incr n6) auto.cache6; + Cache.N4.iteri (fun _ _ _ _ _ b -> if b then incr n4) auto.cache4; Format.eprintf "INFO: automaton %i, cache2: %i entries, cache6: %i entries\n%!" - (auto.id :> int) !n2 !n6; + (auto.id :> int) !n2 !n4; let c2l, c2u = Cache.N2.stats auto.cache2 in - let c6l, c6u = Cache.N6.stats auto.cache6 in + let c4l, c4u = Cache.N4.stats auto.cache4 in Format.eprintf "INFO: cache2: length: %i, used: %i, occupation: %f\n%!" c2l c2u (float c2u /. float c2l); - Format.eprintf "INFO: cache6: length: %i, used: %i, occupation: %f\n%!" c6l c6u (float c6u /. float c6l) + Format.eprintf "INFO: cache4: length: %i, used: %i, occupation: %f\n%!" c4l c4u (float c4u /. float c4l) ); auto let reset a = - a.cache2 <- Cache.N2.create dummy2; - a.cache6 <- Cache.N6.create dummy6 + a.cache2 <- Cache.N2.create (Cache.N2.dummy a.cache2); + a.cache4 <- Cache.N4.create (Cache.N4.dummy a.cache4) let get_trans_aux a tag states = @@ -230,7 +295,7 @@ let get_trans a tag states = else trs - +(* let eval_form phi fcs nss ps ss is_left is_right has_left has_right kind = let rec loop phi = begin match SFormula.expr phi with @@ -290,7 +355,7 @@ let eval_trans auto ltrs fcs nss ps ss is_left is_right has_left has_right kind else if SFormula.is_false new_phi then (acct, accs) else - let new_tr = Transition.make (q, lab, new_phi) in + let new_tr = Transition.make (q, lab, new_phi) in (TransList.cons new_tr acct, accs) ) ltrs (TransList.nil, ss) in @@ -303,9 +368,86 @@ let eval_trans auto ltrs fcs nss ps ss is_left is_right has_left has_right kind in loop ltrs ss +*) + +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_form 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 fcsid = (fcs.Config.id :> int) in + let nssid = (nss.Config.id :> int) in + let psid = (ps.Config.id :> int) in + let rec loop old_config = + let oid = (old_config.Config.id :> int) in + let res = + let res = Cache.N4.find auto.cache4 oid fcsid nssid psid in + if res != dummy_config then res + else + 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_form 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 + Cache.N4.add auto.cache4 oid fcsid nssid psid new_config; + new_config + in + if res == old_config then res else loop res + in + loop ss (* [add_trans a q labels f] adds a transition [(q,labels) -> f] to the diff --git a/src/ata.mli b/src/ata.mli index bb94a7c..fd75e2e 100644 --- a/src/ata.mli +++ b/src/ata.mli @@ -14,7 +14,7 @@ (***********************************************************************) (* - Time-stamp: + Time-stamp: *) type predicate = @@ -66,13 +66,26 @@ module TransList : sig end +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 + + type t = private { id : Uid.t; mutable states : StateSet.t; mutable selection_states: StateSet.t; transitions: (State.t, (QNameSet.t*SFormula.t) list) Hashtbl.t; mutable cache2 : TransList.t Cache.N2.t; - mutable cache6 : (TransList.t*StateSet.t) Cache.N6.t; + mutable cache4 : Config.t Cache.N4.t; } @@ -81,10 +94,8 @@ 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 + +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 5ebd1ec..e8e1d5a 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 @@ -50,56 +58,49 @@ END let fc = T.first_child tree node in let ns = T.next_sibling tree node in let tag = T.tag tree node in - let states0 = get cache tree node in - let trans0 = Ata.get_trans auto tag auto.Ata.states in - let () = - TRACE(Html.trace (T.preorder tree node) _i "Pre States: %a
Pre Trans: %a
" - StateSet.print states0 (Ata.TransList.print ~sep:"
") trans0) + let config0 = + 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; + 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 + + 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 trans1, states1 = - Ata.eval_trans auto trans0 - fcs nss ps states0 - is_left is_right has_left has_right kind - in - let () = - TRACE(Html.trace (T.preorder tree node) _i "TD States: %a
TD Trans: %a
" StateSet.print states1 (Ata.TransList.print ~sep:"
") trans1) - in - if states1 != states0 then set cache tree node states1; + 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 trans2, states2 = - Ata.eval_trans auto trans1 - fcs1 nss ps states1 - is_left is_right has_left has_right kind - in - let () = - TRACE(Html.trace (T.preorder tree node) _i "Left BU States: %a
Left BU Trans: %a
" StateSet.print states2 (Ata.TransList.print ~sep:"
") trans2) - in - if states2 != states1 then set cache tree node states2; + 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 _trans3, states3 = - Ata.eval_trans auto trans2 - fcs1 (get cache tree ns) ps states2 - is_left is_right has_left has_right kind - in - let () = - TRACE(Html.trace (T.preorder tree node) _i "Right BU States: %a
Right BU Trans: %a
" StateSet.print states3 (Ata.TransList.print ~sep:"
") _trans3) - in - if states3 != states2 then set cache tree node states3; - (*if states0 != states3 && (not !redo) then redo := true *) - if (not !redo) - && not (Ata.TransList.nil == _trans3) - && (states1 != states3) - && not (StateSet.intersect states3 auto.Ata.selection_states) + 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 ( + 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 @@ -113,7 +114,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) 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 @@ -121,12 +122,19 @@ END loop node [] let eval auto tree node = - let cache = Cache.N1.create StateSet.empty in + let cache = Cache.N1.create + (Ata.Config.make { Ata.sat = StateSet.empty; + Ata.unsat = StateSet.empty; + Ata.todo = Ata.TransList.nil; + Ata.summary = Ata.dummy_summary; + }) + in let redo = ref true in let iter = ref 0 in Ata.reset auto; while !redo do redo := false; + Ata.reset auto; redo := top_down_run auto tree node cache !iter; incr iter; done;