From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Tue, 29 Jun 2010 15:14:23 +0000 (+0000)
Subject: Speedup. Generate nicer circuits for unsigned division.
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=ce9c23ae8eecdcd2db932ee2eb28733e51a0e01e;p=francis%2Fstp.git

Speedup. Generate nicer circuits for unsigned division.



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

diff --git a/src/to-sat/BitBlastNew.cpp b/src/to-sat/BitBlastNew.cpp
index c5b3650..00d944c 100644
--- a/src/to-sat/BitBlastNew.cpp
+++ b/src/to-sat/BitBlastNew.cpp
@@ -937,14 +937,23 @@ void BitBlasterNew::BBDivMod(const BBNodeVec &y, const BBNodeVec &x,
 		BBNodeVec r1lshift1(r1);
 		BBLShift(r1lshift1, 1);
 
-		BBNodeVec r1lshift1plusyodd = BBAddOneBit(r1lshift1, y[0]);
-		BBNodeVec rminusx(r1lshift1plusyodd);
-		BBSub(rminusx, x, support);
-
-		// Adjusted q, r values when when r is too large.
-		BBNode rtoolarge = BBBVLE(x, r1lshift1plusyodd, false);
-		BBNodeVec ygtrxqval = BBITE(rtoolarge, BBInc(q1lshift1), q1lshift1);
-		BBNodeVec ygtrxrval = BBITE(rtoolarge, rminusx, r1lshift1plusyodd);
+		BBNodeVec r1lshift1plusyodd(r1lshift1);
+		r1lshift1plusyodd[0] = y[0];
+
+                // By extending rminusx by one bit, we can use that top-bit
+                // to check whether r>=x. We need to compute rminusx anyway,
+                // so this saves having a separate compare circut.
+                BBNodeVec rminusx(r1lshift1plusyodd);
+                rminusx.push_back(nf->getFalse());
+                BBNodeVec xCopy(x);
+                xCopy.push_back(nf->getFalse());
+                BBSub(rminusx, xCopy, support);
+                BBNode sign = rminusx[width];
+                rminusx.pop_back();
+
+                // Adjusted q, r values when when r is too large.
+                BBNodeVec ygtrxqval = BBITE(sign, q1lshift1, BBInc(q1lshift1));
+                BBNodeVec ygtrxrval = BBITE(sign, r1lshift1plusyodd, rminusx );
 
 		BBNodeVec notylessxqval;
 		BBNodeVec notylessxrval;
@@ -981,6 +990,7 @@ void BitBlasterNew::BBDivMod(const BBNodeVec &y, const BBNodeVec &x,
 			notylessxrval = BBITE(yeqx, zero,ygtrxrval);
 		}
 
+		/****************/
 		BBNode ylessx;
 		if (division_variant_2)
 		{
@@ -995,6 +1005,17 @@ void BitBlasterNew::BBDivMod(const BBNodeVec &y, const BBNodeVec &x,
 		// final values of q and r
 		q = BBITE(ylessx, zero, notylessxqval);
 		r = BBITE(ylessx, y, notylessxrval);
+
+                // The above does nothing. This gives the correct answer too:
+                //q = notylessxqval;
+                //r = notylessxrval;
+
+                // But, it's about 30% slower on factoring12x12.
+                // Either these help during solving, or, the CNF generation
+                // generates nicer code with them present.
+
+
+		/****************/
 	}
 }