From: trevor_hansen Date: Fri, 17 Feb 2012 13:48:39 +0000 (+0000) Subject: Improvements speedups for better test code. X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=8e15c81e9bf89f6ffc8e5c40f0ee2325032a40fb;p=francis%2Fstp.git 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 55a08a2..273175a 100644 --- 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 da231aa..6d7fb27 100644 --- 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 b7dabab..6c931a6 100644 --- 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&), int (*op)(int a, int b)) { vector list; - const Kind kind = BVPLUS; const int numberOfInputParams = 2; - Result (*transfer)(vector&, 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<= 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 children; FixedBits a(150, false);