1 (***********************************************************************)
5 (* Kim Nguyen, LRI UMR8623 *)
6 (* Université Paris-Sud & CNRS *)
8 (* Copyright 2010-2013 Université Paris-Sud and Centre National de la *)
9 (* Recherche Scientifique. All rights reserved. This file is *)
10 (* distributed under the terms of the GNU Lesser General Public *)
11 (* License, with the special exception on linking described in file *)
14 (***********************************************************************)
19 module Make (T : Tree.S) :
21 val eval : Ata.t -> T.t -> T.node -> T.node list
33 let html tree node i config msg =
34 let config = config.Ata.Config.node in
35 Html.trace (T.preorder tree node) i
36 "node: %i<br/>%s<br/>sat: %a<br/>unsat: %a<br/>todo: %around: %i<br/>"
37 (T.preorder tree node)
39 StateSet.print config.Ata.sat
40 StateSet.print config.Ata.unsat
41 (Ata.TransList.print ~sep:"<br/>") config.Ata.todo i
45 type run = { config : Ata.Config.t array;
46 unstable : Bitvector.t;
53 let top_down_run auto tree node run =
58 if i < 0 then Ata.dummy_config else get a i
60 if i < 0 then Ata.dummy_config else unsafe_get a i
63 let cache = run.config in
64 let unstable = run.unstable in
67 let node_id = T.preorder tree node in
68 if node == T.nil || not (Bitvector.get unstable node_id) then false else begin
69 let parent = T.parent tree node in
70 let fc = T.first_child tree node in
71 let fc_id = T.preorder tree fc in
72 let ns = T.next_sibling tree node in
73 let ns_id = T.preorder tree ns in
74 let tag = T.tag tree node in
76 let c = cache.(node_id) in
77 if c == Ata.dummy_config then
79 { c.Ata.Config.node with
80 Ata.todo = Ata.get_trans auto tag auto.Ata.states;
81 summary = Ata.node_summary
82 (node == T.first_child tree parent) (* is_left *)
83 (node == T.next_sibling tree parent) (* is_right *)
84 (fc != T.nil) (* has_left *)
85 (ns != T.nil) (* has_right *)
86 (T.kind tree node) (* kind *)
91 TRACE(html tree node _i config0 "Entering node");
93 let ps = cache.(T.preorder tree parent) in
94 let fcs = cache.(fc_id) in
95 let nss = cache.(ns_id) in
96 let config1 = Ata.eval_trans auto fcs nss ps config0 in
98 TRACE(html tree node _i config1 "Updating transitions");
100 if config0 != config1 then cache.(node_id) <- config1;
101 let unstable_left = loop fc in
102 let fcs1 = cache.(fc_id) in
103 let config2 = Ata.eval_trans auto fcs1 nss ps config1 in
105 TRACE(html tree node _i config2 "Updating transitions (after first-child)");
107 if config1 != config2 then cache.(node_id) <- config2;
108 let unstable_right = loop ns in
109 let nss1 = cache.(ns_id) in
110 let config3 = Ata.eval_trans auto fcs1 nss1 ps config2 in
112 TRACE(html tree node _i config3 "Updating transitions (after next-sibling)");
114 if config2 != config3 then cache.(node_id) <- config3;
118 || Ata.(TransList.nil != config3.Config.node.todo)
120 Bitvector.unsafe_set unstable node_id unstable_self;
121 TRACE((if not unstable_self then
125 Ata.(StateSet.intersect config3.Config.node.sat auto.selection_states)));
131 let get_results auto tree node cache =
132 let rec loop node acc =
133 if node == T.nil then acc
135 let acc0 = loop (T.next_sibling tree node) acc in
136 let acc1 = loop (T.first_child tree node) acc0 in
140 cache.(T.preorder tree node).Config.node.sat
141 auto.selection_states) then node::acc1
149 let len = Bitvector.length run.unstable in
150 for i = 0 to len - 1 do
151 if not (Bitvector.unsafe_get run.unstable i) then
155 "%i nodes over %i were skipped in iteration %i (%.2f %%), redo is: %b"
156 !count len run.pass (100. *. (float !count /. float len))
160 let eval auto tree node =
161 let len = T.size tree in
162 let run = { config = Array.create len Ata.dummy_config;
163 unstable = Bitvector.create ~init:true len;
170 Ata.reset auto; (* prevents the .cache2 and .cache4 memoization tables from growing too much *)
171 run.redo <- top_down_run auto tree node run;
173 run.pass <- run.pass + 1;
175 at_exit (fun () -> Logger.msg `STATS "%i iterations" run.pass);
176 at_exit (fun () -> stats run);
177 let r = get_results auto tree node run.config in
179 TRACE(Html.gen_trace (module T : Tree.S with type t = T.t) (tree));