Improvement. Create fewer objects.

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

diff --git a/src/STPManager/STPManager.cpp b/src/STPManager/STPManager.cpp
index dd8c134c3ab747e96deecbcf2ced2ac25c04c643..3aef19efe245f532bf6010b45db22eb4e50a878a 100644 (file)
--- a/src/STPManager/STPManager.cpp
+++ b/src/STPManager/STPManager.cpp
@@ -164,6 +164,20 @@ namespace BEEV
       return true;
   }
 
+  bool STPMgr::LookupSymbol(const char * const name, ASTNode& output)
+  {
+    ASTSymbol temp_sym(name);
+    ASTSymbolSet::const_iterator it = _symbol_unique_table.find(&temp_sym);
+    if (it != _symbol_unique_table.end())
+      {
+        output = ASTNode(*it);
+        return true;
+      }
+  return false;
+  }
+
+
+
 
   //Create a ASTBVConst node
   ASTNode STPMgr::CreateBVConst(unsigned int width, 
@@ -209,36 +223,32 @@ namespace BEEV
 
   }
 
-  ASTNode STPMgr::CreateBVConst(string& strval, int base, int bit_width)
+  ASTNode STPMgr::charToASTNode(unsigned char* strval, int base , int bit_width)
   {
+    assert ((2 == base || 10 == base || 16 == base));
+    assert (bit_width > 0);
 
-    if (bit_width <= 0)
-      FatalError("CreateBVConst: trying to create a bvconst of width: ", 
-                ASTUndefined, bit_width);
-
-
-    if (!(2 == base || 10 == base || 16 == base))
-      {
-        FatalError("CreateBVConst: unsupported base: ", ASTUndefined, base);
-      }
+    // We create a single bvconst that gets reused.
+    if (NULL == CreateBVConstVal)
+      CreateBVConstVal = CONSTANTBV::BitVector_Create(65, true);
+    CreateBVConstVal  = CONSTANTBV::BitVector_Resize(CreateBVConstVal,bit_width);
+    CONSTANTBV::BitVector_Empty(CreateBVConstVal);
 
-    //checking if the input is in the correct format
-    CBV bv = CONSTANTBV::BitVector_Create(bit_width, true);
     CONSTANTBV::ErrCode e;
     if (2 == base)
       {
-        e = CONSTANTBV::BitVector_from_Bin(bv,
-                                          (unsigned char*) strval.c_str());
+        e = CONSTANTBV::BitVector_from_Bin(CreateBVConstVal,
+                                           strval);
       }
     else if (10 == base)
       {
-        e = CONSTANTBV::BitVector_from_Dec(bv,
-                                          (unsigned char*) strval.c_str());
+        e = CONSTANTBV::BitVector_from_Dec(CreateBVConstVal,
+                                           strval);
       }
     else if (16 == base)
       {
-        e = CONSTANTBV::BitVector_from_Hex(bv, 
-                                          (unsigned char*) strval.c_str());
+        e = CONSTANTBV::BitVector_from_Hex(CreateBVConstVal,
+                                           strval);
       }
     else
       {
@@ -251,17 +261,25 @@ namespace BEEV
         FatalError("", ASTUndefined);
       }
 
-    return CreateBVConst(bv, bit_width);
+    ASTBVConst temp_bvconst(CreateBVConstVal, bit_width,ASTBVConst::CBV_MANAGED_OUTSIDE);
+    ASTNode n(LookupOrCreateBVConst(temp_bvconst));
+    return n;
+  }
+
+  ASTNode STPMgr::CreateBVConst(string& strval, int base, int bit_width)
+  {
+    assert (bit_width > 0);
+
+    return charToASTNode((unsigned char*)strval.c_str(), base , bit_width);
   }
 
-  //Create a ASTBVConst node from std::string
+  //Create a ASTBVConst node from a char*
   ASTNode STPMgr::CreateBVConst(const char* const strval, int base)
   {
+    assert ((2 == base || 10 == base || 16 == base));
+
     size_t width = strlen((const char *) strval);
-    if (!(2 == base || 10 == base || 16 == base))
-      {
-        FatalError("CreateBVConst: unsupported base: ", ASTUndefined, base);
-      }
+
     //FIXME Tim: Earlier versions of the code assume that the length of
     //binary strings is 32 bits.
     if (10 == base)
@@ -269,45 +287,15 @@ namespace BEEV
     if (16 == base)
       width = width * 4;
 
-    //checking if the input is in the correct format
-    CBV bv = CONSTANTBV::BitVector_Create(width, true);
-    CONSTANTBV::ErrCode e;
-    if (2 == base)
-      {
-        e = CONSTANTBV::BitVector_from_Bin(bv, (unsigned char*) strval);
-      }
-    else if (10 == base)
-      {
-        e = CONSTANTBV::BitVector_from_Dec(bv, (unsigned char*) strval);
-      }
-    else if (16 == base)
-      {
-        e = CONSTANTBV::BitVector_from_Hex(bv, (unsigned char*) strval);
-      }
-    else
-      {
-        e = CONSTANTBV::ErrCode_Pars;
-      }
-
-    if (0 != e)
-      {
-        cerr << "CreateBVConst: " << BitVector_Error(e);
-        FatalError("", ASTUndefined);
-      }
-
-    //FIXME
-    return CreateBVConst(bv, width);
+    return charToASTNode((unsigned char*)strval, base , width);
   }
 
-  //FIXME Code currently assumes that it will destroy the bitvector
-  //passed to it
+  //NB Assumes that it will destroy the bitvector passed to it
   ASTNode STPMgr::CreateBVConst(CBV bv, unsigned width)
   {
-    ASTBVConst temp_bvconst(bv, width);
+    ASTBVConst temp_bvconst(bv, width,ASTBVConst::CBV_MANAGED_OUTSIDE);
     ASTNode n(LookupOrCreateBVConst(temp_bvconst));
-
     CONSTANTBV::BitVector_Destroy(bv);
-
     return n;
   }
 
@@ -392,9 +380,7 @@ namespace BEEV
     ASTBVConstSet::const_iterator it;
     if ((it = _bvconst_unique_table.find(s_ptr)) == _bvconst_unique_table.end())
       {
-        // Make a new ASTBVConst with duplicated string (can't assign
-        // _name because it's const).  Can cast the iterator to
-        // non-const -- carefully.
+        // Make a new ASTBVConst with duplicated constant.
 
         ASTBVConst * s_copy = new ASTBVConst(s);
         s_copy->SetNodeNum(NewNodeNum());
@@ -405,7 +391,7 @@ namespace BEEV
       }
     else
       {
-        // return symbol found in table.
+        // return constant found in table.
         return *it;
       }
   }

diff --git a/src/STPManager/STPManager.h b/src/STPManager/STPManager.h
index ac9242698e4dba1ba578a7445fa4fd83ed801d5d..24aefb8bcf4a9a726774f92bade21e46adcec07a 100644 (file)
--- a/src/STPManager/STPManager.h
+++ b/src/STPManager/STPManager.h
@@ -141,6 +141,7 @@ namespace BEEV
   public:
 
     bool LookupSymbol(const char * const name);
+    bool LookupSymbol(const char * const name, ASTNode& output);
     
     /****************************************************************
      * Public Flags                                                 *
@@ -277,6 +278,7 @@ namespace BEEV
     ASTNode CreateBVConst(const char *strval, int base);
     ASTNode CreateBVConst(string& strval, int base, int bit_width);    
     ASTNode CreateBVConst(unsigned int width, unsigned long long int bvconst);
+    ASTNode charToASTNode(unsigned char* strval, int base , int bit_width);
     
     /****************************************************************
      * Create Node functions                                        *

diff --git a/src/parser/ParserInterface.h b/src/parser/ParserInterface.h
index eaf45072dec143103eddd981b70152a0ce418b27..83e7f91cd0f80f08a9fb18800e3fbe10f449b2b4 100644 (file)
--- a/src/parser/ParserInterface.h
+++ b/src/parser/ParserInterface.h
@@ -99,6 +99,11 @@ public:
        return bm.LookupOrCreateSymbol(name.c_str());
     }
 
+    bool LookupSymbol(const char * const name, ASTNode& output)
+    {
+      return bm.LookupSymbol(name,output);
+    }
+
     bool isSymbolAlreadyDeclared(char* name)
     {
            return bm.LookupSymbol(name);

diff --git a/src/parser/cvc.lex b/src/parser/cvc.lex
index a7b93c4ca07d02394ac0d575556f4f4df8796bc1..bfdbbcdcf9d31fc404b27c6c636ecb16993db102 100644 (file)
--- a/src/parser/cvc.lex
+++ b/src/parser/cvc.lex
@@ -125,9 +125,8 @@ ANYTHING ({LETTER}|{DIGIT}|{OPCHAR})
   
    ASTNode nptr;
    
-   if (BEEV::parserInterface->isSymbolAlreadyDeclared(yytext)) // it's a symbol.
+   if (BEEV::parserInterface->LookupSymbol(yytext,nptr)) // it's a symbol.
     {
-       nptr= BEEV::parserInterface->LookupOrCreateSymbol(yytext);
            cvclval.node = BEEV::parserInterface->newNode(nptr);
                if ((cvclval.node)->GetType() == BEEV::BOOLEAN_TYPE)
                  return FORMID_TOK;