Add ability to provide theory-specific proof rules to EqualityEngine, extends enumeration of MergeReasonType. Add initial use in TheoryArrays.

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<TNode>& 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; i<d_children.size(); i++ ){
       if( i>0 || !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;
 }