From: trevor_hansen Date: Tue, 7 Feb 2012 14:32:09 +0000 (+0000) Subject: Disable signed bvmod propagator, I think it implements old style semantics. Add... X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=9f6e13410191ad308f80887b4580df6040dde2e0;p=francis%2Fstp.git Disable signed bvmod propagator, I think it implements old style semantics. Add a test function to compare propagators against the effect of the maximally precise propagator. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1561 e59a4935-1847-0410-ae03-e826735625c1 --- diff --git a/src/simplifier/constantBitP/ConstantBitP_Division.cpp b/src/simplifier/constantBitP/ConstantBitP_Division.cpp index 6f89f68..d2e9b91 100644 --- a/src/simplifier/constantBitP/ConstantBitP_Division.cpp +++ b/src/simplifier/constantBitP/ConstantBitP_Division.cpp @@ -1041,6 +1041,9 @@ Result bvSignedModulusBothWays(vector& children, FixedBits& output, (bvneg (bvurem (bvneg s) (bvneg t))))))) */ + // I think this implements old style (broken) semantics, so avoiding it. + return NO_CHANGE; + if (children[0] == children[1]) // same pointer. { return NO_CHANGE; diff --git a/src/simplifier/constantBitP/ConstantBitP_MaxPrecision.cpp b/src/simplifier/constantBitP/ConstantBitP_MaxPrecision.cpp index 2950f5a..30535f6 100644 --- a/src/simplifier/constantBitP/ConstantBitP_MaxPrecision.cpp +++ b/src/simplifier/constantBitP/ConstantBitP_MaxPrecision.cpp @@ -495,7 +495,7 @@ bool maxPrecision(vector children, FixedBits& output, Kind kind, STP //beev->ClearAllCaches(); // The first time we AddAsserts() it creates a new ASTVec to store them (on the heap). - beev->Pop(); + //beev->Pop(); beev->UserFlags.bitConstantProp_flag = !disabledProp; beev->UserFlags.print_output_flag = printOutput; diff --git a/src/simplifier/constantBitP/ConstantBitPropagation.cpp b/src/simplifier/constantBitP/ConstantBitPropagation.cpp index b9bfb36..ae22989 100644 --- a/src/simplifier/constantBitP/ConstantBitPropagation.cpp +++ b/src/simplifier/constantBitP/ConstantBitPropagation.cpp @@ -744,13 +744,13 @@ namespace simplifier } // This propagator is very slow. It needs to be reimplemented. - //#if 0 + #if 0 else if (k == SBVMOD) { result = bvSignedModulusBothWays(children, output, n.GetSTPMgr()); mult_like=true; } - //#endif + #endif else diff --git a/src/simplifier/constantBitP/FixedBits.cpp b/src/simplifier/constantBitP/FixedBits.cpp index 6ee9d7b..55a08a2 100644 --- a/src/simplifier/constantBitP/FixedBits.cpp +++ b/src/simplifier/constantBitP/FixedBits.cpp @@ -1,5 +1,6 @@ #include "../../AST/AST.h" #include "FixedBits.h" +#include "MersenneTwister.h" #include "ConstantBitP_Utility.h" @@ -151,8 +152,83 @@ namespace simplifier return result; } -#if 0 - #include "MersenneTwister.h" + + + void + FixedBits::join(const FixedBits& a) + { + assert(a.getWidth() == getWidth()); + assert(a.isBoolean() == isBoolean()); + + for (int i = 0; i < a.getWidth(); i++) + { + if (a.isFixed(i) && isFixed(i) && (a.getValue(i) == getValue(i))) + { + // nothind. + } + else + { + setFixed(i,false); + } + } + } + + void + FixedBits::join(unsigned int a) + { + for (int i = 0; i < getWidth(); i++) + { + if (isFixed(i)) + { + if ( + (((a >> i) & 1) ==1) + && + !getValue(i) + ) + setFixed(i,false); + else if ((((a >> i) & 1) ==0) && getValue(i)) + setFixed(i,false); + } + } + } + + // 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; + } + + + + + + + // Getting a new random number is expensive. Not sure why. FixedBits FixedBits::createRandom(const int length, const int probabilityOfSetting, MTRand& trand) @@ -206,7 +282,6 @@ namespace simplifier } return result; } -#endif // In the world of static analysis this is ALPHA. FixedBits diff --git a/src/simplifier/constantBitP/FixedBits.h b/src/simplifier/constantBitP/FixedBits.h index c22d4d8..da231aa 100644 --- a/src/simplifier/constantBitP/FixedBits.h +++ b/src/simplifier/constantBitP/FixedBits.h @@ -252,29 +252,8 @@ namespace simplifier // Whether the set of values contains this one. bool - unsignedHolds(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; - } + unsignedHolds(unsigned val); + void replaceWithContents(const FixedBits& a) @@ -295,6 +274,7 @@ namespace simplifier } } + void copyIn(const FixedBits& a) { @@ -359,6 +339,13 @@ namespace simplifier static FixedBits meet(const FixedBits& a, const FixedBits& b); + void + join(const FixedBits& a); + + void + join(unsigned int a); + + static FixedBits createRandom(const int length, const int probabilityOfSetting, MTRand& rand); diff --git a/src/util/MersenneTwister.h b/src/simplifier/constantBitP/MersenneTwister.h similarity index 100% rename from src/util/MersenneTwister.h rename to src/simplifier/constantBitP/MersenneTwister.h diff --git a/src/util/Makefile b/src/util/Makefile index 379611c..231e6df 100644 --- a/src/util/Makefile +++ b/src/util/Makefile @@ -1,7 +1,7 @@ TOP = ../../ include $(TOP)scripts/Makefile.common -SRCS = rewrite.cpp time_cbitp.cpp +SRCS = rewrite.cpp time_cbitp.cpp test_cbitp.cpp OBJS = $(SRCS:.cpp=.o) CXXFLAGS += -L../../lib/ @@ -10,9 +10,12 @@ CXXFLAGS += -L../../lib/ time_cbitp: $(OBJS) $(TOP)lib/libstp.a $(CXX) $(CXXFLAGS) $@.o -o $@ -lstp - rewrite: $(OBJS) $(TOP)lib/libstp.a $(CXX) $(CXXFLAGS) $@.o -o $@ -lstp +test_cbitp: $(OBJS) $(TOP)lib/libstp.a + $(CXX) $(CXXFLAGS) $@.o -o $@ -lstp + + clean: - rm -f $(OBJS) rewrite time_cbitp + rm -f $(OBJS) rewrite time_cbitp test_cbitp diff --git a/src/util/test_cbitp.cpp b/src/util/test_cbitp.cpp new file mode 100644 index 0000000..b7dabab --- /dev/null +++ b/src/util/test_cbitp.cpp @@ -0,0 +1,897 @@ +// Runs some of the constant bit propagators and compares their results against the maximally precise transformer. +// Those that aren't maximally precise have the super-set relationship checked. + +// NB: This is testing code that I don't expect anyone else will use, it's hard to follow what it does! + + +#include "../simplifier/constantBitP/ConstantBitPropagation.h" +#include "../simplifier/constantBitP/ConstantBitP_TransferFunctions.h" +#include "../simplifier/constantBitP/ConstantBitP_MaxPrecision.h" +#include "../simplifier/constantBitP/FixedBits.h" +#include "../simplifier/constantBitP/MersenneTwister.h" +#include +#include +#include +#include "../AST/AST.h" +#include "../AST/AST.h" + +#include "../STPManager/STPManager.h" +#include "../to-sat/AIG/ToSATAIG.h" +#include "../sat/MinisatCore.h" +#include "../STPManager/STP.h" +#include "../cpp_interface/cpp_interface.h" + +using simplifier::constantBitP::FixedBits; +using namespace simplifier::constantBitP; + + +namespace simplifier +{ + namespace constantBitP + { + + using namespace BEEV; + + STPMgr * beev; + 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) + { + assert(val >=0 && val <=2); + + switch (val) + { + case 0: + result.setFixed(id, false); + break; + case 1: + result.setFixed(id, true); + result.setValue(id, false); + break; + case 2: + result.setFixed(id, true); + result.setValue(id, true); + break; + } + } + + 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 + checkEqual(vector& initialChildren, FixedBits& initialOutput, Result + (*transfer)(vector&, FixedBits&), Kind kind, bool imprecise) + { + // 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]))); + } + + Result tempResult = transfer(tempChildren, tempOutput); + + // 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])) + { + assert(FixedBits::updateOK(*initialChildren[i],*manualChildren[i])); + 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) + { + assert(changed); + } + + bool first = maxPrecision(autoChildren, autoOutput, kind, beev); + beev->ClearAllTables(); + + 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]; + } + } + +// Exhaustively generate all the bitpatterns for the number of inputs. +// For each input compare the solver's result to the manual Transfer functions result. + void + exhaustive(Result + (*transfer)(vector&, FixedBits&), Signature signature) + { + cout << "trying:" << signature.kind << endl; + + assert(signature.maxInputWidth >0); + if (signature.inputType == BOOL_TYPE) + assert(signature.maxInputWidth =1); + + for (int length = 1; length <= signature.maxInputWidth; length++) + { + int totalLength; + int resultLength; + + vector children; + for (int i = 0; i < signature.numberOfInputs; i++) + { + children.push_back(new FixedBits(length, signature.inputType == BOOL_TYPE)); + } + + if (signature.resultType == BOOL_TYPE) + { + resultLength = 1; + totalLength = (length * signature.numberOfInputs + 1); + } + + else + { + resultLength = length; + totalLength = (length * (signature.numberOfInputs + 1)); + + } + + { + + for (long j = 0; j < pow(3, totalLength); j++) + { + FixedBits output(resultLength, signature.resultType == BOOL_TYPE); + + int current = j; + + for (int k = 0; k < totalLength; k++) + { + if (k < resultLength) + { + setV(output, k, current % 3); + } + else + { + int id = (k - resultLength) / length; + setV(*(children[id]), k - resultLength - (id * length), current % 3); + } + current /= 3; + } + + if (isDivide && children[1]->containsZero()) + { + continue; + } + + checkEqual(children, output, transfer, signature.kind, signature.imprecise); + } + } + + for (unsigned i = 0; i < children.size(); i++) + delete children[i]; + } + } + +// Random. + void + runSomeRandom(Result + (*transfer)(vector&, FixedBits&), const Kind kind, const vector late, FixedBits out) + { + const int PROBABILITY_OF_SETTING = 5; + + cout << "Running Random:" << kind << endl; + assert(late.size() ==2); + MTRand mtrand; + + vector children; + + for (int i = 0; i < 2000; i++) + { + children.clear(); + FixedBits a = FixedBits::createRandom(out.getWidth(), PROBABILITY_OF_SETTING, mtrand); + children.push_back(&a); + FixedBits b = FixedBits::createRandom(out.getWidth(), PROBABILITY_OF_SETTING, mtrand); + children.push_back(&b); + FixedBits output = FixedBits::createRandom(out.getWidth(), PROBABILITY_OF_SETTING, mtrand); + + checkEqual(children, output, transfer, kind, false); + cout << "."; + } + return; + } + +// Exhaustively generate all the bitpatterns for the number of inputs. +// For each input compare the solver's result to the manual Transfer functions result. + void + newExhaustive(Result + (*transfer)(vector&, FixedBits&), const Kind kind, const vector temp, + const FixedBits tempOutput) + { + cout << "trying:" << kind << endl; + + int numberOfInputParams = temp.size(); + assert(numberOfInputParams >0); + + vector lengths; + int totalLength = 0; + vector children; + for (int i = 0; i < numberOfInputParams; i++) + { + children.push_back(new FixedBits(temp[i]->getWidth(), temp[i]->isBoolean())); + totalLength += children[i]->getWidth(); + lengths.push_back(children[i]->getWidth()); + } + + int resultLength = tempOutput.getWidth(); + FixedBits output(resultLength, tempOutput.isBoolean()); + + lengths.push_back(resultLength); + totalLength += resultLength; + + for (long j = 0; j < pow(3, totalLength); j++) + { + int current = j; + + int id = 0; + int usedUp = 0; + + for (int k = 0; k < totalLength; k++) + { + if (k < resultLength) + { + setV(output, k, current % 3); + } + else + { + int working = (k - resultLength - usedUp); + if (working == lengths[id]) + { + usedUp += lengths[id]; + id++; + working = 0; + } + setV(*(children[id]), working, current % 3); + } + current /= 3; + } + + checkEqual(children, output, transfer, kind, false); + } + + for (unsigned i = 0; i < children.size(); i++) + delete children[i]; + + } + + } + +} + +Result +multiply(vector& children, FixedBits& output) +{ + return bvMultiplyBothWays(children, output, simplifier::constantBitP::beev, 0); +} + +Result +unsignedDivide(vector& children, FixedBits& output) +{ + return bvUnsignedDivisionBothWays(children, output, simplifier::constantBitP::beev); +} + +Result +signedDivide(vector& children, FixedBits& output) +{ + return bvSignedDivisionBothWays(children, output, simplifier::constantBitP::beev); +} + +Result +signedRemainder(vector& children, FixedBits& output) +{ + return bvSignedRemainderBothWays(children, output, simplifier::constantBitP::beev); +} + +Result +signedModulus(vector& children, FixedBits& output) +{ + return bvSignedModulusBothWays(children, output, simplifier::constantBitP::beev); +} + +Result +unsignedModulus(vector& children, FixedBits& output) +{ + return bvUnsignedModulusBothWays(children, output, simplifier::constantBitP::beev); +} + +struct D +{ + int a, b, c; + void + print() + { + cerr << a << " " << b << " " << c << endl; + } +}; + +void +exhaustively_check(const int bitwidth) +{ + 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; + list.push_back(d); + } + + FixedBits a(bitwidth, false); + FixedBits b(bitwidth, false); + vector temp; + temp.push_back(&a); + temp.push_back(&b); + FixedBits tempOutput(bitwidth, false); + + vector lengths; + int totalLength = 0; + vector children; + for (int i = 0; i < numberOfInputParams; i++) + { + children.push_back(new FixedBits(temp[i]->getWidth(), temp[i]->isBoolean())); + totalLength += children[i]->getWidth(); + lengths.push_back(children[i]->getWidth()); + } + + int resultLength = tempOutput.getWidth(); + FixedBits output(resultLength, tempOutput.isBoolean()); + + lengths.push_back(resultLength); + totalLength += resultLength; + + const int to_iterate = pow(3, totalLength); + for (long j = 0; j < to_iterate; j++) + { + int current = j; + + if (j% 5000 == 0) + cerr << j << " of " << to_iterate << endl; + + int id = 0; + int usedUp = 0; + + for (int k = 0; k < totalLength; k++) + { + if (k < resultLength) + { + setV(output, k, current % 3); + } + else + { + int working = (k - resultLength - usedUp); + if (working == lengths[id]) + { + usedUp += lengths[id]; + id++; + working = 0; + } + setV(*(children[id]), working, current % 3); + } + 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++) + { + D& d = list[j]; + if (children[0]->unsignedHolds(d.a) && children[1]->unsignedHolds(d.b) && output.unsignedHolds(d.c)) + { + if (first) + { + c_a = FixedBits::fromUnsignedInt(bitwidth, d.a); + c_b = FixedBits::fromUnsignedInt(bitwidth, d.b); + c_o = FixedBits::fromUnsignedInt(bitwidth, d.c); + first = false; + } + else + { + c_a.join(d.a); + c_b.join(d.b); + c_o.join(d.c); + } + } + } + + Result r = transfer(children, output); + if (r == CONFLICT) + { + assert(first); + } + else + { + assert(FixedBits::equals(*children[0],c_a)); + assert(FixedBits::equals(*children[1],c_b)); + assert(FixedBits::equals(output,c_o)); + } + } + +} + +int +main(void) +{ + beev = new BEEV::STPMgr(); + beev->UserFlags.disableSimplifications(); + + Cpp_interface interface(*beev, beev->defaultNodeFactory); + interface.startup(); + srand(time(NULL)); + BEEV::ParserBM = beev; + + #ifdef NDEBUG + cerr << "needs debug please."; + exit(1); + #endif + + + const int bits = 4; + exhaustively_check(bits); + + + if (true) + { + Signature signature; + signature.resultType = VALUE_TYPE; + signature.inputType = VALUE_TYPE; + signature.numberOfInputs = 2; + signature.imprecise = true; + signature.kind = BVMULT; + signature.maxInputWidth = 2; + exhaustive(&multiply, signature); + + signature.maxInputWidth = bits; + signature.imprecise = true; + exhaustive(&multiply, signature); + + signature.imprecise = true; + isDivide = true; + signature.kind = SBVMOD; + exhaustive(&signedModulus, signature); + signature.kind = SBVREM; + exhaustive(&signedRemainder, signature); + signature.kind = BVMOD; + exhaustive(&unsignedModulus, signature); + signature.kind = BVDIV; + exhaustive(&unsignedDivide, signature); + signature.kind = SBVDIV; + exhaustive(&signedDivide, signature); + isDivide = false; + } + + { //TWO INPUT. (value, value)->value + Signature signature; + + signature.resultType = VALUE_TYPE; + signature.inputType = VALUE_TYPE; + 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 + { + Signature signature; + signature.resultType = BOOL_TYPE; + signature.inputType = BOOL_TYPE; + signature.numberOfInputs = 2; + signature.maxInputWidth = 1; + signature.kind = IMPLIES; + exhaustive(&bvImpliesBothWays, signature); + } + + // One input (value -> value) + { + Signature signature; + signature.resultType = VALUE_TYPE; + signature.inputType = VALUE_TYPE; + signature.maxInputWidth = bits; + signature.numberOfInputs = 1; + + // BVUMINUS + signature.kind = BVUMINUS; + exhaustive(&bvUnaryMinusBothWays, signature); + + // BVNOT --- Same function as NOT. + signature.kind = BVNEG; + exhaustive(&bvNotBothWays, signature); + + } + + // bvConcat + { + if (bits >= 2) + for (int i = 1; i < bits; i++) + { + vector children; + FixedBits a(bits - i, false); + FixedBits b(i, false); + + children.push_back(&a); + children.push_back(&b); + FixedBits output(bits, false); + newExhaustive(&bvConcatBothWays, BVCONCAT, children, output); + } + } + + // 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); + } + + // BVEQ. + { + Signature signature; + signature.kind = EQ; + signature.resultType = BOOL_TYPE; + signature.inputType = VALUE_TYPE; + signature.maxInputWidth = bits; + signature.numberOfInputs = 2; + exhaustive(&bvEqualsBothWays, signature); + } + + // 2 Params at most. (Bool,Bool) -> Bool + { + Signature signature; + signature.resultType = BOOL_TYPE; + signature.inputType = BOOL_TYPE; + signature.maxInputWidth = 1; + signature.numberOfInputs = 2; + + // IFF. + signature.kind = IFF; + exhaustive(&bvEqualsBothWays, signature); + + // XOR. + signature.kind = XOR; + exhaustive(&bvXorBothWays, signature); + } + + // n Params at most. (Bool,Bool) -> Bool + { + Signature signature; + signature.resultType = BOOL_TYPE; + signature.inputType = BOOL_TYPE; + signature.maxInputWidth = 1; + + // AND. + signature.kind = AND; + signature.numberOfInputs = 3; + exhaustive(&bvAndBothWays, signature); + signature.numberOfInputs = 2; + exhaustive(&bvAndBothWays, signature); + + // OR. + signature.kind = OR; + signature.numberOfInputs = 3; + exhaustive(&bvOrBothWays, signature); + signature.numberOfInputs = 2; + exhaustive(&bvOrBothWays, signature); + } + + // NOT + { + Signature signature; + signature.kind = NOT; + signature.resultType = BOOL_TYPE; + signature.inputType = BOOL_TYPE; + signature.numberOfInputs = 1; + signature.maxInputWidth = 1; + exhaustive(&bvNotBothWays, signature); + } + + // Term ITE. + { + vector children; + FixedBits a(1, true); + FixedBits b(bits, false); + FixedBits c(bits, false); + + children.push_back(&a); + children.push_back(&b); + children.push_back(&c); + FixedBits output(bits, false); + newExhaustive(&bvITEBothWays, ITE, children, output); + } + + // Propositional ITE. + { + vector children; + FixedBits a(1, true); + FixedBits b(1, true); + FixedBits c(1, true); + + children.push_back(&a); + children.push_back(&b); + children.push_back(&c); + FixedBits output(1, true); + newExhaustive(&bvITEBothWays, ITE, children, output); + } + + { + if (bits >= 2) + { + FixedBits output(bits, false); + for (int i = 1; i < bits; i++) + { + vector children; + FixedBits a(i, false); + children.push_back(&a); + children.push_back(&a); // To type check needs a second argument. Ignored. + + newExhaustive(&bvZeroExtendBothWays, BVZX, children, output); + newExhaustive(&bvSignExtendBothWays, BVSX, children, output); + } + } + } + + // Add had a defect effecting bithWidth > 90. + // Shifting had a defect effecting bitWidth > 64. + { + 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; + + return 1; +} + diff --git a/src/util/time_cbitp.cpp b/src/util/time_cbitp.cpp index 55ed845..e76c98a 100644 --- a/src/util/time_cbitp.cpp +++ b/src/util/time_cbitp.cpp @@ -2,13 +2,16 @@ #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 "MersenneTwister.h" + #include "../AST/ASTKind.h" #include "../STPManager/STPManager.h" #include "../cpp_interface/cpp_interface.h" + using namespace std; using simplifier::constantBitP::FixedBits; using namespace simplifier::constantBitP; @@ -20,58 +23,7 @@ const unsigned bitWidth = 64; BEEV::STPMgr* beev; -// Create a random assignment to fixed bits. -FixedBits createRandom(const int length, const int probabilityOfSetting, MTRand& trand) - { - assert( 0 <= probabilityOfSetting); - assert( 100 >= probabilityOfSetting); - - FixedBits result(length, false); - - // I'm not sure if the random number generator is generating just 32 bit numbers?? - int i = 0; - int randomV = trand.randInt(); - - int pool = 32; - - while (i < length) - { - if (pool < 8) - { - randomV = trand.randInt(); - pool = 32; - } - - int val = (randomV & 127); - randomV >>= 7; - pool = pool - 7; - - if (val >= 100) - continue; - - if (val < probabilityOfSetting) - { - switch (randomV & 1) - { - case 0: - result.setFixed(i, true); - result.setValue(i, false); - break; - case 1: - result.setFixed(i, true); - result.setValue(i, true); - break; - default: - BEEV::FatalError(LOCATION "never."); - - } - randomV >>= 1; - } - i++; - - } - return result; - } + class Stopwatch { @@ -116,10 +68,10 @@ void run(Result(*transfer)(vector&, FixedBits&), const int probabili { vector children; - FixedBits a = createRandom(bitWidth, probabilityOfFixing, rand); - FixedBits b = createRandom(bitWidth, probabilityOfFixing, rand); + FixedBits a = FixedBits::createRandom(bitWidth, probabilityOfFixing, rand); + FixedBits b = FixedBits::createRandom(bitWidth, probabilityOfFixing, rand); - FixedBits output = createRandom(bitWidth, probabilityOfFixing, rand); + FixedBits output = FixedBits::createRandom(bitWidth, probabilityOfFixing, rand); for (unsigned i = 0; i < bitWidth; i++) { @@ -209,9 +161,9 @@ void runSimple(Result(*transfer)(vector&, FixedBits&), const int pro { vector children; - FixedBits a = createRandom(bitWidth, probabilityOfFixing, rand); - FixedBits b = createRandom(bitWidth, probabilityOfFixing, rand); - FixedBits output = createRandom(bitWidth, probabilityOfFixing, rand); + FixedBits a = FixedBits::createRandom(bitWidth, probabilityOfFixing, rand); + FixedBits b = FixedBits::createRandom(bitWidth, probabilityOfFixing, rand); + FixedBits output = FixedBits::createRandom(bitWidth, probabilityOfFixing, rand); int initial = a.countFixed() + b.countFixed() + output.countFixed();