docs: @Override
  public java_cup.runtime.Symbol next_token() throws java.io.IOException {
      int zzInput;
      int zzAction;
  
      // cached fields:
      int zzCurrentPosL;
      int zzMarkedPosL;
      int zzEndReadL = zzEndRead;
      char [] zzBufferL = zzBuffer;
      char [] zzCMapL = ZZ_CMAP;
  
      int [] zzTransL = ZZ_TRANS;
      int [] zzRowMapL = ZZ_ROWMAP;
      int [] zzAttrL = ZZ_ATTRIBUTE;
  
      while (true) {
        zzMarkedPosL = zzMarkedPos;
  
        yychar+= zzMarkedPosL-zzStartRead;
  
        boolean zzR = false;
        int zzCh;
        int zzCharCount;
        for (zzCurrentPosL = zzStartRead  ;
             zzCurrentPosL < zzMarkedPosL ;
             zzCurrentPosL += zzCharCount ) {
          zzCh = Character.codePointAt(zzBufferL, zzCurrentPosL, zzMarkedPosL);
          zzCharCount = Character.charCount(zzCh);
          switch (zzCh) {
          case '\u000B':
          case '\u000C':
          case '\u0085':
          case '\u2028':
          case '\u2029':
            yyline++;
            yycolumn = 0;
            zzR = false;
            break;
          case '\r':
            yyline++;
            yycolumn = 0;
            zzR = true;
            break;
          case '\n':
            if (zzR)
              zzR = false;
            else {
              yyline++;
              yycolumn = 0;
            }
            break;
          default:
            zzR = false;
            yycolumn += zzCharCount;
          }
        }
  
        if (zzR) {
          // peek one character ahead if it is \n (if we have counted one line too much)
          boolean zzPeek;
          if (zzMarkedPosL < zzEndReadL)
            zzPeek = zzBufferL[zzMarkedPosL] == '\n';
          else if (zzAtEOF)
            zzPeek = false;
          else {
            boolean eof = zzRefill();
            zzEndReadL = zzEndRead;
            zzMarkedPosL = zzMarkedPos;
            zzBufferL = zzBuffer;
            if (eof)
              zzPeek = false;
            else
              zzPeek = zzBufferL[zzMarkedPosL] == '\n';
          }
          if (zzPeek) yyline--;
        }
        zzAction = -1;
  
        zzCurrentPosL = zzCurrentPos = zzStartRead = zzMarkedPosL;
  
        zzState = ZZ_LEXSTATE[zzLexicalState];
  
        // set up zzAction for empty match case:
        int zzAttributes = zzAttrL[zzState];
        if ( (zzAttributes & 1) == 1 ) {
          zzAction = zzState;
        }
  
  
        zzForAction: {
          while (true) {
  
            if (zzCurrentPosL < zzEndReadL) {
              zzInput = Character.codePointAt(zzBufferL, zzCurrentPosL, zzEndReadL);
              zzCurrentPosL += Character.charCount(zzInput);
            }
            else if (zzAtEOF) {
              zzInput = YYEOF;
              break zzForAction;
            }
            else {
              // store back cached positions
              zzCurrentPos  = zzCurrentPosL;
              zzMarkedPos   = zzMarkedPosL;
              boolean eof = zzRefill();
              // get translated positions and possibly new buffer
              zzCurrentPosL  = zzCurrentPos;
              zzMarkedPosL   = zzMarkedPos;
              zzBufferL      = zzBuffer;
              zzEndReadL     = zzEndRead;
              if (eof) {
                zzInput = YYEOF;
                break zzForAction;
              }
              else {
                zzInput = Character.codePointAt(zzBufferL, zzCurrentPosL, zzEndReadL);
                zzCurrentPosL += Character.charCount(zzInput);
              }
            }
            int zzNext = zzTransL[ zzRowMapL[zzState] + zzCMapL[zzInput] ];
            if (zzNext == -1) break zzForAction;
            zzState = zzNext;
  
            zzAttributes = zzAttrL[zzState];
            if ( (zzAttributes & 1) == 1 ) {
              zzAction = zzState;
              zzMarkedPosL = zzCurrentPosL;
              if ( (zzAttributes & 8) == 8 ) break zzForAction;
            }
  
          }
        }
  
        // store back cached position
        zzMarkedPos = zzMarkedPosL;
  
        if (zzInput == YYEOF && zzStartRead == zzCurrentPos) {
          zzAtEOF = true;
              zzDoEOF();
            {     return new java_cup.runtime.ComplexSymbolFactory.ComplexSymbol("", Symbols.EOF);
   }
        }
        else {
          switch (zzAction < 0 ? zzAction : ZZ_ACTION[zzAction]) {
            case 1:
              { return symbol(Symbols.CONSTANT, yytext());
              }
            case 11: break;
            case 2:
              { if (includeCommentsAndWhitespace) {return symbol(Symbols2.WHITESPACE, yytext());}
              }
            case 12: break;
            case 3:
              { return symbol(Symbols.PCLOSE);
              }
            case 13: break;
            case 4:
              { if (includeCommentsAndWhitespace) {return symbol(Symbols2.COMMENT, yytext());}
              }
            case 14: break;
            case 5:
              { return symbol(Symbols.POPEN);
              }
            case 15: break;
            case 6:
              { return symbol(Symbols.VARIABLE, yytext());
              }
            case 16: break;
            case 7:
              { return symbol(Symbols.IMPLIES);
              }
            case 17: break;
            case 8:
              { return symbol(Symbols.OR);
              }
            case 18: break;
            case 9:
              { return symbol(Symbols.NOT);
              }
            case 19: break;
            case 10:
              { return symbol(Symbols.DISTINCT);
              }
            case 20: break;
            default:
              zzScanError(ZZ_NO_MATCH);
          }
        }
      }
    }