+ and loop_td_only node =
+ if node == T.nil then () else begin
+ let node_id = T.preorder tree node in
+ 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.NodeStatus.node.rank < i then
+ (* first time we visit the node during this run *)
+ NodeStatus.make
+ { rank = i;
+ sat = c.NodeStatus.node.sat;
+ todo = td_todo;
+ summary =
+ let summary = c.NodeStatus.node.summary in
+ if summary != NodeSummary.dummy then summary
+ else
+ NodeSummary.make
+ (node != T.next_sibling tree parent)
+ (fc != T.nil) (* has_left *)
+ (ns != T.nil) (* has_right *)
+ (T.kind tree node) (* kind *)
+ }
+ else c
+ in
+ (* get the node_statuses for the first child, next sibling and parent *)
+ let ps = unsafe_get_status status (T.preorder tree parent) in
+ let fcs = unsafe_get_status status fc_id in
+ let nss = unsafe_get_status status ns_id in
+ (* evaluate the transitions with all this statuses *)
+ if status0.NodeStatus.node.todo != StateSet.empty then begin
+ let status1 = eval_trans auto fetch_trans_cache td_cache tag fcs nss ps status0 in
+ (* update the cache if the status of the node changed *)
+ if status1 != status0 then status.(node_id) <- status1;
+ end;
+ (* recursively traverse the first child *)
+ loop_td_only fc;
+ loop_td_only ns
+ end