From 06d3ab9ceeafcc20fb158fb9c726fabf4c7df8f8 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Wed, 7 Jul 2010 07:33:58 +0000 Subject: [PATCH] Neaten up the code for constant bit propagation. Note this code doesn't run by default, so this patch shouldn't change anything. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@932 e59a4935-1847-0410-ae03-e826735625c1 --- scripts/Makefile.in | 3 +- src/STPManager/Makefile | 2 +- src/STPManager/STP.cpp | 17 +- src/simplifier/SubstitutionMap.cpp | 15 +- src/simplifier/SubstitutionMap.h | 2 +- .../constantBitP/ConstantBitP_Utility.h | 1 - .../constantBitP/ConstantBitPropagation.cpp | 785 ++++-------------- .../constantBitP/ConstantBitPropagation.h | 82 +- .../constantBitP/MultiplicationStats.h | 173 ++++ .../constantBitP/NodeToFixedBitsMap.h | 3 +- src/simplifier/constantBitP/WorkList.h | 35 +- src/to-sat/AIG/ToSATAIG.cpp | 96 +++ src/to-sat/AIG/ToSATAIG.h | 74 +- src/to-sat/BitBlaster.cpp | 65 +- src/to-sat/Makefile | 4 +- 15 files changed, 572 insertions(+), 785 deletions(-) create mode 100644 src/simplifier/constantBitP/MultiplicationStats.h create mode 100644 src/to-sat/AIG/ToSATAIG.cpp diff --git a/scripts/Makefile.in b/scripts/Makefile.in index 8dea8ff..e5f4783 100644 --- a/scripts/Makefile.in +++ b/scripts/Makefile.in @@ -42,7 +42,8 @@ endif $(SRC)/to-sat/*.o \ $(SRC)/sat/*.o \ $(SRC)/simplifier/*.o \ - $(SRC)/simplifier/constantBitP/*.o \ + $(SRC)/simplifier/constantBitP/*.o \ + $(SRC)/simplifier/AIG/*.o \ $(SRC)/extlib-constbv/*.o \ $(SRC)/extlib-abc/*/*/*.o \ $(SRC)/c_interface/*.o \ diff --git a/src/STPManager/Makefile b/src/STPManager/Makefile index 06abd42..2b5db76 100644 --- a/src/STPManager/Makefile +++ b/src/STPManager/Makefile @@ -16,4 +16,4 @@ clean: depend: $(SRCS) @$(CXX) -MM $(CXXFLAGS) $(SRCS) > $@ -#-include depend +-include depend diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp index e4e942b..c3de82f 100644 --- a/src/STPManager/STP.cpp +++ b/src/STPManager/STP.cpp @@ -133,11 +133,14 @@ namespace BEEV { simplified_solved_InputToSAT); bm->GetRunTimes()->start(RunTimes::ConstantBitPropagation); - simplifier::constantBitP::ConstantBitPropagation cb(simp, bm->defaultNodeFactory - ); - simplified_solved_InputToSAT = cb.topLevelBothWays( - simplified_solved_InputToSAT); + simplifier::constantBitP::ConstantBitPropagation cb(simp, bm->defaultNodeFactory,simplified_solved_InputToSAT); + simplified_solved_InputToSAT = cb.topLevelBothWays(simplified_solved_InputToSAT); + bm->GetRunTimes()->stop(RunTimes::ConstantBitPropagation); + + if (cb.isUnsatisfiable()) + simplified_solved_InputToSAT = bm->ASTFalse; + } #endif @@ -263,10 +266,12 @@ namespace BEEV { bm->GetRunTimes()->start(RunTimes::ConstantBitPropagation); - cb = new simplifier::constantBitP::ConstantBitPropagation(simp, bm->defaultNodeFactory); - cb->getFixedMap(simplified_solved_InputToSAT); + cb = new simplifier::constantBitP::ConstantBitPropagation(simp, bm->defaultNodeFactory,simplified_solved_InputToSAT); bm->GetRunTimes()->stop(RunTimes::ConstantBitPropagation); + + if (cb->isUnsatisfiable()) + simplified_solved_InputToSAT = bm->ASTFalse; } #endif diff --git a/src/simplifier/SubstitutionMap.cpp b/src/simplifier/SubstitutionMap.cpp index e6a6355..7cda322 100644 --- a/src/simplifier/SubstitutionMap.cpp +++ b/src/simplifier/SubstitutionMap.cpp @@ -193,7 +193,7 @@ ASTNode SubstitutionMap::CreateSubstitutionMap(const ASTNode& a, ArrayTransform ASTNode SubstitutionMap::applySubstitutionMap(const ASTNode& n) { ASTNodeMap cache; - return replace(n,*SolverMap,cache); + return replace(n,*SolverMap,cache,bm->defaultNodeFactory); } // NOTE the fromTo map is changed as we traverse downwards. @@ -203,9 +203,8 @@ ASTNode SubstitutionMap::applySubstitutionMap(const ASTNode& n) // will return 5, rather than y. ASTNode SubstitutionMap::replace(const ASTNode& n, ASTNodeMap& fromTo, - ASTNodeMap& cache) + ASTNodeMap& cache, NodeFactory * nf) { - STPMgr *bm = n.GetSTPMgr(); ASTNodeMap::const_iterator it; if ((it = cache.find(n)) != cache.end()) @@ -218,13 +217,13 @@ ASTNode SubstitutionMap::replace(const ASTNode& n, ASTNodeMap& fromTo, const ASTNode& r = it->second; r.SetIndexWidth(n.GetIndexWidth()); assert(BVTypeCheck(r)); - ASTNode replaced = replace(r, fromTo, cache); + ASTNode replaced = replace(r, fromTo, cache,nf); if (replaced != r) fromTo[n] = replaced; return replaced; } - ASTNode replaced = replace(it->second, fromTo, cache); + ASTNode replaced = replace(it->second, fromTo, cache,nf); if (replaced != it->second) fromTo[n] = replaced; @@ -239,7 +238,7 @@ ASTNode SubstitutionMap::replace(const ASTNode& n, ASTNodeMap& fromTo, children.reserve(n.GetChildren().size()); for (unsigned i = 0; i < n.GetChildren().size(); i++) { - children.push_back(replace(n[i], fromTo, cache)); + children.push_back(replace(n[i], fromTo, cache,nf)); } // This code short-cuts if the children are the same. Nodes with the same children, @@ -252,7 +251,7 @@ ASTNode SubstitutionMap::replace(const ASTNode& n, ASTNodeMap& fromTo, assert(children.size() > 0); if (children != n.GetChildren()) // short-cut. { - result = bm->CreateNode(n.GetKind(), children); + result = nf->CreateNode(n.GetKind(), children); } else result = n; @@ -265,7 +264,7 @@ ASTNode SubstitutionMap::replace(const ASTNode& n, ASTNodeMap& fromTo, // If the index and value width aren't saved, they are reset sometimes (??) const unsigned int indexWidth = n.GetIndexWidth(); const unsigned int valueWidth = n.GetValueWidth(); - result = bm->CreateTerm(n.GetKind(), n.GetValueWidth(), + result = nf->CreateTerm(n.GetKind(), n.GetValueWidth(), children); result.SetValueWidth(valueWidth); result.SetIndexWidth(indexWidth); diff --git a/src/simplifier/SubstitutionMap.h b/src/simplifier/SubstitutionMap.h index 08de752..8345374 100644 --- a/src/simplifier/SubstitutionMap.h +++ b/src/simplifier/SubstitutionMap.h @@ -124,7 +124,7 @@ public: // Replace any nodes in "n" that exist in the fromTo map. // NB the fromTo map is changed. - static ASTNode replace(const ASTNode& n, ASTNodeMap& fromTo, ASTNodeMap& cache); + static ASTNode replace(const ASTNode& n, ASTNodeMap& fromTo, ASTNodeMap& cache, NodeFactory *nf); }; } diff --git a/src/simplifier/constantBitP/ConstantBitP_Utility.h b/src/simplifier/constantBitP/ConstantBitP_Utility.h index e58938d..0e253b1 100644 --- a/src/simplifier/constantBitP/ConstantBitP_Utility.h +++ b/src/simplifier/constantBitP/ConstantBitP_Utility.h @@ -14,7 +14,6 @@ using std::cerr; using std::cout; using std::endl; using std::pair; -using std::list; Result makeEqual(FixedBits& a, FixedBits& b, int from, int to); void setSignedMinMax(FixedBits& v, BEEV::CBV min, BEEV::CBV max); diff --git a/src/simplifier/constantBitP/ConstantBitPropagation.cpp b/src/simplifier/constantBitP/ConstantBitPropagation.cpp index 377fd1d..0eeacc6 100644 --- a/src/simplifier/constantBitP/ConstantBitPropagation.cpp +++ b/src/simplifier/constantBitP/ConstantBitPropagation.cpp @@ -1,20 +1,13 @@ #include "../../AST/AST.h" -#include "FixedBits.h" #include "../../extlib-constbv/constantbv.h" #include "../../printer/printers.h" -#include #include "ConstantBitPropagation.h" -#include "NodeToFixedBitsMap.h" -#include "Dependencies.h" #include "../../AST/NodeFactory/NodeFactory.h" -#include -#include "WorkList.h" #include "../../simplifier/simplifier.h" #include "ConstantBitP_Utility.h" +#include "MultiplicationStats.h" #ifdef WITHCBITP - #include "MultiplicationStats.h" - #include "ConstantBitP_TransferFunctions.h" #include "ConstantBitP_MaxPrecision.h" #endif @@ -27,48 +20,27 @@ using namespace BEEV; /* * Propagates known fixed 0 or 1 bits, as well as TRUE/FALSE values through the formula. * - * After propagation. All the values that are completely known are conjoined at the top. - * * Our approach differs from others because the transfer functions are (mostly) optimally precise. * - * FixedBits stores vectors and booleans both in 1 bit-bitvectors. - */ - -/** TODO - * * Size the containers appropriately at initialisation. - * * Reduce the number of inits() that are done during propagation. - * * + * FixedBits stores booleans in 1 bit-bitvectors. */ namespace simplifier { namespace constantBitP { - - Result status; //Whether changes have occured, and whether a conflict (bad) occurs if true is asserted. - NodeToFixedBitsMap* PrintingHackfixedMap; // Used when debugging. - FixedBits* - getUpdatedFixedBits(const BEEV::ASTNode& n, NodeToFixedBitsMap* fixedMap, - MultiplicationStatsMap * msm = NULL); - FixedBits* - getCurrentFixedBits(const ASTNode& n, NodeToFixedBitsMap* fixedMap); - Result dispatchToTransferFunctions(const Kind k, vector& children, FixedBits& output, const ASTNode n, MultiplicationStatsMap *msm = NULL); + Result dispatchToMaximallyPrecise(const Kind k, vector& children, FixedBits& output, const ASTNode n); - void - propagate(WorkList & workList, const Dependencies & dependents, - NodeToFixedBitsMap* fixedMap, MultiplicationStatsMap *msm); - ASTNode - getGraphAfterFixing(const ASTNode& n); - - const bool debug_cBitProp_messages = false; + const bool debug_cBitProp_messages = true; + const bool output_mult_like = true; //////////////////// @@ -88,36 +60,6 @@ namespace simplifier } - // We add the the worklist any node that immediately depends on a constant. - void - addToWorklist(const ASTNode& n, WorkList& list, ASTNodeSet& visited) - { - if (visited.find(n) != visited.end()) - return; - - visited.insert(n); - - bool alreadyAdded = false; - - for (unsigned i = 0; i < n.GetChildren().size(); i++) - { - if (n[i].isConstant() && !alreadyAdded) - { - alreadyAdded = true; - list.push(n); - } - addToWorklist(n[i], list, visited); - } - } - - // Add to the worklist any node that immediately depends on a constant. - void - ConstantBitPropagation::initialiseWorklist(const ASTNode& top) - { - ASTNodeSet visited; - addToWorklist(top, *workList, visited); - } - // Used when outputting when debugging. // Outputs the fixed bits for a particular node. string @@ -161,6 +103,7 @@ namespace simplifier else FatalError("sadf234s"); + assert(result.isConstant()); return result; } @@ -179,9 +122,8 @@ namespace simplifier const FixedBits& bits = *it->second; // Don't constrain nodes we already know all about. - if (BVCONST == node.GetKind() || TRUE == node.GetKind() || FALSE - == node.GetKind()) - continue; + if (node.isConstant()) + continue; // other nodes will contain the same information (the extract doesn't change the fixings). if (BVEXTRACT == node.GetKind() || BVCONCAT == node.GetKind()) @@ -196,50 +138,35 @@ namespace simplifier return toFrom; } -#ifdef WITHCBITP - // Get the column counts for multiplication. - MultiplicationStatsMap* ConstantBitPropagation::getMultiplicationStats() - { - assert(multiplicationStats != NULL); - return multiplicationStats; - } -#endif - - bool - noNewInfo(const Kind& k) + void + ConstantBitPropagation::setNodeToTrue(const ASTNode& top) { - if (k == BVCONCAT || k == BVEXTRACT) - return true; - - return false; + FixedBits & topFB = *getCurrentFixedBits(top); + topFB.setFixed(0, true); + topFB.setValue(0, true); + workList->push(top); } - // Builds and returns the fixed Map. No writing in of values. - // Note the caller is responsibile for deleting the fixedBitMap. - // It omits values that aren't interesting like constants, extracts and concats. - NodeToFixedBitsMap* - ConstantBitPropagation::getFixedMap(const ASTNode & top) + // Propagates. No writing in of values. Doesn't assume the top is true. + ConstantBitPropagation::ConstantBitPropagation(BEEV::Simplifier* _sm, NodeFactory* _nf,const ASTNode & top) { - assert (NULL == fixedMap); - // assert (NULL == multiplicationStats); - fixedMap = new NodeToFixedBitsMap(1000); // better to use the function that returns the number of nodes.. whatever that is. - - //multiplicationStats= new MultiplicationStatsMap(); + assert (BOOLEAN_TYPE == top.GetType()); + assert (top.GetSTPMgr()->UserFlags.bitConstantProp_flag); - workList = new WorkList(); - initialiseWorklist(top); status = NO_CHANGE; - - FixedBits & topFB = *getCurrentFixedBits(top, fixedMap); - topFB.setFixed(0, true); - topFB.setValue(0, true); - workList->push(top); - + simplifier = _sm; + nf = _nf; + fixedMap = new NodeToFixedBitsMap(1000); // better to use the function that returns the number of nodes.. whatever that is. + workList = new WorkList(top); dependents = new Dependencies(top); // List of the parents of a node. + //msm = new MultiplicationStatsMap(); + - //propagate(*workList, *dependents, fixedMap, multiplicationStats); - propagate(*workList, *dependents, fixedMap, NULL); + // not fixing the topnode. + propagate(); + // is there are good reason to clear out some of them?? +#if 0 // remove constants, and things with nothing fixed. NodeToFixedBitsMap::NodeToFixedBitsMapType::iterator it = fixedMap->map->begin(); @@ -248,7 +175,7 @@ namespace simplifier while (it != it_end) { // No constants, nothing completely unfixed. - if ((it->first).isConstant() || (it->second)->countFixed() == 0 /*|| noNewInfo((it->first).GetKind() )*/) + if ( (it->second)->countFixed() == 0 ) { delete it->second; // making this a reference causes reading from freed memory. @@ -259,89 +186,64 @@ namespace simplifier else it++; } - return fixedMap; +#endif + } // Both way propagation. Initialising the top to "true". + // The hardest thing to understand is the two cases: + // 1) If we get the fixed bits of a node, without assuming the top node is true, + // then we can replace that node by its fixed bits. + // 2) But if we assume the top node is true, then get the bits, we need to conjoin it. + + // NB: This expects that the constructor was called with teh same node. Sorry. ASTNode ConstantBitPropagation::topLevelBothWays(const ASTNode& top) { - if (!top.GetSTPMgr()->UserFlags.bitConstantProp_flag) - return top; - + assert(top.GetSTPMgr()->UserFlags.bitConstantProp_flag); assert (BOOLEAN_TYPE == top.GetType()); - assert (NULL == fixedMap); - //assert (NULL == multiplicationStats); - - //Stopwatch watch; - - fixedMap = new NodeToFixedBitsMap(1000); // better to use the function that returns the number of nodes.. whatever that is. - //multiplicationStats = new MultiplicationStatsMap(); - - workList = new WorkList(); - initialiseWorklist(top); - Dependencies * dependents = new Dependencies(top); // List of the parents of a node. + propagate(); status = NO_CHANGE; - //propagate(*workList, *dependents, fixedMap,multiplicationStats); - propagate(*workList, *dependents, fixedMap, NULL); //Determine what must always be true. ASTNodeMap fromTo = getAllFixed(fixedMap); if (debug_cBitProp_messages) { - cout << "Number removed by bottom UP" << fromTo.size(); + cout << "Number removed by bottom UP:" << fromTo.size() << endl; } - status = NO_CHANGE; - - FixedBits & topFB = *getCurrentFixedBits(top, fixedMap); - topFB.setFixed(0, true); - topFB.setValue(0, true); - workList->push(top); + setNodeToTrue(top); if (debug_cBitProp_messages) { cout << "starting propagation" << endl; printNodeWithFixings(); cout << "Initial Tree:" << endl; - //top.NFASTPrint(0, 10, 10); cerr << top; } - //propagate(*workList, *dependents, fixedMap, multiplicationStats); - propagate(*workList, *dependents, fixedMap, NULL); + propagate(); if (debug_cBitProp_messages) { + cerr << "status:" << status <CreateNode(FALSE); - goto end; - } + return top.GetSTPMgr()->CreateNode(FALSE); + + ASTVec toConjoin; // go through the fixedBits. If a node is entirely fixed. // "and" it onto the top. Creates redundancy. Check that the // node doesn't already depend on "top" directly. - for (it = fixedMap->map->begin(); it != fixedMap->map->end(); it++) // iterates through all the pairs of node->fixedBits. - + for (NodeToFixedBitsMap::NodeToFixedBitsMapType::iterator it = fixedMap->map->begin(); it != fixedMap->map->end(); it++) // iterates through all the pairs of node->fixedBits. { const FixedBits& bits = *it->second; @@ -351,8 +253,7 @@ namespace simplifier const ASTNode& node = (it->first); // Don't constrain nodes we already know all about. - if (BVCONST == node.GetKind() || TRUE == node.GetKind() || FALSE - == node.GetKind()) + if (node.isConstant()) continue; // other nodes will contain the same information (the extract doesn't change the fixings). @@ -368,52 +269,44 @@ namespace simplifier { // If it is already contained in the fromTo map, then it's one of the values - // that have fully been determined (previously). No need to to conjoin it to the top. - + // that have fully been determined (previously). Not conjoined. if (fromTo.find(node) != fromTo.end()) continue; + ASTNode constNode = bitsToNode(node,bits); + if (node.GetType() == BOOLEAN_TYPE) { if (SYMBOL == node.GetKind()) { - constantToReplaceWith - = bits.getValue(0) ? beev.CreateNode(TRUE) - : beev.CreateNode(FALSE); - bool r = simplifier->UpdateSolverMap(node, - constantToReplaceWith); + bool r = simplifier->UpdateSubstitutionMap(node, constNode); assert(r); doAssign = false; - } else if (bits.getValue(0)) { propositionToAssert = node; - constantToReplaceWith = beev.CreateNode(TRUE); + constantToReplaceWith = constNode; } else { propositionToAssert = nf->CreateNode(NOT, node); - constantToReplaceWith = beev.CreateNode(FALSE); + constantToReplaceWith = constNode; } } else if (node.GetType() == BITVECTOR_TYPE) { - ASTNode newV = beev.CreateBVConst(bits.GetBVConst(), - node.GetValueWidth()); assert(((unsigned)bits.getWidth()) == node.GetValueWidth()); if (SYMBOL == node.GetKind()) { - constantToReplaceWith = newV; - bool r = simplifier->UpdateSubstitutionMap(node, - constantToReplaceWith); + bool r = simplifier->UpdateSubstitutionMap(node, constNode); assert(r); doAssign = false; } else { - propositionToAssert = nf->CreateNode(EQ, node, newV); - constantToReplaceWith = newV; + propositionToAssert = nf->CreateNode(EQ, node, constNode); + constantToReplaceWith = constNode; } } else @@ -428,103 +321,23 @@ namespace simplifier assert(propositionToAssert.GetType() == BOOLEAN_TYPE); assert(node.GetValueWidth() == constantToReplaceWith.GetValueWidth()); - nodes.push_back(node); - replaceWith.push_back(constantToReplaceWith); - toAssert.push_back(propositionToAssert); - } - } - - { - // fromTo already contains the replacements we can make with adding any additional assertions. - for (unsigned i = 0; i < nodes.size(); i++) - fromTo.insert(make_pair(nodes[i], replaceWith[i])); - - // Write the constants into the main graph. - ASTNodeMap cache2; - result = SubstitutionMap::replace(top, fromTo, cache2); - } - - /* - * This code attempts to simplify the additional assertions that get added into the problem. - * Unfortunately it breaks some examples. - */ - -#if 0 - assert(top.GetType() == BOOLEAN_TYPE); - - if (debug_cBitProp_messages) - { - PrintingHackfixedMap = fixedMap; - printer::GDL_Print(cout, top, toString); - } - - { - assert(nodes.size() == replaceWith.size()); - assert(nodes.size() == toAssert.size()); - - // load into fromTo2 the replacements that require assertions to be added. - ASTNodeMap fromTo2; - for (int i =0; i < nodes.size();i++) - { - fromTo2.insert(make_pair(nodes[i], replaceWith[i])); + fromTo.insert(make_pair(node, constantToReplaceWith)); + toConjoin.push_back(propositionToAssert); } - - // fromTo contains the replacements we can make with adding any additional assertions. - ASTNodeMap::const_iterator it; - for (it = fromTo.begin(); it != fromTo.end(); it++) - fromTo2.insert(*it); - - // Write the constants into the main graph. - ASTNodeMap cache2; - result = sm->replace(top,fromTo2, cache2); } - { - ASTNodeMap n; - // no extra assertions required. - ASTNodeMap::const_iterator it; - for (it = fromTo.begin(); it != fromTo.end(); it++) - n.insert(*it); - - vector > nodeToConst; - - for (int i =0; i < nodes.size();i++) - { - nodeToConst.push_back(make_pair(nodes[i], replaceWith[i])); - n.insert(nodeToConst.back()); - } - // We want to apply all the replacements except one to every node. - // if "n" must equal five, we don't want to apply the replacement rule n=5 to it. - for (int i =0; i < nodes.size();i++) - { - n.erase(nodes[i]); - ASTNodeMap cache2; - toAssert[i] = sm->replace(toAssert[i], n, cache2); - assert(toAssert[i].GetType() == BOOLEAN_TYPE); - n.insert(nodeToConst[i]); - } - assert(toAssert.size() == nodes.size()); - } -#endif + // Write the constants into the main graph. + ASTNodeMap cache; + ASTNode result = SubstitutionMap::replace(top, fromTo, cache,nf); - // Some of these assertions are unnecessary. - if (0 != toAssert.size()) + if (0 != toConjoin.size()) { - result = nf->CreateNode(AND, result, toAssert); // conjoin the new conditions. - assert(BVTypeCheck(result)); + result = nf->CreateNode(AND, result, toConjoin); // conjoin the new conditions. } - end: - - //multiplicationStats->map.clear(); - //delete multiplicationStats; - - fixedMap->clear(); - delete fixedMap; - fixedMap = NULL; - - delete dependents; + assert(BVTypeCheck(result)); + assert(status != CONFLICT); // conflict should have been seen earlier. return result; } @@ -539,22 +352,8 @@ namespace simplifier } } - // add to the work list any nodes that take the result of the "n" node. - - - void - scheduleUp(const ASTNode& n, WorkList & workList, - const Dependencies & dependents) - { - const set* toAdd = dependents.getDependents(n); - set::iterator it = toAdd->begin(); - while (it != toAdd->end()) - { - workList.push(*it); - it++; - } - } + // add to the work list any nodes that take the result of the "n" node. void ConstantBitPropagation::scheduleUp(const ASTNode& n) { @@ -575,21 +374,19 @@ namespace simplifier } void - ConstantBitPropagation::schedule(const ASTNode& n) + ConstantBitPropagation::scheduleNode(const ASTNode& n) { workList->push(n); } - void - ConstantBitPropagation::checkAtFixedPoint(const ASTNode& n, - ASTNodeSet & visited) + bool + ConstantBitPropagation::checkAtFixedPoint(const ASTNode& n, ASTNodeSet & visited) { if (status == CONFLICT) - return; // can't do anything. - + return true; // can't do anything. if (visited.find(n) != visited.end()) - return; + return true; visited.insert(n); @@ -600,22 +397,16 @@ namespace simplifier // get a copy of the current fixing from the cache. for (unsigned i = 0; i < n.GetChildren().size(); i++) { - childrenFixedBits.push_back(*getCurrentFixedBits(n[i], fixedMap)); + childrenFixedBits.push_back(*getCurrentFixedBits(n[i])); } - FixedBits current = *getCurrentFixedBits(n, fixedMap); + FixedBits current = *getCurrentFixedBits(n); + FixedBits newBits = *getUpdatedFixedBits(n); - //FixedBits newBits = *getUpdatedFixedBits(n, fixedMap,multiplicationStats); - FixedBits newBits = *getUpdatedFixedBits(n, fixedMap, NULL); - - if (!FixedBits::equals(newBits, current)) // has been a change. - { - cerr << "Not fixed point"; - assert(false); - } + assert(FixedBits::equals(newBits, current)); for (int i = 0; i < n.Degree(); i++) { - if (!FixedBits::equals(*getCurrentFixedBits(n[i], fixedMap), + if (!FixedBits::equals(*getUpdatedFixedBits(n[i]), childrenFixedBits[i])) { cerr << "Not fixed point"; @@ -624,30 +415,32 @@ namespace simplifier checkAtFixedPoint(n[i], visited); } + return true; } void - propagate(WorkList & workList, const Dependencies & dependents, - NodeToFixedBitsMap* fixedMap, MultiplicationStatsMap * msm) + ConstantBitPropagation::propagate() { + if (CONFLICT == status) + return; + assert(NULL != fixedMap); - while (!workList.isEmpty()) + while (!workList->isEmpty()) { // get the next node from the worklist. - const ASTNode& n = workList.pop(); + const ASTNode& n = workList->pop(); - if (n.isConstant()) - continue; // no propagation for these. + assert (!n.isConstant()); // shouldn't get into the worklist.. + assert (CONFLICT != status); // should have stopped already. if (debug_cBitProp_messages) { cerr << "working on" << n.GetNodeNum() << endl; } - assert (CONFLICT != status); // get a copy of the current fixing from the cache. - FixedBits current = *getCurrentFixedBits(n, fixedMap); + FixedBits current = *getCurrentFixedBits(n); // get the current for the children. vector childrenFixedBits; @@ -656,11 +449,11 @@ namespace simplifier // get a copy of the current fixing from the cache. for (unsigned i = 0; i < n.GetChildren().size(); i++) { - childrenFixedBits.push_back(*getCurrentFixedBits(n[i], fixedMap)); + childrenFixedBits.push_back(*getCurrentFixedBits(n[i])); } // derive the new ones. - FixedBits newBits = *getUpdatedFixedBits(n, fixedMap, msm); + FixedBits newBits = *getUpdatedFixedBits(n); if (CONFLICT == status) return; @@ -668,65 +461,53 @@ namespace simplifier // Not all transfer function update the status. But if they report NO_CHANGE. There really is no change. if (status != NO_CHANGE) { - assert(FixedBits::updateOK(current,newBits)); - if (!FixedBits::equals(newBits, current)) // has been a change. - { - scheduleUp(n, workList, dependents); // schedule everything that depends on n. + assert(FixedBits::updateOK(current,newBits)); + + scheduleUp(n); // schedule everything that depends on n. if (debug_cBitProp_messages) { - cerr << "Changed " << n.GetNodeNum() << "from:" - << current << "to:" << newBits << endl; + cerr << "Changed " << n.GetNodeNum() << "from:" << current << "to:" << newBits << endl; } } for (unsigned i = 0; i < n.GetChildren().size(); i++) { - assert(FixedBits::updateOK(childrenFixedBits[i], *getCurrentFixedBits(n[i],fixedMap)) ); - - if (!FixedBits::equals(*getCurrentFixedBits(n[i], fixedMap), - childrenFixedBits[i])) + if (!FixedBits::equals(*getCurrentFixedBits(n[i]), childrenFixedBits[i])) { + assert(FixedBits::updateOK(childrenFixedBits[i], *getCurrentFixedBits(n[i])) ); + if (debug_cBitProp_messages) { - cerr << "Changed " << n[i].GetNodeNum() << " from:" - << childrenFixedBits[i] << "to:" - << *getCurrentFixedBits(n[i], fixedMap) << endl; + cerr << "Changed: " << n[i].GetNodeNum() << " from:" << childrenFixedBits[i] << "to:" + << *getCurrentFixedBits(n[i]) << endl; } + assert(!n[i].isConstant()); + // All the immediate parents of this child need to be rescheduled. - scheduleUp(n[i], workList, dependents); + // Shouldn't reschuedule 'n' but it does. + scheduleUp(n[i]); // Scheduling the child updates all the values that feed into it. - workList.push(n[i]); + workList->push(n[i]); } } } } } - void - ConstantBitPropagation::prop() - { - if (CONFLICT == status) - return; - //propagate(*workList,*dependents, fixedMap, multiplicationStats); - propagate(*workList, *dependents, fixedMap, NULL); - } - // get the current value from the map. If no value is in the map. Make a new value. FixedBits* - getCurrentFixedBits(const ASTNode& n, NodeToFixedBitsMap* fixedMap) + ConstantBitPropagation::getCurrentFixedBits(const ASTNode& n) { - if (NULL != fixedMap) + assert (NULL != fixedMap); + + NodeToFixedBitsMap::NodeToFixedBitsMapType::iterator it = fixedMap->map->find(n); + if (it != fixedMap->map->end()) { - NodeToFixedBitsMap::NodeToFixedBitsMapType::iterator it = - fixedMap->map->find(n); - if (it != fixedMap->map->end()) - { - return it->second; - } + return it->second; } int bw; @@ -739,7 +520,7 @@ namespace simplifier bw = n.GetValueWidth(); } - FixedBits* output = new FixedBits(bw, (0 == n.GetValueWidth())); + FixedBits* output = new FixedBits(bw, (BOOLEAN_TYPE == n.GetType())); if (BVCONST == n.GetKind() || BITVECTOR == n.GetKind()) { @@ -763,34 +544,26 @@ namespace simplifier output->setValue(0, false); } - if (NULL != fixedMap) - { - fixedMap->map->insert(pair (n, output)); - } - + fixedMap->map->insert(pair (n, output)); return output; } // For the given node, update which bits are fixed. + FixedBits* - getUpdatedFixedBits(const ASTNode& n, NodeToFixedBitsMap* fixedMap, - MultiplicationStatsMap *msm) + ConstantBitPropagation::getUpdatedFixedBits(const ASTNode& n) { - // If it's upwards only, then any fixedBits that have been calculated prior are still good. - //if (NULL != fixedMap) - //{ - // NodeToFixedBitsMap::iterator it = fixedMap->find(n); - // if (it != fixedMap->end()) - // { - // return it->second; - // } - //} - - FixedBits & output = *getCurrentFixedBits(n, fixedMap); + FixedBits* output = getCurrentFixedBits(n); const Kind k = n.GetKind(); - if (SYMBOL == k || n.isConstant()) - return &output; // No transfer functions for these. + if (n.isConstant()) + { + assert(output->isTotallyFixed()); + return output; + } + + if (SYMBOL == k) + return output; // No transfer functions for these. vector children; const int numberOfChildren = n.GetChildren().size(); @@ -798,40 +571,32 @@ namespace simplifier for (int i = 0; i < numberOfChildren; i++) { - children.push_back(getCurrentFixedBits(n.GetChildren()[i], fixedMap)); + children.push_back(getCurrentFixedBits(n.GetChildren()[i])); } assert(status != CONFLICT); - status = dispatchToTransferFunctions(k, children, output, n, msm); - //result = dispatchToMaximallyPrecise(k, children, output, n); + status = dispatchToTransferFunctions(k, children, *output, n, msm); + //result = dispatchToMaximallyPrecise(k, children, *output, n); - assert(((unsigned)output.getWidth()) == n.GetValueWidth() || output.getWidth() ==1); + assert(((unsigned)output->getWidth()) == n.GetValueWidth() || output->getWidth() ==1); - return &output; + return output; } Result dispatchToTransferFunctions(const Kind k, vector& children, FixedBits& output, const ASTNode n, MultiplicationStatsMap * msm) { + Result result = NO_CHANGE; + + assert(!n.isConstant()); #ifdef WITHCBITP - Result result = NO_CHANGE; Result(*transfer)(vector&, FixedBits&); switch (k) { - case TRUE: - output.setFixed(0, true); - output.setValue(0, true); - return result; - - case FALSE: - output.setFixed(0, true); - output.setValue(0, false); - return result; - case READ: case WRITE: // do nothing. Seems difficult to track properly. @@ -864,19 +629,19 @@ namespace simplifier MAPTFN(BVOR, bvOrBothWays) MAPTFN(AND,bvAndBothWays) MAPTFN(BVAND,bvAndBothWays) + MAPTFN(IFF, bvEqualsBothWays) + MAPTFN(EQ, bvEqualsBothWays) MAPTFN(IMPLIES,bvImpliesBothWays) + MAPTFN(NOT,bvNotBothWays) + MAPTFN(BVNEG, bvNotBothWays) // OTHER MAPTFN(BVZX, bvZeroExtendBothWays) MAPTFN(BVSX, bvSignExtendBothWays) MAPTFN(BVUMINUS,bvUnaryMinusBothWays) MAPTFN(BVEXTRACT,bvExtractBothWays) - MAPTFN(EQ, bvEqualsBothWays) - MAPTFN(IFF, bvEqualsBothWays) MAPTFN(BVPLUS, bvAddBothWays) MAPTFN(BVSUB, bvSubtractBothWays) - MAPTFN(NOT,bvNotBothWays) - MAPTFN(BVNEG, bvNotBothWays) MAPTFN(ITE,bvITEBothWays) MAPTFN(BVCONCAT, bvConcatBothWays) @@ -890,15 +655,12 @@ namespace simplifier break; default: { - // if (k == BVSRSHIFT) - //return dispatchToMaximallyPrecise(k, children, output, n); - notHandled(k); return NO_CHANGE; - //return dispatchToMaximallyPrecise(k, children, output, n); } } #undef MAPTFN + bool mult_like = false; // safe approximation to no overflow multiplication. if (k == BVMULT) @@ -908,85 +670,54 @@ namespace simplifier result = bvMultiplyBothWays(children, output, n.GetSTPMgr()); // if (CONFLICT != result) // msm->map[n] = ms; - cerr << output << "="; - cerr << *children[0] << k; - cerr << *children[1] << std::endl; + mult_like=true; } else if (k == BVDIV) { result = bvUnsignedDivisionBothWays(children, output, n.GetSTPMgr()); - cerr << output << "="; - cerr << *children[0] << k; - cerr << *children[1] << std::endl; + mult_like=true; } else if (k == BVMOD) { result = bvUnsignedModulusBothWays(children, output, n.GetSTPMgr()); - cerr << output << "="; - cerr << *children[0] << k; - cerr << *children[1] << std::endl; + mult_like=true; } else if (k == SBVDIV) { result = bvSignedDivisionBothWays(children, output, n.GetSTPMgr()); - cerr << output << "="; - cerr << *children[0] << k; - cerr << *children[1] << std::endl; + mult_like=true; } else if (k == SBVREM) { result = bvSignedRemainderBothWays(children, output, n.GetSTPMgr()); - cerr << output << "="; - cerr << *children[0] << k; - cerr << *children[1] << std::endl; + mult_like=true; } else if (k == SBVMOD) { result = bvSignedModulusBothWays(children, output, n.GetSTPMgr()); - cerr << output << "="; - cerr << *children[0] << k; - cerr << *children[1] << std::endl; + mult_like=true; } else result = transfer(children, output); - return result; -#else - return NO_CHANGE; -#endif - - } - // compare the new fixed to the old fixed. Is it OK?? - Result - isDifferent(const FixedBits& n, const FixedBits& o) - { - Result result = NO_CHANGE; - assert(n.getWidth() == o.getWidth()); - for (int i = 0; i < n.getWidth(); i++) + if (mult_like && output_mult_like) { - if (n.isFixed(i) && o.isFixed(i)) - { - if (n.getValue(i) != o.getValue(i)) - { - return CONFLICT; - } - } - else if (o.isFixed(i) && !n.isFixed(i)) - { - FatalError(LOCATION "values can't become unfixed.."); - } - else if (n.isFixed(i) && !o.isFixed(i)) - { - result = CHANGED; - } + cerr << output << "="; + cerr << *children[0] << k; + cerr << *children[1] << std::endl; } + +#endif return result; + } -#if 0 + Result dispatchToMaximallyPrecise(const Kind k, vector& children, FixedBits& output, const ASTNode n) { + #if WITHCBITP + Signature signature; signature.kind = k; @@ -1018,219 +749,9 @@ namespace simplifier return CHANGED; } - return NO_CHANGE; + #endif + return NOT_IMPLEMENTED; } -#endif - } - -// Code to conjoin a partially specified node to the top. -#if 0 -else if (bits.countFixed() > 0) - { - // Some are fixed. We only fix the contiguous leading and trailing fixed. - - assert(node.GetType() == BITVECTOR_TYPE); - - // Get the inside indexes of the leading and trailing sections. - unsigned trailing = 0; - while (bits.isFixed(trailing)) - trailing++; - - unsigned leading = bits.getWidth() - 1; - while (bits.isFixed(leading)) - leading--; - - assert(leading >= trailing); // prior case handles totally fixed. - - //The fixed bits might not be at either end as we need them to be. - if (trailing == 0 && (unsigned) bits.getWidth() - 1 == leading) - continue; - - ASTNode trailingConst, leadingConst; - bool trailingB = false; - bool leadingB = false; - if (trailing > 0) - { - trailingConst = beev.CreateBVConst(bits.GetBVConst(trailing - 1, 0), trailing); - ASTNode extract = beev.CreateTerm(BVEXTRACT, trailing, node, beev.CreateBVConst(32,trailing-1),beev.CreateBVConst(32,0)); - assert(beev.BVTypeCheck(extract)); - toAssign = beev.CreateNode(EQ, extract, trailingConst); - trailingB = true; - } - - if (leading < (unsigned) bits.getWidth() - 1) - { - leadingConst = beev.CreateBVConst(bits.GetBVConst(bits.getWidth() - 1, leading + 1), bits.getWidth() - 1 - leading); - ASTNode extract = beev.CreateTerm(BVEXTRACT, bits.getWidth() - leading -1, node, beev.CreateBVConst(32,bits.getWidth() -1),beev.CreateBVConst(32,leading+1)); - assert(beev.BVTypeCheck(extract)); - ASTNode equals = beev.CreateNode(EQ, extract, leadingConst); - leadingB = true; - if(!trailingB) - toAssign = equals; - else - toAssign = beev.CreateNode(AND, equals, toAssign); - } - - assert(trailingB || leadingB); - - if (node.GetKind() == SYMBOL) - { - toAssign = beev.NewVar(leading - trailing + 1); - if (trailingB) - toAssign = beev.CreateTerm(BVCONCAT, leading + 1, toAssign, trailingConst); - if (leadingB) - toAssign = beev.CreateTerm(BVCONCAT, bits.getWidth(), leadingConst, toAssign); - - assert(beev.BVTypeCheck(toAssign)); - bool r = beev.UpdateSolverMap(node, toAssign); - assert(r); - doAssign = false; - } - else - { - toReplace= beev.CreateTerm(BVEXTRACT, leading - trailing + 1, node, beev.CreateBVConst(32, leading), beev.CreateBVConst(32, trailing)); - assert(beev.BVTypeCheck(toAssign)); - if (trailingB) - toReplace = beev.CreateTerm(BVCONCAT, leading + 1, toReplace, trailingConst); - if (leadingB) - toReplace = beev.CreateTerm(BVCONCAT, bits.getWidth(), leadingConst, toReplace); - } - - } -#endif - -#if 0 -// whenever it's fixed replace it by a new constant. -// cycles in the graph would cause an infinite loop. -ASTNode ConstantBitPropagation::topLevelGetGraphAfterFixing(const ASTNode& n) - { - if (BEEV::disable_bitConstantProp_flag) - return n; - - Stopwatch watch; - - assert(NULL == fixedMap); - - fixedMap = new NodeToFixedBitsMap(100); - - //n.SMTLIB_Print(cerr, 0); - status = NO_CHANGE; - - //printer::SMTLIB_Print(cerr, n,0); - - // We start by running from the bottom to the top. - ASTNode result = getGraphAfterFixing(n); - - //if (BOTH_WAYS == direction) - - { - //setTopToTrue(result); - - while (true) // loop until fixed point. - - { - cerr << "|"; - - ASTNode old = result; - result = getGraphAfterFixing(result); - - if (CONFLICT == status) - { - cerr << "Status bad"; - break; - } - - if (result == old) - break; // continue until nothing changes - } - } - - //printer::SMTLIB_Print(cerr, result); - - delete fixedMap; - fixedMap = NULL; - - watch.stop(); - - if (CONFLICT == status) - return n.GetSTPMgr().CreateNode(FALSE); - else - return result; - } - -// Simplifies any parts of the tree that can be fixed to a constant. -ASTNode ConstantBitPropagation::getGraphAfterFixing(const ASTNode& n) - { - assert(NULL != fixedMap); - - if (BVCONST == n.GetKind()) - return n; - - ASTNode result; - - if (getUpdatedFixedBits(n,fixedMap)->isTotallyFixed()) - { - BEEV::CBV cbv = getUpdatedFixedBits(n,fixedMap)->GetBVConst(); - - if (BOOLEAN_TYPE == n.GetType()) - { - if (1 == toInt(cbv)) - result = n.GetSTPMgr().CreateNode(TRUE); - else - result = n.GetSTPMgr().CreateNode(FALSE); - - CONSTANTBV::BitVector_Destroy(cbv); - } - else - { - // runs the deleter on cbv. - result = n.GetSTPMgr().CreateBVConst(cbv, n.GetValueWidth()); - } - } - else - { - ASTVec changed; - const int numberOfChildren = n.GetChildren().size(); - changed.reserve(numberOfChildren); - - for (int i = 0; i < numberOfChildren; i++) - { - ASTNode then = getGraphAfterFixing(n.GetChildren()[i]); - changed.push_back(then); - } - - bool changeFound = false; - for (int i = 0; i < numberOfChildren; i++) - { - if (changed[i] != n.GetChildren()[i]) - { - n.GetSTPMgr().BVTypeCheck(changed[i]); - changeFound = true; - } - } - - if (!changeFound) - result = n; - else - { - if (BOOLEAN_TYPE == n.GetType()) - result = n.GetSTPMgr().CreateNode(n.GetKind(), changed); - else if (BITVECTOR_TYPE == n.GetType()) - result = n.GetSTPMgr().CreateTerm(n.GetKind(), n.GetValueWidth(), changed); - else if (ARRAY_TYPE == n.GetType()) - { - result = n.GetBeevMgr().CreateTerm(n.GetKind(), n.GetValueWidth(), changed); - result.SetIndexWidth(n.GetIndexWidth()); - } - else - FatalError("never get to here:"); - } - } - - return result; - } - -#endif } diff --git a/src/simplifier/constantBitP/ConstantBitPropagation.h b/src/simplifier/constantBitP/ConstantBitPropagation.h index 745e907..2ae6aaf 100644 --- a/src/simplifier/constantBitP/ConstantBitPropagation.h +++ b/src/simplifier/constantBitP/ConstantBitPropagation.h @@ -1,12 +1,10 @@ #ifndef CONSTANTBITPROPAGATION_H_ #define CONSTANTBITPROPAGATION_H_ -#include -#include -#include #include "FixedBits.h" -#include "../../AST/AST.h" +#include "Dependencies.h" #include "NodeToFixedBitsMap.h" +#include "WorkList.h" namespace BEEV { @@ -15,16 +13,11 @@ namespace BEEV class Simplifier; } -class NodeFactory; - -using std::vector; - namespace simplifier { namespace constantBitP { - class FixedBits; enum Direction { UPWARDS_ONLY, BOTH_WAYS @@ -42,46 +35,70 @@ namespace simplifier NO_CHANGE = 1, CHANGED, CONFLICT, NOT_IMPLEMENTED }; - class NodeToFixedBitsMap; class MultiplicationStatsMap; class WorkList; - class Dependencies; using BEEV::ASTNode; using BEEV::Simplifier; class ConstantBitPropagation { + NodeFactory *nf; + + Result status; + WorkList *workList; + Dependencies * dependents; + Simplifier *simplifier; + +#ifdef WITHCBITP + MultiplicationStatsMap* msm; +#endif + void printNodeWithFixings(); - NodeFactory *nf; - public: + FixedBits* + getUpdatedFixedBits(const ASTNode& n); + + FixedBits* + getCurrentFixedBits(const ASTNode& n); + void + scheduleDown(const ASTNode& n); + +public: NodeToFixedBitsMap* fixedMap; -#ifdef WITHCBITP - MultiplicationStatsMap* multiplicationStats; -#endif + bool isUnsatisfiable() + { + return status == CONFLICT; + } - WorkList *workList; - Dependencies * dependents; - Simplifier *simplifier; + // propagates. + ConstantBitPropagation(BEEV::Simplifier* _sm, NodeFactory* _nf, const ASTNode & top); + /* ConstantBitPropagation(BEEV::Simplifier* _sm, NodeFactory* _nf) { + status = NO_CHANGE; + + workList = NULL; + dependents = NULL; + fixedMap = NULL; // ASTNodes mapped to which of their bits are fixed. + msm = NULL; + simplifier = _sm; nf = _nf; - fixedMap = NULL; // ASTNodes mapped to which of their bits are fixed. - //multiplicationStats = NULL; - dependents = NULL; } ; + */ + ~ConstantBitPropagation() { - if (fixedMap != NULL) delete fixedMap; + delete dependents; + delete workList; } ; @@ -89,28 +106,23 @@ namespace simplifier BEEV::ASTNode topLevelBothWays(const BEEV::ASTNode& top); - NodeToFixedBitsMap* - getFixedMap(const ASTNode & top); - MultiplicationStatsMap* - getMultiplicationStats(); - void + + bool checkAtFixedPoint(const ASTNode& n, BEEV::ASTNodeSet & visited); void - scheduleUp(const ASTNode& n); - void - scheduleDown(const ASTNode& n); + propagate(); + void - schedule(const ASTNode& n); + scheduleUp(const ASTNode& n); void - initialiseWorklist(const ASTNode& top); + scheduleNode(const ASTNode& n); void - prop(); + setNodeToTrue(const ASTNode& top); }; - } } diff --git a/src/simplifier/constantBitP/MultiplicationStats.h b/src/simplifier/constantBitP/MultiplicationStats.h new file mode 100644 index 0000000..d82c82c --- /dev/null +++ b/src/simplifier/constantBitP/MultiplicationStats.h @@ -0,0 +1,173 @@ +#ifndef MULTPLICATIONSTATS_H_ +#define MULTPLICATIONSTATS_H_ + +#include "../../AST/AST.h" +#include +#include "FixedBits.h" + +namespace simplifier +{ + namespace constantBitP + { + struct MultiplicationStats + { + private: + + void + clear() + { + delete[] columnH; + delete[] columnL; + delete[] sumL; + delete[] sumH; + + columnH = NULL; + columnL = NULL; + sumL = NULL; + sumH = NULL; + } + + void + copyIn(const MultiplicationStats& f) + { + bitWidth = f.bitWidth; + columnL = new signed[bitWidth]; + columnH = new signed[bitWidth]; + sumL = new signed[bitWidth]; + sumH = new signed[bitWidth]; + + for (unsigned i = 0; i < bitWidth; i++) + { + columnL[i] = f.columnL[i]; + columnH[i] = f.columnH[i]; + sumL[i] = f.sumL[i]; + sumH[i] = f.sumH[i]; + } + x = f.x; + y = f.y; + r = f.r; + } + + public: + + signed *columnH; // maximum number of true partial products. + signed *columnL; // minimum "" "" + signed *sumH; + signed *sumL; + unsigned int bitWidth; + + FixedBits x, y, r; + + MultiplicationStats() : + x(1, false), y(1, false), r(1, false) + { + columnH = NULL; + columnL = NULL; + sumH = NULL; + sumL = NULL; + bitWidth = 0; + } + + ~MultiplicationStats() + { + clear(); + } + + MultiplicationStats(const MultiplicationStats& f) : + x(f.x), y(f.y), r(f.r) + { + copyIn(f); + } + + MultiplicationStats& + operator=(const MultiplicationStats& f) + { + if (&f == this) + return *this; + + clear(); + copyIn(f); + + return *this; + } + + MultiplicationStats(int bitWidth_, signed * columnL_, signed * columnH_, signed * sumL_, signed * sumH_) : + x(1, false), y(1, false), r(1, false) + { + bitWidth = bitWidth_; + columnL = new signed[bitWidth]; + columnH = new signed[bitWidth]; + sumL = new signed[bitWidth]; + sumH = new signed[bitWidth]; + + for (unsigned i = 0; i < bitWidth; i++) + { + columnL[i] = columnL_[i]; + columnH[i] = columnH_[i]; + sumL[i] = sumL_[i]; + sumH[i] = sumH_[i]; + } + } + + void + print() + { + ostream& log = std::cout; + + log << x << " * " << y << "=" << r << endl; + + log << " columnL:"; + for (unsigned i = 0; i < bitWidth; i++) + { + log << columnL[bitWidth - 1 - i] << " "; + } + log << endl; + log << " columnH:"; + for (unsigned i = 0; i < bitWidth; i++) + { + log << columnH[bitWidth - 1 - i] << " "; + } + log << endl; + log << " sumL: "; + + for (unsigned i = 0; i < bitWidth; i++) + { + log << sumL[bitWidth - 1 - i] << " "; + } + log << endl; + log << " sumH: "; + for (unsigned i = 0; i < bitWidth; i++) + { + log << sumH[bitWidth - 1 - i] << " "; + } + log << endl; + } + + }; + + class MultiplicationStatsMap + { + public: + typedef std::map NodeToStats; + NodeToStats map; + + void + print() + { + cout << "Size:" << map.size() << endl; + + simplifier::constantBitP::MultiplicationStatsMap::NodeToStats::iterator it; + + for (it = map.begin(); it != map.end(); it++) + { + cout << it->first; + it->second.print(); + } + } + }; + + }; + +}; + +#endif diff --git a/src/simplifier/constantBitP/NodeToFixedBitsMap.h b/src/simplifier/constantBitP/NodeToFixedBitsMap.h index 0a26492..563955a 100644 --- a/src/simplifier/constantBitP/NodeToFixedBitsMap.h +++ b/src/simplifier/constantBitP/NodeToFixedBitsMap.h @@ -29,6 +29,7 @@ namespace simplifier virtual ~NodeToFixedBitsMap() { + clear(); delete map; } @@ -38,7 +39,7 @@ namespace simplifier NodeToFixedBitsMap::NodeToFixedBitsMapType::iterator itD = map->begin(); for (; itD != map->end(); itD++) delete itD->second; - + map->clear(); } }; } diff --git a/src/simplifier/constantBitP/WorkList.h b/src/simplifier/constantBitP/WorkList.h index ddc4da7..4900ed5 100644 --- a/src/simplifier/constantBitP/WorkList.h +++ b/src/simplifier/constantBitP/WorkList.h @@ -8,7 +8,7 @@ namespace simplifier class WorkList { - /* Rough worklist. Constraint Programming people probably have lovely structures to do this + /* Rough worklist. Constraint Programming people have lovely structures to do this * The set (on my machine), is implemented by red-black trees. Deleting just from one end may unbalance the tree?? */ @@ -19,9 +19,38 @@ namespace simplifier WorkList& operator=(const WorkList&); + // We add to the worklist any node that immediately depends on a constant. + void + addToWorklist(const ASTNode& n, ASTNodeSet& visited) + { + if (n.isConstant()) + return; + + if (visited.find(n) != visited.end()) + return; + + visited.insert(n); + + bool alreadyAdded = false; + + for (unsigned i = 0; i < n.GetChildren().size(); i++) + { + if (!alreadyAdded && n[i].isConstant()) + { + alreadyAdded = true; + push(n); + } + addToWorklist(n[i], visited); + } + } + public: - WorkList() + // Add to the worklist any node that immediately depends on a constant. + + WorkList(const ASTNode& top) { + ASTNodeSet visited; + addToWorklist(top, visited); } void @@ -63,9 +92,7 @@ namespace simplifier } }; - }; - }; #endif /* WORKLIST_H_ */ diff --git a/src/to-sat/AIG/ToSATAIG.cpp b/src/to-sat/AIG/ToSATAIG.cpp new file mode 100644 index 0000000..ad8c8f4 --- /dev/null +++ b/src/to-sat/AIG/ToSATAIG.cpp @@ -0,0 +1,96 @@ +#include "ToSATAIG.h" +#include "../../simplifier/constantBitP/ConstantBitPropagation.h" +#include "../../sat/sat.h" + +namespace BEEV +{ + + // Can not be used with abstraction refinement. + bool + ToSATAIG::CallSAT(MINISAT::Solver& satSolver, const ASTNode& input) + { + if (cb != NULL && cb->isUnsatisfiable()) + return false; + + BBNodeManagerAIG mgr; + BitBlaster bb(&mgr,cb); + + bm->GetRunTimes()->start(RunTimes::BitBlasting); + BBNodeAIG BBFormula = bb.BBForm(input); + bm->GetRunTimes()->stop(RunTimes::BitBlasting); + + assert(satSolver.nVars() ==0); + + Cnf_Dat_t* cnfData = NULL; + + mgr.toCNF(BBFormula, cnfData, nodeToSATVar); + + // Free the memory in the AIGs. + BBFormula = BBNodeAIG(); // null node + mgr.stop(); + + // make the result true, see if a contradiction arises. + /* + if (cb != NULL) + { + cb->setNodeToTrue(input); + cb->propagate(); + if (cb->isUnsatisfiable()) + return false; + } + */ + + bm->GetRunTimes()->start(RunTimes::SendingToSAT); + + for (int i = 0; i < cnfData->nVars; i++) + satSolver.newVar(); + + MINISAT::vec satSolverClause; + for (int i = 0; i < cnfData->nClauses; i++) + { + satSolverClause.clear(); + for (int * pLit = cnfData->pClauses[i], *pStop = cnfData->pClauses[i + + 1]; pLit < pStop; pLit++) + { + Var var = (*pLit) >> 1; + assert(var < satSolver.nVars()); + MINISAT::Lit l(var, (*pLit) & 1); + satSolverClause.push(l); + } + + satSolver.addClause(satSolverClause); + if (!satSolver.okay()) + break; + } + bm->GetRunTimes()->stop(RunTimes::SendingToSAT); + + if (bm->UserFlags.output_CNF_flag) + Cnf_DataWriteIntoFile(cnfData, "output_0.cnf", 0); + + Cnf_ClearMemory(); + Cnf_DataFree(cnfData); + + // cryptominisat treats simplify() as protected. +#ifndef CRYPTOMINISAT2 + bm->GetRunTimes()->start(RunTimes::SATSimplifying); + if (!satSolver.simplify()) + { + bm->GetRunTimes()->stop(RunTimes::SATSimplifying); + return false; + } + bm->GetRunTimes()->stop(RunTimes::SATSimplifying); +#endif + + + + bm->GetRunTimes()->start(RunTimes::Solving); + satSolver.solve(); + bm->GetRunTimes()->stop(RunTimes::Solving); + + if (bm->UserFlags.stats_flag) + bm->PrintStats(satSolver); + + return satSolver.okay(); + } + +} diff --git a/src/to-sat/AIG/ToSATAIG.h b/src/to-sat/AIG/ToSATAIG.h index 209fc97..d2f670e 100644 --- a/src/to-sat/AIG/ToSATAIG.h +++ b/src/to-sat/AIG/ToSATAIG.h @@ -46,7 +46,6 @@ namespace BEEV cb = cb_; } - void ClearAllTables() { @@ -61,79 +60,8 @@ namespace BEEV } // Can not be used with abstraction refinement. - bool - CallSAT(MINISAT::Solver& satSolver, const ASTNode& input) - { - BBNodeManagerAIG mgr; - BitBlaster bb(&mgr,cb); - - bm->GetRunTimes()->start(RunTimes::BitBlasting); - BBNodeAIG BBFormula = bb.BBForm(input); - bm->GetRunTimes()->stop(RunTimes::BitBlasting); - - assert(satSolver.nVars() ==0); - - Cnf_Dat_t* cnfData = NULL; - - - mgr.toCNF(BBFormula, cnfData, nodeToSATVar); - - // Free the memory in the AIGs. - BBFormula = BBNodeAIG(); // null node - mgr.stop(); - - bm->GetRunTimes()->start(RunTimes::SendingToSAT); - - for (int i = 0; i < cnfData->nVars; i++) - satSolver.newVar(); - - MINISAT::vec satSolverClause; - for (int i = 0; i < cnfData->nClauses; i++) - { - satSolverClause.clear(); - for (int * pLit = cnfData->pClauses[i], *pStop = cnfData->pClauses[i - + 1]; pLit < pStop; pLit++) - { - Var var = (*pLit) >> 1; - assert(var < satSolver.nVars()); - MINISAT::Lit l(var, (*pLit) & 1); - satSolverClause.push(l); - } + bool CallSAT(MINISAT::Solver& satSolver, const ASTNode& input); - satSolver.addClause(satSolverClause); - if (!satSolver.okay()) - break; - } - bm->GetRunTimes()->stop(RunTimes::SendingToSAT); - - if (bm->UserFlags.output_CNF_flag) - Cnf_DataWriteIntoFile(cnfData, "output_0.cnf", 0); - - Cnf_ClearMemory(); - Cnf_DataFree(cnfData); - - // cryptominisat treats simplify() as protected. -#ifndef CRYPTOMINISAT2 - bm->GetRunTimes()->start(RunTimes::SATSimplifying); - if (!satSolver.simplify()) - { - bm->GetRunTimes()->stop(RunTimes::SATSimplifying); - return false; - } - bm->GetRunTimes()->stop(RunTimes::SATSimplifying); -#endif - - - - bm->GetRunTimes()->start(RunTimes::Solving); - satSolver.solve(); - bm->GetRunTimes()->stop(RunTimes::Solving); - - if (bm->UserFlags.stats_flag) - bm->PrintStats(satSolver); - - return satSolver.okay(); - } }; } diff --git a/src/to-sat/BitBlaster.cpp b/src/to-sat/BitBlaster.cpp index 814b8a2..e21e158 100644 --- a/src/to-sat/BitBlaster.cpp +++ b/src/to-sat/BitBlaster.cpp @@ -58,12 +58,10 @@ void BitBlaster::commonCheck(const ASTNode& n) { if (cb == NULL) return; - if (debug_bitblaster && cb->fixedMap->map->find(n) != cb->fixedMap->map->end()) { + if (cb->fixedMap->map->find(n) != cb->fixedMap->map->end()) { FixedBits* b = cb->fixedMap->map->find(n)->second; - if (debug_bitblaster) - cerr <<"fixed bits are:"<< *b << endl; + cerr <<"fixed bits are:"<< *b << endl; } - } // If x isn't a constant, and the bit-blasted version is. Print out the @@ -99,10 +97,10 @@ bool BitBlaster::update(const ASTNode&n, const int i, sim { //We have a fixed bit, but the bitblasted values aren't constant true or false. - if (b->getValue(i)) - support.insert(bb); - else - support.insert(nf->CreateNode(NOT,bb)); + //if (b->getValue(i)) + //support.insert(bb); + //else + // support.insert(nf->CreateNode(NOT,bb)); bb = b->getValue(i) ? BBTrue : BBFalse; } @@ -119,19 +117,34 @@ bool BitBlaster::update(const ASTNode&n, const int i, sim template void BitBlaster::updateForm(const ASTNode&n, BBNode& bb, BBNodeSet& support) { - BBNodeVec v; - v.reserve(1); - v.push_back(bb); - bb = v[0]; - updateTerm(n, v, support); + if (cb == NULL || n.isConstant()) + return; + + BBNodeVec v(1,bb); + updateTerm(n, v, support); + bb = v[0]; } template void BitBlaster::updateTerm(const ASTNode&n, BBNodeVec& bb, BBNodeSet& support) { - if (cb == NULL || n.isConstant()) + if (cb == NULL) return; + if (n.isConstant()) + { + simplifier::constantBitP::NodeToFixedBitsMap::NodeToFixedBitsMapType::const_iterator it; + it = cb->fixedMap->map->find(n); + if(it == cb->fixedMap->map->end()) + { + cerr << n; + assert(it != cb->fixedMap->map->end()); + } + assert(it->second->isTotallyFixed()); + return; + } + + bool bbFixed = false; for (int i =0; i < (int)bb.size(); i++) { @@ -164,14 +177,15 @@ void BitBlaster::updateTerm(const ASTNode&n, BBNodeVec& b bool changed = false; for (int i = 0; i < (int)bb.size(); i++) - changed = changed || update(n,i, b, bb[i], support); + if(update(n,i, b, bb[i], support)) + changed = true; // don't break, we want to run update(..) on each bit. if (changed) { //cerr << "NN" << n.GetNodeNum() << endl; //cerr << *fixedBits; - cb->schedule(n); + cb->scheduleNode(n); cb->scheduleUp(n); //cerr << "##!" << endl; - cb->prop(); + cb->propagate(); //cerr << "##!!" << endl; } } @@ -503,10 +517,19 @@ const BBNode BitBlaster::BBForm(const ASTNode& form) { BBNodeSet support; BBNode r= BBForm(form,support); - vector v; - v.insert(v.end(), support.begin(), support.end()); - v.push_back(r); - return nf->CreateNode(AND,v); + //vector v; + //v.insert(v.end(), support.begin(), support.end()); + //v.push_back(r); + assert(support.size() ==0); + + + if (cb != NULL && !cb->isUnsatisfiable()) + { + ASTNodeSet visited; + assert(cb->checkAtFixedPoint(form,visited)); + } + // return nf->CreateNode(AND,v); + return r; } // bit blast a formula (boolean term). Result is one bit wide, diff --git a/src/to-sat/Makefile b/src/to-sat/Makefile index 6724a66..2d7a27b 100644 --- a/src/to-sat/Makefile +++ b/src/to-sat/Makefile @@ -2,7 +2,9 @@ TOP = ../.. include $(TOP)/scripts/Makefile.common SRCS = $(wildcard *.cpp) +SRCS += $(wildcard AIG/*.cpp) OBJS = $(SRCS:.cpp=.o) + CFLAGS += -I$(MTL) -I$(SOLVER_INCLUDE) libtosat.a: $(OBJS) depend @@ -11,7 +13,7 @@ libtosat.a: $(OBJS) depend .PHONY: clean clean: - rm -rf *.o *~ *.a .#* depend + rm -rf *.o *~ *.a .#* depend AIG/*.o depend: $(SRCS) @$(CXX) -MM $(CXXFLAGS) $(SRCS) > $@ -- 2.47.3