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 ac1c507cf5beb213ce41561647fbc644d2f7156d..eaf45072dec143103eddd981b70152a0ce418b27 100644 (file)
--- 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 1f4521ffc86014c9843b4c68d52ae0277a84ac4b..a7b93c4ca07d02394ac0d575556f4f4df8796bc1 100644 (file)
--- 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.