diff options
Diffstat (limited to 'src/theory/uf/equality_engine.cpp')
-rw-r--r-- | src/theory/uf/equality_engine.cpp | 78 |
1 files changed, 56 insertions, 22 deletions
diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp index 828d53144..8df323992 100644 --- a/src/theory/uf/equality_engine.cpp +++ b/src/theory/uf/equality_engine.cpp @@ -314,10 +314,10 @@ void EqualityEngine::addTermInternal(TNode t, bool isOperator) { // How many children are not constants yet d_subtermsToEvaluate[result] = t.getNumChildren(); for (unsigned i = 0; i < t.getNumChildren(); ++ i) { - if (isConstant(getNodeId(t[i]))) { - Debug("equality::evaluation") << d_name << "::eq::addTermInternal(" << t << "): evaluates " << t[i] << std::endl; - subtermEvaluates(result); - } + if (isConstant(getNodeId(t[i]))) { + Debug("equality::evaluation") << d_name << "::eq::addTermInternal(" << t << "): evaluates " << t[i] << std::endl; + subtermEvaluates(result); + } } } } else { @@ -335,7 +335,7 @@ void EqualityEngine::addTermInternal(TNode t, bool isOperator) { } else if (d_constantsAreTriggers && d_isConstant[result]) { // Non-Boolean constants are trigger terms for all tags EqualityNodeId tId = getNodeId(t); - // Setup the new set + // Setup the new set Theory::Set newSetTags = 0; EqualityNodeId newSetTriggers[THEORY_LAST]; unsigned newSetTriggersSize = THEORY_LAST; @@ -629,12 +629,12 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect Debug("equality") << d_name << "::eq::merge(" << class1.getFind() << "," << class2.getFind() << "): " << d_nodes[currentId] << " in " << d_nodes[funId] << std::endl; const FunctionApplication& fun = d_applications[useNode.getApplicationId()].normalized; // If it's interpreted and we can interpret - if (fun.isInterpreted() && class1isConstant && !d_isInternal[currentId]) { - // Get the actual term id - TNode term = d_nodes[funId]; - subtermEvaluates(getNodeId(term)); - } - // Check if there is an application with find arguments + if (fun.isInterpreted() && class1isConstant && !d_isInternal[currentId]) { + // Get the actual term id + TNode term = d_nodes[funId]; + subtermEvaluates(getNodeId(term)); + } + // Check if there is an application with find arguments EqualityNodeId aNormalized = getEqualityNode(fun.a).getFind(); EqualityNodeId bNormalized = getEqualityNode(fun.b).getFind(); FunctionApplication funNormalized(fun.type, aNormalized, bNormalized); @@ -972,7 +972,7 @@ 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 = d_nodes[t1Id]; + eqp->d_node = ProofManager::currentPM()->mkOp(d_nodes[t1Id]); } return; } @@ -1029,6 +1029,7 @@ 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 << " in currentEdge = (" << d_nodes[currentNode] << "," << d_nodes[edge.getNodeId()] << ")" << std::endl; EqProof * eqpc = NULL; //make child proof if a proof is being constructed @@ -1051,6 +1052,20 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st 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; + 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("equality") << pop; break; @@ -1103,13 +1118,14 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st // Construct the equality Debug("equality") << d_name << "::eq::getExplanation(): adding: " << d_equalityEdges[currentEdge].getReason() << std::endl; if( eqpc ){ - if( reasonType==MERGED_THROUGH_EQUALITY ){ + if(reasonType == MERGED_THROUGH_EQUALITY) { eqpc->d_node = d_equalityEdges[currentEdge].getReason(); - }else{ - //theory-specific proof rule : TODO - eqpc->d_id = reasonType; - //eqpc->d_node = d_equalityEdges[currentEdge].getNodeId(); + } 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; } + eqpc->d_id = reasonType; } equalities.push_back(d_equalityEdges[currentEdge].getReason()); break; @@ -1120,13 +1136,32 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st currentEdge = bfsQueue[currentIndex].edgeId; currentIndex = bfsQueue[currentIndex].previousIndex; + //---from Morgan--- + if(eqpc != NULL && eqpc->d_id == MERGED_THROUGH_REFLEXIVITY) { + if(eqpc->d_node.isNull()) { + Assert(eqpc->d_children.size() == 1); + EqProof *p = eqpc; + eqpc = p->d_children[0]; + delete p; + } else { + Assert(eqpc->d_children.empty()); + } + } + //---end from Morgan--- + eqp_trans.push_back( eqpc ); } while (currentEdge != null_id); - if( eqp ){ - eqp->d_id = MERGED_THROUGH_TRANS; - eqp->d_children.insert( eqp->d_children.end(), eqp_trans.begin(), eqp_trans.end() ); + if(eqp) { + if(eqp_trans.size() == 1) { + *eqp = *eqp_trans[0]; + delete eqp_trans[0]; + } else { + eqp->d_id = MERGED_THROUGH_TRANS; + 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]); + } } // Done @@ -2057,8 +2092,7 @@ bool EqClassIterator::isFinished() const { return d_current == null_id; } - -void EqProof::debug_print( const char * c, unsigned tb ){ +void EqProof::debug_print( const char * c, unsigned tb ) const{ for( unsigned i=0; i<tb; i++ ) { Debug( c ) << " "; } Debug( c ) << d_id << "("; if( !d_children.empty() || !d_node.isNull() ){ |