From 2556f7c211e1acd71ec913718e062e857c5550c3 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Thu, 5 Aug 2010 15:17:31 +0000 Subject: [PATCH] Speedup the bvsolver. Use the applySubstitutionMap function to apply the discovered replacements rather than using simplifyFormula. This means that the simplification caches don't need to be cleaned out (saving time). git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@967 e59a4935-1847-0410-ae03-e826735625c1 --- src/simplifier/SubstitutionMap.cpp | 27 +++++++++--- src/simplifier/SubstitutionMap.h | 5 +++ src/simplifier/bvsolver.cpp | 68 +++++++++++++++--------------- src/simplifier/simplifier.cpp | 15 +++++-- src/simplifier/simplifier.h | 1 + 5 files changed, 73 insertions(+), 43 deletions(-) diff --git a/src/simplifier/SubstitutionMap.cpp b/src/simplifier/SubstitutionMap.cpp index 1f24bf7..6303505 100644 --- a/src/simplifier/SubstitutionMap.cpp +++ b/src/simplifier/SubstitutionMap.cpp @@ -193,7 +193,19 @@ ASTNode SubstitutionMap::CreateSubstitutionMap(const ASTNode& a, ArrayTransform ASTNode SubstitutionMap::applySubstitutionMap(const ASTNode& n) { ASTNodeMap cache; - return replace(n,*SolverMap,cache,bm->defaultNodeFactory); + return replace(n,*SolverMap,cache,bm->defaultNodeFactory, false); +} + +ASTNode SubstitutionMap::applySubstitutionMapUntilArrays(const ASTNode& n) +{ + ASTNodeMap cache; + return replace(n,*SolverMap,cache,bm->defaultNodeFactory, true); +} + +ASTNode SubstitutionMap::replace(const ASTNode& n, ASTNodeMap& fromTo, + ASTNodeMap& cache, NodeFactory * nf) +{ + return replace(n,fromTo,cache,nf,false); } // NOTE the fromTo map is changed as we traverse downwards. @@ -203,7 +215,7 @@ ASTNode SubstitutionMap::applySubstitutionMap(const ASTNode& n) // will return 5, rather than y. ASTNode SubstitutionMap::replace(const ASTNode& n, ASTNodeMap& fromTo, - ASTNodeMap& cache, NodeFactory * nf) + ASTNodeMap& cache, NodeFactory * nf, bool stopAtArrays) { ASTNodeMap::const_iterator it; @@ -217,13 +229,13 @@ ASTNode SubstitutionMap::replace(const ASTNode& n, ASTNodeMap& fromTo, const ASTNode& r = it->second; assert(r.GetIndexWidth() == n.GetIndexWidth()); assert(BVTypeCheck(r)); - ASTNode replaced = replace(r, fromTo, cache,nf); + ASTNode replaced = replace(r, fromTo, cache,nf,stopAtArrays); if (replaced != r) fromTo[n] = replaced; return replaced; } - ASTNode replaced = replace(it->second, fromTo, cache,nf); + ASTNode replaced = replace(it->second, fromTo, cache,nf,stopAtArrays); if (replaced != it->second) fromTo[n] = replaced; @@ -234,11 +246,16 @@ ASTNode SubstitutionMap::replace(const ASTNode& n, ASTNodeMap& fromTo, if (n.isConstant() || n.GetKind() == SYMBOL /*|| n.GetKind() == WRITE*/) return n; + if (stopAtArrays && n.GetType() == ARRAY_TYPE) + { + return n; + } + ASTVec children; children.reserve(n.GetChildren().size()); for (unsigned i = 0; i < n.GetChildren().size(); i++) { - children.push_back(replace(n[i], fromTo, cache,nf)); + children.push_back(replace(n[i], fromTo, cache,nf,stopAtArrays)); } // This code short-cuts if the children are the same. Nodes with the same children, diff --git a/src/simplifier/SubstitutionMap.h b/src/simplifier/SubstitutionMap.h index 8345374..d0aba07 100644 --- a/src/simplifier/SubstitutionMap.h +++ b/src/simplifier/SubstitutionMap.h @@ -122,9 +122,14 @@ public: ASTNode applySubstitutionMap(const ASTNode& n); + ASTNode applySubstitutionMapUntilArrays(const ASTNode& n); + // Replace any nodes in "n" that exist in the fromTo map. // NB the fromTo map is changed. static ASTNode replace(const ASTNode& n, ASTNodeMap& fromTo, ASTNodeMap& cache, NodeFactory *nf); + + static ASTNode replace(const ASTNode& n, ASTNodeMap& fromTo, ASTNodeMap& cache, NodeFactory *nf, bool stopAtArrays); + }; } diff --git a/src/simplifier/bvsolver.cpp b/src/simplifier/bvsolver.cpp index 0b74b81..fa3d4cd 100644 --- a/src/simplifier/bvsolver.cpp +++ b/src/simplifier/bvsolver.cpp @@ -741,50 +741,44 @@ namespace BEEV Simplifying through arrays is very expensive though. I know how to fix it, but don't have time. Trev. */ - #if 1 - ASTNode aaa = - (any_solved - && EQ == it->GetKind()) ? - _simp->SimplifyFormula_TopLevel(*it, false) : - *it; - + ASTNode aaa = (any_solved && EQ == it->GetKind()) ? _simp->applySubstitutionMapUntilArrays(*it) : *it; #else + ASTNode aaa = *it; + if (any_solved && EQ == aaa.GetKind()) + { + bool found = false; - ASTNode aaa = *it; + ASTNodeSet var; + SetofVarsSeenInTerm(aaa[0], var); - if (any_solved && EQ == aaa.GetKind()) - { - bool done = false; - { - ASTNodeSet lhs; - SetofVarsSeenInTerm(aaa[0], lhs); - - for (ASTNodeSet::const_iterator it = lhs.begin(); it != lhs.end(); it++) - if (_simp->CheckSubstitutionMap(*it)) - { - aaa = _simp->applySubstitutionMap(aaa); - done = true; - break; - } + for (ASTNodeSet::const_iterator it = var.begin(); it != var.end(); it++) + if (_simp->CheckSubstitutionMap(*it)) + { + found = true; + break; } - if (!done) + + if (!found) { - ASTNodeSet rhs; - SetofVarsSeenInTerm(aaa[1], rhs); - - for (ASTNodeSet::const_iterator it = rhs.begin(); it != rhs.end(); it++) - if (_simp->CheckSubstitutionMap(*it)) - { - aaa = _simp->applySubstitutionMap(aaa); - done = true; - break; - } + var.clear(); + SetofVarsSeenInTerm(aaa[1], var); + + for (ASTNodeSet::const_iterator it = var.begin(); it != var.end(); it++) + if (_simp->CheckSubstitutionMap(*it)) + { + found = true; + break; + } } + if (found) + aaa = _simp->applySubstitutionMapUntilArrays(aaa); } + #endif + //_bm->ASTNodeStats("Printing after calling simplifyformula //inside the solver:", aaa); aaa = BVSolve_Odd(aaa); @@ -804,7 +798,9 @@ namespace BEEV } } if (ASTTrue == aaa) - any_solved=true; + { + any_solved=true; + } } ASTNode evens; @@ -833,6 +829,10 @@ namespace BEEV output = solveForAndOfXOR(output); + // Imagine in the last conjunct A is replaced by B. But there could + // be variable A's in the first conjunct. This gets rid of 'em. + output = _simp->applySubstitutionMapUntilArrays(output); + UpdateAlreadySolvedMap(_input, output); _bm->GetRunTimes()->stop(RunTimes::BVSolver); return output; diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp index 7f7f746..1e895c1 100644 --- a/src/simplifier/simplifier.cpp +++ b/src/simplifier/simplifier.cpp @@ -155,6 +155,12 @@ namespace BEEV return substitutionMap.applySubstitutionMap(n); } + ASTNode Simplifier::applySubstitutionMapUntilArrays(const ASTNode& n) + { + return substitutionMap.applySubstitutionMapUntilArrays(n); + } + + bool Simplifier::CheckSubstitutionMap(const ASTNode& key) { return substitutionMap.CheckSubstitutionMap(key); @@ -1719,7 +1725,7 @@ namespace BEEV else output = actualInputterm; - inputterm = output; + inputterm = output; } const ASTVec& children = inputterm.GetChildren(); @@ -2863,12 +2869,13 @@ namespace BEEV //memoize UpdateSimplifyMap(inputterm, output, false, VarConstMap); UpdateSimplifyMap(actualInputterm, output, false, VarConstMap); + //cerr << "SimplifyTerm: output" << output << endl; // CheckSimplifyInvariant(inputterm,output); - assert(!output.IsNull()); - assert(inputterm.GetValueWidth() == output.GetValueWidth()); - assert(inputterm.GetIndexWidth() == output.GetIndexWidth()); + assert(!output.IsNull()); + assert(inputterm.GetValueWidth() == output.GetValueWidth()); + assert(inputterm.GetIndexWidth() == output.GetIndexWidth()); return output; } //end of SimplifyTerm() diff --git a/src/simplifier/simplifier.h b/src/simplifier/simplifier.h index 5731f38..0970375 100644 --- a/src/simplifier/simplifier.h +++ b/src/simplifier/simplifier.h @@ -116,6 +116,7 @@ namespace BEEV bool UpdateSubstitutionMap(const ASTNode& e0, const ASTNode& e1); ASTNode applySubstitutionMap(const ASTNode& n); + ASTNode applySubstitutionMapUntilArrays(const ASTNode& n); void ResetSimplifyMaps(void); -- 2.47.3