From 29df9622b570ce843756e05a3ef248de04d2a5c3 Mon Sep 17 00:00:00 2001 From: Guy Date: Sun, 3 Apr 2016 15:58:58 -0700 Subject: Removed the theory-specific merge reason types. Instead, added a mechanism for dynamically allocating these tags upon request. --- src/theory/arrays/array_proof_reconstruction.cpp | 40 +++++++++++++----------- src/theory/arrays/array_proof_reconstruction.h | 13 +++++++- src/theory/arrays/theory_arrays.cpp | 39 ++++++++++++++++------- src/theory/arrays/theory_arrays.h | 9 ++++++ 4 files changed, 70 insertions(+), 31 deletions(-) (limited to 'src/theory/arrays') 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, -- cgit v1.2.3