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                 :      24712 : Smt2Lexer::Smt2Lexer(bool isStrict, bool isSygus)
      24                 :      24712 :     : Lexer(), d_isStrict(isStrict), d_isSygus(isSygus)
      25                 :            : {
      26         [ +  + ]:     667224 :   for (int32_t ch = 'a'; ch <= 'z'; ++ch)
      27                 :            :   {
      28                 :     642512 :     d_charClass[ch] |= static_cast<uint32_t>(CharacterClass::SYMBOL_START);
      29                 :     642512 :     d_charClass[ch] |= static_cast<uint32_t>(CharacterClass::SYMBOL);
      30                 :            :   }
      31         [ +  + ]:     172984 :   for (int32_t ch = 'a'; ch <= 'f'; ++ch)
      32                 :            :   {
      33                 :     148272 :     d_charClass[ch] |= static_cast<uint32_t>(CharacterClass::HEXADECIMAL_DIGIT);
      34                 :            :   }
      35         [ +  + ]:     667224 :   for (int32_t ch = 'A'; ch <= 'Z'; ++ch)
      36                 :            :   {
      37                 :     642512 :     d_charClass[ch] |= static_cast<uint32_t>(CharacterClass::SYMBOL_START);
      38                 :     642512 :     d_charClass[ch] |= static_cast<uint32_t>(CharacterClass::SYMBOL);
      39                 :            :   }
      40         [ +  + ]:     172984 :   for (int32_t ch = 'A'; ch <= 'F'; ++ch)
      41                 :            :   {
      42                 :     148272 :     d_charClass[ch] |= static_cast<uint32_t>(CharacterClass::HEXADECIMAL_DIGIT);
      43                 :            :   }
      44         [ +  + ]:     271832 :   for (int32_t ch = '0'; ch <= '9'; ++ch)
      45                 :            :   {
      46                 :     247120 :     d_charClass[ch] |= static_cast<uint32_t>(CharacterClass::HEXADECIMAL_DIGIT);
      47                 :     247120 :     d_charClass[ch] |= static_cast<uint32_t>(CharacterClass::DECIMAL_DIGIT);
      48                 :     247120 :     d_charClass[ch] |= static_cast<uint32_t>(CharacterClass::SYMBOL);
      49                 :            :   }
      50                 :      24712 :   d_charClass['0'] |= static_cast<uint32_t>(CharacterClass::BIT);
      51                 :      24712 :   d_charClass['1'] |= static_cast<uint32_t>(CharacterClass::BIT);
      52                 :            :   // ~!@$%^&*_-+|=<>.?/
      53         [ +  + ]:     444816 :   for (int32_t ch : s_extraSymbolChars)
      54                 :            :   {
      55                 :     420104 :     d_charClass[ch] |= static_cast<uint32_t>(CharacterClass::SYMBOL_START);
      56                 :     420104 :     d_charClass[ch] |= static_cast<uint32_t>(CharacterClass::SYMBOL);
      57                 :            :   }
      58         [ +  + ]:    2446488 :   for (int32_t ch : s_printableAsciiChars)
      59                 :            :   {
      60                 :    2421776 :     d_charClass[ch] |= static_cast<uint32_t>(CharacterClass::PRINTABLE);
      61                 :            :   }
      62                 :            :   // whitespace
      63                 :      24712 :   d_charClass[' '] |= static_cast<uint32_t>(CharacterClass::WHITESPACE);
      64                 :      24712 :   d_charClass['\t'] |= static_cast<uint32_t>(CharacterClass::WHITESPACE);
      65                 :      24712 :   d_charClass['\r'] |= static_cast<uint32_t>(CharacterClass::WHITESPACE);
      66                 :      24712 :   d_charClass['\n'] |= static_cast<uint32_t>(CharacterClass::WHITESPACE);
      67                 :      24712 : }
      68                 :            : 
      69                 :   15524930 : const char* Smt2Lexer::tokenStr() const
      70                 :            : {
      71 [ +  - ][ +  - ]:   15524930 :   Assert(!d_token.empty() && d_token.back() == 0);
         [ -  + ][ -  + ]
                 [ -  - ]
      72                 :   15524930 :   return d_token.data();
      73                 :            : }
      74                 :     430265 : bool Smt2Lexer::isStrict() const { return d_isStrict; }
      75                 :      24712 : bool Smt2Lexer::isSygus() const { return d_isSygus; }
      76                 :            : 
      77                 :   33478872 : Token Smt2Lexer::nextTokenInternal()
      78                 :            : {
      79         [ +  - ]:   33478872 :   Trace("lexer-debug") << "Call nextToken" << std::endl;
      80                 :   33478872 :   d_token.clear();
      81                 :   33478872 :   Token ret = computeNextToken();
      82                 :            :   // null terminate?
      83                 :   33478866 :   d_token.push_back(0);
      84         [ +  - ]:   66957732 :   Trace("lexer-debug") << "Return nextToken " << ret << " / " << tokenStr()
      85                 :   33478866 :                        << std::endl;
      86                 :   33478866 :   return ret;
      87                 :            : }
      88                 :            : 
      89                 :   33478872 : Token Smt2Lexer::computeNextToken()
      90                 :            : {
      91                 :   33478872 :   bumpSpan();
      92                 :            :   int32_t ch;
      93                 :            :   // skip whitespace and comments
      94                 :      42756 :   for (;;)
      95                 :            :   {
      96                 :            :     do
      97                 :            :     {
      98         [ +  + ]:   51061340 :       if ((ch = nextChar()) == EOF)
      99                 :            :       {
     100                 :      21355 :         return Token::EOF_TOK;
     101                 :            :       }
     102         [ +  + ]:   51039985 :     } while (isCharacterClass(ch, CharacterClass::WHITESPACE));
     103                 :            : 
     104         [ +  + ]:   33500273 :     if (ch != ';')
     105                 :            :     {
     106                 :   33457513 :       break;
     107                 :            :     }
     108         [ +  + ]:    1102178 :     while ((ch = nextChar()) != '\n')
     109                 :            :     {
     110         [ +  + ]:    1059422 :       if (ch == EOF)
     111                 :            :       {
     112                 :          4 :         return Token::EOF_TOK;
     113                 :            :       }
     114                 :            :     }
     115                 :            :   }
     116                 :   33457513 :   bumpSpan();
     117                 :   33457513 :   pushToToken(ch);
     118 [ +  + ][ +  + ]:   33457513 :   switch (ch)
            [ +  + ][ + ]
     119                 :            :   {
     120                 :    8646291 :     case '(': return Token::LPAREN_TOK;
     121                 :    8646134 :     case ')': return Token::RPAREN_TOK;
     122                 :     239003 :     case '|':
     123                 :            :       do
     124                 :            :       {
     125                 :     251642 :         ch = nextChar();
     126         [ -  + ]:     251642 :         if (ch == EOF)
     127                 :            :         {
     128                 :          0 :           return Token::UNTERMINATED_QUOTED_SYMBOL;
     129                 :            :         }
     130                 :     251642 :         pushToToken(ch);
     131         [ +  + ]:     251642 :       } while (ch != '|');
     132                 :      12639 :       return Token::QUOTED_SYMBOL;
     133                 :      19511 :     case '#':
     134 [ +  + ][ +  - ]:      19511 :       ch = nextChar();
     135                 :            :       switch (ch)
     136                 :            :       {
     137                 :      14103 :         case 'b':
     138                 :      14103 :           pushToToken(ch);
     139                 :            :           // parse [01]+
     140         [ +  + ]:      14103 :           if (!parseNonEmptyCharList(CharacterClass::BIT))
     141                 :            :           {
     142                 :          6 :             parseError("Error expected bit string");
     143                 :            :           }
     144                 :      14101 :           return Token::BINARY_LITERAL;
     145                 :       3361 :         case 'x':
     146                 :       3361 :           pushToToken(ch);
     147                 :            :           // parse [0-9a-fA-F]+
     148         [ +  + ]:       3361 :           if (!parseNonEmptyCharList(CharacterClass::HEXADECIMAL_DIGIT))
     149                 :            :           {
     150                 :          6 :             parseError("Error expected hexadecimal string");
     151                 :            :           }
     152                 :       3359 :           return Token::HEX_LITERAL;
     153                 :       2047 :         case 'f':
     154                 :       2047 :           pushToToken(ch);
     155                 :            :           // parse [0-9]+m[0-9]+
     156         [ -  + ]:       2047 :           if (!parseNonEmptyCharList(CharacterClass::DECIMAL_DIGIT))
     157                 :            :           {
     158                 :          0 :             parseError("Error expected decimal for finite field value");
     159                 :            :           }
     160         [ -  + ]:       2047 :           if (!parseLiteralChar('m'))
     161                 :            :           {
     162                 :          0 :             parseError("Error bad syntax for finite field value");
     163                 :            :           }
     164         [ -  + ]:       2047 :           if (!parseNonEmptyCharList(CharacterClass::DECIMAL_DIGIT))
     165                 :            :           {
     166                 :          0 :             parseError("Error expected decimal for finite field size");
     167                 :            :           }
     168                 :       2047 :           return Token::FIELD_LITERAL;
     169                 :          0 :         default:
     170                 :            :           // otherwise error
     171                 :          0 :           parseError("Error finding token following #");
     172                 :          0 :           break;
     173                 :            :       }
     174                 :          0 :       break;
     175                 :     208131 :     case '"':
     176                 :            :       for (;;)
     177                 :            :       {
     178                 :     208131 :         ch = nextChar();
     179         [ -  + ]:     208131 :         if (ch == EOF)
     180                 :            :         {
     181                 :          0 :           return Token::UNTERMINATED_STRING_LITERAL;
     182                 :            :         }
     183         [ +  + ]:     208131 :         else if (!isCharacterClass(ch, CharacterClass::PRINTABLE))
     184                 :            :         {
     185                 :          3 :           parseError("Non-printable character in string literal");
     186                 :            :         }
     187         [ +  + ]:     208130 :         else if (ch == '"')
     188                 :            :         {
     189                 :      31351 :           pushToToken(ch);
     190                 :      31351 :           ch = nextChar();
     191                 :            :           // "" denotes the escape sequence for "
     192         [ +  + ]:      31351 :           if (ch != '"')
     193                 :            :           {
     194                 :      31297 :             saveChar(ch);
     195                 :      31297 :             return Token::STRING_LITERAL;
     196                 :            :           }
     197                 :            :         }
     198                 :     176833 :         pushToToken(ch);
     199                 :            :       }
     200                 :            :       break;
     201                 :      48900 :     case ':':
     202                 :            :       // parse a simple symbol
     203         [ -  + ]:      48900 :       if (!parseChar(CharacterClass::SYMBOL_START))
     204                 :            :       {
     205                 :          0 :         parseError("Error expected symbol following :");
     206                 :            :       }
     207                 :      48900 :       parseNonEmptyCharList(CharacterClass::SYMBOL);
     208                 :      48900 :       return Token::KEYWORD;
     209                 :   16052740 :     default:
     210         [ +  + ]:   16052740 :       if (isCharacterClass(ch, CharacterClass::DECIMAL_DIGIT))
     211                 :            :       {
     212                 :    1350517 :         Token res = Token::INTEGER_LITERAL;
     213                 :            :         // parse [0-9]*
     214                 :    1350517 :         parseCharList(CharacterClass::DECIMAL_DIGIT);
     215                 :            :         // maybe .[0-9]+
     216                 :    1350517 :         ch = nextChar();
     217         [ +  + ]:    1350517 :         if (ch == '.')
     218                 :            :         {
     219                 :      68789 :           pushToToken(ch);
     220                 :      68789 :           res = Token::DECIMAL_LITERAL;
     221                 :            :           // parse [0-9]+
     222         [ +  + ]:      68789 :           if (!parseNonEmptyCharList(CharacterClass::DECIMAL_DIGIT))
     223                 :            :           {
     224                 :          3 :             parseError("Error expected decimal string following .");
     225                 :            :           }
     226                 :            :         }
     227         [ +  + ]:    1281728 :         else if (ch == '/')
     228                 :            :         {
     229                 :          9 :           pushToToken(ch);
     230                 :          9 :           res = Token::RATIONAL_LITERAL;
     231                 :            :           // parse [0-9]+
     232         [ -  + ]:          9 :           if (!parseNonEmptyCharList(CharacterClass::DECIMAL_DIGIT))
     233                 :            :           {
     234                 :          0 :             parseError("Error expected decimal string following .");
     235                 :            :           }
     236                 :            :         }
     237                 :            :         else
     238                 :            :         {
     239                 :            :           // otherwise, undo
     240                 :    1281719 :           saveChar(ch);
     241                 :            :         }
     242                 :    1350516 :         return res;
     243                 :            :       }
     244         [ +  - ]:   14702223 :       else if (isCharacterClass(ch, CharacterClass::SYMBOL_START))
     245                 :            :       {
     246                 :            :         // otherwise, we are a simple symbol or standard alphanumeric token
     247                 :            :         // note that we group the case when `:` is here.
     248                 :   14702223 :         parseCharList(CharacterClass::SYMBOL);
     249                 :            :         // tokenize the current symbol, which may be a special case
     250                 :   14702223 :         return tokenizeCurrentSymbol();
     251                 :            :       }
     252                 :            :       // otherwise error
     253                 :          0 :       break;
     254                 :            :   }
     255                 :          0 :   parseError("Error finding token");
     256                 :          0 :   return Token::NONE;
     257                 :            : }
     258                 :            : 
     259                 :       2047 : bool Smt2Lexer::parseLiteralChar(int32_t chc)
     260                 :            : {
     261                 :       2047 :   int32_t ch = nextChar();
     262         [ -  + ]:       2047 :   if (ch != chc)
     263                 :            :   {
     264                 :            :     // will be an error
     265                 :          0 :     return false;
     266                 :            :   }
     267                 :       2047 :   pushToToken(ch);
     268                 :       2047 :   return true;
     269                 :            : }
     270                 :            : 
     271                 :      48900 : bool Smt2Lexer::parseChar(CharacterClass cc)
     272                 :            : {
     273                 :      48900 :   int32_t ch = nextChar();
     274         [ -  + ]:      48900 :   if (!isCharacterClass(ch, cc))
     275                 :            :   {
     276                 :            :     // will be an error
     277                 :          0 :     return false;
     278                 :            :   }
     279                 :      48900 :   pushToToken(ch);
     280                 :      48900 :   return true;
     281                 :            : }
     282                 :            : 
     283                 :     139256 : bool Smt2Lexer::parseNonEmptyCharList(CharacterClass cc)
     284                 :            : {
     285                 :            :   // must contain at least one character
     286                 :     139256 :   int32_t ch = nextChar();
     287         [ +  + ]:     139256 :   if (!isCharacterClass(ch, cc))
     288                 :            :   {
     289                 :            :     // will be an error
     290                 :          5 :     return false;
     291                 :            :   }
     292                 :     139251 :   pushToToken(ch);
     293                 :     139251 :   parseCharList(cc);
     294                 :     139251 :   return true;
     295                 :            : }
     296                 :            : 
     297                 :   69557153 : void Smt2Lexer::parseCharList(CharacterClass cc)
     298                 :            : {
     299                 :            :   int32_t ch;
     300                 :            :   for (;;)
     301                 :            :   {
     302                 :   69557153 :     ch = nextChar();
     303         [ +  + ]:   69557153 :     if (!isCharacterClass(ch, cc))
     304                 :            :     {
     305                 :            :       // failed, we are done, put the character back
     306                 :   16191991 :       saveChar(ch);
     307                 :   16191991 :       return;
     308                 :            :     }
     309                 :   53365162 :     pushToToken(ch);
     310                 :            :   }
     311                 :            : }
     312                 :            : 
     313                 :   14702223 : Token Smt2Lexer::tokenizeCurrentSymbol() const
     314                 :            : {
     315 [ -  + ][ -  + ]:   14702223 :   Assert(!d_token.empty());
                 [ -  - ]
     316 [ +  + ][ +  + ]:   14702223 :   switch (d_token[0])
         [ +  + ][ +  + ]
     317                 :            :   {
     318                 :      20783 :     case '!':
     319         [ +  + ]:      20783 :       if (d_token.size() == 1)
     320                 :            :       {
     321                 :      20719 :         return Token::ATTRIBUTE_TOK;
     322                 :            :       }
     323                 :         64 :       break;
     324                 :     783299 :     case 'a':
     325 [ +  + ][ +  + ]:     783299 :       if (d_token.size() == 2 && d_token[1] == 's')
                 [ +  + ]
     326                 :            :       {
     327                 :       2091 :         return Token::AS_TOK;
     328                 :            :       }
     329                 :     781208 :       break;
     330                 :     236544 :     case 'p':
     331 [ +  + ][ +  + ]:     236544 :       if (d_token.size() == 3 && d_token[1] == 'a' && d_token[2] == 'r')
         [ +  - ][ +  + ]
     332                 :            :       {
     333                 :        201 :         return Token::PAR_TOK;
     334                 :            :       }
     335                 :     236343 :       break;
     336                 :     271067 :     case 'l':
     337 [ +  + ][ +  + ]:     271067 :       if (d_token.size() == 3 && d_token[1] == 'e' && d_token[2] == 't')
         [ +  + ][ +  + ]
     338                 :            :       {
     339                 :     222599 :         return Token::LET_TOK;
     340                 :            :       }
     341                 :      48468 :       break;
     342                 :      17639 :     case 'm':
     343 [ +  + ][ +  + ]:      19510 :       if (d_token.size() == 5 && d_token[1] == 'a' && d_token[2] == 't'
     344 [ +  + ][ +  - ]:      19510 :           && d_token[3] == 'c' && d_token[4] == 'h')
         [ +  - ][ +  + ]
     345                 :            :       {
     346                 :        164 :         return Token::MATCH_TOK;
     347                 :            :       }
     348                 :      17475 :       break;
     349                 :    2596621 :     case '_':
     350         [ +  + ]:    2596621 :       if (d_token.size() == 1)
     351                 :            :       {
     352                 :     398845 :         return Token::INDEX_TOK;
     353                 :            :       }
     354                 :    2197776 :       break;
     355                 :     366501 :     case '-':
     356                 :            :     {
     357                 :            :       // note that `-4`, `-4.0`, `-4/5` are SMT-LIB symbols, hence we only
     358                 :            :       // convert these to literals if we are not strict parsing.
     359 [ +  + ][ +  + ]:     366501 :       if (!d_isStrict && d_token.size() >= 2)
                 [ +  + ]
     360                 :            :       {
     361                 :            :         // reparse as a negative numeral, rational or decimal
     362                 :      20026 :         Token ret = Token::INTEGER_LITERAL;
     363         [ +  + ]:      20083 :         for (size_t i = 1, tsize = d_token.size(); i < tsize; i++)
     364                 :            :         {
     365         [ +  + ]:      20044 :           if (isCharacterClass(d_token[i], CharacterClass::DECIMAL_DIGIT))
     366                 :            :           {
     367                 :         51 :             continue;
     368                 :            :           }
     369 [ +  + ][ +  - ]:      19993 :           else if (i + 1 < tsize && ret == Token::INTEGER_LITERAL)
     370                 :            :           {
     371         [ +  + ]:         91 :             if (d_token[i] == '.')
     372                 :            :             {
     373                 :          3 :               ret = Token::DECIMAL_LITERAL;
     374                 :          3 :               continue;
     375                 :            :             }
     376         [ +  + ]:         88 :             else if (d_token[i] == '/')
     377                 :            :             {
     378                 :          3 :               ret = Token::RATIONAL_LITERAL;
     379                 :          3 :               continue;
     380                 :            :             }
     381                 :            :           }
     382                 :      19987 :           return Token::SYMBOL;
     383                 :            :         }
     384                 :         39 :         return ret;
     385                 :            :       }
     386                 :            :     }
     387                 :     346475 :     break;
     388                 :   10409769 :     default: break;
     389                 :            :   }
     390                 :            :   // otherwise not a special symbol
     391                 :   14037578 :   return Token::SYMBOL;
     392                 :            : }
     393                 :            : 
     394                 :            : }  // namespace parser
     395                 :            : }  // namespace cvc5