From 6d283af68ce7a3bbd5fc0eabf442169c228dc5cd Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Wed, 23 Mar 2011 12:04:46 +0000 Subject: [PATCH] Move CVC parser to using strings for LET names. Removes the worst problems with names that haven't been defined being usable. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1231 e59a4935-1847-0410-ae03-e826735625c1 --- src/parser/cvc.lex | 38 +++++++++++++------ src/parser/cvc.y | 91 +++++++++++++++++++++------------------------- 2 files changed, 69 insertions(+), 60 deletions(-) diff --git a/src/parser/cvc.lex b/src/parser/cvc.lex index e9089a9..1f4521f 100644 --- 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 0d4221d..050a41f 100644 --- a/src/parser/cvc.y +++ b/src/parser/cvc.y @@ -50,6 +50,7 @@ //ASTNode,ASTVec BEEV::ASTNode *node; BEEV::ASTVec *vec; + vector * 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 Exprs FORM_IDs reverseFORM_IDs -%type Asserts +%type Exprs +%type Asserts +%type FORM_IDs reverseFORM_IDs %type Expr Formula ForDecl IfExpr ElseRestExpr IfForm ElseRestForm Assert Query ArrayUpdateExpr %type Updates @@ -171,6 +173,7 @@ %token BIN_BASED_NUMBER %token DEC_BASED_NUMBER %token HEX_BASED_NUMBER +%token 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::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::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::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(); + $$->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($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; } -- 2.47.3