diff options
| -rw-r--r-- | src/proof/arith_proof.cpp | 173 | ||||
| -rw-r--r-- | src/proof/arith_proof.h | 22 | ||||
| -rw-r--r-- | src/proof/array_proof.cpp | 363 | ||||
| -rw-r--r-- | src/proof/array_proof.h | 17 | ||||
| -rw-r--r-- | src/proof/uf_proof.cpp | 204 | ||||
| -rw-r--r-- | src/proof/uf_proof.h | 31 | ||||
| -rw-r--r-- | src/theory/arrays/array_proof_reconstruction.cpp | 37 | ||||
| -rw-r--r-- | src/theory/arrays/array_proof_reconstruction.h | 3 | ||||
| -rw-r--r-- | src/theory/arrays/theory_arrays.cpp | 16 | ||||
| -rw-r--r-- | src/theory/arrays/theory_arrays.h | 5 | ||||
| -rw-r--r-- | src/theory/uf/equality_engine.cpp | 70 | ||||
| -rw-r--r-- | src/theory/uf/equality_engine.h | 18 | ||||
| -rw-r--r-- | src/theory/uf/theory_uf.cpp | 7 |
13 files changed, 518 insertions, 448 deletions
diff --git a/src/proof/arith_proof.cpp b/src/proof/arith_proof.cpp index 03de1ca4f..dd3ac0bde 100644 --- a/src/proof/arith_proof.cpp +++ b/src/proof/arith_proof.cpp @@ -14,12 +14,14 @@ ** \todo document this file **/ +#include "proof/arith_proof.h" + +#include <memory> +#include <stack> -#include "proof/theory_proof.h" #include "proof/proof_manager.h" -#include "proof/arith_proof.h" +#include "proof/theory_proof.h" #include "theory/arith/theory_arith.h" -#include <stack> namespace CVC4 { @@ -70,56 +72,64 @@ void ProofArith::toStream(std::ostream& out) { Trace("theory-proof-debug") << "; Print Arith proof..." << std::endl; //AJR : carry this further? ProofLetMap map; - toStreamLFSC(out, ProofManager::getArithProof(), d_proof, map); + toStreamLFSC(out, ProofManager::getArithProof(), *d_proof, map); } -void ProofArith::toStreamLFSC(std::ostream& out, TheoryProof * tp, theory::eq::EqProof * pf, const ProofLetMap& map) { +void ProofArith::toStreamLFSC(std::ostream& out, TheoryProof* tp, + const theory::eq::EqProof& pf, + const ProofLetMap& map) { Debug("lfsc-arith") << "Printing arith proof in LFSC : " << std::endl; - pf->debug_print("lfsc-arith"); + pf.debug_print("lfsc-arith"); Debug("lfsc-arith") << std::endl; - toStreamRecLFSC( out, tp, pf, 0, map ); + toStreamRecLFSC(out, tp, pf, 0, map); } -Node ProofArith::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::EqProof * pf, unsigned tb, const ProofLetMap& map) { - Debug("pf::arith") << std::endl << std::endl << "toStreamRecLFSC called. tb = " << tb << " . proof:" << std::endl; - pf->debug_print("pf::arith"); +Node ProofArith::toStreamRecLFSC(std::ostream& out, TheoryProof* tp, + const theory::eq::EqProof& pf, unsigned tb, + const ProofLetMap& map) { + Debug("pf::arith") << std::endl + << std::endl + << "toStreamRecLFSC called. tb = " << tb + << " . proof:" << std::endl; + pf.debug_print("pf::arith"); Debug("pf::arith") << std::endl; 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.d_id == theory::eq::MERGED_THROUGH_TRANS); + Assert(!pf.d_node.isNull()); + Assert(pf.d_children.size() >= 2); int neg = -1; - theory::eq::EqProof subTrans; - subTrans.d_id = theory::eq::MERGED_THROUGH_TRANS; - subTrans.d_node = pf->d_node; + std::shared_ptr<theory::eq::EqProof> subTrans = + std::make_shared<theory::eq::EqProof>(); + subTrans->d_id = theory::eq::MERGED_THROUGH_TRANS; + subTrans->d_node = pf.d_node; size_t i = 0; - while (i < pf->d_children.size()) { + while (i < pf.d_children.size()) { // 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.d_children[i]->d_node.isNull() && pf.d_children[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.d_children[i]->d_id==theory::eq::MERGED_THROUGH_CONGRUENCE && pf.d_children[i]->d_node.isNull()) { Debug("pf::arith") << "Handling congruence over equalities" << std::endl; // Gather the sequence of consecutive congruence closures. - std::vector<const theory::eq::EqProof *> congruenceClosures; + std::vector<std::shared_ptr<const theory::eq::EqProof>> congruenceClosures; 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.d_children.size() && + pf.d_children[i + count]->d_id==theory::eq::MERGED_THROUGH_CONGRUENCE && + pf.d_children[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.d_children[i+count]->debug_print("pf::arith"); + congruenceClosures.push_back(pf.d_children[i+count]); } Debug("pf::arith") << "Total number of congruences found: " << congruenceClosures.size() << std::endl; @@ -133,9 +143,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.d_children.size()) || + (!pf.d_children[i + count]->d_node.isNull() && + pf.d_children[i + count]->d_node.getKind() == kind::NOT)) { Debug("pf::arith") << "Target does not appear after" << std::endl; targetAppearsAfter = false; } @@ -144,37 +154,37 @@ Node ProofArith::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq Assert(targetAppearsBefore != targetAppearsAfter); // Begin breaking up the congruences and ordering the equalities correctly. - std::vector<theory::eq::EqProof *> orderedEqualities; + std::vector<std::shared_ptr<theory::eq::EqProof>> orderedEqualities; // Insert target clause first. if (targetAppearsBefore) { - orderedEqualities.push_back(pf->d_children[i - 1]); + orderedEqualities.push_back(pf.d_children[i - 1]); // The target has already been added to subTrans; remove it. - subTrans.d_children.pop_back(); + subTrans->d_children.pop_back(); } else { - orderedEqualities.push_back(pf->d_children[i + count]); + orderedEqualities.push_back(pf.d_children[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.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]); } } 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.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]); } } // Copy the result into the main transitivity proof. - subTrans.d_children.insert(subTrans.d_children.end(), orderedEqualities.begin(), orderedEqualities.end()); + subTrans->d_children.insert(subTrans->d_children.end(), orderedEqualities.begin(), orderedEqualities.end()); // Increase i to skip over the children that have been processed. i += count; @@ -185,7 +195,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->d_children.push_back(pf.d_children[i]); ++i; } } @@ -193,16 +203,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) { - n1 = toStreamRecLFSC(ss, tp, &subTrans, 1, map); + //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) { + 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->d_children[0]), 1, map); + Debug("pf::arith") << "\nsubTrans unique child " << subTrans->d_children[0]->d_id << " was proven\ngot: " << n1 << std::endl; } - Node n2 = pf->d_children[neg]->d_node; + Node n2 = pf.d_children[neg]->d_node; Assert(n2.getKind() == kind::NOT); out << "(clausify_false (contra _ "; Debug("pf::arith") << "\nhave proven: " << n1 << std::endl; @@ -228,12 +238,14 @@ Node ProofArith::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq return Node(); } - switch(pf->d_id) { + switch(pf.d_id) { case theory::eq::MERGED_THROUGH_CONGRUENCE: { Debug("pf::arith") << "\nok, looking at congruence:\n"; - pf->debug_print("pf::arith"); + pf.debug_print("pf::arith"); std::stack<const theory::eq::EqProof*> 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->d_children[0].get()) { 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); @@ -245,10 +257,10 @@ Node ProofArith::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq 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->d_children[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->d_children[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"; @@ -316,7 +328,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->d_children[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"; @@ -373,27 +385,27 @@ 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.d_node.isNull()); + Assert(pf.d_children.empty()); out << "(refl _ "; - tp->printTerm(NodeManager::currentNM()->toExpr(pf->d_node), out, map); + tp->printTerm(NodeManager::currentNM()->toExpr(pf.d_node), out, map); out << ")"; - return eqNode(pf->d_node, pf->d_node); + return eqNode(pf.d_node, pf.d_node); case theory::eq::MERGED_THROUGH_EQUALITY: - Assert(!pf->d_node.isNull()); - Assert(pf->d_children.empty()); - out << ProofManager::getLitName(pf->d_node.negate()); - return pf->d_node; + Assert(!pf.d_node.isNull()); + Assert(pf.d_children.empty()); + 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.d_node.isNull()); + Assert(pf.d_children.size() >= 2); std::stringstream ss; Debug("pf::arith") << "\ndoing trans proof[[\n"; - pf->debug_print("pf::arith"); + 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.d_children[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 +417,7 @@ Node ProofArith::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq std::map<size_t, Node> childToStream; - for(size_t i = 1; i < pf->d_children.size(); ++i) { + for(size_t i = 1; i < pf.d_children.size(); ++i) { std::stringstream ss1(ss.str()), ss2; ss.str(""); @@ -415,7 +427,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.d_children[i]), tb + 1, map); childToStream[i] = n2; } @@ -446,9 +458,10 @@ 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.d_children.size() && !sequenceOver) { std::stringstream dontCare; - nodeAfterEqualitySequence = toStreamRecLFSC(dontCare, tp, pf->d_children[j], tb + 1, map ); + nodeAfterEqualitySequence = toStreamRecLFSC( + dontCare, tp, *(pf.d_children[j]), tb + 1, map); if (((nodeAfterEqualitySequence[0] == n1[0]) && (nodeAfterEqualitySequence[1] == n1[1])) || ((nodeAfterEqualitySequence[0] == n1[1]) && (nodeAfterEqualitySequence[1] == n1[0]))) { @@ -466,17 +479,17 @@ Node ProofArith::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq Debug("pf::arith") << "Equality sequence of even length" << std::endl; Debug("pf::arith") << "n1 is: " << n1 << std::endl; Debug("pf::arith") << "n2 is: " << n2 << std::endl; - Debug("pf::arith") << "pf-d_node is: " << pf->d_node << std::endl; + Debug("pf::arith") << "pf-d_node is: " << pf.d_node << std::endl; Debug("pf::arith") << "Next node is: " << nodeAfterEqualitySequence << std::endl; ss << "(trans _ _ _ _ "; - // If the sequence is at the very end of the transitivity proof, use pf->d_node to guide us. + // If the sequence is at the very end of the transitivity proof, use pf.d_node to guide us. if (!sequenceOver) { - if (match(n1[0], pf->d_node[0])) { + if (match(n1[0], pf.d_node[0])) { n1 = eqNode(n1[0], n1[0]); ss << ss1.str() << " (symm _ _ _ " << ss1.str() << ")"; - } else if (match(n1[1], pf->d_node[1])) { + } else if (match(n1[1], pf.d_node[1])) { n1 = eqNode(n1[1], n1[1]); ss << " (symm _ _ _ " << ss1.str() << ")" << ss1.str(); } else { @@ -572,7 +585,7 @@ Node ProofArith::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq Warning() << "\n\ntrans proof failure at step " << i << "\n\n"; Warning() << "0 proves " << n1 << "\n"; Warning() << "1 proves " << n2 << "\n\n"; - pf->debug_print("pf::arith",0); + pf.debug_print("pf::arith",0); //toStreamRec(Warning.getStream(), pf, 0); Warning() << "\n\n"; Unreachable(); @@ -613,11 +626,11 @@ Node ProofArith::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq } default: - Assert(!pf->d_node.isNull()); - Assert(pf->d_children.empty()); - Debug("pf::arith") << "theory proof: " << pf->d_node << " by rule " << int(pf->d_id) << std::endl; + Assert(!pf.d_node.isNull()); + Assert(pf.d_children.empty()); + Debug("pf::arith") << "theory proof: " << pf.d_node << " by rule " << int(pf.d_id) << std::endl; AlwaysAssert(false); - return pf->d_node; + return pf.d_node; } } diff --git a/src/proof/arith_proof.h b/src/proof/arith_proof.h index 3de53f866..b36909f78 100644 --- a/src/proof/arith_proof.h +++ b/src/proof/arith_proof.h @@ -19,6 +19,7 @@ #ifndef __CVC4__ARITH__PROOF_H #define __CVC4__ARITH__PROOF_H +#include <memory> #include <unordered_set> #include "expr/expr.h" @@ -30,17 +31,20 @@ namespace CVC4 { //proof object outputted by TheoryArith class ProofArith : public Proof { -private: - static Node toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::EqProof * pf, unsigned tb, const ProofLetMap& map); -public: - ProofArith( theory::eq::EqProof * pf ) : d_proof( pf ) {} - //it is simply an equality engine proof - theory::eq::EqProof * d_proof; - void toStream(std::ostream& out); - static void toStreamLFSC(std::ostream& out, TheoryProof * tp, theory::eq::EqProof * pf, const ProofLetMap& map); + public: + ProofArith(std::shared_ptr<theory::eq::EqProof> pf) : d_proof(pf) {} + void toStream(std::ostream& out) override; + private: + static void toStreamLFSC(std::ostream& out, TheoryProof* tp, + const theory::eq::EqProof& pf, + const ProofLetMap& map); + static Node toStreamRecLFSC(std::ostream& out, TheoryProof* tp, + const theory::eq::EqProof& pf, + unsigned tb, const ProofLetMap& map); + // it is simply an equality engine proof + std::shared_ptr<theory::eq::EqProof> d_proof; }; - namespace theory { namespace arith { class TheoryArith; diff --git a/src/proof/array_proof.cpp b/src/proof/array_proof.cpp index fab9a896d..488c52e33 100644 --- a/src/proof/array_proof.cpp +++ b/src/proof/array_proof.cpp @@ -115,8 +115,8 @@ inline static bool match(TNode n1, TNode n2) { return true; } -ProofArray::ProofArray(theory::eq::EqProof* pf, unsigned row, unsigned row1, - unsigned ext) +ProofArray::ProofArray(std::shared_ptr<theory::eq::EqProof> pf, unsigned row, + unsigned row1, unsigned ext) : d_proof(pf), d_reasonRow(row), d_reasonRow1(row1), d_reasonExt(ext) {} void ProofArray::toStream(std::ostream& out) { @@ -126,69 +126,71 @@ void ProofArray::toStream(std::ostream& out) { void ProofArray::toStream(std::ostream& out, const ProofLetMap& map) { Trace("pf::array") << "; Print Array proof..." << std::endl; - toStreamLFSC(out, ProofManager::getArrayProof(), d_proof, map); + toStreamLFSC(out, ProofManager::getArrayProof(), *d_proof, map); Debug("pf::array") << "; Print Array proof done!" << std::endl; } void ProofArray::toStreamLFSC(std::ostream& out, TheoryProof* tp, - theory::eq::EqProof* pf, const ProofLetMap& map) { + const theory::eq::EqProof& pf, + const ProofLetMap& map) { Debug("pf::array") << "Printing array proof in LFSC : " << std::endl; ArrayProofPrinter proofPrinter(d_reasonRow, d_reasonRow1, d_reasonExt); - pf->debug_print("pf::array", 0, &proofPrinter); + pf.debug_print("pf::array", 0, &proofPrinter); Debug("pf::array") << std::endl; toStreamRecLFSC(out, tp, pf, 0, map); Debug("pf::array") << "Printing array proof in LFSC DONE" << std::endl; } -Node ProofArray::toStreamRecLFSC(std::ostream& out, - TheoryProof* tp, - theory::eq::EqProof* pf, - unsigned tb, +Node ProofArray::toStreamRecLFSC(std::ostream& out, TheoryProof* tp, + const theory::eq::EqProof& pf, unsigned tb, const ProofLetMap& map) { - - Debug("pf::array") << std::endl << std::endl << "toStreamRecLFSC called. tb = " << tb << " . proof:" << std::endl; + Debug("pf::array") << std::endl + << std::endl + << "toStreamRecLFSC called. tb = " << tb + << " . proof:" << std::endl; ArrayProofPrinter proofPrinter(d_reasonRow, d_reasonRow1, d_reasonExt); - pf->debug_print("pf::array", 0, &proofPrinter); + pf.debug_print("pf::array", 0, &proofPrinter); Debug("pf::array") << std::endl; 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.d_id == theory::eq::MERGED_THROUGH_TRANS); + Assert(!pf.d_node.isNull()); + Assert(pf.d_children.size() >= 2); int neg = -1; - theory::eq::EqProof subTrans; - subTrans.d_id = theory::eq::MERGED_THROUGH_TRANS; - subTrans.d_node = pf->d_node; + std::shared_ptr<theory::eq::EqProof> subTrans = + std::make_shared<theory::eq::EqProof>(); + subTrans->d_id = theory::eq::MERGED_THROUGH_TRANS; + 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.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); // 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.d_children[i]->d_node.isNull() && pf.d_children[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.d_children[i]->d_id==theory::eq::MERGED_THROUGH_CONGRUENCE && pf.d_children[i]->d_node.isNull()) { Debug("pf::array") << "Handling congruence over equalities" << std::endl; // Gather the sequence of consecutive congruence closures. - std::vector<const theory::eq::EqProof *> congruenceClosures; + std::vector<std::shared_ptr<const theory::eq::EqProof>> congruenceClosures; 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.d_children.size() && + pf.d_children[i + count]->d_id==theory::eq::MERGED_THROUGH_CONGRUENCE && + pf.d_children[i + count]->d_node.isNull(); ++count) { Debug("pf::array") << "Found a congruence: " << std::endl; - pf->d_children[i + count]->debug_print("pf::array", 0, &proofPrinter); - congruenceClosures.push_back(pf->d_children[i + count]); + pf.d_children[i + count]->debug_print("pf::array", 0, &proofPrinter); + congruenceClosures.push_back(pf.d_children[i + count]); } Debug("pf::array") << "Total number of congruences found: " << congruenceClosures.size() << std::endl; @@ -202,9 +204,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.d_children.size()) || + (!pf.d_children[i + count]->d_node.isNull() && + pf.d_children[i + count]->d_node.getKind() == kind::NOT)) { Debug("pf::array") << "Target does not appear after" << std::endl; targetAppearsAfter = false; } @@ -213,36 +215,36 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, Assert(targetAppearsBefore != targetAppearsAfter); // Begin breaking up the congruences and ordering the equalities correctly. - std::vector<theory::eq::EqProof *> orderedEqualities; + std::vector<std::shared_ptr<theory::eq::EqProof>> orderedEqualities; // Insert target clause first. if (targetAppearsBefore) { - orderedEqualities.push_back(pf->d_children[i - 1]); + orderedEqualities.push_back(pf.d_children[i - 1]); // The target has already been added to subTrans; remove it. - subTrans.d_children.pop_back(); + subTrans->d_children.pop_back(); } else { - orderedEqualities.push_back(pf->d_children[i + count]); + orderedEqualities.push_back(pf.d_children[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.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]); } } 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.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]); } } // Copy the result into the main transitivity proof. - subTrans.d_children.insert(subTrans.d_children.end(), orderedEqualities.begin(), orderedEqualities.end()); + subTrans->d_children.insert(subTrans->d_children.end(), orderedEqualities.begin(), orderedEqualities.end()); // Increase i to skip over the children that have been processed. i += count; @@ -253,7 +255,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->d_children.push_back(pf.d_children[i]); ++i; } } @@ -261,42 +263,44 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, bool disequalityFound = (neg >= 0); if (!disequalityFound) { Debug("pf::array") << "A disequality was NOT found. UNSAT due to merged constants" << std::endl; - Debug("pf::array") << "Proof for: " << pf->d_node << std::endl; - Assert(pf->d_node.getKind() == kind::EQUAL); - Assert(pf->d_node.getNumChildren() == 2); - Assert (pf->d_node[0].isConst() && pf->d_node[1].isConst()); + Debug("pf::array") << "Proof for: " << pf.d_node << std::endl; + Assert(pf.d_node.getKind() == kind::EQUAL); + Assert(pf.d_node.getNumChildren() == 2); + Assert (pf.d_node[0].isConst() && pf.d_node[1].isConst()); } 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) { - n1 = toStreamRecLFSC(ss, tp, &subTrans, 1, map); + //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) { + 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->d_children[0]), 1, map); + Debug("mgdx") << "\nsubTrans unique child " + << subTrans->d_children[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.d_children[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.d_children[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.d_children[neg]->d_id == d_reasonExt) || + (pf.d_children[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.d_children[neg], 1, map); out << ss2.str(); } else if (n2[0].getKind() == kind::APPLY_UF) { out << "(trans _ _ _ _ "; @@ -316,7 +320,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, out << " " << ProofManager::getLitName(n2[0]); } } else { - Node n2 = pf->d_node; + Node n2 = pf.d_node; Assert(n2.getKind() == kind::EQUAL); Assert((n1[0] == n2[0] && n1[1] == n2[1]) || (n1[1] == n2[0] && n1[0] == n2[1])); @@ -332,13 +336,15 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, return Node(); } - if (pf->d_id == theory::eq::MERGED_THROUGH_CONGRUENCE) { + if (pf.d_id == theory::eq::MERGED_THROUGH_CONGRUENCE) { Debug("mgd") << "\nok, looking at congruence:\n"; - pf->debug_print("mgd", 0, &proofPrinter); + pf.debug_print("mgd", 0, &proofPrinter); std::stack<const theory::eq::EqProof*> stk; - for(const theory::eq::EqProof* pf2 = pf; pf2->d_id == theory::eq::MERGED_THROUGH_CONGRUENCE; pf2 = pf2->d_children[0]) { - Debug("mgd") << "Looking at pf2 with d_node: " << pf2->d_node << std::endl; - + for (const theory::eq::EqProof* pf2 = &pf; + pf2->d_id == theory::eq::MERGED_THROUGH_CONGRUENCE; + pf2 = pf2->d_children[0].get()) { + Debug("mgd") << "Looking at pf2 with d_node: " << pf2->d_node + << std::endl; Assert(!pf2->d_node.isNull()); Assert(pf2->d_node.getKind() == kind::PARTIAL_APPLY_UF || pf2->d_node.getKind() == kind::BUILTIN || @@ -359,10 +365,10 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, 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->d_children[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->d_children[1]), tb + 1, map); Debug("mgd") << "\nok, in FIRST cong[" << stk.size() << "]" << "\n"; @@ -478,7 +484,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->d_children[1]), tb + 1, map); Debug("mgd") << "\nok, in cong[" << stk.size() << "]" << "\n"; Debug("mgd") << "looking at " << pf2->d_node << "\n"; @@ -579,28 +585,28 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, return n; } - else if (pf->d_id == theory::eq::MERGED_THROUGH_REFLEXIVITY) { - Assert(!pf->d_node.isNull()); - Assert(pf->d_children.empty()); + else if (pf.d_id == theory::eq::MERGED_THROUGH_REFLEXIVITY) { + Assert(!pf.d_node.isNull()); + Assert(pf.d_children.empty()); out << "(refl _ "; - tp->printTerm(NodeManager::currentNM()->toExpr(pf->d_node), out, map); + tp->printTerm(NodeManager::currentNM()->toExpr(pf.d_node), out, map); out << ")"; - return eqNode(pf->d_node, pf->d_node); + return eqNode(pf.d_node, pf.d_node); } - else if (pf->d_id == theory::eq::MERGED_THROUGH_EQUALITY) { - Assert(!pf->d_node.isNull()); - Assert(pf->d_children.empty()); - 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()); - return pf->d_node; + else if (pf.d_id == theory::eq::MERGED_THROUGH_EQUALITY) { + Assert(!pf.d_node.isNull()); + Assert(pf.d_children.empty()); + 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()); + return pf.d_node; } - else if (pf->d_id == theory::eq::MERGED_THROUGH_CONSTANTS) { - Debug("pf::array") << "Proof for: " << pf->d_node << std::endl; - Assert(pf->d_node.getKind() == kind::NOT); - Node n = pf->d_node[0]; + else if (pf.d_id == theory::eq::MERGED_THROUGH_CONSTANTS) { + Debug("pf::array") << "Proof for: " << pf.d_node << std::endl; + Assert(pf.d_node.getKind() == kind::NOT); + Node n = pf.d_node[0]; Assert(n.getKind() == kind::EQUAL); Assert(n.getNumChildren() == 2); Assert(n[0].isConst() && n[1].isConst()); @@ -609,23 +615,23 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, n[0].toExpr(), n[1].toExpr(), map); - return pf->d_node; + return pf.d_node; } - else if (pf->d_id == theory::eq::MERGED_THROUGH_TRANS) { + else if (pf.d_id == theory::eq::MERGED_THROUGH_TRANS) { bool firstNeg = false; bool secondNeg = false; - Assert(!pf->d_node.isNull()); - Assert(pf->d_children.size() >= 2); + Assert(!pf.d_node.isNull()); + Assert(pf.d_children.size() >= 2); std::stringstream ss; Debug("mgd") << "\ndoing trans proof[[\n"; - pf->debug_print("mgd", 0, &proofPrinter); + pf.debug_print("mgd", 0, &proofPrinter); Debug("mgd") << "\n"; - pf->d_children[0]->d_node = simplifyBooleanNode(pf->d_children[0]->d_node); + pf.d_children[0]->d_node = simplifyBooleanNode(pf.d_children[0]->d_node); - Node n1 = toStreamRecLFSC(ss, tp, pf->d_children[0], tb + 1, map); + Node n1 = toStreamRecLFSC(ss, tp, *(pf.d_children[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"; @@ -637,7 +643,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, std::map<size_t, Node> childToStream; - for(size_t i = 1; i < pf->d_children.size(); ++i) { + for(size_t i = 1; i < pf.d_children.size(); ++i) { std::stringstream ss1(ss.str()), ss2; ss.str(""); @@ -645,8 +651,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.d_children[i]->d_id != theory::eq::MERGED_THROUGH_CONGRUENCE) + pf.d_children[i]->d_node = simplifyBooleanNode(pf.d_children[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. @@ -654,7 +660,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.d_children[i]), tb + 1, map); childToStream[i] = n2; } @@ -688,9 +694,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.d_children.size() && !sequenceOver) { std::stringstream dontCare; - nodeAfterEqualitySequence = toStreamRecLFSC(dontCare, tp, pf->d_children[j], tb + 1, map ); + nodeAfterEqualitySequence = toStreamRecLFSC(dontCare, tp, *(pf.d_children[j]), tb + 1, map ); if (((nodeAfterEqualitySequence[0] == n1[0]) && (nodeAfterEqualitySequence[1] == n1[1])) || ((nodeAfterEqualitySequence[0] == n1[1]) && (nodeAfterEqualitySequence[1] == n1[0]))) { @@ -708,17 +714,17 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, Debug("pf::array") << "Equality sequence of even length" << std::endl; Debug("pf::array") << "n1 is: " << n1 << std::endl; Debug("pf::array") << "n2 is: " << n2 << std::endl; - Debug("pf::array") << "pf-d_node is: " << pf->d_node << std::endl; + Debug("pf::array") << "pf-d_node is: " << pf.d_node << std::endl; Debug("pf::array") << "Next node is: " << nodeAfterEqualitySequence << std::endl; ss << "(trans _ _ _ _ "; - // If the sequence is at the very end of the transitivity proof, use pf->d_node to guide us. + // If the sequence is at the very end of the transitivity proof, use pf.d_node to guide us. if (!sequenceOver) { - if (match(n1[0], pf->d_node[0])) { + if (match(n1[0], pf.d_node[0])) { n1 = eqNode(n1[0], n1[0]); ss << ss1.str() << " (symm _ _ _ " << ss1.str() << ")"; - } else if (match(n1[1], pf->d_node[1])) { + } else if (match(n1[1], pf.d_node[1])) { n1 = eqNode(n1[1], n1[1]); ss << " (symm _ _ _ " << ss1.str() << ")" << ss1.str(); } else { @@ -847,7 +853,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, Warning() << "\n\ntrans proof failure at step " << i << "\n\n"; Warning() << "0 proves " << n1 << "\n"; Warning() << "1 proves " << n2 << "\n\n"; - pf->debug_print("mgdx", 0, &proofPrinter); + pf.debug_print("mgdx", 0, &proofPrinter); //toStreamRec(Warning.getStream(), pf, 0); Warning() << "\n\n"; Unreachable(); @@ -895,46 +901,46 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, return n1; } - else if (pf->d_id == d_reasonRow) { - Debug("mgd") << "row lemma: " << pf->d_node << std::endl; - Assert(pf->d_node.getKind() == kind::EQUAL); + else if (pf.d_id == d_reasonRow) { + Debug("mgd") << "row lemma: " << pf.d_node << std::endl; + Assert(pf.d_node.getKind() == kind::EQUAL); - if (pf->d_node[1].getKind() == kind::SELECT) { + if (pf.d_node[1].getKind() == kind::SELECT) { // This is the case where ((a[i]:=t)[k] == a[k]), and the sub-proof explains why (i != k). TNode t1, t2, t3, t4; Node ret; - if(pf->d_node[1].getKind() == kind::SELECT && - pf->d_node[1][0].getKind() == kind::STORE && - pf->d_node[0].getKind() == kind::SELECT && - pf->d_node[0][0] == pf->d_node[1][0][0] && - pf->d_node[0][1] == pf->d_node[1][1]) { - t2 = pf->d_node[1][0][1]; - t3 = pf->d_node[1][1]; - t1 = pf->d_node[0][0]; - t4 = pf->d_node[1][0][2]; - ret = pf->d_node[1].eqNode(pf->d_node[0]); + if(pf.d_node[1].getKind() == kind::SELECT && + pf.d_node[1][0].getKind() == kind::STORE && + pf.d_node[0].getKind() == kind::SELECT && + pf.d_node[0][0] == pf.d_node[1][0][0] && + pf.d_node[0][1] == pf.d_node[1][1]) { + t2 = pf.d_node[1][0][1]; + t3 = pf.d_node[1][1]; + t1 = pf.d_node[0][0]; + t4 = pf.d_node[1][0][2]; + ret = pf.d_node[1].eqNode(pf.d_node[0]); Debug("mgd") << "t1 " << t1 << "\nt2 " << t2 << "\nt3 " << t3 << "\nt4 " << t4 << "\n"; } else { - Assert(pf->d_node[0].getKind() == kind::SELECT && - pf->d_node[0][0].getKind() == kind::STORE && - pf->d_node[1].getKind() == kind::SELECT && - pf->d_node[1][0] == pf->d_node[0][0][0] && - pf->d_node[1][1] == pf->d_node[0][1]); - t2 = pf->d_node[0][0][1]; - t3 = pf->d_node[0][1]; - t1 = pf->d_node[1][0]; - t4 = pf->d_node[0][0][2]; - ret = pf->d_node; + Assert(pf.d_node[0].getKind() == kind::SELECT && + pf.d_node[0][0].getKind() == kind::STORE && + pf.d_node[1].getKind() == kind::SELECT && + pf.d_node[1][0] == pf.d_node[0][0][0] && + pf.d_node[1][1] == pf.d_node[0][1]); + t2 = pf.d_node[0][0][1]; + t3 = pf.d_node[0][1]; + t1 = pf.d_node[1][0]; + t4 = pf.d_node[0][0][2]; + ret = pf.d_node; Debug("mgd") << "t1 " << t1 << "\nt2 " << t2 << "\nt3 " << t3 << "\nt4 " << t4 << "\n"; } // inner index != outer index // t3 is the outer index - Assert(pf->d_children.size() == 1); + Assert(pf.d_children.size() == 1); std::stringstream ss; - Node subproof = toStreamRecLFSC(ss, tp, pf->d_children[0], tb + 1, map); + Node subproof = toStreamRecLFSC(ss, tp, *(pf.d_children[0]), tb + 1, map); out << "(row _ _ "; tp->printTerm(t2.toExpr(), out, map); @@ -947,7 +953,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.d_children[0]->d_node is: " << pf.d_children[0]->d_node << ". t3 is: " << t3 << std::endl << "subproof is: " << subproof << std::endl; @@ -1020,7 +1026,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.d_children[0]->d_node is: " << pf.d_children[0]->d_node << std::endl; // This is the case where (i == k), and the sub-proof explains why ((a[i]:=t)[k] != a[k]) @@ -1033,19 +1039,19 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, TNode t1, t2, t3, t4; Node ret; - // pf->d_node is an equality, i==k. - t1 = pf->d_node[0]; - t2 = pf->d_node[1]; + // pf.d_node is an equality, i==k. + 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.d_children[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.d_children[0]->d_node[0][0].getKind() == kind::SELECT && + pf.d_children[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.d_children[0]->d_node[0][1].getKind() == kind::SELECT && + pf.d_children[0]->d_node[0][1][0].getKind() == kind::STORE) { side = 1; } else { @@ -1055,18 +1061,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]; - ret = pf->d_node; + t3 = pf.d_children[0]->d_node[0][side][0][0]; + t4 = pf.d_children[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.d_children[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.d_children.size() == 1); std::stringstream ss; - Node subproof = toStreamRecLFSC(ss, tp, pf->d_children[0], tb + 1, map); + Node subproof = toStreamRecLFSC(ss, tp, *(pf.d_children[0]), tb + 1, map); Debug("pf::array") << "Subproof is: " << ss.str() << std::endl; @@ -1100,29 +1106,29 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, } } - else if (pf->d_id == d_reasonRow1) { - Debug("mgd") << "row1 lemma: " << pf->d_node << std::endl; - Assert(pf->d_node.getKind() == kind::EQUAL); + else if (pf.d_id == d_reasonRow1) { + Debug("mgd") << "row1 lemma: " << pf.d_node << std::endl; + Assert(pf.d_node.getKind() == kind::EQUAL); TNode t1, t2, t3; Node ret; - if(pf->d_node[1].getKind() == kind::SELECT && - pf->d_node[1][0].getKind() == kind::STORE && - pf->d_node[1][0][1] == pf->d_node[1][1] && - pf->d_node[1][0][2] == pf->d_node[0]) { - t1 = pf->d_node[1][0][0]; - t2 = pf->d_node[1][0][1]; - t3 = pf->d_node[0]; - ret = pf->d_node[1].eqNode(pf->d_node[0]); + if(pf.d_node[1].getKind() == kind::SELECT && + pf.d_node[1][0].getKind() == kind::STORE && + pf.d_node[1][0][1] == pf.d_node[1][1] && + pf.d_node[1][0][2] == pf.d_node[0]) { + t1 = pf.d_node[1][0][0]; + t2 = pf.d_node[1][0][1]; + t3 = pf.d_node[0]; + ret = pf.d_node[1].eqNode(pf.d_node[0]); Debug("mgd") << "t1 " << t1 << "\nt2 " << t2 << "\nt3 " << t3 << "\n"; } else { - Assert(pf->d_node[0].getKind() == kind::SELECT && - pf->d_node[0][0].getKind() == kind::STORE && - pf->d_node[0][0][1] == pf->d_node[0][1] && - pf->d_node[0][0][2] == pf->d_node[1]); - t1 = pf->d_node[0][0][0]; - t2 = pf->d_node[0][0][1]; - t3 = pf->d_node[1]; - ret = pf->d_node; + Assert(pf.d_node[0].getKind() == kind::SELECT && + pf.d_node[0][0].getKind() == kind::STORE && + pf.d_node[0][0][1] == pf.d_node[0][1] && + pf.d_node[0][0][2] == pf.d_node[1]); + t1 = pf.d_node[0][0][0]; + t2 = pf.d_node[0][0][1]; + t3 = pf.d_node[1]; + ret = pf.d_node; Debug("mgd") << "t1 " << t1 << "\nt2 " << t2 << "\nt3 " << t3 << "\n"; } out << "(row1 _ _ "; @@ -1135,23 +1141,20 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, return ret; } - else if (pf->d_id == d_reasonExt) { - theory::eq::EqProof *child_proof; - - Assert(pf->d_node.getKind() == kind::NOT); - Assert(pf->d_node[0].getKind() == kind::EQUAL); - Assert(pf->d_children.size() == 1); - - child_proof = pf->d_children[0]; + else if (pf.d_id == d_reasonExt) { + Assert(pf.d_node.getKind() == kind::NOT); + Assert(pf.d_node[0].getKind() == kind::EQUAL); + Assert(pf.d_children.size() == 1); + std::shared_ptr<theory::eq::EqProof> child_proof = pf.d_children[0]; Assert(child_proof->d_node.getKind() == kind::NOT); Assert(child_proof->d_node[0].getKind() == kind::EQUAL); - Debug("mgd") << "EXT lemma: " << pf->d_node << std::endl; + Debug("mgd") << "EXT lemma: " << pf.d_node << std::endl; TNode t1, t2, t3; t1 = child_proof->d_node[0][0]; t2 = child_proof->d_node[0][1]; - t3 = pf->d_node[0][0][1]; + t3 = pf.d_node[0][0][1]; Debug("mgd") << "t1 " << t1 << "\nt2 " << t2 << "\nt3 " << t3 << "\n"; @@ -1161,15 +1164,15 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, out << ProofManager::getArrayProof()->skolemToLiteral(t3.toExpr()); out << ")"; - return pf->d_node; + return pf.d_node; } else { - Assert(!pf->d_node.isNull()); - Assert(pf->d_children.empty()); - Debug("mgd") << "theory proof: " << pf->d_node << " by rule " << int(pf->d_id) << std::endl; + Assert(!pf.d_node.isNull()); + Assert(pf.d_children.empty()); + Debug("mgd") << "theory proof: " << pf.d_node << " by rule " << int(pf.d_id) << std::endl; AlwaysAssert(false); - return pf->d_node; + return pf.d_node; } } diff --git a/src/proof/array_proof.h b/src/proof/array_proof.h index f40f13ea6..df8cb58a2 100644 --- a/src/proof/array_proof.h +++ b/src/proof/array_proof.h @@ -19,6 +19,7 @@ #ifndef __CVC4__ARRAY__PROOF_H #define __CVC4__ARRAY__PROOF_H +#include <memory> #include <unordered_set> #include "expr/expr.h" @@ -32,23 +33,23 @@ namespace CVC4 { // Proof object outputted by TheoryARRAY. class ProofArray : public Proof { public: - ProofArray(theory::eq::EqProof* pf, unsigned row, unsigned row1, - unsigned ext); + ProofArray(std::shared_ptr<theory::eq::EqProof> pf, unsigned row, + unsigned row1, unsigned ext); void registerSkolem(Node equality, Node skolem); void toStream(std::ostream& out); void toStream(std::ostream& out, const ProofLetMap& map); - void toStreamLFSC(std::ostream& out, TheoryProof* tp, theory::eq::EqProof* pf, - const ProofLetMap& map); - private: + void toStreamLFSC(std::ostream& out, TheoryProof* tp, + const theory::eq::EqProof& pf, const ProofLetMap& map); + Node toStreamRecLFSC(std::ostream& out, TheoryProof* tp, - theory::eq::EqProof* pf, unsigned tb, + const theory::eq::EqProof& pf, unsigned tb, const ProofLetMap& map); - // it is simply an equality engine proof - theory::eq::EqProof* d_proof; + // It is simply an equality engine proof. + std::shared_ptr<theory::eq::EqProof> d_proof; /** Merge tag for ROW applications */ unsigned d_reasonRow; diff --git a/src/proof/uf_proof.cpp b/src/proof/uf_proof.cpp index a24f58698..f882883e7 100644 --- a/src/proof/uf_proof.cpp +++ b/src/proof/uf_proof.cpp @@ -14,13 +14,13 @@ ** \todo document this file **/ +#include "proof/uf_proof.h" + +#include <stack> #include "proof/proof_manager.h" #include "proof/simplify_boolean_node.h" -#include "proof/theory_proof.h" -#include "proof/uf_proof.h" #include "theory/uf/theory_uf.h" -#include <stack> namespace CVC4 { @@ -75,70 +75,78 @@ void ProofUF::toStream(std::ostream& out) { void ProofUF::toStream(std::ostream& out, const ProofLetMap& map) { Trace("theory-proof-debug") << "; Print UF proof..." << std::endl; //AJR : carry this further? - toStreamLFSC(out, ProofManager::getUfProof(), d_proof, map); + toStreamLFSC(out, ProofManager::getUfProof(), *d_proof, map); } -void ProofUF::toStreamLFSC(std::ostream& out, TheoryProof * tp, theory::eq::EqProof * pf, const ProofLetMap& map) { +void ProofUF::toStreamLFSC(std::ostream& out, TheoryProof* tp, + const theory::eq::EqProof& pf, + const ProofLetMap& map) { Debug("pf::uf") << "ProofUF::toStreamLFSC starting" << std::endl; Debug("lfsc-uf") << "Printing uf proof in LFSC : " << std::endl; - pf->debug_print("lfsc-uf"); + pf.debug_print("lfsc-uf"); Debug("lfsc-uf") << std::endl; toStreamRecLFSC( out, tp, pf, 0, map ); } -Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::EqProof * pf, unsigned tb, const ProofLetMap& map) { - Debug("pf::uf") << std::endl << std::endl << "toStreamRecLFSC called. tb = " << tb << " . proof:" << std::endl; - pf->debug_print("pf::uf"); +Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof* tp, + const theory::eq::EqProof& pf, + unsigned tb, const ProofLetMap& map) { + Debug("pf::uf") << std::endl + << std::endl + << "toStreamRecLFSC called. tb = " << tb + << " . proof:" << std::endl; + pf.debug_print("pf::uf"); Debug("pf::uf") << std::endl; if (tb == 0) { // Special case: false was an input, so the proof is just "false". - if (pf->d_id == theory::eq::MERGED_THROUGH_EQUALITY && - pf->d_node == NodeManager::currentNM()->mkConst(false)) { + if (pf.d_id == theory::eq::MERGED_THROUGH_EQUALITY && + pf.d_node == NodeManager::currentNM()->mkConst(false)) { out << "(clausify_false "; out << ProofManager::getLitName(NodeManager::currentNM()->mkConst(false).notNode()); out << ")" << std::endl; return Node(); } - Assert(pf->d_id == theory::eq::MERGED_THROUGH_TRANS); - Assert(!pf->d_node.isNull()); - Assert(pf->d_children.size() >= 2); + Assert(pf.d_id == theory::eq::MERGED_THROUGH_TRANS); + Assert(!pf.d_node.isNull()); + Assert(pf.d_children.size() >= 2); int neg = -1; - theory::eq::EqProof subTrans; - subTrans.d_id = theory::eq::MERGED_THROUGH_TRANS; - subTrans.d_node = pf->d_node; + std::shared_ptr<theory::eq::EqProof> subTrans = + std::make_shared<theory::eq::EqProof>(); + subTrans->d_id = theory::eq::MERGED_THROUGH_TRANS; + subTrans->d_node = pf.d_node; 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.d_children.size()) { + pf.d_children[i]->d_node = simplifyBooleanNode(pf.d_children[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.d_children[i]->d_node.isNull() && pf.d_children[i]->d_node.getKind() == kind::NOT) { Assert(neg < 0); - Node node = pf->d_children[i]->d_node[0]; + Node node = pf.d_children[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.d_children[i]->d_id==theory::eq::MERGED_THROUGH_CONGRUENCE && pf.d_children[i]->d_node.isNull()) { Debug("pf::uf") << "Handling congruence over equalities" << std::endl; // Gather the sequence of consecutive congruence closures. - std::vector<const theory::eq::EqProof *> congruenceClosures; + std::vector<std::shared_ptr<const theory::eq::EqProof>> congruenceClosures; 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.d_children.size() && + pf.d_children[i + count]->d_id==theory::eq::MERGED_THROUGH_CONGRUENCE && + pf.d_children[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.d_children[i+count]->debug_print("pf::uf"); + congruenceClosures.push_back(pf.d_children[i+count]); } Debug("pf::uf") << "Total number of congruences found: " << congruenceClosures.size() << std::endl; @@ -152,9 +160,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.d_children.size()) || + (!pf.d_children[i + count]->d_node.isNull() && + pf.d_children[i + count]->d_node.getKind() == kind::NOT)) { Debug("pf::uf") << "Target does not appear after" << std::endl; targetAppearsAfter = false; } @@ -167,36 +175,36 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E targetAppearsBefore = false; // Begin breaking up the congruences and ordering the equalities correctly. - std::vector<theory::eq::EqProof *> orderedEqualities; + std::vector<std::shared_ptr<theory::eq::EqProof>> orderedEqualities; // Insert target clause first. if (targetAppearsBefore) { - orderedEqualities.push_back(pf->d_children[i - 1]); + orderedEqualities.push_back(pf.d_children[i - 1]); // The target has already been added to subTrans; remove it. - subTrans.d_children.pop_back(); + subTrans->d_children.pop_back(); } else { - orderedEqualities.push_back(pf->d_children[i + count]); + orderedEqualities.push_back(pf.d_children[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.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]); } } 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.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]); } } // Copy the result into the main transitivity proof. - subTrans.d_children.insert(subTrans.d_children.end(), orderedEqualities.begin(), orderedEqualities.end()); + subTrans->d_children.insert(subTrans->d_children.end(), orderedEqualities.begin(), orderedEqualities.end()); // Increase i to skip over the children that have been processed. i += count; @@ -207,7 +215,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->d_children.push_back(pf.d_children[i]); ++i; } } @@ -215,21 +223,21 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E bool disequalityFound = (neg >= 0); if (!disequalityFound) { Debug("pf::uf") << "A disequality was NOT found. UNSAT due to merged constants" << std::endl; - Debug("pf::uf") << "Proof for: " << pf->d_node << std::endl; - Assert(pf->d_node.getKind() == kind::EQUAL); - Assert(pf->d_node.getNumChildren() == 2); - Assert (pf->d_node[0].isConst() && pf->d_node[1].isConst()); + Debug("pf::uf") << "Proof for: " << pf.d_node << std::endl; + Assert(pf.d_node.getKind() == kind::EQUAL); + Assert(pf.d_node.getNumChildren() == 2); + Assert (pf.d_node[0].isConst() && pf.d_node[1].isConst()); } Node n1; std::stringstream ss; - Debug("pf::uf") << "\nsubtrans has " << subTrans.d_children.size() << " children\n"; + Debug("pf::uf") << "\nsubtrans has " << subTrans->d_children.size() << " children\n"; - if(!disequalityFound || subTrans.d_children.size() >= 2) { - n1 = toStreamRecLFSC(ss, tp, &subTrans, 1, map); + if(!disequalityFound || subTrans->d_children.size() >= 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->d_children[0]), 1, map); + Debug("pf::uf") << "\nsubTrans unique child " << subTrans->d_children[0]->d_id << " was proven\ngot: " << n1 << std::endl; } Debug("pf::uf") << "\nhave proven: " << n1 << std::endl; @@ -237,7 +245,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.d_children[neg]->d_node; Assert(n2.getKind() == kind::NOT); Debug("pf::uf") << "n2 is " << n2[0] << std::endl; @@ -269,7 +277,7 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E out << " " << ProofManager::getLitName(n2[0]) << "))" << std::endl; } } else { - Node n2 = pf->d_node; + Node n2 = pf.d_node; Assert(n2.getKind() == kind::EQUAL); Assert((n1[0] == n2[0] && n1[1] == n2[1]) || (n1[1] == n2[0] && n1[0] == n2[1])); @@ -282,12 +290,14 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E return Node(); } - switch(pf->d_id) { + switch(pf.d_id) { case theory::eq::MERGED_THROUGH_CONGRUENCE: { Debug("pf::uf") << "\nok, looking at congruence:\n"; - pf->debug_print("pf::uf"); + pf.debug_print("pf::uf"); std::stack<const theory::eq::EqProof*> 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->d_children[0].get()) { 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); @@ -299,10 +309,10 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E 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->d_children[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->d_children[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"; @@ -370,7 +380,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->d_children[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"; @@ -427,30 +437,30 @@ 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.d_node.isNull()); + Assert(pf.d_children.empty()); out << "(refl _ "; - tp->printTerm(NodeManager::currentNM()->toExpr(pf->d_node), out, map); + tp->printTerm(NodeManager::currentNM()->toExpr(pf.d_node), out, map); out << ")"; - return eqNode(pf->d_node, pf->d_node); + return eqNode(pf.d_node, pf.d_node); case theory::eq::MERGED_THROUGH_EQUALITY: - Assert(!pf->d_node.isNull()); - Assert(pf->d_children.empty()); - out << ProofManager::getLitName(pf->d_node.negate()); - return pf->d_node; + Assert(!pf.d_node.isNull()); + Assert(pf.d_children.empty()); + 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.d_node.isNull()); + Assert(pf.d_children.size() >= 2); std::stringstream ss; Debug("pf::uf") << "\ndoing trans proof[[\n"; - pf->debug_print("pf::uf"); + pf.debug_print("pf::uf"); Debug("pf::uf") << "\n"; - pf->d_children[0]->d_node = simplifyBooleanNode(pf->d_children[0]->d_node); + pf.d_children[0]->d_node = simplifyBooleanNode(pf.d_children[0]->d_node); - Node n1 = toStreamRecLFSC(ss, tp, pf->d_children[0], tb + 1, map); + Node n1 = toStreamRecLFSC(ss, tp, *(pf.d_children[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 +472,11 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E std::map<size_t, Node> childToStream; - for(size_t i = 1; i < pf->d_children.size(); ++i) { + for(size_t i = 1; i < pf.d_children.size(); ++i) { std::stringstream ss1(ss.str()), ss2; ss.str(""); - pf->d_children[i]->d_node = simplifyBooleanNode(pf->d_children[i]->d_node); + pf.d_children[i]->d_node = simplifyBooleanNode(pf.d_children[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 +484,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.d_children[i]), tb + 1, map); childToStream[i] = n2; } @@ -505,9 +515,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.d_children.size() && !sequenceOver) { std::stringstream dontCare; - nodeAfterEqualitySequence = toStreamRecLFSC(dontCare, tp, pf->d_children[j], tb + 1, map ); + nodeAfterEqualitySequence = toStreamRecLFSC(dontCare, tp, *(pf.d_children[j]), tb + 1, map ); if (((nodeAfterEqualitySequence[0] == n1[0]) && (nodeAfterEqualitySequence[1] == n1[1])) || ((nodeAfterEqualitySequence[0] == n1[1]) && (nodeAfterEqualitySequence[1] == n1[0]))) { @@ -525,17 +535,17 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E Debug("pf::uf") << "Equality sequence of even length" << std::endl; Debug("pf::uf") << "n1 is: " << n1 << std::endl; Debug("pf::uf") << "n2 is: " << n2 << std::endl; - Debug("pf::uf") << "pf-d_node is: " << pf->d_node << std::endl; + Debug("pf::uf") << "pf-d_node is: " << pf.d_node << std::endl; Debug("pf::uf") << "Next node is: " << nodeAfterEqualitySequence << std::endl; ss << "(trans _ _ _ _ "; - // If the sequence is at the very end of the transitivity proof, use pf->d_node to guide us. + // If the sequence is at the very end of the transitivity proof, use pf.d_node to guide us. if (!sequenceOver) { - if (match(n1[0], pf->d_node[0])) { + if (match(n1[0], pf.d_node[0])) { n1 = eqNode(n1[0], n1[0]); ss << ss1.str() << " (symm _ _ _ " << ss1.str() << ")"; - } else if (match(n1[1], pf->d_node[1])) { + } else if (match(n1[1], pf.d_node[1])) { n1 = eqNode(n1[1], n1[1]); ss << " (symm _ _ _ " << ss1.str() << ")" << ss1.str(); } else { @@ -631,7 +641,7 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E Warning() << "\n\ntrans proof failure at step " << i << "\n\n"; Warning() << "0 proves " << n1 << "\n"; Warning() << "1 proves " << n2 << "\n\n"; - pf->debug_print("pf::uf",0); + pf.debug_print("pf::uf",0); //toStreamRec(Warning.getStream(), pf, 0); Warning() << "\n\n"; Unreachable(); @@ -664,33 +674,33 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E // We want to prove b1 = b2, and we know that ((b1), (b2)) or ((not b1), (not b2)) if (n1.getKind() == kind::NOT) { Assert(n2.getKind() == kind::NOT); - Assert(pf->d_node[0] == n1[0] || pf->d_node[0] == n2[0]); - Assert(pf->d_node[1] == n1[0] || pf->d_node[1] == n2[0]); + Assert(pf.d_node[0] == n1[0] || pf.d_node[0] == n2[0]); + Assert(pf.d_node[1] == n1[0] || pf.d_node[1] == n2[0]); Assert(n1[0].getKind() == kind::BOOLEAN_TERM_VARIABLE); Assert(n2[0].getKind() == kind::BOOLEAN_TERM_VARIABLE); - if (pf->d_node[0] == n1[0]) { + if (pf.d_node[0] == n1[0]) { ss << "(false_preds_equal _ _ " << ss1.str() << " " << ss2.str() << ") "; ss << "(pred_refl_neg _ " << ss2.str() << ")"; } else { ss << "(false_preds_equal _ _ " << ss2.str() << " " << ss1.str() << ") "; ss << "(pred_refl_neg _ " << ss1.str() << ")"; } - n1 = pf->d_node; + n1 = pf.d_node; } else if (n1.getKind() == kind::BOOLEAN_TERM_VARIABLE) { Assert(n2.getKind() == kind::BOOLEAN_TERM_VARIABLE); - Assert(pf->d_node[0] == n1 || pf->d_node[0] == n2); - Assert(pf->d_node[1] == n1 || pf->d_node[2] == n2); + Assert(pf.d_node[0] == n1 || pf.d_node[0] == n2); + Assert(pf.d_node[1] == n1 || pf.d_node[2] == n2); - if (pf->d_node[0] == n1) { + if (pf.d_node[0] == n1) { ss << "(true_preds_equal _ _ " << ss1.str() << " " << ss2.str() << ") "; ss << "(pred_refl_pos _ " << ss2.str() << ")"; } else { ss << "(true_preds_equal _ _ " << ss2.str() << " " << ss1.str() << ") "; ss << "(pred_refl_pos _ " << ss1.str() << ")"; } - n1 = pf->d_node; + n1 = pf.d_node; } else { @@ -706,11 +716,11 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E } default: - Assert(!pf->d_node.isNull()); - Assert(pf->d_children.empty()); - Debug("pf::uf") << "theory proof: " << pf->d_node << " by rule " << int(pf->d_id) << std::endl; + Assert(!pf.d_node.isNull()); + Assert(pf.d_children.empty()); + Debug("pf::uf") << "theory proof: " << pf.d_node << " by rule " << int(pf.d_id) << std::endl; AlwaysAssert(false); - return pf->d_node; + return pf.d_node; } } diff --git a/src/proof/uf_proof.h b/src/proof/uf_proof.h index b817ceb69..3dc7d9b58 100644 --- a/src/proof/uf_proof.h +++ b/src/proof/uf_proof.h @@ -19,28 +19,35 @@ #ifndef __CVC4__UF__PROOF_H #define __CVC4__UF__PROOF_H +#include <memory> #include <unordered_set> #include "expr/expr.h" -#include "proof/proof_manager.h" +#include "proof/theory_proof.h" #include "theory/uf/equality_engine.h" +#include "util/proof.h" namespace CVC4 { -//proof object outputted by TheoryUF +// proof object outputted by TheoryUF class ProofUF : public Proof { -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 ) {} - //it is simply an equality engine proof - theory::eq::EqProof * d_proof; - void toStream(std::ostream& out); - void toStream(std::ostream& out, const ProofLetMap& map); - static void toStreamLFSC(std::ostream& out, TheoryProof * tp, theory::eq::EqProof * pf, const ProofLetMap& map); + public: + ProofUF(std::shared_ptr<theory::eq::EqProof> pf) : d_proof(pf) {} + void toStream(std::ostream& out) override; + void toStream(std::ostream& out, const ProofLetMap& map) override; + + private: + static void toStreamLFSC(std::ostream& out, TheoryProof* tp, + const theory::eq::EqProof& pf, + const ProofLetMap& map); + static Node toStreamRecLFSC(std::ostream& out, TheoryProof* tp, + const theory::eq::EqProof& pf, unsigned tb, + const ProofLetMap& map); + + // it is simply an equality engine proof + std::shared_ptr<theory::eq::EqProof> d_proof; }; - namespace theory { namespace uf { class TheoryUF; diff --git a/src/theory/arrays/array_proof_reconstruction.cpp b/src/theory/arrays/array_proof_reconstruction.cpp index 471084d6f..29dfe9b47 100644 --- a/src/theory/arrays/array_proof_reconstruction.cpp +++ b/src/theory/arrays/array_proof_reconstruction.cpp @@ -17,6 +17,8 @@ #include "theory/arrays/array_proof_reconstruction.h" +#include <memory> + namespace CVC4 { namespace theory { namespace arrays { @@ -37,18 +39,18 @@ void ArrayProofReconstruction::setExtMergeTag(unsigned tag) { d_reasonExt = tag; } -void ArrayProofReconstruction::notify(unsigned reasonType, Node reason, Node a, Node b, - std::vector<TNode>& equalities, eq::EqProof* proof) const { - +void ArrayProofReconstruction::notify( + unsigned reasonType, Node reason, Node a, Node b, + std::vector<TNode>& equalities, eq::EqProof* proof) const { Debug("pf::array") << "ArrayProofReconstruction::notify( " << reason << ", " << a << ", " << b << std::endl; if (reasonType == d_reasonExt) { if (proof) { - // Todo: here we assume that a=b is an assertion. We should probably call explain() - // recursively, to explain this. - eq::EqProof* childProof = new eq::EqProof; + // Todo: here we assume that a=b is an assertion. We should probably call + // explain() recursively, to explain this. + std::shared_ptr<eq::EqProof> childProof = std::make_shared<eq::EqProof>(); childProof->d_node = reason; proof->d_children.push_back(childProof); } @@ -101,12 +103,13 @@ void ArrayProofReconstruction::notify(unsigned reasonType, Node reason, Node a, Debug("pf::ee") << "Getting explanation for ROW guard: " << indexOne << " != " << indexTwo << std::endl; + std::shared_ptr<eq::EqProof> childProof = + std::make_shared<eq::EqProof>(); + d_equalityEngine->explainEquality(indexOne, indexTwo, false, equalities, + childProof.get()); - eq::EqProof* childProof = new eq::EqProof; - d_equalityEngine->explainEquality(indexOne, indexTwo, false, equalities, childProof); - - // It could be that the guard condition is a constant disequality. In this case, - // we need to change it to a different format. + // 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) @@ -145,13 +148,15 @@ void ArrayProofReconstruction::notify(unsigned reasonType, Node reason, Node a, } } - eq::EqProof* constantDisequalityProof = new eq::EqProof; + std::shared_ptr<eq::EqProof> constantDisequalityProof = + std::make_shared<eq::EqProof>(); constantDisequalityProof->d_id = theory::eq::MERGED_THROUGH_CONSTANTS; constantDisequalityProof->d_node = NodeManager::currentNM()->mkNode(kind::EQUAL, constantOne, constantTwo).negate(); // Middle is where we need to insert the new disequality - std::vector<eq::EqProof *>::iterator middle = childProof->d_children.begin(); + std::vector<std::shared_ptr<eq::EqProof>>::iterator middle = + childProof->d_children.begin(); ++middle; childProof->d_children.insert(middle, constantDisequalityProof); @@ -174,8 +179,10 @@ void ArrayProofReconstruction::notify(unsigned reasonType, Node reason, Node a, Assert(reason.getNumChildren() == 2); Debug("pf::ee") << "Getting explanation for ROW guard: " << reason[1] << std::endl; - eq::EqProof* childProof = new eq::EqProof; - d_equalityEngine->explainEquality(reason[1][0], reason[1][1], false, equalities, childProof); + std::shared_ptr<eq::EqProof> childProof = + std::make_shared<eq::EqProof>(); + d_equalityEngine->explainEquality(reason[1][0], reason[1][1], false, + equalities, childProof.get()); proof->d_children.push_back(childProof); } } diff --git a/src/theory/arrays/array_proof_reconstruction.h b/src/theory/arrays/array_proof_reconstruction.h index c5ba21569..1b06dc524 100644 --- a/src/theory/arrays/array_proof_reconstruction.h +++ b/src/theory/arrays/array_proof_reconstruction.h @@ -34,7 +34,8 @@ public: ArrayProofReconstruction(const eq::EqualityEngine* equalityEngine); void notify(unsigned reasonType, Node reason, Node a, Node b, - std::vector<TNode>& equalities, eq::EqProof* proof) const; + std::vector<TNode>& equalities, + eq::EqProof* proof) const override; void setRowMergeTag(unsigned tag); void setRow1MergeTag(unsigned tag); diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index a17f506de..b43ba5591 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -17,6 +17,7 @@ #include "theory/arrays/theory_arrays.h" #include <map> +#include <memory> #include "expr/kind.h" #include "options/arrays_options.h" @@ -395,7 +396,8 @@ bool TheoryArrays::propagate(TNode literal) }/* TheoryArrays::propagate(TNode) */ -void TheoryArrays::explain(TNode literal, std::vector<TNode>& assumptions, eq::EqProof *proof) { +void TheoryArrays::explain(TNode literal, std::vector<TNode>& assumptions, + eq::EqProof* proof) { // Do the work bool polarity = literal.getKind() != kind::NOT; TNode atom = polarity ? literal : literal[0]; @@ -831,16 +833,15 @@ Node TheoryArrays::explain(TNode literal) { return explanation; } -Node TheoryArrays::explain(TNode literal, eq::EqProof *proof) -{ +Node TheoryArrays::explain(TNode literal, eq::EqProof* proof) { ++d_numExplain; - Debug("arrays") << spaces(getSatContext()->getLevel()) << "TheoryArrays::explain(" << literal << ")" << std::endl; + Debug("arrays") << spaces(getSatContext()->getLevel()) + << "TheoryArrays::explain(" << literal << ")" << std::endl; std::vector<TNode> assumptions; explain(literal, assumptions, proof); return mkAnd(assumptions); } - ///////////////////////////////////////////////////////////////////////////// // SHARING ///////////////////////////////////////////////////////////////////////////// @@ -2238,9 +2239,10 @@ bool TheoryArrays::dischargeLemmas() void TheoryArrays::conflict(TNode a, TNode b) { Debug("pf::array") << "TheoryArrays::Conflict called" << std::endl; - eq::EqProof* proof = d_proofsEnabled ? new eq::EqProof() : NULL; + std::shared_ptr<eq::EqProof> proof = d_proofsEnabled ? + std::make_shared<eq::EqProof>() : nullptr; - d_conflictNode = explain(a.eqNode(b), proof); + d_conflictNode = explain(a.eqNode(b), proof.get()); if (!d_inCheckModel) { ProofArray* proof_array = NULL; diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index 3ef9578ef..08d1618c2 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -195,7 +195,8 @@ class TheoryArrays : public Theory { bool propagate(TNode literal); /** Explain why this literal is true by adding assumptions */ - void explain(TNode literal, std::vector<TNode>& assumptions, eq::EqProof *proof); + void explain(TNode literal, std::vector<TNode>& assumptions, + eq::EqProof* proof); /** For debugging only- checks invariants about when things are preregistered*/ context::CDHashSet<Node, NodeHashFunction > d_isPreRegistered; @@ -207,7 +208,7 @@ class TheoryArrays : public Theory { void preRegisterTerm(TNode n); void propagate(Effort e); - Node explain(TNode n, eq::EqProof *proof); + Node explain(TNode n, eq::EqProof* proof); Node explain(TNode n); ///////////////////////////////////////////////////////////////////////////// diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp index 1378b4edf..a9142c4ef 100644 --- a/src/theory/uf/equality_engine.cpp +++ b/src/theory/uf/equality_engine.cpp @@ -926,8 +926,12 @@ std::string EqualityEngine::edgesToString(EqualityEdgeId edgeId) const { return out.str(); } -void EqualityEngine::explainEquality(TNode t1, TNode t2, bool polarity, std::vector<TNode>& equalities, EqProof * eqp) const { - Debug("equality") << d_name << "::eq::explainEquality(" << t1 << ", " << t2 << ", " << (polarity ? "true" : "false") << ")" << ", proof = " << (eqp ? "ON" : "OFF") << std::endl; +void EqualityEngine::explainEquality(TNode t1, TNode t2, bool polarity, + std::vector<TNode>& equalities, + EqProof* eqp) const { + Debug("equality") << d_name << "::eq::explainEquality(" << t1 << ", " << t2 + << ", " << (polarity ? "true" : "false") << ")" + << ", proof = " << (eqp ? "ON" : "OFF") << std::endl; // The terms must be there already Assert(hasTerm(t1) && hasTerm(t2));; @@ -953,21 +957,21 @@ void EqualityEngine::explainEquality(TNode t1, TNode t2, bool polarity, std::vec for (unsigned i = reasonRef.mergesStart; i < reasonRef.mergesEnd; ++ i) { EqualityPair toExplain = d_deducedDisequalityReasons[i]; - EqProof* eqpc = NULL; + std::shared_ptr<EqProof> eqpc; // If we're constructing a (transitivity) proof, we don't need to include an explanation for x=x. if (eqp && toExplain.first != toExplain.second) { - eqpc = new EqProof; + eqpc = std::make_shared<EqProof>(); } - getExplanation(toExplain.first, toExplain.second, equalities, eqpc); + getExplanation(toExplain.first, toExplain.second, equalities, eqpc.get()); if (eqpc) { Debug("pf::ee") << "Child proof is:" << std::endl; eqpc->debug_print("pf::ee", 1); if (eqpc->d_id == eq::MERGED_THROUGH_TRANS) { - std::vector<EqProof *> orderedChildren; + std::vector<std::shared_ptr<EqProof>> 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 && @@ -1002,10 +1006,9 @@ void EqualityEngine::explainEquality(TNode t1, TNode t2, bool polarity, std::vec eqp->d_id = MERGED_THROUGH_CONSTANTS; } else if (eqp->d_children.size() == 1) { // The transitivity proof has just one child. Simplify. - EqProof* temp = eqp->d_children[0]; + std::shared_ptr<EqProof> temp = eqp->d_children[0]; eqp->d_children.clear(); *eqp = *temp; - delete temp; } Debug("pf::ee") << "Disequality explanation final proof: " << std::endl; @@ -1014,16 +1017,21 @@ void EqualityEngine::explainEquality(TNode t1, TNode t2, bool polarity, std::vec } } -void EqualityEngine::explainPredicate(TNode p, bool polarity, std::vector<TNode>& assertions, EqProof * eqp) const { - Debug("equality") << d_name << "::eq::explainPredicate(" << p << ")" << std::endl; +void EqualityEngine::explainPredicate(TNode p, bool polarity, + std::vector<TNode>& assertions, + EqProof* eqp) const { + Debug("equality") << d_name << "::eq::explainPredicate(" << p << ")" + << std::endl; // Must have the term Assert(hasTerm(p)); // Get the explanation - getExplanation(getNodeId(p), polarity ? d_trueId : d_falseId, assertions, eqp); + getExplanation(getNodeId(p), polarity ? d_trueId : d_falseId, assertions, + eqp); } -void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, std::vector<TNode>& equalities, EqProof * eqp) const { - +void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, + std::vector<TNode>& equalities, + EqProof* eqp) const { Debug("equality") << d_name << "::eq::getExplanation(" << d_nodes[t1Id] << "," << d_nodes[t2Id] << ")" << std::endl; // We can only explain the nodes that got merged @@ -1094,7 +1102,7 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st Debug("equality") << d_name << "::eq::getExplanation(): path found: " << std::endl; - std::vector<EqProof *> eqp_trans; + std::vector<std::shared_ptr<EqProof>> eqp_trans; // Reconstruct the path do { @@ -1109,10 +1117,10 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st Debug("equality") << d_name << " in currentEdge = (" << d_nodes[currentNode] << "," << d_nodes[edge.getNodeId()] << ")" << std::endl; Debug("equality") << d_name << " reason type = " << reasonType << std::endl; - EqProof* eqpc = NULL; + std::shared_ptr<EqProof> eqpc;; // Make child proof if a proof is being constructed if (eqp) { - eqpc = new EqProof; + eqpc = std::make_shared<EqProof>(); eqpc->d_id = reasonType; } @@ -1126,11 +1134,13 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st Debug("equality") << push; Debug("equality") << "Explaining left hand side equalities" << std::endl; - EqProof * eqpc1 = eqpc ? new EqProof : NULL; - getExplanation(f1.a, f2.a, equalities, eqpc1); + std::shared_ptr<EqProof> eqpc1 = + eqpc ? std::make_shared<EqProof>() : nullptr; + getExplanation(f1.a, f2.a, equalities, eqpc1.get()); Debug("equality") << "Explaining right hand side equalities" << std::endl; - EqProof * eqpc2 = eqpc ? new EqProof : NULL; - getExplanation(f1.b, f2.b, equalities, eqpc2); + std::shared_ptr<EqProof> eqpc2 = + eqpc ? std::make_shared<EqProof>() : nullptr; + getExplanation(f1.b, f2.b, equalities, eqpc2.get()); if( eqpc ){ eqpc->d_children.push_back( eqpc1 ); eqpc->d_children.push_back( eqpc2 ); @@ -1173,8 +1183,9 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st // Explain why a = b constant Debug("equality") << push; - EqProof * eqpc1 = eqpc ? new EqProof : NULL; - getExplanation(eq.a, eq.b, equalities, eqpc1); + std::shared_ptr<EqProof> eqpc1 = + eqpc ? std::make_shared<EqProof>() : nullptr; + getExplanation(eq.a, eq.b, equalities, eqpc1.get()); if( eqpc ){ eqpc->d_children.push_back( eqpc1 ); } @@ -1198,8 +1209,10 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st for (unsigned i = 0; i < interpreted.getNumChildren(); ++ i) { EqualityNodeId childId = getNodeId(interpreted[i]); Assert(isConstant(childId)); - EqProof * eqpcc = eqpc ? new EqProof : NULL; - getExplanation(childId, getEqualityNode(childId).getFind(), equalities, eqpcc); + std::shared_ptr<EqProof> eqpcc = + eqpc ? std::make_shared<EqProof>() : nullptr; + getExplanation(childId, getEqualityNode(childId).getFind(), + equalities, eqpcc.get()); if( eqpc ) { eqpc->d_children.push_back( eqpcc ); @@ -1223,8 +1236,9 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st if (eqpc) { //apply proof reconstruction processing (when eqpc is non-null) if (d_pathReconstructionTriggers.find(reasonType) != d_pathReconstructionTriggers.end()) { - d_pathReconstructionTriggers.find(reasonType)->second->notify(reasonType, reason, a, b, - equalities, eqpc); + d_pathReconstructionTriggers.find(reasonType) + ->second->notify(reasonType, reason, a, b, equalities, + eqpc.get()); } if (reasonType == MERGED_THROUGH_EQUALITY) { eqpc->d_node = reason; @@ -1255,9 +1269,8 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st if (eqpc != NULL && eqpc->d_id == MERGED_THROUGH_REFLEXIVITY) { if(eqpc->d_node.isNull()) { Assert(eqpc->d_children.size() == 1); - EqProof *p = eqpc; + std::shared_ptr<EqProof> p = eqpc; eqpc = p->d_children[0]; - delete p; } else { Assert(eqpc->d_children.empty()); } @@ -1270,7 +1283,6 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st if (eqp) { if(eqp_trans.size() == 1) { *eqp = *eqp_trans[0]; - 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() ); diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h index 9638b9f09..a89e55312 100644 --- a/src/theory/uf/equality_engine.h +++ b/src/theory/uf/equality_engine.h @@ -21,6 +21,7 @@ #include <deque> #include <queue> +#include <memory> #include <unordered_map> #include <vector> @@ -150,7 +151,8 @@ public: virtual ~PathReconstructionNotify() {} virtual void notify(unsigned reasonType, Node reason, Node a, Node b, - std::vector<TNode>& equalities, EqProof* proof) const = 0; + std::vector<TNode>& equalities, + EqProof* proof) const = 0; }; /** @@ -506,7 +508,7 @@ private: * imply t1 = t2. Returns TNodes as the assertion equalities should be hashed somewhere * else. */ - void getExplanation(EqualityEdgeId t1Id, EqualityNodeId t2Id, std::vector<TNode>& equalities, EqProof * eqp) const; + void getExplanation(EqualityEdgeId t1Id, EqualityNodeId t2Id, std::vector<TNode>& equalities, EqProof* eqp) const; /** * Print the equality graph. @@ -794,14 +796,17 @@ public: * Returns the reasons (added when asserting) that imply it * in the assertions vector. */ - void explainEquality(TNode t1, TNode t2, bool polarity, std::vector<TNode>& assertions, EqProof * eqp = NULL) const; + void explainEquality(TNode t1, TNode t2, bool polarity, + std::vector<TNode>& assertions, + EqProof* eqp = nullptr) const; /** * Get an explanation of the predicate being true or false. * Returns the reasons (added when asserting) that imply imply it * in the assertions vector. */ - void explainPredicate(TNode p, bool polarity, std::vector<TNode>& assertions, EqProof * eqp = NULL) const; + void explainPredicate(TNode p, bool polarity, std::vector<TNode>& assertions, + EqProof* eqp = nullptr) const; /** * Add term to the set of trigger terms with a corresponding tag. The notify class will get @@ -925,8 +930,9 @@ public: EqProof() : d_id(MERGED_THROUGH_REFLEXIVITY){} unsigned d_id; Node d_node; - std::vector< EqProof * > d_children; - void debug_print(const char * c, unsigned tb = 0, PrettyPrinter* prettyPrinter = NULL) const; + std::vector<std::shared_ptr<EqProof>> d_children; + void debug_print(const char* c, unsigned tb = 0, + PrettyPrinter* prettyPrinter = nullptr) const; };/* class EqProof */ } // Namespace eq diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index e8cc3b385..170621603 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -17,6 +17,8 @@ #include "theory/uf/theory_uf.h" +#include <memory> + #include "options/quantifiers_options.h" #include "options/smt_options.h" #include "options/uf_options.h" @@ -629,8 +631,9 @@ void TheoryUF::computeCareGraph() { }/* TheoryUF::computeCareGraph() */ void TheoryUF::conflict(TNode a, TNode b) { - eq::EqProof* pf = d_proofsEnabled ? new eq::EqProof() : NULL; - d_conflictNode = explain(a.eqNode(b),pf); + std::shared_ptr<eq::EqProof> pf = + d_proofsEnabled ? std::make_shared<eq::EqProof>() : nullptr; + d_conflictNode = explain(a.eqNode(b), pf.get()); ProofUF* puf = d_proofsEnabled ? new ProofUF( pf ) : NULL; d_out->conflict(d_conflictNode, puf); d_conflict = true; |