From bf7c88a44096d7abd06f46ccf70cd892f527e5d2 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Sat, 18 Feb 2012 12:33:43 +0000 Subject: [PATCH] Improvement. Write the equivalences that the bit-blaster discovers through transitively. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1569 e59a4935-1847-0410-ae03-e826735625c1 --- src/STPManager/STP.cpp | 3 +- src/simplifier/SubstitutionMap.cpp | 102 ++++++----------------------- src/simplifier/SubstitutionMap.h | 3 +- 3 files changed, 21 insertions(+), 87 deletions(-) diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp index c0855e8..c803811 100644 --- a/src/STPManager/STP.cpp +++ b/src/STPManager/STP.cpp @@ -120,12 +120,11 @@ namespace BEEV { /* These nodes have equivalent AIG representations, so even though they have different * word level expressions they are identical semantically. So we pick one of the ASTnodes * and replace the others with it. - * TODO: Isn't applied transitively because it infinite loops. * TODO: I replace with the lower id node, sometimes though we replace with much more * difficult looking ASTNodes. */ ASTNodeMap cache; - simplified_solved_InputToSAT = SubstitutionMap::simple_replace(simplified_solved_InputToSAT, equivs, cache,&nf); + simplified_solved_InputToSAT = SubstitutionMap::replace(simplified_solved_InputToSAT, equivs, cache,&nf,false,true); bm->ASTNodeStats(bb_message.c_str(), simplified_solved_InputToSAT); } diff --git a/src/simplifier/SubstitutionMap.cpp b/src/simplifier/SubstitutionMap.cpp index 84e4b90..6d27bc9 100644 --- a/src/simplifier/SubstitutionMap.cpp +++ b/src/simplifier/SubstitutionMap.cpp @@ -62,13 +62,13 @@ ASTNode SubstitutionMap::applySubstitutionMap(const ASTNode& n) { bm->GetRunTimes()->start(RunTimes::ApplyingSubstitutions); ASTNodeMap cache; - ASTNode result = replace(n,*SolverMap,cache,nf, false); + ASTNode result = replace(n,*SolverMap,cache,nf, false,false); // NB. This is an expensive check. Remove it after it's been idempotent // for a while. #ifndef NDEBUG cache.clear(); - assert( result == replace(result,*SolverMap,cache,nf, false)); + assert( result == replace(result,*SolverMap,cache,nf, false,false)); #endif bm->GetRunTimes()->stop(RunTimes::ApplyingSubstitutions); @@ -80,7 +80,7 @@ ASTNode SubstitutionMap::applySubstitutionMapUntilArrays(const ASTNode& n) { bm->GetRunTimes()->start(RunTimes::ApplyingSubstitutions); ASTNodeMap cache; - ASTNode result = replace(n,*SolverMap,cache,nf, true); + ASTNode result = replace(n,*SolverMap,cache,nf, true,false); bm->GetRunTimes()->stop(RunTimes::ApplyingSubstitutions); return result; } @@ -88,7 +88,7 @@ ASTNode SubstitutionMap::applySubstitutionMapUntilArrays(const ASTNode& n) ASTNode SubstitutionMap::replace(const ASTNode& n, ASTNodeMap& fromTo, ASTNodeMap& cache, NodeFactory * nf) { - return replace(n,fromTo,cache,nf,false); + return replace(n,fromTo,cache,nf,false,false); } // NOTE the fromTo map is changed as we traverse downwards. @@ -101,7 +101,7 @@ ASTNode SubstitutionMap::replace(const ASTNode& n, ASTNodeMap& fromTo, // It's optimised for the symbol to something case. ASTNode SubstitutionMap::replace(const ASTNode& n, ASTNodeMap& fromTo, - ASTNodeMap& cache, NodeFactory * nf, bool stopAtArrays) + ASTNodeMap& cache, NodeFactory * nf, bool stopAtArrays , bool preventInfinite) { const Kind k = n.GetKind(); if (k == BVCONST || k == TRUE || k == FALSE) @@ -116,7 +116,7 @@ ASTNode SubstitutionMap::replace(const ASTNode& n, ASTNodeMap& fromTo, { const ASTNode& r = it->second; assert(r.GetIndexWidth() == n.GetIndexWidth()); - ASTNode replaced = replace(r, fromTo, cache,nf,stopAtArrays); + ASTNode replaced = replace(r, fromTo, cache,nf,stopAtArrays,preventInfinite); if (replaced != r) fromTo[n] = replaced; @@ -142,7 +142,7 @@ ASTNode SubstitutionMap::replace(const ASTNode& n, ASTNodeMap& fromTo, for (ASTVec::const_iterator it = children.begin(); it != children.end(); it++) { - new_children.push_back(replace(*it, fromTo, cache,nf,stopAtArrays)); + new_children.push_back(replace(*it, fromTo, cache,nf,stopAtArrays,preventInfinite)); } assert(new_children.size() == children.size()); @@ -175,11 +175,22 @@ ASTNode SubstitutionMap::replace(const ASTNode& n, ASTNodeMap& fromTo, // I hope that this makes it idempotent. if (fromTo.find(result) != fromTo.end()) - result = replace(result, fromTo, cache,nf,stopAtArrays); + { + // map n->result, if running replace() on result gives us 'n', it will not infinite loop. + // This is only currently required for the bitblast equivalence stuff. + if (preventInfinite) + cache.insert(make_pair(n,result)); + + result = replace(result, fromTo, cache,nf,stopAtArrays,preventInfinite); + } assert(result.GetValueWidth() == valueWidth); assert(result.GetIndexWidth() == indexWidth); + // If there is already an "n" element in the cache, the maps semantics are to ignore the next insertion. + if (preventInfinite) + cache.erase(n); + cache.insert(make_pair(n,result)); return result; } @@ -310,79 +321,4 @@ bool SubstitutionMap::loops(const ASTNode& n0, const ASTNode& n1) return (loops); } - -ASTNode -SubstitutionMap::simple_replace(const ASTNode& n, ASTNodeMap& fromTo, ASTNodeMap& cache, NodeFactory * nf) -{ - const Kind k = n.GetKind(); - if (k == BVCONST || k == TRUE || k == FALSE) - return n; - - ASTNodeMap::const_iterator it; - - if ((it = cache.find(n)) != cache.end()) - return it->second; - - if ((it = fromTo.find(n)) != fromTo.end()) - { - const ASTNode& r = it->second; - assert(r.GetIndexWidth() == n.GetIndexWidth()); - cache.insert(make_pair(n, r)); - return r; - } - - // These can't be created like regular nodes are - if (k == SYMBOL) - return n; - - const unsigned int indexWidth = n.GetIndexWidth(); - - const ASTVec& children = n.GetChildren(); - assert(children.size() > 0); - // Should have no leaves left here. - - ASTVec new_children; - new_children.reserve(children.size()); - - for (ASTVec::const_iterator it = children.begin(); it != children.end(); it++) - { - new_children.push_back(simple_replace(*it, fromTo, cache, nf)); - } - - assert(new_children.size() == children.size()); - - // This code short-cuts if the children are the same. Nodes with the same children, - // won't have necessarily given the same node if the simplifyingNodeFactory is enabled - // now, but wasn't enabled when the node was created. Shortcutting saves lots of time. - if (new_children == children) - { - cache.insert(make_pair(n, n)); - return n; - } - - ASTNode result; - const unsigned int valueWidth = n.GetValueWidth(); - - if (valueWidth == 0) // n.GetType() == BOOLEAN_TYPE - { - result = nf->CreateNode(k, new_children); - } - else - { - // If the index and value width aren't saved, they are reset sometimes (??) - result = nf->CreateArrayTerm(k, indexWidth, valueWidth, new_children); - } - - // We may have created something that should be mapped. For instance, - // if n is READ(A, x), and the fromTo is: {x==0, READ(A,0) == 1}, then - // by here the result will be READ(A,0). Which needs to be mapped again.. - // I hope that this makes it idempotent. - - assert(result.GetValueWidth() == valueWidth); - assert(result.GetIndexWidth() == indexWidth); - - cache.insert(make_pair(n, result)); - return result; -} - }; diff --git a/src/simplifier/SubstitutionMap.h b/src/simplifier/SubstitutionMap.h index 08138d3..60b08f2 100644 --- a/src/simplifier/SubstitutionMap.h +++ b/src/simplifier/SubstitutionMap.h @@ -201,9 +201,8 @@ public: // Replace any nodes in "n" that exist in the fromTo map. // NB the fromTo map is changed. - static ASTNode simple_replace(const ASTNode& n, ASTNodeMap& fromTo, ASTNodeMap& cache, NodeFactory *nf); 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); + static ASTNode replace(const ASTNode& n, ASTNodeMap& fromTo, ASTNodeMap& cache, NodeFactory *nf, bool stopAtArrays, bool preventInfiniteLoops); }; -- 2.47.3