From e1cb3bddd186d8b4032cf55166fd1272a3352fe1 Mon Sep 17 00:00:00 2001
From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Tue, 24 Jan 2012 12:54:59 +0000
Subject: [PATCH] Improvement. Do better trailing zero propagation on
 multiplication.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1522 e59a4935-1847-0410-ae03-e826735625c1
---
 .../ConstantBitP_Multiplication.cpp           | 69 ++++++++++++++-----
 src/simplifier/constantBitP/FixedBits.h       | 26 ++++++-
 2 files changed, 75 insertions(+), 20 deletions(-)

diff --git a/src/simplifier/constantBitP/ConstantBitP_Multiplication.cpp b/src/simplifier/constantBitP/ConstantBitP_Multiplication.cpp
index f861135..ee55e01 100644
--- a/src/simplifier/constantBitP/ConstantBitP_Multiplication.cpp
+++ b/src/simplifier/constantBitP/ConstantBitP_Multiplication.cpp
@@ -162,6 +162,29 @@ Result adjustColumns(const FixedBits& x, const FixedBits& y, int* columnL,
 	return NO_CHANGE;
 }
 
+// returns true on conflict. A helper function.
+bool
+setToZero(FixedBits& y, int from, int to)
+{
+  assert(from<=to);
+  assert(from>= 0);
+  assert(to <= y.getWidth());
+
+  /***NB < to ***/
+  for (int i=from; i < to; i++)
+    {
+      if (y[i] == '*')
+        {
+          y.setFixed(i, true);
+          y.setValue(i, false);
+        }
+      else if (y[i] == '1')
+          return true;
+    }
+
+  return false;
+}
+
 // Finds the leading one in each of the two inputs.
 // If this position is i & j, then in the output
 // there can be no ones higher than i+j+1.
@@ -189,26 +212,34 @@ Result useLeadingZeroesToFix(FixedBits& x, FixedBits&y, FixedBits& output)
 	return NOT_IMPLEMENTED;
 }
 
-Result useTrailingZeroesToFix(FixedBits& x, FixedBits&y, FixedBits& output)
-{
-	int min = x.numberOfTrailingZeroes();
-	min += y.numberOfTrailingZeroes();
 
-	min = std::min(min, output.getWidth());
 
-	for (int i = 0; i < min; i++)
-		if (!output.isFixed(i))
-		{
-			output.setFixed(i, true);
-			output.setValue(i, false);
-		}
-		else if (output.getValue(i))
-		{
-			return CONFLICT;
-		}
+// if x has n trailing zeroes, and y has m trailing zeroes, then the output has n+m trailing zeroes.
+// if the output has n trailing zeroes and x has p trailing zeroes, then y has at least n-p trailing zeroes.
+  Result
+  useTrailingZeroesToFix(FixedBits& x, FixedBits&y, FixedBits& output)
+  {
+    int min = x.minimum_numberOfTrailingZeroes();
+    min += y.minimum_numberOfTrailingZeroes();
 
-	return NOT_IMPLEMENTED;
-}
+    min = std::min(min, output.getWidth());
+
+    if (setToZero(output,0,min))
+         return CONFLICT;
+
+    int output_zeroes = output.minimum_numberOfTrailingZeroes();
+    int x_zeroes = x.maximum_numberOfTrailingZeroes();
+    if (x_zeroes < output_zeroes)
+        if (setToZero(y,0,(output_zeroes - x_zeroes)))
+             return CONFLICT;
+
+    int y_zeroes = y.maximum_numberOfTrailingZeroes();
+    if (y_zeroes < output_zeroes)
+        if (setToZero(x,0,(output_zeroes - y_zeroes)))
+             return CONFLICT;
+
+   return NOT_IMPLEMENTED;
+  }
 
 // About 80% of multipliction runtime is in this function.
 // 48% is generating the multiplicative inverse.
@@ -386,8 +417,6 @@ Result bvMultiplyBothWays(vector<FixedBits*>& children, FixedBits& output,
 
 	const unsigned bitWidth = x.getWidth();
 
-	ImplicationGraph graph;
-
 	if (debug_multiply)
 		cerr << "======================" << endl;
 
@@ -432,6 +461,8 @@ Result bvMultiplyBothWays(vector<FixedBits*>& children, FixedBits& output,
 		return r;
 	}
 
+	ImplicationGraph graph;
+
 	bool changed = true;
 	while (changed)
 	{
diff --git a/src/simplifier/constantBitP/FixedBits.h b/src/simplifier/constantBitP/FixedBits.h
index 5b7c4bf..7ff9048 100644
--- a/src/simplifier/constantBitP/FixedBits.h
+++ b/src/simplifier/constantBitP/FixedBits.h
@@ -67,6 +67,18 @@ namespace simplifier
         return uniqueId <= copy.uniqueId;
       }
 
+      const char
+      operator[] (const int n) const
+      {
+        assert(n >=0 && n <width);
+        if (!isFixed(n))
+            return '*';
+        else if (getValue(n))
+            return '1';
+        else
+            return '0';
+      }
+
       bool
       operator==(const FixedBits& other) const
       {
@@ -132,7 +144,7 @@ namespace simplifier
       }
 
       int
-      numberOfTrailingZeroes()
+      minimum_numberOfTrailingZeroes()
       {
         int i = 0;
         for (; i < getWidth(); i++)
@@ -143,6 +155,18 @@ namespace simplifier
         return i;
       }
 
+      int
+      maximum_numberOfTrailingZeroes()
+      {
+        int i = 0;
+        for (; i < getWidth(); i++)
+          {
+            if (isFixed(i) && getValue(i))
+              break;
+          }
+        return i;
+      }
+
       //Returns the position of the first non-fixed value.
       int
       leastUnfixed() const
-- 
2.47.3