From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Wed, 23 Mar 2011 05:58:12 +0000 (+0000)
Subject: Improvement. SMTLIB2 lets now use strings for names, not SYMBOLS.
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=6fa8d6bd4e6c46363a78be5a113ea6d946876c17;p=francis%2Fstp.git

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 010b643..e9cffb6 100644
--- 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 d98b7c5..8371880 100644
--- 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