Improvement. Add a fast exit case to the inequalities.

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

diff --git a/src/simplifier/constantBitP/ConstantBitP_Comparison.cpp b/src/simplifier/constantBitP/ConstantBitP_Comparison.cpp
index 4f99030f54cd4a3d68fc1e28c224633d6d632b82..275a296738fae5638573974aa20843a6e131b589 100644 (file)
--- a/src/simplifier/constantBitP/ConstantBitP_Comparison.cpp
+++ b/src/simplifier/constantBitP/ConstantBitP_Comparison.cpp
@@ -103,9 +103,35 @@ void destroy(CBV a, CBV b, CBV c, CBV d)
        CONSTANTBV::BitVector_Destroy(d);
 }
 
-///////// Signed operations.
+// Fast exit. Without creating min/max.
+bool
+fast_exit(FixedBits& c0, FixedBits& c1)
+{
+  for (int i = c0.getWidth() - 1; i >= 0; i--)
+    {
+      const char c_0 = c0[i];
+      const char c_1 = c1[i];
+
+      if (c_0 == '0')
+        {
+          if (c_1 == '0')
+            continue;
+        }
+      else if (c_0 == '1')
+        {
+          if (c_1 == '1')
+            continue;
+        }
+      else if (c_0 == '*' && c_1 == '*')
+        {
+          return true;
+        }
+      return false;
+    }
+}
 
 
+///////// Signed operations.
 
 
 Result bvSignedLessThanBothWays(FixedBits& c0, FixedBits& c1, FixedBits& output)
@@ -114,6 +140,9 @@ Result bvSignedLessThanBothWays(FixedBits& c0, FixedBits& c1, FixedBits& output)
 
        assert(c0.getWidth() == c1.getWidth());
 
+       if (!output.isFixed(0) && fast_exit(c0,c1))
+          return NO_CHANGE;
+
        CBV c0_min = CONSTANTBV::BitVector_Create(c0.getWidth(), true);
        CBV c0_max = CONSTANTBV::BitVector_Create(c0.getWidth(), true);
        CBV c1_min = CONSTANTBV::BitVector_Create(c0.getWidth(), true);
@@ -257,12 +286,16 @@ Result bvSignedLessThanBothWays(FixedBits& c0, FixedBits& c1, FixedBits& output)
        return NOT_IMPLEMENTED;
 }
 
+
 Result bvSignedLessThanEqualsBothWays(FixedBits& c0, FixedBits &c1, FixedBits& output)
 {
        Result r = NO_CHANGE;
 
        assert(c0.getWidth() == c1.getWidth());
 
+        if (!output.isFixed(0) && fast_exit(c0,c1))
+          return NO_CHANGE;
+
        CBV c0_min = CONSTANTBV::BitVector_Create(c0.getWidth(), true);
        CBV c0_max = CONSTANTBV::BitVector_Create(c0.getWidth(), true);
        CBV c1_min = CONSTANTBV::BitVector_Create(c0.getWidth(), true);
@@ -313,7 +346,7 @@ Result bvSignedLessThanEqualsBothWays(FixedBits& c0, FixedBits &c1, FixedBits& o
                return bvSignedGreaterThanBothWays(c0, c1, t);
        }
 
-       const int msb = c0.getWidth() - 1;
+       const int msb = c0.getWidth() - 1;
 
        if (output.isFixed(0) && output.getValue(0))
        {
@@ -416,6 +449,9 @@ Result bvLessThanBothWays(FixedBits& c0, FixedBits &c1, FixedBits& output)
 
        assert(c0.getWidth() == c1.getWidth());
 
+        if (!output.isFixed(0) && fast_exit(c0,c1))
+          return NO_CHANGE;
+
        CBV c0_min = CONSTANTBV::BitVector_Create(c0.getWidth(), true);
        CBV c0_max = CONSTANTBV::BitVector_Create(c0.getWidth(), true);
        CBV c1_min = CONSTANTBV::BitVector_Create(c0.getWidth(), true);
@@ -525,6 +561,9 @@ Result bvLessThanEqualsBothWays(FixedBits& c0, FixedBits &c1, FixedBits& output)
 
        assert(c0.getWidth() == c1.getWidth());
 
+        if (!output.isFixed(0) && fast_exit(c0,c1))
+          return NO_CHANGE;
+
        CBV c0_min = CONSTANTBV::BitVector_Create(c0.getWidth(), true);
        CBV c0_max = CONSTANTBV::BitVector_Create(c0.getWidth(), true);
        CBV c1_min = CONSTANTBV::BitVector_Create(c0.getWidth(), true);