diff options
author | Tim King <taking@google.com> | 2016-03-24 15:06:24 -0700 |
---|---|---|
committer | Tim King <taking@google.com> | 2016-03-24 15:06:24 -0700 |
commit | 9c00e3484d1f0ca6b2f10e549b24f717c402cd9f (patch) | |
tree | 56e1160b02ca334a691cd47498ccba4f6e0b321f /src/theory/ite_utilities.cpp | |
parent | df2781c86c2c546e72a8f6204c98e59387229420 (diff) |
Fixing a garbage collection issue in simplifyWithCare(). Bug 729.
Diffstat (limited to 'src/theory/ite_utilities.cpp')
-rw-r--r-- | src/theory/ite_utilities.cpp | 229 |
1 files changed, 128 insertions, 101 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<bool>(true); d_false = NodeManager::currentNM()->mkConst<bool>(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<Node>& css = cs.getCareSet(); - queue.erase(v); - - done = false; - set<Node>::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<Node>& css = cs.getCareSet(); + queue.erase(v); + + done = false; + set<Node>::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 */ |