X-Git-Url: http://git.nguyen.vg/gitweb/?p=tatoo.git;a=blobdiff_plain;f=src%2Feval.ml;h=c6d4326eb63afa04f752ab5821fb9eedcc7f9faa;hp=d90be92c094a443bb7391b2da564df562c14a6fc;hb=e3474bb976d161aa5c42f3d42583bbe290bbfcc4;hpb=acd23a33d837d03c813212ec3896a86edef16e87 diff --git a/src/eval.ml b/src/eval.ml index d90be92..c6d4326 100644 --- a/src/eval.ml +++ b/src/eval.ml @@ -14,7 +14,7 @@ (***********************************************************************) (* - Time-stamp: + Time-stamp: *) INCLUDE "utils.ml" @@ -36,43 +36,49 @@ 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 + Html.trace (T.preorder tree node) i "node: %i
%s
sat: %a
unsat: %a
todo: %around: %i
" - ((T.preorder tree node):>int) + (T.preorder tree node) msg StateSet.print config.Ata.sat StateSet.print config.Ata.unsat - (Ata.TransList.print ~sep:"
") config.Ata.todo oldi + (Ata.TransList.print ~sep:"
") config.Ata.todo i - let get c t n = Cache.N1.find c (T.preorder t n) - let set c t n v i = - v.Ata.Config.node.Ata.round <- i; - Cache.N1.add c (T.preorder t n) v - - - type run = { config : Ata.Config.t Cache.N1.t; + type run = { config : Ata.Config.t array; unstable : Bitvector.t; mutable redo : bool; mutable pass : int; } + 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 false else 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 config0 = - let c = get cache tree node in - if c == Cache.N1.dummy cache then + 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; @@ -88,36 +94,39 @@ END 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 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 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 + 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 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 + 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 set cache tree node config3 _i; + if config2 != config3 then cache.(node_id) <- config3; 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; + 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 @@ -130,9 +139,10 @@ 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 + if Ata.( + StateSet.intersect + cache.(T.preorder tree node).Config.node.sat + auto.selection_states) then node::acc1 else acc1 in loop node [] @@ -145,20 +155,16 @@ END 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@]@." + 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 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); + 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 } @@ -170,7 +176,7 @@ END stats run; run.pass <- run.pass + 1; done; - at_exit (fun () -> eprintf "@[STATS: %i iterations@]@." run.pass); + 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