From b61701018ee053583f20c783ac9d1285fb2178b9 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Thu, 7 Apr 2011 13:22:05 +0000 Subject: [PATCH] Hack. The ITE context simplification blows out ff.stp, i.e. it takes > 5 minutes. This limits ITE context simplifications to small contexts. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1254 e59a4935-1847-0410-ae03-e826735625c1 --- src/simplifier/SubstitutionMap.h | 4 +- src/simplifier/UseITEContext.h | 4 ++ src/simplifier/bvsolver.cpp | 68 +++++++++++++++++--------------- src/simplifier/bvsolver.h | 4 +- src/simplifier/simplifier.cpp | 18 ++++++++- 5 files changed, 63 insertions(+), 35 deletions(-) diff --git a/src/simplifier/SubstitutionMap.h b/src/simplifier/SubstitutionMap.h index 5c4ca60..0cb882a 100644 --- a/src/simplifier/SubstitutionMap.h +++ b/src/simplifier/SubstitutionMap.h @@ -98,7 +98,9 @@ public: ASTNode var = (BVEXTRACT == key.GetKind()) ? key[0] : key; if (var.GetKind() == SYMBOL && loops(var,value)) - return false; + { + return false; + } if (!CheckSubstitutionMap(var) && key != value) { diff --git a/src/simplifier/UseITEContext.h b/src/simplifier/UseITEContext.h index 47d3836..9c19b14 100644 --- a/src/simplifier/UseITEContext.h +++ b/src/simplifier/UseITEContext.h @@ -63,9 +63,13 @@ namespace BEEV if (n.isAtom()) return n; + // Hacks to stop it blowing out.. { if (visited[n]++ > 10) return n; + + if (context.size() > 20) + return n; } ASTVec new_children; diff --git a/src/simplifier/bvsolver.cpp b/src/simplifier/bvsolver.cpp index c67f466..41d4715 100644 --- a/src/simplifier/bvsolver.cpp +++ b/src/simplifier/bvsolver.cpp @@ -37,17 +37,34 @@ //2. paper for actual solving procedure // //4. Outside the solver, Substitute and Re-normalize the input DAG + + +// This has a "slow mode", that performs time-consuming substitutions. +// In slow mode it does applySubstitutions as it goes, it +// applies the Simplify functions, and it solves for "even" monomials. +// If we're not in slow mode this might take longer to fixed point. For +// instance given: +// 0 = 4x1 + 3x2 + 2x3 + 1x4. +// 0 = 4x1 + 8x2 + 6x3 + 5x4. +// 0 = 1x1 + 2x2 + 7x3 + 5x4. +// The first replacement may be for 3x2, because substitutions aren't being applied +// then the next two will fail (because any monomial chosen will appear in the rhs). +// After applying through the substitutions & simplifying. The second formula will +// change from 0 = 4x1 + 8(-(1/3)(4x1 + 2x3 + 1x4)) + 6x3 + 5x4. +// to having each variable appear only a single time, so it can be solved for. + + + namespace BEEV { const bool flatten_ands = true; - const bool sort_extracts_last = false; const bool debug_bvsolver = false; // The simplify functions can increase the size of the DAG, // so we have the option to disable simplifications. ASTNode BVSolver::simplifyNode(const ASTNode n) { - if (!simplify) + if (!slow) return n; if (n.GetType() == BOOLEAN_TYPE) @@ -91,9 +108,11 @@ namespace BEEV assert(number_shifts >0); // shouldn't be odd. } + // This doesn't seem necessary for correctness, it just stops you checking the same values over and over.. bool BVSolver::DoNotSolveThis(const ASTNode& var) { - return (DoNotSolve_TheseVars.find(var) != DoNotSolve_TheseVars.end()); + return false; + //return (DoNotSolve_TheseVars.find(var) != DoNotSolve_TheseVars.end()); } //chooses a variable in the lhs and returns the chosen variable @@ -148,25 +167,12 @@ namespace BEEV // that the variable appears in none of them. ASTNode var = (SYMBOL == monom.GetKind())? monom: monom[0]; - bool duplicated = false; - for (ASTVec::const_iterator it2 = c.begin(); it2 != itend; it2++) - { - if (it2 == it) - continue; - if (vars.VarSeenInTerm(var,*it2)) - { - duplicated = true; - break; - } - } - if (!duplicated) + { outmonom = monom; //nb. monom not var. chosen_symbol = true; checked.insert(var); } - else - o.push_back(monom); } else o.push_back(monom); @@ -281,14 +287,6 @@ namespace BEEV { DoNotSolve_TheseVars.insert(lhs); - //input is of the form x = rhs first make sure that the lhs - //symbol does not occur on the rhs or that it has not been - //solved for - if (!single && vars.VarSeenInTerm(lhs, rhs)) - { - //found the lhs in the rhs. Abort! - return eq; - } if (!_simp->UpdateSolverMap(lhs, rhs)) { @@ -614,15 +612,17 @@ namespace BEEV for (ASTVec::const_iterator and_child = c.begin(), and_end = c.end(); and_child != and_end; and_child++) { + ASTNode r = *and_child; + if (slow && changed) // Simplifier expects substitutions to be applied. + r = _simp->applySubstitutionMapUntilArrays(r); - ASTNode r = solveForXOR(!changed?*and_child:simplifyNode(_simp->applySubstitutionMapUntilArrays(*and_child))); + r = solveForXOR(!changed?r:simplifyNode((r))); if (r!=*and_child) changed=true; output_children.push_back(r); } return nf->CreateNode(AND, output_children); - } @@ -633,7 +633,7 @@ namespace BEEV { assert (_bm->UserFlags.wordlevel_solve_flag); ASTNode input = _input; - simplify = enable_simplify; + slow = enable_simplify; ASTNode output = input; if (CheckAlreadySolvedMap(input, output)) @@ -703,8 +703,14 @@ namespace BEEV which shouldn't be simplified. */ - ASTNode aaa = (any_solved && EQ == it->GetKind()) ? simplifyNode - (_simp->applySubstitutionMapUntilArrays(*it)) : *it; + // simplifyNode expects substitutions to already be applied. + ASTNode aaa = *it; + if (EQ == it->GetKind() && any_solved) + { + if (slow) + aaa = _simp->applySubstitutionMapUntilArrays(aaa); + aaa = (any_solved && EQ == it->GetKind()) ? simplifyNode(aaa) : aaa; + } if (ASTFalse == aaa) { @@ -847,7 +853,7 @@ namespace BEEV // return input; // } - if (!(EQ == input.GetKind() || AND == input.GetKind())) + if (slow || !(EQ == input.GetKind() || AND == input.GetKind())) { return input; } diff --git a/src/simplifier/bvsolver.h b/src/simplifier/bvsolver.h index 1585bd3..0454b39 100644 --- a/src/simplifier/bvsolver.h +++ b/src/simplifier/bvsolver.h @@ -115,7 +115,7 @@ namespace BEEV VariablesInExpression& vars; - bool simplify; //Whether to apply the simplifyTerm & simplifyFormula functions. + bool slow; //Whether to apply the simplifyTerm & simplifyFormula functions. ASTNode simplifyNode(const ASTNode n); @@ -128,7 +128,7 @@ namespace BEEV ASTTrue = _bm->CreateNode(TRUE); ASTFalse = _bm->CreateNode(FALSE); ASTUndefined = _bm->CreateNode(UNDEFINED); - simplify=true; + slow=true; nf = new SimplifyingNodeFactory(*bm->hashingNodeFactory,*bm); }; diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp index ecc4c22..3b02959 100644 --- a/src/simplifier/simplifier.cpp +++ b/src/simplifier/simplifier.cpp @@ -67,6 +67,14 @@ namespace BEEV { return false; } + + if (!pushNeg && key.isSimplfied()) + { + output = key; + return true; + } + + ASTNodeMap::iterator it, itend; it = pushNeg ? SimplifyNegMap->find(key) : SimplifyMap->find(key); itend = pushNeg ? SimplifyNegMap->end() : SimplifyMap->end(); @@ -106,11 +114,16 @@ namespace BEEV // to cache. if (0 == key.Degree()) return; - + if (pushNeg) (*SimplifyNegMap)[key] = value; else (*SimplifyMap)[key] = value; + + if (!pushNeg && key == value) + { + key.hasBeenSimplfied(); + } } // Substitution Map methods.... @@ -1661,6 +1674,9 @@ namespace BEEV if (n.isConstant()) return true; + if (n.isSimplfied()) + return true; + //If it's a symbol that's not in the substitition Map. if (n.GetKind() == SYMBOL && CheckSubstitutionMap(n)) return false; -- 2.47.3