diff options
author | Guy <katz911@gmail.com> | 2016-04-03 15:58:58 -0700 |
---|---|---|
committer | Guy <katz911@gmail.com> | 2016-04-03 15:58:58 -0700 |
commit | 29df9622b570ce843756e05a3ef248de04d2a5c3 (patch) | |
tree | 6577c5eec908571f2ee0fb262c12b3612f0c3118 /src/theory | |
parent | cd5cc65fed2c850100a6f00067d102b48d262742 (diff) |
Removed the theory-specific merge reason types. Instead, added a mechanism for dynamically allocating these tags upon request.
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/arrays/array_proof_reconstruction.cpp | 40 | ||||
-rw-r--r-- | src/theory/arrays/array_proof_reconstruction.h | 13 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays.cpp | 39 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays.h | 9 | ||||
-rw-r--r-- | src/theory/uf/equality_engine.cpp | 19 | ||||
-rw-r--r-- | src/theory/uf/equality_engine.h | 30 | ||||
-rw-r--r-- | src/theory/uf/equality_engine_types.h | 24 |
7 files changed, 107 insertions, 67 deletions
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<TNode>& 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<TNode>& 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<TNode>& 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<MergeReasonType, const PathReconstructionNotify*> d_pathReconstructionTriggers; + std::map<unsigned, const PathReconstructionNotify*> d_pathReconstructionTriggers; /** Map from nodes to their ids */ __gnu_cxx::hash_map<TNode, EqualityNodeId, TNodeHashFunction> d_nodeIds; @@ -274,6 +274,9 @@ private: /** Memory for the use-list nodes */ std::vector<UseListNode> 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<EqualityEdgeId> 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) {} }; |