- { 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 *)
+ { 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.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 *)