Fix the defintion of what a symbol is in the SMTLIB2 format.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@777 e59a4935-1847-0410-ae03-e826735625c1

diff --git a/src/parser/smtlib2.lex b/src/parser/smtlib2.lex
index c9a4cef012594bff4e946a0e8448f8d916263daf..e99e7ba27ba864ebe3a13b4816f0015b91038d57 100644 (file)
--- a/src/parser/smtlib2.lex
+++ b/src/parser/smtlib2.lex
@@ -48,7 +48,23 @@
     case 't': return '\t';
     default: return c;
     }
-  }      
+  }    
+   
+  static int lookup(const char* s)
+  {
+    BEEV::ASTNode nptr = BEEV::parserInterface->CreateSymbol(s); 
+
+  // Check valuesize to see if it's a prop var.  I don't like doing
+  // type determination in the lexer, but it's easier than rewriting
+  // the whole grammar to eliminate the term/formula distinction.  
+  smt2lval.node = new BEEV::ASTNode(BEEV::parserInterface->letMgr.ResolveID(nptr));
+  //smt2lval.node = new BEEV::ASTNode(nptr);
+  if ((smt2lval.node)->GetType() == BEEV::BOOLEAN_TYPE)
+    return FORMID_TOK;
+  else 
+    return TERMID_TOK;
+   }
+   
 %}
 
 %option noyywrap
@@ -63,7 +79,8 @@
 
 LETTER ([a-zA-Z])
 DIGIT  ([0-9])
-OPCHAR (['\.\_]) 
+OPCHAR ([~!@$%^&*\_\-+=<>\.?/]) 
+
 ANYTHING  ({LETTER}|{DIGIT}|{OPCHAR})
 
 %%
@@ -75,6 +92,8 @@ bv{DIGIT}+    { smt2lval.str = new std::string(smt2text+2); return BVCONST_DECIMAL_
 #b{DIGIT}+  { smt2lval.str = new std::string(smt2text+2); return BVCONST_BINARY_TOK; }
 #x(DIGIT|[a-fA-F])+  { smt2lval.str = new std::string(smt2text+2); return BVCONST_HEXIDECIMAL_TOK; }
 
+{DIGIT}+"."{DIGIT}+ { return DECIMAL_TOK;}
+
 ";"            { BEGIN COMMENT; }
 <COMMENT>"\n"  { BEGIN INITIAL; /* return to normal mode */}
 <COMMENT>.     { /* stay in comment mode */ }
@@ -92,15 +111,6 @@ bv{DIGIT}+  { smt2lval.str = new std::string(smt2text+2); return BVCONST_DECIMAL_
 
 <STRING_LITERAL>.      { _string_lit.insert(_string_lit.end(),*smt2text); }                           
 
-<INITIAL>"|"           { BEGIN USER_VALUE;
-                          _string_lit.erase(_string_lit.begin(),
-                                            _string_lit.end()); }
-<USER_VALUE>"|"                { BEGIN INITIAL; /* return to normal mode */
-                         smt2lval.str = new std::string(_string_lit);
-                          return USER_VAL_TOK; }
-<USER_VALUE>"\n"        { _string_lit.insert(_string_lit.end(),'\n');}
-<USER_VALUE>.          { _string_lit.insert(_string_lit.end(),*smt2text); }
-
 
  /*
        <INITIAL>"{"            { BEGIN USER_VALUE;
@@ -139,10 +149,8 @@ bv{DIGIT}+ { smt2lval.str = new std::string(smt2text+2); return BVCONST_DECIMAL_
 "("             { return LPAREN_TOK; }
 ")"             { return RPAREN_TOK; }
 "$"             { return DOLLAR_TOK; }
-"?"             { return QUESTION_TOK; }
+ /*"?"             { return QUESTION_TOK; }*/
 "_"             { return UNDERSCORE_TOK; }
-"\|"             { return PIPE_TOK; }
-"."             { return DOT_TOK; }
 
  /* Set info types */
 "source"        { return SOURCE_TOK;}
@@ -230,26 +238,30 @@ bv{DIGIT}+        { smt2lval.str = new std::string(smt2text+2); return BVCONST_DECIMAL_
 "sign_extend"   { return BVSX_TOK;}  
 "repeat"        { return BVREPEAT_TOK;}  
 "rotate_left"   { return BVROTATE_LEFT_TOK;} 
-"rotate_right"   { return BVROTATE_RIGHT_TOK;}  
+"rotate_right"  { return BVROTATE_RIGHT_TOK;}  
 
  /* Functions for QF_AUFBV. */
 "select"        { return SELECT_TOK; }
 "store"         { return STORE_TOK; }
 
 
-(({LETTER})|(_)({ANYTHING}))({ANYTHING})*      {
-  BEEV::ASTNode nptr = BEEV::parserInterface->CreateSymbol(smt2text); 
-
-  // Check valuesize to see if it's a prop var.  I don't like doing
-  // type determination in the lexer, but it's easier than rewriting
-  // the whole grammar to eliminate the term/formula distinction.  
-  smt2lval.node = new BEEV::ASTNode(BEEV::parserInterface->letMgr.ResolveID(nptr));
-  //smt2lval.node = new BEEV::ASTNode(nptr);
-  if ((smt2lval.node)->GetType() == BEEV::BOOLEAN_TYPE)
-    return FORMID_TOK;
-  else 
-    return TERMID_TOK;
- 
+({LETTER}|{OPCHAR})({ANYTHING})*       {
+       return lookup(smt2text);
 }
+
+<INITIAL>"|"           { BEGIN USER_VALUE;
+                          _string_lit.erase(_string_lit.begin(),
+                                            _string_lit.end());
+                         _string_lit.insert(_string_lit.end(),'|');
+                     }
+<USER_VALUE>"|"                { BEGIN INITIAL; /* return to normal mode */
+                                                 _string_lit.insert(_string_lit.end(),'|');
+                                                 smt2lval.str = new std::string(_string_lit);
+                          return lookup(_string_lit.c_str()); 
+                        }
+
+<USER_VALUE>"\n"        { _string_lit.insert(_string_lit.end(),'\n');}
+<USER_VALUE>.          { _string_lit.insert(_string_lit.end(),*smt2text); }
+
 . { smt2error("Illegal input character."); }
 %%

diff --git a/src/parser/smtlib2.y b/src/parser/smtlib2.y
index ba801ee1d91e6c054676c541a345e38c6d602a70..8f9ce8e6a1c17776875e6d738e7a41ed4a51d0ee 100644 (file)
--- a/src/parser/smtlib2.y
+++ b/src/parser/smtlib2.y
@@ -116,6 +116,7 @@
 %token DIFFICULTY_TOK
 %token VERSION_TOK
 
+%token  DECIMAL_TOK
 
 %token NOTES_TOK
 %token CVC_COMMAND_TOK
@@ -137,11 +138,9 @@
 
  /* ASCII Symbols */
 %token DOLLAR_TOK
-%token QUESTION_TOK
 %token SEMICOLON_TOK
 %token UNDERSCORE_TOK
 %token PIPE_TOK
-%token DOT_TOK
 %token COLON_TOK
 %token LPAREN_TOK
 %token RPAREN_TOK
@@ -261,7 +260,7 @@ cmdi:
        {}
 |      LPAREN_TOK NOTES_TOK attribute FORMID_TOK RPAREN_TOK
        {}
-|      LPAREN_TOK NOTES_TOK attribute NUMERAL_TOK DOT_TOK NUMERAL_TOK RPAREN_TOK
+|      LPAREN_TOK NOTES_TOK attribute DECIMAL_TOK RPAREN_TOK
        {}
 |      LPAREN_TOK NOTES_TOK attribute STRING_TOK RPAREN_TOK
        {}
@@ -672,11 +671,11 @@ lets: let lets
 | let
 {};
 
-let: LPAREN_TOK QUESTION_TOK FORMID_TOK an_formula RPAREN_TOK
+let: LPAREN_TOK FORMID_TOK an_formula RPAREN_TOK
 {
   //set the valuewidth of the identifier
-  $3->SetValueWidth($4->GetValueWidth());
-  $3->SetIndexWidth($4->GetIndexWidth());
+  $2->SetValueWidth($3->GetValueWidth());
+  $2->SetIndexWidth($3->GetIndexWidth());
       
   //populate the hashtable from LET-var -->
   //LET-exprs and then process them:
@@ -686,16 +685,16 @@ let: LPAREN_TOK QUESTION_TOK FORMID_TOK an_formula RPAREN_TOK
   //
   //2. Ensure that LET variables are not
   //2. defined more than once
-  parserInterface->letMgr.LetExprMgr(*$3,*$4);
+  parserInterface->letMgr.LetExprMgr(*$2,*$3);
   
   //delete $5;
   //delete $6;      
 }
-| LPAREN_TOK QUESTION_TOK FORMID_TOK an_term RPAREN_TOK
+| LPAREN_TOK FORMID_TOK an_term RPAREN_TOK
 {
   //set the valuewidth of the identifier
-  $3->SetValueWidth($4->GetValueWidth());
-  $3->SetIndexWidth($4->GetIndexWidth());
+  $2->SetValueWidth($3->GetValueWidth());
+  $2->SetIndexWidth($3->GetIndexWidth());
       
   //populate the hashtable from LET-var -->
   //LET-exprs and then process them:
@@ -705,7 +704,7 @@ let: LPAREN_TOK QUESTION_TOK FORMID_TOK an_formula RPAREN_TOK
   //
   //2. Ensure that LET variables are not
   //2. defined more than once
-  parserInterface->letMgr.LetExprMgr(*$3,*$4);
+  parserInterface->letMgr.LetExprMgr(*$2,*$3);
   
   //delete $5;
   //delete $6;      
@@ -1077,18 +1076,18 @@ var
   $$ = n;
       
 }
-| LPAREN_TOK UNDERSCORE_TOK BVREPEAT_TOK  NUMERAL_TOK  NUMERAL_TOK RPAREN_TOK an_term
+| LPAREN_TOK UNDERSCORE_TOK BVREPEAT_TOK  NUMERAL_TOK RPAREN_TOK an_term
 {
          unsigned count = $4;
          if (count < 1)
                FatalError("One or more repeats please");
 
-         unsigned w = $7->GetValueWidth();  
-      ASTNode n =  *$7;
+         unsigned w = $6->GetValueWidth();  
+      ASTNode n =  *$6;
       
       for (unsigned i =1; i < count; i++)
       {
-         n = parserInterface->nf->CreateTerm(BVCONCAT,w*(i+1),n,*$7);
+         n = parserInterface->nf->CreateTerm(BVCONCAT,w*(i+1),n,*$6);
       }
       $$ = new ASTNode(n);
 }
@@ -1137,10 +1136,6 @@ TERMID_TOK
   $$ = new ASTNode(parserInterface->letMgr.ResolveID(*$1));
   delete $1;
 }
-| QUESTION_TOK TERMID_TOK
-{
-  $$ = $2;
-}
 ;
 
 fvar:
@@ -1153,9 +1148,5 @@ DOLLAR_TOK FORMID_TOK
   $$ = new ASTNode(parserInterface->letMgr.ResolveID(*$1)); 
   delete $1;      
 }
-| QUESTION_TOK FORMID_TOK
-{
-  $$ = $2;
-}   
 ;
 %%