- public boolean merge(Result r) {
- if (results.contains(r)) return true;
- results.add(r);
- if (fromEmptyReduction) return false;
- state.invokeReductions(phase().getToken(), this, false, r);
- return false;
+ boolean destroyed = false;
+
+ public void check() {
+ if (destroyed) return;
+ boolean dead = true;
+ // - all nodes must have a predecessor
+ // - non-doomed nodes must either:
+ // - be on the frontier or
+ // - have a non-doomed node closer to the frontier than themself
+ if (phase.isFrontier()) dead = false;
+ else for(Result r : successors)
+ if (state.doomed) { if (r.usedByAnyNode()) { dead = false; break; } }
+ else { if (r.usedByNonDoomedNode()) { dead = false; break; } }
+ dead |= results.size()==0;
+ if (!dead) return;
+ destroyed = true;
+ while(successors.size()>0)
+ for(Result r : successors) {
+ successors.remove(r);
+ r.destroy();
+ break;
+ }
+ while(results.size()>0)
+ for(Result r : results) {
+ results.remove(r);
+ r.removeSucc(this);
+ break;
+ }
+ results = null;
+ successors = null;