From a3ba0293d1163391fbb48430b33f6aa5a64b5963 Mon Sep 17 00:00:00 2001
From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Sat, 7 Apr 2012 12:43:20 +0000
Subject: [PATCH] Refactor. Automatically format the code, no other change.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1631 e59a4935-1847-0410-ae03-e826735625c1
---
 .../ConstantBitP_Multiplication.cpp           |   1 -
 .../multiplication/ColumnCounts.h             |   3 -
 .../constantBitP/multiplication/ColumnStats.h | 124 +++++++++---------
 3 files changed, 60 insertions(+), 68 deletions(-)

diff --git a/src/simplifier/constantBitP/ConstantBitP_Multiplication.cpp b/src/simplifier/constantBitP/ConstantBitP_Multiplication.cpp
index 84e1a3b..81fd383 100644
--- a/src/simplifier/constantBitP/ConstantBitP_Multiplication.cpp
+++ b/src/simplifier/constantBitP/ConstantBitP_Multiplication.cpp
@@ -645,6 +645,5 @@ namespace simplifier
 
       return NOT_IMPLEMENTED;
     }
-
   }
 }
diff --git a/src/simplifier/constantBitP/multiplication/ColumnCounts.h b/src/simplifier/constantBitP/multiplication/ColumnCounts.h
index 39e9da0..d4b8521 100644
--- a/src/simplifier/constantBitP/multiplication/ColumnCounts.h
+++ b/src/simplifier/constantBitP/multiplication/ColumnCounts.h
@@ -274,11 +274,8 @@ namespace simplifier
         else
           return NO_CHANGE;
       }
-
     };
-
   }
-
 }
 
 #endif /* COLUMNCOUNTS_H_ */
diff --git a/src/simplifier/constantBitP/multiplication/ColumnStats.h b/src/simplifier/constantBitP/multiplication/ColumnStats.h
index ca0bbe9..2ebb3eb 100644
--- a/src/simplifier/constantBitP/multiplication/ColumnStats.h
+++ b/src/simplifier/constantBitP/multiplication/ColumnStats.h
@@ -10,70 +10,66 @@
 
 namespace simplifier
 {
-namespace constantBitP
-{
-
-extern const bool debug_multiply;
-
-
-
-struct ColumnStats
-{
-	int columnUnfixed; // both unfixed.
-	int columnOneFixed; // one of the values is fixed to one, the other is unfixed.
-	int columnOnes; // both are fixed to one.
-	int columnZeroes; // one is fixed to zero.
-
-	ColumnStats(const FixedBits & x, const FixedBits & y, int index)
-	{
-		columnUnfixed = 0;
-		columnOneFixed = 0;
-		columnOnes = 0;
-		columnZeroes = 0;
-
-		assert(index < x.getWidth());
-		assert(y.getWidth() == x.getWidth());
-
-		if (debug_multiply)
-			log << "ColumnStats" << index << " " << x << " " << y << endl;
-
-		for (unsigned i = 0; i <= (unsigned) index; i++)
-		{
-			bool xIsFixed = x.isFixed(index - i);
-			bool yIsFixed;
-
-			if (xIsFixed && !x.getValue(index - i))
-				columnZeroes++;
-			else if ((yIsFixed = y.isFixed(i)) && !y.getValue(i))
-				columnZeroes++;
-			else if (xIsFixed && x.getValue(index - i) && yIsFixed
-					&& y.getValue(i))
-				columnOnes++;
-			else if (yIsFixed && y.getValue(i))
-				columnOneFixed++;
-			else if (xIsFixed && x.getValue(index - i))
-				columnOneFixed++;
-			else
-				columnUnfixed++;
-		}
-
-		assert(columnOnes >=0 && columnUnfixed >=0 && columnZeroes >=0 && columnOneFixed >=0);
-		assert(columnOnes + columnUnfixed + columnOneFixed + columnZeroes == (index+1));
-	}
-
-};
-
-std::ostream& operator<<(std::ostream& o, const ColumnStats& cs)
-{
-	o << "cUnfixed:" << cs.columnUnfixed << endl; // both unfixed.
-	o << "cOneFixed:" << cs.columnOneFixed << endl; // one of the values is fixed to one.
-	o << "cOnes:" << cs.columnOnes << endl;
-	o << "cZero:" << cs.columnZeroes << endl;
-	return o;
+  namespace constantBitP
+  {
+
+    extern const bool debug_multiply;
+
+    struct ColumnStats
+    {
+      int columnUnfixed; // both unfixed.
+      int columnOneFixed; // one of the values is fixed to one, the other is unfixed.
+      int columnOnes; // both are fixed to one.
+      int columnZeroes; // one is fixed to zero.
+
+      ColumnStats(const FixedBits & x, const FixedBits & y, int index)
+      {
+        columnUnfixed = 0;
+        columnOneFixed = 0;
+        columnOnes = 0;
+        columnZeroes = 0;
+
+        assert(index < x.getWidth());
+        assert(y.getWidth() == x.getWidth());
+
+        if (debug_multiply)
+          log << "ColumnStats" << index << " " << x << " " << y << endl;
+
+        for (unsigned i = 0; i <= (unsigned) index; i++)
+          {
+          bool xIsFixed = x.isFixed(index - i);
+          bool yIsFixed;
+
+          if (xIsFixed && !x.getValue(index - i))
+            columnZeroes++;
+          else if ((yIsFixed = y.isFixed(i)) && !y.getValue(i))
+            columnZeroes++;
+          else if (xIsFixed && x.getValue(index - i) && yIsFixed && y.getValue(i))
+            columnOnes++;
+          else if (yIsFixed && y.getValue(i))
+            columnOneFixed++;
+          else if (xIsFixed && x.getValue(index - i))
+            columnOneFixed++;
+          else
+            columnUnfixed++;
+          }
+
+        assert(columnOnes >= 0 && columnUnfixed >= 0 && columnZeroes >= 0 && columnOneFixed >= 0);
+        assert(columnOnes + columnUnfixed + columnOneFixed + columnZeroes == (index + 1));
+      }
+
+    };
+
+    std::ostream&
+    operator<<(std::ostream& o, const ColumnStats& cs)
+    {
+      o << "cUnfixed:" << cs.columnUnfixed << endl; // both unfixed.
+      o << "cOneFixed:" << cs.columnOneFixed << endl; // one of the values is fixed to one.
+      o << "cOnes:" << cs.columnOnes << endl;
+      o << "cZero:" << cs.columnZeroes << endl;
+      return o;
+    }
+  }
 }
 
-}
-}
-
-
 #endif /* COLUMNSTATS_H_ */
-- 
2.47.3