X-Git-Url: http://git.nguyen.vg/gitweb/?p=tatoo.git;a=blobdiff_plain;f=src%2Feval.ml;h=d90be92c094a443bb7391b2da564df562c14a6fc;hp=22a3b5f483cdff0c0e7bc3140c8d8a2dbfce703c;hb=acd23a33d837d03c813212ec3896a86edef16e87;hpb=ff57c96ae37629bfd6ca7695653ac02b4ac013e9 diff --git a/src/eval.ml b/src/eval.ml index 22a3b5f..d90be92 100644 --- a/src/eval.ml +++ b/src/eval.ml @@ -14,7 +14,7 @@ (***********************************************************************) (* - Time-stamp: + Time-stamp: *) INCLUDE "utils.ml" @@ -38,14 +38,14 @@ END let config = config.Ata.Config.node in let oldi = config.Ata.round in Html.trace (T.preorder tree node) i oldi - "%s
sat: %a
unsat: %a
todo: %around: %i
" + "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 i = @@ -53,10 +53,19 @@ END 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 @@ -64,16 +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 @@ -87,29 +96,32 @@ END TRACE(html tree node _i config1 "Updating transitions"); if config0 != config1 then set cache tree node config1 _i; - let () = loop fc in + 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 _i; - let () = loop ns in - let config3 = Ata.eval_trans auto fcs1 (get cache tree ns) ps config2 in + 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; - (* 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 + 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 = @@ -125,27 +137,45 @@ END 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; + eprintf "@[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; - Ata.round = ~-1; - }) + 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 () -> eprintf "@[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