Revert and fix

cvc5 · Jan 31, 2024 · 62249bf · 62249bf
1 parent 3ea1dc9
commit 62249bf
Show file tree

Hide file tree

Showing 2 changed files with 24 additions and 12 deletions.
diff --git a/src/expr_parser.cpp b/src/expr_parser.cpp
@@ -185,19 +185,28 @@ Expr ExprParser::parseExpr()
               // will parse a tuple term that stands for a symbolic bound
               // variable list. We do this because there are no terms that
               // begin ((... currently allowed in this parser.
-              if (d_lex.peekToken()==Token::LPAREN &&
-                  d_lex.peekToken()==Token::LPAREN)
+              tok = d_lex.nextToken();
+              if (tok==Token::LPAREN)
               {
-                nscopes = 1;
-                bool isLookup = !d_state.getOptions().d_binderFresh;
-                d_state.pushScope();
-                std::vector<Expr> vs = parseAndBindSortedVarList(isLookup);
-                if (vs.empty())
+                tok = d_lex.peekToken();
+                d_lex.reinsertToken(Token::LPAREN);
+                if (tok==Token::LPAREN)
                 {
-                  d_lex.parseError("Expected non-empty sorted variable list");
+                  nscopes = 1;
+                  bool isLookup = !d_state.getOptions().d_binderFresh;
+                  d_state.pushScope();
+                  std::vector<Expr> vs = parseAndBindSortedVarList(isLookup);
+                  if (vs.empty())
+                  {
+                    d_lex.parseError("Expected non-empty sorted variable list");
+                  }
+                  Expr vl = d_state.mkBinderList(v.getValue(), vs);
+                  args.push_back(vl);
                 }
-                Expr vl = d_state.mkBinderList(v.getValue(), vs);
-                args.push_back(vl);
+              }
+              else
+              {
+                d_lex.reinsertToken(tok);
               }
             }
             pstack.emplace_back(ParseCtx::NEXT_ARG, nscopes, args);

diff --git a/src/lexer.cpp b/src/lexer.cpp
@@ -113,13 +113,16 @@ Token Lexer::nextToken()
   {
     return nextTokenInternal();
   }
-  Token t = d_peeked[0];
-  d_peeked.erase(d_peeked.begin());
+  Token t = d_peeked.back();
+  d_peeked.pop_back();
   return t;
 }
 
 Token Lexer::peekToken()
 {
+  // since d_peeked is first in, last out, we should not peek more than once
+  // or the order is swapped.
+  Assert(d_peeked.empty());
   // parse next token
   Token t = nextTokenInternal();
   // reinsert it immediately