From 3d353527543d112938adc9f2571ad07bdb061524 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Sun, 22 Apr 2012 11:52:33 +0000 Subject: [PATCH] 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 --- .../constantBitP/ConstantBitP_Comparison.cpp | 43 ++++++++++++++++++- 1 file changed, 41 insertions(+), 2 deletions(-) diff --git a/src/simplifier/constantBitP/ConstantBitP_Comparison.cpp b/src/simplifier/constantBitP/ConstantBitP_Comparison.cpp index 4f99030..275a296 100644 --- 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); -- 2.47.3