From: trevor_hansen Date: Tue, 10 Apr 2012 04:15:35 +0000 (+0000) Subject: Improvements the the code for measuring the effect of propagators. X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=ef0ad55375f92553f679cbd8b6dcf999b7d6c5f2;p=francis%2Fstp.git Improvements the the code for measuring the effect of propagators. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1634 e59a4935-1847-0410-ae03-e826735625c1 --- diff --git a/src/util/Relations.cpp b/src/util/Relations.cpp new file mode 100644 index 0000000..6464497 --- /dev/null +++ b/src/util/Relations.cpp @@ -0,0 +1,20 @@ +/* + * Relations.cpp + * + * Created on: 10/04/2012 + * Author: thansen + */ + +#include "Relations.h" + +Relations::Relations() +{ + // TODO Auto-generated constructor stub + +} + +Relations::~Relations() +{ + // TODO Auto-generated destructor stub +} + diff --git a/src/util/Relations.h b/src/util/Relations.h new file mode 100644 index 0000000..3b927e8 --- /dev/null +++ b/src/util/Relations.h @@ -0,0 +1,80 @@ +/* + * Relations.h + * + * Created on: 10/04/2012 + * Author: thansen + */ + +#ifndef RELATIONS_H_ +#define RELATIONS_H_ + +#include +#include +#include "../AST/AST.h" +#include "../simplifier/constantBitP/FixedBits.h" +#include "../simplifier/constantBitP/MersenneTwister.h" + +#include "../simplifier/constantBitP/ConstantBitP_TransferFunctions.h" +#include "../extlib-constbv/constantbv.h" + +#include "../AST/ASTKind.h" +#include "../STPManager/STPManager.h" +#include "../cpp_interface/cpp_interface.h" +#include + +using namespace std; +using simplifier::constantBitP::FixedBits; +using namespace simplifier::constantBitP; + + +struct Relations +{ + struct Relation + { + FixedBits a,b,output; + int initial; + Relation(FixedBits a_, FixedBits b_, FixedBits output_) + : a(a_), b(b_), output(output_) + { + initial = a.countFixed() + b.countFixed() + output.countFixed(); + } + }; + + list relations; + + Relations (int iterations, int bitWidth,Kind k, STPMgr*beev, int probabilityOfFixing) + { + MTRand rand; + + for (int i = 0; i < iterations; i++) + { + FixedBits a = FixedBits::createRandom(bitWidth, 100, rand); + FixedBits b = FixedBits::createRandom(bitWidth, 100, rand); + + assert(a.isTotallyFixed()); + assert(b.isTotallyFixed()); + ASTVec c; + c.push_back(beev->CreateBVConst(a.GetBVConst(), bitWidth)); + c.push_back(beev->CreateBVConst(b.GetBVConst(), bitWidth)); + ASTNode result = NonMemberBVConstEvaluator(beev, k, c, bitWidth); + FixedBits output = FixedBits::concreteToAbstract(result); + + for (int i = 0; i < a.getWidth(); i++) + { + if (rand.randInt() % 100 >= probabilityOfFixing) + a.setFixed(i, false); + if (rand.randInt() % 100 >= probabilityOfFixing) + b.setFixed(i, false); + } + for (int i = 0; i < output.getWidth(); i++) + if (rand.randInt() % 100 >= probabilityOfFixing) + output.setFixed(i, false); + + Relation r(a, b, output); + relations.push_back(r); + } + } +}; + + +#endif /* RELATIONS_H_ */ diff --git a/src/util/StopWatch.h b/src/util/StopWatch.h new file mode 100644 index 0000000..f00a4b4 --- /dev/null +++ b/src/util/StopWatch.h @@ -0,0 +1,36 @@ +/* + * StopWatch.h + * + * Created on: 10/04/2012 + * Author: thansen + */ + +#ifndef STOPWATCH_H_ +#define STOPWATCH_H_ + +#include + +class Stopwatch +{ +public: + Stopwatch() : + start(std::clock()) + { + } + void stop() + { + clock_t total = clock() - start; + cerr << "ticks: " << total << " " << (float(total) / CLOCKS_PER_SEC) << "s" << endl; + } + clock_t stop2() + { + clock_t total = clock() - start; + return total; + } + +private: + std::clock_t start; +}; + + +#endif /* STOPWATCH_H_ */ diff --git a/src/util/test_cbitp.cpp b/src/util/test_cbitp.cpp index 0da4c9e..1c51988 100644 --- a/src/util/test_cbitp.cpp +++ b/src/util/test_cbitp.cpp @@ -21,6 +21,9 @@ #include "../STPManager/STP.h" #include "../cpp_interface/cpp_interface.h" +#include "StopWatch.h" +#include "Relations.h" + using simplifier::constantBitP::FixedBits; using namespace simplifier::constantBitP; @@ -379,9 +382,6 @@ namespace simplifier runSomeRandom(Result (*transfer)(vector&, FixedBits&), const Kind kind, int prob) { - MTRand mtrand(1); - srand(0); - vector children; int conflicts =0; @@ -390,36 +390,49 @@ namespace simplifier int max =0; int count = 1000; - long st = getCurrentTime(); - const int width =32; + const int width =32; + + Relations r(count,width,kind, beev, prob); - for (int i = 0; i < count; i++) + Stopwatch s; + list::iterator it = r.relations.begin(); + while(it != r.relations.end()) { + Relations::Relation& rel = *it; + FixedBits& a = rel.a; + FixedBits& b = rel.b; + FixedBits& output = rel.output; + children.clear(); - FixedBits a = FixedBits::createRandom(width, prob, mtrand); children.push_back(&a); - FixedBits b = FixedBits::createRandom(width, prob, mtrand); children.push_back(&b); - FixedBits output = FixedBits::createRandom(width, prob, mtrand); Detail d; bool imprecise = false; if (kind == BVDIV || kind == BVMULT || kind == BVMOD || kind == SBVDIV || kind == SBVREM) imprecise = true; checkEqual(children, output, transfer, kind, imprecise,d); - if (d.conflict) - conflicts++; - else - { - initial += d.initial; - transferC += d.transferFixed; - max += d.maxFixed; - } + + assert(!d.conflicts); + + initial += d.initial; + transferC += d.transferFixed; + max += d.maxFixed; + + it++; } + assert(max >= transferC); + assert(transferC >= initial); + + int percent = 100* ((float)transferC - initial) / (max - initial); + if ((max-initial) ==0) + percent = 100; + clock_t t = s.stop2(); cerr.setf(ios::fixed); cerr << "% Count" << count << " prob" << prob << " bits" << width << endl; - cerr << setprecision(2) << (getCurrentTime() - st)/1000.0 << "s&" << conflicts << "&" << initial << "&" << transferC << "&" << max << endl; + cerr << "&" << setprecision(2) << (float(t) / CLOCKS_PER_SEC) << "s"; + cerr << "&" << initial << "&" << transferC << "&" << max << "&" << percent << "\\%\n" ; return; } @@ -699,13 +712,35 @@ void go(Result (*transfer)(vector&, FixedBits&), const Kind kind) { runSomeRandom(transfer, kind, 1 ); - cerr << "&"; runSomeRandom(transfer, kind, 5 ); - cerr << "&"; runSomeRandom(transfer, kind, 50 ); cerr << "\\\\"; } +void g() +{ + FixedBits a(3,false); + FixedBits b(3,false); + a.setFixed(0,true); + a.setValue(0,true); + + b.setFixed(1,true); + b.setValue(1,true); + + vector c; + c.push_back(&a); + c.push_back(&b); + + FixedBits output(3,false); + output.setFixed(0,true); + output.setValue(0,true); + output.setFixed(2,true); + output.setValue(2,true); + + + multiply(c,output); +} + int main(void) @@ -727,40 +762,49 @@ main(void) if (true) { - output << "bit-vector or&" << endl; - go(&bvOrBothWays, BVOR); + output << "signed greater than equals" << endl; + go(&bvSignedGreaterThanEqualsBothWays, BVSGE); + + output << "unsigned less than" << endl; + go(&bvLessThanEqualsBothWays, BVLT); - output << "bit-vector xor&" << endl; - go(&bvXorBothWays, BVXOR); + output << "equals" << endl; + go(&bvEqualsBothWays, EQ); + + output << "bit-vector xor" << endl; + go(&bvXorBothWays, BVXOR); + + output << "bit-vector or" << endl; + go(&bvOrBothWays, BVOR); - output << "bit-vector and&" << endl; + output << "bit-vector and" << endl; go(&bvAndBothWays, BVAND); - output << "right shift&" << endl; + output << "right shift" << endl; go(&bvRightShiftBothWays, BVRIGHTSHIFT); - output << "left shift&" << endl; + output << "left shift" << endl; go(&bvLeftShiftBothWays, BVLEFTSHIFT); - output << "arithmetic shift&" << endl; + output << "arithmetic shift" << endl; go(&bvArithmeticRightShiftBothWays, BVSRSHIFT); - output << "addition&" << endl; + output << "addition" << endl; go(&bvAddBothWays, BVPLUS); - output << "multiplication&" << endl; + output << "multiplication" << endl; go(&multiply, BVMULT); - output << "unsigned division&" << endl; + output << "unsigned division" << endl; go(&unsignedDivide, BVDIV); - output << "unsigned remainder&" << endl; + output << "unsigned remainder" << endl; go(&unsignedModulus, BVMOD); - output << "signed division&" << endl; + output << "signed division" << endl; go(&signedDivide, SBVDIV); - output << "signed remainder&" << endl; + output << "signed remainder" << endl; go(&signedRemainder, SBVREM); exit(1); diff --git a/src/util/time_cbitp.cpp b/src/util/time_cbitp.cpp index eb4cfb1..24fc610 100644 --- a/src/util/time_cbitp.cpp +++ b/src/util/time_cbitp.cpp @@ -12,40 +12,20 @@ #include "../cpp_interface/cpp_interface.h" #include +#include "StopWatch.h" +#include "Relations.h" + using namespace std; using simplifier::constantBitP::FixedBits; using namespace simplifier::constantBitP; -const int iterations = 100000; +const int iterations = 500000; const unsigned bitWidth = 64; BEEV::STPMgr* beev; -class Stopwatch -{ -public: - Stopwatch() : - start(std::clock()) - { - } - void stop() - { - clock_t total = clock() - start; - cerr << "ticks: " << total << " " << (float(total) / CLOCKS_PER_SEC) << "s" << endl; - } - clock_t stop2() - { - clock_t total = clock() - start; - return total; - //cerr.setf(ios::fixed); -// cerr << setprecision(2) << (float(total) / CLOCKS_PER_SEC) << "s"; - } - -private: - std::clock_t start; -}; @@ -146,18 +126,6 @@ void run(Result(*transfer)(vector&, FixedBits&), const int probabili return; } -struct Relation -{ - FixedBits a,b,output; - int initial; - Relation(FixedBits a_, FixedBits b_, FixedBits output_) - : a(a_), b(b_), output(output_) - { - initial = a.countFixed() + b.countFixed() + output.countFixed(); - } - -}; - void runSimple(Result (*transfer)(vector&, FixedBits&), const int probabilityOfFixing, ostream& output, Kind k) @@ -165,47 +133,17 @@ runSimple(Result int conflicts = 0; - MTRand rand; - int initially_fixed = 0; int finally_fixed = 0; - list relations; - - for (int i = 0; i < iterations; i++) - { - FixedBits a = FixedBits::createRandom(bitWidth, 100, rand); - FixedBits b = FixedBits::createRandom(bitWidth, 100, rand); - - assert(a.isTotallyFixed()); - assert(b.isTotallyFixed()); - ASTVec c; - c.push_back(beev->CreateBVConst(a.GetBVConst(), bitWidth)); - c.push_back(beev->CreateBVConst(b.GetBVConst(), bitWidth)); - ASTNode result = NonMemberBVConstEvaluator(beev, k, c, bitWidth); - FixedBits output = FixedBits::concreteToAbstract(result); - - for (int i = 0; i < a.getWidth(); i++) - { - if (rand.randInt() % 100 >= probabilityOfFixing) - a.setFixed(i, false); - if (rand.randInt() % 100 >= probabilityOfFixing) - b.setFixed(i, false); - } - for (int i = 0; i < output.getWidth(); i++) - if (rand.randInt() % 100 >= probabilityOfFixing) - output.setFixed(i, false); - - Relation r(a, b, output); - relations.push_back(r); - } + Relations r(iterations,bitWidth,k, beev, probabilityOfFixing); Stopwatch s; - for (int i = 0; i < iterations; i++) + list::iterator it = r.relations.begin(); + while(it != r.relations.end()) { - - Relation& rel = relations.back(); + Relations::Relation& rel = *it; FixedBits& a = rel.a; FixedBits& b = rel.b; FixedBits& output = rel.output; @@ -223,7 +161,7 @@ runSimple(Result finally_fixed += final; initially_fixed += rel.initial; - relations.pop_back(); + it++; } clock_t t = s.stop2();