From: trevor_hansen Date: Sat, 28 Aug 2010 02:52:36 +0000 (+0000) Subject: Changes to inactive by default code. X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=ca9a9486e38b48dc7853b34e2ae49f3da42f6207;p=francis%2Fstp.git Changes to inactive by default code. This patch makes the term-level simplifier, the bit-blaster and the constant bit propagation co-operate during simplification. If the cbitp or the bitblaster discover a new constant. Then the term-level simplifier will be re-ran. I haven't experimented whether this is useful yet. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1002 e59a4935-1847-0410-ae03-e826735625c1 --- diff --git a/src/AST/NodeFactory/NodeFactory.cpp b/src/AST/NodeFactory/NodeFactory.cpp index ff7af9b..3e4b805 100644 --- a/src/AST/NodeFactory/NodeFactory.cpp +++ b/src/AST/NodeFactory/NodeFactory.cpp @@ -104,6 +104,9 @@ BEEV::ASTNode NodeFactory::CreateArrayTerm(Kind kind, unsigned int index, return result; } +BEEV::ASTNode NodeFactory::getTrue() {return bm.ASTTrue;} +BEEV::ASTNode NodeFactory::getFalse(){return bm.ASTFalse;} + ASTNode NodeFactory::CreateSymbol(const char * const name, unsigned indexWidth, unsigned valueWidth) { @@ -112,3 +115,8 @@ ASTNode NodeFactory::CreateSymbol(const char * const name, unsigned indexWidth, n.SetValueWidth(valueWidth); return n; } + +ASTNode NodeFactory::CreateConstant(BEEV::CBV cbv, unsigned width) +{ + return bm.CreateBVConst(cbv,width); +} diff --git a/src/AST/NodeFactory/NodeFactory.h b/src/AST/NodeFactory/NodeFactory.h index e09934d..a32e3a0 100644 --- a/src/AST/NodeFactory/NodeFactory.h +++ b/src/AST/NodeFactory/NodeFactory.h @@ -11,6 +11,7 @@ class ASTNode; typedef std::vector ASTVec; extern ASTVec _empty_ASTVec; class STPMgr; +typedef unsigned int * CBV; } using BEEV::ASTNode; @@ -60,6 +61,11 @@ public: const ASTNode& child1, const ASTNode& child2, const ASTVec &children = _empty_ASTVec); + ASTNode getTrue(); + ASTNode getFalse(); + + ASTNode CreateConstant(BEEV::CBV cbv, unsigned width); + }; #endif diff --git a/src/simplifier/constantBitP/ConstantBitPropagation.h b/src/simplifier/constantBitP/ConstantBitPropagation.h index 7b8bdd3..454c799 100644 --- a/src/simplifier/constantBitP/ConstantBitPropagation.h +++ b/src/simplifier/constantBitP/ConstantBitPropagation.h @@ -105,6 +105,12 @@ public: ASTNodeMap getAllFixed(); + + void initWorkList(const ASTNode n) + { + workList->initWorkList(n); + } + }; } } diff --git a/src/simplifier/constantBitP/FixedBits.h b/src/simplifier/constantBitP/FixedBits.h index 6ded3d7..859a715 100644 --- a/src/simplifier/constantBitP/FixedBits.h +++ b/src/simplifier/constantBitP/FixedBits.h @@ -279,6 +279,21 @@ namespace simplifier void getUnsignedMinMax(unsigned &minShift, unsigned &maxShift) const; + void + mergeIn(const FixedBits& a) + { + assert(a.getWidth() == getWidth()); + for (int i= 0; i < width;i++) + { + if (a.isFixed(i) && !isFixed(i)) + { + setFixed(i,true); + setValue(i,a.getValue(i)); + } + } + } + + static FixedBits meet(const FixedBits& a, const FixedBits& b); diff --git a/src/simplifier/constantBitP/WorkList.h b/src/simplifier/constantBitP/WorkList.h index 4900ed5..df957fe 100644 --- a/src/simplifier/constantBitP/WorkList.h +++ b/src/simplifier/constantBitP/WorkList.h @@ -48,11 +48,18 @@ namespace simplifier // Add to the worklist any node that immediately depends on a constant. WorkList(const ASTNode& top) + { + initWorkList(top); + } + + void + initWorkList(const ASTNode&n) { ASTNodeSet visited; - addToWorklist(top, visited); + addToWorklist(n, visited); } + void push(const BEEV::ASTNode& n) { diff --git a/src/to-sat/AIG/BBNodeManagerAIG.cpp b/src/to-sat/AIG/BBNodeManagerAIG.cpp index 088349d..f124737 100644 --- a/src/to-sat/AIG/BBNodeManagerAIG.cpp +++ b/src/to-sat/AIG/BBNodeManagerAIG.cpp @@ -18,12 +18,13 @@ namespace BEEV // Rewriting is sometimes very slow. Can it be configured to be faster? // What about refactoring??? - if (uf.enable_AIG_rewrites_flag) - { - int nodeCount = aigMgr->nObjs[AIG_OBJ_AND]; - if (uf.stats_flag) - cerr << "Nodes before AIG rewrite:" << nodeCount <nObjs[AIG_OBJ_AND]; + if (uf.stats_flag) + cerr << "Nodes before AIG rewrite:" << nodeCount <nObjs[AIG_OBJ_AND] < 5000) + { Dar_LibStart(); Aig_Man_t * pTemp; Dar_RwrPar_t Pars, * pPars = &Pars; @@ -38,12 +39,6 @@ namespace BEEV // With nCutsMax =2, CNF generation takes 16 seconds, solving 10 seconds. // The rewriting doesn't remove as many nodes of course.. int iterations = 3; - if (nodeCount > 1000000) - { - iterations =1; - pPars->nCutsMax=2; - } - for (int i=0; i < iterations;i++) { diff --git a/src/to-sat/AIG/ToSATAIG.cpp b/src/to-sat/AIG/ToSATAIG.cpp index f1980f0..7774d6a 100644 --- a/src/to-sat/AIG/ToSATAIG.cpp +++ b/src/to-sat/AIG/ToSATAIG.cpp @@ -1,5 +1,6 @@ #include "ToSATAIG.h" #include "../../simplifier/constantBitP/ConstantBitPropagation.h" +#include "../../simplifier/simplifier.h" namespace BEEV { @@ -12,14 +13,20 @@ namespace BEEV return false; BBNodeManagerAIG mgr; - BitBlaster bb(&mgr,cb); + Simplifier simp(bm); + BitBlaster bb(&mgr,cb,&simp,bm->defaultNodeFactory,&bm->UserFlags); bm->GetRunTimes()->start(RunTimes::BitBlasting); BBNodeAIG BBFormula = bb.BBForm(input); bm->GetRunTimes()->stop(RunTimes::BitBlasting); + bb.ClearAllTables(); assert(satSolver.nVars() ==0); + // Oddly the substitution map, which is necessary to output a model is kept in the simplifier. + // The bitblaster should never enter anything into the solver map. + //assert(simp.Return_SolverMap()->size() ==0); + Cnf_Dat_t* cnfData = NULL; bm->GetRunTimes()->start(RunTimes::CNFConversion); @@ -30,17 +37,6 @@ namespace BEEV 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; - } - */ - //Clear out all the constant bit stuff before sending the SAT. if (cb != NULL) cb->clearTables(); diff --git a/src/to-sat/BitBlaster.cpp b/src/to-sat/BitBlaster.cpp index ee2b0dd..46cc4cf 100644 --- a/src/to-sat/BitBlaster.cpp +++ b/src/to-sat/BitBlaster.cpp @@ -15,6 +15,7 @@ #include "../simplifier/constantBitP/FixedBits.h" #include "../simplifier/constantBitP/ConstantBitPropagation.h" #include "../simplifier/constantBitP/NodeToFixedBitsMap.h" +#include "../simplifier/simplifier.h" namespace BEEV { @@ -136,6 +137,9 @@ void BitBlaster::updateTerm(const ASTNode&n, BBNodeVec& b if (cb == NULL) return; + if (cb->isUnsatisfiable()) + return; + if (n.isConstant()) { simplifier::constantBitP::NodeToFixedBitsMap::NodeToFixedBitsMapType::const_iterator it; @@ -212,18 +216,169 @@ void BitBlaster::updateTerm(const ASTNode&n, BBNodeVec& b } } +template +bool BitBlaster::isConstant(const BBNodeVec& v) +{ + for (int i =0; i < v.size();i++) + { + if (v[i] != nf->getTrue() && v[i] != nf->getFalse()) + return false; + } + return true; +} template -const BBNodeVec BitBlaster::BBTerm(const ASTNode& term, BBNodeSet& support) { - typename BBNodeVecMap::iterator it = BBTermMemo.find(term); +ASTNode BitBlaster::getConstant(const BBNodeVec& v, const ASTNode&n ) +{ + if (n.GetType() == BOOLEAN_TYPE) + { + if (v[0] == nf->getTrue()) + return ASTNF->getTrue(); + else + return ASTNF->getFalse(); + } + + CBV bv = CONSTANTBV::BitVector_Create(v.size(),true); + + for (int i =0; i < v.size();i++) + if (v[i] == nf->getTrue()) + CONSTANTBV::BitVector_Bit_On(bv,i); + + return ASTNF->CreateConstant(bv,v.size()); + +} + +template +const BBNodeVec BitBlaster::BBTerm(const ASTNode& _term, BBNodeSet& support) { + ASTNode term = _term; // mutable local copy. + + typename BBNodeVecMap::iterator it = BBTermMemo.find(term); if (it != BBTermMemo.end()) { // Constant bit propagation may have updated something. updateTerm(term,it->second,support); return it->second; } + // This block checks if the bitblasting/fixed bits have discovered + // any new constants. If they've discovered a new constant, then + // the simplification function is called on a new term with the constant + // value replacing what used to be a variable child. For instance, if + // the term is ite(x,y,z), and we now know that x is true. Then we will + // call SimplifyTerm on ite(true,y,z), which will do the expected simplification. + // Then the term that we bitblast will by "y". + + if (uf !=NULL && uf->optimize_flag) + { + const int numberOfChildren = term.Degree(); + vector ch; + ch.reserve(numberOfChildren); + + for (int i = 0; i < numberOfChildren; i++) + { + if (term[i].GetType() == BITVECTOR_TYPE) + { + ch.push_back(BBTerm(term[i],support)); + } + else if (term[i].GetType() == BOOLEAN_TYPE) + { + BBNodeVec t; + t.push_back(BBForm(term[i],support)); + ch.push_back(t); + } + else + throw "sdfssfa"; + } + + bool newConst = false; + for (int i = 0; i < numberOfChildren; i++) + { + if (term[i].isConstant()) + continue; + + if (isConstant(ch[i])) + { + // it's only interesting if the child isn't a constant, + // but the bitblasted version is. + newConst = true; + break; + } + } + + // Something is now constant that didn't used to be. + if (newConst) + { + ASTVec new_ch; + new_ch.reserve(numberOfChildren); + for (int i = 0; i < numberOfChildren; i++) + { + if (!term[i].isConstant() && isConstant(ch[i])) + new_ch.push_back(getConstant(ch[i], term[i])); + else + new_ch.push_back(term[i]); + } + + + ASTNode n_term = simp->SimplifyTerm(ASTNF->CreateTerm(term.GetKind(),term.GetValueWidth(),new_ch)); + assert(BVTypeCheck(n_term)); + // n_term is the potentially simplified version of term. + + if (cb!= NULL) + { + // Add all the nodes to the worklist that have a constant as a child. + cb->initWorkList(n_term); + + simplifier::constantBitP::NodeToFixedBitsMap::NodeToFixedBitsMapType::iterator it; + it = cb->fixedMap->map->find(n_term) ; + FixedBits* nBits; + if (it == cb->fixedMap->map->end()) + { + nBits = new FixedBits(std::max((unsigned)1,n_term.GetValueWidth()), term.GetType() == BOOLEAN_TYPE); + cb->fixedMap->map->insert(pair (n_term, nBits)); + }else + nBits = it->second; + + if (n_term.isConstant()) + { + // It's assumed elsewhere that constants map to themselves in the fixed map. + // That doesn't happen here unless it's added explicitly. + *nBits = FixedBits::concreteToAbstract(n_term); + } + + it = cb->fixedMap->map->find(term); + if (it != cb->fixedMap->map->end()) + { + // Copy over to the (potentially) new node. Everything we know about the old node. + nBits->mergeIn(*(it->second)); + + } + cb->propagate(); + + it = cb->fixedMap->map->find(term); + if (it != cb->fixedMap->map->end()) + { + // Copy to the old node, all we know about the new node. This means that + // all the parents of the old node get the (potentially) updated fixings. + it->second->mergeIn(*nBits); + } + // Propagate through all the parents of term. + cb->scheduleUp(term); + cb->propagate(); + // Now we've propagated. + } + term = n_term; + + // check if we've already done the simplified one. + it = BBTermMemo.find(term); + if (it != BBTermMemo.end()) { + // Constant bit propagation may have updated something. + updateTerm(term,it->second,support); + return it->second; + } + } + } + BBNodeVec result; const Kind k = term.GetKind(); @@ -1305,6 +1460,7 @@ const bool multiplication_variant3 = true; // multiplication with booth recoding const bool multiplication_variant4 = false; // multiplication via sorting networks. const bool multiplication_variant5 = false; // Using bounds. + // Multiply two bitblasted numbers template BBNodeVec BitBlaster::BBMult(const BBNodeVec& _x, const BBNodeVec& _y, @@ -1323,23 +1479,27 @@ BBNodeVec BitBlaster::BBMult(const BBNodeVec& _x, const B const int bitWidth = x.size(); if (multiplication_variant1) { + //cout << "v1"; return mult_normal(x, y, support); } stack products[bitWidth]; if (multiplication_variant2) { + //cout << "v2"; mult_allPairs(x, y, support,products); return buildAdditionNetworkResult(products,support, bitWidth); } if (multiplication_variant3) { + //cout << "v3"; mult_Booth(_x, _y, support,n[0],n[1],products); return buildAdditionNetworkResult(products,support,bitWidth); } if (multiplication_variant4) { + //cout << "v4"; mult_Booth(_x, _y, support,n[0],n[1],products); for (int i = 0; i < bitWidth; i++) { @@ -1354,7 +1514,7 @@ BBNodeVec BitBlaster::BBMult(const BBNodeVec& _x, const B if (multiplication_variant5) { - + //cout << "v5"; if (!statsFound(n)) { mult_Booth(_x, _y, support, n[0], n[1], products); diff --git a/src/to-sat/BitBlaster.h b/src/to-sat/BitBlaster.h index e73f3e3..a78d716 100644 --- a/src/to-sat/BitBlaster.h +++ b/src/to-sat/BitBlaster.h @@ -14,6 +14,7 @@ #include #include #include "../STPManager/STPManager.h" +//#include "../STPManager/UserDefinedFlags.h" namespace simplifier { @@ -26,6 +27,7 @@ namespace simplifier namespace BEEV { +class Simplifier; class ASTNode; typedef std::vector ASTVec; @@ -150,12 +152,19 @@ class BitBlaster { const BBNode BBForm(const ASTNode& form, set& support); + bool isConstant(const vector& v); + ASTNode getConstant(const vector& v, const ASTNode&n ); + // Nodes in this set can be replaced by their constant values, without being // conjoined to the top.. ASTNodeSet fixedFromBottom; + UserDefinedFlags *uf; + NodeFactory* ASTNF; + Simplifier* simp; + BBNodeManagerT* nf; + public: - BBNodeManagerT* nf; // Bit blast a bitvector term. The term must have a kind for a // bitvector term. Result is a ref to a vector of formula nodes @@ -166,28 +175,39 @@ public: * Public Member Functions * ****************************************************************/ - BitBlaster(BBNodeManagerT* bnm , simplifier::constantBitP::ConstantBitPropagation *cb_) + BitBlaster(BBNodeManagerT* bnm , simplifier::constantBitP::ConstantBitPropagation *cb_, Simplifier* _simp, NodeFactory *astNodeF, UserDefinedFlags *_uf) { nf = bnm; cb = cb_; BBTrue = nf->getTrue(); BBFalse = nf->getFalse(); + simp = _simp; + ASTNF = astNodeF; + uf = _uf; } - BitBlaster(BBNodeManagerT* bnm) + BitBlaster(BBNodeManagerT* bnm, Simplifier* _simp, NodeFactory *astNodeF) { nf = bnm; BBTrue = nf->getTrue(); BBFalse = nf->getFalse(); cb = NULL; + simp = _simp; + ASTNF = astNodeF; + uf = NULL; } + void ClearAllTables() + { + BBTermMemo.clear(); + BBFormMemo.clear(); + } + ~BitBlaster() { - BBTermMemo.clear(); - BBFormMemo.clear(); + ClearAllTables(); } //Bitblast a formula diff --git a/src/to-sat/ToSAT.cpp b/src/to-sat/ToSAT.cpp index 3cae175..9954dc3 100644 --- a/src/to-sat/ToSAT.cpp +++ b/src/to-sat/ToSAT.cpp @@ -337,7 +337,8 @@ namespace BEEV ASTNode BBFormula; { BBNodeManagerASTNode nm(bm); - BitBlaster BB(&nm); + Simplifier simp(bm); + BitBlaster BB(&nm,&simp, bm->defaultNodeFactory); BBFormula = BB.BBForm(input); }