diff options
Diffstat (limited to 'src/theory/uf/equality_engine.cpp')
| -rw-r--r-- | src/theory/uf/equality_engine.cpp | 210 |
1 files changed, 165 insertions, 45 deletions
diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp index 0ac5096d2..9b429765e 100644 --- a/src/theory/uf/equality_engine.cpp +++ b/src/theory/uf/equality_engine.cpp @@ -1,13 +1,13 @@ /********************* */ /*! \file equality_engine.cpp ** \verbatim - ** Original author: Dejan Jovanovic - ** Major contributors: none - ** Minor contributors (to current version): Dejan Jovanovic, Tianyi Liang, Tim King, Francois Bobot, Morgan Deters, Andrew Reynolds + ** Top contributors (to current version): + ** Dejan Jovanovic, Guy Katz, Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief [[ Add one-line brief description here ]] ** @@ -42,7 +42,6 @@ EqualityEngine::Statistics::~Statistics() { smtStatisticsRegistry()->unregisterStat(&constantTermsCount); } - /** * Data used in the BFS search through the equality graph. */ @@ -94,6 +93,8 @@ void EqualityEngine::init() { d_trueId = getNodeId(d_true); d_falseId = getNodeId(d_false); + + d_freshMergeReasonType = eq::NUMBER_OF_MERGE_REASONS; } EqualityEngine::~EqualityEngine() throw(AssertionException) { @@ -157,7 +158,7 @@ void EqualityEngine::setMasterEqualityEngine(EqualityEngine* master) { } void EqualityEngine::enqueue(const MergeCandidate& candidate, bool back) { - Debug("equality") << d_name << "::eq::enqueue(" << d_nodes[candidate.t1Id] << ", " << d_nodes[candidate.t2Id] << ", " << candidate.type << ")" << std::endl; + Debug("equality") << d_name << "::eq::enqueue(" << d_nodes[candidate.t1Id] << ", " << d_nodes[candidate.t2Id] << ", " << candidate.type << "). reason: " << candidate.reason << std::endl; if (back) { d_propagationQueue.push_back(candidate); } else { @@ -390,7 +391,7 @@ const EqualityNode& EqualityEngine::getEqualityNode(EqualityNodeId nodeId) const return d_equalityNodes[nodeId]; } -void EqualityEngine::assertEqualityInternal(TNode t1, TNode t2, TNode reason, MergeReasonType pid) { +void EqualityEngine::assertEqualityInternal(TNode t1, TNode t2, TNode reason, unsigned pid) { Debug("equality") << d_name << "::eq::addEqualityInternal(" << t1 << "," << t2 << "), pid = " << pid << std::endl; @@ -408,7 +409,7 @@ void EqualityEngine::assertEqualityInternal(TNode t1, TNode t2, TNode reason, Me enqueue(MergeCandidate(t1Id, t2Id, pid, reason)); } -void EqualityEngine::assertPredicate(TNode t, bool polarity, TNode reason, MergeReasonType pid) { +void EqualityEngine::assertPredicate(TNode t, bool polarity, TNode reason, unsigned pid) { Debug("equality") << d_name << "::eq::addPredicate(" << t << "," << (polarity ? "true" : "false") << ")" << std::endl; Assert(t.getKind() != kind::EQUAL, "Use assertEquality instead"); assertEqualityInternal(t, polarity ? d_true : d_false, reason, pid); @@ -421,7 +422,7 @@ void EqualityEngine::mergePredicates(TNode p, TNode q, TNode reason) { propagate(); } -void EqualityEngine::assertEquality(TNode eq, bool polarity, TNode reason, MergeReasonType pid) { +void EqualityEngine::assertEquality(TNode eq, bool polarity, TNode reason, unsigned pid) { Debug("equality") << d_name << "::eq::addEquality(" << eq << "," << (polarity ? "true" : "false") << ")" << std::endl; if (polarity) { // If two terms are already equal, don't assert anything @@ -889,7 +890,7 @@ void EqualityEngine::backtrack() { } -void EqualityEngine::addGraphEdge(EqualityNodeId t1, EqualityNodeId t2, MergeReasonType type, TNode reason) { +void EqualityEngine::addGraphEdge(EqualityNodeId t1, EqualityNodeId t2, unsigned type, TNode reason) { Debug("equality") << d_name << "::eq::addGraphEdge(" << d_nodes[t1] << "," << d_nodes[t2] << "," << reason << ")" << std::endl; EqualityEdgeId edge = d_equalityEdges.size(); d_equalityEdges.push_back(EqualityEdge(t2, d_equalityGraph[t1], type, reason)); @@ -920,7 +921,7 @@ std::string EqualityEngine::edgesToString(EqualityEdgeId edgeId) const { } void EqualityEngine::explainEquality(TNode t1, TNode t2, bool polarity, std::vector<TNode>& equalities, EqProof * eqp) const { - Debug("equality") << d_name << "::eq::explainEquality(" << t1 << ", " << t2 << ", " << (polarity ? "true" : "false") << ")" << std::endl; + Debug("equality") << d_name << "::eq::explainEquality(" << t1 << ", " << t2 << ", " << (polarity ? "true" : "false") << ")" << ", proof = " << (eqp ? "ON" : "OFF") << std::endl; // The terms must be there already Assert(hasTerm(t1) && hasTerm(t2));; @@ -933,13 +934,72 @@ void EqualityEngine::explainEquality(TNode t1, TNode t2, bool polarity, std::vec // Get the explanation getExplanation(t1Id, t2Id, equalities, eqp); } else { + if (eqp) { + eqp->d_id = eq::MERGED_THROUGH_TRANS; + eqp->d_node = d_nodes[t1Id].eqNode(d_nodes[t2Id]).notNode(); + } + // Get the reason for this disequality EqualityPair pair(t1Id, t2Id); Assert(d_disequalityReasonsMap.find(pair) != d_disequalityReasonsMap.end(), "Don't ask for stuff I didn't notify you about"); DisequalityReasonRef reasonRef = d_disequalityReasonsMap.find(pair)->second; + for (unsigned i = reasonRef.mergesStart; i < reasonRef.mergesEnd; ++ i) { + EqualityPair toExplain = d_deducedDisequalityReasons[i]; - getExplanation(toExplain.first, toExplain.second, equalities, eqp); + EqProof* eqpc = NULL; + + // If we're constructing a (transitivity) proof, we don't need to include an explanation for x=x. + if (eqp && toExplain.first != toExplain.second) { + eqpc = new EqProof; + } + + getExplanation(toExplain.first, toExplain.second, equalities, eqpc); + + if (eqpc) { + Debug("pf::ee") << "Child proof is:" << std::endl; + eqpc->debug_print("pf::ee", 1); + + if (eqpc->d_id == eq::MERGED_THROUGH_TRANS) { + std::vector<EqProof *> orderedChildren; + bool nullCongruenceFound = false; + for (unsigned i = 0; i < eqpc->d_children.size(); ++i) { + if (eqpc->d_children[i]->d_id==eq::MERGED_THROUGH_CONGRUENCE && eqpc->d_children[i]->d_node.isNull()) { + + // For now, assume there can only be one null congruence child + Assert(!nullCongruenceFound); + nullCongruenceFound = true; + + Debug("pf::ee") << "Have congruence with empty d_node. Splitting..." << std::endl; + orderedChildren.insert(orderedChildren.begin(), eqpc->d_children[i]->d_children[0]); + orderedChildren.push_back(eqpc->d_children[i]->d_children[1]); + } else { + orderedChildren.push_back(eqpc->d_children[i]); + } + } + + if (nullCongruenceFound) { + eqpc->d_children = orderedChildren; + Debug("pf::ee") << "Child proof's children have been reordered. It is now:" << std::endl; + eqpc->debug_print("pf::ee", 1); + } + } + + eqp->d_children.push_back(eqpc); + } + } + + if (eqp) { + if(eqp->d_children.size() == 1) { + // The transitivity proof has just one child. Simplify. + EqProof* temp = eqp->d_children[0]; + eqp->d_children.clear(); + *eqp = *temp; + delete temp; + } + + Debug("pf::ee") << "Disequality explanation final proof: " << std::endl; + eqp->debug_print("pf::ee", 1); } } } @@ -972,7 +1032,12 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st // If the nodes are the same, we're done if (t1Id == t2Id){ if( eqp ) { - eqp->d_node = ProofManager::currentPM()->mkOp(d_nodes[t1Id]); + if ((d_nodes[t1Id].getKind() == kind::BUILTIN) && (d_nodes[t1Id].getConst<Kind>() == kind::SELECT)) { + std::vector<Node> no_children; + eqp->d_node = NodeManager::currentNM()->mkNode(kind::PARTIAL_SELECT_0, no_children); + } else { + eqp->d_node = ProofManager::currentPM()->mkOp(d_nodes[t1Id]); + } } return; } @@ -1019,24 +1084,28 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st Debug("equality") << d_name << "::eq::getExplanation(): path found: " << std::endl; - std::vector< EqProof * > eqp_trans; + std::vector<EqProof *> eqp_trans; // Reconstruct the path do { // The current node currentNode = bfsQueue[currentIndex].nodeId; EqualityNodeId edgeNode = d_equalityEdges[currentEdge].getNodeId(); - MergeReasonType reasonType = d_equalityEdges[currentEdge].getReasonType(); + unsigned reasonType = d_equalityEdges[currentEdge].getReasonType(); + Node reason = d_equalityEdges[currentEdge].getReason(); Debug("equality") << d_name << "::eq::getExplanation(): currentEdge = " << currentEdge << ", currentNode = " << currentNode << std::endl; + Debug("equality") << d_name << " targetNode = " << d_nodes[edgeNode] << std::endl; Debug("equality") << d_name << " in currentEdge = (" << d_nodes[currentNode] << "," << d_nodes[edge.getNodeId()] << ")" << std::endl; + Debug("equality") << d_name << " reason type = " << reasonType << std::endl; - EqProof * eqpc = NULL; - //make child proof if a proof is being constructed - if( eqp ){ + EqProof* eqpc = NULL; + // Make child proof if a proof is being constructed + if (eqp) { eqpc = new EqProof; eqpc->d_id = reasonType; } + // Add the actual equality to the vector switch (reasonType) { case MERGED_THROUGH_CONGRUENCE: { @@ -1044,32 +1113,47 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st Debug("equality") << d_name << "::eq::getExplanation(): due to congruence, going deeper" << std::endl; const FunctionApplication& f1 = d_applications[currentNode].original; const FunctionApplication& f2 = d_applications[edgeNode].original; + Debug("equality") << push; + Debug("equality") << "Explaining left hand side equalities" << std::endl; EqProof * eqpc1 = eqpc ? new EqProof : NULL; getExplanation(f1.a, f2.a, equalities, eqpc1); + Debug("equality") << "Explaining right hand side equalities" << std::endl; EqProof * eqpc2 = eqpc ? new EqProof : NULL; getExplanation(f1.b, f2.b, equalities, eqpc2); if( eqpc ){ eqpc->d_children.push_back( eqpc1 ); eqpc->d_children.push_back( eqpc2 ); - Debug("equality-pf") << "Congruence : " << d_nodes[currentNode] << " " << d_nodes[edgeNode] << std::endl; if( d_nodes[currentNode].getKind()==kind::EQUAL ){ //leave node null for now eqpc->d_node = Node::null(); - }else{ - Debug("equality-pf") << d_nodes[f1.a] << " / " << d_nodes[f2.a] << ", " << d_nodes[f1.b] << " / " << d_nodes[f2.b] << std::endl; + } else { if(d_nodes[f1.a].getKind() == kind::APPLY_UF || d_nodes[f1.a].getKind() == kind::SELECT || d_nodes[f1.a].getKind() == kind::STORE) { eqpc->d_node = d_nodes[f1.a]; } else { - eqpc->d_node = NodeManager::currentNM()->mkNode(kind::PARTIAL_APPLY_UF, ProofManager::currentPM()->mkOp(d_nodes[f1.a]), d_nodes[f1.b]); + if (d_nodes[f1.a].getKind() == kind::BUILTIN && d_nodes[f1.a].getConst<Kind>() == kind::SELECT) { + eqpc->d_node = NodeManager::currentNM()->mkNode(kind::PARTIAL_SELECT_1, d_nodes[f1.b]); + // The first child is a PARTIAL_SELECT_0. + // Give it a child so that we know what kind of (read) it is, when we dump to LFSC. + Assert(eqpc->d_children[0]->d_node.getKind() == kind::PARTIAL_SELECT_0); + Assert(eqpc->d_children[0]->d_children.size() == 0); + + eqpc->d_children[0]->d_node = NodeManager::currentNM()->mkNode(kind::PARTIAL_SELECT_0, + d_nodes[f1.b]); + } else { + eqpc->d_node = NodeManager::currentNM()->mkNode(kind::PARTIAL_APPLY_UF, + ProofManager::currentPM()->mkOp(d_nodes[f1.a]), + d_nodes[f1.b]); + } } } } Debug("equality") << pop; break; } + case MERGED_THROUGH_REFLEXIVITY: { // x1 == x1 Debug("equality") << d_name << "::eq::getExplanation(): due to reflexivity, going deeper" << std::endl; @@ -1088,6 +1172,7 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st break; } + case MERGED_THROUGH_CONSTANTS: { // f(c1, ..., cn) = c semantically, we can just ignore it Debug("equality") << d_name << "::eq::getExplanation(): due to constants, explain the constants" << std::endl; @@ -1111,23 +1196,41 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st } Debug("equality") << pop; - break; } + default: { // Construct the equality - Debug("equality") << d_name << "::eq::getExplanation(): adding: " << d_equalityEdges[currentEdge].getReason() << std::endl; - if( eqpc ){ - if(reasonType == MERGED_THROUGH_EQUALITY) { - eqpc->d_node = d_equalityEdges[currentEdge].getReason(); + Debug("equality") << d_name << "::eq::getExplanation(): adding: " + << reason << std::endl; + Debug("equality") << d_name << "::eq::getExplanation(): reason type = " << reasonType << std::endl; + + Node a = d_nodes[currentNode]; + Node b = d_nodes[d_equalityEdges[currentEdge].getNodeId()]; + + if (eqpc) { + //apply proof reconstruction processing (when eqpc is non-null) + if (d_pathReconstructionTriggers.find(reasonType) != d_pathReconstructionTriggers.end()) { + d_pathReconstructionTriggers.find(reasonType)->second->notify(reasonType, reason, a, b, + equalities, eqpc); + } + if (reasonType == MERGED_THROUGH_EQUALITY) { + eqpc->d_node = reason; } else { - // theory-specific proof rule - eqpc->d_node = d_nodes[d_equalityEdges[currentEdge].getNodeId()].eqNode(d_nodes[currentNode]); - Debug("equality-pf") << "theory eq : " << eqpc->d_node << std::endl; + // The LFSC translator prefers (not (= a b)) over (= (= a b) false) + + if (a == NodeManager::currentNM()->mkConst(false)) { + eqpc->d_node = b.notNode(); + } else if (b == NodeManager::currentNM()->mkConst(false)) { + eqpc->d_node = a.notNode(); + } else { + eqpc->d_node = b.eqNode(a); + } } eqpc->d_id = reasonType; } - equalities.push_back(d_equalityEdges[currentEdge].getReason()); + + equalities.push_back(reason); break; } } @@ -1137,7 +1240,7 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st currentIndex = bfsQueue[currentIndex].previousIndex; //---from Morgan--- - if(eqpc != NULL && eqpc->d_id == MERGED_THROUGH_REFLEXIVITY) { + if (eqpc != NULL && eqpc->d_id == MERGED_THROUGH_REFLEXIVITY) { if(eqpc->d_node.isNull()) { Assert(eqpc->d_children.size() == 1); EqProof *p = eqpc; @@ -1149,11 +1252,10 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st } //---end from Morgan--- - eqp_trans.push_back( eqpc ); - + eqp_trans.push_back(eqpc); } while (currentEdge != null_id); - if(eqp) { + if (eqp) { if(eqp_trans.size() == 1) { *eqp = *eqp_trans[0]; delete eqp_trans[0]; @@ -1162,6 +1264,8 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st eqp->d_children.insert( eqp->d_children.end(), eqp_trans.begin(), eqp_trans.end() ); eqp->d_node = NodeManager::currentNM()->mkNode(d_nodes[t1Id].getType().isBoolean() ? kind::IFF : kind::EQUAL, d_nodes[t1Id], d_nodes[t2Id]); } + + eqp->debug_print("pf::ee", 1); } // Done @@ -1508,7 +1612,7 @@ void EqualityEngine::debugPrintGraph() const { EqualityEdgeId edgeId = d_equalityGraph[nodeId]; while (edgeId != null_edge) { const EqualityEdge& edge = d_equalityEdges[edgeId]; - Debug("equality::graph") << " " << d_nodes[edge.getNodeId()] << ":" << edge.getReason(); + Debug("equality::graph") << " [" << edge.getNodeId() << "] " << d_nodes[edge.getNodeId()] << ":" << edge.getReason(); edgeId = edge.getNext(); } @@ -1517,17 +1621,19 @@ void EqualityEngine::debugPrintGraph() const { } bool EqualityEngine::areEqual(TNode t1, TNode t2) const { - Debug("equality") << d_name << "::eq::areEqual(" << t1 << "," << t2 << ")" << std::endl; + Debug("equality") << d_name << "::eq::areEqual(" << t1 << "," << t2 << ")"; Assert(hasTerm(t1)); Assert(hasTerm(t2)); - return getEqualityNode(t1).getFind() == getEqualityNode(t2).getFind(); + bool result = getEqualityNode(t1).getFind() == getEqualityNode(t2).getFind(); + Debug("equality") << (result ? "\t(YES)" : "\t(NO)") << std::endl; + return result; } bool EqualityEngine::areDisequal(TNode t1, TNode t2, bool ensureProof) const { - Debug("equality") << d_name << "::eq::areDisequal(" << t1 << "," << t2 << ")" << std::endl; + Debug("equality") << d_name << "::eq::areDisequal(" << t1 << "," << t2 << ")"; // Add the terms Assert(hasTerm(t1)); @@ -1539,6 +1645,7 @@ bool EqualityEngine::areDisequal(TNode t1, TNode t2, bool ensureProof) const // If we propagated this disequality we're true if (hasPropagatedDisequality(t1Id, t2Id)) { + Debug("equality") << "\t(YES)" << std::endl; return true; } @@ -1556,6 +1663,7 @@ bool EqualityEngine::areDisequal(TNode t1, TNode t2, bool ensureProof) const nonConst->d_deducedDisequalityReasons.push_back(EqualityPair(t2Id, t2ClassId)); nonConst->storePropagatedDisequality(THEORY_LAST, t1Id, t2Id); } + Debug("equality") << "\t(YES)" << std::endl; return true; } @@ -1571,6 +1679,7 @@ bool EqualityEngine::areDisequal(TNode t1, TNode t2, bool ensureProof) const nonConst->d_deducedDisequalityReasons.push_back(EqualityPair(t2Id, original.b)); nonConst->storePropagatedDisequality(THEORY_LAST, t1Id, t2Id); } + Debug("equality") << "\t(YES)" << std::endl; return true; } } @@ -1587,21 +1696,33 @@ bool EqualityEngine::areDisequal(TNode t1, TNode t2, bool ensureProof) const nonConst->d_deducedDisequalityReasons.push_back(EqualityPair(t1Id, original.b)); nonConst->storePropagatedDisequality(THEORY_LAST, t1Id, t2Id); } + Debug("equality") << "\t(YES)" << std::endl; return true; } } // Couldn't deduce dis-equalityReturn whether the terms are disequal + Debug("equality") << "\t(NO)" << std::endl; return false; } -size_t EqualityEngine::getSize(TNode t) -{ +size_t EqualityEngine::getSize(TNode t) { // Add the term addTermInternal(t); return getEqualityNode(getEqualityNode(t).getFind()).getSize(); } + +void EqualityEngine::addPathReconstructionTrigger(unsigned trigger, const PathReconstructionNotify* notify) { + // Currently we can only inform one callback per trigger + Assert(d_pathReconstructionTriggers.find(trigger) == d_pathReconstructionTriggers.end()); + d_pathReconstructionTriggers[trigger] = notify; +} + +unsigned EqualityEngine::getFreshMergeReasonType() { + return d_freshMergeReasonType++; +} + void EqualityEngine::addTriggerTerm(TNode t, TheoryId tag) { Debug("equality::trigger") << d_name << "::eq::addTriggerTerm(" << t << ", " << tag << ")" << std::endl; @@ -2103,10 +2224,9 @@ void EqProof::debug_print( const char * c, unsigned tb ) const{ d_children[i]->debug_print( c, tb+1 ); } } - Debug( c ) << ")"; + Debug( c ) << ")" << std::endl; } - } // Namespace uf } // Namespace theory } // Namespace CVC4 |