X-Git-Url: http://git.nguyen.vg/gitweb/?p=tatoo.git;a=blobdiff_plain;f=src%2Feval.ml;h=d0961d70a094ed88b6b48eaff8ca3a1043a41024;hp=e8e1d5af195fb7f1a072e7e4dd2e564815391a09;hb=c6327064b172a54ee7fc03ee54d398fb34f00142;hpb=f71defc62c481fe8a3a161d904790f3ca117a8cb diff --git a/src/eval.ml b/src/eval.ml index e8e1d5a..d0961d7 100644 --- a/src/eval.ml +++ b/src/eval.ml @@ -14,7 +14,7 @@ (***********************************************************************) (* - Time-stamp: + Time-stamp: *) INCLUDE "utils.ml" @@ -62,7 +62,8 @@ END 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; + { 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 *) @@ -114,10 +115,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 - 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 [] @@ -134,11 +135,11 @@ END Ata.reset auto; while !redo do redo := false; - Ata.reset auto; + 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; done; - at_exit (fun () -> eprintf "INFO: %i iterations\n" !iter); + at_exit (fun () -> eprintf "@[STATS: %i iterations@]@." !iter); let r = get_results auto tree node cache in TRACE(Html.gen_trace (module T : Tree.S with type t = T.t) (tree)); r