- let top_down run =
- let _i = run.pass in
- let tree = run.tree in
- let auto = run.auto in
- let status = run.status in
- let cache2 = run.cache2 in
- let cache5 = run.cache5 in
- let unstable = run.unstable in
- let init_todo = StateSet.diff (Ata.get_states auto) (Ata.get_starting_states auto) in
- let rec loop node =
- 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
- (* We enter the node from its parent *)
-
- let status0 =
- let c = unsafe_get_status status node_id in
- if c == dummy_status then
- (* first time we visit the node *)
- NodeStatus.make
- { sat = StateSet.empty;
- todo = init_todo;
- summary = NodeSummary.make
- (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
- TRACE(html tree node _i status0 "Entering node");
+module Make (T : Tree.S) (L : Node_list.S with type node = T.node) =
+ struct
+
+ let make auto tree =
+ let len = T.size tree in
+ let ba = Array1.create int16_unsigned c_layout len in
+ Array1.fill ba 0;
+ {
+ tree = tree;
+ auto = auto;
+ sat = (let a = Array.create len StateSet.empty in
+ IFHTML([a], a));
+ pass = 0;
+ fetch_trans_cache = Cache.N2.create dummy_form;
+ td_cache = Cache.N6.create dummy_set;
+ bu_cache = Cache.N6.create dummy_set;
+ node_summaries = ba;
+ stats = {
+ pass = 0;
+ tree_size = len;
+ fetch_trans_cache_access = 0;
+ fetch_trans_cache_hit = 0;
+ eval_trans_cache_access = 0;
+ eval_trans_cache_hit = 0;
+ nodes_per_run = [];
+ }
+ }
+