Speedup. This makes it much faster to create some bvconsts.

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

diff --git a/src/STPManager/STPManager.cpp b/src/STPManager/STPManager.cpp
index d20a787d510fb8add128f743472816a3586599bd..734749f554c1623d100558c1a7560132c2d5cec0 100644 (file)
--- a/src/STPManager/STPManager.cpp
+++ b/src/STPManager/STPManager.cpp
@@ -157,7 +157,13 @@ namespace BEEV
                 "unsigned long long of width: ", 
                  ASTUndefined, width);
 
-    CBV bv = CONSTANTBV::BitVector_Create(width, true);
+
+    // We create a single bvconst that gets reused.
+    if (NULL == CreateBVConstVal)
+      CreateBVConstVal = CONSTANTBV::BitVector_Create(65, true);
+    CreateBVConstVal  = CONSTANTBV::BitVector_Resize(CreateBVConstVal,width);
+    CONSTANTBV::BitVector_Empty(CreateBVConstVal);
+
     unsigned long c_val = (~((unsigned long) 0)) & bvconst;
     unsigned int copied = 0;
 
@@ -170,16 +176,19 @@ namespace BEEV
     //number of bits in unsigned long. The variable "copied" keeps
     //track of the number of chunks copied so far
 
-    int shift_amount = (sizeof(unsigned long) << 3);
-    while (copied + (sizeof(unsigned long) << 3) < width)
+    const int shift_amount = (sizeof(unsigned long) << 3);
+    while (copied + shift_amount < width)
       {
-        CONSTANTBV::BitVector_Chunk_Store(bv, shift_amount, copied, c_val);
+        CONSTANTBV::BitVector_Chunk_Store(CreateBVConstVal, shift_amount, copied, c_val);
         bvconst = bvconst >> shift_amount;
         c_val = (~((unsigned long) 0)) & bvconst;
         copied += shift_amount;
       }
-    CONSTANTBV::BitVector_Chunk_Store(bv, width - copied, copied, c_val);
-    return CreateBVConst(bv, width);
+    CONSTANTBV::BitVector_Chunk_Store(CreateBVConstVal, width - copied, copied, c_val);
+
+    ASTBVConst temp_bvconst(CreateBVConstVal, width,ASTBVConst::CBV_MANAGED_OUTSIDE);
+    return  ASTNode(LookupOrCreateBVConst(temp_bvconst));
+
   }
 
   ASTNode STPMgr::CreateBVConst(string*& strval, int base, int bit_width)

diff --git a/src/STPManager/STPManager.h b/src/STPManager/STPManager.h
index 6e63371048f5e66e5b1f563c88069579157579ef..065c72e558aa45570ab8338a1806e769e13dfa87 100644 (file)
--- a/src/STPManager/STPManager.h
+++ b/src/STPManager/STPManager.h
@@ -136,6 +136,8 @@ namespace BEEV
     // Set of new symbols introduced that replace the array read terms
     ASTNodeSet Introduced_SymbolsSet;
 
+    CBV CreateBVConstVal;
+
   public:
     
     /****************************************************************
@@ -198,6 +200,7 @@ namespace BEEV
       runTimes     = new RunTimes();
       _current_query = ASTUndefined;
       UserFlags.num_absrefine = 2;
+      CreateBVConstVal = NULL;
     }    
     
     RunTimes * GetRunTimes(void)