From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Wed, 23 Mar 2011 13:34:31 +0000 (+0000)
Subject: Speedup. Short cut before some copies were created.
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=c4a723d507538eccdae2dd1c7308e1bed81b977d;p=francis%2Fstp.git

Speedup. Short cut before some copies were created.

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

diff --git a/src/parser/ParserInterface.h b/src/parser/ParserInterface.h
index ac1c507..eaf4507 100644
--- a/src/parser/ParserInterface.h
+++ b/src/parser/ParserInterface.h
@@ -99,6 +99,12 @@ public:
     	return bm.LookupOrCreateSymbol(name.c_str());
     }
 
+    bool isSymbolAlreadyDeclared(char* name)
+    {
+           return bm.LookupSymbol(name);
+    }
+
+
     bool isSymbolAlreadyDeclared(string name)
 	{
 	   return bm.LookupSymbol(name.c_str());
diff --git a/src/parser/cvc.lex b/src/parser/cvc.lex
index 1f4521f..a7b93c4 100644
--- a/src/parser/cvc.lex
+++ b/src/parser/cvc.lex
@@ -122,29 +122,32 @@ ANYTHING ({LETTER}|{DIGIT}|{OPCHAR})
 "POP"            { return POP_TOK;}
 
 (({LETTER})|(_)({ANYTHING}))({ANYTHING})*	{
-  string str(yytext);
-   bool found = false;
+  
    ASTNode nptr;
    
-  if (BEEV::parserInterface->isSymbolAlreadyDeclared(str)) // it's a symbol.
+   if (BEEV::parserInterface->isSymbolAlreadyDeclared(yytext)) // it's a symbol.
     {
-    	nptr= BEEV::parserInterface->LookupOrCreateSymbol(str);
-    	found = true;
+    	nptr= BEEV::parserInterface->LookupOrCreateSymbol(yytext);
+	    cvclval.node = BEEV::parserInterface->newNode(nptr);
+		if ((cvclval.node)->GetType() == BEEV::BOOLEAN_TYPE)
+		  return FORMID_TOK;
+		else 
+		  return TERMID_TOK;
     }
-    else if (BEEV::parserInterface->letMgr.isLetDeclared(str)) // a let.
+
+    // Making 4.4M strings took 1B instructions. So I split out the above case 
+    // which occurs >90% of the time (so avoiding turning the char* into a string).
+    string str(yytext);
+    if (BEEV::parserInterface->letMgr.isLetDeclared(str)) // a let.
     {
     	nptr= BEEV::parserInterface->letMgr.resolveLet(str);
-    	found = true;
+    	cvclval.node = BEEV::parserInterface->newNode(nptr);
+	  
+	    if ((cvclval.node)->GetType() == BEEV::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.