Improvements speedups for better test code.

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

diff --git a/src/simplifier/constantBitP/FixedBits.cpp b/src/simplifier/constantBitP/FixedBits.cpp
index 55a08a2b2694b0e606e387723e9ebc37a172c7fe..273175a7dbcf7db20b6979c24eb597cd30b526f8 100644 (file)
--- a/src/simplifier/constantBitP/FixedBits.cpp
+++ b/src/simplifier/constantBitP/FixedBits.cpp
@@ -192,43 +192,65 @@ namespace simplifier
         }
     }
 
-    // Whether the set of values contains this one.
     bool
     FixedBits::unsignedHolds(unsigned val)
     {
-      for (unsigned i = 0; i < width; i++)
-        {
-          if (i < (unsigned) width && i < sizeof(unsigned) * 8)
-            {
-              if (isFixed(i) && (getValue(i) != (((val & (1 << i))) != 0)))
-                return false;
-            }
-          else if (i < (unsigned) width)
-            {
-              if (isFixed(i) && getValue(i))
-                return false;
-            }
-          else // The unsigned value is bigger than the bitwidth of this.
-            {
-              if (val & (1 << i))
-                return false;
-            }
-        }
-
-      // If the unsigned representation is bigger, we check (slowly) for leading ones.
-      for (unsigned i = width; i < (int) sizeof(unsigned) * 8; i++)
-        if (val & (1 << i))
-             return false;
-
-      return true;
+      bool r = unsignedHolds_new(val);
+      //assert (unsignedHolds_old(val) == r);
+      return r;
     }
 
+    // Whether the set of values contains this one. Much faster than the _old version.
+    bool
+    FixedBits::unsignedHolds_new(unsigned val)
+    {
+      const int initial_width = std::min((int)width, (int)sizeof(unsigned) * 8);
 
+      for (int i = 0; i < initial_width; i++)
+        {
+          char v = (*this)[i];
+          if ('*'== v)
+            {} // ok
+          else if ((v == '1') != ((val & 1) != 0))
+            return false;
+          val = val >> 1;
+        }
 
+      // If the unsigned representation is bigger, false if not zero.
+      if ((int) sizeof(unsigned) * 8 > width && (val !=0))
+         return false;
 
+      for (int i = (int) sizeof(unsigned) * 8; i < width; i++)
+        if (isFixed(i) && getValue(i))
+          return false;
 
+      return true;
+    }
 
-
+    bool
+    FixedBits::unsignedHolds_old(unsigned val)
+    {
+      const unsigned maxWidth = std::max((int) sizeof(unsigned) * 8, width);
+      for (unsigned i = 0; i < maxWidth; i++)
+        {
+        if (i < (unsigned) width && i < sizeof(unsigned) * 8)
+          {
+          if (isFixed(i) && (getValue(i) != (((val & (1 << i))) != 0)))
+            return false;
+          }
+        else if (i < (unsigned) width)
+          {
+          if (isFixed(i) && getValue(i))
+            return false;
+          }
+        else // The unsigned value is bigger than the bitwidth of this.
+          {
+          if (val & (1 << i))
+            return false;
+          }
+        }
+      return true;
+    }
 
     // Getting a new random number is expensive. Not sure why.
     FixedBits FixedBits::createRandom(const int length, const int probabilityOfSetting, MTRand& trand)
@@ -356,6 +378,32 @@ namespace simplifier
       return output;
     }
 
+
+    void
+    FixedBits::fromUnsigned(unsigned val)
+    {
+      for (unsigned i = 0; i < width; i++)
+        {
+          if (i < (unsigned) width && i < sizeof(unsigned) * 8)
+            {
+              setFixed(i, true);
+              setValue(i, (val & (1 << i)));
+            }
+          else if (i < (unsigned) width)
+            {
+              setFixed(i, true);
+              setValue(i, false);
+            }
+          else // The unsigned value is bigger than the bitwidth of this.
+            { // so it can't be represented.
+              if (val & (1 << i))
+                {
+                  BEEV::FatalError(LOCATION "Cant be represented.");
+                }
+            }
+        }
+    }
+
     int
     FixedBits::getUnsignedValue() const
     {

diff --git a/src/simplifier/constantBitP/FixedBits.h b/src/simplifier/constantBitP/FixedBits.h
index da231aa45b3d5dec76551bb7ca73475626e4af57..6d7fb276327abb4a45bf52da12eb1f9f1254c518 100644 (file)
--- a/src/simplifier/constantBitP/FixedBits.h
+++ b/src/simplifier/constantBitP/FixedBits.h
@@ -39,6 +39,12 @@ namespace simplifier
       init(const FixedBits& copy);
       int uniqueId;
 
+      bool
+      unsignedHolds_new(unsigned val);
+      bool
+      unsignedHolds_old(unsigned val);
+
+
     public:
       FixedBits(int n, bool isBoolean);
 
@@ -79,6 +85,7 @@ namespace simplifier
             return '0';
       }
 
+      // Equality when I was a java programmer sorry!~.
       bool
       operator==(const FixedBits& other) const
       {
@@ -254,7 +261,6 @@ namespace simplifier
       bool
       unsignedHolds(unsigned val);
 
-
       void
       replaceWithContents(const FixedBits& a)
       {
@@ -350,6 +356,9 @@ namespace simplifier
       createRandom(const int length, const int probabilityOfSetting,
           MTRand& rand);
 
+      void
+      fromUnsigned(unsigned val);
+
       static FixedBits
       fromUnsignedInt(int width, unsigned val);
 

diff --git a/src/util/test_cbitp.cpp b/src/util/test_cbitp.cpp
index b7dababfadb4eca5cc0bd75f5e8f92f74bd7b9dc..6c931a6c0e28cb3dd0e88e02692734924a7f66ed 100644 (file)
--- a/src/util/test_cbitp.cpp
+++ b/src/util/test_cbitp.cpp
@@ -180,7 +180,10 @@ namespace simplifier
         {
         if (!FixedBits::equals(*manualChildren[i], *initialChildren[i]))
           {
-          assert(FixedBits::updateOK(*initialChildren[i],*manualChildren[i]));
+          if(!FixedBits::updateOK(*initialChildren[i],*manualChildren[i]))
+            {
+              FatalError("not ok");
+            }
           changed = true;
           }
         }
@@ -199,7 +202,8 @@ namespace simplifier
       // If the status is changed. Then there should have been a change.
       if (CHANGED == manualResult)
         {
-        assert(changed);
+        if (!changed)
+          FatalError("Should have changed");
         }
 
       bool first = maxPrecision(autoChildren, autoOutput, kind, beev);
@@ -482,25 +486,22 @@ struct D
 };
 
 void
-exhaustively_check(const int bitwidth)
+exhaustively_check(const int bitwidth, Result (*transfer)(vector<FixedBits*>&, FixedBits&), int (*op)(int a, int b))
 {
   vector<D> list;
 
-  const Kind kind = BVPLUS;
   const int numberOfInputParams = 2;
-  Result (*transfer)(vector<FixedBits*>&, FixedBits&) = &bvAddBothWays;
 
   assert(numberOfInputParams >0);
   const int mask = pow(2, bitwidth) - 1;
 
-
   // Create all the possible inputs, and apply the function.
   for (int i = 0; i < pow(2, bitwidth * numberOfInputParams); i++)
     {
     D d;
     d.a = i & mask;
     d.b = (i >> bitwidth) & mask;
-    d.c = (d.a + d.b) & mask;
+    d.c = op(d.a,d.b) & mask;
     list.push_back(d);
     }
 
@@ -527,12 +528,15 @@ exhaustively_check(const int bitwidth)
   lengths.push_back(resultLength);
   totalLength += resultLength;
 
+  FixedBits empty(bitwidth, false);
+  FixedBits c_a(bitwidth, false), c_b(bitwidth, false), c_o(bitwidth, false);
+
   const int to_iterate = pow(3, totalLength);
   for (long j = 0; j < to_iterate; j++)
     {
     int current = j;
 
-    if (j% 5000 == 0)
+    if (j% 100000 == 0)
       cerr << j << " of " << to_iterate << endl;
 
     int id = 0;
@@ -558,7 +562,6 @@ exhaustively_check(const int bitwidth)
       current /= 3;
       }
 
-    FixedBits c_a(bitwidth, false), c_b(bitwidth, false), c_o(bitwidth, false);
     bool first = true;
     for (int j = 0; j < list.size(); j++)
       {
@@ -567,9 +570,9 @@ exhaustively_check(const int bitwidth)
         {
         if (first)
           {
-          c_a = FixedBits::fromUnsignedInt(bitwidth, d.a);
-          c_b = FixedBits::fromUnsignedInt(bitwidth, d.b);
-          c_o = FixedBits::fromUnsignedInt(bitwidth, d.c);
+          c_a.fromUnsigned(d.a);
+          c_b.fromUnsigned(d.b);
+          c_o.fromUnsigned(d.c);
           first = false;
           }
         else
@@ -581,25 +584,68 @@ exhaustively_check(const int bitwidth)
         }
       }
 
+
     Result r = transfer(children, output);
     if (r == CONFLICT)
       {
-      assert(first);
+      if(!first)
+        FatalError("Not First");
       }
     else
       {
-      assert(FixedBits::equals(*children[0],c_a));
-      assert(FixedBits::equals(*children[1],c_b));
-      assert(FixedBits::equals(output,c_o));
+      if(!FixedBits::equals(*children[0],c_a))
+        FatalError("First");
+      if(!FixedBits::equals(*children[1],c_b))
+        FatalError("Second");
+      if(!FixedBits::equals(output,c_o))
+        FatalError("Third");
       }
     }
+  for (int i=0; i < children.size();i++)
+    delete children[i];
+}
+
+int plusF(int a, int b)
+{
+  return a+b;
+}
+
+int subF(int a, int b)
+{
+  return a-b;
+}
+
+int leftSF(int a, int b)
+{
+  if (b >= sizeof(int)*8)
+    return 0;
+
+  return a<<b;
+}
+
+int rightSF(int a, int b)
+{
+  if (b >= sizeof(int)*8)
+    return 0;
 
+  return a>>b;
+}
+
+int bvandF(int a, int b)
+{
+  return a &b;
+}
+
+int bvorF(int a, int b)
+{
+  return a | b;
 }
 
 int
 main(void)
 {
-  beev = new BEEV::STPMgr();
+  BEEV::STPMgr stp;
+  beev = &stp;
   beev->UserFlags.disableSimplifications();
 
   Cpp_interface interface(*beev, beev->defaultNodeFactory);
@@ -607,15 +653,18 @@ main(void)
   srand(time(NULL));
   BEEV::ParserBM = beev;
 
-  #ifdef NDEBUG
-    cerr << "needs debug please.";
-    exit(1);
-  #endif
-
-
-  const int bits = 4;
-  exhaustively_check(bits);
+  const int exhaustive_bits = 6;
+  for (int i = 1; i <= exhaustive_bits; i++)
+    {
+    exhaustively_check(i, &bvLeftShiftBothWays, &leftSF);
+    exhaustively_check(i, &bvRightShiftBothWays, &rightSF);
+    exhaustively_check(i, &bvAddBothWays, &plusF);
+    exhaustively_check(i, &bvSubtractBothWays, &subF);
+    exhaustively_check(i, &bvAndBothWays, &bvandF);
+    exhaustively_check(i, &bvOrBothWays, &bvorF);
+    }
 
+  const int bits = 5;
 
   if (true)
     {
@@ -655,37 +704,13 @@ main(void)
     signature.maxInputWidth = bits;
     signature.numberOfInputs = 2;
 
-    // BVADD
-    signature.kind = BVPLUS;
-    exhaustive(&bvAddBothWays, signature);
-
-    // BVRIGHTSHIFT
-    signature.kind = BVRIGHTSHIFT;
-    exhaustive(&bvRightShiftBothWays, signature);
-
     // BVaritmeticRIGHTSHIFT
     signature.kind = BVSRSHIFT;
     exhaustive(&bvArithmeticRightShiftBothWays, signature);
 
-    // BVLEFTSHIFT
-    signature.kind = BVLEFTSHIFT;
-    exhaustive(&bvLeftShiftBothWays, signature);
-
-    // BVSUB
-    signature.kind = BVSUB;
-    exhaustive(&bvSubtractBothWays, signature);
-
     // BVXOR.
     signature.kind = BVXOR;
     exhaustive(&bvXorBothWays, signature);
-
-    // BVAND.
-    signature.kind = BVAND;
-    exhaustive(&bvAndBothWays, signature);
-
-    // BVOR
-    signature.kind = BVOR;
-    exhaustive(&bvOrBothWays, signature);
     }
 
   // n Params at most. (Bool,Bool) -> Bool
@@ -875,6 +900,7 @@ main(void)
 
   // Add had a defect effecting bithWidth > 90.
   // Shifting had a defect effecting bitWidth > 64.
+    if (true)
     {
     vector<FixedBits*> children;
     FixedBits a(150, false);