From 39cbbff37a21380c43128af0d34381804f615a62 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Sat, 22 May 2010 14:08:29 +0000 Subject: [PATCH] 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 --- src/parser/smtlib2.lex | 68 +++++++++++++++++++++++++----------------- src/parser/smtlib2.y | 37 +++++++++-------------- 2 files changed, 54 insertions(+), 51 deletions(-) diff --git a/src/parser/smtlib2.lex b/src/parser/smtlib2.lex index c9a4cef..e99e7ba 100644 --- 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; } "\n" { BEGIN INITIAL; /* return to normal mode */} . { /* stay in comment mode */ } @@ -92,15 +111,6 @@ bv{DIGIT}+ { smt2lval.str = new std::string(smt2text+2); return BVCONST_DECIMAL_ . { _string_lit.insert(_string_lit.end(),*smt2text); } -"|" { BEGIN USER_VALUE; - _string_lit.erase(_string_lit.begin(), - _string_lit.end()); } -"|" { BEGIN INITIAL; /* return to normal mode */ - smt2lval.str = new std::string(_string_lit); - return USER_VAL_TOK; } -"\n" { _string_lit.insert(_string_lit.end(),'\n');} -. { _string_lit.insert(_string_lit.end(),*smt2text); } - /* "{" { 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); } + +"|" { BEGIN USER_VALUE; + _string_lit.erase(_string_lit.begin(), + _string_lit.end()); + _string_lit.insert(_string_lit.end(),'|'); + } +"|" { 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()); + } + +"\n" { _string_lit.insert(_string_lit.end(),'\n');} +. { _string_lit.insert(_string_lit.end(),*smt2text); } + . { smt2error("Illegal input character."); } %% diff --git a/src/parser/smtlib2.y b/src/parser/smtlib2.y index ba801ee..8f9ce8e 100644 --- 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; -} ; %% -- 2.47.3