From: trevor_hansen Date: Thu, 5 Aug 2010 15:17:31 +0000 (+0000) Subject: Speedup the bvsolver. Use the applySubstitutionMap function to apply the discovered... X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=2556f7c211e1acd71ec913718e062e857c5550c3;p=francis%2Fstp.git 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 --- 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);