From df2781c86c2c546e72a8f6204c98e59387229420 Mon Sep 17 00:00:00 2001 From: Tim King Date: Thu, 24 Mar 2016 14:58:13 -0700 Subject: Deleting allocated NodeVecs in ITESimplifier. --- src/theory/ite_utilities.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/theory/ite_utilities.cpp b/src/theory/ite_utilities.cpp index 2791a9555..e5c56a2a4 100644 --- a/src/theory/ite_utilities.cpp +++ b/src/theory/ite_utilities.cpp @@ -657,6 +657,7 @@ ITESimplifier::NodeVec* ITESimplifier::computeConstantLeaves(TNode ite){ // special case 2 constant children if(thenB.isConst() && elseB.isConst()){ NodeVec* pair = new NodeVec(2); + d_allocatedConstantLeaves.push_back(pair); (*pair)[0] = std::min(thenB, elseB); (*pair)[1] = std::max(thenB, elseB); d_constantLeaves[ite] = pair; @@ -694,6 +695,7 @@ ITESimplifier::NodeVec* ITESimplifier::computeConstantLeaves(TNode ite){ } NodeVec* both = new NodeVec(defChildren->size()+maybeChildren->size()); + d_allocatedConstantLeaves.push_back(both); NodeVec::iterator newEnd; newEnd = std::set_union(defChildren->begin(), defChildren->end(), maybeChildren->begin(), maybeChildren->end(), -- cgit v1.2.3 From 9c00e3484d1f0ca6b2f10e549b24f717c402cd9f Mon Sep 17 00:00:00 2001 From: Tim King Date: Thu, 24 Mar 2016 15:06:24 -0700 Subject: Fixing a garbage collection issue in simplifyWithCare(). Bug 729. --- src/theory/ite_utilities.cpp | 229 ++++++++++++++++++++++++------------------- src/theory/ite_utilities.h | 29 ++++-- 2 files changed, 148 insertions(+), 110 deletions(-) diff --git a/src/theory/ite_utilities.cpp b/src/theory/ite_utilities.cpp index e5c56a2a4..3ae9bc019 100644 --- a/src/theory/ite_utilities.cpp +++ b/src/theory/ite_utilities.cpp @@ -658,6 +658,7 @@ ITESimplifier::NodeVec* ITESimplifier::computeConstantLeaves(TNode ite){ if(thenB.isConst() && elseB.isConst()){ NodeVec* pair = new NodeVec(2); d_allocatedConstantLeaves.push_back(pair); + (*pair)[0] = std::min(thenB, elseB); (*pair)[1] = std::max(thenB, elseB); d_constantLeaves[ite] = pair; @@ -1401,25 +1402,32 @@ Node ITESimplifier::simpITE(TNode assertion) } ITECareSimplifier::ITECareSimplifier() - : d_usedSets() + : d_careSetsOutstanding(0) + , d_usedSets() { d_true = NodeManager::currentNM()->mkConst(true); d_false = NodeManager::currentNM()->mkConst(false); } -ITECareSimplifier::~ITECareSimplifier(){} +ITECareSimplifier::~ITECareSimplifier(){ + Assert(d_usedSets.empty()); + Assert(d_careSetsOutstanding == 0); +} void ITECareSimplifier::clear(){ - d_usedSets.clear(); + Assert(d_usedSets.empty()); + Assert(d_careSetsOutstanding == 0); } ITECareSimplifier::CareSetPtr ITECareSimplifier::getNewSet() { if (d_usedSets.empty()) { + d_careSetsOutstanding++; return ITECareSimplifier::CareSetPtr::mkNew(*this); } else { - ITECareSimplifier::CareSetPtr cs = ITECareSimplifier::CareSetPtr::recycle(d_usedSets.back()); + ITECareSimplifier::CareSetPtr cs = + ITECareSimplifier::CareSetPtr::recycle(d_usedSets.back()); cs.getCareSet().clear(); d_usedSets.pop_back(); return cs; @@ -1490,125 +1498,144 @@ Node ITECareSimplifier::substitute(TNode e, TNodeMap& substTable, TNodeMap& cach Node ITECareSimplifier::simplifyWithCare(TNode e) { TNodeMap substTable; - CareMap queue; - CareMap::iterator it; - ITECareSimplifier::CareSetPtr cs = getNewSet(); - ITECareSimplifier::CareSetPtr cs2; - queue[e] = cs; - - TNode v; - bool done; - unsigned i; - - while (!queue.empty()) { - it = queue.end(); - --it; - v = it->first; - cs = it->second; - set& css = cs.getCareSet(); - queue.erase(v); - - done = false; - set::iterator iCare, iCareEnd = css.end(); - - switch (v.getKind()) { - case kind::ITE: { - iCare = css.find(v[0]); - if (iCare != iCareEnd) { - Assert(substTable.find(v) == substTable.end()); - substTable[v] = v[1]; - updateQueue(queue, v[1], cs); - done = true; - break; - } - else { - iCare = css.find(v[0].negate()); + + /* This extra block is to trigger the destructors for cs and cs2 + * before starting garbage collection. + */ + { + CareMap queue; + CareMap::iterator it; + ITECareSimplifier::CareSetPtr cs = getNewSet(); + ITECareSimplifier::CareSetPtr cs2; + queue[e] = cs; + + TNode v; + bool done; + unsigned i; + + while (!queue.empty()) { + it = queue.end(); + --it; + v = it->first; + cs = it->second; + set& css = cs.getCareSet(); + queue.erase(v); + + done = false; + set::iterator iCare, iCareEnd = css.end(); + + switch (v.getKind()) { + case kind::ITE: { + iCare = css.find(v[0]); if (iCare != iCareEnd) { Assert(substTable.find(v) == substTable.end()); - substTable[v] = v[2]; - updateQueue(queue, v[2], cs); + substTable[v] = v[1]; + updateQueue(queue, v[1], cs); done = true; break; } - } - updateQueue(queue, v[0], cs); - cs2 = getNewSet(); - cs2.getCareSet() = css; - cs2.getCareSet().insert(v[0]); - updateQueue(queue, v[1], cs2); - cs2 = getNewSet(); - cs2.getCareSet() = css; - cs2.getCareSet().insert(v[0].negate()); - updateQueue(queue, v[2], cs2); - done = true; - break; - } - case kind::AND: { - for (i = 0; i < v.getNumChildren(); ++i) { - iCare = css.find(v[i].negate()); - if (iCare != iCareEnd) { - Assert(substTable.find(v) == substTable.end()); - substTable[v] = d_false; - done = true; - break; + else { + iCare = css.find(v[0].negate()); + if (iCare != iCareEnd) { + Assert(substTable.find(v) == substTable.end()); + substTable[v] = v[2]; + updateQueue(queue, v[2], cs); + done = true; + break; + } } + updateQueue(queue, v[0], cs); + cs2 = getNewSet(); + cs2.getCareSet() = css; + cs2.getCareSet().insert(v[0]); + updateQueue(queue, v[1], cs2); + cs2 = getNewSet(); + cs2.getCareSet() = css; + cs2.getCareSet().insert(v[0].negate()); + updateQueue(queue, v[2], cs2); + done = true; + break; } - if (done) break; - - Assert(v.getNumChildren() > 1); - updateQueue(queue, v[0], cs); - cs2 = getNewSet(); - cs2.getCareSet() = css; - cs2.getCareSet().insert(v[0]); - for (i = 1; i < v.getNumChildren(); ++i) { - updateQueue(queue, v[i], cs2); - } - done = true; - break; - } - case kind::OR: { - for (i = 0; i < v.getNumChildren(); ++i) { - iCare = css.find(v[i]); - if (iCare != iCareEnd) { - Assert(substTable.find(v) == substTable.end()); - substTable[v] = d_true; - done = true; - break; + case kind::AND: { + for (i = 0; i < v.getNumChildren(); ++i) { + iCare = css.find(v[i].negate()); + if (iCare != iCareEnd) { + Assert(substTable.find(v) == substTable.end()); + substTable[v] = d_false; + done = true; + break; + } + } + if (done) break; + + Assert(v.getNumChildren() > 1); + updateQueue(queue, v[0], cs); + cs2 = getNewSet(); + cs2.getCareSet() = css; + cs2.getCareSet().insert(v[0]); + for (i = 1; i < v.getNumChildren(); ++i) { + updateQueue(queue, v[i], cs2); } + done = true; + break; } - if (done) break; - - Assert(v.getNumChildren() > 1); - updateQueue(queue, v[0], cs); - cs2 = getNewSet(); - cs2.getCareSet() = css; - cs2.getCareSet().insert(v[0].negate()); - for (i = 1; i < v.getNumChildren(); ++i) { - updateQueue(queue, v[i], cs2); + case kind::OR: { + for (i = 0; i < v.getNumChildren(); ++i) { + iCare = css.find(v[i]); + if (iCare != iCareEnd) { + Assert(substTable.find(v) == substTable.end()); + substTable[v] = d_true; + done = true; + break; + } + } + if (done) break; + + Assert(v.getNumChildren() > 1); + updateQueue(queue, v[0], cs); + cs2 = getNewSet(); + cs2.getCareSet() = css; + cs2.getCareSet().insert(v[0].negate()); + for (i = 1; i < v.getNumChildren(); ++i) { + updateQueue(queue, v[i], cs2); + } + done = true; + break; } - done = true; - break; + default: + break; } - default: - break; - } - if (done) { - continue; - } + if (done) { + continue; + } - for (unsigned i = 0; i < v.getNumChildren(); ++i) { - updateQueue(queue, v[i], cs); + for (unsigned i = 0; i < v.getNumChildren(); ++i) { + updateQueue(queue, v[i], cs); + } } } + /* Perform garbage collection. */ while (!d_usedSets.empty()) { - delete d_usedSets.back(); + CareSetPtrVal* used = d_usedSets.back(); d_usedSets.pop_back(); + Assert(used->safeToGarbageCollect()); + delete used; + Assert(d_careSetsOutstanding > 0); + d_careSetsOutstanding--; } TNodeMap cache; return substitute(e, substTable, cache); } +ITECareSimplifier::CareSetPtr ITECareSimplifier::CareSetPtr::mkNew( + ITECareSimplifier& simp) { + CareSetPtrVal* val = new CareSetPtrVal(simp); + return CareSetPtr(val); +} + + + } /* namespace theory */ } /* namespace CVC4 */ diff --git a/src/theory/ite_utilities.h b/src/theory/ite_utilities.h index 10fe2853b..3c78a8790 100644 --- a/src/theory/ite_utilities.h +++ b/src/theory/ite_utilities.h @@ -133,7 +133,7 @@ public: private: typedef std::hash_map NodeCountMap; NodeCountMap d_termITEHeight; -}; +}; /* class TermITEHeightCounter */ /** * A routine designed to undo the potentially large blow up @@ -177,7 +177,7 @@ private: ~Statistics(); }; Statistics d_statistics; -}; +}; /* class ITECompressor */ class ITESimplifier { public: @@ -302,6 +302,15 @@ public: void clear(); private: + + /** + * This should always equal the number of care sets allocated by + * this object - the number of these that have been deleted. This is + * initially 0 and should always be 0 at the *start* of + * ~ITECareSimplifier(). + */ + unsigned d_careSetsOutstanding; + Node d_true; Node d_false; @@ -309,12 +318,16 @@ private: class CareSetPtr; class CareSetPtrVal { + public: + bool safeToGarbageCollect() const { return d_refCount == 0; } + private: friend class ITECareSimplifier::CareSetPtr; ITECareSimplifier& d_iteSimplifier; unsigned d_refCount; std::set d_careSet; - CareSetPtrVal(ITECareSimplifier& simp) : d_iteSimplifier(simp), d_refCount(1) {} - }; + CareSetPtrVal(ITECareSimplifier& simp) + : d_iteSimplifier(simp), d_refCount(1) {} + }; /* class ITECareSimplifier::CareSetPtrVal */ std::vector d_usedSets; void careSetPtrGC(CareSetPtrVal* val) { @@ -350,16 +363,14 @@ private: return *this; } std::set& getCareSet() { return d_val->d_careSet; } - static CareSetPtr mkNew(ITECareSimplifier& simp) { - CareSetPtrVal* val = new CareSetPtrVal(simp); - return CareSetPtr(val); - } + + static CareSetPtr mkNew(ITECareSimplifier& simp); static CareSetPtr recycle(CareSetPtrVal* val) { Assert(val != NULL && val->d_refCount == 0); val->d_refCount = 1; return CareSetPtr(val); } - }; + }; /* class ITECareSimplifier::CareSetPtr */ CareSetPtr getNewSet(); -- cgit v1.2.3