From 29df9622b570ce843756e05a3ef248de04d2a5c3 Mon Sep 17 00:00:00 2001 From: Guy Date: Sun, 3 Apr 2016 15:58:58 -0700 Subject: [PATCH] Removed the theory-specific merge reason types. Instead, added a mechanism for dynamically allocating these tags upon request. --- src/proof/array_proof.cpp | 119 ++++++++++-------- src/proof/array_proof.h | 11 +- src/proof/uf_proof.cpp | 82 ------------ .../arrays/array_proof_reconstruction.cpp | 40 +++--- .../arrays/array_proof_reconstruction.h | 13 +- src/theory/arrays/theory_arrays.cpp | 39 ++++-- src/theory/arrays/theory_arrays.h | 9 ++ src/theory/uf/equality_engine.cpp | 19 +-- src/theory/uf/equality_engine.h | 30 +++-- src/theory/uf/equality_engine_types.h | 24 +--- 10 files changed, 185 insertions(+), 201 deletions(-) diff --git a/src/proof/array_proof.cpp b/src/proof/array_proof.cpp index 764028c6b..aa615f90e 100644 --- a/src/proof/array_proof.cpp +++ b/src/proof/array_proof.cpp @@ -23,6 +23,10 @@ namespace CVC4 { +unsigned ProofArray::d_reasonRow; +unsigned ProofArray::d_reasonRow1; +unsigned ProofArray::d_reasonExt; + inline static Node eqNode(TNode n1, TNode n2) { return NodeManager::currentNM()->mkNode(n1.getType().isBoolean() ? kind::IFF : kind::EQUAL, n1, n2); } @@ -79,6 +83,18 @@ inline static bool match(TNode n1, TNode n2) { return true; } +void ProofArray::setRowMergeTag(unsigned tag) { + d_reasonRow = tag; +} + +void ProofArray::setRow1MergeTag(unsigned tag) { + d_reasonRow1 = tag; +} + +void ProofArray::setExtMergeTag(unsigned tag) { + d_reasonExt = tag; +} + void ProofArray::toStream(std::ostream& out) { Trace("pf::array") << "; Print Array proof..." << std::endl; //AJR : carry this further? @@ -95,16 +111,16 @@ void ProofArray::toStreamLFSC(std::ostream& out, TheoryProof* tp, theory::eq::Eq Debug("pf::array") << "Printing array proof in LFSC DONE" << std::endl; } -void ProofArray::registerSkolem(Node equality, Node skolem) { - d_nodeToSkolem[equality] = skolem; -} - Node ProofArray::toStreamRecLFSC(std::ostream& out, TheoryProof* tp, theory::eq::EqProof* pf, unsigned tb, const LetMap& map) { + Debug("gk::temp") << "d_reasonExt = " << d_reasonExt << std::endl; + Debug("gk::temp") << "d_reasonRow = " << d_reasonRow << std::endl; + Debug("gk::temp") << "d_reasonRow1 = " << d_reasonRow1 << std::endl; + Debug("pf::array") << std::endl << std::endl << "toStreamRecLFSC called. tb = " << tb << " . proof:" << std::endl; pf->debug_print("pf::array"); Debug("pf::array") << std::endl; @@ -138,8 +154,8 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, 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(); + 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"); @@ -235,7 +251,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, 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 == theory::eq::MERGED_ARRAYS_EXT) { + if (pf->d_children[neg]->d_id == d_reasonExt) { // The negative node was created by an EXT rule; e.g. it is a[k]!=b[k], due to a!=b. // (clausify_false (contra _ .gl2 (or_elim_1 _ _ .gl1 FIXME))))))) (\ .glemc6 @@ -275,8 +291,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, return Node(); } - switch(pf->d_id) { - case 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"); std::stack stk; @@ -324,8 +339,8 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, } else { 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"); + Debug("mgd") << "IN BAD CASE, our first subproof is\n"; + pf2->d_children[0]->debug_print("mgd"); } Assert(match(pf2->d_node, n1[1])); side = 1; @@ -370,7 +385,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, b2 << kind::PARTIAL_APPLY_UF; b2 << ProofManager::currentPM()->mkOp(n1[1-side].getOperator()); } - b2.append(n1[1-side].begin(), n1[1-side].end()); + b2.append(n1[1-side].begin(), n1[1-side].end()); } else if (n1[1-side].getKind() == kind::PARTIAL_SELECT_0) { b2 << kind::PARTIAL_SELECT_1; } else { @@ -464,13 +479,13 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, b1.append(n1.begin(), n1.end()); n1 = b1; Debug("mgd") << "New n1: " << n1 << std::endl; - // } else if (n1.getKind() == kind::PARTIAL_SELECT_0 && n1.getNumChildren() == 1) { - // Debug("mgd") << "Finished a PARTIAL_SELECT_1. Updating.." << std::endl; - // b1.clear(kind::PARTIAL_SELECT_1); - // b1.append(n1.begin(), n1.end()); - // n1 = b1; - // Debug("mgd") << "New n1: " << n1 << std::endl; - // } else + // } else if (n1.getKind() == kind::PARTIAL_SELECT_0 && n1.getNumChildren() == 1) { + // Debug("mgd") << "Finished a PARTIAL_SELECT_1. Updating.." << std::endl; + // b1.clear(kind::PARTIAL_SELECT_1); + // b1.append(n1.begin(), n1.end()); + // n1 = b1; + // Debug("mgd") << "New n1: " << n1 << std::endl; + // } else } else if(n1.getOperator().getType().getNumChildren() == n1.getNumChildren() + 1) { if(ProofManager::currentPM()->hasOp(n1.getOperator())) { b1.clear(ProofManager::currentPM()->lookupOp(n2.getOperator()).getConst()); @@ -498,13 +513,13 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, b2.append(n2.begin(), n2.end()); n2 = b2; Debug("mgd") << "New n2: " << n2 << std::endl; - // } else if (n2.getKind() == kind::PARTIAL_SELECT_0 && n2.getNumChildren() == 1) { - // Debug("mgd") << "Finished a PARTIAL_SELECT_1. Updating.." << std::endl; - // b2.clear(kind::PARTIAL_SELECT_1); - // b2.append(n2.begin(), n2.end()); - // n2 = b2; - // Debug("mgd") << "New n2: " << n2 << std::endl; - // } else + // } else if (n2.getKind() == kind::PARTIAL_SELECT_0 && n2.getNumChildren() == 1) { + // Debug("mgd") << "Finished a PARTIAL_SELECT_1. Updating.." << std::endl; + // b2.clear(kind::PARTIAL_SELECT_1); + // b2.append(n2.begin(), n2.end()); + // n2 = b2; + // Debug("mgd") << "New n2: " << n2 << std::endl; + // } else } else if(n2.getOperator().getType().getNumChildren() == n2.getNumChildren() + 1) { if(ProofManager::currentPM()->hasOp(n2.getOperator())) { b2.clear(ProofManager::currentPM()->lookupOp(n2.getOperator()).getConst()); @@ -521,23 +536,25 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, return n; } - case theory::eq::MERGED_THROUGH_REFLEXIVITY: + 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); out << ")"; return eqNode(pf->d_node, pf->d_node); + } - case theory::eq::MERGED_THROUGH_EQUALITY: + 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; + } - case theory::eq::MERGED_THROUGH_TRANS: { + else if (pf->d_id == theory::eq::MERGED_THROUGH_TRANS) { bool firstNeg = false; bool secondNeg = false; @@ -734,27 +751,27 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, // Both elements of the transitivity rule are equalities/iffs { if(n1[0] == n2[0]) { - if(tb == 1) { Debug("mgdx") << "case 1\n"; } - n1 = eqNode(n1[1], n2[1]); - ss << (firstNeg ? "(negsymm _ _ _ " : "(symm _ _ _ ") << ss1.str() << ") " << ss2.str(); + if(tb == 1) { Debug("mgdx") << "case 1\n"; } + n1 = eqNode(n1[1], n2[1]); + ss << (firstNeg ? "(negsymm _ _ _ " : "(symm _ _ _ ") << ss1.str() << ") " << ss2.str(); } else if(n1[1] == n2[1]) { if(tb == 1) { Debug("mgdx") << "case 2\n"; } n1 = eqNode(n1[0], n2[0]); ss << ss1.str() << (secondNeg ? " (negsymm _ _ _ " : " (symm _ _ _ " ) << ss2.str() << ")"; } else if(n1[0] == n2[1]) { - if(tb == 1) { Debug("mgdx") << "case 3\n"; } - if(!firstNeg && !secondNeg) { - n1 = eqNode(n2[0], n1[1]); - ss << ss2.str() << " " << ss1.str(); - } else if (firstNeg) { - n1 = eqNode(n1[1], n2[0]); - ss << " (negsymm _ _ _ " << ss1.str() << ") (symm _ _ _ " << ss2.str() << ")"; - } else { - Assert(secondNeg); - n1 = eqNode(n1[1], n2[0]); - ss << " (symm _ _ _ " << ss1.str() << ") (negsymm _ _ _ " << ss2.str() << ")"; - } - if(tb == 1) { Debug("mgdx") << "++ proved " << n1 << "\n"; } + if(tb == 1) { Debug("mgdx") << "case 3\n"; } + if(!firstNeg && !secondNeg) { + n1 = eqNode(n2[0], n1[1]); + ss << ss2.str() << " " << ss1.str(); + } else if (firstNeg) { + n1 = eqNode(n1[1], n2[0]); + ss << " (negsymm _ _ _ " << ss1.str() << ") (symm _ _ _ " << ss2.str() << ")"; + } else { + Assert(secondNeg); + n1 = eqNode(n1[1], n2[0]); + ss << " (symm _ _ _ " << ss1.str() << ") (negsymm _ _ _ " << ss2.str() << ")"; + } + if(tb == 1) { Debug("mgdx") << "++ proved " << n1 << "\n"; } } else if(n1[1] == n2[0]) { if(tb == 1) { Debug("mgdx") << "case 4\n"; } n1 = eqNode(n1[0], n2[1]); @@ -811,7 +828,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, return n1; } - case theory::eq::MERGED_ARRAYS_ROW: { + else if (pf->d_id == d_reasonRow) { Debug("mgd") << "row lemma: " << pf->d_node << std::endl; Assert(pf->d_node.getKind() == kind::EQUAL); @@ -942,8 +959,8 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, // if (subproof[0][1] == t3) { - Debug("pf::array") << "Dont need symmetry!" << std::endl; - out << ss.str(); + Debug("pf::array") << "Dont need symmetry!" << std::endl; + out << ss.str(); // } else { // Debug("pf::array") << "Need symmetry!" << std::endl; // out << "(negsymm _ _ _ " << ss.str() << ")"; @@ -957,7 +974,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, } } - case theory::eq::MERGED_ARRAYS_ROW1: { + 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; @@ -992,7 +1009,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, return ret; } - case theory::eq::MERGED_ARRAYS_EXT: { + else if (pf->d_id == d_reasonExt) { theory::eq::EqProof *child_proof; Assert(pf->d_node.getKind() == kind::NOT); @@ -1021,7 +1038,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, return pf->d_node; } - default: + 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; diff --git a/src/proof/array_proof.h b/src/proof/array_proof.h index 9b308dcd8..b3fe89f0b 100644 --- a/src/proof/array_proof.h +++ b/src/proof/array_proof.h @@ -35,7 +35,12 @@ private: unsigned tb, const LetMap& map); - std::hash_map d_nodeToSkolem; + /** Merge tag for ROW applications */ + static unsigned d_reasonRow; + /** Merge tag for ROW1 applications */ + static unsigned d_reasonRow1; + /** Merge tag for EXT applications */ + static unsigned d_reasonExt; public: ProofArray(theory::eq::EqProof* pf) : d_proof(pf) {} //it is simply an equality engine proof @@ -44,6 +49,10 @@ public: static void toStreamLFSC(std::ostream& out, TheoryProof* tp, theory::eq::EqProof* pf, const LetMap& map); void registerSkolem(Node equality, Node skolem); + + static void setRowMergeTag(unsigned tag); + static void setRow1MergeTag(unsigned tag); + static void setExtMergeTag(unsigned tag); }; namespace theory { diff --git a/src/proof/uf_proof.cpp b/src/proof/uf_proof.cpp index 6a6f8d906..e728e9e49 100644 --- a/src/proof/uf_proof.cpp +++ b/src/proof/uf_proof.cpp @@ -615,88 +615,6 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E return n1; } - case theory::eq::MERGED_ARRAYS_ROW: { - Debug("pf::uf") << "eq::MERGED_ARRAYS_ROW encountered in UF_PROOF" << std::endl; - Unreachable(); - - Debug("pf::uf") << "row lemma: " << pf->d_node << std::endl; - Assert(pf->d_node.getKind() == kind::EQUAL); - 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]); - Debug("pf::uf") << "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; - Debug("pf::uf") << "t1 " << t1 << "\nt2 " << t2 << "\nt3 " << t3 << "\nt4 " << t4 << "\n"; - } - out << "(row _ _ "; - tp->printTerm(t2.toExpr(), out, map); - out << " "; - tp->printTerm(t3.toExpr(), out, map); - out << " "; - tp->printTerm(t1.toExpr(), out, map); - out << " "; - tp->printTerm(t4.toExpr(), out, map); - out << " " << ProofManager::getLitName(t2.eqNode(t3)) << ")"; - return ret; - } - - case theory::eq::MERGED_ARRAYS_ROW1: { - Debug("pf::uf") << "eq::MERGED_ARRAYS_ROW1 encountered in UF_PROOF" << std::endl; - Unreachable(); - - Debug("pf::uf") << "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]); - Debug("pf::uf") << "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; - Debug("pf::uf") << "t1 " << t1 << "\nt2 " << t2 << "\nt3 " << t3 << "\n"; - } - out << "(row1 _ _ "; - tp->printTerm(t1.toExpr(), out, map); - out << " "; - tp->printTerm(t2.toExpr(), out, map); - out << " "; - tp->printTerm(t3.toExpr(), out, map); - out << ")"; - return ret; - } - default: Assert(!pf->d_node.isNull()); Assert(pf->d_children.empty()); diff --git a/src/theory/arrays/array_proof_reconstruction.cpp b/src/theory/arrays/array_proof_reconstruction.cpp index b2e8c3ab3..c8a6716f5 100644 --- a/src/theory/arrays/array_proof_reconstruction.cpp +++ b/src/theory/arrays/array_proof_reconstruction.cpp @@ -1,10 +1,10 @@ /********************* */ /*! \file array_proof_reconstruction.h - ** \verbatim - ** - ** \brief Array-specific proof construction logic to be used during the - ** equality engine's path reconstruction - **/ +** \verbatim +** +** \brief Array-specific proof construction logic to be used during the +** equality engine's path reconstruction +**/ #include "theory/arrays/array_proof_reconstruction.h" @@ -16,16 +16,26 @@ ArrayProofReconstruction::ArrayProofReconstruction(const eq::EqualityEngine* equ : d_equalityEngine(equalityEngine) { } -void ArrayProofReconstruction::notify(eq::MergeReasonType reasonType, Node reason, Node a, Node b, +void ArrayProofReconstruction::setRowMergeTag(unsigned tag) { + d_reasonRow = tag; +} + +void ArrayProofReconstruction::setRow1MergeTag(unsigned tag) { + d_reasonRow1 = tag; +} + +void ArrayProofReconstruction::setExtMergeTag(unsigned tag) { + d_reasonExt = tag; +} + +void ArrayProofReconstruction::notify(unsigned reasonType, Node reason, Node a, Node b, std::vector& equalities, eq::EqProof* proof) const { Debug("pf::array") << "ArrayProofReconstruction::notify( " << reason << ", " << a << ", " << b << std::endl; - switch (reasonType) { - - case eq::MERGED_ARRAYS_EXT: { + 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. @@ -33,10 +43,9 @@ void ArrayProofReconstruction::notify(eq::MergeReasonType reasonType, Node reaso childProof->d_node = reason; proof->d_children.push_back(childProof); } - break; } - case eq::MERGED_ARRAYS_ROW: { + else if (reasonType == d_reasonRow) { // ROW rules mean that (i==k) OR ((a[i]:=t)[k] == a[k]) // The equality here will be either (i == k) because ((a[i]:=t)[k] != a[k]), // or ((a[i]:=t)[k] == a[k]) because (i != k). @@ -103,16 +112,11 @@ void ArrayProofReconstruction::notify(eq::MergeReasonType reasonType, Node reaso proof->d_children.push_back(childProof); } } - break; - } - case eq::MERGED_ARRAYS_ROW1: { - // No special handling required at this time - break; } - default: - break; + else if (reasonType == d_reasonRow1) { + // No special handling required at this time } } diff --git a/src/theory/arrays/array_proof_reconstruction.h b/src/theory/arrays/array_proof_reconstruction.h index 8afc0d3f7..6502b0e6b 100644 --- a/src/theory/arrays/array_proof_reconstruction.h +++ b/src/theory/arrays/array_proof_reconstruction.h @@ -26,10 +26,21 @@ class ArrayProofReconstruction : public eq::PathReconstructionNotify { public: ArrayProofReconstruction(const eq::EqualityEngine* equalityEngine); - void notify(eq::MergeReasonType reasonType, Node reason, Node a, Node b, + void notify(unsigned reasonType, Node reason, Node a, Node b, std::vector& equalities, eq::EqProof* proof) const; + void setRowMergeTag(unsigned tag); + void setRow1MergeTag(unsigned tag); + void setExtMergeTag(unsigned tag); + private: + /** Merge tag for ROW applications */ + unsigned d_reasonRow; + /** Merge tag for ROW1 applications */ + unsigned d_reasonRow1; + /** Merge tag for EXT applications */ + unsigned d_reasonExt; + const eq::EqualityEngine* d_equalityEngine; }; /* class ArrayProofReconstruction */ diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 37854ee90..8d97eb89d 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -129,9 +129,17 @@ TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u, d_equalityEngine.addFunctionKind(kind::ARR_TABLE_FUN); } - d_equalityEngine.addPathReconstructionTrigger(eq::MERGED_ARRAYS_ROW, &d_proofReconstruction); - d_equalityEngine.addPathReconstructionTrigger(eq::MERGED_ARRAYS_ROW1, &d_proofReconstruction); - d_equalityEngine.addPathReconstructionTrigger(eq::MERGED_ARRAYS_EXT, &d_proofReconstruction); + d_reasonRow = d_equalityEngine.getFreshMergeReasonType(); + d_reasonRow1 = d_equalityEngine.getFreshMergeReasonType(); + d_reasonExt = d_equalityEngine.getFreshMergeReasonType(); + + d_proofReconstruction.setRowMergeTag(d_reasonRow); + d_proofReconstruction.setRow1MergeTag(d_reasonRow1); + d_proofReconstruction.setExtMergeTag(d_reasonExt); + + d_equalityEngine.addPathReconstructionTrigger(d_reasonRow, &d_proofReconstruction); + d_equalityEngine.addPathReconstructionTrigger(d_reasonRow1, &d_proofReconstruction); + d_equalityEngine.addPathReconstructionTrigger(d_reasonExt, &d_proofReconstruction); } TheoryArrays::~TheoryArrays() { @@ -665,7 +673,7 @@ void TheoryArrays::preRegisterTermInternal(TNode node) if (ni != node) { preRegisterTermInternal(ni); } - d_equalityEngine.assertEquality(ni.eqNode(s[2]), true, d_true, eq::MERGED_ARRAYS_ROW1); + d_equalityEngine.assertEquality(ni.eqNode(s[2]), true, d_true, d_reasonRow1); Assert(++it == stores->end()); } } @@ -751,7 +759,7 @@ void TheoryArrays::preRegisterTermInternal(TNode node) } // Apply RIntro1 Rule - d_equalityEngine.assertEquality(ni.eqNode(v), true, d_true, eq::MERGED_ARRAYS_ROW1); + d_equalityEngine.assertEquality(ni.eqNode(v), true, d_true, d_reasonRow1); } d_infoMap.addStore(node, node); @@ -1367,7 +1375,7 @@ void TheoryArrays::check(Effort e) { << "\teq = " << eq << std::endl << "\treason = " << fact << std::endl; - d_equalityEngine.assertEquality(eq, false, fact, eq::MERGED_ARRAYS_EXT); + d_equalityEngine.assertEquality(eq, false, fact, d_reasonExt); ++d_numProp; } @@ -1669,7 +1677,7 @@ void TheoryArrays::checkRIntro1(TNode a, TNode b) d_infoMap.setRIntro1Applied(s); Node ni = nm->mkNode(kind::SELECT, s, s[1]); preRegisterTermInternal(ni); - d_equalityEngine.assertEquality(ni.eqNode(s[2]), true, d_true, eq::MERGED_ARRAYS_ROW1); + d_equalityEngine.assertEquality(ni.eqNode(s[2]), true, d_true, d_reasonRow1); } } @@ -1976,7 +1984,7 @@ void TheoryArrays::propagate(RowLemmaType lem) if (!bjExists) { preRegisterTermInternal(bj); } - d_equalityEngine.assertEquality(aj_eq_bj, true, reason, eq::MERGED_ARRAYS_ROW); + d_equalityEngine.assertEquality(aj_eq_bj, true, reason, d_reasonRow); ++d_numProp; return; } @@ -1986,7 +1994,7 @@ void TheoryArrays::propagate(RowLemmaType lem) Node i_eq_j = i.eqNode(j); Node reason = nm->mkNode(kind::OR, i_eq_j, aj_eq_bj); d_permRef.push_back(reason); - d_equalityEngine.assertEquality(i_eq_j, true, reason, eq::MERGED_ARRAYS_ROW); + d_equalityEngine.assertEquality(i_eq_j, true, reason, d_reasonRow); ++d_numProp; return; } @@ -2230,15 +2238,22 @@ void TheoryArrays::conflict(TNode a, TNode b) { } if (!d_inCheckModel) { - if (proof) { proof->debug_print("pf::array"); } - ProofArray* proof_array = d_proofsEnabled ? new ProofArray( proof ) : NULL; + ProofArray* proof_array = NULL; + + if (d_proofsEnabled) { + proof->debug_print("pf::array"); + proof_array = new ProofArray( proof ); + proof_array->setRowMergeTag(d_reasonRow); + proof_array->setRow1MergeTag(d_reasonRow1); + proof_array->setExtMergeTag(d_reasonExt); + } + d_out->conflict(d_conflictNode, proof_array); } d_conflict = true; } - }/* CVC4::theory::arrays namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index 6d2bb9e73..14e5a622a 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -125,6 +125,15 @@ class TheoryArrays : public Theory { /** conflicts in setModelVal */ IntStat d_numSetModelValConflicts; + // Merge reason types + + /** Merge tag for ROW applications */ + unsigned d_reasonRow; + /** Merge tag for ROW1 applications */ + unsigned d_reasonRow1; + /** Merge tag for EXT applications */ + unsigned d_reasonExt; + public: TheoryArrays(context::Context* c, context::UserContext* u, OutputChannel& out, diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp index d4a1e5ca4..20d0d85a8 100644 --- a/src/theory/uf/equality_engine.cpp +++ b/src/theory/uf/equality_engine.cpp @@ -93,6 +93,8 @@ void EqualityEngine::init() { d_trueId = getNodeId(d_true); d_falseId = getNodeId(d_false); + + d_freshMergeReasonType = eq::NUMBER_OF_MERGE_REASONS; } EqualityEngine::~EqualityEngine() throw(AssertionException) { @@ -389,7 +391,7 @@ const EqualityNode& EqualityEngine::getEqualityNode(EqualityNodeId nodeId) const return d_equalityNodes[nodeId]; } -void EqualityEngine::assertEqualityInternal(TNode t1, TNode t2, TNode reason, MergeReasonType pid) { +void EqualityEngine::assertEqualityInternal(TNode t1, TNode t2, TNode reason, unsigned pid) { Debug("equality") << d_name << "::eq::addEqualityInternal(" << t1 << "," << t2 << "), pid = " << pid << std::endl; @@ -407,7 +409,7 @@ void EqualityEngine::assertEqualityInternal(TNode t1, TNode t2, TNode reason, Me enqueue(MergeCandidate(t1Id, t2Id, pid, reason)); } -void EqualityEngine::assertPredicate(TNode t, bool polarity, TNode reason, MergeReasonType pid) { +void EqualityEngine::assertPredicate(TNode t, bool polarity, TNode reason, unsigned pid) { Debug("equality") << d_name << "::eq::addPredicate(" << t << "," << (polarity ? "true" : "false") << ")" << std::endl; Assert(t.getKind() != kind::EQUAL, "Use assertEquality instead"); assertEqualityInternal(t, polarity ? d_true : d_false, reason, pid); @@ -420,7 +422,7 @@ void EqualityEngine::mergePredicates(TNode p, TNode q, TNode reason) { propagate(); } -void EqualityEngine::assertEquality(TNode eq, bool polarity, TNode reason, MergeReasonType pid) { +void EqualityEngine::assertEquality(TNode eq, bool polarity, TNode reason, unsigned pid) { Debug("equality") << d_name << "::eq::addEquality(" << eq << "," << (polarity ? "true" : "false") << ")" << std::endl; if (polarity) { // If two terms are already equal, don't assert anything @@ -888,7 +890,7 @@ void EqualityEngine::backtrack() { } -void EqualityEngine::addGraphEdge(EqualityNodeId t1, EqualityNodeId t2, MergeReasonType type, TNode reason) { +void EqualityEngine::addGraphEdge(EqualityNodeId t1, EqualityNodeId t2, unsigned type, TNode reason) { Debug("equality") << d_name << "::eq::addGraphEdge(" << d_nodes[t1] << "," << d_nodes[t2] << "," << reason << ")" << std::endl; EqualityEdgeId edge = d_equalityEdges.size(); d_equalityEdges.push_back(EqualityEdge(t2, d_equalityGraph[t1], type, reason)); @@ -1089,7 +1091,7 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st // The current node currentNode = bfsQueue[currentIndex].nodeId; EqualityNodeId edgeNode = d_equalityEdges[currentEdge].getNodeId(); - MergeReasonType reasonType = d_equalityEdges[currentEdge].getReasonType(); + unsigned reasonType = d_equalityEdges[currentEdge].getReasonType(); Node reason = d_equalityEdges[currentEdge].getReason(); Debug("equality") << d_name << "::eq::getExplanation(): currentEdge = " << currentEdge << ", currentNode = " << currentNode << std::endl; @@ -1711,12 +1713,16 @@ size_t EqualityEngine::getSize(TNode t) { } -void EqualityEngine::addPathReconstructionTrigger(MergeReasonType trigger, const PathReconstructionNotify* notify) { +void EqualityEngine::addPathReconstructionTrigger(unsigned trigger, const PathReconstructionNotify* notify) { // Currently we can only inform one callback per trigger Assert(d_pathReconstructionTriggers.find(trigger) == d_pathReconstructionTriggers.end()); d_pathReconstructionTriggers[trigger] = notify; } +unsigned EqualityEngine::getFreshMergeReasonType() { + return d_freshMergeReasonType++; +} + void EqualityEngine::addTriggerTerm(TNode t, TheoryId tag) { Debug("equality::trigger") << d_name << "::eq::addTriggerTerm(" << t << ", " << tag << ")" << std::endl; @@ -2221,7 +2227,6 @@ void EqProof::debug_print( const char * c, unsigned tb ) const{ Debug( c ) << ")" << std::endl; } - } // Namespace uf } // Namespace theory } // Namespace CVC4 diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h index 97abfccf1..7bc645c24 100644 --- a/src/theory/uf/equality_engine.h +++ b/src/theory/uf/equality_engine.h @@ -149,7 +149,7 @@ public: virtual ~PathReconstructionNotify() {} - virtual void notify(MergeReasonType reasonType, Node reason, Node a, Node b, + virtual void notify(unsigned reasonType, Node reason, Node a, Node b, std::vector& equalities, EqProof* proof) const = 0; }; @@ -231,7 +231,7 @@ private: KindMap d_congruenceKindsInterpreted; /** Objects that need to be notified during equality path reconstruction */ - std::map d_pathReconstructionTriggers; + std::map d_pathReconstructionTriggers; /** Map from nodes to their ids */ __gnu_cxx::hash_map d_nodeIds; @@ -274,6 +274,9 @@ private: /** Memory for the use-list nodes */ std::vector d_useListNodes; + /** A fresh merge reason type to return upon request */ + unsigned d_freshMergeReasonType; + /** * We keep a list of asserted equalities. Not among original terms, but * among the class representatives. @@ -304,7 +307,7 @@ private: // The next edge EqualityEdgeId d_nextId; // Type of reason for this equality - MergeReasonType d_mergeType; + unsigned d_mergeType; // Reason of this equality TNode d_reason; @@ -313,7 +316,7 @@ private: EqualityEdge(): d_nodeId(null_edge), d_nextId(null_edge), d_mergeType(MERGED_THROUGH_CONGRUENCE) {} - EqualityEdge(EqualityNodeId nodeId, EqualityNodeId nextId, MergeReasonType type, TNode reason): + EqualityEdge(EqualityNodeId nodeId, EqualityNodeId nextId, unsigned type, TNode reason): d_nodeId(nodeId), d_nextId(nextId), d_mergeType(type), d_reason(reason) {} /** Returns the id of the next edge */ @@ -323,7 +326,7 @@ private: EqualityNodeId getNodeId() const { return d_nodeId; } /** The reason of this edge */ - MergeReasonType getReasonType() const { return d_mergeType; } + unsigned getReasonType() const { return d_mergeType; } /** The reason of this edge */ TNode getReason() const { return d_reason; } @@ -348,7 +351,7 @@ private: std::vector d_equalityGraph; /** Add an edge to the equality graph */ - void addGraphEdge(EqualityNodeId t1, EqualityNodeId t2, MergeReasonType type, TNode reason); + void addGraphEdge(EqualityNodeId t1, EqualityNodeId t2, unsigned type, TNode reason); /** Returns the equality node of the given node */ EqualityNode& getEqualityNode(TNode node); @@ -520,7 +523,7 @@ private: /** * Adds an equality of terms t1 and t2 to the database. */ - void assertEqualityInternal(TNode t1, TNode t2, TNode reason, MergeReasonType pid = MERGED_THROUGH_EQUALITY); + void assertEqualityInternal(TNode t1, TNode t2, TNode reason, unsigned pid = MERGED_THROUGH_EQUALITY); /** * Adds a trigger equality to the database with the trigger node and polarity for notification. @@ -744,7 +747,7 @@ public: * asserting the negated predicate * @param reason the reason to keep for building explanations */ - void assertPredicate(TNode p, bool polarity, TNode reason, MergeReasonType pid = MERGED_THROUGH_EQUALITY); + void assertPredicate(TNode p, bool polarity, TNode reason, unsigned pid = MERGED_THROUGH_EQUALITY); /** * Adds predicate p and q and makes them equal. @@ -759,7 +762,7 @@ public: * asserting the negated equality * @param reason the reason to keep for building explanations */ - void assertEquality(TNode eq, bool polarity, TNode reason, MergeReasonType pid = MERGED_THROUGH_EQUALITY); + void assertEquality(TNode eq, bool polarity, TNode reason, unsigned pid = MERGED_THROUGH_EQUALITY); /** * Returns the current representative of the term t. @@ -851,7 +854,12 @@ public: /** * Marks an object for merge type based notification during equality path reconstruction. */ - void addPathReconstructionTrigger(MergeReasonType trigger, const PathReconstructionNotify* notify); + void addPathReconstructionTrigger(unsigned trigger, const PathReconstructionNotify* notify); + + /** + * Returns a fresh merge reason type tag for the client to use. + */ + unsigned getFreshMergeReasonType(); }; /** @@ -895,7 +903,7 @@ class EqProof { public: EqProof() : d_id(MERGED_THROUGH_REFLEXIVITY){} - MergeReasonType d_id; + unsigned d_id; Node d_node; std::vector< EqProof * > d_children; void debug_print( const char * c, unsigned tb = 0 ) const; diff --git a/src/theory/uf/equality_engine_types.h b/src/theory/uf/equality_engine_types.h index 0c2c3e354..5bf9db436 100644 --- a/src/theory/uf/equality_engine_types.h +++ b/src/theory/uf/equality_engine_types.h @@ -67,14 +67,11 @@ enum MergeReasonType { MERGED_THROUGH_REFLEXIVITY, /** Equality was merged to false, due to both sides of equality being a constant */ MERGED_THROUGH_CONSTANTS, - /** (for proofs only) Equality was merged due to transitivity */ MERGED_THROUGH_TRANS, - /** Theory specific proof rules */ - MERGED_ARRAYS_ROW, - MERGED_ARRAYS_ROW1, - MERGED_ARRAYS_EXT + /** Reason types beyond this constant are theory specific reasons */ + NUMBER_OF_MERGE_REASONS }; inline std::ostream& operator << (std::ostream& out, MergeReasonType reason) { @@ -91,20 +88,11 @@ inline std::ostream& operator << (std::ostream& out, MergeReasonType reason) { case MERGED_THROUGH_CONSTANTS: out << "constants disequal"; break; - // (for proofs only) case MERGED_THROUGH_TRANS: out << "transitivity"; break; - case MERGED_ARRAYS_ROW: - out << "arrays ROW"; - break; - case MERGED_ARRAYS_ROW1: - out << "arrays ROW1"; - break; - case MERGED_ARRAYS_EXT: - out << "arrays EXT"; - break; -default: + + default: out << "[theory]"; break; } @@ -117,9 +105,9 @@ default: */ struct MergeCandidate { EqualityNodeId t1Id, t2Id; - MergeReasonType type; + unsigned type; TNode reason; - MergeCandidate(EqualityNodeId x, EqualityNodeId y, MergeReasonType type, TNode reason) + MergeCandidate(EqualityNodeId x, EqualityNodeId y, unsigned type, TNode reason) : t1Id(x), t2Id(y), type(type), reason(reason) {} }; -- 2.30.2