From: Dejan Jovanović Date: Thu, 24 May 2012 05:54:39 +0000 (+0000) Subject: Significant changes to the internals of the equality engine. Equality is not handled... X-Git-Tag: cvc5-1.0.0~8146 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=13e7de0006e9c34cc715521fc9f1866c25682113;p=cvc5.git Significant changes to the internals of the equality engine. Equality is not handled natively and not as a generic predicate. The changes also change the order of propagation, and can produce different conflicts. Since the engine is now used everywhere this means that so some crazy results are to be expected. --- diff --git a/src/theory/uf/Makefile.am b/src/theory/uf/Makefile.am index 9d95eaa22..50147b997 100644 --- a/src/theory/uf/Makefile.am +++ b/src/theory/uf/Makefile.am @@ -11,6 +11,7 @@ libuf_la_SOURCES = \ theory_uf_type_rules.h \ theory_uf_rewriter.h \ equality_engine.h \ + equality_engine_types.h \ equality_engine.cpp \ symmetry_breaker.h \ symmetry_breaker.cpp diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp index 2527893ff..e60d52c7a 100644 --- a/src/theory/uf/equality_engine.cpp +++ b/src/theory/uf/equality_engine.cpp @@ -58,11 +58,16 @@ void EqualityEngine::init() { Debug("equality") << "EqualityEdge::EqualityEngine(): id_null = " << +null_id << std::endl; Debug("equality") << "EqualityEdge::EqualityEngine(): edge_null = " << +null_edge << std::endl; Debug("equality") << "EqualityEdge::EqualityEngine(): trigger_null = " << +null_trigger << std::endl; + d_true = NodeManager::currentNM()->mkConst(true); d_false = NodeManager::currentNM()->mkConst(false); + addTerm(d_true); addTerm(d_false); + d_trueId = getNodeId(d_true); + d_falseId = getNodeId(d_false); + d_triggerDatabaseAllocatedSize = 100000; d_triggerDatabase = (char*) malloc(d_triggerDatabaseAllocatedSize); } @@ -75,14 +80,13 @@ EqualityEngine::~EqualityEngine() throw(AssertionException) { EqualityEngine::EqualityEngine(context::Context* context, std::string name) : ContextNotifyObj(context) , d_context(context) +, d_done(context, false) , d_performNotify(true) , d_notify(s_notifyNone) , d_applicationLookupsCount(context, 0) , d_nodesCount(context, 0) , d_assertedEqualitiesCount(context, 0) , d_equalityTriggersCount(context, 0) -, d_constantRepresentativesSize(context, 0) -, d_constantsSize(context, 0) , d_stats(name) , d_triggerDatabaseSize(context, 0) , d_triggerTermSetUpdatesSize(context, 0) @@ -93,14 +97,13 @@ EqualityEngine::EqualityEngine(context::Context* context, std::string name) EqualityEngine::EqualityEngine(EqualityEngineNotify& notify, context::Context* context, std::string name) : ContextNotifyObj(context) , d_context(context) +, d_done(context, false) , d_performNotify(true) , d_notify(notify) , d_applicationLookupsCount(context, 0) , d_nodesCount(context, 0) , d_assertedEqualitiesCount(context, 0) , d_equalityTriggersCount(context, 0) -, d_constantRepresentativesSize(context, 0) -, d_constantsSize(context, 0) , d_stats(name) , d_triggerDatabaseSize(context, 0) , d_triggerTermSetUpdatesSize(context, 0) @@ -109,22 +112,21 @@ EqualityEngine::EqualityEngine(EqualityEngineNotify& notify, context::Context* c } void EqualityEngine::enqueue(const MergeCandidate& candidate) { - Debug("equality") << "EqualityEngine::enqueue(" << candidate.toString(*this) << ")" << std::endl; d_propagationQueue.push(candidate); } -EqualityNodeId EqualityEngine::newApplicationNode(TNode original, EqualityNodeId t1, EqualityNodeId t2) { +EqualityNodeId EqualityEngine::newApplicationNode(TNode original, EqualityNodeId t1, EqualityNodeId t2, bool isEquality) { Debug("equality") << "EqualityEngine::newApplicationNode(" << original << ", " << t1 << ", " << t2 << ")" << std::endl; ++ d_stats.functionTermsCount; // Get another id for this EqualityNodeId funId = newNode(original); - FunctionApplication funOriginal(t1, t2); + FunctionApplication funOriginal(isEquality, t1, t2); // The function application we're creating EqualityNodeId t1ClassId = getEqualityNode(t1).getFind(); EqualityNodeId t2ClassId = getEqualityNode(t2).getFind(); - FunctionApplication funNormalized(t1ClassId, t2ClassId); + FunctionApplication funNormalized(isEquality, t1ClassId, t2ClassId); // We add the original version d_applications[funId] = FunctionApplicationPair(funOriginal, funNormalized); @@ -136,11 +138,17 @@ EqualityNodeId EqualityEngine::newApplicationNode(TNode original, EqualityNodeId Debug("equality") << "EqualityEngine::newApplicationNode(" << original << ", " << t1 << ", " << t2 << "): no lookup, setting up" << std::endl; // Mark the normalization to the lookup storeApplicationLookup(funNormalized, funId); + // If an equality, we do some extra reasoning + if (isEquality && d_isConstant[t1ClassId] && d_isConstant[t2ClassId]) { + if (t1ClassId != t2ClassId) { + Debug("equality") << "EqualityEngine::newApplicationNode(" << original << ", " << t1 << ", " << t2 << "): got constants" << std::endl; + enqueue(MergeCandidate(funId, d_falseId, MERGED_THROUGH_CONSTANTS, TNode::null())); + } + } } else { // If it's there, we need to merge these two Debug("equality") << "EqualityEngine::newApplicationNode(" << original << ", " << t1 << ", " << t2 << "): lookup exists, adding to queue" << std::endl; enqueue(MergeCandidate(funId, find->second, MERGED_THROUGH_CONGRUENCE, TNode::null())); - propagate(); } // Add to the use lists @@ -173,7 +181,9 @@ EqualityNodeId EqualityEngine::newNode(TNode node) { // Mark the no-individual trigger d_nodeIndividualTrigger.push_back(+null_set_id); // Mark non-constant by default - d_constantRepresentative.push_back(node.isConst() ? newId : +null_id); + d_isConstant.push_back(node.isConst()); + // Mark Boolean nodes + d_isBoolean.push_back(false); // Add the equality node to the nodes d_equalityNodes.push_back(EqualityNode(newId)); @@ -182,24 +192,6 @@ EqualityNodeId EqualityEngine::newNode(TNode node) { Debug("equality") << "EqualityEngine::newNode(" << node << ") => " << newId << std::endl; - // If the node is a constant, assert all the dis-eqalities - if (node.isConst() && node.getKind() != kind::CONST_BOOLEAN) { - - TypeNode nodeType = node.getType(); - for (unsigned i = 0; i < d_constants.size(); ++ i) { - TNode constant = d_constants[i]; - if (constant.getType().isComparableTo(nodeType)) { - Debug("equality::constants") << "adding const dis-equality " << node << " != " << constant << std::endl; - assertEquality(node.eqNode(constant), false, d_true); - } - } - - d_constants.push_back(node); - d_constantsSize = d_constantsSize + 1; - - propagate(); - } - return newId; } @@ -215,9 +207,11 @@ void EqualityEngine::addTerm(TNode t) { EqualityNodeId result; - // If a function application we go in - if (t.getNumChildren() > 0 && d_congruenceKinds[t.getKind()]) - { + if (t.getKind() == kind::EQUAL) { + addTerm(t[0]); + addTerm(t[1]); + result = newApplicationNode(t, getNodeId(t[0]), getNodeId(t[1]), true); + } else if (t.getNumChildren() > 0 && d_congruenceKinds[t.getKind()]) { // Add the operator TNode tOp = t.getOperator(); addTerm(tOp); @@ -227,13 +221,21 @@ void EqualityEngine::addTerm(TNode t) { // Add the child addTerm(t[i]); // Add the application - result = newApplicationNode(t, result, getNodeId(t[i])); + result = newApplicationNode(t, result, getNodeId(t[i]), false); } } else { // Otherwise we just create the new id result = newNode(t); } + if (t.getType().isBoolean()) { + // We set this here as this only applies to actual terms, not the + // intermediate application terms + d_isBoolean[result] = true; + } + + propagate(); + Debug("equality") << "EqualityEngine::addTerm(" << t << ") => " << result << std::endl; } @@ -334,6 +336,17 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect EqualityNodeId class1Id = class1.getFind(); EqualityNodeId class2Id = class2.getFind(); + // Check for constant merges + bool isConstant = d_isConstant[class1Id]; + if (isConstant && d_isConstant[class2Id]) { + if (d_performNotify) { + if (!d_notify.eqNotifyConstantTermMerge(d_nodes[class1Id], d_nodes[class2Id])) { + // Now merge the so that backtracking is OK + class1.merge(class2); + return false; + } + } + } // Update class2 representative information Debug("equality") << "EqualityEngine::merge(" << class1.getFind() << "," << class2.getFind() << "): updating class " << class2Id << std::endl; EqualityNodeId currentId = class2Id; @@ -370,67 +383,60 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect } while (currentId != class2Id); - // Update class2 table lookup and information - Debug("equality") << "EqualityEngine::merge(" << class1.getFind() << "," << class2.getFind() << "): updating lookups of " << class2Id << std::endl; - do { - // Get the current node - EqualityNode& currentNode = getEqualityNode(currentId); - Debug("equality") << "EqualityEngine::merge(" << class1.getFind() << "," << class2.getFind() << "): updating lookups of node " << currentId << std::endl; + // Update class2 table lookup and information if not a boolean + // since booleans can't be in an application + if (!d_isBoolean[class2Id]) { + Debug("equality") << "EqualityEngine::merge(" << class1.getFind() << "," << class2.getFind() << "): updating lookups of " << class2Id << std::endl; + do { + // Get the current node + EqualityNode& currentNode = getEqualityNode(currentId); + Debug("equality") << "EqualityEngine::merge(" << class1.getFind() << "," << class2.getFind() << "): updating lookups of node " << currentId << std::endl; - // Go through the uselist and check for congruences - UseListNodeId currentUseId = currentNode.getUseList(); - while (currentUseId != null_uselist_id) { - // Get the node of the use list - UseListNode& useNode = d_useListNodes[currentUseId]; - // Get the function application - EqualityNodeId funId = useNode.getApplicationId(); - Debug("equality") << "EqualityEngine::merge(" << class1.getFind() << "," << class2.getFind() << "): " << currentId << " in " << d_nodes[funId] << std::endl; - const FunctionApplication& fun = d_applications[useNode.getApplicationId()].normalized; - // Check if there is an application with find arguments - EqualityNodeId aNormalized = getEqualityNode(fun.a).getFind(); - EqualityNodeId bNormalized = getEqualityNode(fun.b).getFind(); - FunctionApplication funNormalized(aNormalized, bNormalized); - ApplicationIdsMap::iterator find = d_applicationLookup.find(funNormalized); - if (find != d_applicationLookup.end()) { - // Applications fun and the funNormalized can be merged due to congruence - if (getEqualityNode(funId).getFind() != getEqualityNode(find->second).getFind()) { - enqueue(MergeCandidate(funId, find->second, MERGED_THROUGH_CONGRUENCE, TNode::null())); + // Go through the uselist and check for congruences + UseListNodeId currentUseId = currentNode.getUseList(); + while (currentUseId != null_uselist_id) { + // Get the node of the use list + UseListNode& useNode = d_useListNodes[currentUseId]; + // Get the function application + EqualityNodeId funId = useNode.getApplicationId(); + Debug("equality") << "EqualityEngine::merge(" << class1.getFind() << "," << class2.getFind() << "): " << currentId << " in " << d_nodes[funId] << std::endl; + const FunctionApplication& fun = d_applications[useNode.getApplicationId()].normalized; + // Check if there is an application with find arguments + EqualityNodeId aNormalized = getEqualityNode(fun.a).getFind(); + EqualityNodeId bNormalized = getEqualityNode(fun.b).getFind(); + FunctionApplication funNormalized(fun.isEquality, aNormalized, bNormalized); + ApplicationIdsMap::iterator find = d_applicationLookup.find(funNormalized); + if (find != d_applicationLookup.end()) { + // Applications fun and the funNormalized can be merged due to congruence + if (getEqualityNode(funId).getFind() != getEqualityNode(find->second).getFind()) { + enqueue(MergeCandidate(funId, find->second, MERGED_THROUGH_CONGRUENCE, TNode::null())); + } + } else { + // There is no representative, so we can add one, we remove this when backtracking + storeApplicationLookup(funNormalized, funId); + // Now, if we're constant and it's an equality, check if the other guy is also a constant + if (isConstant && funNormalized.isEquality) { + if (d_isConstant[funNormalized.a] && d_isConstant[funNormalized.b]) { + // both constants + if (funNormalized.a != funNormalized.b) { + enqueue(MergeCandidate(funId, d_falseId, MERGED_THROUGH_CONSTANTS, TNode::null())); + } + } + } } - } else { - // There is no representative, so we can add one, we remove this when backtracking - storeApplicationLookup(funNormalized, funId); + + // Go to the next one in the use list + currentUseId = useNode.getNext(); } - // Go to the next one in the use list - currentUseId = useNode.getNext(); - } - - // Move to the next node - currentId = currentNode.getNext(); - } while (currentId != class2Id); - + + // Move to the next node + currentId = currentNode.getNext(); + } while (currentId != class2Id); + } + // Now merge the lists class1.merge(class2); - - // Check for constants - EqualityNodeId class2constId = d_constantRepresentative[class2Id]; - if (class2constId != +null_id) { - EqualityNodeId class1constId = d_constantRepresentative[class1Id]; - if (class1constId != +null_id) { - if (d_performNotify) { - TNode const1 = d_nodes[class1constId]; - TNode const2 = d_nodes[class2constId]; - if (!d_notify.eqNotifyConstantTermMerge(const1, const2)) { - return false; - } - } - } else { - // If the class we're merging in is constant, mark the representative as constant - d_constantRepresentative[class1Id] = d_constantRepresentative[class2Id]; - d_constantRepresentatives.push_back(class1Id); - d_constantRepresentativesSize = d_constantRepresentativesSize + 1; - } - } - + // Notify the trigger term merges TriggerTermSetRef class2triggerRef = d_nodeIndividualTrigger[class2Id]; if (class2triggerRef != +null_set_id) { @@ -576,14 +582,6 @@ void EqualityEngine::backtrack() { d_triggerTermSetUpdates.resize(d_triggerTermSetUpdatesSize); } - if (d_constantRepresentatives.size() > d_constantRepresentativesSize) { - // Unset the constant representatives - for (int i = d_constantRepresentatives.size() - 1, i_end = d_constantRepresentativesSize; i >= i_end; -- i) { - d_constantRepresentative[d_constantRepresentatives[i]] = +null_id; - } - d_constantRepresentatives.resize(d_constantRepresentativesSize); - } - if (d_equalityTriggers.size() > d_equalityTriggersCount) { // Unlink the triggers from the lists for (int i = d_equalityTriggers.size() - 1, i_end = d_equalityTriggersCount; i >= i_end; -- i) { @@ -623,12 +621,11 @@ void EqualityEngine::backtrack() { d_applications.resize(d_nodesCount); d_nodeTriggers.resize(d_nodesCount); d_nodeIndividualTrigger.resize(d_nodesCount); - d_constantRepresentative.resize(d_nodesCount); + d_isConstant.resize(d_nodesCount); + d_isBoolean.resize(d_nodesCount); d_equalityGraph.resize(d_nodesCount); d_equalityNodes.resize(d_nodesCount); } - - d_constants.resize(d_constantsSize); } void EqualityEngine::addGraphEdge(EqualityNodeId t1, EqualityNodeId t2, MergeReasonType type, TNode reason) { @@ -698,14 +695,18 @@ void EqualityEngine::explainPredicate(TNode p, bool polarity, std::vector addTerm(p); // Get the explanation - getExplanation(getNodeId(p), getNodeId(polarity ? d_true : d_false), assertions); + getExplanation(getNodeId(p), polarity ? d_trueId : d_falseId, assertions); } void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, std::vector& equalities) const { Debug("equality") << "EqualityEngine::getExplanation(" << d_nodes[t1Id] << "," << d_nodes[t2Id] << ")" << std::endl; - Assert(getEqualityNode(t1Id).getFind() == getEqualityNode(t2Id).getFind()); + // We can only explain the nodes that got merged (or between + // constants since they didn't get merged but we stil added the + // edge in the graph equality + Assert(getEqualityNode(t1Id).getFind() == getEqualityNode(t2Id).getFind() || + (d_isConstant[getEqualityNode(t1Id).getFind()] && d_isConstant[getEqualityNode(t2Id).getFind()])); // If the nodes are the same, we're done if (t1Id == t2Id) return; @@ -759,7 +760,8 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st Debug("equality") << "EqualityEngine::getExplanation(): currentEdge = " << currentEdge << ", currentNode = " << currentNode << std::endl; // Add the actual equality to the vector - if (reasonType == MERGED_THROUGH_CONGRUENCE) { + switch (reasonType) { + case MERGED_THROUGH_CONGRUENCE: { // f(x1, x2) == f(y1, y2) because x1 = y1 and x2 = y2 Debug("equality") << "EqualityEngine::getExplanation(): due to congruence, going deeper" << std::endl; const FunctionApplication& f1 = d_applications[currentNode].original; @@ -768,15 +770,37 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st getExplanation(f1.a, f2.a, equalities); getExplanation(f1.b, f2.b, equalities); Debug("equality") << pop; - } else { + break; + } + case MERGED_THROUGH_EQUALITY: // Construct the equality Debug("equality") << "EqualityEngine::getExplanation(): adding: " << d_equalityEdges[currentEdge].getReason() << std::endl; equalities.push_back(d_equalityEdges[currentEdge].getReason()); + break; + case MERGED_THROUGH_CONSTANTS: { + // (a = b) == false bacause a and b are different constants + Debug("equality") << "EqualityEngine::getExplanation(): due to constants, going deeper" << std::endl; + EqualityNodeId eqId = currentNode == d_falseId ? edgeNode : currentNode; + const FunctionApplication& eq = d_applications[eqId].original; + Assert(eq.isEquality, "Must be an equality"); + + Debug("equality") << push; + // Explain why a is a constant + getExplanation(eq.a, getEqualityNode(eq.a).getFind(), equalities); + // Explain why b is a constant + getExplanation(eq.b, getEqualityNode(eq.b).getFind(), equalities); + Debug("equality") << pop; + + break; } - + default: + Unreachable(); + } + // Go to the previous currentEdge = bfsQueue[currentIndex].edgeId; currentIndex = bfsQueue[currentIndex].previousIndex; + } while (currentEdge != null_id); // Done @@ -870,14 +894,13 @@ void EqualityEngine::propagate() { Debug("equality") << "EqualityEngine::propagate()" << std::endl; - bool done = false; while (!d_propagationQueue.empty()) { // The current merge candidate const MergeCandidate current = d_propagationQueue.front(); d_propagationQueue.pop(); - if (done) { + if (d_done) { // If we're done, just empty the queue continue; } @@ -904,27 +927,35 @@ void EqualityEngine::propagate() { // One more equality added d_assertedEqualitiesCount = d_assertedEqualitiesCount + 1; - // Depending on the merge preference (such as size), merge them + // Depending on the merge preference (such as size, or being a constant), merge them std::vector triggers; - if (node2.getSize() > node1.getSize()) { + if (node2.getSize() > node1.getSize() || d_isConstant[t2classId]) { Debug("equality") << "EqualityEngine::propagate(): merging " << d_nodes[current.t1Id]<< " into " << d_nodes[current.t2Id] << std::endl; d_assertedEqualities.push_back(Equality(t2classId, t1classId)); - done = !merge(node2, node1, triggers); + if (!merge(node2, node1, triggers)) { + d_done = true; + } } else { Debug("equality") << "EqualityEngine::propagate(): merging " << d_nodes[current.t2Id] << " into " << d_nodes[current.t1Id] << std::endl; d_assertedEqualities.push_back(Equality(t1classId, t2classId)); - done = !merge(node1, node2, triggers); + if (!merge(node1, node2, triggers)) { + d_done = true; + } } // Notify the triggers - if (d_performNotify && !done) { - for (size_t trigger_i = 0, trigger_end = triggers.size(); trigger_i < trigger_end && !done; ++ trigger_i) { + if (d_performNotify && !d_done) { + for (size_t trigger_i = 0, trigger_end = triggers.size(); trigger_i < trigger_end && !d_done; ++ trigger_i) { const TriggerInfo& triggerInfo = d_equalityTriggersOriginal[triggers[trigger_i]]; // Notify the trigger and exit if it fails if (triggerInfo.trigger.getKind() == kind::EQUAL) { - done = !d_notify.eqNotifyTriggerEquality(triggerInfo.trigger, triggerInfo.polarity); + if (!d_notify.eqNotifyTriggerEquality(triggerInfo.trigger, triggerInfo.polarity)) { + d_done = true; + } } else { - done = !d_notify.eqNotifyTriggerPredicate(triggerInfo.trigger, triggerInfo.polarity); + if (!d_notify.eqNotifyTriggerPredicate(triggerInfo.trigger, triggerInfo.polarity)) { + d_done = true; + } } } } diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h index c59436aaf..8fc57eb48 100644 --- a/src/theory/uf/equality_engine.h +++ b/src/theory/uf/equality_engine.h @@ -24,7 +24,6 @@ #include #include #include -#include #include "expr/node.h" #include "expr/kind_map.h" @@ -34,186 +33,12 @@ #include "theory/rewriter.h" #include "theory/theory.h" +#include "theory/uf/equality_engine_types.h" + namespace CVC4 { namespace theory { namespace eq { -/** Id of the node */ -typedef size_t EqualityNodeId; - -/** Id of the use list */ -typedef size_t UseListNodeId; - -/** The trigger ids */ -typedef size_t TriggerId; - -/** The equality edge ids */ -typedef size_t EqualityEdgeId; - -/** The null node */ -static const EqualityNodeId null_id = (size_t)(-1); - -/** The null use list node */ -static const EqualityNodeId null_uselist_id = (size_t)(-1); - -/** The null trigger */ -static const TriggerId null_trigger = (size_t)(-1); - -/** The null edge id */ -static const EqualityEdgeId null_edge = (size_t)(-1); - -/** - * A reason for a merge. Either an equality x = y, or a merge of two - * function applications f(x1, x2), f(y1, y2) - */ -enum MergeReasonType { - MERGED_THROUGH_CONGRUENCE, - MERGED_THROUGH_EQUALITY -}; - -inline std::ostream& operator << (std::ostream& out, MergeReasonType reason) { - switch (reason) { - case MERGED_THROUGH_CONGRUENCE: - out << "c"; - break; - case MERGED_THROUGH_EQUALITY: - out << "e"; - break; - default: - Unreachable(); - } - return out; -} - -/** A node in the uselist */ -class UseListNode { - -private: - - /** The id of the application node where this representative is at */ - EqualityNodeId d_applicationId; - - /** The next one in the class */ - UseListNodeId d_nextUseListNodeId; - -public: - - /** - * Creates a new node, which is in a list of it's own. - */ - UseListNode(EqualityNodeId nodeId = null_id, UseListNodeId nextId = null_uselist_id) - : d_applicationId(nodeId), d_nextUseListNodeId(nextId) {} - - /** - * Returns the next node in the circular list. - */ - UseListNodeId getNext() const { - return d_nextUseListNodeId; - } - - /** - * Returns the id of the function application. - */ - EqualityNodeId getApplicationId() const { - return d_applicationId; - } -}; - - -class EqualityNode { - -private: - - /** The size of this equivalence class (if it's a representative) */ - size_t d_size; - - /** The id (in the eq-manager) of the representative equality node */ - EqualityNodeId d_findId; - - /** The next equality node in this class */ - EqualityNodeId d_nextId; - - /** The use list of this node */ - UseListNodeId d_useList; - -public: - - /** - * Creates a new node, which is in a list of it's own. - */ - EqualityNode(EqualityNodeId nodeId = null_id) - : d_size(1), - d_findId(nodeId), - d_nextId(nodeId), - d_useList(null_uselist_id) - {} - - /** - * Retuerns the uselist. - */ - UseListNodeId getUseList() const { - return d_useList; - } - - /** - * Returns the next node in the class circular list. - */ - EqualityNodeId getNext() const { - return d_nextId; - } - - /** - * Returns the size of this equivalence class (only valid if this is the representative). - */ - size_t getSize() const { - return d_size; - } - - /** - * Merges the two lists. If add size is true the size of this node is increased by the size of - * the other node, otherwise the size is decreased by the size of the other node. - */ - template - void merge(EqualityNode& other) { - EqualityNodeId tmp = d_nextId; d_nextId = other.d_nextId; other.d_nextId = tmp; - if (addSize) { - d_size += other.d_size; - } else { - d_size -= other.d_size; - } - } - - /** - * Returns the class representative. - */ - EqualityNodeId getFind() const { return d_findId; } - - /** - * Set the class representative. - */ - void setFind(EqualityNodeId findId) { d_findId = findId; } - - /** - * Note that this node is used in a function a application funId. - */ - template - void usedIn(EqualityNodeId funId, memory_class& memory) { - UseListNodeId newUseId = memory.size(); - memory.push_back(UseListNode(funId, d_useList)); - d_useList = newUseId; - } - - /** - * For backtracking: remove the first element from the uselist and pop the memory. - */ - template - void removeTopFromUseList(memory_class& memory) { - Assert ((int)d_useList == (int)memory.size() - 1); - d_useList = memory.back().getNext(); - memory.pop_back(); - } -}; - /** * Interface for equality engine notifications. All the notifications * are safe as TNodes, but not necessarily for negations. @@ -316,30 +141,6 @@ public: } }; - /** - * f(a,b) - */ - struct FunctionApplication { - EqualityNodeId a, b; - FunctionApplication(EqualityNodeId a = null_id, EqualityNodeId b = null_id): - a(a), b(b) {} - bool operator == (const FunctionApplication& other) const { - return a == other.a && b == other.b; - } - bool isApplication() const { - return a != null_id && b != null_id; - } - }; - - struct FunctionApplicationHashFunction { - size_t operator () (const FunctionApplication& app) const { - size_t hash = 0; - hash = 0x9e3779b9 + app.a; - hash ^= 0x9e3779b9 + app.b + (hash << 6) + (hash >> 2); - return hash; - } - }; - /** * Store the application lookup, with enough information to backtrack */ @@ -350,6 +151,9 @@ private: /** The context we are using */ context::Context* d_context; + /** If we are done, we don't except any new assertions */ + context::CDO d_done; + /** Whether to notify or not (temporarily disabled on equality checks) */ bool d_performNotify; @@ -375,13 +179,13 @@ private: std::vector d_applicationLookups; /** Number of application lookups, for backtracking. */ - context::CDO d_applicationLookupsCount; + context::CDO d_applicationLookupsCount; /** Map from ids to the nodes (these need to be nodes as we pick-up the opreators) */ std::vector d_nodes; /** A context-dependents count of nodes */ - context::CDO d_nodesCount; + context::CDO d_nodesCount; /** * At time of addition a function application can already normalize to something, so @@ -404,7 +208,7 @@ private: std::vector d_equalityNodes; /** Number of asserted equalities we have so far */ - context::CDO d_assertedEqualitiesCount; + context::CDO d_assertedEqualitiesCount; /** Memory for the use-list nodes */ std::vector d_useListNodes; @@ -550,7 +354,7 @@ private: /** * Context dependent count of triggers */ - context::CDO d_equalityTriggersCount; + context::CDO d_equalityTriggersCount; /** * Trigger lists per node. The begin id changes as we merge, but the end always points to @@ -559,23 +363,15 @@ private: std::vector d_nodeTriggers; /** - * Map from ids to the id of the constant that is the representative. + * Map from ids to wheather they are constants (constants are always + * representatives of their class. */ - std::vector d_constantRepresentative; + std::vector d_isConstant; /** - * Size of the constant representatives list. + * Map from ids to wheather they are Boolean. */ - context::CDO d_constantRepresentativesSize; - - /** The list of representatives that became constant. */ - std::vector d_constantRepresentatives; - - /** List of all the constants. */ - std::vector d_constants; - - /** Size of the constants list */ - context::CDO d_constantsSize; + std::vector d_isBoolean; /** * Adds the trigger with triggerId to the beginning of the trigger list of the node with id nodeId. @@ -586,25 +382,11 @@ private: Statistics d_stats; /** Add a new function application node to the database, i.e APP t1 t2 */ - EqualityNodeId newApplicationNode(TNode original, EqualityNodeId t1, EqualityNodeId t2); + EqualityNodeId newApplicationNode(TNode original, EqualityNodeId t1, EqualityNodeId t2, bool isEquality); /** Add a new node to the database */ EqualityNodeId newNode(TNode t); - struct MergeCandidate { - EqualityNodeId t1Id, t2Id; - MergeReasonType type; - TNode reason; - MergeCandidate(EqualityNodeId x, EqualityNodeId y, MergeReasonType type, TNode reason): - t1Id(x), t2Id(y), type(type), reason(reason) {} - - std::string toString(EqualityEngine& eqEngine) const { - std::stringstream ss; - ss << eqEngine.d_nodes[t1Id] << " = " << eqEngine.d_nodes[t2Id] << ", " << type; - return ss.str(); - } - }; - /** Propagation queue */ std::queue d_propagationQueue; @@ -628,8 +410,13 @@ private: /** The true node */ Node d_true; + /** True node id */ + EqualityNodeId d_trueId; + /** The false node */ Node d_false; + /** False node id */ + EqualityNodeId d_falseId; /** * Adds an equality of terms t1 and t2 to the database. @@ -680,13 +467,13 @@ private: char* d_triggerDatabase; /** Allocated size of the trigger term database */ - size_t d_triggerDatabaseAllocatedSize ; + DefaultSizeType d_triggerDatabaseAllocatedSize ; /** Reference for the trigger terms set */ - typedef size_t TriggerTermSetRef; + typedef DefaultSizeType TriggerTermSetRef; /** Null reference */ - static const TriggerTermSetRef null_set_id = (size_t)(-1); + static const TriggerTermSetRef null_set_id = (TriggerTermSetRef)(-1); /** Create new trigger term set based on the internally set information */ TriggerTermSetRef newTriggerTermSet(); @@ -704,7 +491,7 @@ private: } /** Used part of the trigger term database */ - context::CDO d_triggerDatabaseSize; + context::CDO d_triggerDatabaseSize; struct TriggerSetUpdate { EqualityNodeId classId; diff --git a/src/theory/uf/equality_engine_types.h b/src/theory/uf/equality_engine_types.h new file mode 100644 index 000000000..a0d84a1ed --- /dev/null +++ b/src/theory/uf/equality_engine_types.h @@ -0,0 +1,272 @@ +/********************* */ +/*! \file equality_engine_types.h + ** \verbatim + ** Original author: dejan + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + +#include "cvc4_private.h" + +#include +#include +#include + +namespace CVC4 { +namespace theory { +namespace eq { + +/** Default type for the size of the sizes (size_t replacement) */ +typedef uint32_t DefaultSizeType; + +/** Id of the node */ +typedef DefaultSizeType EqualityNodeId; + +/** Id of the use list */ +typedef DefaultSizeType UseListNodeId; + +/** The trigger ids */ +typedef DefaultSizeType TriggerId; + +/** The equality edge ids */ +typedef DefaultSizeType EqualityEdgeId; + +/** The null node */ +static const EqualityNodeId null_id = (EqualityNodeId)(-1); + +/** The null use list node */ +static const EqualityNodeId null_uselist_id = (EqualityNodeId)(-1); + +/** The null trigger */ +static const TriggerId null_trigger = (TriggerId)(-1); + +/** The null edge id */ +static const EqualityEdgeId null_edge = (EqualityEdgeId)(-1); + +/** + * A reason for a merge. Either an equality x = y, a merge of two + * function applications f(x1, x2), f(y1, y2) due to congruence, + * or a merge of an equality to false due to both sides being + * (different) constants. + */ +enum MergeReasonType { + /** Terms were merged due to application of congruence closure */ + MERGED_THROUGH_CONGRUENCE, + /** Terms were merged due to application of pure equality */ + MERGED_THROUGH_EQUALITY, + /** Equality was merged to false, due to both sides of equality being a constant */ + MERGED_THROUGH_CONSTANTS, +}; + +inline std::ostream& operator << (std::ostream& out, MergeReasonType reason) { + switch (reason) { + case MERGED_THROUGH_CONGRUENCE: + out << "congruence"; + break; + case MERGED_THROUGH_EQUALITY: + out << "pure equality"; + break; + case MERGED_THROUGH_CONSTANTS: + out << "constants disequal"; + break; + default: + Unreachable(); + } + return out; +} + +/** + * A candidate for merging two equivalence classes, with the necessary + * additional information. + */ +struct MergeCandidate { + EqualityNodeId t1Id, t2Id; + MergeReasonType type; + TNode reason; + MergeCandidate(EqualityNodeId x, EqualityNodeId y, MergeReasonType type, TNode reason): + t1Id(x), t2Id(y), type(type), reason(reason) {} +}; + +/** + * We mantaint uselist where a node appears in, and this is the node + * of such a list. + */ +class UseListNode { + +private: + + /** The id of the application node where this representative is at */ + EqualityNodeId d_applicationId; + + /** The next one in the class */ + UseListNodeId d_nextUseListNodeId; + +public: + + /** + * Creates a new node, which is in a list of it's own. + */ + UseListNode(EqualityNodeId nodeId = null_id, UseListNodeId nextId = null_uselist_id) + : d_applicationId(nodeId), d_nextUseListNodeId(nextId) {} + + /** + * Returns the next node in the circular list. + */ + UseListNodeId getNext() const { + return d_nextUseListNodeId; + } + + /** + * Returns the id of the function application. + */ + EqualityNodeId getApplicationId() const { + return d_applicationId; + } +}; + +/** + * Main class for representing nodes in the equivalence class. The + * nodes are a circular list, with the representative carrying the + * size. Each individual node carries with itself the uselist of + * functino applications it appears in and the list of asserted + * disequalities it belongs to. In order to get these lists one must + * traverse the entire class and pick up all the individual lists. + */ +class EqualityNode { + +private: + + /** The size of this equivalence class (if it's a representative) */ + DefaultSizeType d_size; + + /** The id (in the eq-manager) of the representative equality node */ + EqualityNodeId d_findId; + + /** The next equality node in this class */ + EqualityNodeId d_nextId; + + /** The use list of this node */ + UseListNodeId d_useList; + +public: + + /** + * Creates a new node, which is in a list of it's own. + */ + EqualityNode(EqualityNodeId nodeId = null_id) + : d_size(1), + d_findId(nodeId), + d_nextId(nodeId), + d_useList(null_uselist_id) + {} + + /** + * Returns the function uselist. + */ + UseListNodeId getUseList() const { + return d_useList; + } + + /** + * Returns the next node in the class circular list. + */ + EqualityNodeId getNext() const { + return d_nextId; + } + + /** + * Returns the size of this equivalence class (only valid if this is the representative). + */ + DefaultSizeType getSize() const { + return d_size; + } + + /** + * Merges the two lists. If add size is true the size of this node is increased by the size of + * the other node, otherwise the size is decreased by the size of the other node. + */ + template + void merge(EqualityNode& other) { + EqualityNodeId tmp = d_nextId; d_nextId = other.d_nextId; other.d_nextId = tmp; + if (addSize) { + d_size += other.d_size; + } else { + d_size -= other.d_size; + } + } + + /** + * Returns the class representative. + */ + EqualityNodeId getFind() const { return d_findId; } + + /** + * Set the class representative. + */ + void setFind(EqualityNodeId findId) { d_findId = findId; } + + /** + * Note that this node is used in a function application funId, or + * a negatively asserted equality (dis-equality) with funId. + */ + template + void usedIn(EqualityNodeId funId, memory_class& memory) { + UseListNodeId newUseId = memory.size(); + memory.push_back(UseListNode(funId, d_useList)); + d_useList = newUseId; + } + + /** + * For backtracking: remove the first element from the uselist and pop the memory. + */ + template + void removeTopFromUseList(memory_class& memory) { + Assert ((int)d_useList == (int)memory.size() - 1); + d_useList = memory.back().getNext(); + memory.pop_back(); + } +}; + +/** + * Represents the function APPLY a b. If isEquality is true then it + * represents the predicate (a = b). Note that since one can not + * construct the equality over function terms, the equality and hash + * function below are still well defined. + */ +struct FunctionApplication { + bool isEquality; + EqualityNodeId a, b; + FunctionApplication(bool isEquality = false, EqualityNodeId a = null_id, EqualityNodeId b = null_id) + : isEquality(isEquality), a(a), b(b) {} + bool operator == (const FunctionApplication& other) const { + return a == other.a && b == other.b; + } + bool isApplication() const { + return a != null_id && b != null_id; + } +}; + +struct FunctionApplicationHashFunction { + size_t operator () (const FunctionApplication& app) const { + size_t hash = 0; + hash = 0x9e3779b9 + app.a; + hash ^= 0x9e3779b9 + app.b + (hash << 6) + (hash >> 2); + return hash; + } +}; + +} // namespace eq +} // namespace theory +} // namespace CVC4 + diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 0b9e1b3a7..9c1229f80 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -36,8 +36,6 @@ TheoryUF::TheoryUF(context::Context* c, context::UserContext* u, OutputChannel& { // The kinds we are treating as function application in congruence d_equalityEngine.addFunctionKind(kind::APPLY_UF); - d_equalityEngine.addFunctionKind(kind::EQUAL); - }/* TheoryUF::TheoryUF() */ static Node mkAnd(const std::vector& conjunctions) {