From 0906304d7b8ac3726318645b6a2bd042f233c0f4 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Fri, 26 May 2017 01:20:55 -0700 Subject: Fix EqProof memory management --- src/proof/arith_proof.cpp | 94 +++++++-------- src/proof/array_proof.cpp | 147 +++++++++++------------ src/proof/proof_output_channel.cpp | 6 + src/proof/proof_output_channel.h | 4 +- src/proof/sat_proof_implementation.h | 17 ++- src/proof/uf_proof.cpp | 103 ++++++++-------- src/proof/uf_proof.h | 2 + src/theory/arrays/array_proof_reconstruction.cpp | 49 ++++---- src/theory/uf/equality_engine.cpp | 57 +++++---- src/theory/uf/equality_engine.h | 52 +++++++- 10 files changed, 295 insertions(+), 236 deletions(-) diff --git a/src/proof/arith_proof.cpp b/src/proof/arith_proof.cpp index 0f0c14eb2..feee738eb 100644 --- a/src/proof/arith_proof.cpp +++ b/src/proof/arith_proof.cpp @@ -88,7 +88,7 @@ Node ProofArith::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq if(tb == 0) { Assert(pf->d_id == theory::eq::MERGED_THROUGH_TRANS); Assert(!pf->d_node.isNull()); - Assert(pf->d_children.size() >= 2); + Assert(pf->num_children() >= 2); int neg = -1; theory::eq::EqProof subTrans; @@ -96,16 +96,16 @@ Node ProofArith::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq subTrans.d_node = pf->d_node; size_t i = 0; - while (i < pf->d_children.size()) { + while (i < pf->num_children()) { // Look for the negative clause, with which we will form a contradiction. - if(!pf->d_children[i]->d_node.isNull() && pf->d_children[i]->d_node.getKind() == kind::NOT) { + if(!pf->get_child(i)->d_node.isNull() && pf->get_child(i)->d_node.getKind() == kind::NOT) { Assert(neg < 0); neg = i; ++i; } // Handle congruence closures over equalities. - else if (pf->d_children[i]->d_id==theory::eq::MERGED_THROUGH_CONGRUENCE && pf->d_children[i]->d_node.isNull()) { + else if (pf->get_child(i)->d_id==theory::eq::MERGED_THROUGH_CONGRUENCE && pf->get_child(i)->d_node.isNull()) { Debug("pf::arith") << "Handling congruence over equalities" << std::endl; // Gather the sequence of consecutive congruence closures. @@ -113,13 +113,13 @@ Node ProofArith::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq unsigned count; Debug("pf::arith") << "Collecting congruence sequence" << std::endl; for (count = 0; - i + count < pf->d_children.size() && - pf->d_children[i + count]->d_id==theory::eq::MERGED_THROUGH_CONGRUENCE && - pf->d_children[i + count]->d_node.isNull(); + i + count < pf->num_children() && + pf->get_child(i + count)->d_id==theory::eq::MERGED_THROUGH_CONGRUENCE && + pf->get_child(i + count)->d_node.isNull(); ++count) { Debug("pf::arith") << "Found a congruence: " << std::endl; - pf->d_children[i+count]->debug_print("pf::arith"); - congruenceClosures.push_back(pf->d_children[i+count]); + pf->get_child(i+count)->debug_print("pf::arith"); + congruenceClosures.push_back(pf->get_child(i+count)); } Debug("pf::arith") << "Total number of congruences found: " << congruenceClosures.size() << std::endl; @@ -133,9 +133,9 @@ Node ProofArith::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq targetAppearsBefore = false; } - if ((i + count >= pf->d_children.size()) || - (!pf->d_children[i + count]->d_node.isNull() && - pf->d_children[i + count]->d_node.getKind() == kind::NOT)) { + if ((i + count >= pf->num_children()) || + (!pf->get_child(i + count)->d_node.isNull() && + pf->get_child(i + count)->d_node.getKind() == kind::NOT)) { Debug("pf::arith") << "Target does not appear after" << std::endl; targetAppearsAfter = false; } @@ -149,32 +149,32 @@ Node ProofArith::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq // Insert target clause first. if (targetAppearsBefore) { - orderedEqualities.push_back(pf->d_children[i - 1]); + orderedEqualities.push_back(pf->get_child(i - 1)); // The target has already been added to subTrans; remove it. - subTrans.d_children.pop_back(); + subTrans.remove_last_child(); } else { - orderedEqualities.push_back(pf->d_children[i + count]); + orderedEqualities.push_back(pf->get_child(i + count)); } // Start with the congruence closure closest to the target clause, and work our way back/forward. if (targetAppearsBefore) { for (unsigned j = 0; j < count; ++j) { - if (pf->d_children[i + j]->d_children[0]->d_id != theory::eq::MERGED_THROUGH_REFLEXIVITY) - orderedEqualities.insert(orderedEqualities.begin(), pf->d_children[i + j]->d_children[0]); - if (pf->d_children[i + j]->d_children[1]->d_id != theory::eq::MERGED_THROUGH_REFLEXIVITY) - orderedEqualities.insert(orderedEqualities.end(), pf->d_children[i + j]->d_children[1]); + if (pf->get_child(i + j)->get_child(0)->d_id != theory::eq::MERGED_THROUGH_REFLEXIVITY) + orderedEqualities.insert(orderedEqualities.begin(), pf->get_child(i + j)->get_child(0)); + if (pf->get_child(i + j)->get_child(1)->d_id != theory::eq::MERGED_THROUGH_REFLEXIVITY) + orderedEqualities.insert(orderedEqualities.end(), pf->get_child(i + j)->get_child(1)); } } else { for (unsigned j = 0; j < count; ++j) { - if (pf->d_children[i + count - 1 - j]->d_children[0]->d_id != theory::eq::MERGED_THROUGH_REFLEXIVITY) - orderedEqualities.insert(orderedEqualities.begin(), pf->d_children[i + count - 1 - j]->d_children[0]); - if (pf->d_children[i + count - 1 - j]->d_children[1]->d_id != theory::eq::MERGED_THROUGH_REFLEXIVITY) - orderedEqualities.insert(orderedEqualities.end(), pf->d_children[i + count - 1 - j]->d_children[1]); + if (pf->get_child(i + count - 1 - j)->get_child(0)->d_id != theory::eq::MERGED_THROUGH_REFLEXIVITY) + orderedEqualities.insert(orderedEqualities.begin(), pf->get_child(i + count - 1 - j)->get_child(0)); + if (pf->get_child(i + count - 1 - j)->get_child(1)->d_id != theory::eq::MERGED_THROUGH_REFLEXIVITY) + orderedEqualities.insert(orderedEqualities.end(), pf->get_child(i + count - 1 - j)->get_child(1)); } } // Copy the result into the main transitivity proof. - subTrans.d_children.insert(subTrans.d_children.end(), orderedEqualities.begin(), orderedEqualities.end()); + subTrans.add_children(orderedEqualities); // Increase i to skip over the children that have been processed. i += count; @@ -185,7 +185,7 @@ Node ProofArith::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq // Else, just copy the child proof as is else { - subTrans.d_children.push_back(pf->d_children[i]); + subTrans.add_child(pf->get_child(i)); ++i; } } @@ -193,16 +193,16 @@ Node ProofArith::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq Node n1; std::stringstream ss; - //Assert(subTrans.d_children.size() == pf->d_children.size() - 1); - Debug("pf::arith") << "\nsubtrans has " << subTrans.d_children.size() << " children\n"; - if(pf->d_children.size() > 2) { + //Assert(subTrans.num_children() == pf->num_children() - 1); + Debug("pf::arith") << "\nsubtrans has " << subTrans.num_children() << " children\n"; + if(pf->num_children() > 2) { n1 = toStreamRecLFSC(ss, tp, &subTrans, 1, map); } else { - n1 = toStreamRecLFSC(ss, tp, subTrans.d_children[0], 1, map); - Debug("pf::arith") << "\nsubTrans unique child " << subTrans.d_children[0]->d_id << " was proven\ngot: " << n1 << std::endl; + n1 = toStreamRecLFSC(ss, tp, subTrans.get_child(0), 1, map); + Debug("pf::arith") << "\nsubTrans unique child " << subTrans.get_child(0)->d_id << " was proven\ngot: " << n1 << std::endl; } - Node n2 = pf->d_children[neg]->d_node; + Node n2 = pf->get_child(neg)->d_node; Assert(n2.getKind() == kind::NOT); out << "(clausify_false (contra _ "; Debug("pf::arith") << "\nhave proven: " << n1 << std::endl; @@ -233,22 +233,22 @@ Node ProofArith::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq Debug("pf::arith") << "\nok, looking at congruence:\n"; pf->debug_print("pf::arith"); std::stack stk; - for(const theory::eq::EqProof* pf2 = pf; pf2->d_id == theory::eq::MERGED_THROUGH_CONGRUENCE; pf2 = pf2->d_children[0]) { + for(const theory::eq::EqProof* pf2 = pf; pf2->d_id == theory::eq::MERGED_THROUGH_CONGRUENCE; pf2 = pf2->get_child(0)) { Assert(!pf2->d_node.isNull()); Assert(pf2->d_node.getKind() == kind::PARTIAL_APPLY_UF || pf2->d_node.getKind() == kind::BUILTIN || pf2->d_node.getKind() == kind::APPLY_UF || pf2->d_node.getKind() == kind::SELECT || pf2->d_node.getKind() == kind::STORE); - Assert(pf2->d_children.size() == 2); + Assert(pf2->num_children() == 2); out << "(cong _ _ _ _ _ _ "; stk.push(pf2); } - Assert(stk.top()->d_children[0]->d_id != theory::eq::MERGED_THROUGH_CONGRUENCE); + Assert(stk.top()->get_child(0)->d_id != theory::eq::MERGED_THROUGH_CONGRUENCE); NodeBuilder<> b1(kind::PARTIAL_APPLY_UF), b2(kind::PARTIAL_APPLY_UF); const theory::eq::EqProof* pf2 = stk.top(); stk.pop(); Assert(pf2->d_id == theory::eq::MERGED_THROUGH_CONGRUENCE); - Node n1 = toStreamRecLFSC(out, tp, pf2->d_children[0], tb + 1, map); + Node n1 = toStreamRecLFSC(out, tp, pf2->get_child(0), tb + 1, map); out << " "; std::stringstream ss; - Node n2 = toStreamRecLFSC(ss, tp, pf2->d_children[1], tb + 1, map); + Node n2 = toStreamRecLFSC(ss, tp, pf2->get_child(1), tb + 1, map); Debug("pf::arith") << "\nok, in FIRST cong[" << stk.size() << "]" << "\n"; pf2->debug_print("pf::arith"); Debug("pf::arith") << "looking at " << pf2->d_node << "\n"; @@ -266,7 +266,7 @@ Node ProofArith::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq //} if(!match(pf2->d_node, n1[1])) { Debug("pf::arith") << "IN BAD CASE, our first subproof is\n"; - pf2->d_children[0]->debug_print("pf::arith"); + pf2->get_child(0)->debug_print("pf::arith"); } Assert(match(pf2->d_node, n1[1])); side = 1; @@ -316,7 +316,7 @@ Node ProofArith::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq Assert(pf2->d_id == theory::eq::MERGED_THROUGH_CONGRUENCE); out << " "; ss.str(""); - n2 = toStreamRecLFSC(ss, tp, pf2->d_children[1], tb + 1, map); + n2 = toStreamRecLFSC(ss, tp, pf2->get_child(1), tb + 1, map); Debug("pf::arith") << "\nok, in cong[" << stk.size() << "]" << "\n"; Debug("pf::arith") << "looking at " << pf2->d_node << "\n"; Debug("pf::arith") << " " << n1 << "\n"; @@ -374,7 +374,7 @@ Node ProofArith::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq case theory::eq::MERGED_THROUGH_REFLEXIVITY: Assert(!pf->d_node.isNull()); - Assert(pf->d_children.empty()); + Assert(pf->num_children() == 0); out << "(refl _ "; tp->printTerm(NodeManager::currentNM()->toExpr(pf->d_node), out, map); out << ")"; @@ -382,18 +382,18 @@ Node ProofArith::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq case theory::eq::MERGED_THROUGH_EQUALITY: Assert(!pf->d_node.isNull()); - Assert(pf->d_children.empty()); + Assert(pf->num_children() == 0); out << ProofManager::getLitName(pf->d_node.negate()); return pf->d_node; case theory::eq::MERGED_THROUGH_TRANS: { Assert(!pf->d_node.isNull()); - Assert(pf->d_children.size() >= 2); + Assert(pf->num_children() >= 2); std::stringstream ss; Debug("pf::arith") << "\ndoing trans proof[[\n"; pf->debug_print("pf::arith"); Debug("pf::arith") << "\n"; - Node n1 = toStreamRecLFSC(ss, tp, pf->d_children[0], tb + 1, map); + Node n1 = toStreamRecLFSC(ss, tp, pf->get_child(0), tb + 1, map); Debug("pf::arith") << "\ndoing trans proof, got n1 " << n1 << "\n"; if(tb == 1) { Debug("pf::arith") << "\ntrans proof[0], got n1 " << n1 << "\n"; @@ -405,7 +405,7 @@ Node ProofArith::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq std::map childToStream; - for(size_t i = 1; i < pf->d_children.size(); ++i) { + for(size_t i = 1; i < pf->num_children(); ++i) { std::stringstream ss1(ss.str()), ss2; ss.str(""); @@ -415,7 +415,7 @@ Node ProofArith::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq if (childToStream.find(i) != childToStream.end()) n2 = childToStream[i]; else { - n2 = toStreamRecLFSC(ss2, tp, pf->d_children[i], tb + 1, map); + n2 = toStreamRecLFSC(ss2, tp, pf->get_child(i), tb + 1, map); childToStream[i] = n2; } @@ -446,9 +446,9 @@ Node ProofArith::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq bool sequenceOver = false; size_t j = i + 1; - while (j < pf->d_children.size() && !sequenceOver) { + while (j < pf->num_children() && !sequenceOver) { std::stringstream dontCare; - nodeAfterEqualitySequence = toStreamRecLFSC(dontCare, tp, pf->d_children[j], tb + 1, map ); + nodeAfterEqualitySequence = toStreamRecLFSC(dontCare, tp, pf->get_child(j), tb + 1, map ); if (((nodeAfterEqualitySequence[0] == n1[0]) && (nodeAfterEqualitySequence[1] == n1[1])) || ((nodeAfterEqualitySequence[0] == n1[1]) && (nodeAfterEqualitySequence[1] == n1[0]))) { @@ -614,7 +614,7 @@ Node ProofArith::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq default: Assert(!pf->d_node.isNull()); - Assert(pf->d_children.empty()); + Assert(pf->num_children() == 0); Debug("pf::arith") << "theory proof: " << pf->d_node << " by rule " << int(pf->d_id) << std::endl; AlwaysAssert(false); return pf->d_node; diff --git a/src/proof/array_proof.cpp b/src/proof/array_proof.cpp index 6d1bd567d..371dda246 100644 --- a/src/proof/array_proof.cpp +++ b/src/proof/array_proof.cpp @@ -139,7 +139,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, if(tb == 0) { Assert(pf->d_id == theory::eq::MERGED_THROUGH_TRANS); Assert(!pf->d_node.isNull()); - Assert(pf->d_children.size() >= 2); + Assert(pf->num_children() >= 2); int neg = -1; theory::eq::EqProof subTrans; @@ -147,19 +147,19 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, subTrans.d_node = pf->d_node; size_t i = 0; - while (i < pf->d_children.size()) { - if (pf->d_children[i]->d_id != theory::eq::MERGED_THROUGH_CONGRUENCE) - pf->d_children[i]->d_node = simplifyBooleanNode(pf->d_children[i]->d_node); + while (i < pf->num_children()) { + if (pf->get_child(i)->d_id != theory::eq::MERGED_THROUGH_CONGRUENCE) + pf->get_child(i)->d_node = simplifyBooleanNode(pf->get_child(i)->d_node); // Look for the negative clause, with which we will form a contradiction. - if(!pf->d_children[i]->d_node.isNull() && pf->d_children[i]->d_node.getKind() == kind::NOT) { + if(!pf->get_child(i)->d_node.isNull() && pf->get_child(i)->d_node.getKind() == kind::NOT) { Assert(neg < 0); neg = i; ++i; } // Handle congruence closures over equalities. - else if (pf->d_children[i]->d_id==theory::eq::MERGED_THROUGH_CONGRUENCE && pf->d_children[i]->d_node.isNull()) { + else if (pf->get_child(i)->d_id==theory::eq::MERGED_THROUGH_CONGRUENCE && pf->get_child(i)->d_node.isNull()) { Debug("pf::array") << "Handling congruence over equalities" << std::endl; // Gather the sequence of consecutive congruence closures. @@ -167,13 +167,13 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, unsigned count; Debug("pf::array") << "Collecting congruence sequence" << std::endl; for (count = 0; - i + count < pf->d_children.size() && - pf->d_children[i + count]->d_id==theory::eq::MERGED_THROUGH_CONGRUENCE && - pf->d_children[i + count]->d_node.isNull(); + i + count < pf->num_children() && + pf->get_child(i + count)->d_id==theory::eq::MERGED_THROUGH_CONGRUENCE && + pf->get_child(i + count)->d_node.isNull(); ++count) { Debug("pf::array") << "Found a congruence: " << std::endl; - pf->d_children[i+count]->debug_print("pf::array", 0, &d_proofPrinter); - congruenceClosures.push_back(pf->d_children[i+count]); + pf->get_child(i+count)->debug_print("pf::array", 0, &d_proofPrinter); + congruenceClosures.push_back(pf->get_child(i+count)); } Debug("pf::array") << "Total number of congruences found: " << congruenceClosures.size() << std::endl; @@ -187,9 +187,9 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, targetAppearsBefore = false; } - if ((i + count >= pf->d_children.size()) || - (!pf->d_children[i + count]->d_node.isNull() && - pf->d_children[i + count]->d_node.getKind() == kind::NOT)) { + if ((i + count >= pf->num_children()) || + (!pf->get_child(i + count)->d_node.isNull() && + pf->get_child(i + count)->d_node.getKind() == kind::NOT)) { Debug("pf::array") << "Target does not appear after" << std::endl; targetAppearsAfter = false; } @@ -202,32 +202,32 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, // Insert target clause first. if (targetAppearsBefore) { - orderedEqualities.push_back(pf->d_children[i - 1]); + orderedEqualities.push_back(pf->get_child(i - 1)); // The target has already been added to subTrans; remove it. - subTrans.d_children.pop_back(); + subTrans.remove_last_child(); } else { - orderedEqualities.push_back(pf->d_children[i + count]); + orderedEqualities.push_back(pf->get_child(i + count)); } // Start with the congruence closure closest to the target clause, and work our way back/forward. if (targetAppearsBefore) { for (unsigned j = 0; j < count; ++j) { - if (pf->d_children[i + j]->d_children[0]->d_id != theory::eq::MERGED_THROUGH_REFLEXIVITY) - orderedEqualities.insert(orderedEqualities.begin(), pf->d_children[i + j]->d_children[0]); - if (pf->d_children[i + j]->d_children[1]->d_id != theory::eq::MERGED_THROUGH_REFLEXIVITY) - orderedEqualities.insert(orderedEqualities.end(), pf->d_children[i + j]->d_children[1]); + if (pf->get_child(i + j)->get_child(0)->d_id != theory::eq::MERGED_THROUGH_REFLEXIVITY) + orderedEqualities.insert(orderedEqualities.begin(), pf->get_child(i + j)->get_child(0)); + if (pf->get_child(i + j)->get_child(1)->d_id != theory::eq::MERGED_THROUGH_REFLEXIVITY) + orderedEqualities.insert(orderedEqualities.end(), pf->get_child(i + j)->get_child(1)); } } else { for (unsigned j = 0; j < count; ++j) { - if (pf->d_children[i + count - 1 - j]->d_children[0]->d_id != theory::eq::MERGED_THROUGH_REFLEXIVITY) - orderedEqualities.insert(orderedEqualities.begin(), pf->d_children[i + count - 1 - j]->d_children[0]); - if (pf->d_children[i + count - 1 - j]->d_children[1]->d_id != theory::eq::MERGED_THROUGH_REFLEXIVITY) - orderedEqualities.insert(orderedEqualities.end(), pf->d_children[i + count - 1 - j]->d_children[1]); + if (pf->get_child(i + count - 1 - j)->get_child(0)->d_id != theory::eq::MERGED_THROUGH_REFLEXIVITY) + orderedEqualities.insert(orderedEqualities.begin(), pf->get_child(i + count - 1 - j)->get_child(0)); + if (pf->get_child(i + count - 1 - j)->get_child(1)->d_id != theory::eq::MERGED_THROUGH_REFLEXIVITY) + orderedEqualities.insert(orderedEqualities.end(), pf->get_child(i + count - 1 - j)->get_child(1)); } } // Copy the result into the main transitivity proof. - subTrans.d_children.insert(subTrans.d_children.end(), orderedEqualities.begin(), orderedEqualities.end()); + subTrans.add_children(orderedEqualities); // Increase i to skip over the children that have been processed. i += count; @@ -238,7 +238,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, // Else, just copy the child proof as is else { - subTrans.d_children.push_back(pf->d_children[i]); + subTrans.add_child(pf->get_child(i)); ++i; } } @@ -254,34 +254,33 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, Node n1; std::stringstream ss, ss2; - //Assert(subTrans.d_children.size() == pf->d_children.size() - 1); - Debug("mgdx") << "\nsubtrans has " << subTrans.d_children.size() << " children\n"; - if(!disequalityFound || pf->d_children.size() > 2) { + Debug("mgdx") << "\nsubtrans has " << subTrans.num_children() << " children\n"; + if(!disequalityFound || pf->num_children() > 2) { n1 = toStreamRecLFSC(ss, tp, &subTrans, 1, map); } else { - n1 = toStreamRecLFSC(ss, tp, subTrans.d_children[0], 1, map); - Debug("mgdx") << "\nsubTrans unique child " << subTrans.d_children[0]->d_id << " was proven\ngot: " << n1 << std::endl; + n1 = toStreamRecLFSC(ss, tp, subTrans.get_child(0), 1, map); + Debug("mgdx") << "\nsubTrans unique child " << subTrans.get_child(0)->d_id << " was proven\ngot: " << n1 << std::endl; } out << "(clausify_false (contra _ "; if (disequalityFound) { - Node n2 = pf->d_children[neg]->d_node; + Node n2 = pf->get_child(neg)->d_node; Assert(n2.getKind() == kind::NOT); Debug("mgdx") << "\nhave proven: " << n1 << std::endl; Debug("mgdx") << "n2 is " << n2 << std::endl; - Debug("mgdx") << "n2->d_id is " << pf->d_children[neg]->d_id << std::endl; + Debug("mgdx") << "n2->d_id is " << pf->get_child(neg)->d_id << std::endl; Debug("mgdx") << "n2[0] is " << n2[0] << std::endl; if (n2[0].getNumChildren() > 0) { Debug("mgdx") << "\nn2[0]: " << n2[0][0] << std::endl; } if (n1.getNumChildren() > 1) { Debug("mgdx") << "n1[1]: " << n1[1] << std::endl; } - if ((pf->d_children[neg]->d_id == d_reasonExt) || - (pf->d_children[neg]->d_id == theory::eq::MERGED_THROUGH_TRANS)) { + if ((pf->get_child(neg)->d_id == d_reasonExt) || + (pf->get_child(neg)->d_id == theory::eq::MERGED_THROUGH_TRANS)) { // Ext case: The negative node was created by an EXT rule; e.g. it is a[k]!=b[k], due to a!=b. out << ss.str(); out << " "; - toStreamRecLFSC(ss2, tp, pf->d_children[neg], 1, map); + toStreamRecLFSC(ss2, tp, pf->get_child(neg), 1, map); out << ss2.str(); } else if (n2[0].getKind() == kind::APPLY_UF) { out << "(trans _ _ _ _ "; @@ -321,7 +320,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, Debug("mgd") << "\nok, looking at congruence:\n"; pf->debug_print("mgd", 0, &d_proofPrinter); std::stack stk; - for(const theory::eq::EqProof* pf2 = pf; pf2->d_id == theory::eq::MERGED_THROUGH_CONGRUENCE; pf2 = pf2->d_children[0]) { + for(const theory::eq::EqProof* pf2 = pf; pf2->d_id == theory::eq::MERGED_THROUGH_CONGRUENCE; pf2 = pf2->get_child(0)) { Debug("mgd") << "Looking at pf2 with d_node: " << pf2->d_node << std::endl; Assert(!pf2->d_node.isNull()); @@ -333,28 +332,28 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, pf2->d_node.getKind() == kind::PARTIAL_SELECT_1 || pf2->d_node.getKind() == kind::STORE); - Assert(pf2->d_children.size() == 2); + Assert(pf2->num_children() == 2); out << "(cong _ _ _ _ _ _ "; stk.push(pf2); } - Assert(stk.top()->d_children[0]->d_id != theory::eq::MERGED_THROUGH_CONGRUENCE); + Assert(stk.top()->get_child(0)->d_id != theory::eq::MERGED_THROUGH_CONGRUENCE); // NodeBuilder<> b1(kind::PARTIAL_APPLY_UF), b2(kind::PARTIAL_APPLY_UF); NodeBuilder<> b1, b2; const theory::eq::EqProof* pf2 = stk.top(); stk.pop(); Assert(pf2->d_id == theory::eq::MERGED_THROUGH_CONGRUENCE); - Node n1 = toStreamRecLFSC(out, tp, pf2->d_children[0], tb + 1, map); + Node n1 = toStreamRecLFSC(out, tp, pf2->get_child(0), tb + 1, map); out << " "; std::stringstream ss; - Node n2 = toStreamRecLFSC(ss, tp, pf2->d_children[1], tb + 1, map); + Node n2 = toStreamRecLFSC(ss, tp, pf2->get_child(1), tb + 1, map); Debug("mgd") << "\nok, in FIRST cong[" << stk.size() << "]" << "\n"; pf2->debug_print("mgd", 0, &d_proofPrinter); // Temp - Debug("mgd") << "n1 is a proof for: " << pf2->d_children[0]->d_node << ". It is: " << n1 << std::endl; - Debug("mgd") << "n2 is a proof for: " << pf2->d_children[1]->d_node << ". It is: " << n2 << std::endl; + Debug("mgd") << "n1 is a proof for: " << pf2->get_child(0)->d_node << ". It is: " << n1 << std::endl; + Debug("mgd") << "n2 is a proof for: " << pf2->get_child(1)->d_node << ". It is: " << n2 << std::endl; // Debug("mgd") << "looking at " << pf2->d_node << "\n"; Debug("mgd") << " " << n1 << "\n"; @@ -368,7 +367,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, Debug("mgd") << "SIDE IS 1\n"; if(!match(pf2->d_node, n1[1])) { Debug("mgd") << "IN BAD CASE, our first subproof is\n"; - pf2->d_children[0]->debug_print("mgd", 0, &d_proofPrinter); + pf2->get_child(0)->debug_print("mgd", 0, &d_proofPrinter); } Assert(match(pf2->d_node, n1[1])); side = 1; @@ -463,7 +462,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, Assert(pf2->d_id == theory::eq::MERGED_THROUGH_CONGRUENCE); out << " "; ss.str(""); - n2 = toStreamRecLFSC(ss, tp, pf2->d_children[1], tb + 1, map); + n2 = toStreamRecLFSC(ss, tp, pf2->get_child(1), tb + 1, map); Debug("mgd") << "\nok, in cong[" << stk.size() << "]" << "\n"; Debug("mgd") << "looking at " << pf2->d_node << "\n"; @@ -566,7 +565,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, else if (pf->d_id == theory::eq::MERGED_THROUGH_REFLEXIVITY) { Assert(!pf->d_node.isNull()); - Assert(pf->d_children.empty()); + Assert(pf->num_children() == 0); out << "(refl _ "; tp->printTerm(NodeManager::currentNM()->toExpr(pf->d_node), out, map); out << ")"; @@ -575,7 +574,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, else if (pf->d_id == theory::eq::MERGED_THROUGH_EQUALITY) { Assert(!pf->d_node.isNull()); - Assert(pf->d_children.empty()); + Assert(pf->num_children() == 0); Debug("pf::array") << "ArrayProof::toStream: getLitName( " << pf->d_node.negate() << " ) = " << ProofManager::getLitName(pf->d_node.negate()) << std::endl; out << ProofManager::getLitName(pf->d_node.negate()); @@ -602,15 +601,15 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, bool secondNeg = false; Assert(!pf->d_node.isNull()); - Assert(pf->d_children.size() >= 2); + Assert(pf->num_children() >= 2); std::stringstream ss; Debug("mgd") << "\ndoing trans proof[[\n"; pf->debug_print("mgd", 0, &d_proofPrinter); Debug("mgd") << "\n"; - pf->d_children[0]->d_node = simplifyBooleanNode(pf->d_children[0]->d_node); + pf->get_child(0)->d_node = simplifyBooleanNode(pf->get_child(0)->d_node); - Node n1 = toStreamRecLFSC(ss, tp, pf->d_children[0], tb + 1, map); + Node n1 = toStreamRecLFSC(ss, tp, pf->get_child(0), tb + 1, map); Debug("mgd") << "\ndoing trans proof, got n1 " << n1 << "\n"; if(tb == 1) { Debug("mgdx") << "\ntrans proof[0], got n1 " << n1 << "\n"; @@ -622,7 +621,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, std::map childToStream; - for(size_t i = 1; i < pf->d_children.size(); ++i) { + for(size_t i = 1; i < pf->num_children(); ++i) { std::stringstream ss1(ss.str()), ss2; ss.str(""); @@ -630,8 +629,8 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, // and not turn them into (a[x]=true), because that will mess up the congruence application // later. - if (pf->d_children[i]->d_id != theory::eq::MERGED_THROUGH_CONGRUENCE) - pf->d_children[i]->d_node = simplifyBooleanNode(pf->d_children[i]->d_node); + if (pf->get_child(i)->d_id != theory::eq::MERGED_THROUGH_CONGRUENCE) + pf->get_child(i)->d_node = simplifyBooleanNode(pf->get_child(i)->d_node); // It is possible that we've already converted the i'th child to stream. If so, // use previously stored result. Otherwise, convert and store. @@ -639,7 +638,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, if (childToStream.find(i) != childToStream.end()) n2 = childToStream[i]; else { - n2 = toStreamRecLFSC(ss2, tp, pf->d_children[i], tb + 1, map); + n2 = toStreamRecLFSC(ss2, tp, pf->get_child(i), tb + 1, map); childToStream[i] = n2; } @@ -673,9 +672,9 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, bool sequenceOver = false; size_t j = i + 1; - while (j < pf->d_children.size() && !sequenceOver) { + while (j < pf->num_children() && !sequenceOver) { std::stringstream dontCare; - nodeAfterEqualitySequence = toStreamRecLFSC(dontCare, tp, pf->d_children[j], tb + 1, map ); + nodeAfterEqualitySequence = toStreamRecLFSC(dontCare, tp, pf->get_child(j), tb + 1, map ); if (((nodeAfterEqualitySequence[0] == n1[0]) && (nodeAfterEqualitySequence[1] == n1[1])) || ((nodeAfterEqualitySequence[0] == n1[1]) && (nodeAfterEqualitySequence[1] == n1[0]))) { @@ -917,9 +916,9 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, // inner index != outer index // t3 is the outer index - Assert(pf->d_children.size() == 1); + Assert(pf->num_children() == 1); std::stringstream ss; - Node subproof = toStreamRecLFSC(ss, tp, pf->d_children[0], tb + 1, map); + Node subproof = toStreamRecLFSC(ss, tp, pf->get_child(0), tb + 1, map); out << "(row _ _ "; tp->printTerm(t2.toExpr(), out, map); @@ -932,7 +931,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, out << " "; - Debug("pf::array") << "pf->d_children[0]->d_node is: " << pf->d_children[0]->d_node + Debug("pf::array") << "pf->get_child(0)->d_node is: " << pf->get_child(0)->d_node << ". t3 is: " << t3 << std::endl << "subproof is: " << subproof << std::endl; @@ -1005,7 +1004,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, } else { Debug("pf::array") << "In the case of NEGATIVE ROW" << std::endl; - Debug("pf::array") << "pf->d_children[0]->d_node is: " << pf->d_children[0]->d_node << std::endl; + Debug("pf::array") << "pf->get_child(0)->d_node is: " << pf->get_child(0)->d_node << std::endl; // This is the case where (i == k), and the sub-proof explains why ((a[i]:=t)[k] != a[k]) @@ -1022,15 +1021,15 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, t1 = pf->d_node[0]; t2 = pf->d_node[1]; - // pf->d_children[0]->d_node will have the form: (not (= (select (store a_565 i7 e_566) i1) (select a_565 i1))), + // pf->get_child(0)->d_node will have the form: (not (= (select (store a_565 i7 e_566) i1) (select a_565 i1))), // or its symmetrical version. unsigned side; - if (pf->d_children[0]->d_node[0][0].getKind() == kind::SELECT && - pf->d_children[0]->d_node[0][0][0].getKind() == kind::STORE) { + if (pf->get_child(0)->d_node[0][0].getKind() == kind::SELECT && + pf->get_child(0)->d_node[0][0][0].getKind() == kind::STORE) { side = 0; - } else if (pf->d_children[0]->d_node[0][1].getKind() == kind::SELECT && - pf->d_children[0]->d_node[0][1][0].getKind() == kind::STORE) { + } else if (pf->get_child(0)->d_node[0][1].getKind() == kind::SELECT && + pf->get_child(0)->d_node[0][1][0].getKind() == kind::STORE) { side = 1; } else { @@ -1040,18 +1039,18 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, Debug("pf::array") << "Side is: " << side << std::endl; // The array's index and element types will come from the subproof... - t3 = pf->d_children[0]->d_node[0][side][0][0]; - t4 = pf->d_children[0]->d_node[0][side][0][2]; + t3 = pf->get_child(0)->d_node[0][side][0][0]; + t4 = pf->get_child(0)->d_node[0][side][0][2]; ret = pf->d_node; // The order of indices needs to match; we might have to swap t1 and t2 and then apply symmetry. - bool swap = (t2 == pf->d_children[0]->d_node[0][side][0][1]); + bool swap = (t2 == pf->get_child(0)->d_node[0][side][0][1]); Debug("mgd") << "t1 " << t1 << "\nt2 " << t2 << "\nt3 " << t3 << "\nt4 " << t4 << "\n"; - Assert(pf->d_children.size() == 1); + Assert(pf->num_children() == 1); std::stringstream ss; - Node subproof = toStreamRecLFSC(ss, tp, pf->d_children[0], tb + 1, map); + Node subproof = toStreamRecLFSC(ss, tp, pf->get_child(0), tb + 1, map); Debug("pf::array") << "Subproof is: " << ss.str() << std::endl; @@ -1125,9 +1124,9 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, Assert(pf->d_node.getKind() == kind::NOT); Assert(pf->d_node[0].getKind() == kind::EQUAL); - Assert(pf->d_children.size() == 1); + Assert(pf->num_children() == 1); - child_proof = pf->d_children[0]; + child_proof = pf->get_child(0); Assert(child_proof->d_node.getKind() == kind::NOT); Assert(child_proof->d_node[0].getKind() == kind::EQUAL); @@ -1151,7 +1150,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, else { Assert(!pf->d_node.isNull()); - Assert(pf->d_children.empty()); + Assert(pf->num_children() == 0); Debug("mgd") << "theory proof: " << pf->d_node << " by rule " << int(pf->d_id) << std::endl; AlwaysAssert(false); return pf->d_node; diff --git a/src/proof/proof_output_channel.cpp b/src/proof/proof_output_channel.cpp index c87ccd37c..376f3ce1d 100644 --- a/src/proof/proof_output_channel.cpp +++ b/src/proof/proof_output_channel.cpp @@ -16,6 +16,12 @@ namespace CVC4 { ProofOutputChannel::ProofOutputChannel() : d_conflict(), d_proof(NULL) {} +ProofOutputChannel::~ProofOutputChannel() { + if (d_proof != NULL) { + delete d_proof; + } +} + void ProofOutputChannel::conflict(TNode n, Proof* pf) throw() { Trace("pf::tp") << "ProofOutputChannel: CONFLICT: " << n << std::endl; Assert(d_conflict.isNull()); diff --git a/src/proof/proof_output_channel.h b/src/proof/proof_output_channel.h index b44689fe5..f3ef572a1 100644 --- a/src/proof/proof_output_channel.h +++ b/src/proof/proof_output_channel.h @@ -16,13 +16,13 @@ namespace CVC4 { class ProofOutputChannel : public theory::OutputChannel { public: Node d_conflict; + // ProofOutputChannel owns d_proof Proof* d_proof; Node d_lemma; std::set d_propagations; ProofOutputChannel(); - - virtual ~ProofOutputChannel() throw() {} + virtual ~ProofOutputChannel(); virtual void conflict(TNode n, Proof* pf) throw(); virtual bool propagate(TNode x) throw(); diff --git a/src/proof/sat_proof_implementation.h b/src/proof/sat_proof_implementation.h index 9f77f3bdd..ca757b61f 100644 --- a/src/proof/sat_proof_implementation.h +++ b/src/proof/sat_proof_implementation.h @@ -236,6 +236,12 @@ template TSatProof::~TSatProof() { delete d_proxy; + typename IdToConflicts::const_iterator debug_it = d_assumptionConflictsDebug.begin(); + typename IdToConflicts::const_iterator debug_end = d_assumptionConflictsDebug.end(); + for (; debug_it != debug_end; ++debug_it) { + delete debug_it->second; + } + // FIXME: double free if deleted clause also appears in d_seenLemmas? IdToSatClause::const_iterator it = d_deletedTheoryLemmas.begin(); IdToSatClause::const_iterator end = d_deletedTheoryLemmas.end(); @@ -267,16 +273,6 @@ TSatProof::~TSatProof() { for (; resolution_it != resolution_it_end; ++resolution_it) { delete *resolution_it; } - - // It could be the case that d_resStack is not empty at destruction time - // (for example in the SAT case). - typename ResStack::const_iterator resolution_stack_it = d_resStack.begin(); - typename ResStack::const_iterator resolution_stack_it_end = d_resStack.end(); - for (; resolution_stack_it != resolution_stack_it_end; - ++resolution_stack_it) { - ResChain* current = *resolution_stack_it; - delete current; - } } template @@ -807,6 +803,7 @@ template void TSatProof::cancelResChain() { Assert(d_resStack.size() > 0); ResolutionChain* back = d_resStack.back(); + d_existingResolutionChains.erase(back); delete back; d_resStack.pop_back(); } diff --git a/src/proof/uf_proof.cpp b/src/proof/uf_proof.cpp index cea873b6d..e150ab5ca 100644 --- a/src/proof/uf_proof.cpp +++ b/src/proof/uf_proof.cpp @@ -66,6 +66,9 @@ inline static bool match(TNode n1, TNode n2) { return true; } +ProofUF::~ProofUF() { + delete d_proof; +} void ProofUF::toStream(std::ostream& out) { ProofLetMap map; @@ -103,7 +106,7 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E Assert(pf->d_id == theory::eq::MERGED_THROUGH_TRANS); Assert(!pf->d_node.isNull()); - Assert(pf->d_children.size() >= 2); + Assert(pf->num_children() >= 2); int neg = -1; theory::eq::EqProof subTrans; @@ -112,19 +115,19 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E size_t i = 0; - while (i < pf->d_children.size()) { - pf->d_children[i]->d_node = simplifyBooleanNode(pf->d_children[i]->d_node); + while (i < pf->num_children()) { + pf->get_child(i)->d_node = simplifyBooleanNode(pf->get_child(i)->d_node); // Look for the negative clause, with which we will form a contradiction. - if(!pf->d_children[i]->d_node.isNull() && pf->d_children[i]->d_node.getKind() == kind::NOT) { + if(!pf->get_child(i)->d_node.isNull() && pf->get_child(i)->d_node.getKind() == kind::NOT) { Assert(neg < 0); - Node node = pf->d_children[i]->d_node[0]; + Node node = pf->get_child(i)->d_node[0]; neg = i; ++i; } // Handle congruence closures over equalities. - else if (pf->d_children[i]->d_id==theory::eq::MERGED_THROUGH_CONGRUENCE && pf->d_children[i]->d_node.isNull()) { + else if (pf->get_child(i)->d_id==theory::eq::MERGED_THROUGH_CONGRUENCE && pf->get_child(i)->d_node.isNull()) { Debug("pf::uf") << "Handling congruence over equalities" << std::endl; // Gather the sequence of consecutive congruence closures. @@ -132,13 +135,13 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E unsigned count; Debug("pf::uf") << "Collecting congruence sequence" << std::endl; for (count = 0; - i + count < pf->d_children.size() && - pf->d_children[i + count]->d_id==theory::eq::MERGED_THROUGH_CONGRUENCE && - pf->d_children[i + count]->d_node.isNull(); + i + count < pf->num_children() && + pf->get_child(i + count)->d_id==theory::eq::MERGED_THROUGH_CONGRUENCE && + pf->get_child(i + count)->d_node.isNull(); ++count) { Debug("pf::uf") << "Found a congruence: " << std::endl; - pf->d_children[i+count]->debug_print("pf::uf"); - congruenceClosures.push_back(pf->d_children[i+count]); + pf->get_child(i+count)->debug_print("pf::uf"); + congruenceClosures.push_back(pf->get_child(i+count)); } Debug("pf::uf") << "Total number of congruences found: " << congruenceClosures.size() << std::endl; @@ -152,9 +155,9 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E targetAppearsBefore = false; } - if ((i + count >= pf->d_children.size()) || - (!pf->d_children[i + count]->d_node.isNull() && - pf->d_children[i + count]->d_node.getKind() == kind::NOT)) { + if ((i + count >= pf->num_children()) || + (!pf->get_child(i + count)->d_node.isNull() && + pf->get_child(i + count)->d_node.getKind() == kind::NOT)) { Debug("pf::uf") << "Target does not appear after" << std::endl; targetAppearsAfter = false; } @@ -171,32 +174,32 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E // Insert target clause first. if (targetAppearsBefore) { - orderedEqualities.push_back(pf->d_children[i - 1]); + orderedEqualities.push_back(pf->get_child(i - 1)); // The target has already been added to subTrans; remove it. - subTrans.d_children.pop_back(); + subTrans.remove_last_child(); } else { - orderedEqualities.push_back(pf->d_children[i + count]); + orderedEqualities.push_back(pf->get_child(i + count)); } // Start with the congruence closure closest to the target clause, and work our way back/forward. if (targetAppearsBefore) { for (unsigned j = 0; j < count; ++j) { - if (pf->d_children[i + j]->d_children[0]->d_id != theory::eq::MERGED_THROUGH_REFLEXIVITY) - orderedEqualities.insert(orderedEqualities.begin(), pf->d_children[i + j]->d_children[0]); - if (pf->d_children[i + j]->d_children[1]->d_id != theory::eq::MERGED_THROUGH_REFLEXIVITY) - orderedEqualities.insert(orderedEqualities.end(), pf->d_children[i + j]->d_children[1]); + if (pf->get_child(i + j)->get_child(0)->d_id != theory::eq::MERGED_THROUGH_REFLEXIVITY) + orderedEqualities.insert(orderedEqualities.begin(), pf->get_child(i + j)->get_child(0)); + if (pf->get_child(i + j)->get_child(1)->d_id != theory::eq::MERGED_THROUGH_REFLEXIVITY) + orderedEqualities.insert(orderedEqualities.end(), pf->get_child(i + j)->get_child(1)); } } else { for (unsigned j = 0; j < count; ++j) { - if (pf->d_children[i + count - 1 - j]->d_children[0]->d_id != theory::eq::MERGED_THROUGH_REFLEXIVITY) - orderedEqualities.insert(orderedEqualities.begin(), pf->d_children[i + count - 1 - j]->d_children[0]); - if (pf->d_children[i + count - 1 - j]->d_children[1]->d_id != theory::eq::MERGED_THROUGH_REFLEXIVITY) - orderedEqualities.insert(orderedEqualities.end(), pf->d_children[i + count - 1 - j]->d_children[1]); + if (pf->get_child(i + count - 1 - j)->get_child(0)->d_id != theory::eq::MERGED_THROUGH_REFLEXIVITY) + orderedEqualities.insert(orderedEqualities.begin(), pf->get_child(i + count - 1 - j)->get_child(0)); + if (pf->get_child(i + count - 1 - j)->get_child(1)->d_id != theory::eq::MERGED_THROUGH_REFLEXIVITY) + orderedEqualities.insert(orderedEqualities.end(), pf->get_child(i + count - 1 - j)->get_child(1)); } } // Copy the result into the main transitivity proof. - subTrans.d_children.insert(subTrans.d_children.end(), orderedEqualities.begin(), orderedEqualities.end()); + subTrans.add_children(orderedEqualities); // Increase i to skip over the children that have been processed. i += count; @@ -207,7 +210,7 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E // Else, just copy the child proof as is else { - subTrans.d_children.push_back(pf->d_children[i]); + subTrans.add_child(pf->get_child(i)); ++i; } } @@ -223,13 +226,13 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E Node n1; std::stringstream ss; - Debug("pf::uf") << "\nsubtrans has " << subTrans.d_children.size() << " children\n"; + Debug("pf::uf") << "\nsubtrans has " << subTrans.num_children() << " children\n"; - if(!disequalityFound || subTrans.d_children.size() >= 2) { + if(!disequalityFound || subTrans.num_children() >= 2) { n1 = toStreamRecLFSC(ss, tp, &subTrans, 1, map); } else { - n1 = toStreamRecLFSC(ss, tp, subTrans.d_children[0], 1, map); - Debug("pf::uf") << "\nsubTrans unique child " << subTrans.d_children[0]->d_id << " was proven\ngot: " << n1 << std::endl; + n1 = toStreamRecLFSC(ss, tp, subTrans.get_child(0), 1, map); + Debug("pf::uf") << "\nsubTrans unique child " << subTrans.get_child(0)->d_id << " was proven\ngot: " << n1 << std::endl; } Debug("pf::uf") << "\nhave proven: " << n1 << std::endl; @@ -237,7 +240,7 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E out << "(clausify_false (contra _ "; if (disequalityFound) { - Node n2 = pf->d_children[neg]->d_node; + Node n2 = pf->get_child(neg)->d_node; Assert(n2.getKind() == kind::NOT); Debug("pf::uf") << "n2 is " << n2[0] << std::endl; @@ -287,22 +290,22 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E Debug("pf::uf") << "\nok, looking at congruence:\n"; pf->debug_print("pf::uf"); std::stack stk; - for(const theory::eq::EqProof* pf2 = pf; pf2->d_id == theory::eq::MERGED_THROUGH_CONGRUENCE; pf2 = pf2->d_children[0]) { + for(const theory::eq::EqProof* pf2 = pf; pf2->d_id == theory::eq::MERGED_THROUGH_CONGRUENCE; pf2 = pf2->get_child(0)) { Assert(!pf2->d_node.isNull()); Assert(pf2->d_node.getKind() == kind::PARTIAL_APPLY_UF || pf2->d_node.getKind() == kind::BUILTIN || pf2->d_node.getKind() == kind::APPLY_UF || pf2->d_node.getKind() == kind::SELECT || pf2->d_node.getKind() == kind::STORE); - Assert(pf2->d_children.size() == 2); + Assert(pf2->num_children() == 2); out << "(cong _ _ _ _ _ _ "; stk.push(pf2); } - Assert(stk.top()->d_children[0]->d_id != theory::eq::MERGED_THROUGH_CONGRUENCE); + Assert(stk.top()->get_child(0)->d_id != theory::eq::MERGED_THROUGH_CONGRUENCE); NodeBuilder<> b1(kind::PARTIAL_APPLY_UF), b2(kind::PARTIAL_APPLY_UF); const theory::eq::EqProof* pf2 = stk.top(); stk.pop(); Assert(pf2->d_id == theory::eq::MERGED_THROUGH_CONGRUENCE); - Node n1 = toStreamRecLFSC(out, tp, pf2->d_children[0], tb + 1, map); + Node n1 = toStreamRecLFSC(out, tp, pf2->get_child(0), tb + 1, map); out << " "; std::stringstream ss; - Node n2 = toStreamRecLFSC(ss, tp, pf2->d_children[1], tb + 1, map); + Node n2 = toStreamRecLFSC(ss, tp, pf2->get_child(1), tb + 1, map); Debug("pf::uf") << "\nok, in FIRST cong[" << stk.size() << "]" << "\n"; pf2->debug_print("pf::uf"); Debug("pf::uf") << "looking at " << pf2->d_node << "\n"; @@ -320,7 +323,7 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E //} if(!match(pf2->d_node, n1[1])) { Debug("pf::uf") << "IN BAD CASE, our first subproof is\n"; - pf2->d_children[0]->debug_print("pf::uf"); + pf2->get_child(0)->debug_print("pf::uf"); } Assert(match(pf2->d_node, n1[1])); side = 1; @@ -370,7 +373,7 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E Assert(pf2->d_id == theory::eq::MERGED_THROUGH_CONGRUENCE); out << " "; ss.str(""); - n2 = toStreamRecLFSC(ss, tp, pf2->d_children[1], tb + 1, map); + n2 = toStreamRecLFSC(ss, tp, pf2->get_child(1), tb + 1, map); Debug("pf::uf") << "\nok, in cong[" << stk.size() << "]" << "\n"; Debug("pf::uf") << "looking at " << pf2->d_node << "\n"; Debug("pf::uf") << " " << n1 << "\n"; @@ -428,7 +431,7 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E case theory::eq::MERGED_THROUGH_REFLEXIVITY: Assert(!pf->d_node.isNull()); - Assert(pf->d_children.empty()); + Assert(pf->num_children() == 0); out << "(refl _ "; tp->printTerm(NodeManager::currentNM()->toExpr(pf->d_node), out, map); out << ")"; @@ -436,21 +439,21 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E case theory::eq::MERGED_THROUGH_EQUALITY: Assert(!pf->d_node.isNull()); - Assert(pf->d_children.empty()); + Assert(pf->num_children() == 0); out << ProofManager::getLitName(pf->d_node.negate()); return pf->d_node; case theory::eq::MERGED_THROUGH_TRANS: { Assert(!pf->d_node.isNull()); - Assert(pf->d_children.size() >= 2); + Assert(pf->num_children() >= 2); std::stringstream ss; Debug("pf::uf") << "\ndoing trans proof[[\n"; pf->debug_print("pf::uf"); Debug("pf::uf") << "\n"; - pf->d_children[0]->d_node = simplifyBooleanNode(pf->d_children[0]->d_node); + pf->get_child(0)->d_node = simplifyBooleanNode(pf->get_child(0)->d_node); - Node n1 = toStreamRecLFSC(ss, tp, pf->d_children[0], tb + 1, map); + Node n1 = toStreamRecLFSC(ss, tp, pf->get_child(0), tb + 1, map); Debug("pf::uf") << "\ndoing trans proof, got n1 " << n1 << "\n"; if(tb == 1) { Debug("pf::uf") << "\ntrans proof[0], got n1 " << n1 << "\n"; @@ -462,11 +465,11 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E std::map childToStream; - for(size_t i = 1; i < pf->d_children.size(); ++i) { + for(size_t i = 1; i < pf->num_children(); ++i) { std::stringstream ss1(ss.str()), ss2; ss.str(""); - pf->d_children[i]->d_node = simplifyBooleanNode(pf->d_children[i]->d_node); + pf->get_child(i)->d_node = simplifyBooleanNode(pf->get_child(i)->d_node); // It is possible that we've already converted the i'th child to stream. If so, // use previously stored result. Otherwise, convert and store. @@ -474,7 +477,7 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E if (childToStream.find(i) != childToStream.end()) n2 = childToStream[i]; else { - n2 = toStreamRecLFSC(ss2, tp, pf->d_children[i], tb + 1, map); + n2 = toStreamRecLFSC(ss2, tp, pf->get_child(i), tb + 1, map); childToStream[i] = n2; } @@ -505,9 +508,9 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E bool sequenceOver = false; size_t j = i + 1; - while (j < pf->d_children.size() && !sequenceOver) { + while (j < pf->num_children() && !sequenceOver) { std::stringstream dontCare; - nodeAfterEqualitySequence = toStreamRecLFSC(dontCare, tp, pf->d_children[j], tb + 1, map ); + nodeAfterEqualitySequence = toStreamRecLFSC(dontCare, tp, pf->get_child(j), tb + 1, map ); if (((nodeAfterEqualitySequence[0] == n1[0]) && (nodeAfterEqualitySequence[1] == n1[1])) || ((nodeAfterEqualitySequence[0] == n1[1]) && (nodeAfterEqualitySequence[1] == n1[0]))) { @@ -707,7 +710,7 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E default: Assert(!pf->d_node.isNull()); - Assert(pf->d_children.empty()); + Assert(pf->num_children() == 0); Debug("pf::uf") << "theory proof: " << pf->d_node << " by rule " << int(pf->d_id) << std::endl; AlwaysAssert(false); return pf->d_node; diff --git a/src/proof/uf_proof.h b/src/proof/uf_proof.h index c4bd28dc5..bfc242ea8 100644 --- a/src/proof/uf_proof.h +++ b/src/proof/uf_proof.h @@ -31,6 +31,8 @@ private: static Node toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::EqProof * pf, unsigned tb, const ProofLetMap& map); public: ProofUF( theory::eq::EqProof * pf ) : d_proof( pf ) {} + ~ProofUF(); + //it is simply an equality engine proof theory::eq::EqProof * d_proof; void toStream(std::ostream& out); diff --git a/src/theory/arrays/array_proof_reconstruction.cpp b/src/theory/arrays/array_proof_reconstruction.cpp index 5ecccdd53..56cfd501f 100644 --- a/src/theory/arrays/array_proof_reconstruction.cpp +++ b/src/theory/arrays/array_proof_reconstruction.cpp @@ -50,7 +50,7 @@ void ArrayProofReconstruction::notify(unsigned reasonType, Node reason, Node a, // recursively, to explain this. eq::EqProof* childProof = new eq::EqProof; childProof->d_node = reason; - proof->d_children.push_back(childProof); + proof->add_child(childProof); } } @@ -108,40 +108,40 @@ void ArrayProofReconstruction::notify(unsigned reasonType, Node reason, Node a, // It could be that the guard condition is a constant disequality. In this case, // we need to change it to a different format. bool haveNegChild = false; - for (unsigned i = 0; i < childProof->d_children.size(); ++i) { - if (childProof->d_children[i]->d_node.getKind() == kind::NOT) + for (unsigned i = 0; i < childProof->num_children(); ++i) { + if (childProof->get_child(i)->d_node.getKind() == kind::NOT) haveNegChild = true; } - if ((childProof->d_children.size() != 0) && + if ((childProof->num_children() != 0) && (childProof->d_id == theory::eq::MERGED_THROUGH_CONSTANTS || !haveNegChild)) { // The proof has two children, explaining why each index is a (different) constant. - Assert(childProof->d_children.size() == 2); + Assert(childProof->num_children() == 2); Node constantOne, constantTwo; // Each subproof explains why one of the indices is constant. - if (childProof->d_children[0]->d_id == theory::eq::MERGED_THROUGH_REFLEXIVITY) { - constantOne = childProof->d_children[0]->d_node; + if (childProof->get_child(0)->d_id == theory::eq::MERGED_THROUGH_REFLEXIVITY) { + constantOne = childProof->get_child(0)->d_node; } else { - Assert(childProof->d_children[0]->d_node.getKind() == kind::EQUAL); - if ((childProof->d_children[0]->d_node[0] == indexOne) || - (childProof->d_children[0]->d_node[0] == indexTwo)) { - constantOne = childProof->d_children[0]->d_node[1]; + Assert(childProof->get_child(0)->d_node.getKind() == kind::EQUAL); + if ((childProof->get_child(0)->d_node[0] == indexOne) || + (childProof->get_child(0)->d_node[0] == indexTwo)) { + constantOne = childProof->get_child(0)->d_node[1]; } else { - constantOne = childProof->d_children[0]->d_node[0]; + constantOne = childProof->get_child(0)->d_node[0]; } } - if (childProof->d_children[1]->d_id == theory::eq::MERGED_THROUGH_REFLEXIVITY) { - constantTwo = childProof->d_children[1]->d_node; + if (childProof->get_child(1)->d_id == theory::eq::MERGED_THROUGH_REFLEXIVITY) { + constantTwo = childProof->get_child(1)->d_node; } else { - Assert(childProof->d_children[1]->d_node.getKind() == kind::EQUAL); - if ((childProof->d_children[1]->d_node[0] == indexOne) || - (childProof->d_children[1]->d_node[0] == indexTwo)) { - constantTwo = childProof->d_children[1]->d_node[1]; + Assert(childProof->get_child(1)->d_node.getKind() == kind::EQUAL); + if ((childProof->get_child(1)->d_node[0] == indexOne) || + (childProof->get_child(1)->d_node[0] == indexTwo)) { + constantTwo = childProof->get_child(1)->d_node[1]; } else { - constantTwo = childProof->d_children[1]->d_node[0]; + constantTwo = childProof->get_child(1)->d_node[0]; } } @@ -150,18 +150,15 @@ void ArrayProofReconstruction::notify(unsigned reasonType, Node reason, Node a, constantDisequalityProof->d_node = NodeManager::currentNM()->mkNode(kind::EQUAL, constantOne, constantTwo).negate(); - // Middle is where we need to insert the new disequality - std::vector::iterator middle = childProof->d_children.begin(); - ++middle; - - childProof->d_children.insert(middle, constantDisequalityProof); + // We need to insert the new disequality at position 1 + childProof->insert_child(1, constantDisequalityProof); childProof->d_id = theory::eq::MERGED_THROUGH_TRANS; childProof->d_node = NodeManager::currentNM()->mkNode(kind::EQUAL, indexOne, indexTwo).negate(); } - proof->d_children.push_back(childProof); + proof->add_child(childProof); } else { // This is the case of (i == k) because ((a[i]:=t)[k] != a[k]), @@ -176,7 +173,7 @@ void ArrayProofReconstruction::notify(unsigned reasonType, Node reason, Node a, eq::EqProof* childProof = new eq::EqProof; d_equalityEngine->explainEquality(reason[1][0], reason[1][1], false, equalities, childProof); - proof->d_children.push_back(childProof); + proof->add_child(childProof); } } diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp index f7084bec3..7a6e0bdfc 100644 --- a/src/theory/uf/equality_engine.cpp +++ b/src/theory/uf/equality_engine.cpp @@ -963,41 +963,41 @@ void EqualityEngine::explainEquality(TNode t1, TNode t2, bool polarity, std::vec if (eqpc->d_id == eq::MERGED_THROUGH_TRANS) { std::vector orderedChildren; bool nullCongruenceFound = false; - for (unsigned i = 0; i < eqpc->d_children.size(); ++i) { - if (eqpc->d_children[i]->d_id==eq::MERGED_THROUGH_CONGRUENCE && - eqpc->d_children[i]->d_node.isNull()) { + for (unsigned i = 0; i < eqpc->num_children(); ++i) { + if (eqpc->get_child(i)->d_id==eq::MERGED_THROUGH_CONGRUENCE && + eqpc->get_child(i)->d_node.isNull()) { nullCongruenceFound = true; Debug("pf::ee") << "Have congruence with empty d_node. Splitting..." << std::endl; - orderedChildren.insert(orderedChildren.begin(), eqpc->d_children[i]->d_children[0]); - orderedChildren.push_back(eqpc->d_children[i]->d_children[1]); + orderedChildren.insert(orderedChildren.begin(), eqpc->get_child(i)->get_child(0)); + orderedChildren.push_back(eqpc->get_child(i)->get_child(1)); } else { - orderedChildren.push_back(eqpc->d_children[i]); + orderedChildren.push_back(eqpc->get_child(i)); } } if (nullCongruenceFound) { - eqpc->d_children = orderedChildren; + eqpc->add_children(orderedChildren); Debug("pf::ee") << "Child proof's children have been reordered. It is now:" << std::endl; eqpc->debug_print("pf::ee", 1); } } - eqp->d_children.push_back(eqpc); + eqp->add_child(eqpc); } } if (eqp) { - if (eqp->d_children.size() == 0) { + if (eqp->num_children() == 0) { // Corner case where this is actually a disequality between two constants Debug("pf::ee") << "Encountered a constant disequality (not a transitivity proof): " << eqp->d_node << std::endl; Assert(eqp->d_node[0][0].isConst()); Assert(eqp->d_node[0][1].isConst()); eqp->d_id = MERGED_THROUGH_CONSTANTS; - } else if (eqp->d_children.size() == 1) { + } else if (eqp->num_children() == 1) { // The transitivity proof has just one child. Simplify. - EqProof* temp = eqp->d_children[0]; - eqp->d_children.clear(); + EqProof* temp = eqp->get_child(0); + eqp->remove_all_children(); *eqp = *temp; delete temp; } @@ -1126,8 +1126,8 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st EqProof * eqpc2 = eqpc ? new EqProof : NULL; getExplanation(f1.b, f2.b, equalities, eqpc2); if( eqpc ){ - eqpc->d_children.push_back( eqpc1 ); - eqpc->d_children.push_back( eqpc2 ); + eqpc->add_child( eqpc1 ); + eqpc->add_child( eqpc2 ); if( d_nodes[currentNode].getKind()==kind::EQUAL ){ //leave node null for now eqpc->d_node = Node::null(); @@ -1141,10 +1141,10 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st eqpc->d_node = NodeManager::currentNM()->mkNode(kind::PARTIAL_SELECT_1, d_nodes[f1.b]); // The first child is a PARTIAL_SELECT_0. // Give it a child so that we know what kind of (read) it is, when we dump to LFSC. - Assert(eqpc->d_children[0]->d_node.getKind() == kind::PARTIAL_SELECT_0); - Assert(eqpc->d_children[0]->d_children.size() == 0); + Assert(eqpc->get_child(0)->d_node.getKind() == kind::PARTIAL_SELECT_0); + Assert(eqpc->get_child(0)->num_children() == 0); - eqpc->d_children[0]->d_node = NodeManager::currentNM()->mkNode(kind::PARTIAL_SELECT_0, + eqpc->get_child(0)->d_node = NodeManager::currentNM()->mkNode(kind::PARTIAL_SELECT_0, d_nodes[f1.b]); } else { eqpc->d_node = NodeManager::currentNM()->mkNode(kind::PARTIAL_APPLY_UF, @@ -1170,7 +1170,7 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st EqProof * eqpc1 = eqpc ? new EqProof : NULL; getExplanation(eq.a, eq.b, equalities, eqpc1); if( eqpc ){ - eqpc->d_children.push_back( eqpc1 ); + eqpc->add_child( eqpc1 ); } Debug("equality") << pop; @@ -1195,7 +1195,7 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st EqProof * eqpcc = eqpc ? new EqProof : NULL; getExplanation(childId, getEqualityNode(childId).getFind(), equalities, eqpcc); if( eqpc ) { - eqpc->d_children.push_back( eqpcc ); + eqpc->add_child( eqpcc ); Debug("pf::ee") << "MERGED_THROUGH_CONSTANTS. Dumping the child proof" << std::endl; eqpc->debug_print("pf::ee", 1); @@ -1248,12 +1248,13 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st //---from Morgan--- if (eqpc != NULL && eqpc->d_id == MERGED_THROUGH_REFLEXIVITY) { if(eqpc->d_node.isNull()) { - Assert(eqpc->d_children.size() == 1); + Assert(eqpc->num_children() == 1); EqProof *p = eqpc; - eqpc = p->d_children[0]; + eqpc = p->take_child(0); + p->discard_children(); delete p; } else { - Assert(eqpc->d_children.empty()); + Assert(eqpc->num_children() == 0); } } //---end from Morgan--- @@ -1264,10 +1265,11 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st if (eqp) { if(eqp_trans.size() == 1) { *eqp = *eqp_trans[0]; + eqp_trans[0]->discard_children(); delete eqp_trans[0]; } else { eqp->d_id = MERGED_THROUGH_TRANS; - eqp->d_children.insert( eqp->d_children.end(), eqp_trans.begin(), eqp_trans.end() ); + eqp->add_children(eqp_trans); eqp->d_node = NodeManager::currentNM()->mkNode(kind::EQUAL, d_nodes[t1Id], d_nodes[t2Id]); } @@ -2217,6 +2219,11 @@ bool EqClassIterator::isFinished() const { return d_current == null_id; } +EqProof::~EqProof() { +Assert(this->refs == 0); +this->remove_all_children(); +} + void EqProof::debug_print(const char* c, unsigned tb, PrettyPrinter* prettyPrinter) const { for(unsigned i=0; i0 || !d_node.isNull() ) Debug( c ) << ","; Debug( c ) << std::endl; - d_children[i]->debug_print( c, tb+1, prettyPrinter ); + get_child(i)->debug_print( c, tb+1, prettyPrinter ); } } Debug( c ) << ")" << std::endl; diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h index 46ec7403b..2354aa76e 100644 --- a/src/theory/uf/equality_engine.h +++ b/src/theory/uf/equality_engine.h @@ -901,6 +901,9 @@ public: class EqProof { +private: + std::vector< EqProof * > d_children; + public: class PrettyPrinter { public: @@ -908,10 +911,55 @@ public: virtual std::string printTag(unsigned tag) = 0; }; - EqProof() : d_id(MERGED_THROUGH_REFLEXIVITY){} + EqProof() : d_id(MERGED_THROUGH_REFLEXIVITY), refs(0) {} + ~EqProof(); unsigned d_id; + unsigned refs; Node d_node; - std::vector< EqProof * > d_children; + void add_child(EqProof* child) { + child->refs++; + d_children.push_back(child); + } + void insert_child(size_t i, EqProof* child) { + child->refs++; + std::vector::iterator middle = d_children.begin(); + middle += i; + d_children.insert(middle, child); + } + void add_children(const std::vector children) { + for (size_t i = 0; i < children.size(); i++) { + this->add_child(children[i]); + } + } + void remove_all_children() { + for( unsigned i=0; irefs--; + if (d_children[i]->refs == 0) { + delete d_children[i]; +} + } + } + void discard_children() { + d_children.clear(); + } + void remove_last_child() { + EqProof* last_child = d_children[d_children.size() - 1]; + last_child->refs--; + if (last_child->refs == 0) { + delete last_child; + } + d_children.pop_back(); + } + size_t num_children() const { + return d_children.size(); + } + EqProof* get_child(size_t n) const { + return d_children[n]; + } + EqProof* take_child(size_t i) { + d_children[i]->refs--; +return d_children[i]; + } void debug_print(const char * c, unsigned tb = 0, PrettyPrinter* prettyPrinter = NULL) const; };/* class EqProof */ -- cgit v1.2.3