Refactor

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

diff --git a/src/to-sat/BitBlaster.cpp b/src/to-sat/BitBlaster.cpp
index 0932f19ef2b4514197e9915274b7ae7cdc162de9..76c334f63a673d0bd0d35400ad70b1b33f033356 100644 (file)
--- a/src/to-sat/BitBlaster.cpp
+++ b/src/to-sat/BitBlaster.cpp
@@ -1150,7 +1150,9 @@ BBNodeVec BitBlaster<BBNode,BBNodeManagerT>::buildAdditionNetworkResult(stack<BB
   BBNodeVec results;
   for (int i = 0; i < bitWidth; i++)
     {
-      buildAdditionNetworkResult(products, support, bitWidth, i);
+              buildAdditionNetworkResult(&(products[i]), &(products[i+1]), support, bitWidth, i);
+          else
+              buildAdditionNetworkResult(&(products[i]), NULL, support, bitWidth, i);
       assert(products[i].size() == 1);
       results.push_back(products[i].top());
     }
@@ -1163,23 +1165,26 @@ BBNodeVec BitBlaster<BBNode,BBNodeManagerT>::buildAdditionNetworkResult(stack<BB
 // Use full adders to create an addition network that adds together each of the
 // partial products.
 template <class BBNode, class BBNodeManagerT>
-void BitBlaster<BBNode,BBNodeManagerT>::buildAdditionNetworkResult(stack<BBNode>* products, set<BBNode>& support,
+void BitBlaster<BBNode,BBNodeManagerT>::buildAdditionNetworkResult(stack<BBNode>* from_, stack<BBNode>* to_, set<BBNode>& support,
                const int bitWidth, const int i, const int minTrue, const int maxTrue )
 {
-      while (products[i].size() >= 2) {
+    stack<BBNode> from = *from_;
+    stack<BBNode> to = *to_;
+
+    while (from.size() >= 2) {
               BBNode c;
 
-              if (products[i].size() == 2)
+              if (from.size() == 2)
                       c = nf->getFalse();
               else {
-                      c = products[i].top();
-                      products[i].pop();
+                      c = from.top();
+                      from.pop();
               }
 
-              const BBNode a = products[i].top();
-              products[i].pop();
-              const BBNode b = products[i].top();
-              products[i].pop();
+              const BBNode a = from.top();
+              from.pop();
+              const BBNode b = from.top();
+              from.pop();
 
               BBNode carry, sum;
 
@@ -1216,7 +1221,7 @@ void BitBlaster<BBNode,BBNodeManagerT>::buildAdditionNetworkResult(stack<BBNode>
                {
                // I experimented with making products[] a deque and accessing the front and back of the queue.
                // As a stack is works considerably better.
-               products[i].push(sum);
+               from.push(sum);
                }
              if (conjoin_to_top && maxTrue ==1)
              {
@@ -1224,13 +1229,14 @@ void BitBlaster<BBNode,BBNodeManagerT>::buildAdditionNetworkResult(stack<BBNode>
              }
              else if (i + 1 != bitWidth && carry != BBFalse)
              {
-                     products[i + 1].push(carry);
+                     assert(to != NULL);
+                     to.push(carry);
              }
       }
-      if (0==products[i].size())
-        products[i].push(BBFalse);
+      if (0==from.size())
+        from.push(BBFalse);
 
-      assert(1==products[i].size());
+      assert(1==from.size());
 }
 
 
@@ -1328,7 +1334,7 @@ BBNodeVec BitBlaster<BBNode,BBNodeManagerT>::multWithBounds(const ASTNode&n, sta
                         if (debug_bounds)
                                 cerr << "A";
 
-                        buildAdditionNetworkResult(products,toConjoinToTop,bitWidth,i, ms.sumL[i], ms.sumH[i]);
+                        buildAdditionNetworkResult(&(products[i]), ((i+1==bitWidth)?NULL: &(products[i+1])), toConjoinToTop,bitWidth,i, ms.sumL[i], ms.sumH[i]);
                 }
 
                 assert(products[i].size() == 1);

diff --git a/src/to-sat/BitBlaster.h b/src/to-sat/BitBlaster.h
index 587c8108c2c35c4a70bf767798150d9cb078ee8f..aab61c0f912e31f044e1041f632cc899f1977b6c 100644 (file)
--- a/src/to-sat/BitBlaster.h
+++ b/src/to-sat/BitBlaster.h
@@ -85,7 +85,7 @@ class BitBlaster {
             set<BBNode>& support, stack<BBNode>& currentColumn, vector<BBNode>& currentSorted, vector<BBNode>& priorSorted,
                 const int minTrue = 0, const int maxTrue = ((unsigned)~0) >> 1 );
 
-       void buildAdditionNetworkResult(stack<BBNode>* products, set<BBNode>& support, const int bitWidth, const int index, const int minTrue = 0, const int maxTrue = ((unsigned)~0) >> 1 );
+       void buildAdditionNetworkResult(stack<BBNode>* from, stack<BBNode>* to,  set<BBNode>& support, const int bitWidth, const int index, const int minTrue = 0, const int maxTrue = ((unsigned)~0) >> 1 );
        vector<BBNode> buildAdditionNetworkResult(stack<BBNode>* products, set<BBNode>& support, int bitWidth);
 
        vector<BBNode> BBAndBit(const vector<BBNode>& y, BBNode b);