Fix lexer for symbols starting with ! (#92)

cvc5 · Nov 6, 2024 · 8619733 · 8619733
1 parent 5b74e02
commit 8619733
Show file tree

Hide file tree

Showing 3 changed files with 9 additions and 1 deletion.
diff --git a/src/lexer.cpp b/src/lexer.cpp
@@ -220,7 +220,6 @@ Token Lexer::computeNextToken()
   pushToToken(ch);
   switch (ch)
   {
-    case '!': return Token::ATTRIBUTE;
     case '(': return Token::LPAREN;
     case ')': return Token::RPAREN;
     case '|':
@@ -383,6 +382,12 @@ Token Lexer::tokenizeCurrentSymbol() const
   Assert(!d_token.empty());
   switch (d_token[0])
   {
+    case '!':
+      if (d_token.size()==1)
+      {
+        return Token::ATTRIBUTE;
+      }
+      break;
     case '-':
     {
       if (d_token.size()>=2)

diff --git a/tests/CMakeLists.txt b/tests/CMakeLists.txt
@@ -129,6 +129,7 @@ set(ethos_test_file_list
     left-cons.eo
     overload-standalone.eo
     simul-overload.eo
+    bang-lex.eo
 )
 
 if(ENABLE_ORACLES)

diff --git a/tests/bang-lex.eo b/tests/bang-lex.eo
@@ -0,0 +1,2 @@
+(declare-type Int ())
+(declare-const !x Int)