From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Sun, 4 Jul 2010 08:25:47 +0000 (+0000)
Subject: Tiny speedup. Generate the encoding of multiplication slightly more efficiently.
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=15c47f9e575968f9c85730bd467b9fccc9e2082c;p=francis%2Fstp.git

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 f43c207..a1729bb 100644
--- 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;