+ couldremove.retainAll(nodes);
+
+
+ /* Check for consequence nodes which are fine */
+
+ for(Iterator it=termination.consequencenodes.iterator();it.hasNext();) {
+ GraphNode gn=(GraphNode) it.next();
+ if (safetransclosure(gn, mustremove,cantremove, couldremove)) {
+ couldremove.remove(gn);
+ }
+ }
+
+ /* Check for update nodes which are fine */
+
+ for(Iterator it=termination.updatenodes.iterator();it.hasNext();) {
+ GraphNode gn=(GraphNode) it.next();
+ if (safetransclosure(gn, mustremove,cantremove, cantremove)) {
+ couldremove.remove(gn);
+ }
+ }
+
+ /* Check for conjunction nodes which are fine */
+
+ for(Iterator it=termination.conjunctions.iterator();it.hasNext();) {
+ GraphNode gn=(GraphNode) it.next();
+ if (mustremove.contains(gn)||cantremove.contains(gn))
+ continue;
+ if (!safetransclosure(gn, mustremove,cantremove, cantremove))
+ continue;
+
+ boolean allgood=true;
+ for(Iterator edgeit=gn.edges();edgeit.hasNext();) {
+ GraphNode gn2=((GraphNode.Edge)edgeit.next()).getTarget();
+ TermNode tn2=(TermNode)gn2.getOwner();
+ assert tn2.getType()==TermNode.ABSTRACT;
+ boolean foundupdate=false;
+ for(Iterator edgeit2=gn2.edges();edgeit2.hasNext();) {
+ GraphNode gn3=((GraphNode.Edge)edgeit2.next()).getTarget();
+ if (!couldremove.contains(gn3)&&!mustremove.contains(gn3)) {
+ TermNode tn3=(TermNode)gn3.getOwner();
+ if (tn3.getType()==TermNode.UPDATE)
+ foundupdate=true;
+ }
+ }
+ if (!foundupdate)
+ allgood=false;
+ }
+ if (allgood) {
+ couldremove.remove(gn);
+ if (Compiler.PRUNEQUANTIFIERS) {
+ TermNode tn=(TermNode)gn.getOwner();
+ Constraint constr=tn.getConstraint();
+ for(Iterator consit=((Set)termination.conjunctionmap.get(constr)).iterator();consit.hasNext();) {
+ GraphNode gn4=(GraphNode)consit.next();
+ TermNode tn4=(TermNode)gn4.getOwner();
+ if (tn4.getquantifiernode()) {
+ mustremove.add(gn4); /* This node is history */
+ System.out.println("Eliminating: "+gn4.getTextLabel());
+ }
+ }
+ }
+ }
+ }
+