private void addToRenaming(Renaming renaming,HashSet<String> prevDeclared,ExprNode expr){
  if (!(expr instanceof OpApplNode)) {
    return;
  }
  HashSet<String> newDeclared=(HashSet<String>)prevDeclared.clone();
  OpApplNode node=(OpApplNode)expr;
  if (node.getUnbdedQuantSymbols() != null) {
    for (int i=0; i < node.getUnbdedQuantSymbols().length; i++) {
      FormalParamNode id=node.getUnbdedQuantSymbols()[i];
      if (newDeclared.contains(getCurrentName(id,renaming))) {
        String newname=getNewName(id,newDeclared,renaming);
        newDeclared.add(newname);
        addCurrentName(id,newname,renaming);
      }
    }
  }
  if (node.getBdedQuantSymbolLists() != null) {
    for (int i=0; i < node.getBdedQuantSymbolLists().length; i++) {
      addToRenaming(renaming,prevDeclared,node.getBdedQuantBounds()[i]);
      FormalParamNode[] nodeList=node.getBdedQuantSymbolLists()[i];
      for (int j=0; j < nodeList.length; j++) {
        FormalParamNode id=nodeList[j];
        if (newDeclared.contains(getCurrentName(id,renaming))) {
          String newname=getNewName(id,newDeclared,renaming);
          newDeclared.add(newname);
          addCurrentName(id,newname,renaming);
        }
      }
    }
  }
  for (int i=0; i < node.getArgs().length; i++) {
    if (node.getArgs()[i] instanceof ExprNode) {
      addToRenaming(renaming,newDeclared,(ExprNode)node.getArgs()[i]);
    }
  }
}

private void addToRenaming ( Renaming renaming , HashSet < String > prevDeclared , ExprNode expr ) { if ( ! ( expr instanceof OpApplNode ) ) { return ; } HashSet < String > newDeclared = ( HashSet < String > ) prevDeclared . clone ( ) ; OpApplNode node = ( OpApplNode ) expr ; if ( node . getUnbdedQuantSymbols ( ) != null ) { for ( int i = 0 ; i < node . getUnbdedQuantSymbols ( ) . length ; i ++ ) { FormalParamNode id = node . getUnbdedQuantSymbols ( ) [ i ] ; if ( newDeclared . contains ( getCurrentName ( id , renaming ) ) ) { String newname = getNewName ( id , newDeclared , renaming ) ; newDeclared . add ( newname ) ; addCurrentName ( id , newname , renaming ) ; } } } if ( node . getBdedQuantSymbolLists ( ) != null ) { for ( int i = 0 ; i < node . getBdedQuantSymbolLists ( ) . length ; i ++ ) { addToRenaming ( renaming , prevDeclared , node . getBdedQuantBounds ( ) [ i ] ) ; FormalParamNode [ ] nodeList = node . getBdedQuantSymbolLists ( ) [ i ] ; for ( int j = 0 ; j < nodeList . length ; j ++ ) { FormalParamNode id = nodeList [ j ] ; if ( newDeclared . contains ( getCurrentName ( id , renaming ) ) ) { String newname = getNewName ( id , newDeclared , renaming ) ; newDeclared . add ( newname ) ; addCurrentName ( id , newname , renaming ) ; } } } } for ( int i = 0 ; i < node . getArgs ( ) . length ; i ++ ) { if ( node . getArgs ( ) [ i ] instanceof ExprNode ) { addToRenaming ( renaming , newDeclared , ( ExprNode ) node . getArgs ( ) [ i ] ) ; } } }
adds to ` renaming ' all the renamings to bound identifiers in expr that are necessary to eliminate clashes with names in the set prevdeclared . this code was obtained by modifying the implementation of resourcehelper . innergetboundidentifiers .
