Branch data     Line data    Source code

       1                 :            : /******************************************************************************
       2                 :            :  * This file is part of the cvc5 project.
       3                 :            :  *
       4                 :            :  * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
       5                 :            :  * in the top-level source directory and their institutional affiliations.
       6                 :            :  * All rights reserved.  See the file COPYING in the top-level source
       7                 :            :  * directory for licensing information.
       8                 :            :  * ****************************************************************************
       9                 :            :  *
      10                 :            :  * The lexer for smt2
      11                 :            :  */
      12                 :            : 
      13                 :            : #include "parser/smt2/smt2_lexer.h"
      14                 :            : 
      15                 :            : #include <cstdio>
      16                 :            : 
      17                 :            : #include "base/output.h"
      18                 :            : #include "parser/lexer.h"
      19                 :            : 
      20                 :            : namespace cvc5 {
      21                 :            : namespace parser {
      22                 :            : 
      23                 :      24382 : Smt2Lexer::Smt2Lexer(bool isStrict, bool isSygus)
      24                 :            :     : Lexer(),
      25                 :      24382 :       d_isStrict(isStrict),
      26                 :      24382 :       d_isSygus(isSygus)
      27                 :            : {
      28         [ +  + ]:     658314 :   for (int32_t ch = 'a'; ch <= 'z'; ++ch)
      29                 :            :   {
      30                 :     633932 :     d_charClass[ch] |= static_cast<uint32_t>(CharacterClass::SYMBOL_START);
      31                 :     633932 :     d_charClass[ch] |= static_cast<uint32_t>(CharacterClass::SYMBOL);
      32                 :            :   }
      33         [ +  + ]:     170674 :   for (int32_t ch = 'a'; ch <= 'f'; ++ch)
      34                 :            :   {
      35                 :     146292 :     d_charClass[ch] |= static_cast<uint32_t>(CharacterClass::HEXADECIMAL_DIGIT);
      36                 :            :   }
      37         [ +  + ]:     658314 :   for (int32_t ch = 'A'; ch <= 'Z'; ++ch)
      38                 :            :   {
      39                 :     633932 :     d_charClass[ch] |= static_cast<uint32_t>(CharacterClass::SYMBOL_START);
      40                 :     633932 :     d_charClass[ch] |= static_cast<uint32_t>(CharacterClass::SYMBOL);
      41                 :            :   }
      42         [ +  + ]:     170674 :   for (int32_t ch = 'A'; ch <= 'F'; ++ch)
      43                 :            :   {
      44                 :     146292 :     d_charClass[ch] |= static_cast<uint32_t>(CharacterClass::HEXADECIMAL_DIGIT);
      45                 :            :   }
      46         [ +  + ]:     268202 :   for (int32_t ch = '0'; ch <= '9'; ++ch)
      47                 :            :   {
      48                 :     243820 :     d_charClass[ch] |= static_cast<uint32_t>(CharacterClass::HEXADECIMAL_DIGIT);
      49                 :     243820 :     d_charClass[ch] |= static_cast<uint32_t>(CharacterClass::DECIMAL_DIGIT);
      50                 :     243820 :     d_charClass[ch] |= static_cast<uint32_t>(CharacterClass::SYMBOL);
      51                 :            :   }
      52                 :      24382 :   d_charClass['0'] |= static_cast<uint32_t>(CharacterClass::BIT);
      53                 :      24382 :   d_charClass['1'] |= static_cast<uint32_t>(CharacterClass::BIT);
      54                 :            :   // ~!@$%^&*_-+|=<>.?/
      55         [ +  + ]:     438876 :   for (int32_t ch : s_extraSymbolChars)
      56                 :            :   {
      57                 :     414494 :     d_charClass[ch] |= static_cast<uint32_t>(CharacterClass::SYMBOL_START);
      58                 :     414494 :     d_charClass[ch] |= static_cast<uint32_t>(CharacterClass::SYMBOL);
      59                 :            :   }
      60         [ +  + ]:    2413818 :   for (int32_t ch : s_printableAsciiChars)
      61                 :            :   {
      62                 :    2389436 :     d_charClass[ch] |= static_cast<uint32_t>(CharacterClass::PRINTABLE);
      63                 :            :   }
      64                 :            :   // whitespace
      65                 :      24382 :   d_charClass[' '] |= static_cast<uint32_t>(CharacterClass::WHITESPACE);
      66                 :      24382 :   d_charClass['\t'] |= static_cast<uint32_t>(CharacterClass::WHITESPACE);
      67                 :      24382 :   d_charClass['\r'] |= static_cast<uint32_t>(CharacterClass::WHITESPACE);
      68                 :      24382 :   d_charClass['\n'] |= static_cast<uint32_t>(CharacterClass::WHITESPACE);
      69                 :      24382 : }
      70                 :            : 
      71                 :   15511453 : const char* Smt2Lexer::tokenStr() const
      72                 :            : {
      73 [ +  - ][ +  - ]:   15511453 :   Assert(!d_token.empty() && d_token.back() == 0);
         [ -  + ][ -  + ]
                 [ -  - ]
      74                 :   15511453 :   return d_token.data();
      75                 :            : }
      76                 :     429442 : bool Smt2Lexer::isStrict() const { return d_isStrict; }
      77                 :      24382 : bool Smt2Lexer::isSygus() const { return d_isSygus; }
      78                 :            : 
      79                 :   33449957 : Token Smt2Lexer::nextTokenInternal()
      80                 :            : {
      81         [ +  - ]:   33449957 :   Trace("lexer-debug") << "Call nextToken" << std::endl;
      82                 :   33449957 :   d_token.clear();
      83                 :   33449957 :   Token ret = computeNextToken();
      84                 :            :   // null terminate?
      85                 :   33449951 :   d_token.push_back(0);
      86         [ +  - ]:   66899902 :   Trace("lexer-debug") << "Return nextToken " << ret << " / " << tokenStr()
      87                 :   33449951 :                        << std::endl;
      88                 :   33449951 :   return ret;
      89                 :            : }
      90                 :            : 
      91                 :   33449957 : Token Smt2Lexer::computeNextToken()
      92                 :            : {
      93                 :   33449957 :   bumpSpan();
      94                 :            :   int32_t ch;
      95                 :            :   // skip whitespace and comments
      96                 :      42090 :   for (;;)
      97                 :            :   {
      98                 :            :     do
      99                 :            :     {
     100         [ +  + ]:   51027302 :       if ((ch = nextChar()) == EOF)
     101                 :            :       {
     102                 :      21024 :         return Token::EOF_TOK;
     103                 :            :       }
     104         [ +  + ]:   51006278 :     } while (isCharacterClass(ch, CharacterClass::WHITESPACE));
     105                 :            : 
     106         [ +  + ]:   33471023 :     if (ch != ';')
     107                 :            :     {
     108                 :   33428929 :       break;
     109                 :            :     }
     110         [ +  + ]:    1083038 :     while ((ch = nextChar()) != '\n')
     111                 :            :     {
     112         [ +  + ]:    1040948 :       if (ch == EOF)
     113                 :            :       {
     114                 :          4 :         return Token::EOF_TOK;
     115                 :            :       }
     116                 :            :     }
     117                 :            :   }
     118                 :   33428929 :   bumpSpan();
     119                 :   33428929 :   pushToToken(ch);
     120 [ +  + ][ +  + ]:   33428929 :   switch (ch)
            [ +  + ][ + ]
     121                 :            :   {
     122                 :    8638955 :     case '(': return Token::LPAREN_TOK;
     123                 :    8638799 :     case ')': return Token::RPAREN_TOK;
     124                 :     238676 :     case '|':
     125                 :            :       do
     126                 :            :       {
     127                 :     251306 :         ch = nextChar();
     128         [ -  + ]:     251306 :         if (ch == EOF)
     129                 :            :         {
     130                 :          0 :           return Token::UNTERMINATED_QUOTED_SYMBOL;
     131                 :            :         }
     132                 :     251306 :         pushToToken(ch);
     133         [ +  + ]:     251306 :       } while (ch != '|');
     134                 :      12630 :       return Token::QUOTED_SYMBOL;
     135                 :      19334 :     case '#':
     136 [ +  + ][ +  - ]:      19334 :       ch = nextChar();
     137                 :            :       switch (ch)
     138                 :            :       {
     139                 :      13945 :         case 'b':
     140                 :      13945 :           pushToToken(ch);
     141                 :            :           // parse [01]+
     142         [ +  + ]:      13945 :           if (!parseNonEmptyCharList(CharacterClass::BIT))
     143                 :            :           {
     144                 :          6 :             parseError("Error expected bit string");
     145                 :            :           }
     146                 :      13943 :           return Token::BINARY_LITERAL;
     147                 :       3354 :         case 'x':
     148                 :       3354 :           pushToToken(ch);
     149                 :            :           // parse [0-9a-fA-F]+
     150         [ +  + ]:       3354 :           if (!parseNonEmptyCharList(CharacterClass::HEXADECIMAL_DIGIT))
     151                 :            :           {
     152                 :          6 :             parseError("Error expected hexadecimal string");
     153                 :            :           }
     154                 :       3352 :           return Token::HEX_LITERAL;
     155                 :       2035 :         case 'f':
     156                 :       2035 :           pushToToken(ch);
     157                 :            :           // parse [0-9]+m[0-9]+
     158         [ -  + ]:       2035 :           if (!parseNonEmptyCharList(CharacterClass::DECIMAL_DIGIT))
     159                 :            :           {
     160                 :          0 :             parseError("Error expected decimal for finite field value");
     161                 :            :           }
     162         [ -  + ]:       2035 :           if (!parseLiteralChar('m'))
     163                 :            :           {
     164                 :          0 :             parseError("Error bad syntax for finite field value");
     165                 :            :           }
     166         [ -  + ]:       2035 :           if (!parseNonEmptyCharList(CharacterClass::DECIMAL_DIGIT))
     167                 :            :           {
     168                 :          0 :             parseError("Error expected decimal for finite field size");
     169                 :            :           }
     170                 :       2035 :           return Token::FIELD_LITERAL;
     171                 :          0 :         default:
     172                 :            :           // otherwise error
     173                 :          0 :           parseError("Error finding token following #");
     174                 :          0 :           break;
     175                 :            :       }
     176                 :          0 :       break;
     177                 :     207794 :     case '"':
     178                 :            :       for (;;)
     179                 :            :       {
     180                 :     207794 :         ch = nextChar();
     181         [ -  + ]:     207794 :         if (ch == EOF)
     182                 :            :         {
     183                 :          0 :           return Token::UNTERMINATED_STRING_LITERAL;
     184                 :            :         }
     185         [ +  + ]:     207794 :         else if (!isCharacterClass(ch, CharacterClass::PRINTABLE))
     186                 :            :         {
     187                 :          3 :           parseError("Non-printable character in string literal");
     188                 :            :         }
     189         [ +  + ]:     207793 :         else if (ch == '"')
     190                 :            :         {
     191                 :      31126 :           pushToToken(ch);
     192                 :      31126 :           ch = nextChar();
     193                 :            :           // "" denotes the escape sequence for "
     194         [ +  + ]:      31126 :           if (ch != '"')
     195                 :            :           {
     196                 :      31072 :             saveChar(ch);
     197                 :      31072 :             return Token::STRING_LITERAL;
     198                 :            :           }
     199                 :            :         }
     200                 :     176721 :         pushToToken(ch);
     201                 :            :       }
     202                 :            :       break;
     203                 :      48845 :     case ':':
     204                 :            :       // parse a simple symbol
     205         [ -  + ]:      48845 :       if (!parseChar(CharacterClass::SYMBOL_START))
     206                 :            :       {
     207                 :          0 :         parseError("Error expected symbol following :");
     208                 :            :       }
     209                 :      48845 :       parseNonEmptyCharList(CharacterClass::SYMBOL);
     210                 :      48845 :       return Token::KEYWORD;
     211                 :   16039293 :     default:
     212         [ +  + ]:   16039293 :       if (isCharacterClass(ch, CharacterClass::DECIMAL_DIGIT))
     213                 :            :       {
     214                 :    1349443 :         Token res = Token::INTEGER_LITERAL;
     215                 :            :         // parse [0-9]*
     216                 :    1349443 :         parseCharList(CharacterClass::DECIMAL_DIGIT);
     217                 :            :         // maybe .[0-9]+
     218                 :    1349443 :         ch = nextChar();
     219         [ +  + ]:    1349443 :         if (ch == '.')
     220                 :            :         {
     221                 :      68681 :           pushToToken(ch);
     222                 :      68681 :           res = Token::DECIMAL_LITERAL;
     223                 :            :           // parse [0-9]+
     224         [ +  + ]:      68681 :           if (!parseNonEmptyCharList(CharacterClass::DECIMAL_DIGIT))
     225                 :            :           {
     226                 :          3 :             parseError("Error expected decimal string following .");
     227                 :            :           }
     228                 :            :         }
     229         [ +  + ]:    1280762 :         else if (ch == '/')
     230                 :            :         {
     231                 :          9 :           pushToToken(ch);
     232                 :          9 :           res = Token::RATIONAL_LITERAL;
     233                 :            :           // parse [0-9]+
     234         [ -  + ]:          9 :           if (!parseNonEmptyCharList(CharacterClass::DECIMAL_DIGIT))
     235                 :            :           {
     236                 :          0 :             parseError("Error expected decimal string following .");
     237                 :            :           }
     238                 :            :         }
     239                 :            :         else
     240                 :            :         {
     241                 :            :           // otherwise, undo
     242                 :    1280753 :           saveChar(ch);
     243                 :            :         }
     244                 :    1349442 :         return res;
     245                 :            :       }
     246         [ +  - ]:   14689850 :       else if (isCharacterClass(ch, CharacterClass::SYMBOL_START))
     247                 :            :       {
     248                 :            :         // otherwise, we are a simple symbol or standard alphanumeric token
     249                 :            :         // note that we group the case when `:` is here.
     250                 :   14689850 :         parseCharList(CharacterClass::SYMBOL);
     251                 :            :         // tokenize the current symbol, which may be a special case
     252                 :   14689850 :         return tokenizeCurrentSymbol();
     253                 :            :       }
     254                 :            :       // otherwise error
     255                 :          0 :       break;
     256                 :            :   }
     257                 :          0 :   parseError("Error finding token");
     258                 :          0 :   return Token::NONE;
     259                 :            : }
     260                 :            : 
     261                 :       2035 : bool Smt2Lexer::parseLiteralChar(int32_t chc)
     262                 :            : {
     263                 :       2035 :   int32_t ch = nextChar();
     264         [ -  + ]:       2035 :   if (ch != chc)
     265                 :            :   {
     266                 :            :     // will be an error
     267                 :          0 :     return false;
     268                 :            :   }
     269                 :       2035 :   pushToToken(ch);
     270                 :       2035 :   return true;
     271                 :            : }
     272                 :            : 
     273                 :      48845 : bool Smt2Lexer::parseChar(CharacterClass cc)
     274                 :            : {
     275                 :      48845 :   int32_t ch = nextChar();
     276         [ -  + ]:      48845 :   if (!isCharacterClass(ch, cc))
     277                 :            :   {
     278                 :            :     // will be an error
     279                 :          0 :     return false;
     280                 :            :   }
     281                 :      48845 :   pushToToken(ch);
     282                 :      48845 :   return true;
     283                 :            : }
     284                 :            : 
     285                 :     138904 : bool Smt2Lexer::parseNonEmptyCharList(CharacterClass cc)
     286                 :            : {
     287                 :            :   // must contain at least one character
     288                 :     138904 :   int32_t ch = nextChar();
     289         [ +  + ]:     138904 :   if (!isCharacterClass(ch, cc))
     290                 :            :   {
     291                 :            :     // will be an error
     292                 :          5 :     return false;
     293                 :            :   }
     294                 :     138899 :   pushToToken(ch);
     295                 :     138899 :   parseCharList(cc);
     296                 :     138899 :   return true;
     297                 :            : }
     298                 :            : 
     299                 :   69555745 : void Smt2Lexer::parseCharList(CharacterClass cc)
     300                 :            : {
     301                 :            :   int32_t ch;
     302                 :            :   for (;;)
     303                 :            :   {
     304                 :   69555745 :     ch = nextChar();
     305         [ +  + ]:   69555745 :     if (!isCharacterClass(ch, cc))
     306                 :            :     {
     307                 :            :       // failed, we are done, put the character back
     308                 :   16178192 :       saveChar(ch);
     309                 :   16178192 :       return;
     310                 :            :     }
     311                 :   53377553 :     pushToToken(ch);
     312                 :            :   }
     313                 :            : }
     314                 :            : 
     315                 :   14689850 : Token Smt2Lexer::tokenizeCurrentSymbol() const
     316                 :            : {
     317 [ -  + ][ -  + ]:   14689850 :   Assert(!d_token.empty());
                 [ -  - ]
     318 [ +  + ][ +  + ]:   14689850 :   switch (d_token[0])
         [ +  + ][ +  + ]
     319                 :            :   {
     320                 :      20808 :     case '!':
     321         [ +  + ]:      20808 :       if (d_token.size() == 1)
     322                 :            :       {
     323                 :      20744 :         return Token::ATTRIBUTE_TOK;
     324                 :            :       }
     325                 :         64 :       break;
     326                 :     783390 :     case 'a':
     327 [ +  + ][ +  + ]:     783390 :       if (d_token.size() == 2 && d_token[1] == 's')
                 [ +  + ]
     328                 :            :       {
     329                 :       2091 :         return Token::AS_TOK;
     330                 :            :       }
     331                 :     781299 :       break;
     332                 :     236657 :     case 'p':
     333 [ +  + ][ +  + ]:     236657 :       if (d_token.size() == 3 && d_token[1] == 'a' && d_token[2] == 'r')
         [ +  - ][ +  + ]
     334                 :            :       {
     335                 :        200 :         return Token::PAR_TOK;
     336                 :            :       }
     337                 :     236457 :       break;
     338                 :     271109 :     case 'l':
     339 [ +  + ][ +  + ]:     271109 :       if (d_token.size() == 3 && d_token[1] == 'e' && d_token[2] == 't')
         [ +  + ][ +  + ]
     340                 :            :       {
     341                 :     222694 :         return Token::LET_TOK;
     342                 :            :       }
     343                 :      48415 :       break;
     344                 :      17651 :     case 'm':
     345 [ +  + ][ +  + ]:      19521 :       if (d_token.size() == 5 && d_token[1] == 'a' && d_token[2] == 't'
     346 [ +  + ][ +  - ]:      19521 :           && d_token[3] == 'c' && d_token[4] == 'h')
         [ +  - ][ +  + ]
     347                 :            :       {
     348                 :        163 :         return Token::MATCH_TOK;
     349                 :            :       }
     350                 :      17488 :       break;
     351                 :    2589595 :     case '_':
     352         [ +  + ]:    2589595 :       if (d_token.size() == 1)
     353                 :            :       {
     354                 :     398303 :         return Token::INDEX_TOK;
     355                 :            :       }
     356                 :    2191292 :       break;
     357                 :     366472 :     case '-':
     358                 :            :     {
     359                 :            :       // note that `-4`, `-4.0`, `-4/5` are SMT-LIB symbols, hence we only
     360                 :            :       // convert these to literals if we are not strict parsing.
     361 [ +  + ][ +  + ]:     366472 :       if (!d_isStrict && d_token.size() >= 2)
                 [ +  + ]
     362                 :            :       {
     363                 :            :         // reparse as a negative numeral, rational or decimal
     364                 :      20025 :         Token ret = Token::INTEGER_LITERAL;
     365         [ +  + ]:      20075 :         for (size_t i = 1, tsize = d_token.size(); i < tsize; i++)
     366                 :            :         {
     367         [ +  + ]:      20043 :           if (isCharacterClass(d_token[i], CharacterClass::DECIMAL_DIGIT))
     368                 :            :           {
     369                 :         44 :             continue;
     370                 :            :           }
     371 [ +  + ][ +  - ]:      19999 :           else if (i + 1 < tsize && ret == Token::INTEGER_LITERAL)
     372                 :            :           {
     373         [ +  + ]:         73 :             if (d_token[i] == '.')
     374                 :            :             {
     375                 :          3 :               ret = Token::DECIMAL_LITERAL;
     376                 :          3 :               continue;
     377                 :            :             }
     378         [ +  + ]:         70 :             else if (d_token[i] == '/')
     379                 :            :             {
     380                 :          3 :               ret = Token::RATIONAL_LITERAL;
     381                 :          3 :               continue;
     382                 :            :             }
     383                 :            :           }
     384                 :      19993 :           return Token::SYMBOL;
     385                 :            :         }
     386                 :         32 :         return ret;
     387                 :            :       }
     388                 :            :     }
     389                 :     346447 :     break;
     390                 :   10404168 :     default: break;
     391                 :            :   }
     392                 :            :   // otherwise not a special symbol
     393                 :   14025630 :   return Token::SYMBOL;
     394                 :            : }
     395                 :            : 
     396                 :            : }  // namespace parser
     397                 :            : }  // namespace cvc5