From 2ad315a59ad2bd7f69ba7a975874aab12f0fa605 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 14 Mar 2014 11:50:28 -0500 Subject: [PATCH] Add ability to provide theory-specific proof rules to EqualityEngine, extends enumeration of MergeReasonType. Add initial use in TheoryArrays. --- src/theory/arrays/theory_arrays.cpp | 18 +++++++---- src/theory/uf/equality_engine.cpp | 45 +++++++++++++++------------ src/theory/uf/equality_engine.h | 6 ++-- src/theory/uf/equality_engine_types.h | 7 ++++- 4 files changed, 46 insertions(+), 30 deletions(-) diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index b82216378..cd9fd2497 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -374,11 +374,17 @@ void TheoryArrays::explain(TNode literal, std::vector& assumptions) { // Do the work bool polarity = literal.getKind() != kind::NOT; TNode atom = polarity ? literal : literal[0]; + //eq::EqProof * eqp = new eq::EqProof; + eq::EqProof * eqp = NULL; if (atom.getKind() == kind::EQUAL || atom.getKind() == kind::IFF) { - d_equalityEngine.explainEquality(atom[0], atom[1], polarity, assumptions); + d_equalityEngine.explainEquality(atom[0], atom[1], polarity, assumptions, eqp); } else { d_equalityEngine.explainPredicate(atom, polarity, assumptions); } + if( eqp ){ + Debug("array-pf") << " Proof is : " << std::endl; + eqp->debug_print("array-pf"); + } } @@ -435,7 +441,7 @@ void TheoryArrays::preRegisterTermInternal(TNode node) if (ni != node) { preRegisterTermInternal(ni); } - d_equalityEngine.assertEquality(ni.eqNode(s[2]), true, d_true); + d_equalityEngine.assertEquality(ni.eqNode(s[2]), true, d_true, eq::MERGED_ARRAYS_ROW1); Assert(++it == stores->end()); } } @@ -482,7 +488,7 @@ void TheoryArrays::preRegisterTermInternal(TNode node) } // Apply RIntro1 Rule - d_equalityEngine.assertEquality(ni.eqNode(v), true, d_true); + d_equalityEngine.assertEquality(ni.eqNode(v), true, d_true, eq::MERGED_ARRAYS_ROW1); } d_infoMap.addStore(node, node); @@ -1892,7 +1898,7 @@ void TheoryArrays::checkRIntro1(TNode a, TNode b) d_infoMap.setRIntro1Applied(s); Node ni = nm->mkNode(kind::SELECT, s, s[1]); preRegisterTermInternal(ni); - d_equalityEngine.assertEquality(ni.eqNode(s[2]), true, d_true); + d_equalityEngine.assertEquality(ni.eqNode(s[2]), true, d_true, eq::MERGED_ARRAYS_ROW1); } } @@ -2283,7 +2289,7 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem) if (!bjExists) { preRegisterTermInternal(bj); } - d_equalityEngine.assertEquality(aj_eq_bj, true, reason); + d_equalityEngine.assertEquality(aj_eq_bj, true, reason, eq::MERGED_ARRAYS_ROW); ++d_numProp; return; } @@ -2293,7 +2299,7 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem) Node i_eq_j = i.eqNode(j); Node reason = nm->mkNode(kind::OR, i_eq_j, aj_eq_bj); d_permRef.push_back(reason); - d_equalityEngine.assertEquality(i_eq_j, true, reason); + d_equalityEngine.assertEquality(i_eq_j, true, reason, eq::MERGED_ARRAYS_ROW); ++d_numProp; return; } diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp index df1d2ebde..0fb42231f 100644 --- a/src/theory/uf/equality_engine.cpp +++ b/src/theory/uf/equality_engine.cpp @@ -3,7 +3,7 @@ ** \verbatim ** Original author: Dejan Jovanovic ** Major contributors: none - ** Minor contributors (to current version): Dejan Jovanovic, Tim King, Francois Bobot, Morgan Deters + ** Minor contributors (to current version): Dejan Jovanovic, Tim King, Francois Bobot, Morgan Deters, Andrew Reynolds ** This file is part of the CVC4 project. ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing @@ -364,9 +364,9 @@ const EqualityNode& EqualityEngine::getEqualityNode(EqualityNodeId nodeId) const return d_equalityNodes[nodeId]; } -void EqualityEngine::assertEqualityInternal(TNode t1, TNode t2, TNode reason) { +void EqualityEngine::assertEqualityInternal(TNode t1, TNode t2, TNode reason, MergeReasonType pid) { - Debug("equality") << d_name << "::eq::addEqualityInternal(" << t1 << "," << t2 << ")" << std::endl; + Debug("equality") << d_name << "::eq::addEqualityInternal(" << t1 << "," << t2 << "), pid = " << pid << std::endl; if (d_done) { return; @@ -379,13 +379,13 @@ void EqualityEngine::assertEqualityInternal(TNode t1, TNode t2, TNode reason) { // Add to the queue and propagate EqualityNodeId t1Id = getNodeId(t1); EqualityNodeId t2Id = getNodeId(t2); - enqueue(MergeCandidate(t1Id, t2Id, MERGED_THROUGH_EQUALITY, reason)); + enqueue(MergeCandidate(t1Id, t2Id, pid, reason)); } -void EqualityEngine::assertPredicate(TNode t, bool polarity, TNode reason) { +void EqualityEngine::assertPredicate(TNode t, bool polarity, TNode reason, MergeReasonType 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); + assertEqualityInternal(t, polarity ? d_true : d_false, reason, pid); propagate(); } @@ -395,7 +395,7 @@ void EqualityEngine::mergePredicates(TNode p, TNode q, TNode reason) { propagate(); } -void EqualityEngine::assertEquality(TNode eq, bool polarity, TNode reason) { +void EqualityEngine::assertEquality(TNode eq, bool polarity, TNode reason, MergeReasonType 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 @@ -403,7 +403,7 @@ void EqualityEngine::assertEquality(TNode eq, bool polarity, TNode reason) { return; } // Add equality between terms - assertEqualityInternal(eq[0], eq[1], reason); + assertEqualityInternal(eq[0], eq[1], reason, pid); propagate(); } else { // If two terms are already dis-equal, don't assert anything @@ -418,7 +418,7 @@ void EqualityEngine::assertEquality(TNode eq, bool polarity, TNode reason) { Debug("equality::trigger") << d_name << "::eq::addEquality(" << eq << "," << (polarity ? "true" : "false") << ")" << std::endl; - assertEqualityInternal(eq, d_false, reason); + assertEqualityInternal(eq, d_false, reason, pid); propagate(); if (d_done) { @@ -1028,14 +1028,6 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st Debug("equality") << pop; break; } - case MERGED_THROUGH_EQUALITY: - // Construct the equality - Debug("equality") << d_name << "::eq::getExplanation(): adding: " << d_equalityEdges[currentEdge].getReason() << std::endl; - if( eqpc ){ - eqpc->d_node = d_equalityEdges[currentEdge].getReason(); - } - equalities.push_back(d_equalityEdges[currentEdge].getReason()); - break; case MERGED_THROUGH_REFLEXIVITY: { // x1 == x1 Debug("equality") << d_name << "::eq::getExplanation(): due to reflexivity, going deeper" << std::endl; @@ -1080,8 +1072,21 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st break; } - default: - Unreachable(); + 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(); + }else{ + //theory-specific proof rule : TODO + eqpc->d_id = reasonType; + //eqpc->d_node = d_equalityEdges[currentEdge].getNodeId(); + } + } + equalities.push_back(d_equalityEdges[currentEdge].getReason()); + break; + } } // Go to the previous @@ -2054,7 +2059,7 @@ void EqProof::debug_print( const char * c, unsigned tb ){ } for( unsigned i=0; i0 || !d_node.isNull() ) Debug( c ) << ","; - std::cout << std::endl; + Debug( c ) << std::endl; d_children[i]->debug_print( c, tb+1 ); } } diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h index 8bb849496..2961b510a 100644 --- a/src/theory/uf/equality_engine.h +++ b/src/theory/uf/equality_engine.h @@ -521,7 +521,7 @@ private: /** * Adds an equality of terms t1 and t2 to the database. */ - void assertEqualityInternal(TNode t1, TNode t2, TNode reason); + void assertEqualityInternal(TNode t1, TNode t2, TNode reason, MergeReasonType pid = MERGED_THROUGH_EQUALITY); /** * Adds a trigger equality to the database with the trigger node and polarity for notification. @@ -751,7 +751,7 @@ public: * asserting the negated predicate * @param reason the reason to keep for building explanations */ - void assertPredicate(TNode p, bool polarity, TNode reason); + void assertPredicate(TNode p, bool polarity, TNode reason, MergeReasonType pid = MERGED_THROUGH_EQUALITY); /** * Adds predicate p and q and makes them equal. @@ -766,7 +766,7 @@ public: * asserting the negated equality * @param reason the reason to keep for building explanations */ - void assertEquality(TNode eq, bool polarity, TNode reason); + void assertEquality(TNode eq, bool polarity, TNode reason, MergeReasonType pid = MERGED_THROUGH_EQUALITY); /** * Returns the current representative of the term t. diff --git a/src/theory/uf/equality_engine_types.h b/src/theory/uf/equality_engine_types.h index 435a1ece5..0ee50c74d 100644 --- a/src/theory/uf/equality_engine_types.h +++ b/src/theory/uf/equality_engine_types.h @@ -70,6 +70,10 @@ enum MergeReasonType { /** (for proofs only) Equality was merged due to transitivity */ MERGED_THROUGH_TRANS, + + /** Theory specific proof rules */ + MERGED_ARRAYS_ROW, + MERGED_ARRAYS_ROW1, }; inline std::ostream& operator << (std::ostream& out, MergeReasonType reason) { @@ -91,7 +95,8 @@ inline std::ostream& operator << (std::ostream& out, MergeReasonType reason) { out << "transitivity"; break; default: - Unreachable(); + out << "[theory]"; + break; } return out; } -- 2.30.2