Tiny speedup. Generate the encoding of multiplication slightly more efficiently.

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

diff --git a/src/to-sat/BitBlaster.cpp b/src/to-sat/BitBlaster.cpp
index f43c2077d61645190e546ba873c694b35a67a010..a1729bb2000e397fe99cb5a07fec581fd28f57dd 100644 (file)
--- a/src/to-sat/BitBlaster.cpp
+++ b/src/to-sat/BitBlaster.cpp
@@ -944,9 +944,20 @@ void BitBlaster<BBNode,BBNodeManagerT>::BBDivMod(const BBNodeVec &y, const BBNod
                BBNodeVec &q, BBNodeVec &r, unsigned int rwidth, BBNodeSet& support) {
        const unsigned int width = y.size();
        const BBNodeVec zero = BBfill(width, nf->getFalse());
-       const BBNodeVec one = BBInc(zero);
+       BBNodeVec one = zero;
+       one[0] = nf->getTrue();
 
-       if (rwidth == 0) {
+       // check if y is already zero.
+       bool isZero=true;
+       for (int i =0; i < rwidth;i++)
+          if (y[i] != nf->getFalse())
+          {
+            isZero = false;
+            break;
+            }
+
+
+       if (isZero || rwidth == 0) {
                // When we have shifted the entire width, y is guaranteed to be 0.
                q = zero;
                r = zero;