Speedups.

* Cache the max, one and zero values inside the Create__Const() functions.
* Return a reference from the [] operator to reduce unncessary copies.

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

diff --git a/src/AST/ASTNode.h b/src/AST/ASTNode.h
index 013247dc95c38bfa743cc940ab7510b84f056adf..75d1b2270cb3c2adfff2df869642fd66e463522b 100644 (file)
--- a/src/AST/ASTNode.h
+++ b/src/AST/ASTNode.h
@@ -301,7 +301,7 @@ namespace BEEV
     ;
 
     // Get indexth childNode.
-    const ASTNode operator[](size_t index) const
+    const ASTNode& operator[](size_t index) const
     {
       return GetChildren()[index];
     }

diff --git a/src/STPManager/STPManager.cpp b/src/STPManager/STPManager.cpp
index 1947efbbadb76960a07bbcc5ece83de03dd22dfe..207e9e93c57765a12772d1b0a354bbc590a60f1c 100644 (file)
--- a/src/STPManager/STPManager.cpp
+++ b/src/STPManager/STPManager.cpp
@@ -285,16 +285,43 @@ namespace BEEV
 
   ASTNode STPMgr::CreateZeroConst(unsigned width)
   {
-    CBV z = CONSTANTBV::BitVector_Create(width, true);
-    return CreateBVConst(z, width);
+         assert(width > 0);
+         if (zeroes.size() == 0)
+         {
+                 zeroes.push_back(ASTNode()); // null
+                 for (int i =1; i < 65;i++)
+                         zeroes.push_back(CreateZeroConst(i));
+         }
+
+       if (width < zeroes.size())
+               return zeroes[width];
+       else
+       {
+               CBV z = CONSTANTBV::BitVector_Create(width, true);
+               return CreateBVConst(z, width);
+       }
   }
 
+
   ASTNode STPMgr::CreateOneConst(unsigned width)
   {
-    CBV o = CONSTANTBV::BitVector_Create(width, true);
-    CONSTANTBV::BitVector_increment(o);
+         assert(width > 0);
+         if (ones.size() == 0)
+         {
+                 ones.push_back(ASTNode()); // null
+                 for (int i =1; i < 65;i++)
+                         ones.push_back(CreateOneConst(i));
+         }
+
+       if (width < ones.size())
+               return ones[width];
+       else
+       {
+           CBV o = CONSTANTBV::BitVector_Create(width, true);
+           CONSTANTBV::BitVector_increment(o);
 
-    return CreateBVConst(o, width);
+           return CreateBVConst(o, width);
+       }
   }
 
   ASTNode STPMgr::CreateTwoConst(unsigned width)
@@ -308,10 +335,23 @@ namespace BEEV
 
   ASTNode STPMgr::CreateMaxConst(unsigned width)
   {
-    CBV max = CONSTANTBV::BitVector_Create(width, false);
-    CONSTANTBV::BitVector_Fill(max);
+         assert(width > 0);
+         if (max.size() == 0)
+         {
+                 max.push_back(ASTNode()); // null
+                 for (int i =1; i < 65;i++)
+                         max.push_back(CreateMaxConst(i));
+         }
+
+       if (width < max.size())
+               return max[width];
+       else
+       {
+                 CBV max = CONSTANTBV::BitVector_Create(width, false);
+           CONSTANTBV::BitVector_Fill(max);
 
-    return CreateBVConst(max, width);
+           return CreateBVConst(max, width);
+       }
   }
 
   //To ensure unique BVConst nodes, lookup the node in unique-table

diff --git a/src/STPManager/STPManager.h b/src/STPManager/STPManager.h
index 78b394b3bab467efc550fd85765afe016a8524c3..c7dc7ec83ebc0497ca949569acf16993c484d95e 100644 (file)
--- a/src/STPManager/STPManager.h
+++ b/src/STPManager/STPManager.h
@@ -127,6 +127,11 @@ namespace BEEV
     // Called by ASTNode constructors to uniqueify ASTBVConst
     ASTBVConst *LookupOrCreateBVConst(ASTBVConst& s);
   
+    // Cache of zero/one/max BVConsts of different widths.
+    ASTVec zeroes;
+    ASTVec ones;
+    ASTVec max;
+
   public:
     
     /****************************************************************

diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp
index f406029f350fadc04bd8e64f233adac90c73e00e..ca235c3e6f5cb4517e8f357356ec6e90d96d2080 100644 (file)
--- a/src/simplifier/simplifier.cpp
+++ b/src/simplifier/simplifier.cpp
@@ -1640,9 +1640,11 @@ namespace BEEV
 
     if (simplify_upfront)
     {
-               if (k != BVCONST && k != SYMBOL) // const and symbols need to be created specially.
+       assert(k != BVCONST);
+               if (k != SYMBOL) // const and symbols need to be created specially.
                {
                        ASTVec v;
+                       v.reserve(actualInputterm.Degree());
                        for (unsigned i = 0; i < actualInputterm.Degree(); i++)
                                if (inputterm[i].GetType() == BITVECTOR_TYPE)
                                        v.push_back(SimplifyTerm(inputterm[i], VarConstMap));
@@ -1651,10 +1653,14 @@ namespace BEEV
                                else
                                        v.push_back(inputterm[i]);
 
-                       // TODO: Should check if the children arrays are different and only
-                       // create then.
-                       output = nf->CreateTerm(k, inputValueWidth, v);
-                       output.SetIndexWidth(actualInputterm.GetIndexWidth());
+                       assert(v.size() > 0);
+                       if (v != actualInputterm.GetChildren()) // short-cut.
+                       {
+                               output = nf->CreateTerm(k, inputValueWidth, v);
+                               output.SetIndexWidth(actualInputterm.GetIndexWidth());
+                       }
+                       else
+                               output = actualInputterm;
 
                        if (inputterm != output) {
                                UpdateSimplifyMap(inputterm, output, false, VarConstMap);
@@ -2011,7 +2017,8 @@ namespace BEEV
           //indices for BVEXTRACT
           ASTNode i = inputterm[1];
           ASTNode j = inputterm[2];
-          ASTNode zero = _bm->CreateBVConst(32, 0);
+          ASTNode zero = _bm->CreateZeroConst(32);
+
           //recall that the indices of BVEXTRACT are always 32 bits
           //long. therefore doing a GetBVUnsigned is ok.
           unsigned int i_val = i.GetUnsignedConst();
@@ -2160,7 +2167,7 @@ namespace BEEV
               //        } break; }
             case ITE:
               {
-                ASTNode t0 = a0[0];
+                const ASTNode& t0 = a0[0];
                 ASTNode t1 = 
                   SimplifyTerm(nf->CreateTerm(BVEXTRACT,
                                                a_len, a0[1], i, j), 
@@ -2526,7 +2533,7 @@ namespace BEEV
                         {
                           ASTNode zero = _bm->CreateZeroConst(shift);
                           ASTNode hi = _bm->CreateBVConst(32, width - shift -1);
-                          ASTNode low = _bm->CreateBVConst(32, 0);
+                          ASTNode low = _bm->CreateZeroConst(32);
                           ASTNode extract = 
                             nf->CreateTerm(BVEXTRACT, width - shift,
                                             a, hi, low);