diff options
Diffstat (limited to 'src/theory/uf')
-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 |
3 files changed, 37 insertions, 36 deletions
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) {} }; |