Move CVC parser to using strings for LET names. Removes the worst problems with names...

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

diff --git a/src/parser/cvc.lex b/src/parser/cvc.lex
index e9089a974562f71a442c9d2940de73e290e90856..1f4521ffc86014c9843b4c68d52ae0277a84ac4b 100644 (file)
--- a/src/parser/cvc.lex
+++ b/src/parser/cvc.lex
@@ -122,18 +122,34 @@ ANYTHING ({LETTER}|{DIGIT}|{OPCHAR})
 "POP"            { return POP_TOK;}
 
 (({LETTER})|(_)({ANYTHING}))({ANYTHING})*      {
-  BEEV::ASTNode nptr = parserInterface->LookupOrCreateSymbol(yytext); 
+  string str(yytext);
+   bool found = false;
+   ASTNode nptr;
+   
+  if (BEEV::parserInterface->isSymbolAlreadyDeclared(str)) // it's a symbol.
+    {
+       nptr= BEEV::parserInterface->LookupOrCreateSymbol(str);
+       found = true;
+    }
+    else if (BEEV::parserInterface->letMgr.isLetDeclared(str)) // a let.
+    {
+       nptr= BEEV::parserInterface->letMgr.resolveLet(str);
+       found = true;
+    }
 
-  // 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.  
-  cvclval.node = 
-    new BEEV::ASTNode(parserInterface->letMgr.ResolveID(nptr));
-  //cvclval.node = new BEEV::ASTNode(nptr);
-  if ((cvclval.node)->GetType() == BOOLEAN_TYPE)
-    return FORMID_TOK;
-  else 
-    return TERMID_TOK;  
+       if (found)
+       {
+         cvclval.node = BEEV::parserInterface->newNode(nptr);
+         if ((cvclval.node)->GetType() == BEEV::BOOLEAN_TYPE)
+           return FORMID_TOK;
+         else 
+           return TERMID_TOK;
+          }
+          
+    // It hasn't been found. So it's not already declared.
+    // it has not been seen before.
+       cvclval.str = strdup(yytext);
+       return STRING_TOK;
 }
 
 .                { cvcerror("Illegal input character."); }

diff --git a/src/parser/cvc.y b/src/parser/cvc.y
index 0d4221dd314d37e67c591de59b399759314736cc..050a41fe83a655869e2439c41969b7d2d2d8d82a 100644 (file)
--- a/src/parser/cvc.y
+++ b/src/parser/cvc.y
@@ -50,6 +50,7 @@
   //ASTNode,ASTVec
   BEEV::ASTNode *node;
   BEEV::ASTVec *vec;
+  vector<char*> * stringVec;
   char* str;
 
   //Hash_Map to hold Array Updates during parse A map from array index
@@ -158,8 +159,9 @@
 %nonassoc '{' '.' '('
 %nonassoc BV_TOK
 
-%type <vec>  Exprs FORM_IDs reverseFORM_IDs
-%type <vec>  Asserts 
+%type <vec>  Exprs 
+%type <vec>  Asserts
+%type <stringVec>  FORM_IDs reverseFORM_IDs  
 %type <node> Expr Formula ForDecl IfExpr ElseRestExpr IfForm ElseRestForm Assert Query ArrayUpdateExpr
 %type <Index_To_UpdateValue> Updates
 
@@ -171,6 +173,7 @@
 %token <str> BIN_BASED_NUMBER
 %token <str> DEC_BASED_NUMBER
 %token <str> HEX_BASED_NUMBER
+%token <str> STRING_TOK
 
 %%
 
@@ -280,7 +283,10 @@ Asserts         :      Assert
 }
 ;
 
-Assert          :      ASSERT_TOK Formula ';' { $$ = $2; }                
+Assert          :      ASSERT_TOK Formula ';' 
+{ 
+  $$ = $2;
+ }                
 ;
 
 Query           :      QUERY_TOK Formula ';' { parserInterface->AddQuery(*$2); $$ = $2;}
@@ -298,11 +304,12 @@ VarDecls        :      VarDecl ';'
 
 VarDecl         :      FORM_IDs ':' Type 
 {
-  for(ASTVec::iterator i=$1->begin(),iend=$1->end();i!=iend;i++) {
-    parserInterface->letMgr._parser_symbol_table.insert(*i);
-    i->SetIndexWidth($3.indexwidth);
-    i->SetValueWidth($3.valuewidth);
-    ParserBM->ListOfDeclaredVars.push_back(*i);
+  for(vector<char*>::iterator i=$1->begin(),iend=$1->end();i!=iend;i++) {
+    ASTNode s = BEEV::parserInterface->LookupOrCreateSymbol(*i);
+    s.SetIndexWidth($3.indexwidth);
+    s.SetValueWidth($3.valuewidth);
+    parserInterface->letMgr._parser_symbol_table.insert(s);
+    ParserBM->ListOfDeclaredVars.push_back(s);
   }
   delete $1;
 }
@@ -315,11 +322,7 @@ VarDecl         :      FORM_IDs ':' Type
   if($3.valuewidth != $5->GetValueWidth())
     yyerror("Fatal Error: parsing: LET Expr: Type check fail: ");
                          
-  for(ASTVec::iterator i=$1->begin(),iend=$1->end();i!=iend;i++) {                         
-    //set the valuewidth of the identifier
-    i->SetValueWidth($5->GetValueWidth());
-    i->SetIndexWidth($5->GetIndexWidth());
-                           
+  for(vector<char*>::iterator i=$1->begin(),iend=$1->end();i!=iend;i++) {                         
     parserInterface->letMgr.LetExprMgr(*i,*$5);
   }
     delete $5;
@@ -334,11 +337,7 @@ VarDecl         :      FORM_IDs ':' Type
   if($3.valuewidth != $5->GetValueWidth())
     yyerror("Fatal Error: parsing: LET Expr: Type check fail: ");
                          
-  for(ASTVec::iterator i=$1->begin(),iend=$1->end();i!=iend;i++) {                         
-    //set the valuewidth of the identifier
-    i->SetValueWidth($5->GetValueWidth());
-    i->SetIndexWidth($5->GetIndexWidth());
-                           
+  for(vector<char*>::iterator i=$1->begin(),iend=$1->end();i!=iend;i++) {                         
     parserInterface->letMgr.LetExprMgr(*i,*$5);
   }
   delete $5;
@@ -346,23 +345,23 @@ VarDecl         :      FORM_IDs ':' Type
 }                
 ;
 
-reverseFORM_IDs  :      FORMID_TOK
+reverseFORM_IDs  :      STRING_TOK
 {
-  $$ = new ASTVec;                      
-  $$->push_back(*$1);
-  delete $1;
+  $$ = new vector<char*>();                      
+  $$->push_back($1);
+ // delete $1;
 }
-|      FORMID_TOK ',' reverseFORM_IDs
+|      STRING_TOK ',' reverseFORM_IDs
 {
-  $3->push_back(*$1);
+  $3->push_back($1);
   $$ = $3;
-  delete $1;
+ // delete $1;
 }
 ;
 
 FORM_IDs         :     reverseFORM_IDs
 {
-  $$ = new ASTVec($1->rbegin(),$1->rend());
+  $$ = new vector<char*>($1->rbegin(),$1->rend());
   delete $1;
 }
 ;
@@ -693,6 +692,10 @@ ElseRestForm    :      ELSE_TOK Formula ENDIF_TOK  { $$ = $2; }
   delete $2;
   delete $4;
   delete $5;
+} | STRING_TOK
+{
+   cerr << "Unresolved symbol:" << $1 << endl;
+   yyerror("bad symbol"); 
 }
 ;
 
@@ -1064,6 +1067,10 @@ Expr            :      TERMID_TOK { $$ = new ASTNode(parserInterface->letMgr.Res
 |      LET_TOK LetDecls IN_TOK Expr
 {
   $$ = $4;
+} | STRING_TOK
+{
+   cerr << "Unresolved symbol:" << $1 << endl;
+   yyerror("bad symbol"); 
 }
 ;
 
@@ -1118,15 +1125,13 @@ LetDecls        :       LetDecl
 |       LetDecls ',' LetDecl 
 ;
 
-LetDecl         :       FORMID_TOK '=' Expr 
+LetDecl         :       STRING_TOK '=' Expr 
 {
   //Expr must typecheck
   BVTypeCheck(*$3);
 
   //set the valuewidth of the identifier
-  $1->SetValueWidth($3->GetValueWidth());
-  $1->SetIndexWidth($3->GetIndexWidth());
-
+  
   //populate the hashtable from LET-var -->
   //LET-exprs and then process them:
   //
@@ -1135,11 +1140,11 @@ LetDecl         :       FORMID_TOK '=' Expr
   //
   //2. Ensure that LET variables are not
   //2. defined more than once
-  parserInterface->letMgr.LetExprMgr(*$1,*$3);
+  parserInterface->letMgr.LetExprMgr($1,*$3);
   delete $1;
   delete $3;
 }
-|       FORMID_TOK ':' Type '=' Expr
+|       STRING_TOK ':' Type '=' Expr
 {
   //do type checking. if doesn't pass then abort
   BVTypeCheck(*$5);
@@ -1149,29 +1154,21 @@ LetDecl         :       FORMID_TOK '=' Expr
   if($3.valuewidth != $5->GetValueWidth())
     yyerror("Fatal Error: parsing: LET Expr: Type check fail: ");
 
-  //set the valuewidth of the identifier
-  $1->SetValueWidth($5->GetValueWidth());
-  $1->SetIndexWidth($5->GetIndexWidth());
-
-  parserInterface->letMgr.LetExprMgr(*$1,*$5);
+  parserInterface->letMgr.LetExprMgr($1,*$5);
   delete $1;
   delete $5;
 }
-|       FORMID_TOK '=' Formula
+|       STRING_TOK '=' Formula
 {
   //Expr must typecheck
   BVTypeCheck(*$3);
 
-  //set the valuewidth of the identifier
-  $1->SetValueWidth($3->GetValueWidth());
-  $1->SetIndexWidth($3->GetIndexWidth());
-
   //Do LET-expr management
-  parserInterface->letMgr.LetExprMgr(*$1,*$3);
+  parserInterface->letMgr.LetExprMgr($1,*$3);
   delete $1;
   delete $3;
 }
-|       FORMID_TOK ':' Type '=' Formula
+|       STRING_TOK ':' Type '=' Formula
 {
   //do type checking. if doesn't pass then abort
   BVTypeCheck(*$5);
@@ -1181,12 +1178,8 @@ LetDecl         :       FORMID_TOK '=' Expr
   if($3.valuewidth != $5->GetValueWidth())
     yyerror("Fatal Error: parsing: LET Expr: Type check fail: ");
 
-  //set the valuewidth of the identifier
-  $1->SetValueWidth($5->GetValueWidth());
-  $1->SetIndexWidth($5->GetIndexWidth());
-
   //Do LET-expr management
-  parserInterface->letMgr.LetExprMgr(*$1,*$5);
+  parserInterface->letMgr.LetExprMgr($1,*$5);
   delete $1;
   delete $5;
 }