Fix the SMTLIB1 to not accept badly formed input. Previously if a variable wasn't...

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

diff --git a/src/parser/LetMgr.cpp b/src/parser/LetMgr.cpp
index b75ef2b42583de36cd4f8942418525bdb0ecb60d..ffb5054d824573b9861342e29ea3b36100c4759a 100644 (file)
--- a/src/parser/LetMgr.cpp
+++ b/src/parser/LetMgr.cpp
@@ -37,9 +37,16 @@ namespace BEEV {
                "cannot redeclare as a letvar: v =", var);
     }
 
+    LetExprMgr(var.GetName(),letExpr);
+  }//end of LetExprMgr()
+
+  void LETMgr::LetExprMgr(string name, const ASTNode& letExpr)
+  {
+    assert (_letid_expr_map->find(name) == _letid_expr_map->end());
     (*_letid_expr_map)[name] = letExpr;
   }//end of LetExprMgr()
 
+
   //this function looks up the "var to letexpr map" and returns the
   //corresponding letexpr. if there is no letexpr, then it simply
   //returns the var.

diff --git a/src/parser/LetMgr.h b/src/parser/LetMgr.h
index 51e3148b23765666addfb15382b0b78ed1a6ea9b..6455fba4dd7bbd25de58eafa61317afd499f281d 100644 (file)
--- a/src/parser/LetMgr.h
+++ b/src/parser/LetMgr.h
@@ -70,10 +70,18 @@ namespace BEEV
       delete _letid_expr_map;
     }
 
+    // We know for sure that it's a let.
+    ASTNode resolveLet(const string s)
+    {
+      assert(isLetDeclared(s));
+      return _letid_expr_map->find(s)->second;
+    }
+
     ASTNode ResolveID(const ASTNode& var);
       
     //Functions that are used to manage LET expressions
     void LetExprMgr(const ASTNode& var, const ASTNode& letExpr);
+    void LetExprMgr(string name, const ASTNode& letExpr);
       
     //Delete Letid Map. Called when we move onto the expression after (let ... )
     void CleanupLetIDMap(void);

diff --git a/src/parser/smt.lex b/src/parser/smt.lex
index 4fa24b73882ae431d9cbb9dc1ad54855d0da2a61..c2233326fa057f4180d4fc52ffd6e463953034db 100644 (file)
--- a/src/parser/smt.lex
+++ b/src/parser/smt.lex
@@ -220,17 +220,34 @@ bit{DIGIT}+     {
 "boolbv"        { return BOOL_TO_BV_TOK;}
 
 (({LETTER})|(_)({ANYTHING}))({ANYTHING})*      {
-  BEEV::ASTNode nptr = parserInterface->LookupOrCreateSymbol(smttext); 
-
-  // 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.  
-  smtlval.node = new BEEV::ASTNode(parserInterface->letMgr.ResolveID(nptr));
-  //smtlval.node = new BEEV::ASTNode(nptr);
-  if ((smtlval.node)->GetType() == BOOLEAN_TYPE)
-    return FORMID_TOK;
-  else 
-    return TERMID_TOK;  
+  string str(smttext);
+   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;
+    }
+
+       if (found)
+       {
+         smtlval.node = BEEV::parserInterface->newNode(nptr);
+         if ((smtlval.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.
+       smtlval.str = new std::string(str);
+       return STRING_TOK;
 }
 . { smterror("Illegal input character."); }
 %%

diff --git a/src/parser/smt.y b/src/parser/smt.y
index 37e38b5362c08ee576190b26f9d8c0eb3238b02a..ed37d5230b5caf6675af650b94b3cd21403477a6 100644 (file)
--- a/src/parser/smt.y
+++ b/src/parser/smt.y
@@ -91,11 +91,11 @@
 %type <node> status
 %type <vec> bench_attributes an_formulas an_terms
 
-%type <node> benchmark bench_name bench_attribute
+%type <node> benchmark bench_attribute
 %type <node> an_term an_nonbvconst_term an_formula 
 
-%type <node> var fvar logic_name
-%type <str> user_value
+%type <node> var fvar 
+%type <str> user_value logic_name bench_name
 
 %token <uintval> NUMERAL_TOK
 %token <str> BVCONST_TOK
@@ -254,7 +254,7 @@ LPAREN_TOK BENCHMARK_TOK bench_name bench_attributes RPAREN_TOK
 ;
 
 bench_name:
-FORMID_TOK
+STRING_TOK
 {
 }
 ;
@@ -303,10 +303,10 @@ COLON_TOK ASSUMPTION_TOK an_formula
 }
 | COLON_TOK LOGIC_TOK logic_name
 {
-  if (!(0 == strcmp($3->GetName(),"QF_UFBV")  ||
-        0 == strcmp($3->GetName(),"QF_BV") ||
-        //0 == strcmp($3->GetName(),"QF_UF") ||
-        0 == strcmp($3->GetName(),"QF_AUFBV"))) {
+  if (!(0 == strcmp($3->c_str(),"QF_UFBV")  ||
+        0 == strcmp($3->c_str(),"QF_BV") ||
+        //0 == strcmp($3->c_str(),"QF_UF") ||
+        0 == strcmp($3->c_str(),"QF_AUFBV"))) {
     yyerror("Wrong input logic:");
   }
   delete $3;
@@ -327,11 +327,11 @@ COLON_TOK ASSUMPTION_TOK an_formula
 ;
 
 logic_name:
-FORMID_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK
+STRING_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK
 {
   $$ = $1;
 }
-| FORMID_TOK
+| STRING_TOK
 {
   $$ = $1;
 }
@@ -405,34 +405,37 @@ sort_symb
 }
 ;
 
+// There are some gulwani benchmarks that create multiple variables in the same header.
+// Maybe you shouldn'.t..
 var_decls:
 var_decl
-{
-}
-//  | LPAREN_TOK var_decl RPAREN_TOK
+{}
 |
 var_decls var_decl
-{
-}
+{}
 ;
 
+
+
 var_decl:
-LPAREN_TOK FORMID_TOK sort_symbs RPAREN_TOK
+LPAREN_TOK STRING_TOK sort_symbs RPAREN_TOK
 {
-  parserInterface->letMgr._parser_symbol_table.insert(*$2);
+  ASTNode s = BEEV::parserInterface->LookupOrCreateSymbol($2->c_str());
   //Sort_symbs has the indexwidth/valuewidth. Set those fields in
   //var
-  $2->SetIndexWidth($3.indexwidth);
-  $2->SetValueWidth($3.valuewidth);
+  s.SetIndexWidth($3.indexwidth);
+  s.SetValueWidth($3.valuewidth);
+  parserInterface->letMgr._parser_symbol_table.insert(s);
   delete $2;
 }
-| LPAREN_TOK FORMID_TOK RPAREN_TOK
+| LPAREN_TOK STRING_TOK RPAREN_TOK
 {
-  parserInterface->letMgr._parser_symbol_table.insert(*$2);
+  ASTNode s = BEEV::parserInterface->LookupOrCreateSymbol($2->c_str());
+  s.SetIndexWidth(0);
+  s.SetValueWidth(0);
+  parserInterface->letMgr._parser_symbol_table.insert(s);
   //Sort_symbs has the indexwidth/valuewidth. Set those fields in
   //var
-  $2->SetIndexWidth(0);
-  $2->SetValueWidth(0);
   delete $2;
 }
 ;
@@ -627,13 +630,8 @@ TRUE_TOK
 ;
 
 letexpr_mgmt: 
-LPAREN_TOK LET_TOK LPAREN_TOK QUESTION_TOK FORMID_TOK an_term RPAREN_TOK
+LPAREN_TOK LET_TOK LPAREN_TOK QUESTION_TOK STRING_TOK an_term RPAREN_TOK
 {
-      
-  //set the valuewidth of the identifier
-  $5->SetValueWidth($6->GetValueWidth());
-  $5->SetIndexWidth($6->GetIndexWidth());
-      
   //populate the hashtable from LET-var -->
   //LET-exprs and then process them:
   //
@@ -647,14 +645,8 @@ LPAREN_TOK LET_TOK LPAREN_TOK QUESTION_TOK FORMID_TOK an_term RPAREN_TOK
   delete $5;
   delete $6;      
 }
-| LPAREN_TOK FLET_TOK LPAREN_TOK DOLLAR_TOK FORMID_TOK an_formula RPAREN_TOK 
+| LPAREN_TOK FLET_TOK LPAREN_TOK DOLLAR_TOK STRING_TOK an_formula RPAREN_TOK 
 {
-  //Expr must typecheck
-     
-  //set the valuewidth of the identifier
-  $5->SetValueWidth($6->GetValueWidth());
-  $5->SetIndexWidth($6->GetIndexWidth());
-     
   //Do LET-expr management
   parserInterface->letMgr.LetExprMgr(*$5,*$6);
   delete $5;
@@ -702,7 +694,7 @@ an_nonbvconst_term:
 BITCONST_TOK { $$ = $1; }
 | var
 {
-  $$ = new ASTNode(parserInterface->letMgr.ResolveID(*$1));
+  $$ = new ASTNode((*$1));
   delete $1;
 }
 | LPAREN_TOK an_term RPAREN_TOK
@@ -1096,12 +1088,12 @@ BITVEC_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK
 var:
 FORMID_TOK 
 {
-  $$ = new ASTNode(parserInterface->letMgr.ResolveID(*$1)); 
+  $$ = new ASTNode((*$1)); 
   delete $1;      
 }
 | TERMID_TOK
 {
-  $$ = new ASTNode(parserInterface->letMgr.ResolveID(*$1));
+  $$ = new ASTNode((*$1));
   delete $1;
 }
 | QUESTION_TOK TERMID_TOK
@@ -1117,7 +1109,7 @@ DOLLAR_TOK FORMID_TOK
 }
 | FORMID_TOK
 {
-  $$ = new ASTNode(parserInterface->letMgr.ResolveID(*$1)); 
+  $$ = new ASTNode((*$1)); 
   delete $1;      
 }   
 ;