From c40b9f97098d41f0007a53de616147b21d3216df Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Fri, 3 Feb 2012 03:41:30 +0000 Subject: [PATCH] Improvement. Use the results of bit-blasting to detect equivalent predicates. Currently disabled by default until I finish testing. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1552 e59a4935-1847-0410-ae03-e826735625c1 --- src/STPManager/STP.cpp | 20 +++++++- src/simplifier/SubstitutionMap.cpp | 74 ++++++++++++++++++++++++++++++ src/simplifier/SubstitutionMap.h | 1 + src/simplifier/simplifier.cpp | 9 +++- src/to-sat/AIG/BBNodeAIG.h | 8 +++- src/to-sat/BitBlaster.cpp | 37 ++++++++++++++- src/to-sat/BitBlaster.h | 2 +- 7 files changed, 145 insertions(+), 6 deletions(-) diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp index 142f593..e14d99e 100644 --- a/src/STPManager/STP.cpp +++ b/src/STPManager/STP.cpp @@ -112,11 +112,27 @@ namespace BEEV { SimplifyingNodeFactory nf(*(bm->hashingNodeFactory), *bm); BitBlaster bb(&bbnm, simp, &nf , &(bm->UserFlags)); ASTNodeMap fromTo; - bb.getConsts(simplified_solved_InputToSAT, fromTo); + ASTNodeMap equivs; + bb.getConsts(simplified_solved_InputToSAT, fromTo,equivs); + if (equivs.size() > 0) + { + /* 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: Currently only for booleans, + * 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, fromTo, cache,&nf); + bm->ASTNodeStats(bb_message.c_str(), simplified_solved_InputToSAT); + } + if (fromTo.size() > 0) { ASTNodeMap cache; - simplified_solved_InputToSAT = SubstitutionMap::replace(simplified_solved_InputToSAT, fromTo, cache,&nf); + simplified_solved_InputToSAT = SubstitutionMap:: replace(simplified_solved_InputToSAT, fromTo, cache,&nf); bm->ASTNodeStats(bb_message.c_str(), simplified_solved_InputToSAT); } actualBBSize = bbnm.totalNumberOfNodes(); diff --git a/src/simplifier/SubstitutionMap.cpp b/src/simplifier/SubstitutionMap.cpp index a726ca2..84e4b90 100644 --- a/src/simplifier/SubstitutionMap.cpp +++ b/src/simplifier/SubstitutionMap.cpp @@ -311,4 +311,78 @@ 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 08bb9d0..08138d3 100644 --- a/src/simplifier/SubstitutionMap.h +++ b/src/simplifier/SubstitutionMap.h @@ -201,6 +201,7 @@ 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); diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp index 1afbb20..5edf37f 100644 --- a/src/simplifier/simplifier.cpp +++ b/src/simplifier/simplifier.cpp @@ -213,7 +213,14 @@ namespace BEEV void Simplifier::UpdateAlwaysTrueFormSet(const ASTNode& key) { - AlwaysTrueHashSet.insert(key.GetNodeNum()); + // The always true/ always false relies on the top level constraint not being removed. + // however with bb equivalence checking, AIGs can figure out that the outer constraint + // is unncessary because it's enforced by the implicit constraint---removing it. That + // leaves just one instance of the constraint, so it we replace it with true/false + // the constraint is lost. This is subsumed by constant bit propagation, so I suspect + // it's not a big loss. + if (!_bm->UserFlags.isSet("bb-equiv","0")) + AlwaysTrueHashSet.insert(key.GetNodeNum()); } ASTNode diff --git a/src/to-sat/AIG/BBNodeAIG.h b/src/to-sat/AIG/BBNodeAIG.h index a00208f..846ebb5 100644 --- a/src/to-sat/AIG/BBNodeAIG.h +++ b/src/to-sat/AIG/BBNodeAIG.h @@ -57,6 +57,12 @@ namespace BEEV print(c1); } public: + + intptr_t GetNodeNum() const + { + return (intptr_t)n; + } + // If the pointer is odd. Then it's the NOT of the pointer one less. Aig_Obj_t * n; @@ -90,7 +96,7 @@ public: bool operator==(const BBNodeAIG &other) const { - return n == other.n; + return n == other.n; } bool operator!=(const BBNodeAIG &other) const diff --git a/src/to-sat/BitBlaster.cpp b/src/to-sat/BitBlaster.cpp index c056ce3..c5cbd18 100644 --- a/src/to-sat/BitBlaster.cpp +++ b/src/to-sat/BitBlaster.cpp @@ -58,7 +58,7 @@ namespace BEEV // Look through the maps to see what the bitblaster has discovered (if anything) is constant. template void - BitBlaster::getConsts(const ASTNode& form, ASTNodeMap& fromTo) + BitBlaster::getConsts(const ASTNode& form, ASTNodeMap& fromTo, ASTNodeMap& equivs) { assert(form.GetType() == BOOLEAN_TYPE); @@ -132,6 +132,41 @@ namespace BEEV fromTo.insert(make_pair(n, r)); } + + if (form.GetSTPMgr()->UserFlags.isSet("bb-equiv","0")) + { + HASHMAP nodeToFn; + typename map::iterator it; + for (it = BBFormMemo.begin(); it != BBFormMemo.end(); it++) + { + const ASTNode& n = it->first; + if (n.isConstant()) + continue; + + const BBNode& x = it->second; + if (x == BBTrue || x == BBFalse) + continue; + + if (nodeToFn.find(x.GetNodeNum()) == nodeToFn.end()) + { + nodeToFn.insert(make_pair(x.GetNodeNum(),n)); + } + else + { + const ASTNode other = (nodeToFn.find(x.GetNodeNum()))->second; + std::pair p; + if (other.GetNodeNum() > n.GetNodeNum()) + p = make_pair(other,n); + else + p = make_pair(n,other); + + equivs.insert(p); + //std::cerr << "from" << p.first << " to" << p.second; + //ASTNode equals = ASTNF->CreateNode(NOT,ASTNF->CreateNode(EQ,p.first,p.second)); + //printer::SMTLIB2_PrintBack(std::cerr,p.second); + } + } + } } template diff --git a/src/to-sat/BitBlaster.h b/src/to-sat/BitBlaster.h index 30fdc77..9113f77 100644 --- a/src/to-sat/BitBlaster.h +++ b/src/to-sat/BitBlaster.h @@ -292,7 +292,7 @@ namespace BEEV BBForm(const ASTNode& form); void - getConsts(const ASTNode& n, ASTNodeMap& fromTo); + getConsts(const ASTNode& n, ASTNodeMap& fromTo, ASTNodeMap& equivs); }; //end of class BitBlaster -- 2.47.3