From cef8b193fa6528cfa051be78b3201460addea28a Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Mon, 5 Jul 2010 04:43:52 +0000 Subject: [PATCH] Add the interface code for constant bit propagation. This isn't all of the code, just the code required to interface with the bit blaster. This code isn't called. So this patch doesn't change STP at all. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@923 e59a4935-1847-0410-ae03-e826735625c1 --- src/STPManager/UserDefinedFlags.h | 5 + src/simplifier/Makefile | 4 +- src/simplifier/SubstitutionMap.cpp | 4 +- src/simplifier/SubstitutionMap.h | 2 +- .../constantBitP/ConstantBitP_Utility.cpp | 195 +++ .../constantBitP/ConstantBitP_Utility.h | 42 + .../constantBitP/ConstantBitPropagation.cpp | 1236 +++++++++++++++++ .../constantBitP/ConstantBitPropagation.h | 110 ++ src/simplifier/constantBitP/Dependencies.h | 132 ++ src/simplifier/constantBitP/FixedBits.cpp | 439 ++++++ src/simplifier/constantBitP/FixedBits.h | 317 +++++ .../constantBitP/NodeToFixedBitsMap.h | 49 + src/simplifier/constantBitP/WorkList.h | 71 + src/to-sat/BitBlaster.cpp | 144 +- src/to-sat/BitBlaster.h | 36 +- 15 files changed, 2755 insertions(+), 31 deletions(-) create mode 100644 src/simplifier/constantBitP/ConstantBitP_Utility.cpp create mode 100644 src/simplifier/constantBitP/ConstantBitP_Utility.h create mode 100644 src/simplifier/constantBitP/ConstantBitPropagation.cpp create mode 100644 src/simplifier/constantBitP/ConstantBitPropagation.h create mode 100644 src/simplifier/constantBitP/Dependencies.h create mode 100644 src/simplifier/constantBitP/FixedBits.cpp create mode 100644 src/simplifier/constantBitP/FixedBits.h create mode 100644 src/simplifier/constantBitP/NodeToFixedBitsMap.h create mode 100644 src/simplifier/constantBitP/WorkList.h diff --git a/src/STPManager/UserDefinedFlags.h b/src/STPManager/UserDefinedFlags.h index 85e0e5a..00eb60a 100644 --- a/src/STPManager/UserDefinedFlags.h +++ b/src/STPManager/UserDefinedFlags.h @@ -111,6 +111,8 @@ namespace BEEV // Create a new Tseitin variable for every intermediate value. bool renameAllInCNF_flag; + bool bitConstantProp_flag; + // Available back-end SAT solvers. enum SATSolvers { @@ -216,6 +218,9 @@ namespace BEEV // beware of turning this on if you are using cryptominsat2. renameAllInCNF_flag= false; + // Should constant bit propagation be enabled? + bitConstantProp_flag = true; + } //End of constructor for UserDefinedFlags }; //End of struct UserDefinedFlags diff --git a/src/simplifier/Makefile b/src/simplifier/Makefile index fbd7507..af46f14 100644 --- a/src/simplifier/Makefile +++ b/src/simplifier/Makefile @@ -2,7 +2,9 @@ TOP = ../.. include $(TOP)/scripts/Makefile.common SRCS = $(wildcard *.cpp) +SRCS += $(wildcard constantBitP/*.cpp) OBJS = $(SRCS:.cpp=.o) + CFLAGS += -I$(MTL) -I$(SOLVER_INCLUDE) libsimplifier.a:$(OBJS) depend @@ -11,7 +13,7 @@ libsimplifier.a:$(OBJS) depend .PHONY: clean clean: - rm -rf *.o *~ *.a .#* depend + rm -rf *.o *~ *.a .#* depend constantBitP/*.o depend: $(SRCS) @$(CXX) -MM $(CXXFLAGS) $(SRCS) > $@ diff --git a/src/simplifier/SubstitutionMap.cpp b/src/simplifier/SubstitutionMap.cpp index 50a8020..e6a6355 100644 --- a/src/simplifier/SubstitutionMap.cpp +++ b/src/simplifier/SubstitutionMap.cpp @@ -205,7 +205,9 @@ ASTNode SubstitutionMap::applySubstitutionMap(const ASTNode& n) ASTNode SubstitutionMap::replace(const ASTNode& n, ASTNodeMap& fromTo, ASTNodeMap& cache) { - ASTNodeMap::const_iterator it; + STPMgr *bm = n.GetSTPMgr(); + + ASTNodeMap::const_iterator it; if ((it = cache.find(n)) != cache.end()) return it->second; diff --git a/src/simplifier/SubstitutionMap.h b/src/simplifier/SubstitutionMap.h index dff8db1..08de752 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. - ASTNode replace(const ASTNode& n, ASTNodeMap& fromTo, ASTNodeMap& cache); + static ASTNode replace(const ASTNode& n, ASTNodeMap& fromTo, ASTNodeMap& cache); }; } diff --git a/src/simplifier/constantBitP/ConstantBitP_Utility.cpp b/src/simplifier/constantBitP/ConstantBitP_Utility.cpp new file mode 100644 index 0000000..4a914ab --- /dev/null +++ b/src/simplifier/constantBitP/ConstantBitP_Utility.cpp @@ -0,0 +1,195 @@ +#include "ConstantBitP_Utility.h" +#include "../../extlib-constbv/constantbv.h" + +// Utility functions used by the transfer functions. + +namespace BEEV +{ +typedef unsigned int * CBV; +void FatalError(const char * str); +} + + +namespace simplifier +{ +namespace constantBitP +{ + +using BEEV::CBV; + +// Find ALL the unfixed values in the column and fix it to the specified value. +void fixUnfixedTo(vector& operands, const unsigned position, bool toFix) +{ + for (unsigned i = 0; i < operands.size(); i++) + { + if (!operands[i]->isFixed(position)) + { + operands[i]->setFixed(position, true); + operands[i]->setValue(position, toFix); + } + } +} + +// counts of how many of each in the column. +stats getStats(const vector& operands, const unsigned position) +{ + stats result = { 0, 0, 0 }; + + for (unsigned i = 0, size = operands.size(); i < size; i++) + { + if (operands[i]->isFixed(position)) + { + if (operands[i]->getValue(position)) // fixed to one. + result.fixedToOne++; + else + result.fixedToZero++; // fixed to zero. + } + else + result.unfixed++; + } + + assert(result.fixedToOne + result.fixedToZero + result.unfixed == operands.size()); + return result; +} + +Result makeEqual(FixedBits& a, FixedBits& b, int from, int to) +{ + assert(to >= from); + assert(from >=0); + assert(from <= a.getWidth()); + assert(from <= b.getWidth()); + + Result result = NO_CHANGE; + for (int i = from; i < to; i++) + { + if (a.isFixed(i) && !b.isFixed(i)) + { + b.setFixed(i, true); + b.setValue(i, a.getValue(i)); + result = CHANGED; + } + else if (b.isFixed(i) && !a.isFixed(i)) + { + a.setFixed(i, true); + a.setValue(i, b.getValue(i)); + result = CHANGED; + } + else if (b.isFixed(i) && a.isFixed(i)) + { + if (a.getValue(i) != b.getValue(i)) + return CONFLICT; + } + } + return result; +} + +void setSignedMinMax(FixedBits& v, CBV min, CBV max) +{ + const unsigned int msb = v.getWidth() - 1; + + for (unsigned i = 0; i < (unsigned) v.getWidth(); i++) + { + if (v.isFixed(i)) + { + if (v.getValue(i)) // if it's on. It's on. + + { + CONSTANTBV::BitVector_Bit_On(max, i); + CONSTANTBV::BitVector_Bit_On(min, i); + } + else + { + CONSTANTBV::BitVector_Bit_Off(max, i); + CONSTANTBV::BitVector_Bit_Off(min, i); + } + } + else + { + if (i != msb) + { // not fixed. Make the maximum Maximum. + CONSTANTBV::BitVector_Bit_On(max, i); + CONSTANTBV::BitVector_Bit_Off(min, i); + } + else + { //except for the msb. Where we reduce the min. + CONSTANTBV::BitVector_Bit_On(min, i); + CONSTANTBV::BitVector_Bit_Off(max, i); + } + } + } + assert(CONSTANTBV::BitVector_Compare(min,max) <=0); +} + +void setUnsignedMinMax(const FixedBits& v, CBV min, CBV max) +{ + CONSTANTBV::BitVector_Fill(max); + CONSTANTBV::BitVector_Empty(min); + + for (int i = 0; i < v.getWidth(); i++) + { + if (v.isFixed(i)) + { + if (v.getValue(i)) // if it's on. It's on. + + { + //CONSTANTBV::BitVector_Bit_On(max, i); + CONSTANTBV::BitVector_Bit_On(min, i); + } + else + { + CONSTANTBV::BitVector_Bit_Off(max, i); + //CONSTANTBV::BitVector_Bit_Off(min, i); + } + } + //else // not fixed. Just set the max. + //{ + // CONSTANTBV::BitVector_Bit_On(max, i); + // CONSTANTBV::BitVector_Bit_Off(min, i); + //} + } + assert(CONSTANTBV::BitVector_Lexicompare(min,max) <=0); +} + +// Convert from arbitary precision. +unsigned cbvTOInt(const BEEV::CBV v) +{ + unsigned result = 0; + const unsigned bitSize = sizeof(unsigned) * 8; + + for (unsigned j = 0; j < (bits_(v)); j++) + { + if (CONSTANTBV::BitVector_bit_test(v, j)) + { + if (j > bitSize) + { + BEEV::FatalError( LOCATION "Can't fix a bit so very much way up high."); + } + result += (1 << j); + } + + } + return result; +} + +int unsignedCompare(const BEEV::CBV& lhs, const BEEV::CBV& rhs) +{ + /// NB: Uses the memory layout of the constant bit library to extract the bitwidth. + //assert(*((unsigned *)&lhs-3) == *((unsigned *)&rhs-3)); + return CONSTANTBV::BitVector_Lexicompare(lhs,rhs); +} + +int signedCompare(const BEEV::CBV& lhs, const BEEV::CBV& rhs) +{ + /// NB: Uses the memory layout of the constant bit library to extract the bitwidth. + //assert(*((unsigned *)&lhs-3) == *((unsigned *)&rhs-3)); + return CONSTANTBV::BitVector_Compare(lhs,rhs); +} + + +int toInt(const BEEV::CBV value) +{ + return *((unsigned int*) value); +} + +} +} diff --git a/src/simplifier/constantBitP/ConstantBitP_Utility.h b/src/simplifier/constantBitP/ConstantBitP_Utility.h new file mode 100644 index 0000000..e58938d --- /dev/null +++ b/src/simplifier/constantBitP/ConstantBitP_Utility.h @@ -0,0 +1,42 @@ +#ifndef CONSTANTBITP_UTILITY_H_ +#define CONSTANTBITP_UTILITY_H_ + +#include "ConstantBitPropagation.h" + +// Utility functions for use by the transfer functions. +// This should only be included by files defining transfer functions. + +namespace simplifier +{ +namespace constantBitP +{ +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); +void setUnsignedMinMax(const FixedBits& v, BEEV::CBV min, BEEV::CBV max); +unsigned cbvTOInt(const BEEV::CBV v); +void fixUnfixedTo(vector& operands, const unsigned position, bool toFix); +int toInt(BEEV::CBV value); + +// wraps the comparison function, including a check that the bitWidth is the same. +int unsignedCompare(const BEEV::CBV& lhs, const BEEV::CBV& rhs); +int signedCompare(const BEEV::CBV& lhs, const BEEV::CBV& rhs); + +struct stats +{ + unsigned fixedToZero; + unsigned fixedToOne; + unsigned unfixed; +}; + +stats getStats(const vector& operands, const unsigned position); +} +} + + +#endif diff --git a/src/simplifier/constantBitP/ConstantBitPropagation.cpp b/src/simplifier/constantBitP/ConstantBitPropagation.cpp new file mode 100644 index 0000000..377fd1d --- /dev/null +++ b/src/simplifier/constantBitP/ConstantBitPropagation.cpp @@ -0,0 +1,1236 @@ +#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" + +#ifdef WITHCBITP + #include "MultiplicationStats.h" + + #include "ConstantBitP_TransferFunctions.h" + #include "ConstantBitP_MaxPrecision.h" +#endif + +using std::endl; +using std::cout; + +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. + * * + */ + +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; + + //////////////////// + + void + ConstantBitPropagation::printNodeWithFixings() + { + NodeToFixedBitsMap::NodeToFixedBitsMapType::const_iterator it = + fixedMap->map->begin(); + + cerr << "+Nodes with fixings" << endl; + + for (/**/; it != fixedMap->map->end(); it++) // iterates through all the pairs of node->fixedBits. + { + cerr << (it->first).GetNodeNum() << " " << *(it->second) << endl; + } + cerr << "-Nodes with fixings" << endl; + + } + + // 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 + toString(const ASTNode& n) + { + NodeToFixedBitsMap::NodeToFixedBitsMapType::const_iterator it = + PrintingHackfixedMap->map->find(n); + if (it == PrintingHackfixedMap->map->end()) + return ""; + + std::stringstream s; + s << *it->second; + return s.str(); + } + + // If the bits are totally fixed, then return a new matching ASTNode. + ASTNode + bitsToNode(const ASTNode& node, const FixedBits& bits) + { + ASTNode result; + STPMgr & beev = *node.GetSTPMgr(); + + assert (bits.isTotallyFixed()); + assert (!node.isConstant()); // Peformance. Shouldn't waste time calling it on constants. + + if (node.GetType() == BOOLEAN_TYPE) + { + if (bits.getValue(0)) + { + result = beev.CreateNode(TRUE); + } + else + { + result = beev.CreateNode(FALSE); + } + } + else if (node.GetType() == BITVECTOR_TYPE) + { + result = beev.CreateBVConst(bits.GetBVConst(), node.GetValueWidth()); + } + else + FatalError("sadf234s"); + + return result; + } + + // Put anything that's entirely fixed into a from->to map. + ASTNodeMap + getAllFixed(NodeToFixedBitsMap* fixedMap) + { + NodeToFixedBitsMap::NodeToFixedBitsMapType::iterator it; + + ASTNodeMap toFrom; + + // iterates through all the pairs of node->fixedBits. + for (it = fixedMap->map->begin(); it != fixedMap->map->end(); it++) + { + const ASTNode& node = (it->first); + 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; + + // other nodes will contain the same information (the extract doesn't change the fixings). + if (BVEXTRACT == node.GetKind() || BVCONCAT == node.GetKind()) + continue; + + if (bits.isTotallyFixed()) + { + toFrom.insert(std::make_pair(node, bitsToNode(node, bits))); + } + } + + return toFrom; + } + +#ifdef WITHCBITP + // Get the column counts for multiplication. + MultiplicationStatsMap* ConstantBitPropagation::getMultiplicationStats() + { + assert(multiplicationStats != NULL); + return multiplicationStats; + } +#endif + + bool + noNewInfo(const Kind& k) + { + if (k == BVCONCAT || k == BVEXTRACT) + return true; + + return false; + } + + // 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) + { + 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(); + + workList = new WorkList(); + initialiseWorklist(top); + status = NO_CHANGE; + + FixedBits & topFB = *getCurrentFixedBits(top, fixedMap); + topFB.setFixed(0, true); + topFB.setValue(0, true); + workList->push(top); + + dependents = new Dependencies(top); // List of the parents of a node. + + //propagate(*workList, *dependents, fixedMap, multiplicationStats); + propagate(*workList, *dependents, fixedMap, NULL); + + // remove constants, and things with nothing fixed. + NodeToFixedBitsMap::NodeToFixedBitsMapType::iterator it = + fixedMap->map->begin(); + NodeToFixedBitsMap::NodeToFixedBitsMapType::iterator it_end = + fixedMap->map->end(); + while (it != it_end) + { + // No constants, nothing completely unfixed. + if ((it->first).isConstant() || (it->second)->countFixed() == 0 /*|| noNewInfo((it->first).GetKind() )*/) + { + delete it->second; + // making this a reference causes reading from freed memory. + const ASTNode n = it->first; + it++; + fixedMap->map->erase(n); + } + else + it++; + } + return fixedMap; + } + + // Both way propagation. Initialising the top to "true". + ASTNode + ConstantBitPropagation::topLevelBothWays(const ASTNode& top) + { + if (!top.GetSTPMgr()->UserFlags.bitConstantProp_flag) + return top; + + 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. + 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(); + } + + status = NO_CHANGE; + + FixedBits & topFB = *getCurrentFixedBits(top, fixedMap); + topFB.setFixed(0, true); + topFB.setValue(0, true); + workList->push(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); + + if (debug_cBitProp_messages) + { + cerr << "ended propagation" << endl; + printNodeWithFixings(); + } + + ASTNode result; + ASTVec toAssert; + NodeToFixedBitsMap::NodeToFixedBitsMapType::iterator it; + STPMgr & beev = *top.GetSTPMgr(); + ASTNodeMap cache; + + ASTVec nodes; + ASTVec replaceWith; + ASTVec assertions; + + // propagate may have stopped with a conflict. + if (CONFLICT == status) + { + result = top.GetSTPMgr()->CreateNode(FALSE); + goto end; + } + + // 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. + + { + const FixedBits& bits = *it->second; + + if (!bits.isTotallyFixed()) + continue; + + const ASTNode& node = (it->first); + + // Don't constrain nodes we already know all about. + if (BVCONST == node.GetKind() || TRUE == node.GetKind() || FALSE + == node.GetKind()) + continue; + + // other nodes will contain the same information (the extract doesn't change the fixings). + if (BVEXTRACT == node.GetKind() || BVCONCAT == node.GetKind()) + continue; + + // toAssign: conjoin it with the top level. + // toReplace: replace all references to it (except the one conjoined to the top) with this. + ASTNode propositionToAssert; + ASTNode constantToReplaceWith; + // skip the assigning and replacing. + bool doAssign = true; + + { + // 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. + + if (fromTo.find(node) != fromTo.end()) + continue; + + 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); + assert(r); + doAssign = false; + + } + else if (bits.getValue(0)) + { + propositionToAssert = node; + constantToReplaceWith = beev.CreateNode(TRUE); + } + else + { + propositionToAssert = nf->CreateNode(NOT, node); + constantToReplaceWith = beev.CreateNode(FALSE); + } + } + 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); + assert(r); + doAssign = false; + } + else + { + propositionToAssert = nf->CreateNode(EQ, node, newV); + constantToReplaceWith = newV; + } + } + else + FatalError("sadf234s"); + } + + if (doAssign && top != propositionToAssert + && !dependents->nodeDependsOn(top, propositionToAssert)) + { + assert(!constantToReplaceWith.IsNull()); + assert(constantToReplaceWith.isConstant()); + 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 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 + + // Some of these assertions are unnecessary. + if (0 != toAssert.size()) + { + result = nf->CreateNode(AND, result, toAssert); // conjoin the new conditions. + assert(BVTypeCheck(result)); + } + + end: + + //multiplicationStats->map.clear(); + //delete multiplicationStats; + + fixedMap->clear(); + delete fixedMap; + fixedMap = NULL; + + delete dependents; + return result; + } + + void + notHandled(const Kind& k) + { + if (READ != k && WRITE != k) + //if (debug_cBitProp_messages) + + { + cout << "!" << k << endl; + } + } + + // 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++; + } + } + + void + ConstantBitPropagation::scheduleUp(const ASTNode& n) + { + const set* toAdd = dependents->getDependents(n); + set::iterator it = toAdd->begin(); + while (it != toAdd->end()) + { + workList->push(*it); + it++; + } + } + + void + ConstantBitPropagation::scheduleDown(const ASTNode& n) + { + for (int i = 0; i < n.Degree(); i++) + workList->push(n[i]); + } + + void + ConstantBitPropagation::schedule(const ASTNode& n) + { + workList->push(n); + } + + void + ConstantBitPropagation::checkAtFixedPoint(const ASTNode& n, + ASTNodeSet & visited) + { + if (status == CONFLICT) + return; // can't do anything. + + + if (visited.find(n) != visited.end()) + return; + + visited.insert(n); + + // get the current for the children. + vector childrenFixedBits; + childrenFixedBits.reserve(n.GetChildren().size()); + + // 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)); + } + FixedBits current = *getCurrentFixedBits(n, fixedMap); + + //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); + } + + for (int i = 0; i < n.Degree(); i++) + { + if (!FixedBits::equals(*getCurrentFixedBits(n[i], fixedMap), + childrenFixedBits[i])) + { + cerr << "Not fixed point"; + assert(false); + } + + checkAtFixedPoint(n[i], visited); + } + } + + void + propagate(WorkList & workList, const Dependencies & dependents, + NodeToFixedBitsMap* fixedMap, MultiplicationStatsMap * msm) + { + assert(NULL != fixedMap); + + while (!workList.isEmpty()) + { + // get the next node from the worklist. + const ASTNode& n = workList.pop(); + + if (n.isConstant()) + continue; // no propagation for these. + + 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); + + // get the current for the children. + vector childrenFixedBits; + childrenFixedBits.reserve(n.GetChildren().size()); + + // 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)); + } + + // derive the new ones. + FixedBits newBits = *getUpdatedFixedBits(n, fixedMap, msm); + + if (CONFLICT == status) + return; + + // 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. + if (debug_cBitProp_messages) + { + 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 (debug_cBitProp_messages) + { + cerr << "Changed " << n[i].GetNodeNum() << " from:" + << childrenFixedBits[i] << "to:" + << *getCurrentFixedBits(n[i], fixedMap) << endl; + } + + // All the immediate parents of this child need to be rescheduled. + scheduleUp(n[i], workList, dependents); + + // Scheduling the child updates all the values that feed into it. + 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) + { + if (NULL != fixedMap) + { + NodeToFixedBitsMap::NodeToFixedBitsMapType::iterator it = + fixedMap->map->find(n); + if (it != fixedMap->map->end()) + { + return it->second; + } + } + + int bw; + if (0 == n.GetValueWidth()) + { + bw = 1; + } + else + { + bw = n.GetValueWidth(); + } + + FixedBits* output = new FixedBits(bw, (0 == n.GetValueWidth())); + + if (BVCONST == n.GetKind() || BITVECTOR == n.GetKind()) + { + // the CBV doesn't leak. it is a copy of the cbv inside the node. + CBV cbv = n.GetBVConst(); + + for (unsigned int j = 0; j < n.GetValueWidth(); j++) + { + output->setFixed(j, true); + output->setValue(j, CONSTANTBV::BitVector_bit_test(cbv, j)); + } + } + else if (TRUE == n.GetKind()) + { + output->setFixed(0, true); + output->setValue(0, true); + } + else if (FALSE == n.GetKind()) + { + output->setFixed(0, true); + output->setValue(0, false); + } + + if (NULL != fixedMap) + { + 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) + { + // 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); + const Kind k = n.GetKind(); + + if (SYMBOL == k || n.isConstant()) + return &output; // No transfer functions for these. + + vector children; + const int numberOfChildren = n.GetChildren().size(); + children.reserve(numberOfChildren); + + for (int i = 0; i < numberOfChildren; i++) + { + children.push_back(getCurrentFixedBits(n.GetChildren()[i], fixedMap)); + } + + assert(status != CONFLICT); + status = dispatchToTransferFunctions(k, children, output, n, msm); + //result = dispatchToMaximallyPrecise(k, children, output, n); + + assert(((unsigned)output.getWidth()) == n.GetValueWidth() || output.getWidth() ==1); + + return &output; + } + + Result + dispatchToTransferFunctions(const Kind k, vector& children, + FixedBits& output, const ASTNode n, MultiplicationStatsMap * msm) + { + +#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. + return NO_CHANGE; + break; + +#define MAPTFN(caseV, FN) case caseV: transfer = FN; break; + + // Shifting + MAPTFN(BVLEFTSHIFT, bvLeftShiftBothWays) + MAPTFN(BVRIGHTSHIFT, bvRightShiftBothWays) + MAPTFN(BVSRSHIFT, bvArithmeticRightShiftBothWays) + + // Unsigned Comparison. + MAPTFN(BVLT,bvLessThanBothWays) + MAPTFN(BVLE,bvLessThanEqualsBothWays) + MAPTFN(BVGT, bvGreaterThanBothWays) + MAPTFN(BVGE, bvGreaterThanEqualsBothWays) + + // Signed Comparison. + MAPTFN(BVSLT, bvSignedLessThanBothWays) + MAPTFN(BVSGT,bvSignedGreaterThanBothWays) + MAPTFN(BVSLE, bvSignedLessThanEqualsBothWays) + MAPTFN(BVSGE, bvSignedGreaterThanEqualsBothWays) + + // Logic. + MAPTFN(XOR,bvXorBothWays) + MAPTFN(BVXOR, bvXorBothWays) + MAPTFN(OR, bvOrBothWays) + MAPTFN(BVOR, bvOrBothWays) + MAPTFN(AND,bvAndBothWays) + MAPTFN(BVAND,bvAndBothWays) + MAPTFN(IMPLIES,bvImpliesBothWays) + + // 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) + + case BVMULT: // handled specially later. + case BVDIV: + case BVMOD: + case SBVDIV: + case SBVREM: + case SBVMOD: + transfer = NULL; + break; + default: + { + // if (k == BVSRSHIFT) + //return dispatchToMaximallyPrecise(k, children, output, n); + + notHandled(k); + return NO_CHANGE; + //return dispatchToMaximallyPrecise(k, children, output, n); + } + } +#undef MAPTFN + + // safe approximation to no overflow multiplication. + if (k == BVMULT) + { + //MultiplicationStats ms; + //result = bvMultiplyBothWays(children, output, n.GetSTPMgr(),&ms); + result = bvMultiplyBothWays(children, output, n.GetSTPMgr()); + // if (CONFLICT != result) + // msm->map[n] = ms; + cerr << output << "="; + cerr << *children[0] << k; + cerr << *children[1] << std::endl; + } + else if (k == BVDIV) + { + result = bvUnsignedDivisionBothWays(children, output, n.GetSTPMgr()); + cerr << output << "="; + cerr << *children[0] << k; + cerr << *children[1] << std::endl; + } + else if (k == BVMOD) + { + result = bvUnsignedModulusBothWays(children, output, n.GetSTPMgr()); + cerr << output << "="; + cerr << *children[0] << k; + cerr << *children[1] << std::endl; + } + else if (k == SBVDIV) + { + result = bvSignedDivisionBothWays(children, output, n.GetSTPMgr()); + cerr << output << "="; + cerr << *children[0] << k; + cerr << *children[1] << std::endl; + } + else if (k == SBVREM) + { + result = bvSignedRemainderBothWays(children, output, n.GetSTPMgr()); + cerr << output << "="; + cerr << *children[0] << k; + cerr << *children[1] << std::endl; + } + else if (k == SBVMOD) + { + result = bvSignedModulusBothWays(children, output, n.GetSTPMgr()); + cerr << output << "="; + cerr << *children[0] << k; + cerr << *children[1] << std::endl; + } + 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 (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; + } + } + return result; + } + +#if 0 + Result dispatchToMaximallyPrecise(const Kind k, vector& children, + FixedBits& output, const ASTNode n) + { + Signature signature; + signature.kind = k; + + vector childrenCopy; + + for (int i = 0; i < (int) children.size(); i++) + childrenCopy.push_back(*(children[i])); + FixedBits outputCopy(output); + + if (k == BVMULT) + { + // We've got some of multiply already implemented. So help it out by getting some done first. + Result r = bvMultiplyBothWays(children, output, n.GetSTPMgr()); + if (CONFLICT == r) + return CONFLICT; + } + + bool bad = maxPrecision(children, output, k, n.GetSTPMgr()); + + if (bad) + return CONFLICT; + + if (!FixedBits::equals(outputCopy, output)) + return CHANGED; + + for (int i = 0; i < (int) children.size(); i++) + { + if (!FixedBits::equals(*(children[i]), childrenCopy[i])) + return CHANGED; + } + + return NO_CHANGE; + } +#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 new file mode 100644 index 0000000..3b246d3 --- /dev/null +++ b/src/simplifier/constantBitP/ConstantBitPropagation.h @@ -0,0 +1,110 @@ +#ifndef CONSTANTBITPROPAGATION_H_ +#define CONSTANTBITPROPAGATION_H_ + +#include +#include +#include +#include "FixedBits.h" +#include "../../AST/AST.h" + +namespace BEEV +{ + class ASTNode; + typedef unsigned int * CBV; + class Simplifier; +} + +class NodeFactory; + +using std::vector; + +namespace simplifier +{ + namespace constantBitP + { + + class FixedBits; + enum Direction + { + UPWARDS_ONLY, BOTH_WAYS + }; + + // This is used for very specific purposes. + enum Type + { + BOOL_TYPE, VALUE_TYPE + }; + + // The only status that's correctly maintained at present is the conflict status. + enum Result + { + NO_CHANGE = 1, CHANGED, CONFLICT, NOT_IMPLEMENTED + }; + + class NodeToFixedBitsMap; + class MultiplicationStatsMap; + class WorkList; + class Dependencies; + + using BEEV::ASTNode; + using BEEV::Simplifier; + + class ConstantBitPropagation + { + void + printNodeWithFixings(); + NodeFactory *nf; + + public: + + NodeToFixedBitsMap* fixedMap; + //MultiplicationStatsMap* multiplicationStats; + WorkList *workList; + Dependencies * dependents; + Simplifier *simplifier; + + ConstantBitPropagation(BEEV::Simplifier* _sm, NodeFactory* _nf) + { + simplifier = _sm; + nf = _nf; + fixedMap = NULL; // ASTNodes mapped to which of their bits are fixed. + //multiplicationStats = NULL; + dependents = NULL; + } + ; + + ~ConstantBitPropagation() + { + } + ; + + // Returns the node after writing in simplifications from constant Bit propagation. + BEEV::ASTNode + topLevelBothWays(const BEEV::ASTNode& top); + + NodeToFixedBitsMap* + getFixedMap(const ASTNode & top); + MultiplicationStatsMap* + getMultiplicationStats(); + + void + checkAtFixedPoint(const ASTNode& n, BEEV::ASTNodeSet & visited); + + void + scheduleUp(const ASTNode& n); + void + scheduleDown(const ASTNode& n); + void + schedule(const ASTNode& n); + + void + initialiseWorklist(const ASTNode& top); + + void + prop(); + }; + + } +} + +#endif /* CONSTANTBITPROPAGATION_H_ */ diff --git a/src/simplifier/constantBitP/Dependencies.h b/src/simplifier/constantBitP/Dependencies.h new file mode 100644 index 0000000..b8c8184 --- /dev/null +++ b/src/simplifier/constantBitP/Dependencies.h @@ -0,0 +1,132 @@ +#ifndef DEPENDENCIES_H_ +#define DEPENDENCIES_H_ + +#include "../../AST/AST.h" +namespace simplifier +{ + namespace constantBitP + { + + using namespace BEEV; + + // From a child, get the parents of that node. + class Dependencies + { + private: + + typedef hash_map*, + BEEV::ASTNode::ASTNodeHasher, BEEV::ASTNode::ASTNodeEqual> + NodeToDependentNodeMap; + NodeToDependentNodeMap dependents; + + const set empty; + + // All the nodes that depend on the value of a particular node. + void + build(const ASTNode & current, const ASTNode & prior) + { + if (current.isConstant()) // don't care about what depends on constants. + return; + + set * vec; + const NodeToDependentNodeMap::iterator it = dependents.find(current); + if (dependents.end() == it) + { + // add it in with a reference to the vector. + vec = new set (); + + dependents.insert(std::pair*>(current, vec)); + } + else + { + vec = it->second; + } + + if (prior != current) // initially called with both the same. + { + if (vec->count(prior) == 0) + vec->insert(prior); + else + return; // already been added in. + } + + for (unsigned int i = 0; i < current.GetChildren().size(); i++) + { + build(current.GetChildren()[i], current); + } + } + + Dependencies(const Dependencies&); // Shouldn't needed to copy or assign. + Dependencies& operator=(const Dependencies&); + + public: + Dependencies(const ASTNode &top) + { + build(top, top); + checkInvariant(); + } + + ~Dependencies() + { + NodeToDependentNodeMap::iterator it = dependents.begin(); + for (/**/; it != dependents.end(); it++) + { + //set* + delete it->second; + } + } + + void + print() const + { + NodeToDependentNodeMap::const_iterator it = dependents.begin(); + for (/**/; it != dependents.end(); it++) + { + cout << (it->first).GetNodeNum(); + + const set* dep = it->second; + + set::iterator it = dep->begin(); + while (it != dep->end()) + { + cout << " " << (*it).GetNodeNum(); + it++; + } + cout << endl; + } + } + + void + checkInvariant() const + { + // only one node with a single dependent. + } + + const set* + getDependents(const ASTNode n) const + { + if (n.isConstant()) + return ∅ + const NodeToDependentNodeMap::const_iterator it = dependents.find(n); + if (it == dependents.end()) + return ∅ + + return it->second; + } + + // The higher node depends on the lower node. + // The value produces by the lower node is read by the higher node. + bool + nodeDependsOn(const ASTNode& higher, const ASTNode& lower) const + { + const set *s = getDependents(lower); + return s->count(higher) > 0; + } + }; + + } + ; +} +; + +#endif /* DEPENDENCIES_H_ */ diff --git a/src/simplifier/constantBitP/FixedBits.cpp b/src/simplifier/constantBitP/FixedBits.cpp new file mode 100644 index 0000000..6304562 --- /dev/null +++ b/src/simplifier/constantBitP/FixedBits.cpp @@ -0,0 +1,439 @@ +#include "../../AST/AST.h" +#include "FixedBits.h" +//#include "../../utility/MersenneTwister.h" +#include "ConstantBitP_Utility.h" + +// To reduce the memory I tried using the constantbv stuff. But because it is not +// inlined it took about twice as long per propagation as does using a boolean array. +// Other options to reduce memory usage are: vector, dynamic_bitset, or bitMagic. + + +namespace simplifier +{ + namespace constantBitP + { + + std::ostream& + operator<<(std::ostream& output, const FixedBits& h) + { + output << "<"; + for (int i = h.getWidth() - 1; i >= 0; i--) + { + if (h.isFixed(i)) + output << h.getValue(i); + else + output << "-"; + } + + output << ">"; + + return output; + } + + void + FixedBits::fixToZero() + { + for (int i = 0; i < getWidth(); i++) + { + setFixed(i, true); + setValue(i, false); + } + } + + BEEV::CBV + FixedBits::GetBVConst() const + { + assert(isTotallyFixed()); + + BEEV::CBV result = CONSTANTBV::BitVector_Create(width, true); + + for (int i = 0; i < width; i++) + { + if (values[i]) + CONSTANTBV::BitVector_Bit_On(result, i); + } + + return result; + } + + //inclusive + BEEV::CBV + FixedBits::GetBVConst(int to, int from) const + { + assert(to>=from); + assert(from >=0); + int resultWidth = to - from + 1; + + BEEV::CBV result = CONSTANTBV::BitVector_Create(resultWidth, true); + + for (int i = from; i <= to; i++) + { + if (getValue(i)) + CONSTANTBV::BitVector_Bit_On(result, i - from); + } + + return result; + } + + void + FixedBits::init(const FixedBits& copy) + { + width = copy.width; + fixed = new bool[width]; + values = new bool[width]; + representsBoolean = copy.representsBoolean; + + memcpy(fixed, copy.fixed, width * sizeof(bool)); + memcpy(values, copy.values, width * sizeof(bool)); + } + + bool + FixedBits::isTotallyFixed() const + { + for (int i = 0; i < width; i++) + { + if (!fixed[i]) + return false; + } + + return true; + } + + FixedBits::FixedBits(int n, bool isbool) + { + assert(n > 0); + + fixed = new bool[n]; + values = new bool[n]; + width = n; + + for (int i = 0; i < width; i++) + { + fixed[i] = false; // I don't know if there's a default value?? + values[i] = false; // stops it printing out junk. + } + + representsBoolean = isbool; + if (isbool) + assert(1 == width); + + uniqueId = staticUniqueId++; + } + + // There is no way to represent bottom. So we assume a and b are already at least + // one step up the lattice. + FixedBits + FixedBits::meet(const FixedBits& a, const FixedBits& b) + { + assert(a.getWidth() == b.getWidth()); + assert(a.isBoolean() == b.isBoolean()); + + FixedBits result(a.getWidth(), a.isBoolean()); + + for (int i = 0; i < a.getWidth(); i++) + { + if (a.isFixed(i) != b.isFixed(i)) + { + result.setFixed(i, false); + } + else if (a.isFixed(i) && b.isFixed(i) && (a.getValue(i) + != b.getValue(i))) + { + result.setFixed(i, false); + } + else if (a.isFixed(i) && b.isFixed(i)) + { // fixed to the same value. + result.setFixed(i, true); + result.setValue(i, a.getValue(i)); + } + } + return result; + } + +#if 0 + // Getting a new random number is expensive. Not sure why. + FixedBits 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: + throw std::runtime_error(LOCATION "never."); + + } + randomV >>= 1; + } + i++; + + } + return result; + } +#endif + + // In the world of static analysis this is ALPHA. + FixedBits + FixedBits::concreteToAbstract(const BEEV::ASTNode& n) + { + //cout << n; + + int bitWidth; + if (BEEV::BITVECTOR_TYPE == n.GetType()) + bitWidth = n.GetValueWidth(); + else + bitWidth = 1; + + FixedBits output(bitWidth, BEEV::BOOLEAN_TYPE == n.GetType()); + + if (BEEV::BITVECTOR_TYPE == n.GetType()) + { + // loop through testing each of the bits. + BEEV::CBV cbv = n.GetBVConst(); + + for (int j = 0; j < bitWidth; j++) + { + output.setFixed(j, true); + output.setValue(j, CONSTANTBV::BitVector_bit_test(cbv, j)); + } + } + else + { + if (n.GetKind() == BEEV::TRUE) + { + output.setFixed(0, true); + output.setValue(0, true); + } + else if (n.GetKind() == BEEV::FALSE) + { + output.setFixed(0, true); + output.setValue(0, false); + } + else + BEEV::FatalError("Unexpected", n); + } + return output; + } + + FixedBits + FixedBits::fromUnsignedInt(int width, unsigned val) + { + FixedBits output(width, false); + + 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) + { + output.setFixed(i, true); + output.setValue(i, (val & (1 << i))); + } + else if (i < (unsigned) width) + { + output.setFixed(i, true); + output.setValue(i, false); + + } + else // The unsigned value is bigger than the bitwidth of this. + { // so it can't be represented. + if (val & (1 << i)) + { + BEEV::FatalError(LOCATION "Cant be represented."); + } + } + } + return output; + } + + int + FixedBits::getUnsignedValue() const + { + assert(isTotallyFixed()); + assert(getWidth() <= 32); + int result = 0; + + for (int i = 0; i < width; i++) + { + if (getValue(i)) + result += (1 << i); + } + return result; + } + + bool + FixedBits::updateOK(const FixedBits& o, const FixedBits &n, const int upTo) + { + assert (n.getWidth() >= upTo); + assert (o.getWidth() >= upTo); + + for (int i = 0; i < upTo; i++) + { + if (n.isFixed(i) && o.isFixed(i)) + { + if (n.getValue(i) != o.getValue(i)) + { + return false; + } + } + else if (o.isFixed(i) && !n.isFixed(i)) + { + return false; + } + } + return true; + } + + // If the oldBits can't become the new bits. While respecting the lattice rules. That's bad. + // For example. A transfer function shouldn't unfix bits. Or chance the fixed bits value. + bool + FixedBits::updateOK(const FixedBits& o, const FixedBits &n) + { + if (n.getWidth() != o.getWidth()) + return false; + + for (int i = 0; i < n.getWidth(); i++) + { + if (n.isFixed(i) && o.isFixed(i)) + { + if (n.getValue(i) != o.getValue(i)) + { + return false; + } + } + else if (o.isFixed(i) && !n.isFixed(i)) + { + return false; + } + } + return true; + } + + // a is "IN" b. + bool + FixedBits::in(const FixedBits& a, const FixedBits& b) + { + assert(a.getWidth() == b.getWidth()); + + for (int i = 0; i < a.getWidth(); i++) + { + if (a.isFixed(i) && b.isFixed(i) && (a.getValue(i) != b.getValue(i))) + { + return false; + } + if (!a.isFixed(i) && b.isFixed(i)) + return false; + } + return true; + } + + // Gets the minimum and maximum unsigned values that are represented by the set "shift". + void + FixedBits::getUnsignedMinMax(unsigned &minShift, unsigned &maxShift) const + { + const FixedBits& shift = *this; + + // Get the unsigned minimum and maximum of the shift. + BEEV::CBV minCBV = CONSTANTBV::BitVector_Create(shift.getWidth(), true); + BEEV::CBV maxCBV = CONSTANTBV::BitVector_Create(shift.getWidth(), true); + + setUnsignedMinMax(shift, minCBV, maxCBV); + + BEEV::CBV maxValue = CONSTANTBV::BitVector_Create(shift.getWidth(), true); + for (unsigned i = 0; i < sizeof(unsigned) * 8; i++) + CONSTANTBV::BitVector_Bit_On(maxValue, i); + + if (unsignedCompare(minCBV, maxValue) > 0) + { + minShift = UINT_MAX; + } + else + { + minShift = cbvTOInt(minCBV); + } + + if (unsignedCompare(maxCBV, maxValue) > 0) + { + maxShift = UINT_MAX; + } + else + { + maxShift = cbvTOInt(maxCBV); + } + + CONSTANTBV::BitVector_Destroy(maxValue); + CONSTANTBV::BitVector_Destroy(minCBV); + CONSTANTBV::BitVector_Destroy(maxCBV); + } + + bool + FixedBits::equals(const FixedBits& a, const FixedBits& b, const int upTo) + { + assert (a.getWidth() >= upTo); + assert (b.getWidth() >= upTo); + + for (int i = 0; i < upTo; i++) + { + if (a.isFixed(i) != b.isFixed(i)) + { + return false; + } + if (a.isFixed(i)) + if (a.getValue(i) != b.getValue(i)) + return false; + } + return true; + } + + bool + FixedBits::equals(const FixedBits& a, const FixedBits& b) + { + if (a.getWidth() != b.getWidth()) + return false; + + for (int i = 0; i < a.getWidth(); i++) + { + if (a.isFixed(i) != b.isFixed(i)) + { + return false; + } + if (a.isFixed(i)) + if (a.getValue(i) != b.getValue(i)) + return false; + } + return true; + } + } +} diff --git a/src/simplifier/constantBitP/FixedBits.h b/src/simplifier/constantBitP/FixedBits.h new file mode 100644 index 0000000..e6cd072 --- /dev/null +++ b/src/simplifier/constantBitP/FixedBits.h @@ -0,0 +1,317 @@ +#ifndef FIXEDBITS_H_ +#define FIXEDBITS_H_ + +#include +#include +#include + +class MTRand; + +namespace BEEV +{ + class ASTNode; + typedef unsigned int * CBV; + extern bool disable_bitConstantProp; +} + +namespace simplifier +{ + namespace constantBitP + { + + // Gives the file and line number as a string. +#define CONSTANTBITP_UTILITY_STR(s) #s +#define CONSTANTBITP_UTILITY_XSTR(s) CONSTANTBITP_UTILITY_STR(s) +#define LOCATION __FILE__ ":" CONSTANTBITP_UTILITY_XSTR(__LINE__) ": " + + static int staticUniqueId = 1; + + // Bits can be fixed, or unfixed. Fixed bits are fixed to either zero or one. + class FixedBits + { + private: + bool* fixed; + bool* values; + int width; + bool representsBoolean; + + void + init(const FixedBits& copy); + int uniqueId; + + public: + FixedBits(int n, bool isBoolean); + + FixedBits(const FixedBits& copy) + { + assert(this != ©); + init(copy); + uniqueId = staticUniqueId++; + } + + bool + isBoolean() const + { + return representsBoolean; + } + + ~FixedBits() + { + delete[] fixed; + delete[] values; + } + + bool + operator<=(const FixedBits& copy) const + { + return uniqueId <= copy.uniqueId; + } + + bool + operator==(const FixedBits& other) const + { + return this == &(other); + } + + FixedBits& + operator=(const FixedBits& copy) + { + if (this == ©) + return *this; + delete[] fixed; + delete[] values; + init(copy); + return *this; + } + + //All values are fixed to false. + void + fixToZero(); + + int + getWidth() const + { + return width; + } + + // the value contained in the fixed thingy. + int + getUnsignedValue() const; + + // True if all bits are fixed (irrespective of what value they are fixed to). + bool + isTotallyFixed() const; + + // set value of bit "n" to the value. + void + setValue(int n, bool value) + { + assert(((char)value) == 0 || (char)value ==1 ); + assert(n >=0 && n =0 && n = 0; i--) + { + if (!isFixed(i) || getValue(i)) + break; + } + return i; + } + + int + numberOfTrailingZeroes() + { + int i = 0; + for (; i < getWidth(); i++) + { + if (!isFixed(i) || getValue(i)) + break; + } + return i; + } + + //Returns the position of the first non-fixed value. + int + leastUnfixed() + { + int i = 0; + for (; i < getWidth(); i++) + { + if (!isFixed(i)) + break; + } + return i; + } + + // is this bit fixed to zero? + bool + isFixedToZero(int n) const + { + return isFixed(n) && !getValue(n); + } + + // is this bit fixed to one? + bool + isFixedToOne(int n) const + { + return isFixed(n) && getValue(n); + } + + // is this bit fixed to either zero or one? + bool + isFixed(int n) const + { + assert(n >=0 && n =0 && n = a.getWidth()); + + for (int i = 0; i < a.getWidth(); i++) + { + if (a.isFixed(i)) + { + setFixed(i, true); + setValue(i, a.getValue(i)); + } + else + { + setFixed(i, false); + } + } + } + + void + copyIn(const FixedBits& a) + { + int to = std::min(getWidth(), a.getWidth()); + for (int i = 0; i < to; i++) + { + assert(!isFixed(i)); + if (a.isFixed(i)) + { + setFixed(i, true); + setValue(i, a.getValue(i)); + } + } + } + + //todo merger with unsignedHolds() + bool + containsZero() const + { + for (int i = 0; i < getWidth(); i++) + if (isFixed(i) && getValue(i)) + return false; + return true; + } + + int + countFixed() const + { + int result = 0; + for (unsigned i = 0; i < (unsigned) width; i++) + if (isFixed(i)) + result++; + return result; + } + + // Result needs to be explicitly deleted. + BEEV::CBV + GetBVConst() const; + + // Result needs to be explicitly deleted. + BEEV::CBV + GetBVConst(int to, int from) const; + + void + getUnsignedMinMax(unsigned &minShift, unsigned &maxShift) const; + + static FixedBits + meet(const FixedBits& a, const FixedBits& b); + + static FixedBits + createRandom(const int length, const int probabilityOfSetting, + MTRand& rand); + + static FixedBits + fromUnsignedInt(int width, unsigned val); + + static FixedBits + concreteToAbstract(const BEEV::ASTNode& n); + + static bool + equals(const FixedBits& a, const FixedBits& b); + + static bool + equals(const FixedBits& a, const FixedBits& b, const int upTo); + + static bool + updateOK(const FixedBits& o, const FixedBits & n); + + static bool + updateOK(const FixedBits& o, const FixedBits &n, const int upTo); + + static bool + in(const FixedBits& a, const FixedBits& b); + + }; + + std::ostream& + operator<<(std::ostream& output, const FixedBits& h); + + } +} +#endif /*FIXED_H_*/ diff --git a/src/simplifier/constantBitP/NodeToFixedBitsMap.h b/src/simplifier/constantBitP/NodeToFixedBitsMap.h new file mode 100644 index 0000000..0a26492 --- /dev/null +++ b/src/simplifier/constantBitP/NodeToFixedBitsMap.h @@ -0,0 +1,49 @@ +/* + * pimpl class to make compiling easier. + */ + +#ifndef NODETOFIXEDBITSMAP_H_ +#define NODETOFIXEDBITSMAP_H_ + +#include "../../AST/AST.h" +#include "FixedBits.h" + +namespace simplifier +{ + namespace constantBitP + { + + class NodeToFixedBitsMap + { + public: + typedef BEEV::hash_map + NodeToFixedBitsMapType; + + NodeToFixedBitsMapType* map; + + NodeToFixedBitsMap(int size) + { + map = new NodeToFixedBitsMapType(size); + } + virtual + ~NodeToFixedBitsMap() + { + delete map; + } + + void + clear() + { + NodeToFixedBitsMap::NodeToFixedBitsMapType::iterator itD = map->begin(); + for (; itD != map->end(); itD++) + delete itD->second; + + } + }; + } + ; +} +; + +#endif /* NODETOFIXEDBITSMAP_H_ */ diff --git a/src/simplifier/constantBitP/WorkList.h b/src/simplifier/constantBitP/WorkList.h new file mode 100644 index 0000000..ddc4da7 --- /dev/null +++ b/src/simplifier/constantBitP/WorkList.h @@ -0,0 +1,71 @@ +#ifndef WORKLIST_H_ +#define WORKLIST_H_ + +namespace simplifier +{ + namespace constantBitP + { + + class WorkList + { + /* Rough worklist. Constraint Programming people probably 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?? + */ + + private: + + set workList; // Nodes to work on. + WorkList(const WorkList&); // Shouldn't needed to copy or assign. + WorkList& + operator=(const WorkList&); + + public: + WorkList() + { + } + + void + push(const BEEV::ASTNode& n) + { + if (n.isConstant()) // don't ever add constants to the worklist. + return; + + //cerr << "WorkList Inserting:" << n.GetNodeNum() << endl; + workList.insert(n); + } + + BEEV::ASTNode + pop() + { + assert(!isEmpty()); + ASTNode ret = *workList.begin(); + workList.erase(workList.begin()); + return ret; + } + + bool + isEmpty() + { + return workList.empty(); + } + + void + print() + { + cerr << "+Worklist" << endl; + set::const_iterator it = workList.begin(); + while (it != workList.end()) + { + cerr << *it << " "; + it++; + } + cerr << "-Worklist" << endl; + + } + }; + + }; + +}; + +#endif /* WORKLIST_H_ */ diff --git a/src/to-sat/BitBlaster.cpp b/src/to-sat/BitBlaster.cpp index a1729bb..8387083 100644 --- a/src/to-sat/BitBlaster.cpp +++ b/src/to-sat/BitBlaster.cpp @@ -12,6 +12,9 @@ #include "BitBlaster.h" #include "AIG/BBNodeManagerAIG.h" #include "BBNodeManagerASTNode.h" +#include "../simplifier/constantBitP/FixedBits.h" +#include "../simplifier/constantBitP/ConstantBitPropagation.h" +#include "../simplifier/constantBitP/NodeToFixedBitsMap.h" namespace BEEV { @@ -29,6 +32,8 @@ namespace BEEV { * the vector corresponds to bit 0 -- the low-order bit. ********************************************************************/ + using simplifier::constantBitP::FixedBits; + #define BBNodeVec vector #define BBNodeVecMap map > #define BBNodeSet set @@ -44,46 +49,131 @@ vector _empty_BBNodeAIGVec; // reaching the bitblaster don't have obvious simplifications // that should have already been applied. const bool debug_do_check = false; +const bool debug_bitblaster = false; + +template +void BitBlaster::commonCheck(const ASTNode& n) { + cerr << "Non constant is constant:"; + cerr << n << endl; + + if (cb == NULL) + return; + if (debug_bitblaster && 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; + } +} +// If x isn't a constant, and the bit-blasted version is. Print out the +// AST nodes and the fixed bits. template -void check(const BBNode& x, const ASTNode& n, BBNodeManagerT* nf) -{ - if (n.isConstant()) - return; +void BitBlaster::check(const BBNode& x, const ASTNode& n) { + if (n.isConstant()) + return; - const BBNode& BBTrue = nf->getTrue(); - const BBNode& BBFalse = nf->getFalse(); + if (x != BBTrue && x != BBFalse) + return; + commonCheck(n); +} - if (x != BBTrue && x != BBFalse) - return; +template +void BitBlaster::check(const vector& x, const ASTNode& n) { + if (n.isConstant()) + return; + for (int i = 0; i < (int) x.size(); i++) { + if (x[i] != BBTrue && x[i] != BBFalse) + return; + } - cerr << "Non constant is constant:" ; - cerr << n << endl; + commonCheck(n); } - template -void check(BBNodeVec& x, const ASTNode& n, BBNodeManagerT* nf) +bool BitBlaster::update(const ASTNode&n, const int i, simplifier::constantBitP::FixedBits* b, BBNode& bb, BBNodeSet& support) { - if (n.isConstant()) - return; - - const BBNode& BBTrue = nf->getTrue(); - const BBNode& BBFalse = nf->getFalse(); - - for (int i =0; i < x.size(); i++) - { - if (x[i] != BBTrue && x[i] != BBFalse) - return; - } + if (b->isFixed(i) && (!(bb == BBTrue || bb == BBFalse))) + { + //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)); + + bb = b->getValue(i) ? BBTrue : BBFalse; + } + else if (!b->isFixed(i) && (bb == BBTrue || bb == BBFalse)) + { + b->setFixed(i,true); + b->setValue(i,bb == BBTrue ? true : false); + return true; // Need to propagate. + } + + return false; +} - cerr << "Non constant is constant:" ; - cerr << n << endl; +template +void BitBlaster::updateForm(const ASTNode&n, BBNode& bb, BBNodeSet& support) +{ + BBNodeVec v; + v.reserve(1); + v.push_back(bb); + bb = v[0]; } +template +void BitBlaster::updateTerm(const ASTNode&n, BBNodeVec& bb, BBNodeSet& support) { + + if (cb == NULL || n.isConstant()) + return; + + bool bbFixed = false; + for (int i =0; i < (int)bb.size(); i++) + { + if (bb[i] == BBTrue || bb[i] == BBFalse) + { + bbFixed = true; + break; + } + } + + FixedBits * b = NULL; + + simplifier::constantBitP::NodeToFixedBitsMap::NodeToFixedBitsMapType::const_iterator it; + if ((it = cb->fixedMap->map->find(n)) == cb->fixedMap->map->end()) + { + if (bbFixed) + { + b = new FixedBits(n.GetType() == BOOLEAN_TYPE? 1:n.GetValueWidth(),n.GetType() == BOOLEAN_TYPE); + cb->fixedMap->map->insert(pair (n, b)); + if (debug_bitblaster) + cerr << "inserting" << n.GetNodeNum() << endl; + } + else + return; // nothing to update. + } + else + b = it->second; + + assert(b != NULL); + + bool changed = false; + for (int i = 0; i < (int)bb.size(); i++) + changed = changed || update(n,i, b, bb[i], support); + if (changed) { + //cerr << "NN" << n.GetNodeNum() << endl; + //cerr << *fixedBits; + cb->schedule(n); + cb->scheduleUp(n); + //cerr << "##!" << endl; + cb->prop(); + //cerr << "##!!" << endl; + } +} template @@ -399,7 +489,7 @@ const BBNodeVec BitBlaster::BBTerm(const ASTNode& term, B assert(result.size() == term.GetValueWidth()); if (debug_do_check) - check(result, term,nf); + check(result, term); return (BBTermMemo[term] = result); } @@ -496,7 +586,7 @@ const BBNode BitBlaster::BBForm(const ASTNode& form, BBNo assert(!result.IsNull()); if (debug_do_check) - check(result, form,nf); + check(result, form); return (BBFormMemo[form] = result); } diff --git a/src/to-sat/BitBlaster.h b/src/to-sat/BitBlaster.h index e3e747d..7e03456 100644 --- a/src/to-sat/BitBlaster.h +++ b/src/to-sat/BitBlaster.h @@ -15,6 +15,15 @@ #include #include "../STPManager/STPManager.h" +namespace simplifier +{ + namespace constantBitP + { + class ConstantBitPropagation; + class FixedBits; + } +} + namespace BEEV { class ASTNode; @@ -24,7 +33,11 @@ template class BitBlaster; template class BitBlaster { -private: + BBNode BBTrue, BBFalse; + + + simplifier::constantBitP::ConstantBitPropagation* cb; + // Memo table for bit blasted terms. If a node has already been // bitblasted, it is mapped to a vector of Boolean formulas for // the @@ -110,6 +123,14 @@ private: BitBlaster& operator = (const BitBlaster& other); BitBlaster(const BitBlaster& other); + // Checks for constants. + void commonCheck(const ASTNode& n); + void check(const BBNode& x, const ASTNode& n); + void check(const vector& x, const ASTNode& n); + + bool update(const ASTNode&n, const int i, simplifier::constantBitP::FixedBits*b, BBNode& bb, set& support); + void updateTerm(const ASTNode&n, vector& bb, set& support); + void updateForm(const ASTNode&n, BBNode& bb, set& support); public: BBNodeManagerT* nf; @@ -123,9 +144,22 @@ public: * Public Member Functions * ****************************************************************/ + BitBlaster(BBNodeManagerT* bnm , simplifier::constantBitP::ConstantBitPropagation *cb_) + { + nf = bnm; + cb = cb_; + BBTrue = nf->getTrue(); + BBFalse = nf->getFalse(); + } + + + BitBlaster(BBNodeManagerT* bnm) { nf = bnm; + BBTrue = nf->getTrue(); + BBFalse = nf->getFalse(); + cb = NULL; } -- 2.47.3