From ded912df6dc4a00636278bd2fdad13e9e750ab53 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Mon, 28 Mar 2011 00:36:48 +0000 Subject: [PATCH] During the size reducing transformations, now set the top node to true during constant bit propagation. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1243 e59a4935-1847-0410-ae03-e826735625c1 --- src/STPManager/STP.cpp | 44 ++++++++++++++----- .../constantBitP/ConstantBitPropagation.cpp | 43 +++++++++++++++--- .../constantBitP/ConstantBitPropagation.h | 2 +- src/simplifier/constantBitP/FixedBits.h | 14 +++++- 4 files changed, 83 insertions(+), 20 deletions(-) diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp index dd36322..5ca0883 100644 --- a/src/STPManager/STP.cpp +++ b/src/STPManager/STP.cpp @@ -100,27 +100,33 @@ namespace BEEV { bm->ASTNodeStats("After Establishing Intervals: ", simplified_solved_InputToSAT); } + simplified_solved_InputToSAT = simp->CreateSubstitutionMap(simplified_solved_InputToSAT, arrayTransformer); + if (simp->hasUnappliedSubstitutions()) + { + simplified_solved_InputToSAT = simp->applySubstitutionMap(simplified_solved_InputToSAT); + simp->haveAppliedSubstitutionMap(); + bm->ASTNodeStats("After Propagating Equalities: ", simplified_solved_InputToSAT); + } + if (bm->UserFlags.bitConstantProp_flag) { bm->GetRunTimes()->start(RunTimes::ConstantBitPropagation); SimplifyingNodeFactory nf(*(bm->hashingNodeFactory), *bm); simplifier::constantBitP::ConstantBitPropagation cb(simp, &nf, simplified_solved_InputToSAT); - simplified_solved_InputToSAT = cb.topLevelBothWays(simplified_solved_InputToSAT, false); + simplified_solved_InputToSAT = cb.topLevelBothWays(simplified_solved_InputToSAT, true,false); bm->GetRunTimes()->stop(RunTimes::ConstantBitPropagation); if (cb.isUnsatisfiable()) simplified_solved_InputToSAT = bm->ASTFalse; - bm->ASTNodeStats("After Constant Bit Propagation begins: ", simplified_solved_InputToSAT); - } + if (simp->hasUnappliedSubstitutions()) + { + simplified_solved_InputToSAT = simp->applySubstitutionMap(simplified_solved_InputToSAT); + simp->haveAppliedSubstitutionMap(); + } - simplified_solved_InputToSAT = simp->CreateSubstitutionMap(simplified_solved_InputToSAT, arrayTransformer); - if (simp->hasUnappliedSubstitutions()) - { - simplified_solved_InputToSAT = simp->applySubstitutionMap(simplified_solved_InputToSAT); - simp->haveAppliedSubstitutionMap(); - bm->ASTNodeStats("After Propagating Equalities: ", simplified_solved_InputToSAT); + bm->ASTNodeStats("After Constant Bit Propagation begins: ", simplified_solved_InputToSAT); } // Find pure literals. @@ -167,19 +173,35 @@ namespace BEEV { BVSolver* bvSolver = new BVSolver(bm, simp); simplified_solved_InputToSAT = sizeReducing(inputToSAT, bvSolver); - //simplified_solved_InputToSAT = sizeReducing(simplified_solved_InputToSAT,bvSolver); unsigned initial_difficulty_score = difficulty.score(simplified_solved_InputToSAT); + + // Fixed point it if it's not too difficult. + // Currently we discards all the state each time sizeReducing is called, + // so it's expensive to call. + if (!arrayops && initial_difficulty_score < 1000000) + { + while (true) + { + ASTNode last = simplified_solved_InputToSAT; + simplified_solved_InputToSAT = sizeReducing(last, bvSolver); + if (last == simplified_solved_InputToSAT) + break; + } + initial_difficulty_score = difficulty.score(simplified_solved_InputToSAT); + } + if (bm->UserFlags.stats_flag) cout << "Difficulty After Size reducing:" << initial_difficulty_score << endl; // Copy the solver map incase we need to revert. ASTNodeMap initialSolverMap; + ASTNode toRevertTo; if (!arrayops) // we don't revert for Array problems yet, so don't copy it. { initialSolverMap.insert(simp->Return_SolverMap()->begin(), simp->Return_SolverMap()->end()); + toRevertTo = simplified_solved_InputToSAT; } - ASTNode toRevertTo = simplified_solved_InputToSAT; //round of substitution, solving, and simplification. ensures that //DAG is minimized as much as possibly, and ideally should diff --git a/src/simplifier/constantBitP/ConstantBitPropagation.cpp b/src/simplifier/constantBitP/ConstantBitPropagation.cpp index 53b307d..05d970e 100644 --- a/src/simplifier/constantBitP/ConstantBitPropagation.cpp +++ b/src/simplifier/constantBitP/ConstantBitPropagation.cpp @@ -209,9 +209,9 @@ namespace simplifier // 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. + // NB: This expects that the constructor was called with the same node. Sorry. ASTNode - ConstantBitPropagation::topLevelBothWays(const ASTNode& top, bool setTopToTrue) + ConstantBitPropagation::topLevelBothWays(const ASTNode& top, bool setTopToTrue, bool conjoinToTop) { assert(top.GetSTPMgr()->UserFlags.bitConstantProp_flag); assert (BOOLEAN_TYPE == top.GetType()); @@ -261,10 +261,35 @@ namespace simplifier { const FixedBits& bits = *it->second; + const ASTNode& node = (it->first); + + if (false && node.GetKind() == SYMBOL && !bits.isTotallyFixed() && bits.countFixed() > 0) + { + // replace partially known variables with new variables. + int leastFixed = bits.leastUnfixed(); + int mostFixed = bits.mostUnfixed(); + const int width = node.GetValueWidth(); + + int new_width = mostFixed - leastFixed +1; + assert(new_width > 0); + ASTNode fresh = node.GetSTPMgr()->CreateFreshVariable(0,new_width,"STP_REPLACE"); + ASTNode a,b; + if (leastFixed > 0) + a= node.GetSTPMgr()->CreateBVConst(bits.GetBVConst( leastFixed-1, 0), leastFixed); + if (mostFixed != width-1) + b = node.GetSTPMgr()->CreateBVConst(bits.GetBVConst( width-1, mostFixed+1),width-1-mostFixed); + if (!a.IsNull()) + fresh = nf->CreateTerm(BVCONCAT, a.GetValueWidth() + fresh.GetValueWidth(), fresh, a); + if (!b.IsNull()) + fresh = nf->CreateTerm(BVCONCAT, b.GetValueWidth() + fresh.GetValueWidth(), b, fresh); + assert(fresh.GetValueWidth() == node.GetValueWidth()); + bool r = simplifier->UpdateSubstitutionMap(node, fresh); + assert(r); + } + if (!bits.isTotallyFixed()) continue; - const ASTNode& node = (it->first); // Don't constrain nodes we already know all about. if (node.isConstant()) @@ -279,7 +304,7 @@ namespace simplifier ASTNode propositionToAssert; ASTNode constantToReplaceWith; // skip the assigning and replacing. - bool doAssign = true; + bool doAssign = false; { // If it is already contained in the fromTo map, then it's one of the values @@ -297,15 +322,17 @@ namespace simplifier assert(r); doAssign = false; } - else if (bits.getValue(0)) + else if (conjoinToTop && bits.getValue(0)) { propositionToAssert = node; constantToReplaceWith = constNode; + doAssign=true; } - else + else if (conjoinToTop) { propositionToAssert = nf->CreateNode(NOT, node); constantToReplaceWith = constNode; + doAssign=true; } } else if (node.GetType() == BITVECTOR_TYPE) @@ -317,10 +344,11 @@ namespace simplifier assert(r); doAssign = false; } - else + else if (conjoinToTop) { propositionToAssert = nf->CreateNode(EQ, node, constNode); constantToReplaceWith = constNode; + doAssign=true; } } else @@ -337,6 +365,7 @@ namespace simplifier fromTo.insert(make_pair(node, constantToReplaceWith)); toConjoin.push_back(propositionToAssert); + assert(conjoinToTop); } } diff --git a/src/simplifier/constantBitP/ConstantBitPropagation.h b/src/simplifier/constantBitP/ConstantBitPropagation.h index 0bdb5b0..6159c80 100644 --- a/src/simplifier/constantBitP/ConstantBitPropagation.h +++ b/src/simplifier/constantBitP/ConstantBitPropagation.h @@ -73,7 +73,7 @@ public: // Returns the node after writing in simplifications from constant Bit propagation. BEEV::ASTNode - topLevelBothWays(const ASTNode& top, bool setTopToTrue = true); + topLevelBothWays(const ASTNode& top, bool setTopToTrue = true, bool conjoinToTop=true); void clearTables() diff --git a/src/simplifier/constantBitP/FixedBits.h b/src/simplifier/constantBitP/FixedBits.h index 859a715..5b7c4bf 100644 --- a/src/simplifier/constantBitP/FixedBits.h +++ b/src/simplifier/constantBitP/FixedBits.h @@ -145,7 +145,7 @@ namespace simplifier //Returns the position of the first non-fixed value. int - leastUnfixed() + leastUnfixed() const { int i = 0; for (; i < getWidth(); i++) @@ -156,6 +156,18 @@ namespace simplifier return i; } + int + mostUnfixed() const + { + int i = getWidth()-1; + for (; i >=0; i--) + { + if (!isFixed(i)) + break; + } + return i; + } + // is this bit fixed to zero? bool isFixedToZero(int n) const -- 2.47.3