X-Git-Url: http://git.nguyen.vg/gitweb/?p=tatoo.git;a=blobdiff_plain;f=src%2Feval.ml;h=c6d4326eb63afa04f752ab5821fb9eedcc7f9faa;hp=76d9153fb969e915c04c927642fd92ad1805558c;hb=e3474bb976d161aa5c42f3d42583bbe290bbfcc4;hpb=974dacbf4f625bfd8ea83db69d6b346050141fea diff --git a/src/eval.ml b/src/eval.ml index 76d9153..c6d4326 100644 --- a/src/eval.ml +++ b/src/eval.ml @@ -14,7 +14,7 @@ (***********************************************************************) (* - Time-stamp: + Time-stamp: *) INCLUDE "utils.ml" @@ -34,77 +34,103 @@ 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 + "node: %i
%s
sat: %a
unsat: %a
todo: %around: %i
" + (T.preorder tree node) + msg + StateSet.print config.Ata.sat + StateSet.print config.Ata.unsat + (Ata.TransList.print ~sep:"
") config.Ata.todo i - 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 + type run = { config : Ata.Config.t array; + unstable : Bitvector.t; + mutable redo : bool; + mutable pass : int; + } - let top_down_run auto tree node cache _i = - let redo = ref false in + + let top_down_run auto tree node run = + let module Array = + struct + include Array + let get a i = + if i < 0 then Ata.dummy_config else get a i + let unsafe_get a i = + if i < 0 then Ata.dummy_config else unsafe_get a i + end + in + let cache = run.config in + let unstable = run.unstable in + let _i = run.pass in let rec loop node = - if node != T.nil then begin + let node_id = T.preorder tree node in + if node == T.nil || not (Bitvector.get unstable node_id) then false else begin let parent = T.parent tree node in let fc = T.first_child tree node in + let fc_id = T.preorder tree fc in let ns = T.next_sibling tree node in + let ns_id = T.preorder tree ns 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) - in - 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 () = 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 + let config0 = + let c = cache.(node_id) in + if c == Ata.dummy_config 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 - 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 _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) + + TRACE(html tree node _i config0 "Entering node"); + + let ps = cache.(T.preorder tree parent) in + let fcs = cache.(fc_id) in + let nss = cache.(ns_id) in + let config1 = Ata.eval_trans auto fcs nss ps config0 in + + TRACE(html tree node _i config1 "Updating transitions"); + + if config0 != config1 then cache.(node_id) <- config1; + let unstable_left = loop fc in + let fcs1 = cache.(fc_id) 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 cache.(node_id) <- config2; + let unstable_right = loop ns in + let nss1 = cache.(ns_id) in + let config3 = Ata.eval_trans auto fcs1 nss1 ps config2 in + + TRACE(html tree node _i config3 "Updating transitions (after next-sibling)"); + + if config2 != config3 then cache.(node_id) <- config3; + let unstable_self = + unstable_left + || unstable_right + || Ata.(TransList.nil != config3.Config.node.todo) 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) - then redo := true + Bitvector.unsafe_set unstable node_id unstable_self; + TRACE((if not unstable_self then + Html.finalize_node + node_id + _i + Ata.(StateSet.intersect config3.Config.node.sat auto.selection_states))); + unstable_self end in - loop node; - !redo + loop node let get_results auto tree node cache = let rec loop node acc = @@ -113,26 +139,49 @@ 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 - node::acc1 - else - acc1 + if Ata.( + StateSet.intersect + cache.(T.preorder tree node).Config.node.sat + auto.selection_states) then node::acc1 + else acc1 in loop node [] + + let stats run = + let count = ref 0 in + let len = Bitvector.length run.unstable in + for i = 0 to len - 1 do + if not (Bitvector.unsafe_get run.unstable i) then + incr count + done; + Logger.msg `STATS + "%i nodes over %i were skipped in iteration %i (%.2f %%), redo is: %b" + !count len run.pass (100. *. (float !count /. float len)) + run.redo + + let eval auto tree node = - 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 := false; - redo := top_down_run auto tree node cache !iter; - incr iter; + let len = T.size tree in + let run = { config = Array.create len Ata.dummy_config; + unstable = Bitvector.create ~init:true len; + redo = true; + pass = 0 + } + in + while run.redo do + run.redo <- false; + Ata.reset auto; (* prevents the .cache2 and .cache4 memoization tables from growing too much *) + run.redo <- top_down_run auto tree node run; + stats run; + run.pass <- run.pass + 1; done; - at_exit (fun () -> eprintf "INFO: %i iterations\n" !iter); - let r = get_results auto tree node cache in - TRACE(Html.gen_trace (module T : Tree.Sig.S with type t = T.t) (tree)); + at_exit (fun () -> Logger.msg `STATS "%i iterations" run.pass); + at_exit (fun () -> stats run); + let r = get_results auto tree node run.config in + + TRACE(Html.gen_trace (module T : Tree.S with type t = T.t) (tree)); + r end