From 4cb203c14a66786adef1dcbf3d658bf5560507b5 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Mon, 23 Apr 2012 02:09:15 +0000 Subject: [PATCH] Changes to code for experiments. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1653 e59a4935-1847-0410-ae03-e826735625c1 --- src/util/checkEqual.include | 247 ++++++++++++++++++++++++++ src/util/test_cbitp.cpp | 339 ++++++------------------------------ 2 files changed, 297 insertions(+), 289 deletions(-) create mode 100644 src/util/checkEqual.include diff --git a/src/util/checkEqual.include b/src/util/checkEqual.include new file mode 100644 index 0000000..2dc35d9 --- /dev/null +++ b/src/util/checkEqual.include @@ -0,0 +1,247 @@ +// Very rough I know. One the way to being made a class. + +#include "../simplifier/constantBitP/ConstantBitP_MaxPrecision.h" + + const bool debug_printAll = false; + + void + print(const vector children, const FixedBits& output, Kind k) + { + if (2 == children.size()) + cout << "(" << *(children[0]) << " " << k << " " << *(children[1]) << ")" << " == " << output << endl; + else + { + cout << "(" << k << " "; + for (unsigned i = 0; i < children.size(); i++) + cout << *(children[i]) << " "; + cout << ")" << " == " << output << endl; + } + } + + + void + error(Kind kind, vector initialChildren, FixedBits initialOutput, // + vector autoChildren, FixedBits autoOutput, // + vector manualChildren, FixedBits manualOutput) + { + + cerr << "difference(kind:" << kind << ")" << endl; + const int size = initialChildren.size(); + + cerr << "--------------The Initial Values that were passed to the function" << endl; + for (int i = 0; i < size; i++) + cerr << ":" << *(initialChildren[i]) << endl; + cerr << "result:" << initialOutput << endl; + + cerr << "--------------Values from the Solver" << endl; + for (int i = 0; i < size; i++) + cerr << ":" << *(autoChildren[i]) << endl; + cerr << "result:" << autoOutput << endl; + + cerr << "--------------Values from the Implemented Transfer Function" << endl; + for (int i = 0; i < size; i++) + cerr << ":" << *(manualChildren[i]) << endl; + cerr << "result:" << manualOutput << endl; + + FatalError("As described"); + } + +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, 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. + vector manualChildren; + vector autoChildren; + + for (int i = 0; i < (int) initialChildren.size(); i++) + { + manualChildren.push_back(new FixedBits(*(initialChildren[i]))); + autoChildren.push_back(new FixedBits(*(initialChildren[i]))); + } + + FixedBits manualOutput(initialOutput); + FixedBits autoOutput(initialOutput); + + Result manualResult = transfer(manualChildren, manualOutput); + + // Make a copy of the manualResult so we can check if it varies after calling the transfer function a second time. + + FixedBits tempOutput(manualOutput); + vector tempChildren; + + 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)) + { + cerr << "One conflict, both conflict"; + error(kind, initialChildren, initialOutput, autoChildren, autoOutput, manualChildren, manualOutput); + } + + bool different = !FixedBits::equals(tempOutput, manualOutput); + for (int i = 0; i < (int) initialChildren.size(); i++) + { + if (!FixedBits::equals(*tempChildren[i], *manualChildren[i])) + different = true; + } + + // running it immediately afterwards with the same input/output should cause no changes. + if (manualResult != CONFLICT && (CHANGED == tempResult || different)) + { + cerr << "Result varied after second call" << endl; + cerr << "first"; + print(manualChildren, manualOutput, kind); + cerr << "second"; + print(tempChildren, tempOutput, kind); + error(kind, initialChildren, initialOutput, autoChildren, autoOutput, manualChildren, manualOutput); + } + for (int i = 0; i < (int) initialChildren.size(); i++) + { + delete tempChildren[i]; + } + + // find if the values have changed. If they've changed, ensure they follow the lattice. + bool changed = false; + if (!FixedBits::equals(initialOutput, manualOutput)) + { + if (!FixedBits::updateOK(initialOutput, manualOutput)) + { + // BAD UPDATE. + cerr << "bad update." << "Value changed not according to the lattice" << endl; + print(manualChildren, manualOutput, kind); + error(kind, initialChildren, initialOutput, autoChildren, autoOutput, manualChildren, manualOutput); + + } + changed = true; + } + + for (int i = 0; i < (int) initialChildren.size(); i++) + { + if (!FixedBits::equals(*manualChildren[i], *initialChildren[i])) + { + if (!FixedBits::updateOK(*initialChildren[i], *manualChildren[i])) + { + FatalError("not ok"); + } + changed = true; + } + } + + // if they've changed the status should have changed. + if (changed && manualResult != NOT_IMPLEMENTED) + { + // if changed then manualResult should be conflict or changed. + if (!(CHANGED == manualResult || CONFLICT == manualResult)) + { + cerr << "result should be changed or conflict" << endl; + error(kind, initialChildren, initialOutput, autoChildren, autoOutput, manualChildren, manualOutput); + } + } + + // If the status is changed. Then there should have been a change. + if (CHANGED == manualResult) + { + if (!changed) + FatalError("Should have changed"); + } + + bool first = maxPrecision(autoChildren, autoOutput, kind, mgr); + mgr->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: "; + print(initialChildren, initialOutput, kind); + + cout << " manual:"; + print(manualChildren, manualOutput, kind); + + cout << " auto:"; + print(autoChildren, autoOutput, kind); + } + + // if we failed on the first time through. Then the generated equation is impossible. + // For example: (= (bvand 1 0) 1) + // If it's bad, then the transfer function should have reported it. + + if (first) + { + if (!imprecise && CONFLICT != manualResult) + { + cerr << "TRANSFER FUNCTION DIDN'T DETECT IT WAS BAD" << endl; + cerr << "result was:" << manualResult << endl; + error(kind, initialChildren, initialOutput, autoChildren, autoOutput, manualChildren, manualOutput); + } + } + else + { + // if it wasn't bad, then the transfer function shouldn't say it is. + if (CONFLICT == manualResult) + { + cerr << "TRANSFER FUNCTION REPORTED CONFLICT WHEN THERE WAS NONE." << endl; + cerr << "result was:" << manualResult << endl; + error(kind, initialChildren, initialOutput, autoChildren, autoOutput, manualChildren, manualOutput); + } + + if (imprecise) + { + if (!FixedBits::in(autoOutput, manualOutput)) + { + error(kind, initialChildren, initialOutput, autoChildren, autoOutput, manualChildren, manualOutput); + } + } + else if (!FixedBits::equals(autoOutput, manualOutput)) + error(kind, initialChildren, initialOutput, autoChildren, autoOutput, manualChildren, manualOutput); + + for (int i = 0; i < (int) initialChildren.size(); i++) + { + if (imprecise) + { + if (!FixedBits::in(*(autoChildren[i]), *(manualChildren[i]))) + error(kind, initialChildren, initialOutput, autoChildren, autoOutput, manualChildren, manualOutput); + } + else if (!FixedBits::equals(*(autoChildren[i]), *(manualChildren[i]))) + error(kind, initialChildren, initialOutput, autoChildren, autoOutput, manualChildren, manualOutput); + } + } + for (int i = 0; i < (int) initialChildren.size(); i++) + { + delete manualChildren[i]; + delete autoChildren[i]; + } +} diff --git a/src/util/test_cbitp.cpp b/src/util/test_cbitp.cpp index 42ff756..04ee963 100644 --- a/src/util/test_cbitp.cpp +++ b/src/util/test_cbitp.cpp @@ -35,38 +35,9 @@ namespace simplifier using namespace BEEV; - STPMgr * beev; + STPMgr * mgr; bool isDivide = false; - const bool debug_printAll = false; - - void - error(Kind kind, vector initialChildren, FixedBits initialOutput, // - vector autoChildren, FixedBits autoOutput, // - vector manualChildren, FixedBits manualOutput) - { - - cerr << "difference(kind:" << kind << ")" << endl; - const int size = initialChildren.size(); - - cerr << "--------------The Initial Values that were passed to the function" << endl; - for (int i = 0; i < size; i++) - cerr << ":" << *(initialChildren[i]) << endl; - cerr << "result:" << initialOutput << endl; - - cerr << "--------------Values from the Solver" << endl; - for (int i = 0; i < size; i++) - cerr << ":" << *(autoChildren[i]) << endl; - cerr << "result:" << autoOutput << endl; - - cerr << "--------------Values from the Implemented Transfer Function" << endl; - for (int i = 0; i < size; i++) - cerr << ":" << *(manualChildren[i]) << endl; - cerr << "result:" << manualOutput << endl; - - FatalError("As described"); - } - // Set the given fixed bit to one of three values. void setV(FixedBits& result, int id, int val) @@ -89,220 +60,7 @@ namespace simplifier } } - void - print(const vector children, const FixedBits& output, Kind k) - { - if (2 == children.size()) - cout << "(" << *(children[0]) << " " << k << " " << *(children[1]) << ")" << " == " << output << endl; - else - { - cout << "(" << k << " "; - for (unsigned i = 0; i < children.size(); i++) - cout << *(children[i]) << " "; - cout << ")" << " == " << output << endl; - } - } - - 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, 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. - vector manualChildren; - vector autoChildren; - - for (int i = 0; i < (int) initialChildren.size(); i++) - { - manualChildren.push_back(new FixedBits(*(initialChildren[i]))); - autoChildren.push_back(new FixedBits(*(initialChildren[i]))); - } - - FixedBits manualOutput(initialOutput); - FixedBits autoOutput(initialOutput); - - Result manualResult = transfer(manualChildren, manualOutput); - - // Make a copy of the manualResult so we can check if it varies after calling the transfer function a second time. - - FixedBits tempOutput(manualOutput); - vector tempChildren; - - 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)) - { - cerr << "One conflict, both conflict"; - error(kind, initialChildren, initialOutput, autoChildren, autoOutput, manualChildren, manualOutput); - } - - bool different = !FixedBits::equals(tempOutput, manualOutput); - for (int i = 0; i < (int) initialChildren.size(); i++) - { - if (!FixedBits::equals(*tempChildren[i], *manualChildren[i])) - different = true; - } - - // running it immediately afterwards with the same input/output should cause no changes. - if (manualResult != CONFLICT && (CHANGED == tempResult || different)) - { - cerr << "Result varied after second call" << endl; - cerr << "first"; - print(manualChildren, manualOutput, kind); - cerr << "second"; - print(tempChildren, tempOutput, kind); - error(kind, initialChildren, initialOutput, autoChildren, autoOutput, manualChildren, manualOutput); - } - for (int i = 0; i < (int) initialChildren.size(); i++) - { - delete tempChildren[i]; - } - - // find if the values have changed. If they've changed, ensure they follow the lattice. - bool changed = false; - if (!FixedBits::equals(initialOutput, manualOutput)) - { - if (!FixedBits::updateOK(initialOutput, manualOutput)) - { - // BAD UPDATE. - cerr << "bad update." << "Value changed not according to the lattice" << endl; - print(manualChildren, manualOutput, kind); - error(kind, initialChildren, initialOutput, autoChildren, autoOutput, manualChildren, manualOutput); - - } - changed = true; - } - - for (int i = 0; i < (int) initialChildren.size(); i++) - { - if (!FixedBits::equals(*manualChildren[i], *initialChildren[i])) - { - if(!FixedBits::updateOK(*initialChildren[i],*manualChildren[i])) - { - FatalError("not ok"); - } - changed = true; - } - } - - // if they've changed the status should have changed. - if (changed && manualResult != NOT_IMPLEMENTED) - { - // if changed then manualResult should be conflict or changed. - if (!(CHANGED == manualResult || CONFLICT == manualResult)) - { - cerr << "result should be changed or conflict" << endl; - error(kind, initialChildren, initialOutput, autoChildren, autoOutput, manualChildren, manualOutput); - } - } - - // If the status is changed. Then there should have been a change. - if (CHANGED == manualResult) - { - if (!changed) - FatalError("Should have changed"); - } - - 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: "; - print(initialChildren, initialOutput, kind); - - cout << " manual:"; - print(manualChildren, manualOutput, kind); - - cout << " auto:"; - print(autoChildren, autoOutput, kind); - } - - // if we failed on the first time through. Then the generated equation is impossible. - // For example: (= (bvand 1 0) 1) - // If it's bad, then the transfer function should have reported it. - - if (first) - { - if (!imprecise && CONFLICT != manualResult) - { - cerr << "TRANSFER FUNCTION DIDN'T DETECT IT WAS BAD" << endl; - cerr << "result was:" << manualResult << endl; - error(kind, initialChildren, initialOutput, autoChildren, autoOutput, manualChildren, manualOutput); - } - } - else - { - // if it wasn't bad, then the transfer function shouldn't say it is. - if (CONFLICT == manualResult) - { - cerr << "TRANSFER FUNCTION REPORTED CONFLICT WHEN THERE WAS NONE." << endl; - cerr << "result was:" << manualResult << endl; - error(kind, initialChildren, initialOutput, autoChildren, autoOutput, manualChildren, manualOutput); - } - - if (imprecise) - { - if (!FixedBits::in(autoOutput, manualOutput)) - { - error(kind, initialChildren, initialOutput, autoChildren, autoOutput, manualChildren, manualOutput); - } - } - else if (!FixedBits::equals(autoOutput, manualOutput)) - error(kind, initialChildren, initialOutput, autoChildren, autoOutput, manualChildren, manualOutput); - - for (int i = 0; i < (int) initialChildren.size(); i++) - { - if (imprecise) - { - if (!FixedBits::in(*(autoChildren[i]), *(manualChildren[i]))) - error(kind, initialChildren, initialOutput, autoChildren, autoOutput, manualChildren, manualOutput); - } - else if (!FixedBits::equals(*(autoChildren[i]), *(manualChildren[i]))) - error(kind, initialChildren, initialOutput, autoChildren, autoOutput, manualChildren, manualOutput); - } - } - for (int i = 0; i < (int) initialChildren.size(); i++) - { - delete manualChildren[i]; - delete autoChildren[i]; - } - } +#include "checkEqual.include" // Exhaustively generate all the bitpatterns for the number of inputs. // For each input compare the solver's result to the manual Transfer functions result. @@ -392,7 +150,7 @@ namespace simplifier int count = 1000; const int width =32; - Relations r(count,width,kind, beev, prob); + Relations r(count,width,kind, mgr, prob); Stopwatch s; list::iterator it = r.relations.begin(); @@ -508,38 +266,38 @@ namespace simplifier Result multiply(vector& children, FixedBits& output) { - return bvMultiplyBothWays(children, output, simplifier::constantBitP::beev, 0); + return bvMultiplyBothWays(children, output, simplifier::constantBitP::mgr, 0); } Result unsignedDivide(vector& children, FixedBits& output) { - return bvUnsignedDivisionBothWays(children, output, simplifier::constantBitP::beev); + return bvUnsignedDivisionBothWays(children, output, simplifier::constantBitP::mgr); } Result signedDivide(vector& children, FixedBits& output) { - return bvSignedDivisionBothWays(children, output, simplifier::constantBitP::beev); + return bvSignedDivisionBothWays(children, output, simplifier::constantBitP::mgr); } Result signedRemainder(vector& children, FixedBits& output) { - return bvSignedRemainderBothWays(children, output, simplifier::constantBitP::beev); + return bvSignedRemainderBothWays(children, output, simplifier::constantBitP::mgr); } Result signedModulus(vector& children, FixedBits& output) { - return bvSignedModulusBothWays(children, output, simplifier::constantBitP::beev); + return bvSignedModulusBothWays(children, output, simplifier::constantBitP::mgr); } Result unsignedModulus(vector& children, FixedBits& output) { - return bvUnsignedModulusBothWays(children, output, simplifier::constantBitP::beev); + return bvUnsignedModulusBothWays(children, output, simplifier::constantBitP::mgr); } struct D @@ -746,20 +504,22 @@ int main(void) { BEEV::STPMgr stp; - beev = &stp; - beev->UserFlags.disableSimplifications(); - beev->UserFlags.division_by_zero_returns_one_flag = true; + mgr = &stp; + mgr->UserFlags.disableSimplifications(); + mgr->UserFlags.division_by_zero_returns_one_flag = true; - Cpp_interface interface(*beev, beev->defaultNodeFactory); + Cpp_interface interface(*mgr, mgr->defaultNodeFactory); interface.startup(); srand(time(NULL)); - BEEV::ParserBM = beev; + BEEV::ParserBM = mgr; // Add had a defect effecting bithWidth > 90. // Shifting had a defect effecting bitWidth > 64. ostream& output = cerr; + const int bits = 5; + if (true) { output << "signed greater than equals" << endl; @@ -821,7 +581,7 @@ main(void) exhaustively_check(i, &bvOrBothWays, &bvorF); } - const int bits = 5; + if (true) { @@ -915,39 +675,40 @@ main(void) } } - // bvSignedComparisons - { - Signature signature; - signature.resultType = BOOL_TYPE; - signature.inputType = VALUE_TYPE; - signature.numberOfInputs = 2; - signature.maxInputWidth = bits; - signature.kind = BVSLT; - exhaustive(&bvSignedLessThanBothWays, signature); - signature.kind = BVSLE; - exhaustive(&bvSignedLessThanEqualsBothWays, signature); - signature.kind = BVSGT; - exhaustive(&bvSignedGreaterThanBothWays, signature); - signature.kind = BVSGE; - exhaustive(&bvSignedGreaterThanEqualsBothWays, signature); - } + // bvSignedComparisons + { + Signature signature; + signature.resultType = BOOL_TYPE; + signature.inputType = VALUE_TYPE; + signature.numberOfInputs = 2; + signature.maxInputWidth = bits; + signature.kind = BVSLT; + exhaustive(&bvSignedLessThanBothWays, signature); + signature.kind = BVSLE; + exhaustive(&bvSignedLessThanEqualsBothWays, signature); + signature.kind = BVSGT; + exhaustive(&bvSignedGreaterThanBothWays, signature); + signature.kind = BVSGE; + exhaustive(&bvSignedGreaterThanEqualsBothWays, signature); + } + + // bvUnSignedComparisons + { + Signature signature; + signature.resultType = BOOL_TYPE; + signature.inputType = VALUE_TYPE; + signature.numberOfInputs = 2; + signature.maxInputWidth = bits; + signature.kind = BVGT; + exhaustive(&bvGreaterThanBothWays, signature); + signature.kind = BVLT; + exhaustive(&bvLessThanBothWays, signature); + signature.kind = BVLE; + exhaustive(&bvLessThanEqualsBothWays, signature); + signature.kind = BVGE; + exhaustive(&bvGreaterThanEqualsBothWays, signature); + } - // bvUnSignedComparisons - { - Signature signature; - signature.resultType = BOOL_TYPE; - signature.inputType = VALUE_TYPE; - signature.numberOfInputs = 2; - signature.maxInputWidth = bits; - signature.kind = BVGT; - exhaustive(&bvGreaterThanBothWays, signature); - signature.kind = BVLT; - exhaustive(&bvLessThanBothWays, signature); - signature.kind = BVLE; - exhaustive(&bvLessThanEqualsBothWays, signature); - signature.kind = BVGE; - exhaustive(&bvGreaterThanEqualsBothWays, signature); - } // BVEQ. { -- 2.47.3