From c0c345e287d79638f9d38f7ff01de979805e299e Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Tue, 27 Mar 2012 12:10:37 +0000 Subject: [PATCH] Improvements to utility code. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1615 e59a4935-1847-0410-ae03-e826735625c1 --- src/util/find_rewrites/rewrite.cpp | 4 +- src/util/find_rewrites/rewrite_rule.h | 4 +- src/util/find_rewrites/rewrite_system.h | 2 +- src/util/test_cbitp.cpp | 148 ++++++++++++++++++------ 4 files changed, 120 insertions(+), 38 deletions(-) diff --git a/src/util/find_rewrites/rewrite.cpp b/src/util/find_rewrites/rewrite.cpp index 085491e..0b28bdb 100644 --- a/src/util/find_rewrites/rewrite.cpp +++ b/src/util/find_rewrites/rewrite.cpp @@ -1014,11 +1014,11 @@ findRewrites(ASTVec& expressions, const vector& values, cons VariableAssignment different; bool bad = false; - const int st = getCurrentTime(); + const long st = getCurrentTime(); if (checkRule(from, to, different, bad)) { - const int checktime = getCurrentTime() - st; + const long checktime = getCurrentTime() - st; equiv[i] = rewriteThroughWithAIGS(equiv[i]); equiv[j] = rewriteThroughWithAIGS(equiv[j]); diff --git a/src/util/find_rewrites/rewrite_rule.h b/src/util/find_rewrites/rewrite_rule.h index 6508cbc..7638199 100644 --- a/src/util/find_rewrites/rewrite_rule.h +++ b/src/util/find_rewrites/rewrite_rule.h @@ -47,7 +47,7 @@ public: writeOut(ostream& outputFileSMT2) const { outputFileSMT2 << ";id:0" << "\tverified_to:" << verified_to_bits << "\ttime:" << getTime() << "\tfrom_difficulty:" - << getDifficulty(getFrom()) << "\tto_difficulty:" << getDifficulty(getTo()) << "\n"; + << getDifficulty(/*getFrom()*/ mgr->CreateBVConst(32,0)) << "\tto_difficulty:" << getDifficulty(/*getTo()*/ mgr->CreateBVConst(32,0)) << "\n"; outputFileSMT2 << "(push 1)" << endl; printer::SMTLIB2_PrintBack(outputFileSMT2, getN(), true); outputFileSMT2 << "(exit)" << endl; @@ -147,7 +147,7 @@ public: timeout.it_value.tv_sec = timeout_ms / 1000; setitimer(ITIMER_VIRTUAL, &timeout, NULL); - const int st = getCurrentTime(); + const long st = getCurrentTime(); int checked_to = 0; // Start it verifying where we left off.. diff --git a/src/util/find_rewrites/rewrite_system.h b/src/util/find_rewrites/rewrite_system.h index 5043991..a1a86d9 100644 --- a/src/util/find_rewrites/rewrite_system.h +++ b/src/util/find_rewrites/rewrite_system.h @@ -304,7 +304,7 @@ public: { VariableAssignment assignment; bool bad = false; - const int st = getCurrentTime(); + const long st = getCurrentTime(); bool r = checkRule(it->getFrom(), it->getTo(), assignment, bad); if (!r || bad) { diff --git a/src/util/test_cbitp.cpp b/src/util/test_cbitp.cpp index 6c931a6..b9aae70 100644 --- a/src/util/test_cbitp.cpp +++ b/src/util/test_cbitp.cpp @@ -100,9 +100,25 @@ namespace simplifier } } + struct Detail + { + Detail() + { + conflict =false; + maxFixed =0; + transferFixed = 0; + initial =0; + } + bool conflict; + int maxFixed; + int transferFixed; + int initial; + + }; + void checkEqual(vector& initialChildren, FixedBits& initialOutput, Result - (*transfer)(vector&, FixedBits&), Kind kind, bool imprecise) + (*transfer)(vector&, FixedBits&), Kind kind, bool imprecise, Detail& d) { // Make two copies of the initial values. One to send to the maximum Precision. // The other to send to the manually built transfer functions. @@ -128,10 +144,17 @@ namespace simplifier for (int i = 0; i < (int) initialChildren.size(); i++) { tempChildren.push_back(new FixedBits(*(manualChildren[i]))); + d.initial += tempChildren[i]->countFixed(); } + d.initial += initialOutput.countFixed(); Result tempResult = transfer(tempChildren, tempOutput); + for (int i = 0; i < (int) tempChildren.size(); i++) + d.transferFixed += tempChildren[i]->countFixed(); + d.transferFixed += tempOutput.countFixed(); + + // First and second time should have the same conflict status. if ((manualResult == CONFLICT) != (tempResult == CONFLICT)) { @@ -209,6 +232,12 @@ namespace simplifier bool first = maxPrecision(autoChildren, autoOutput, kind, beev); beev->ClearAllTables(); + if (first) + d.conflict = true; + for (int i = 0; i < (int) autoChildren.size(); i++) + d.maxFixed += autoChildren[i]->countFixed(); + d.maxFixed += autoOutput.countFixed(); + if (debug_printAll) { cout << "initial: "; @@ -335,7 +364,8 @@ namespace simplifier continue; } - checkEqual(children, output, transfer, signature.kind, signature.imprecise); + Detail d; + checkEqual(children, output, transfer, signature.kind, signature.imprecise,d); } } @@ -347,28 +377,49 @@ namespace simplifier // Random. void runSomeRandom(Result - (*transfer)(vector&, FixedBits&), const Kind kind, const vector late, FixedBits out) + (*transfer)(vector&, FixedBits&), const Kind kind, int prob) { - const int PROBABILITY_OF_SETTING = 5; - - cout << "Running Random:" << kind << endl; - assert(late.size() ==2); - MTRand mtrand; + MTRand mtrand(1); + srand(0); vector children; - for (int i = 0; i < 2000; i++) + int conflicts =0; + int initial =0; + int transferC =0; + int max =0; + + int count = 100; + long st = getCurrentTime(); + + for (int width = 7; width <= 256; width++) { children.clear(); - FixedBits a = FixedBits::createRandom(out.getWidth(), PROBABILITY_OF_SETTING, mtrand); + FixedBits a = FixedBits::createRandom(width, prob, mtrand); children.push_back(&a); - FixedBits b = FixedBits::createRandom(out.getWidth(), PROBABILITY_OF_SETTING, mtrand); + FixedBits b = FixedBits::createRandom(width, prob, mtrand); children.push_back(&b); - FixedBits output = FixedBits::createRandom(out.getWidth(), PROBABILITY_OF_SETTING, mtrand); - - checkEqual(children, output, transfer, kind, false); - cout << "."; + FixedBits output = FixedBits::createRandom(width, prob, mtrand); + + Detail d; + bool imprecise = false; + if (kind == BVDIV) + imprecise = true; + checkEqual(children, output, transfer, kind, imprecise,d); + if (d.conflict) + conflicts++; + else + { + initial += d.initial; + transferC += d.transferFixed; + max += d.maxFixed; + } } + + cerr.setf(ios::fixed); + cerr << "% Count" << count << " prob" << prob << endl; + cerr << setprecision(2) << (getCurrentTime() - st)/1000.0 << "s&" << conflicts << "&" << initial << "&" << transferC << "&" << max << endl; + return; } @@ -427,7 +478,8 @@ namespace simplifier current /= 3; } - checkEqual(children, output, transfer, kind, false); + Detail d; + checkEqual(children, output, transfer, kind, false,d); } for (unsigned i = 0; i < children.size(); i++) @@ -641,18 +693,65 @@ int bvorF(int a, int b) return a | b; } +void +go(Result (*transfer)(vector&, FixedBits&), const Kind kind) +{ + runSomeRandom(transfer, kind, 1 ); + cerr << "&"; + runSomeRandom(transfer, kind, 5 ); + cerr << "&"; + runSomeRandom(transfer, kind, 50 ); + cerr << "\\\\"; +} + + int main(void) { BEEV::STPMgr stp; beev = &stp; beev->UserFlags.disableSimplifications(); + beev->UserFlags.division_by_zero_returns_one_flag = true; Cpp_interface interface(*beev, beev->defaultNodeFactory); interface.startup(); srand(time(NULL)); BEEV::ParserBM = beev; + // Add had a defect effecting bithWidth > 90. + // Shifting had a defect effecting bitWidth > 64. + + ostream& output = cerr; + + if (true) + { + output << "bit-vector or&" << endl; + go(&bvOrBothWays, BVOR); + + output << "unsigned division&" << endl; + go(&unsignedDivide, BVDIV); + + output << "bit-vector xor&" << endl; + go(&bvXorBothWays, BVXOR); + + output << "bit-vector and&" << endl; + go(&bvAndBothWays, BVAND); + + output << "right shift&" << endl; + go(&bvRightShiftBothWays, BVRIGHTSHIFT); + + output << "left shift&" << endl; + go(&bvLeftShiftBothWays, BVLEFTSHIFT); + + output << "arith shift&" << endl; + go(&bvArithmeticRightShiftBothWays, BVSRSHIFT); + + output << "addition&" << endl; + go(&bvAddBothWays, BVPLUS); + + exit(1); + } + const int exhaustive_bits = 6; for (int i = 1; i <= exhaustive_bits; i++) { @@ -898,23 +997,6 @@ main(void) } } - // Add had a defect effecting bithWidth > 90. - // Shifting had a defect effecting bitWidth > 64. - if (true) - { - vector children; - FixedBits a(150, false); - FixedBits b(150, false); - - children.push_back(&a); - children.push_back(&b); - FixedBits output(150, false); - runSomeRandom(&bvAndBothWays, BVAND, children, output); - runSomeRandom(&bvRightShiftBothWays, BVRIGHTSHIFT, children, output); - runSomeRandom(&bvLeftShiftBothWays, BVLEFTSHIFT, children, output); - runSomeRandom(&bvAddBothWays, BVPLUS, children, output); - runSomeRandom(&bvOrBothWays, BVOR, children, output); - } cout << "Done" << endl; -- 2.47.3