From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Fri, 31 Dec 2010 02:35:05 +0000 (+0000)
Subject: Speedup. This makes it much faster to create some bvconsts.
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=b1bac1af52be23871dfc1711d7030614daa0adc4;p=francis%2Fstp.git

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 d20a787..734749f 100644
--- 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 6e63371..065c72e 100644
--- 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)