From e06b03868ac3157bde788d9946f60e821d8b5341 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Thu, 29 Mar 2012 23:33:56 +0000 Subject: [PATCH] Improvements to measurement code. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1616 e59a4935-1847-0410-ae03-e826735625c1 --- src/util/test_cbitp.cpp | 40 +++++++++++++++++++++++++++------------- src/util/time_cbitp.cpp | 41 +++++++++++++++++++++++++++++++++-------- 2 files changed, 60 insertions(+), 21 deletions(-) diff --git a/src/util/test_cbitp.cpp b/src/util/test_cbitp.cpp index b9aae70..0da4c9e 100644 --- a/src/util/test_cbitp.cpp +++ b/src/util/test_cbitp.cpp @@ -339,7 +339,7 @@ namespace simplifier { - for (long j = 0; j < pow(3, totalLength); j++) + for (long j = 0; j < pow((double)3, totalLength); j++) { FixedBits output(resultLength, signature.resultType == BOOL_TYPE); @@ -389,10 +389,11 @@ namespace simplifier int transferC =0; int max =0; - int count = 100; + int count = 1000; long st = getCurrentTime(); + const int width =32; - for (int width = 7; width <= 256; width++) + for (int i = 0; i < count; i++) { children.clear(); FixedBits a = FixedBits::createRandom(width, prob, mtrand); @@ -403,7 +404,7 @@ namespace simplifier Detail d; bool imprecise = false; - if (kind == BVDIV) + if (kind == BVDIV || kind == BVMULT || kind == BVMOD || kind == SBVDIV || kind == SBVREM) imprecise = true; checkEqual(children, output, transfer, kind, imprecise,d); if (d.conflict) @@ -417,7 +418,7 @@ namespace simplifier } cerr.setf(ios::fixed); - cerr << "% Count" << count << " prob" << prob << endl; + cerr << "% Count" << count << " prob" << prob << " bits" << width << endl; cerr << setprecision(2) << (getCurrentTime() - st)/1000.0 << "s&" << conflicts << "&" << initial << "&" << transferC << "&" << max << endl; return; @@ -451,7 +452,7 @@ namespace simplifier lengths.push_back(resultLength); totalLength += resultLength; - for (long j = 0; j < pow(3, totalLength); j++) + for (long j = 0; j < pow((double)3, totalLength); j++) { int current = j; @@ -503,6 +504,7 @@ unsignedDivide(vector& children, FixedBits& output) return bvUnsignedDivisionBothWays(children, output, simplifier::constantBitP::beev); } + Result signedDivide(vector& children, FixedBits& output) { @@ -545,10 +547,10 @@ exhaustively_check(const int bitwidth, Result (*transfer)(vector&, F const int numberOfInputParams = 2; assert(numberOfInputParams >0); - const int mask = pow(2, bitwidth) - 1; + const int mask = pow((double)2, bitwidth) - 1; // Create all the possible inputs, and apply the function. - for (int i = 0; i < pow(2, bitwidth * numberOfInputParams); i++) + for (int i = 0; i < pow((double)2, bitwidth * numberOfInputParams); i++) { D d; d.a = i & mask; @@ -583,7 +585,7 @@ exhaustively_check(const int bitwidth, Result (*transfer)(vector&, F FixedBits empty(bitwidth, false); FixedBits c_a(bitwidth, false), c_b(bitwidth, false), c_o(bitwidth, false); - const int to_iterate = pow(3, totalLength); + const int to_iterate = pow((double)3, totalLength); for (long j = 0; j < to_iterate; j++) { int current = j; @@ -728,9 +730,6 @@ main(void) output << "bit-vector or&" << endl; go(&bvOrBothWays, BVOR); - output << "unsigned division&" << endl; - go(&unsignedDivide, BVDIV); - output << "bit-vector xor&" << endl; go(&bvXorBothWays, BVXOR); @@ -743,12 +742,27 @@ main(void) output << "left shift&" << endl; go(&bvLeftShiftBothWays, BVLEFTSHIFT); - output << "arith shift&" << endl; + output << "arithmetic shift&" << endl; go(&bvArithmeticRightShiftBothWays, BVSRSHIFT); output << "addition&" << endl; go(&bvAddBothWays, BVPLUS); + output << "multiplication&" << endl; + go(&multiply, BVMULT); + + output << "unsigned division&" << endl; + go(&unsignedDivide, BVDIV); + + output << "unsigned remainder&" << endl; + go(&unsignedModulus, BVMOD); + + output << "signed division&" << endl; + go(&signedDivide, SBVDIV); + + output << "signed remainder&" << endl; + go(&signedRemainder, SBVREM); + exit(1); } diff --git a/src/util/time_cbitp.cpp b/src/util/time_cbitp.cpp index e76c98a..6acb128 100644 --- a/src/util/time_cbitp.cpp +++ b/src/util/time_cbitp.cpp @@ -40,7 +40,8 @@ public: void stop2() { clock_t total = clock() - start; - cerr << (float(total) / CLOCKS_PER_SEC) << "s"; + cerr.setf(ios::fixed); + cerr << setprecision(2) << (float(total) / CLOCKS_PER_SEC) << "s"; } private: @@ -197,19 +198,25 @@ simplifier::constantBitP::Result signedModulus(vector& children, return bvSignedModulusBothWays(children, output,beev); } -simplifier::constantBitP::Result unsignedDivision(vector& children, +simplifier::constantBitP::Result signedRemainder(vector& children, FixedBits& output) { - return bvUnsignedDivisionBothWays(children, output,beev); + return bvSignedRemainderBothWays(children, output,beev); } -simplifier::constantBitP::Result divide(vector& children, +simplifier::constantBitP::Result unsignedDivision(vector& children, FixedBits& output) { return bvUnsignedDivisionBothWays(children, output,beev); } +simplifier::constantBitP::Result signedDivision(vector& children, + FixedBits& output) +{ + return bvSignedDivisionBothWays(children, output,beev); +} + simplifier::constantBitP::Result multiply(vector& children, FixedBits& output) @@ -259,23 +266,41 @@ main(void) output << "no_op&" << endl; run_with_various_prob(no_op, output); + output << "bit-vector xor&" << endl; + run_with_various_prob(bvXorBothWays, output); + + output << "bit-vector or&" << endl; + run_with_various_prob(bvOrBothWays, output); + + output << "bit-vector and&" << endl; + run_with_various_prob(bvAndBothWays, output); + output << "right shift&" << endl; run_with_various_prob(bvRightShiftBothWays, output); + output << "left shift&" << endl; + run_with_various_prob(bvLeftShiftBothWays, output); + output << "arithmetic shift&" << endl; run_with_various_prob(bvArithmeticRightShiftBothWays, output); + output << "addition&" << endl; + run_with_various_prob(bvAddBothWays, output); + output << "multiplication&" << endl; run_with_various_prob(multiply, output); output << "unsigned division&" << endl; run_with_various_prob(unsignedDivision, output); - output << "bit-vector xor&" << endl; - run_with_various_prob(bvXorBothWays, output); + output << "unsigned remainder&" << endl; + run_with_various_prob(signedRemainder, output); - output << "addition&" << endl; - run_with_various_prob(bvAddBothWays, output); + output << "signed division&" << endl; + run_with_various_prob(signedDivision, output); + + output << "signed remainder&" << endl; + run_with_various_prob(signedRemainder, output); output << "%" << "iterations" << iterations; output << "%" << "bit-width" << iterations; -- 2.47.3