From 399788b6e81f9718e7870ef0b8061a77fb22b9cf Mon Sep 17 00:00:00 2001 From: Guy Date: Thu, 24 Mar 2016 16:56:13 -0700 Subject: [PATCH] Refactored the equality engine in order to remove theory-specific logic from equality path reconstruction --- src/Makefile.am | 2 + .../arrays/array_proof_reconstruction.cpp | 121 ++++++++++ .../arrays/array_proof_reconstruction.h | 40 ++++ src/theory/arrays/theory_arrays.cpp | 7 +- src/theory/arrays/theory_arrays.h | 4 + src/theory/uf/equality_engine.cpp | 213 +++--------------- src/theory/uf/equality_engine.h | 19 ++ 7 files changed, 224 insertions(+), 182 deletions(-) create mode 100644 src/theory/arrays/array_proof_reconstruction.cpp create mode 100644 src/theory/arrays/array_proof_reconstruction.h diff --git a/src/Makefile.am b/src/Makefile.am index 94ddf452a..77c69c9ec 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -287,6 +287,8 @@ libcvc4_la_SOURCES = \ theory/arrays/array_info.cpp \ theory/arrays/static_fact_manager.h \ theory/arrays/static_fact_manager.cpp \ + theory/arrays/array_proof_reconstruction.cpp \ + theory/arrays/array_proof_reconstruction.h \ theory/quantifiers/theory_quantifiers_type_rules.h \ theory/quantifiers/theory_quantifiers.h \ theory/quantifiers/quantifiers_rewriter.h \ diff --git a/src/theory/arrays/array_proof_reconstruction.cpp b/src/theory/arrays/array_proof_reconstruction.cpp new file mode 100644 index 000000000..b2e8c3ab3 --- /dev/null +++ b/src/theory/arrays/array_proof_reconstruction.cpp @@ -0,0 +1,121 @@ +/********************* */ +/*! \file array_proof_reconstruction.h + ** \verbatim + ** + ** \brief Array-specific proof construction logic to be used during the + ** equality engine's path reconstruction + **/ + +#include "theory/arrays/array_proof_reconstruction.h" + +namespace CVC4 { +namespace theory { +namespace arrays { + +ArrayProofReconstruction::ArrayProofReconstruction(const eq::EqualityEngine* equalityEngine) + : d_equalityEngine(equalityEngine) { +} + +void ArrayProofReconstruction::notify(eq::MergeReasonType 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 (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; + childProof->d_node = reason; + proof->d_children.push_back(childProof); + } + break; + } + + case eq::MERGED_ARRAYS_ROW: { + // 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). + + if (proof) { + if (a.getNumChildren() == 2) { + // This is the case of ((a[i]:=t)[k] == a[k]) because (i != k). + + // The edge is ((a[i]:=t)[k], a[k]), or (a[k], (a[i]:=t)[k]). This flag should be + // false in the first case and true in the second case. + bool currentNodeIsUnchangedArray; + + Assert(a.getNumChildren() == 2); + Assert(b.getNumChildren() == 2); + + if (a[0].getKind() == kind::VARIABLE || a[0].getKind() == kind::SKOLEM) { + currentNodeIsUnchangedArray = true; + } else if (b[0].getKind() == kind::VARIABLE || b[0].getKind() == kind::SKOLEM) { + currentNodeIsUnchangedArray = false; + } else { + Assert(a[0].getKind() == kind::STORE); + Assert(b[0].getKind() == kind::STORE); + + if (a[0][0] == b[0]) { + currentNodeIsUnchangedArray = false; + } else if (b[0][0] == a[0]) { + currentNodeIsUnchangedArray = true; + } else { + Unreachable(); + } + } + + Node indexOne = currentNodeIsUnchangedArray ? a[1] : a[0][1]; + Node indexTwo = currentNodeIsUnchangedArray ? b[0][1] : b[1]; + + // Some assertions to ensure that the theory of arrays behaves as expected + Assert(a[1] == b[1]); + if (currentNodeIsUnchangedArray) { + Assert(a[0] == b[0][0]); + } else { + Assert(a[0][0] == b[0]); + } + + Debug("pf::ee") << "Getting explanation for ROW guard: " + << indexOne << " != " << indexTwo << std::endl; + + eq::EqProof* childProof = new eq::EqProof; + d_equalityEngine->explainEquality(indexOne, indexTwo, false, equalities, childProof); + proof->d_children.push_back(childProof); + } else { + // This is the case of (i == k) because ((a[i]:=t)[k] != a[k]), + + Node indexOne = a; + Node indexTwo = b; + + Debug("pf::ee") << "The two indices are: " << indexOne << ", " << indexTwo << std::endl + << "The reason for the edge is: " << reason << std::endl; + + 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); + proof->d_children.push_back(childProof); + } + } + break; + } + + case eq::MERGED_ARRAYS_ROW1: { + // No special handling required at this time + break; + } + + default: + break; + } +} + +}/* CVC4::theory::arrays namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ diff --git a/src/theory/arrays/array_proof_reconstruction.h b/src/theory/arrays/array_proof_reconstruction.h new file mode 100644 index 000000000..8afc0d3f7 --- /dev/null +++ b/src/theory/arrays/array_proof_reconstruction.h @@ -0,0 +1,40 @@ +/********************* */ +/*! \file array_proof_reconstruction.h + ** \verbatim + ** + ** \brief Array-specific proof construction logic to be used during the + ** equality engine's path reconstruction + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__ARRAYS__ARRAY_PROOF_RECONSTRUCTION_H +#define __CVC4__THEORY__ARRAYS__ARRAY_PROOF_RECONSTRUCTION_H + +#include "theory/uf/equality_engine.h" + +namespace CVC4 { +namespace theory { +namespace arrays { + +/** + * A callback class to be invoked whenever the equality engine traverses + * an "array-owned" edge during path reconstruction. + */ + +class ArrayProofReconstruction : public eq::PathReconstructionNotify { +public: + ArrayProofReconstruction(const eq::EqualityEngine* equalityEngine); + + void notify(eq::MergeReasonType reasonType, Node reason, Node a, Node b, + std::vector& equalities, eq::EqProof* proof) const; + +private: + const eq::EqualityEngine* d_equalityEngine; +}; /* class ArrayProofReconstruction */ + +}/* CVC4::theory::arrays namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__THEORY__ARRAYS__ARRAY_PROOF_RECONSTRUCTION_H */ diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index fcde18b66..37854ee90 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -99,7 +99,8 @@ TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u, d_defValues(c), d_readTableContext(new context::Context()), d_arrayMerges(c), - d_inCheckModel(false) + d_inCheckModel(false), + d_proofReconstruction(&d_equalityEngine) { smtStatisticsRegistry()->registerStat(&d_numRow); smtStatisticsRegistry()->registerStat(&d_numExt); @@ -127,6 +128,10 @@ TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u, if (d_useArrTable) { 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); } TheoryArrays::~TheoryArrays() { diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index 2f69c52f9..6d2bb9e73 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -23,6 +23,7 @@ #include "context/cdhashset.h" #include "context/cdqueue.h" #include "theory/arrays/array_info.h" +#include "theory/arrays/array_proof_reconstruction.h" #include "theory/theory.h" #include "theory/uf/equality_engine.h" #include "util/statistics_registry.h" @@ -430,6 +431,9 @@ class TheoryArrays : public Theory { bool d_inCheckModel; int d_topLevel; + /** An equality-engine callback for proof reconstruction */ + ArrayProofReconstruction d_proofReconstruction; + public: eq::EqualityEngine* getEqualityEngine() { diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp index 53347c365..48aee1c35 100644 --- a/src/theory/uf/equality_engine.cpp +++ b/src/theory/uf/equality_engine.cpp @@ -942,10 +942,6 @@ void EqualityEngine::explainEquality(TNode t1, TNode t2, bool polarity, std::vec Assert(d_disequalityReasonsMap.find(pair) != d_disequalityReasonsMap.end(), "Don't ask for stuff I didn't notify you about"); DisequalityReasonRef reasonRef = d_disequalityReasonsMap.find(pair)->second; - for (unsigned i = reasonRef.mergesStart; i < reasonRef.mergesEnd; ++ i) { - EqualityPair toExplain = d_deducedDisequalityReasons[i]; - } - for (unsigned i = reasonRef.mergesStart; i < reasonRef.mergesEnd; ++ i) { EqualityPair toExplain = d_deducedDisequalityReasons[i]; @@ -956,15 +952,8 @@ void EqualityEngine::explainEquality(TNode t1, TNode t2, bool polarity, std::vec eqpc = new EqProof; } - // Some edges have the form ((a == b) == false). Translate this into (not (a == b)). - // Assert(d_nodes[toExplain.first] != NodeManager::currentNM()->mkConst(false)); - getExplanation(toExplain.first, toExplain.second, equalities, eqpc); - // if (eqpc) { - // eqp->d_children.push_back(eqpc); - // } - if (eqpc) { Debug("pf::ee") << "Child proof is:" << std::endl; eqpc->debug_print("pf::ee", 1); @@ -1101,6 +1090,7 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st currentNode = bfsQueue[currentIndex].nodeId; EqualityNodeId edgeNode = d_equalityEdges[currentEdge].getNodeId(); MergeReasonType reasonType = d_equalityEdges[currentEdge].getReasonType(); + Node reason = d_equalityEdges[currentEdge].getReason(); Debug("equality") << d_name << "::eq::getExplanation(): currentEdge = " << currentEdge << ", currentNode = " << currentNode << std::endl; Debug("equality") << d_name << " targetNode = " << d_nodes[edgeNode] << std::endl; @@ -1113,6 +1103,7 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st eqpc = new EqProof; eqpc->d_id = reasonType; } + // Add the actual equality to the vector switch (reasonType) { case MERGED_THROUGH_CONGRUENCE: { @@ -1121,10 +1112,6 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st const FunctionApplication& f1 = d_applications[currentNode].original; const FunctionApplication& f2 = d_applications[edgeNode].original; - Debug("pf::ee") << "We need to prove two equalities:" << std::endl; - Debug("pf::ee") << "\tLHS: " << d_nodes[f1.a] << " = " << d_nodes[f2.a] << std::endl; - Debug("pf::ee") << "\tRHS: " << d_nodes[f1.b] << " = " << d_nodes[f2.b] << std::endl; - Debug("equality") << push; Debug("equality") << "Explaining left hand side equalities" << std::endl; EqProof * eqpc1 = eqpc ? new EqProof : NULL; @@ -1135,51 +1122,36 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st if( eqpc ){ eqpc->d_children.push_back( eqpc1 ); eqpc->d_children.push_back( eqpc2 ); - Debug("pf::ee") << "Congruence : " << d_nodes[currentNode] << " " << d_nodes[edgeNode] << std::endl; if( d_nodes[currentNode].getKind()==kind::EQUAL ){ //leave node null for now eqpc->d_node = Node::null(); - }else{ - Debug("pf::ee") << d_nodes[f1.a] << " / " << d_nodes[f2.a] << ", " << d_nodes[f1.b] << " / " << d_nodes[f2.b] << std::endl; + } else { if(d_nodes[f1.a].getKind() == kind::APPLY_UF || d_nodes[f1.a].getKind() == kind::SELECT || d_nodes[f1.a].getKind() == kind::STORE) { eqpc->d_node = d_nodes[f1.a]; } else { - - Debug("pf::ee") << "f1.a is: " << d_nodes[f1.a] - << ". kind is: " << d_nodes[f1.a].getKind() << std::endl; - if (d_nodes[f1.a].getKind() == kind::BUILTIN && d_nodes[f1.a].getConst() == kind::SELECT) { - Debug("pf::ee") << "f1.a getConst is: " << d_nodes[f1.a].getConst() << std::endl; - eqpc->d_node = NodeManager::currentNM()->mkNode(kind::PARTIAL_SELECT_1, d_nodes[f1.b]); - // The first child is a PARTIAL_SELECT_0. Give it a child so that we know what kind of (read) it is, when we dump to LFSC. - Debug("pf::ee") << "eqpc->d_children[0]->d_node.getKind() == " << eqpc->d_children[0]->d_node.getKind() << std::endl; + // The first child is a PARTIAL_SELECT_0. + // Give it a child so that we know what kind of (read) it is, when we dump to LFSC. Assert(eqpc->d_children[0]->d_node.getKind() == kind::PARTIAL_SELECT_0); Assert(eqpc->d_children[0]->d_children.size() == 0); - Debug("pf::ee") << "Dumping the equality proof before:" << std::endl; - eqpc->debug_print("pf::ee", 1); - - eqpc->d_children[0]->d_node = NodeManager::currentNM()->mkNode(kind::PARTIAL_SELECT_0, d_nodes[f1.b]); - - Debug("pf::ee") << "Dumping the equality proof after:" << std::endl; - eqpc->debug_print("pf::ee", 1); - - //eqpc->d_children[0]->d_node.append(d_nodes[f1.b]); + eqpc->d_children[0]->d_node = NodeManager::currentNM()->mkNode(kind::PARTIAL_SELECT_0, + d_nodes[f1.b]); } else { eqpc->d_node = NodeManager::currentNM()->mkNode(kind::PARTIAL_APPLY_UF, ProofManager::currentPM()->mkOp(d_nodes[f1.a]), d_nodes[f1.b]); } - Debug("pf::ee") << "New d_node is: " << eqpc->d_node << std::endl; } } } Debug("equality") << pop; break; } + case MERGED_THROUGH_REFLEXIVITY: { // x1 == x1 Debug("equality") << d_name << "::eq::getExplanation(): due to reflexivity, going deeper" << std::endl; @@ -1198,6 +1170,7 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st break; } + case MERGED_THROUGH_CONSTANTS: { // f(c1, ..., cn) = c semantically, we can just ignore it Debug("equality") << d_name << "::eq::getExplanation(): due to constants, explain the constants" << std::endl; @@ -1221,169 +1194,41 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st } Debug("equality") << pop; - - break; - } - case MERGED_ARRAYS_EXT: - - Debug("equality") << d_name << "::eq::getExplanation(): MERGED_ARRAYS_EXT" << std::endl; - - if (eqpc) { - Node a = d_nodes[d_equalityEdges[currentEdge].getNodeId()]; - Node b = d_nodes[currentNode]; - - // GK: todo: here we assume that a=b is an assertion. We should probably call explain() - // recursively, to explain this. - - if (a == NodeManager::currentNM()->mkConst(false)) { - eqpc->d_node = b.notNode(); - } else if (b == NodeManager::currentNM()->mkConst(false)) { - eqpc->d_node = a.notNode(); - } else { - eqpc->d_node = a.eqNode(b); - } - - EqProof* eqpc1 = new EqProof; - eqpc1->d_node = d_equalityEdges[currentEdge].getReason(); - eqpc->d_children.push_back( eqpc1 ); - - eqpc1->debug_print("pf::ee", 1); - eqpc->debug_print("pf::ee", 1); - } - - // We push the reason into "equalities" because that's what the theory of arrays expects. - equalities.push_back(d_equalityEdges[currentEdge].getReason()); - break; - - case MERGED_ARRAYS_ROW: { - Debug("equality") << d_name << "::eq::getExplanation(): MERGED_ARRAYS_ROW" << std::endl; - - // 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). - - if (eqpc) { - if (d_nodes[currentNode].getNumChildren() == 2) { - // This is the case of ((a[i]:=t)[k] == a[k]) because (i != k). - - // The edge is ((a[i]:=t)[k], a[k]), or (a[k], (a[i]:=t)[k]). This flag should be - // false in the first case and true in the second case. - bool currentNodeIsUnchangedArray; - - Assert(d_nodes[currentNode].getNumChildren() == 2); - Assert(d_nodes[edgeNode].getNumChildren() == 2); - - if (d_nodes[currentNode][0].getKind() == kind::VARIABLE || - d_nodes[currentNode][0].getKind() == kind::SKOLEM) { - currentNodeIsUnchangedArray = true; - } else if (d_nodes[edgeNode][0].getKind() == kind::VARIABLE || - d_nodes[edgeNode][0].getKind() == kind::SKOLEM) { - currentNodeIsUnchangedArray = false; - } else { - Assert(d_nodes[currentNode][0].getKind() == kind::STORE); - Assert(d_nodes[edgeNode][0].getKind() == kind::STORE); - - if (d_nodes[currentNode][0][0] == d_nodes[edgeNode][0]) { - currentNodeIsUnchangedArray = false; - } else if (d_nodes[edgeNode][0][0] == d_nodes[currentNode][0]) { - currentNodeIsUnchangedArray = true; - } else { - Unreachable(); - } - } - - Node indexOne = - currentNodeIsUnchangedArray ? d_nodes[currentNode][1] : d_nodes[currentNode][0][1]; - Node indexTwo = - currentNodeIsUnchangedArray ? d_nodes[edgeNode][0][1] : d_nodes[edgeNode][1]; - - // Some assertions to ensure that the theory of arrays behaves as expected - Assert(d_nodes[currentNode][1] == d_nodes[edgeNode][1]); - if (currentNodeIsUnchangedArray) { - Assert(d_nodes[currentNode][0] == d_nodes[edgeNode][0][0]); - } else { - Assert(d_nodes[currentNode][0][0] == d_nodes[edgeNode][0]); - } - - Debug("pf::ee") << "Getting explanation for ROW guard: " - << indexOne << " != " << indexTwo << std::endl; - - EqProof* eqpcc = eqpc ? new EqProof : NULL; - explainEquality(indexOne, indexTwo, false, equalities, eqpcc); - - Debug("pf::ee") << "The two indices are: " << indexOne << ", " << indexTwo << std::endl; - Debug("pf::ee") << "And the explanation of their disequality is: " << std::endl; - eqpcc->debug_print("pf::ee", 1); - eqpc->d_children.push_back(eqpcc); - } else { - // This is the case of (i == k) because ((a[i]:=t)[k] != a[k]), - - Debug("pf::ee") << "In the new case of ROW!" << std::endl; - - Node indexOne = d_nodes[currentNode]; - Node indexTwo = d_nodes[edgeNode]; - - Debug("pf::ee") << "The two indices are: " << indexOne << ", " << indexTwo << std::endl; - Debug("pf::ee") << "The reason for the edge is: " << d_equalityEdges[currentEdge].getReason() - << std::endl; - - Assert(d_equalityEdges[currentEdge].getReason().getNumChildren() == 2); - Node reason = d_equalityEdges[currentEdge].getReason()[1]; - Debug("pf::ee") << "Getting explanation for ROW guard: " << reason << std::endl; - - EqProof* eqpcc = eqpc ? new EqProof : NULL; - explainEquality(reason[0], reason[1], false, equalities, eqpcc); - - if (eqpc) { - Debug("pf::ee") << "The guard's explanation is: " << std::endl; - eqpcc->debug_print("pf::ee", 1); - eqpc->d_children.push_back(eqpcc); - } - } - - Node a = d_nodes[d_equalityEdges[currentEdge].getNodeId()]; - Node b = d_nodes[currentNode]; - - if (a == NodeManager::currentNM()->mkConst(false)) { - eqpc->d_node = b.notNode(); - } else if (b == NodeManager::currentNM()->mkConst(false)) { - eqpc->d_node = a.notNode(); - } else { - eqpc->d_node = a.eqNode(b); - } - } - - // We push the reason into "equalities" because that's what the theory of arrays expects. - equalities.push_back(d_equalityEdges[currentEdge].getReason()); break; } default: { // Construct the equality - Debug("equality") << d_name << "::eq::getExplanation(): adding: " << d_equalityEdges[currentEdge].getReason() << std::endl; + Debug("equality") << d_name << "::eq::getExplanation(): adding: " + << reason << std::endl; Debug("equality") << d_name << "::eq::getExplanation(): reason type = " << reasonType << std::endl; + Node a = d_nodes[currentNode]; + Node b = d_nodes[d_equalityEdges[currentEdge].getNodeId()]; + + if (d_pathReconstructionTriggers.find(reasonType) != d_pathReconstructionTriggers.end()) { + d_pathReconstructionTriggers.find(reasonType)->second->notify(reasonType, reason, a, b, + equalities, eqpc); + } + if (eqpc) { if (reasonType == MERGED_THROUGH_EQUALITY) { - eqpc->d_node = d_equalityEdges[currentEdge].getReason(); + eqpc->d_node = reason; } else { - // The LFSC translator prefers (not (= a b)) over (= (a==b) false) - - Node a = d_nodes[d_equalityEdges[currentEdge].getNodeId()]; - Node b = d_nodes[currentNode]; + // The LFSC translator prefers (not (= a b)) over (= (= a b) false) if (a == NodeManager::currentNM()->mkConst(false)) { eqpc->d_node = b.notNode(); } else if (b == NodeManager::currentNM()->mkConst(false)) { eqpc->d_node = a.notNode(); } else { - eqpc->d_node = a.eqNode(b); + eqpc->d_node = b.eqNode(a); } - Debug("pf::ee") << "theory eq : " << eqpc->d_node << std::endl; } eqpc->d_id = reasonType; } - equalities.push_back(d_equalityEdges[currentEdge].getReason()); + + equalities.push_back(reason); break; } } @@ -1859,13 +1704,19 @@ bool EqualityEngine::areDisequal(TNode t1, TNode t2, bool ensureProof) const return false; } -size_t EqualityEngine::getSize(TNode t) -{ +size_t EqualityEngine::getSize(TNode t) { // Add the term addTermInternal(t); return getEqualityNode(getEqualityNode(t).getFind()).getSize(); } + +void EqualityEngine::addPathReconstructionTrigger(MergeReasonType 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; +} + void EqualityEngine::addTriggerTerm(TNode t, TheoryId tag) { Debug("equality::trigger") << d_name << "::eq::addTriggerTerm(" << t << ", " << tag << ")" << std::endl; diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h index 9cfa16adf..97abfccf1 100644 --- a/src/theory/uf/equality_engine.h +++ b/src/theory/uf/equality_engine.h @@ -140,6 +140,18 @@ public: void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) { } };/* class EqualityEngineNotifyNone */ +/** + * An interface for equality engine notifications during equality path reconstruction. + * Can be used to add theory-specific logic for, e.g., proof construction. + */ +class PathReconstructionNotify { +public: + + virtual ~PathReconstructionNotify() {} + + virtual void notify(MergeReasonType reasonType, Node reason, Node a, Node b, + std::vector& equalities, EqProof* proof) const = 0; +}; /** * Class for keeping an incremental congruence closure over a set of terms. It provides @@ -218,6 +230,9 @@ private: /** The map of kinds to be treated as interpreted function applications (for evaluation of constants) */ KindMap d_congruenceKindsInterpreted; + /** Objects that need to be notified during equality path reconstruction */ + std::map d_pathReconstructionTriggers; + /** Map from nodes to their ids */ __gnu_cxx::hash_map d_nodeIds; @@ -833,6 +848,10 @@ public: */ bool consistent() const { return !d_done; } + /** + * Marks an object for merge type based notification during equality path reconstruction. + */ + void addPathReconstructionTrigger(MergeReasonType trigger, const PathReconstructionNotify* notify); }; /** -- 2.30.2