private static void innerGetBoundIdentifiers(Vector<FormalParamNode> vec,ExprNode expr){
  if (expr instanceof OpApplNode) {
    OpApplNode node=(OpApplNode)expr;
    if (node.getUnbdedQuantSymbols() != null) {
      for (int i=0; i < node.getUnbdedQuantSymbols().length; i++) {
        vec.add(node.getUnbdedQuantSymbols()[i]);
      }
    }
    if (node.getBdedQuantSymbolLists() != null) {
      for (int i=0; i < node.getBdedQuantSymbolLists().length; i++) {
        FormalParamNode[] nodeList=node.getBdedQuantSymbolLists()[i];
        for (int j=0; j < nodeList.length; j++) {
          vec.add(nodeList[j]);
        }
        innerGetBoundIdentifiers(vec,node.getBdedQuantBounds()[i]);
      }
    }
    for (int i=0; i < node.getArgs().length; i++) {
      if (node.getArgs()[i] instanceof ExprNode) {
        innerGetBoundIdentifiers(vec,(ExprNode)node.getArgs()[i]);
      }
    }
  }
 else   if (expr instanceof LetInNode) {
    LetInNode node=(LetInNode)expr;
    for (int i=0; i < node.getLets().length; i++) {
      OpDefNode def=node.getLets()[i];
      for (int j=0; j < def.getParams().length; j++) {
        vec.add(def.getParams()[j]);
      }
      innerGetBoundIdentifiers(vec,node.getBody());
      return;
    }
  }
 else {
    return;
  }
}

private static void innerGetBoundIdentifiers ( Vector < FormalParamNode > vec , ExprNode expr ) { if ( expr instanceof OpApplNode ) { OpApplNode node = ( OpApplNode ) expr ; if ( node . getUnbdedQuantSymbols ( ) != null ) { for ( int i = 0 ; i < node . getUnbdedQuantSymbols ( ) . length ; i ++ ) { vec . add ( node . getUnbdedQuantSymbols ( ) [ i ] ) ; } } if ( node . getBdedQuantSymbolLists ( ) != null ) { for ( int i = 0 ; i < node . getBdedQuantSymbolLists ( ) . length ; i ++ ) { FormalParamNode [ ] nodeList = node . getBdedQuantSymbolLists ( ) [ i ] ; for ( int j = 0 ; j < nodeList . length ; j ++ ) { vec . add ( nodeList [ j ] ) ; } innerGetBoundIdentifiers ( vec , node . getBdedQuantBounds ( ) [ i ] ) ; } } for ( int i = 0 ; i < node . getArgs ( ) . length ; i ++ ) { if ( node . getArgs ( ) [ i ] instanceof ExprNode ) { innerGetBoundIdentifiers ( vec , ( ExprNode ) node . getArgs ( ) [ i ] ) ; } } } else if ( expr instanceof LetInNode ) { LetInNode node = ( LetInNode ) expr ; for ( int i = 0 ; i < node . getLets ( ) . length ; i ++ ) { OpDefNode def = node . getLets ( ) [ i ] ; for ( int j = 0 ; j < def . getParams ( ) . length ; j ++ ) { vec . add ( def . getParams ( ) [ j ] ) ; } innerGetBoundIdentifiers ( vec , node . getBody ( ) ) ; return ; } } else { return ; } }
this is the recursive operator that implements getboundidentifiers . it adds the bound identifiers in expr to those in vec . the identifiers in vec should be different from the ones declared in expr .
