+// In some cases the analysis has determined that generating removes
+// is unnecessary
+ if (generateremove&&munremove==null)
+ generateremove=false;
+
+ Descriptor d=ep.getDescriptor();
+ if (generateremove) {
+ cr.outputline("for(;"+change.getSafeSymbol()+"<0;"+change.getSafeSymbol()+"++)");
+ cr.startblock();
+ /* Find element to remove */
+ VarDescriptor leftvar=VarDescriptor.makeNew("leftvar");
+ VarDescriptor rightvar=VarDescriptor.makeNew("rightvar");
+ if (d instanceof RelationDescriptor) {
+ if (ep.inverted()) {
+ rightvar=((ImageSetExpr)((SizeofExpr)((OpExpr)expr).left).setexpr).getVar();
+ cr.outputline("int "+leftvar.getSafeSymbol()+";");
+ cr.outputline(d.getSafeSymbol()+"_hashinv->get((int)"+rightvar.getSafeSymbol()+","+leftvar.getSafeSymbol()+");");
+ } else {
+ leftvar=((ImageSetExpr)((SizeofExpr)((OpExpr)expr).left).setexpr).getVar();
+ cr.outputline("int "+rightvar.getSafeSymbol()+"=0;");
+ cr.outputline(d.getSafeSymbol()+"_hash->get((int)"+leftvar.getSafeSymbol()+","+rightvar.getSafeSymbol()+");");
+ }
+ } else {
+ cr.outputline("int "+leftvar.getSafeSymbol()+"="+d.getSafeSymbol()+"_hash->firstkey();");
+ }
+ /* Generate abstract remove instruction */
+ if (d instanceof RelationDescriptor) {
+ RelationDescriptor rd=(RelationDescriptor) d;
+ boolean usageimage=rd.testUsage(RelationDescriptor.IMAGE);
+ boolean usageinvimage=rd.testUsage(RelationDescriptor.INVIMAGE);
+ if (usageimage)
+ cr.outputline(rd.getSafeSymbol() + "_hash->remove((int)" + leftvar.getSafeSymbol() + ", (int)" + rightvar.getSafeSymbol() + ");");
+ if (usageinvimage)
+ cr.outputline(rd.getSafeSymbol() + "_hashinv->remove((int)" + rightvar.getSafeSymbol() + ", (int)" + leftvar.getSafeSymbol() + ");");
+ } else {
+ cr.outputline(d.getSafeSymbol() + "_hash->remove((int)" + leftvar.getSafeSymbol() + ", (int)" + leftvar.getSafeSymbol() + ");");
+ }
+ /* Generate concrete remove instruction */
+ for(int i=0;i<state.vRules.size();i++) {
+ Rule r=(Rule)state.vRules.get(i);
+ if (r.getInclusion().getTargetDescriptors().contains(d)) {
+ for(int j=0;j<munremove.numUpdates();j++) {
+ UpdateNode un=munremove.getUpdate(j);
+ if (un.getRule()==r) {
+ /* Update for rule rule r */
+ String name=(String)updatenames.get(un);
+ if (d instanceof RelationDescriptor) {
+ cr.outputline(repairtable.getSafeSymbol()+"->addrelation("+d.getNum()+","+r.getNum()+","+leftvar.getSafeSymbol()+","+rightvar.getSafeSymbol()+",(int) &"+name+");");
+ } else {
+ cr.outputline(repairtable.getSafeSymbol()+"->addset("+d.getNum()+","+r.getNum()+","+leftvar.getSafeSymbol()+",(int) &"+name+");");
+ }
+ }
+ }
+ }
+ }
+ cr.endblock();
+ }
+ if (generateadd) {
+
+ cr.outputline("for(;"+change.getSafeSymbol()+">0;"+change.getSafeSymbol()+"--)");
+ cr.startblock();
+ VarDescriptor newobject=VarDescriptor.makeNew("newobject");
+ if (d instanceof RelationDescriptor) {
+ VarDescriptor otherside=((ImageSetExpr)((SizeofExpr)((OpExpr)ep.expr).left).setexpr).vd;
+ RelationDescriptor rd=(RelationDescriptor)d;
+ if (termination.sources.relsetSource(rd,!ep.inverted())) {
+ /* Set Source */
+ SetDescriptor sd=termination.sources.relgetSourceSet(rd,!ep.inverted());
+ VarDescriptor iterator=VarDescriptor.makeNew("iterator");
+ cr.outputline(sd.getType().getGenerateType().getSafeSymbol() +" "+newobject.getSafeSymbol()+";");
+ cr.outputline("for("+iterator.getSafeSymbol()+"="+sd.getSafeSymbol()+"_hash->iterator();"+iterator.getSafeSymbol()+".hasNext();)");
+ cr.startblock();
+ if (ep.inverted()) {
+ cr.outputline("if !"+rd.getSafeSymbol()+"_hashinv->contains("+iterator.getSafeSymbol()+"->key(),"+otherside.getSafeSymbol()+")");
+ } else {
+ cr.outputline("if !"+rd.getSafeSymbol()+"_hash->contains("+otherside.getSafeSymbol()+","+iterator.getSafeSymbol()+"->key())");
+ }
+ cr.outputline(newobject.getSafeSymbol()+"="+iterator.getSafeSymbol()+".key();");
+ cr.outputline(iterator.getSafeSymbol()+"->next();");
+ cr.endblock();
+ } else if (termination.sources.relallocSource(rd,!ep.inverted())) {
+ /* Allocation Source*/
+ termination.sources.relgenerateSourceAlloc(cr,newobject,rd,!ep.inverted());
+ } else throw new Error("No source for adding to Relation");
+ if (ep.inverted()) {
+ boolean usageimage=rd.testUsage(RelationDescriptor.IMAGE);
+ boolean usageinvimage=rd.testUsage(RelationDescriptor.INVIMAGE);
+ if (usageimage)
+ cr.outputline(rd.getSafeSymbol()+"_hash->add("+newobject.getSafeSymbol()+","+otherside.getSafeSymbol()+");");
+ if (usageinvimage)
+ cr.outputline(rd.getSafeSymbol()+"_hashinv->add("+otherside.getSafeSymbol()+","+newobject.getSafeSymbol()+");");
+
+ UpdateNode un=munadd.getUpdate(0);
+ String name=(String)updatenames.get(un);
+ cr.outputline(name+"(this,"+newmodel.getSafeSymbol()+","+repairtable.getSafeSymbol()+","+newobject.getSafeSymbol()+","+otherside.getSafeSymbol()+");");
+ } else {
+ boolean usageimage=rd.testUsage(RelationDescriptor.IMAGE);
+ boolean usageinvimage=rd.testUsage(RelationDescriptor.INVIMAGE);
+ if (usageimage)
+ cr.outputline(rd.getSafeSymbol()+"_hash->add("+otherside.getSafeSymbol()+","+newobject.getSafeSymbol()+");");
+ if (usageinvimage)
+ cr.outputline(rd.getSafeSymbol()+"_hashinv->add("+newobject.getSafeSymbol()+","+otherside.getSafeSymbol()+");");
+ UpdateNode un=munadd.getUpdate(0);
+ String name=(String)updatenames.get(un);
+ cr.outputline(name+"(this,"+newmodel.getSafeSymbol()+","+repairtable.getSafeSymbol()+","+otherside.getSafeSymbol()+","+newobject.getSafeSymbol()+");");
+ }
+ } else {
+ SetDescriptor sd=(SetDescriptor)d;
+ if (termination.sources.setSource(sd)) {
+ /* Set Source */
+ /* Set Source */
+ SetDescriptor sourcesd=termination.sources.getSourceSet(sd);
+ VarDescriptor iterator=VarDescriptor.makeNew("iterator");
+ cr.outputline(sourcesd.getType().getGenerateType().getSafeSymbol() +" "+newobject.getSafeSymbol()+";");
+ cr.outputline("for("+iterator.getSafeSymbol()+"="+sourcesd.getSafeSymbol()+"_hash->iterator();"+iterator.getSafeSymbol()+".hasNext();)");
+ cr.startblock();
+ cr.outputline("if !"+sd.getSafeSymbol()+"_hash->contains("+iterator.getSafeSymbol()+"->key())");
+ cr.outputline(newobject.getSafeSymbol()+"="+iterator.getSafeSymbol()+".key();");
+ cr.outputline(iterator.getSafeSymbol()+"->next();");
+ cr.endblock();
+ } else if (termination.sources.allocSource(sd)) {
+ /* Allocation Source*/
+ termination.sources.generateSourceAlloc(cr,newobject,sd);
+ } else throw new Error("No source for adding to Set");
+ cr.outputline(sd.getSafeSymbol()+"_hash->add("+newobject.getSafeSymbol()+","+newobject.getSafeSymbol()+");");
+ UpdateNode un=munadd.getUpdate(0);
+ String name=(String)updatenames.get(un);
+ cr.outputline(name+"(this,"+newmodel.getSafeSymbol()+","+repairtable.getSafeSymbol()+","+newobject.getSafeSymbol()+");");
+ }
+ cr.endblock();
+ }
+ }