X-Git-Url: http://git.nguyen.vg/gitweb/?p=tatoo.git;a=blobdiff_plain;f=src%2Fauto%2Feval.ml;h=4a27fa5cd8ee931242f9b293cf7141213f79fccf;hp=cc9ed71074436f9d9acf4f20ed538f8c9d6f77dd;hb=03b6a364e7240ca827585e7baff225a0aaa33bc6;hpb=9b3611f8b650edf4183169a9c2c4317e13be536d diff --git a/src/auto/eval.ml b/src/auto/eval.ml index cc9ed71..4a27fa5 100644 --- a/src/auto/eval.ml +++ b/src/auto/eval.ml @@ -14,7 +14,7 @@ (***********************************************************************) (* - Time-stamp: + Time-stamp: *) INCLUDE "utils.ml" @@ -27,87 +27,24 @@ module Make (T : Tree.Sig.S) : end = struct - type cache = StateSet.t Cache.N1.t - let get c t n = Cache.N1.find c (T.preorder t n) - let set c t n v = Cache.N1.add c (T.preorder t n) v +IFDEF HTMLTRACE + THEN +DEFINE TRACE(e) = (e) + ELSE +DEFINE TRACE(e) = () +END - module Info = struct - type t = { is_left : bool; - is_right : bool; - has_left : bool; - has_right : bool; - kind : Tree.Common.NodeKind.t; - } - let equal a b = a = b - let hash a = Hashtbl.hash a - end - module NodeInfo = Hcons.Make(Info) - let eval_form phi node_info fcs nss ps ss = - let open NodeInfo in - let open Info in - let rec loop phi = - begin match Ata.SFormula.expr phi with - Formula.True -> true - | Formula.False -> false - | Formula.Atom a -> - let p, b, q = Ata.Atom.node a in - let pos = - let open Ata in - match p with - | First_child -> StateSet.mem q fcs - | Next_sibling -> StateSet.mem q nss - | Parent | Previous_sibling -> StateSet.mem q ps - | Stay -> StateSet.mem q ss - | Is_first_child -> node_info.node.is_left - | Is_next_sibling -> node_info.node.is_right - | Is k -> k == node_info.node.kind - | Has_first_child -> node_info.node.has_left - | Has_next_sibling -> node_info.node.has_right - in - if Ata.is_move p && (not b) then - eprintf "Warning: Invalid negative atom %a" Ata.Atom.print a; - b == pos - | Formula.And(phi1, phi2) -> loop phi1 && loop phi2 - | Formula.Or (phi1, phi2) -> loop phi1 || loop phi2 - end - in - loop phi + type cache = StateSet.t Cache.N1.t + let get c t n = Cache.N1.find c (T.preorder t n) + + let set c t n v = Cache.N1.add c (T.preorder t n) v - let eval_trans cache ltrs node_info fcs nss ps ss = - let i = (ltrs.Ata.TransList.id :> int) - and j = (node_info.NodeInfo.id :> int) - and k = (fcs.StateSet.id :> int) - and l = (nss.StateSet.id :> int) - and m = (ps.StateSet.id :> int) - and n = (ss.StateSet.id :> int) in - let res = Cache.N6.find cache i j k l m n in - if res == Cache.N6.dummy cache then - let res = - Ata.TransList.fold (fun trs (acct, accs) -> - let q, _, phi = Ata.Transition.node trs in - if StateSet.mem q accs then (acct, accs) else - if eval_form phi node_info fcs nss ps accs then - (acct, StateSet.add q accs) - else - (Ata.TransList.cons trs acct, accs) - ) ltrs (Ata.TransList.nil, ss) - in - Cache.N6.add cache i j k l m n res; res - else - res let top_down_run auto tree node cache _i = let redo = ref false in - let dummy2 = Ata.TransList.cons - (Ata.Transition.make (State.dummy,QNameSet.empty, Ata.SFormula.false_)) - Ata.TransList.nil - in - let dummy6 = (dummy2, StateSet.empty) in - let trans_cache6 = Cache.N6.create 17 dummy6 in - let trans_cache2 = Cache.N2.create 17 dummy2 in let rec loop node = if node != T.nil then begin let parent = T.parent tree node in @@ -115,42 +52,48 @@ module Make (T : Tree.Sig.S) : let ns = T.next_sibling tree node in let tag = T.tag tree node in let states0 = get cache tree node in - let trans0 = - let trs = - Cache.N2.find trans_cache2 - (tag.QName.id :> int) (auto.Ata.states.StateSet.id :> int) - in - if trs == dummy2 then - let trs = Ata.get_trans auto auto.Ata.states tag in - (Cache.N2.add - trans_cache2 - (tag.QName.id :> int) - (auto.Ata.states.StateSet.id :> int) trs; trs) - else trs + 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) in let ps = get cache tree parent in let fcs = get cache tree fc in let nss = get cache tree ns in - let node_info = NodeInfo.make - (Info.({ is_left = node == T.first_child tree parent; - is_right = node == T.next_sibling tree parent; - has_left = fc != T.nil; - has_right = ns != T.nil; - kind = T.kind tree node })) + 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 = - eval_trans trans_cache6 trans0 node_info fcs nss ps states0 + 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 () = loop fc in let fcs1 = get cache tree fc in let trans2, states2 = - eval_trans trans_cache6 trans1 node_info fcs1 nss ps states1 + 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 () = loop ns in - let _, states3 = - eval_trans trans_cache6 trans2 node_info fcs1 (get cache tree ns) ps states2 + 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 @@ -174,13 +117,16 @@ module Make (T : Tree.Sig.S) : loop node [] let eval auto tree node = - let cache = Cache.N1.create (T.size tree) StateSet.empty in + let cache = Cache.N1.create StateSet.empty in let redo = ref true in let iter = ref 0 in + Ata.reset auto; while !redo do redo := top_down_run auto tree node cache !iter; incr iter; done; - get_results auto tree node cache + let r = get_results auto tree node cache in + TRACE(Html.gen_trace (module T : Tree.Sig.S with type t = T.t) (tree)); + r end