diff options
author | Guy <katz911@gmail.com> | 2016-03-23 12:07:59 -0700 |
---|---|---|
committer | Guy <katz911@gmail.com> | 2016-03-23 12:07:59 -0700 |
commit | aa9aa46b77f048f2865c29e40ed946371fd115ef (patch) | |
tree | 254f392449a03901f7acb7a65e9499193d07ac9a /src/theory/uf/equality_engine.cpp | |
parent | 786cd2dd5b1c53f650c891d6dfbf299a62840848 (diff) |
squash-merge from proof branch
Diffstat (limited to 'src/theory/uf/equality_engine.cpp')
-rw-r--r-- | src/theory/uf/equality_engine.cpp | 316 |
1 files changed, 290 insertions, 26 deletions
diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp index 0ac5096d2..53347c365 100644 --- a/src/theory/uf/equality_engine.cpp +++ b/src/theory/uf/equality_engine.cpp @@ -42,7 +42,6 @@ EqualityEngine::Statistics::~Statistics() { smtStatisticsRegistry()->unregisterStat(&constantTermsCount); } - /** * Data used in the BFS search through the equality graph. */ @@ -157,7 +156,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 { @@ -920,7 +919,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 +932,83 @@ 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); + } + + for (unsigned i = reasonRef.mergesStart; i < reasonRef.mergesEnd; ++ i) { + + EqualityPair toExplain = d_deducedDisequalityReasons[i]; + 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; + } + + // Some edges have the form ((a == b) == false). Translate this into (not (a == b)). + // Assert(d_nodes[toExplain.first] != NodeManager::currentNM()->mkConst(false)); + + getExplanation(toExplain.first, toExplain.second, equalities, eqpc); + + // if (eqpc) { + // eqp->d_children.push_back(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 +1041,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,7 +1093,7 @@ 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 { @@ -1029,11 +1103,13 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st MergeReasonType reasonType = d_equalityEdges[currentEdge].getReasonType(); 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; } @@ -1044,26 +1120,60 @@ 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("pf::ee") << "We need to prove two equalities:" << std::endl; + Debug("pf::ee") << "\tLHS: " << d_nodes[f1.a] << " = " << d_nodes[f2.a] << std::endl; + Debug("pf::ee") << "\tRHS: " << d_nodes[f1.b] << " = " << d_nodes[f2.b] << std::endl; + 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; + Debug("pf::ee") << "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; + Debug("pf::ee") << d_nodes[f1.a] << " / " << d_nodes[f2.a] << ", " << d_nodes[f1.b] << " / " << d_nodes[f2.b] << std::endl; 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]); + + Debug("pf::ee") << "f1.a is: " << d_nodes[f1.a] + << ". kind is: " << d_nodes[f1.a].getKind() << std::endl; + + if (d_nodes[f1.a].getKind() == kind::BUILTIN && d_nodes[f1.a].getConst<Kind>() == kind::SELECT) { + Debug("pf::ee") << "f1.a getConst<kind> is: " << d_nodes[f1.a].getConst<Kind>() << std::endl; + + 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. + Debug("pf::ee") << "eqpc->d_children[0]->d_node.getKind() == " << eqpc->d_children[0]->d_node.getKind() << std::endl; + Assert(eqpc->d_children[0]->d_node.getKind() == kind::PARTIAL_SELECT_0); + Assert(eqpc->d_children[0]->d_children.size() == 0); + + Debug("pf::ee") << "Dumping the equality proof before:" << std::endl; + eqpc->debug_print("pf::ee", 1); + + eqpc->d_children[0]->d_node = NodeManager::currentNM()->mkNode(kind::PARTIAL_SELECT_0, d_nodes[f1.b]); + + Debug("pf::ee") << "Dumping the equality proof after:" << std::endl; + eqpc->debug_print("pf::ee", 1); + + //eqpc->d_children[0]->d_node.append(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("pf::ee") << "New d_node is: " << eqpc->d_node << std::endl; } } } @@ -1114,16 +1224,162 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st break; } + case MERGED_ARRAYS_EXT: + + Debug("equality") << d_name << "::eq::getExplanation(): MERGED_ARRAYS_EXT" << std::endl; + + if (eqpc) { + Node a = d_nodes[d_equalityEdges[currentEdge].getNodeId()]; + Node b = d_nodes[currentNode]; + + // GK: todo: here we assume that a=b is an assertion. We should probably call explain() + // recursively, to explain this. + + 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 = a.eqNode(b); + } + + EqProof* eqpc1 = new EqProof; + eqpc1->d_node = d_equalityEdges[currentEdge].getReason(); + eqpc->d_children.push_back( eqpc1 ); + + eqpc1->debug_print("pf::ee", 1); + eqpc->debug_print("pf::ee", 1); + } + + // We push the reason into "equalities" because that's what the theory of arrays expects. + equalities.push_back(d_equalityEdges[currentEdge].getReason()); + break; + + case MERGED_ARRAYS_ROW: { + Debug("equality") << d_name << "::eq::getExplanation(): MERGED_ARRAYS_ROW" << std::endl; + + // ROW rules mean that (i==k) OR ((a[i]:=t)[k] == a[k]) + // The equality here will be either (i == k) because ((a[i]:=t)[k] != a[k]), + // or ((a[i]:=t)[k] == a[k]) because (i != k). + + if (eqpc) { + if (d_nodes[currentNode].getNumChildren() == 2) { + // This is the case of ((a[i]:=t)[k] == a[k]) because (i != k). + + // The edge is ((a[i]:=t)[k], a[k]), or (a[k], (a[i]:=t)[k]). This flag should be + // false in the first case and true in the second case. + bool currentNodeIsUnchangedArray; + + Assert(d_nodes[currentNode].getNumChildren() == 2); + Assert(d_nodes[edgeNode].getNumChildren() == 2); + + if (d_nodes[currentNode][0].getKind() == kind::VARIABLE || + d_nodes[currentNode][0].getKind() == kind::SKOLEM) { + currentNodeIsUnchangedArray = true; + } else if (d_nodes[edgeNode][0].getKind() == kind::VARIABLE || + d_nodes[edgeNode][0].getKind() == kind::SKOLEM) { + currentNodeIsUnchangedArray = false; + } else { + Assert(d_nodes[currentNode][0].getKind() == kind::STORE); + Assert(d_nodes[edgeNode][0].getKind() == kind::STORE); + + if (d_nodes[currentNode][0][0] == d_nodes[edgeNode][0]) { + currentNodeIsUnchangedArray = false; + } else if (d_nodes[edgeNode][0][0] == d_nodes[currentNode][0]) { + currentNodeIsUnchangedArray = true; + } else { + Unreachable(); + } + } + + Node indexOne = + currentNodeIsUnchangedArray ? d_nodes[currentNode][1] : d_nodes[currentNode][0][1]; + Node indexTwo = + currentNodeIsUnchangedArray ? d_nodes[edgeNode][0][1] : d_nodes[edgeNode][1]; + + // Some assertions to ensure that the theory of arrays behaves as expected + Assert(d_nodes[currentNode][1] == d_nodes[edgeNode][1]); + if (currentNodeIsUnchangedArray) { + Assert(d_nodes[currentNode][0] == d_nodes[edgeNode][0][0]); + } else { + Assert(d_nodes[currentNode][0][0] == d_nodes[edgeNode][0]); + } + + Debug("pf::ee") << "Getting explanation for ROW guard: " + << indexOne << " != " << indexTwo << std::endl; + + EqProof* eqpcc = eqpc ? new EqProof : NULL; + explainEquality(indexOne, indexTwo, false, equalities, eqpcc); + + Debug("pf::ee") << "The two indices are: " << indexOne << ", " << indexTwo << std::endl; + Debug("pf::ee") << "And the explanation of their disequality is: " << std::endl; + eqpcc->debug_print("pf::ee", 1); + eqpc->d_children.push_back(eqpcc); + } else { + // This is the case of (i == k) because ((a[i]:=t)[k] != a[k]), + + Debug("pf::ee") << "In the new case of ROW!" << std::endl; + + Node indexOne = d_nodes[currentNode]; + Node indexTwo = d_nodes[edgeNode]; + + Debug("pf::ee") << "The two indices are: " << indexOne << ", " << indexTwo << std::endl; + Debug("pf::ee") << "The reason for the edge is: " << d_equalityEdges[currentEdge].getReason() + << std::endl; + + Assert(d_equalityEdges[currentEdge].getReason().getNumChildren() == 2); + Node reason = d_equalityEdges[currentEdge].getReason()[1]; + Debug("pf::ee") << "Getting explanation for ROW guard: " << reason << std::endl; + + EqProof* eqpcc = eqpc ? new EqProof : NULL; + explainEquality(reason[0], reason[1], false, equalities, eqpcc); + + if (eqpc) { + Debug("pf::ee") << "The guard's explanation is: " << std::endl; + eqpcc->debug_print("pf::ee", 1); + eqpc->d_children.push_back(eqpcc); + } + } + + Node a = d_nodes[d_equalityEdges[currentEdge].getNodeId()]; + Node b = d_nodes[currentNode]; + + 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 = a.eqNode(b); + } + } + + // We push the reason into "equalities" because that's what the theory of arrays expects. + equalities.push_back(d_equalityEdges[currentEdge].getReason()); + 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) { + Debug("equality") << d_name << "::eq::getExplanation(): reason type = " << reasonType << std::endl; + + if (eqpc) { + if (reasonType == MERGED_THROUGH_EQUALITY) { eqpc->d_node = d_equalityEdges[currentEdge].getReason(); } 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) + + Node a = d_nodes[d_equalityEdges[currentEdge].getNodeId()]; + Node b = d_nodes[currentNode]; + + 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 = a.eqNode(b); + } + Debug("pf::ee") << "theory eq : " << eqpc->d_node << std::endl; } eqpc->d_id = reasonType; } @@ -1137,7 +1393,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 +1405,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 +1417,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 +1765,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 +1774,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 +1798,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 +1816,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 +1832,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,11 +1849,13 @@ 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; } @@ -2103,7 +2367,7 @@ void EqProof::debug_print( const char * c, unsigned tb ) const{ d_children[i]->debug_print( c, tb+1 ); } } - Debug( c ) << ")"; + Debug( c ) << ")" << std::endl; } |