diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/theory/uf/Makefile.am | 1 | ||||
| -rw-r--r-- | src/theory/uf/equality_engine.cpp | 259 | ||||
| -rw-r--r-- | src/theory/uf/equality_engine.h | 261 | ||||
| -rw-r--r-- | src/theory/uf/equality_engine_types.h | 272 | ||||
| -rw-r--r-- | src/theory/uf/theory_uf.cpp | 2 |
5 files changed, 442 insertions, 353 deletions
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<bool>(true); d_false = NodeManager::currentNM()->mkConst<bool>(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<true>(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<true>(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<TNode> 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<TNode>& 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<TriggerId> 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 <queue> #include <vector> #include <ext/hash_map> -#include <sstream> #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<bool addSize> - 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<typename memory_class> - 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<typename memory_class> - 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. @@ -317,30 +142,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 */ void storeApplicationLookup(FunctionApplication& funNormalized, EqualityNodeId funId); @@ -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<bool> d_done; + /** Whether to notify or not (temporarily disabled on equality checks) */ bool d_performNotify; @@ -375,13 +179,13 @@ private: std::vector<FunctionApplication> d_applicationLookups; /** Number of application lookups, for backtracking. */ - context::CDO<size_t> d_applicationLookupsCount; + context::CDO<DefaultSizeType> d_applicationLookupsCount; /** Map from ids to the nodes (these need to be nodes as we pick-up the opreators) */ std::vector<Node> d_nodes; /** A context-dependents count of nodes */ - context::CDO<size_t> d_nodesCount; + context::CDO<DefaultSizeType> d_nodesCount; /** * At time of addition a function application can already normalize to something, so @@ -404,7 +208,7 @@ private: std::vector<EqualityNode> d_equalityNodes; /** Number of asserted equalities we have so far */ - context::CDO<size_t> d_assertedEqualitiesCount; + context::CDO<DefaultSizeType> d_assertedEqualitiesCount; /** Memory for the use-list nodes */ std::vector<UseListNode> d_useListNodes; @@ -550,7 +354,7 @@ private: /** * Context dependent count of triggers */ - context::CDO<size_t> d_equalityTriggersCount; + context::CDO<DefaultSizeType> 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<TriggerId> 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<EqualityNodeId> d_constantRepresentative; + std::vector<bool> d_isConstant; /** - * Size of the constant representatives list. + * Map from ids to wheather they are Boolean. */ - context::CDO<unsigned> d_constantRepresentativesSize; - - /** The list of representatives that became constant. */ - std::vector<EqualityNodeId> d_constantRepresentatives; - - /** List of all the constants. */ - std::vector<TNode> d_constants; - - /** Size of the constants list */ - context::CDO<unsigned> d_constantsSize; + std::vector<bool> 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<MergeCandidate> 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<size_t> d_triggerDatabaseSize; + context::CDO<DefaultSizeType> 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 <string> +#include <iostream> +#include <sstream> + +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<bool addSize> + 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<typename memory_class> + 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<typename memory_class> + 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<TNode>& conjunctions) { |