diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-06-07 07:11:24 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-06-07 07:11:24 +0000 |
commit | 49dd14da8d872403b4d772a2d49224e4d6bda227 (patch) | |
tree | 5abbd246c8a1bb797e97d4b9754a4f850e1dc1b5 /src/theory | |
parent | 67903280f8fe6946a36ef9fc08bfc747f74bfbd7 (diff) |
fixing some bugs in propagation of disequalities
still doesnt fix the wrong answers thought :(
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/arrays/theory_arrays.cpp | 5 | ||||
-rw-r--r-- | src/theory/theory.h | 1 | ||||
-rw-r--r-- | src/theory/theory_engine.cpp | 44 | ||||
-rw-r--r-- | src/theory/uf/equality_engine.cpp | 221 | ||||
-rw-r--r-- | src/theory/uf/equality_engine.h | 42 |
5 files changed, 244 insertions, 69 deletions
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 4ba4aeba5..91bbae2f4 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -581,8 +581,8 @@ void TheoryArrays::computeCareGraph() Assert(false); break; case EQUALITY_FALSE_AND_PROPAGATED: - // TODO: eventually this should be an Assert(false), but for now, disequalities are not propagated - continue; + // Should have been propagated to us + Assert(false); break; case EQUALITY_FALSE: case EQUALITY_TRUE: @@ -591,7 +591,6 @@ void TheoryArrays::computeCareGraph() break; case EQUALITY_FALSE_IN_MODEL: Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): false in model" << std::endl; - continue; break; default: break; diff --git a/src/theory/theory.h b/src/theory/theory.h index 36255d1d6..020a2b194 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -447,6 +447,7 @@ public: * the actual computation, and use addCarePair to add pairs to the care graph. */ void getCareGraph(CareGraph& careGraph) { + Trace("sharing") << "Theory<" << getId() << ">::getCareGraph()" << std::endl; TimerStat::CodeTimer computeCareGraphTime(d_computeCareGraphTime); d_careGraph = &careGraph; computeCareGraph(); diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index ca2460805..a7b13dc2f 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -190,6 +190,44 @@ void TheoryEngine::dumpAssertions(const char* tag) { Dump(tag) << AssertCommand(assertionExpr); } Dump(tag) << CheckSatCommand(); + + // Check for any missed propagations of shared terms + if (d_logicInfo.isSharingEnabled()) { + Dump(tag) << CommentCommand("Shared term equalities"); + context::CDList<TNode>::const_iterator it = theory->shared_terms_begin(), it_end = theory->shared_terms_end(); + for (; it != it_end; ++ it) { + TNode t1 = (*it); + context::CDList<TNode>::const_iterator it2 = it; + for (++ it2; it2 != it_end; ++ it2) { + TNode t2 = (*it2); + if (t1.getType() == t2.getType()) { + Node equality = t1.eqNode(t2); + if (d_sharedTerms.isKnown(equality)) { + continue; + } + Node disequality = equality.notNode(); + if (d_sharedTerms.isKnown(disequality)) { + continue; + } + + // Check equality + Dump(tag) << PushCommand(); + BoolExpr eqExpr(equality.toExpr()); + Dump(tag) << AssertCommand(eqExpr); + Dump(tag) << CheckSatCommand(); + Dump(tag) << PopCommand(); + + // Check disequality + Dump(tag) << PushCommand(); + BoolExpr diseqExpr(disequality.toExpr()); + Dump(tag) << AssertCommand(diseqExpr); + Dump(tag) << CheckSatCommand(); + Dump(tag) << PopCommand(); + } + } + } + } + Dump(tag) << PopCommand(); } } @@ -316,6 +354,8 @@ void TheoryEngine::combineTheories() { // Call on each parametric theory to give us its care graph CVC4_FOR_EACH_THEORY; + Debug("sharing") << "TheoryEngine::combineTheories(): care graph size = " << careGraph.size() << std::endl; + // Now add splitters for the ones we are interested in CareGraph::const_iterator care_it = careGraph.begin(); CareGraph::const_iterator care_it_end = careGraph.end(); @@ -328,7 +368,7 @@ void TheoryEngine::combineTheories() { Assert(!d_sharedTerms.areDisequal(carePair.a, carePair.b), "Please don't care about stuff you were notified about"); // The equality in question - Node equality = carePair.a.eqNode(carePair.b); + Node equality = Rewriter::rewriteEquality(carePair.theory, carePair.a.eqNode(carePair.b)); // Normalize the equality Node normalizedEquality = Rewriter::rewrite(equality); @@ -349,6 +389,8 @@ void TheoryEngine::combineTheories() { // Mark that we have more information d_factsAsserted = true; continue; + } else { + Unreachable(); } } } diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp index 4cd54a2bf..c5ccaaeea 100644 --- a/src/theory/uf/equality_engine.cpp +++ b/src/theory/uf/equality_engine.cpp @@ -351,14 +351,16 @@ void EqualityEngine::assertEquality(TNode eq, bool polarity, TNode reason) { // If both have constant representatives, we don't notify anyone EqualityNodeId a = getNodeId(eq[0]); EqualityNodeId b = getNodeId(eq[1]); - if (isConstant(a) && isConstant(b)) { + EqualityNodeId aClassId = getEqualityNode(a).getFind(); + EqualityNodeId bClassId = getEqualityNode(b).getFind(); + if (d_isConstant[aClassId] && d_isConstant[bClassId]) { return; } // If we are adding a disequality, notify of the shared term representatives EqualityNodeId eqId = getNodeId(eq); - TriggerTermSetRef aTriggerRef = d_nodeIndividualTrigger[a]; - TriggerTermSetRef bTriggerRef = d_nodeIndividualTrigger[b]; + TriggerTermSetRef aTriggerRef = d_nodeIndividualTrigger[aClassId]; + TriggerTermSetRef bTriggerRef = d_nodeIndividualTrigger[bClassId]; if (aTriggerRef != +null_set_id && bTriggerRef != +null_set_id) { // The sets of trigger terms TriggerTermSet& aTriggerTerms = getTriggerTermSet(aTriggerRef); @@ -419,8 +421,31 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect EqualityNodeId class2Id = class2.getFind(); // Check for constant merges - bool isConstant = d_isConstant[class1Id]; - Assert(isConstant || !d_isConstant[class2Id]); + bool class1isConstant = d_isConstant[class1Id]; + bool class2isConstant = d_isConstant[class2Id]; + Assert(class1isConstant || !class2isConstant, "Should always merge into constants"); + + // Trigger set of class 1 + TriggerTermSetRef class1triggerRef = d_nodeIndividualTrigger[class1Id]; + Theory::Set class1Tags = class1triggerRef == null_set_id ? 0 : getTriggerTermSet(class1triggerRef).tags; + // Trigger set of class 2 + TriggerTermSetRef class2triggerRef = d_nodeIndividualTrigger[class2Id]; + Theory::Set class2Tags = class2triggerRef == null_set_id ? 0 : getTriggerTermSet(class2triggerRef).tags; + + // Disequalities coming from class2 + TaggedEqualitiesSet class2disequalitiesToNotify; + // Disequalities coming from class1 + TaggedEqualitiesSet class1disequalitiesToNotify; + + // Individual tags + Theory::Set class1OnlyTags = Theory::setDifference(class1Tags, class2Tags); + Theory::Set class2OnlyTags = Theory::setDifference(class2Tags, class1Tags); + + // Only get disequalities if they are not both constant + if (!class1isConstant || !class2isConstant) { + getDisequalities(!class1isConstant, class2Id, class1OnlyTags, class2disequalitiesToNotify); + getDisequalities(!class2isConstant, class1Id, class2OnlyTags, class1disequalitiesToNotify); + } // Update class2 representative information Debug("equality") << "EqualityEngine::merge(" << class1.getFind() << "," << class2.getFind() << "): updating class " << class2Id << std::endl; @@ -519,7 +544,7 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect // Notify of the constants merge bool constantMerge = false; - if (isConstant && d_isConstant[class2Id]) { + if (class1isConstant && d_isConstant[class2Id]) { constantMerge = true; if (d_performNotify) { if (!d_notify.eqNotifyConstantTermMerge(d_nodes[class1Id], d_nodes[class2Id])) { @@ -547,10 +572,16 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect } triggersFired.resize(j); + // Go through the trigger term disequalities and propagate + if (!propagateTriggerTermDisequalities(class1OnlyTags, class1triggerRef, class2disequalitiesToNotify)) { + return false; + } + if (!propagateTriggerTermDisequalities(class2OnlyTags, class2triggerRef, class1disequalitiesToNotify)) { + return false; + } + // Notify the trigger term merges - TriggerTermSetRef class2triggerRef = d_nodeIndividualTrigger[class2Id]; if (class2triggerRef != +null_set_id) { - TriggerTermSetRef class1triggerRef = d_nodeIndividualTrigger[class1Id]; if (class1triggerRef == +null_set_id) { // If class1 doesn't have individual triggers, but class2 does, mark it d_nodeIndividualTrigger[class1Id] = class2triggerRef; @@ -1293,61 +1324,9 @@ void EqualityEngine::addTriggerTerm(TNode t, TheoryId tag) // Check for disequalities by going through the equivalence class looking for equalities in the // uselists that have been asserted to false. All the representatives appearing on the other // side of such disequalities, that have the tag on, are put in a set. - std::set<EqualityNodeId> disequalSet; - EqualityNodeId currentId = classId; - do { - // Current node - EqualityNode& currentNode = getEqualityNode(currentId); - // Go through the uselist and look for disequalities - UseListNodeId currentUseId = currentNode.getUseList(); - while (!d_done && currentUseId != null_uselist_id) { - // Get the normalized equality - UseListNode& useNode = d_useListNodes[currentUseId]; - EqualityNodeId funId = useNode.getApplicationId(); - const FunctionApplication& fun = d_applications[useNode.getApplicationId()].original; - // Check for asserted disequalities - if (fun.isEquality && getEqualityNode(funId).getFind() == getEqualityNode(d_false).getFind()) { - // Get the other equality member - EqualityNodeId toCompare = fun.b; - if (toCompare == currentId) { - toCompare = fun.a; - } - // Representative of the other member - EqualityNodeId toCompareRep = getEqualityNode(toCompare).getFind(); - Assert(toCompareRep != classId); - // Get the trigger set - TriggerTermSetRef toCompareTriggerSetRef = d_nodeIndividualTrigger[toCompareRep]; - // Only notify if we're not both constants - if ((!d_isConstant[classId] || !d_isConstant[toCompareRep]) && toCompareTriggerSetRef != null_set_id) { - TriggerTermSet& toCompareTriggerSet = getTriggerTermSet(toCompareTriggerSetRef); - if (Theory::setContains(tag, toCompareTriggerSet.tags)) { - // Get the tag representative - EqualityNodeId tagRep = toCompareTriggerSet.getTrigger(tag); - // Propagate the disequality if not already done - if (!disequalSet.count(tagRep) && d_performNotify) { - // Mark as propagated - disequalSet.insert(tagRep); - // Store the propagation - d_deducedDisequalityReasons.push_back(EqualityPair(eqNodeId, currentId)); - d_deducedDisequalityReasons.push_back(EqualityPair(toCompare, tagRep)); - d_deducedDisequalityReasons.push_back(EqualityPair(funId, d_falseId)); - storePropagatedDisequality(t, d_nodes[tagRep], 3); - // We don't check if it's been propagated already, as we need one per tag - if (d_performNotify) { - if (!d_notify.eqNotifyTriggerTermEquality(tag, t, d_nodes[tagRep], false)) { - d_done = true; - } - } - } - } - } - } - // Go to the next one in the use list - currentUseId = useNode.getNext(); - } - // Next in equivalence class - currentId = currentNode.getNext(); - } while (!d_done && currentId != classId); + TaggedEqualitiesSet disequalitiesToNotify; + Theory::Set tags = Theory::setInsert(tag); + getDisequalities(!d_isConstant[classId], classId, tags, disequalitiesToNotify); // Setup the data for the new set if (triggerSetRef != null_set_id) { @@ -1378,7 +1357,10 @@ void EqualityEngine::addTriggerTerm(TNode t, TheoryId tag) d_triggerTermSetUpdates.push_back(TriggerSetUpdate(classId, triggerSetRef)); d_triggerTermSetUpdatesSize = d_triggerTermSetUpdatesSize + 1; // Mark the the new set as a trigger - d_nodeIndividualTrigger[classId] = newTriggerTermSet(); + d_nodeIndividualTrigger[classId] = triggerSetRef = newTriggerTermSet(); + + // Propagate trigger term disequalities we remembered + propagateTriggerTermDisequalities(tags, triggerSetRef, disequalitiesToNotify); } } @@ -1497,6 +1479,117 @@ bool EqualityEngine::storePropagatedDisequality(TNode lhs, TNode rhs, unsigned r } } +void EqualityEngine::getDisequalities(bool allowConstants, EqualityNodeId classId, Theory::Set inputTags, TaggedEqualitiesSet& out) { + // Must be empty on input + Assert(out.size() == 0); + // The class we are looking for, shouldn't have any of the tags we are looking for already set + Assert(d_nodeIndividualTrigger[classId] == null_set_id || Theory::setIntersection(getTriggerTermSet(d_nodeIndividualTrigger[classId]).tags, inputTags) == 0); + + if (inputTags == 0) { + return; + } + + // Set of already (through disequalities) visited equivalence classes + std::set<EqualityNodeId> alreadyVisited; + + // Go through the equivalence class + EqualityNodeId currentId = classId; + do { + // Current node in the equivalence class + EqualityNode& currentNode = getEqualityNode(currentId); + + // Go through the uselist and look for disequalities + UseListNodeId currentUseId = currentNode.getUseList(); + while (currentUseId != null_uselist_id) { + UseListNode& useListNode = d_useListNodes[currentUseId]; + EqualityNodeId funId = useListNode.getApplicationId(); + const FunctionApplication& fun = d_applications[useListNode.getApplicationId()].original; + // If it's an equality asserted to false, we do the work + if (fun.isEquality && getEqualityNode(funId).getFind() == getEqualityNode(d_false).getFind()) { + // Get the other equality member + bool lhs = false; + EqualityNodeId toCompare = fun.b; + if (toCompare == currentId) { + toCompare = fun.a; + lhs = true; + } + // Representative of the other member + EqualityNodeId toCompareRep = getEqualityNode(toCompare).getFind(); + Assert(toCompareRep != classId, "Otherwise we are in conflict"); + // Check if we already have this one + if (alreadyVisited.count(toCompareRep) == 0) { + // Mark as visited + alreadyVisited.insert(toCompareRep); + // Get the trigger set + TriggerTermSetRef toCompareTriggerSetRef = d_nodeIndividualTrigger[toCompareRep]; + // We only care if we're not both constants and there are trigger terms in the other class + if ((allowConstants || !d_isConstant[toCompareRep]) && toCompareTriggerSetRef != null_set_id) { + // Tags of the other gey + TriggerTermSet& toCompareTriggerSet = getTriggerTermSet(toCompareTriggerSetRef); + // We only care if there are things in inputTags that is also in toCompareTags + Theory::Set commonTags = Theory::setIntersection(inputTags, toCompareTriggerSet.tags); + if (commonTags) { + out.push_back(TaggedEquality(funId, toCompareTriggerSetRef, lhs)); + } + } + } + } + // Go to the next one in the use list + currentUseId = useListNode.getNext(); + } + // Next in equivalence class + currentId = currentNode.getNext(); + } while (!d_done && currentId != classId); + +} + +bool EqualityEngine::propagateTriggerTermDisequalities(Theory::Set tags, TriggerTermSetRef triggerSetRef, const TaggedEqualitiesSet& disequalitiesToNotify) { + + // No tags, no food + if (!tags) { + return !d_done; + } + + Assert(triggerSetRef != null_set_id); + + // This is the class trigger set + const TriggerTermSet& triggerSet = getTriggerTermSet(triggerSetRef); + // Go throught the disequalities and notify + TaggedEqualitiesSet::const_iterator it = disequalitiesToNotify.begin(); + TaggedEqualitiesSet::const_iterator it_end = disequalitiesToNotify.end(); + for (; !d_done && it != it_end; ++ it) { + // The information about the equality that is asserted to false + const TaggedEquality& disequalityInfo = *it; + const TriggerTermSet& disequalityTriggerSet = getTriggerTermSet(disequalityInfo.triggerSetRef); + Theory::Set commonTags = Theory::setIntersection(disequalityTriggerSet.tags, tags); + Assert(commonTags); + // This is the actual function + const FunctionApplication& fun = d_applications[disequalityInfo.equalityId].original; + // Figure out who we are comparing to in the original equality + EqualityNodeId toCompare = disequalityInfo.lhs ? fun.a : fun.b; + EqualityNodeId myCompare = disequalityInfo.lhs ? fun.b : fun.a; + // Go through the tags, and add the disequalities + TheoryId currentTag; + while (!d_done && ((currentTag = Theory::setPop(commonTags)) != THEORY_LAST)) { + // Get the tag representative + EqualityNodeId tagRep = disequalityTriggerSet.getTrigger(currentTag); + EqualityNodeId myRep = triggerSet.getTrigger(currentTag); + // Store the propagation + d_deducedDisequalityReasons.push_back(EqualityPair(myCompare, myRep)); + d_deducedDisequalityReasons.push_back(EqualityPair(toCompare, tagRep)); + d_deducedDisequalityReasons.push_back(EqualityPair(disequalityInfo.equalityId, d_falseId)); + storePropagatedDisequality(d_nodes[myRep], d_nodes[tagRep], 3); + // We don't check if it's been propagated already, as we need one per tag + if (d_performNotify) { + if (!d_notify.eqNotifyTriggerTermEquality(currentTag, d_nodes[myRep], d_nodes[tagRep], false)) { + d_done = true; + } + } + } + } + + return !d_done; +} } // Namespace uf } // Namespace theory diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h index f40c79df3..5935ddc1f 100644 --- a/src/theory/uf/equality_engine.h +++ b/src/theory/uf/equality_engine.h @@ -520,8 +520,48 @@ private: */ std::vector<EqualityPair> d_deducedDisequalityReasons; - + /** + * Stores a propagated disequality for explanation purpooses and remembers the reasons. + */ bool storePropagatedDisequality(TNode lhs, TNode rhs, unsigned reasonsCount) const; + + /** + * An equality tagged with a set of tags. + */ + struct TaggedEquality { + /** Id of the equality */ + EqualityNodeId equalityId; + /** TriggerSet reference for the class of one of the sides */ + TriggerTermSetRef triggerSetRef; + /** Is trigger equivalent to the lhs (rhs otherwise) */ + bool lhs; + + TaggedEquality(EqualityNodeId equalityId = null_id, TriggerTermSetRef triggerSetRef = null_set_id, bool lhs = true) + : equalityId(equalityId), triggerSetRef(triggerSetRef), lhs(lhs) {} + }; + + /** A map from equivalence class id's to tagged equalities */ + typedef std::vector<TaggedEquality> TaggedEqualitiesSet; + + /** + * Returns a set of equalities that have been asserted false where one side of the equality + * belongs to the given equivalence class. The equalities are restricted to the ones where + * one side of the equality is in the tags set, but the other one isn't. Each returned + * dis-equality is associated with the tags that are the subset of the input tags, such that + * exactly one side of the equality is not in the set yet. + * + * @param classId the equivalence class to search + * @param inputTags the tags to filter the equalities + * @param out the output equalities, as described above + */ + void getDisequalities(bool allowConstants, EqualityNodeId classId, Theory::Set inputTags, TaggedEqualitiesSet& out); + + /** + * Propagates the remembered disequalities with given tags the original triggers for those tags, + * and the set of disequalities produced by above. + */ + bool propagateTriggerTermDisequalities(Theory::Set tags, + TriggerTermSetRef triggerSetRef, const TaggedEqualitiesSet& disequalitiesToNotify); public: |