- let i = run.pass in
- let tree = run.tree in
- let auto = run.auto in
- let states_by_rank = Ata.get_states_by_rank auto in
- let td_todo = states_by_rank.(i) in
- let bu_todo =
- if i == Array.length states_by_rank - 1 then StateSet.empty
- else
- states_by_rank.(i+1)
- in
- let last_run = i >= Array.length states_by_rank - 2 in
- let rec loop_td_and_bu node parent parent_sat =
- if node == T.nil then StateSet.empty
- else begin
- let tag = T.tag tree node in
- let node_id = T.preorder tree node in
- let fc = T.first_child tree node in
- let ns = T.next_sibling tree node in
- (* We enter the node from its parent *)
- let summary =
- let s = Array1.unsafe_get run.node_summaries node_id in
- if s != 0 then s else
- let s =
+ let num_visited = ref 0 in
+ let i = run.pass in
+ let tree = run.tree in
+ let auto = run.auto in
+ let states_by_rank = Ata.get_states_by_rank auto in
+ let td_todo = states_by_rank.(i) in
+ let bu_todo =
+ if i == Array.length states_by_rank - 1 then StateSet.empty
+ else
+ states_by_rank.(i+1)
+ in
+ let last_run = i >= Array.length states_by_rank - 2 in
+ let rec loop_td_and_bu node parent parent_sat =
+ if node == T.nil then StateSet.empty
+ else begin
+ incr num_visited;
+ let tag = T.tag tree node in
+ let node_id = T.preorder tree node in
+ let fc = T.first_child tree node in
+ let ns = T.next_sibling tree node in
+ (* We enter the node from its parent *)
+ let summary =
+ let s = Array1.unsafe_get run.node_summaries node_id in
+ if s != 0 then s else
+ let s =