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

diff --git a/src/simplifier/constantBitP/ConstantBitP_Multiplication.cpp b/src/simplifier/constantBitP/ConstantBitP_Multiplication.cpp
index 84e1a3b9a0798ab7e62fd1e9abefdb5f807cf721..81fd383f9046f20f061f0e3c2aa2ce2413777b8b 100644 (file)
--- 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 39e9da055981ef2d530859d4271fef633d242f14..d4b85212699cc5879e0bb3ee3e31f57dbc602fb3 100644 (file)
--- 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 ca0bbe9953d7995644b4073e70f9ab97548fdb3e..2ebb3eb6d462e24df4423ea8cf17fabb705ff76f 100644 (file)
--- 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_ */