Improvement. SMTLIB2 lets now use strings for names, not SYMBOLS.

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

diff --git a/src/parser/smt2.lex b/src/parser/smt2.lex
index 010b6431f1ade1c4012c6db7c46c09ce7b79c789..e9cffb698c74521152ba473edb9a9ac9b3c6bfc7 100644 (file)
--- a/src/parser/smt2.lex
+++ b/src/parser/smt2.lex
@@ -78,8 +78,7 @@
     }
     else if (BEEV::parserInterface->letMgr.isLetDeclared(str)) // a let.
     {
-       nptr= BEEV::parserInterface->LookupOrCreateSymbol(str);
-       nptr = BEEV::parserInterface->letMgr.ResolveID(nptr);
+       nptr = BEEV::parserInterface->letMgr.resolveLet(str);
        found = true;
     }
 
@@ -88,7 +87,7 @@
          // 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 = BEEV::parserInterface->newNode(BEEV::parserInterface->letMgr.ResolveID(nptr));
+         smt2lval.node = BEEV::parserInterface->newNode(nptr);
          if ((smt2lval.node)->GetType() == BEEV::BOOLEAN_TYPE)
            return FORMID_TOK;
          else 

diff --git a/src/parser/smt2.y b/src/parser/smt2.y
index d98b7c5f01c48425e7f6f7f066b288f226fa4e93..8371880cb4c8f9824c764a2f3fd40adc1c202bea 100644 (file)
--- a/src/parser/smt2.y
+++ b/src/parser/smt2.y
@@ -360,7 +360,7 @@ TRUE_TOK
 }
 | FORMID_TOK
 {
-  $$ = parserInterface->newNode(parserInterface->letMgr.ResolveID(*$1)); 
+  $$ = parserInterface->newNode(*$1); 
   parserInterface->deleteNode($1);      
 }
 | LPAREN_TOK EQ_TOK an_term an_term RPAREN_TOK
@@ -534,12 +534,6 @@ lets: let lets
 
 let: LPAREN_TOK STRING_TOK an_formula RPAREN_TOK
 {
-  ASTNode s = BEEV::parserInterface->LookupOrCreateSymbol($2->c_str());
-
-  //set the valuewidth of the identifier
-  s.SetValueWidth($3->GetValueWidth());
-  s.SetIndexWidth($3->GetIndexWidth());
-      
   //populate the hashtable from LET-var -->
   //LET-exprs and then process them:
   //
@@ -548,19 +542,12 @@ let: LPAREN_TOK STRING_TOK an_formula RPAREN_TOK
   //
   //2. Ensure that LET variables are not
   //2. defined more than once
-  parserInterface->letMgr.LetExprMgr(s,*$3);
-  
-       delete $2;
+  parserInterface->letMgr.LetExprMgr(*$2,*$3);
+  delete $2;
   parserInterface->deleteNode( $3);
 }
 | LPAREN_TOK STRING_TOK an_term RPAREN_TOK
 {
-  ASTNode s = BEEV::parserInterface->LookupOrCreateSymbol($2->c_str());
-
-  //set the valuewidth of the identifier
-  s.SetValueWidth($3->GetValueWidth());
-  s.SetIndexWidth($3->GetIndexWidth());
-      
   //populate the hashtable from LET-var -->
   //LET-exprs and then process them:
   //
@@ -569,9 +556,8 @@ let: LPAREN_TOK STRING_TOK an_formula RPAREN_TOK
   //
   //2. Ensure that LET variables are not
   //2. defined more than once
-  parserInterface->letMgr.LetExprMgr(s,*$3);
-  
-       delete $2;
+  parserInterface->letMgr.LetExprMgr(*$2,*$3);
+  delete $2;
   parserInterface->deleteNode( $3);
 
 }
@@ -601,7 +587,7 @@ an_terms an_term
 an_term: 
 TERMID_TOK
 {
-  $$ = parserInterface->newNode(parserInterface->letMgr.ResolveID(*$1));
+  $$ = parserInterface->newNode((*$1));
   parserInterface->deleteNode( $1);
 }
 | LPAREN_TOK an_term RPAREN_TOK