X-Git-Url: http://git.nguyen.vg/gitweb/?p=tatoo.git;a=blobdiff_plain;f=src%2Feval.ml;h=575ee09db0cc4614397bece43c1bf75ca1b1b4e3;hp=206debe84ce4489e69131a939bdad2f6dc1634de;hb=969febf12344a3fe3bf793a323b2e88f7b20ebae;hpb=b00bff88c7902e828804c06b7f9dc55222fdc84e diff --git a/src/eval.ml b/src/eval.ml index 206debe..575ee09 100644 --- a/src/eval.ml +++ b/src/eval.ml @@ -14,7 +14,7 @@ (***********************************************************************) (* - Time-stamp: + Time-stamp: *) INCLUDE "utils.ml" @@ -34,72 +34,94 @@ DEFINE TRACE(e) = (e) DEFINE TRACE(e) = () END + let html tree node i config msg = + let config = config.Ata.Config.node in + let oldi = config.Ata.round in + Html.trace (T.preorder tree node) i oldi + "node: %i
%s
sat: %a
unsat: %a
todo: %around: %i
" + ((T.preorder tree node):>int) + msg + StateSet.print config.Ata.sat + StateSet.print config.Ata.unsat + (Ata.TransList.print ~sep:"
") config.Ata.todo oldi - 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 set c t n v i = + v.Ata.Config.node.Ata.round <- i; + Cache.N1.add c (T.preorder t n) v - let top_down_run auto tree node cache _i = - let redo = ref false in + type run = { config : Ata.Config.t Cache.N1.t; + unstable : Bitvector.t; + mutable redo : bool; + mutable pass : int; + } + + + let top_down_run auto tree node run = + 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 + if node == T.nil then false else begin let parent = T.parent tree node in 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 () = loop fc 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 _i; + let old_unstable_left = Bitvector.unsafe_get unstable (T.preorder tree fc) in + let unstable_left = old_unstable_left && 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 () = 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) + 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 _i; + let old_unstable_right = Bitvector.unsafe_get unstable (T.preorder tree ns) in + let unstable_right = old_unstable_right && loop ns in + let nss1 = get cache tree ns 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 set cache tree node config3 _i; + 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 + Bitvector.unsafe_set unstable (T.preorder tree node) unstable_self; + unstable_self end in - loop node; - !redo + loop node let get_results auto tree node cache = let rec loop node acc = @@ -108,24 +130,53 @@ 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 StateSet.intersect + (get cache tree node).Ata.Config.node.Ata.sat + auto.Ata.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 := top_down_run auto tree node cache !iter; - incr iter; + let run = { config = Cache.N1.create + Ata.(Config.make { sat = StateSet.empty; + unsat = StateSet.empty; + todo = TransList.nil; + summary = dummy_summary; + round = ~-1 + }); + unstable = Bitvector.create ~init:true (T.size tree); + 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; - 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