From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Wed, 28 Jul 2010 03:09:57 +0000 (+0000)
Subject: Speed up of the unsigned division encoding. Update the runtimes for the different... 
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=f3287a50775c3420fe6b9a10fbc36486d0e490ba;p=francis%2Fstp.git

Speed up of the unsigned division encoding. Update the runtimes for the different variants of unsigned division.





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

diff --git a/src/to-sat/BitBlaster.cpp b/src/to-sat/BitBlaster.cpp
index 7f0fc2a..73a5028 100644
--- a/src/to-sat/BitBlaster.cpp
+++ b/src/to-sat/BitBlaster.cpp
@@ -1080,15 +1080,35 @@ BBNodeVec BitBlaster<BBNode,BBNodeManagerT>::BBMult(const BBNodeVec& x, const BB
 	FatalError("sda44f");
 }
 
-// on factoring12bitsx12.cvc
-// variant1 = t, variant2 = t: 66 seconds
-// variant1 = t, variant2 = f: 37 seconds
-// variant1 = f, variant2 = f: 46 seconds
-// variant1 = f, variant2 = t: 65 seconds
+//======
+// on factoring12bitsx12.cvc with CMS2.
+// variant1 = t, variant2 = t, variant3 = f:  7.3 seconds
+// variant1 = t, variant2 = f, variant3 = f:  3.7 seconds <---
+// variant1 = f, variant2 = f, variant3 = f:  6.1 seconds
+// variant1 = f, variant2 = t, variant3 = f:  9.2 seconds
+
+// variant1 = t, variant2 = t, variant3 = t:  7.0 seconds
+// variant1 = t, variant2 = f, variant3 = t:  6.9 seconds
+// variant1 = f, variant2 = f, variant3 = t:  9.9 seconds
+// variant1 = f, variant2 = t, variant3 = t:  7.3 seconds
+//======
+// on factoring12bitsx12.cvc with MINISAT2.
+// variant1 = t, variant2 = t, variant3 = f: 10.6 seconds
+// variant1 = t, variant2 = f, variant3 = f: 7.8 seconds
+// variant1 = f, variant2 = f, variant3 = f: 10.1 seconds
+// variant1 = f, variant2 = t, variant3 = f: 11.6 seconds
+
+// variant1 = t, variant2 = t, variant3 = t: 10.6 seconds
+// variant1 = t, variant2 = f, variant3 = t: 10.7 seconds
+// variant1 = f, variant2 = f, variant3 = t: 11.8 seconds
+// variant1 = f, variant2 = t, variant3 = t: 11.2 seconds
+//======
+
 
 // You can select these with any combination you want of true & false.
 const bool division_variant_1 = true;
 const bool division_variant_2 = false;
+const bool division_variant_3 = false;
 
 // This implements a variant of binary long division.
 // q and r are "out" parameters.  rwidth puts a bound on the
@@ -1144,7 +1164,9 @@ void BitBlaster<BBNode,BBNodeManagerT>::BBDivMod(const BBNodeVec &y, const BBNod
                 rminusx.pop_back();
 
                 // Adjusted q, r values when when r is too large.
-                BBNodeVec ygtrxqval = BBITE(sign, q1lshift1, BBInc(q1lshift1));
+                //q1lshift1 has zero in the least significant digit.
+                //BBNodeVec ygtrxqval = BBITE(sign, q1lshift1, BBInc(q1lshift1));
+                q1lshift1[0] = nf->CreateNode(NOT,sign);
                 BBNodeVec ygtrxrval = BBITE(sign, r1lshift1plusyodd, rminusx );
 
 		BBNodeVec notylessxqval;
@@ -1170,7 +1192,7 @@ void BitBlaster<BBNode,BBNodeManagerT>::BBDivMod(const BBNodeVec &y, const BBNod
 
 		if (division_variant_1)
 		{
-			notylessxqval = ygtrxqval;
+			notylessxqval = q1lshift1;
 			notylessxrval = ygtrxrval;
 		}
 		else
@@ -1178,7 +1200,7 @@ void BitBlaster<BBNode,BBNodeManagerT>::BBDivMod(const BBNodeVec &y, const BBNod
 			// q & r values when y >= x
 			BBNode yeqx = BBEQ(y, x);
 			// *** Problem: the bbfill for qval is wrong.  Should be 1, not -1.
-			notylessxqval = BBITE(yeqx, one, ygtrxqval);
+			notylessxqval = BBITE(yeqx, one, q1lshift1);
 			notylessxrval = BBITE(yeqx, zero,ygtrxrval);
 		}
 
@@ -1194,20 +1216,18 @@ void BitBlaster<BBNode,BBNodeManagerT>::BBDivMod(const BBNodeVec &y, const BBNod
 			ylessx = nf->CreateNode(NOT, BBBVLE(x, y, false));
 		}
 
-		// 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.
-
-
-		/****************/
+		if (division_variant_3)
+		  {
+                     q = notylessxqval;
+                     r = notylessxrval;
+		  }
+		else
+		  {
+                      // This variant often helps somehow. I don't know why.
+                      // Even though it uses more memory..
+                      q = BBITE(ylessx, zero, notylessxqval);
+                      r = BBITE(ylessx, y, notylessxrval);
+            }
 	}
 }