X-Git-Url: http://git.nguyen.vg/gitweb/?p=tatoo.git;a=blobdiff_plain;f=src%2Feval.ml;h=575ee09db0cc4614397bece43c1bf75ca1b1b4e3;hp=23d168524f8f2f922fde8cabdcdef7e92ea23bf2;hb=969febf12344a3fe3bf793a323b2e88f7b20ebae;hpb=318ebb395fe3665046b76cf4de6cf8166b94d4cc diff --git a/src/eval.ml b/src/eval.ml index 23d1685..575ee09 100644 --- a/src/eval.ml +++ b/src/eval.ml @@ -14,7 +14,7 @@ (***********************************************************************) (* - Time-stamp: + Time-stamp: *) INCLUDE "utils.ml" @@ -36,24 +36,36 @@ 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
" + 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 + (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 @@ -61,15 +73,16 @@ END 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 *) - } + 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 @@ -82,30 +95,33 @@ END TRACE(html tree node _i config1 "Updating transitions"); - if config0 != config1 then set cache tree node config1; - let () = loop fc in + 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 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 config3 = Ata.eval_trans auto fcs1 (get cache tree ns) ps config2 in + 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; - (* 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 + 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 + 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 = @@ -114,33 +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).Ata.Config.node.Ata.sat 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 - (Ata.Config.make { Ata.sat = StateSet.empty; - Ata.unsat = StateSet.empty; - Ata.todo = Ata.TransList.nil; - Ata.summary = Ata.dummy_summary; - }) + 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 - let redo = ref true in - let iter = ref 0 in - Ata.reset auto; - while !redo do - redo := false; + while run.redo do + run.redo <- false; Ata.reset auto; (* prevents the .cache2 and .cache4 memoization tables from growing too much *) - redo := top_down_run auto tree node cache !iter; - incr iter; + run.redo <- top_down_run auto tree node run; + stats run; + run.pass <- run.pass + 1; done; - at_exit (fun () -> eprintf "@[STATS: %i iterations@]@." !iter); - let r = get_results auto tree node cache in + 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