Add InferenceIds for theory of arrays (#5910)

This PR introduces new InferenceIds for the theory of arrays and uses them instead of InferenceId::UNKNOWN.

diff --git a/src/theory/arrays/inference_manager.cpp b/src/theory/arrays/inference_manager.cpp
index be29724447d07d05f156a2e25310c34bbd35f55a..afcc9a719fae89559cb05f84a8c076a1ece5ee0f 100644 (file)
--- a/src/theory/arrays/inference_manager.cpp
+++ b/src/theory/arrays/inference_manager.cpp
@@ -37,8 +37,9 @@ InferenceManager::InferenceManager(Theory& t,
 
 bool InferenceManager::assertInference(TNode atom,
                                        bool polarity,
+                                       InferenceId id,
                                        TNode reason,
-                                       PfRule id)
+                                       PfRule pfr)
 {
   Trace("arrays-infer") << "TheoryArrays::assertInference: "
                         << (polarity ? Node(atom) : atom.notNode()) << " by "
@@ -52,14 +53,14 @@ bool InferenceManager::assertInference(TNode atom,
     std::vector<Node> children;
     std::vector<Node> args;
     // convert to proof rule application
-    convert(id, fact, reason, children, args);
-    return assertInternalFact(atom, polarity, InferenceId::UNKNOWN, id, children, args);
+    convert(pfr, fact, reason, children, args);
+    return assertInternalFact(atom, polarity, id, pfr, children, args);
   }
-  return assertInternalFact(atom, polarity, InferenceId::UNKNOWN, reason);
+  return assertInternalFact(atom, polarity, id, reason);
 }
 
 bool InferenceManager::arrayLemma(
-    Node conc, Node exp, PfRule id, LemmaProperty p, bool doCache)
+    Node conc, InferenceId id, Node exp, PfRule pfr, LemmaProperty p, bool doCache)
 {
   Trace("arrays-infer") << "TheoryArrays::arrayLemma: " << conc << " by " << exp
                         << "; " << id << std::endl;
@@ -69,14 +70,14 @@ bool InferenceManager::arrayLemma(
     std::vector<Node> children;
     std::vector<Node> args;
     // convert to proof rule application
-    convert(id, conc, exp, children, args);
+    convert(pfr, conc, exp, children, args);
     // make the trusted lemma based on the eager proof generator and send
-    TrustNode tlem = d_lemmaPg->mkTrustNode(conc, id, children, args);
-    return trustedLemma(tlem, InferenceId::UNKNOWN, p, doCache);
+    TrustNode tlem = d_lemmaPg->mkTrustNode(conc, pfr, children, args);
+    return trustedLemma(tlem, id, p, doCache);
   }
   // send lemma without proofs
   Node lem = nm->mkNode(IMPLIES, exp, conc);
-  return lemma(lem, InferenceId::UNKNOWN, p, doCache);
+  return lemma(lem, id, p, doCache);
 }
 
 void InferenceManager::convert(PfRule& id,

diff --git a/src/theory/arrays/inference_manager.h b/src/theory/arrays/inference_manager.h
index b4ae228be2d93623e595a00972d5e7316872faae..96af0b6771857f16a0bac11a7963a0d41f79af72 100644 (file)
--- a/src/theory/arrays/inference_manager.h
+++ b/src/theory/arrays/inference_manager.h
@@ -45,14 +45,15 @@ class InferenceManager : public TheoryInferenceManager
    * @return true if the fact was successfully asserted, and false if the
    * fact was redundant.
    */
-  bool assertInference(TNode atom, bool polarity, TNode reason, PfRule id);
+  bool assertInference(TNode atom, bool polarity, InferenceId id, TNode reason, PfRule pfr);
   /**
    * Send lemma (exp => conc) based on proof rule id with properties p. Cache
    * the lemma if doCache is true.
    */
   bool arrayLemma(Node conc,
+                  InferenceId id,
                   Node exp,
-                  PfRule id,
+                  PfRule pfr,
                   LemmaProperty p = LemmaProperty::NONE,
                   bool doCache = false);
 

diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index b13bd6926e0f5ef3a22005f66cedeeeab9e0f72f..f07140d4e93f58cc0602ab4274400597518229d4 100644 (file)
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -771,8 +771,11 @@ void TheoryArrays::preRegisterTermInternal(TNode node)
         preRegisterTermInternal(ni);
       }
       // Apply RIntro1 Rule
-      d_im.assertInference(
-          ni.eqNode(v), true, d_true, PfRule::ARRAYS_READ_OVER_WRITE_1);
+      d_im.assertInference(ni.eqNode(v),
+                           true,
+                           InferenceId::ARRAYS_READ_OVER_WRITE_1,
+                           d_true,
+                           PfRule::ARRAYS_READ_OVER_WRITE_1);
 
       d_infoMap.addStore(node, node);
       d_infoMap.addInStore(a, node);
@@ -1373,14 +1376,14 @@ void TheoryArrays::notifyFact(TNode atom, bool pol, TNode fact, bool isInternal)
         Debug("pf::array") << "Asserting to the equality engine:" << std::endl
                            << "\teq = " << eq << std::endl
                            << "\treason = " << fact << std::endl;
-        d_im.assertInference(eq, false, fact, PfRule::ARRAYS_EXT);
+        d_im.assertInference(eq, false, InferenceId::ARRAYS_EXT, fact, PfRule::ARRAYS_EXT);
         ++d_numProp;
       }
 
       // If this is the solution pass, generate the lemma. Otherwise, don't
       // generate it - as this is the lemma that we're reproving...
       Trace("arrays-lem") << "Arrays::addExtLemma " << lemma << "\n";
-      d_im.arrayLemma(eq.notNode(), fact, PfRule::ARRAYS_EXT);
+      d_im.arrayLemma(eq.notNode(), InferenceId::ARRAYS_EXT, fact, PfRule::ARRAYS_EXT);
       ++d_numExt;
     }
     else
@@ -1660,8 +1663,11 @@ void TheoryArrays::checkRowForIndex(TNode i, TNode a)
     {
       preRegisterTermInternal(selConst);
     }
-    d_im.assertInference(
-        selConst.eqNode(defValue), true, d_true, PfRule::ARRAYS_TRUST);
+    d_im.assertInference(selConst.eqNode(defValue),
+                         true,
+                         InferenceId::UNKNOWN,
+                         d_true,
+                         PfRule::ARRAYS_TRUST);
   }
 
   const CTNodeList* stores = d_infoMap.getStores(a);
@@ -1798,7 +1804,7 @@ void TheoryArrays::propagateRowLemma(RowLemmaType lem)
         preRegisterTermInternal(bj);
       }
       d_im.assertInference(
-          aj_eq_bj, true, reason, PfRule::ARRAYS_READ_OVER_WRITE);
+          aj_eq_bj, true, InferenceId::ARRAYS_READ_OVER_WRITE, reason, PfRule::ARRAYS_READ_OVER_WRITE);
       ++d_numProp;
       return;
     }
@@ -1809,7 +1815,7 @@ void TheoryArrays::propagateRowLemma(RowLemmaType lem)
           (aj.isConst() && bj.isConst()) ? d_true : aj.eqNode(bj).notNode();
       Node j_eq_i = j.eqNode(i);
       d_im.assertInference(
-          j_eq_i, true, reason, PfRule::ARRAYS_READ_OVER_WRITE_CONTRA);
+          j_eq_i, true, InferenceId::ARRAYS_READ_OVER_WRITE_CONTRA, reason, PfRule::ARRAYS_READ_OVER_WRITE_CONTRA);
       ++d_numProp;
       return;
     }
@@ -1876,7 +1882,7 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem)
         preRegisterTermInternal(aj2);
       }
       d_im.assertInference(
-          aj.eqNode(aj2), true, d_true, PfRule::MACRO_SR_PRED_INTRO);
+          aj.eqNode(aj2), true, InferenceId::UNKNOWN, d_true, PfRule::MACRO_SR_PRED_INTRO);
     }
     Node bj2 = Rewriter::rewrite(bj);
     if (bj != bj2) {
@@ -1888,7 +1894,7 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem)
         preRegisterTermInternal(bj2);
       }
       d_im.assertInference(
-          bj.eqNode(bj2), true, d_true, PfRule::MACRO_SR_PRED_INTRO);
+          bj.eqNode(bj2), true, InferenceId::UNKNOWN, d_true, PfRule::MACRO_SR_PRED_INTRO);
     }
     if (aj2 == bj2) {
       return;
@@ -1906,14 +1912,14 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem)
       {
         preRegisterTermInternal(bj2);
       }
-      d_im.assertInference(eq1, true, d_true, PfRule::MACRO_SR_PRED_INTRO);
+      d_im.assertInference(eq1, true, InferenceId::UNKNOWN, d_true, PfRule::MACRO_SR_PRED_INTRO);
       return;
     }
 
     Node eq2 = i.eqNode(j);
     Node eq2_r = Rewriter::rewrite(eq2);
     if (eq2_r == d_true) {
-      d_im.assertInference(eq2, true, d_true, PfRule::MACRO_SR_PRED_INTRO);
+      d_im.assertInference(eq2, true, InferenceId::UNKNOWN, d_true, PfRule::MACRO_SR_PRED_INTRO);
       return;
     }
 
@@ -1923,7 +1929,7 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem)
     d_RowAlreadyAdded.insert(lem);
     // use non-rewritten nodes
     d_im.arrayLemma(
-        aj.eqNode(bj), eq2.notNode(), PfRule::ARRAYS_READ_OVER_WRITE);
+        aj.eqNode(bj), InferenceId::ARRAYS_READ_OVER_WRITE, eq2.notNode(), PfRule::ARRAYS_READ_OVER_WRITE);
     ++d_numRow;
   }
   else {
@@ -1993,7 +1999,7 @@ bool TheoryArrays::dischargeLemmas()
         preRegisterTermInternal(aj2);
       }
       d_im.assertInference(
-          aj.eqNode(aj2), true, d_true, PfRule::MACRO_SR_PRED_INTRO);
+          aj.eqNode(aj2), true, InferenceId::UNKNOWN, d_true, PfRule::MACRO_SR_PRED_INTRO);
     }
     Node bj2 = Rewriter::rewrite(bj);
     if (bj != bj2) {
@@ -2005,7 +2011,7 @@ bool TheoryArrays::dischargeLemmas()
         preRegisterTermInternal(bj2);
       }
       d_im.assertInference(
-          bj.eqNode(bj2), true, d_true, PfRule::MACRO_SR_PRED_INTRO);
+          bj.eqNode(bj2), true, InferenceId::UNKNOWN, d_true, PfRule::MACRO_SR_PRED_INTRO);
     }
     if (aj2 == bj2) {
       continue;
@@ -2023,14 +2029,14 @@ bool TheoryArrays::dischargeLemmas()
       {
         preRegisterTermInternal(bj2);
       }
-      d_im.assertInference(eq1, true, d_true, PfRule::MACRO_SR_PRED_INTRO);
+      d_im.assertInference(eq1, true, InferenceId::UNKNOWN, d_true, PfRule::MACRO_SR_PRED_INTRO);
       continue;
     }
 
     Node eq2 = i.eqNode(j);
     Node eq2_r = Rewriter::rewrite(eq2);
     if (eq2_r == d_true) {
-      d_im.assertInference(eq2, true, d_true, PfRule::MACRO_SR_PRED_INTRO);
+      d_im.assertInference(eq2, true, InferenceId::UNKNOWN, d_true, PfRule::MACRO_SR_PRED_INTRO);
       continue;
     }
 
@@ -2040,7 +2046,7 @@ bool TheoryArrays::dischargeLemmas()
     d_RowAlreadyAdded.insert(l);
     // use non-rewritten nodes, theory preprocessing will rewrite
     d_im.arrayLemma(
-        aj.eqNode(bj), eq2.notNode(), PfRule::ARRAYS_READ_OVER_WRITE);
+        aj.eqNode(bj), InferenceId::ARRAYS_READ_OVER_WRITE, eq2.notNode(), PfRule::ARRAYS_READ_OVER_WRITE);
     ++d_numRow;
     lemmasAdded = true;
     if (options::arraysReduceSharing()) {

diff --git a/src/theory/inference_id.cpp b/src/theory/inference_id.cpp
index c037a035acb281fc1e2de48b7a17d4ba3ab8b40f..5a2158d00bad90db9bed16c680f7359ab669f295 100644 (file)
--- a/src/theory/inference_id.cpp
+++ b/src/theory/inference_id.cpp
@@ -46,6 +46,11 @@ const char* toString(InferenceId i)
     case InferenceId::ARITH_NL_ICP_CONFLICT: return "ICP_CONFLICT";
     case InferenceId::ARITH_NL_ICP_PROPAGATION: return "ICP_PROPAGATION";
 
+    case InferenceId::ARRAYS_EXT: return "ARRAYS_EXT";
+    case InferenceId::ARRAYS_READ_OVER_WRITE: return "ARRAYS_READ_OVER_WRITE";
+    case InferenceId::ARRAYS_READ_OVER_WRITE_1: return "ARRAYS_READ_OVER_WRITE_1";
+    case InferenceId::ARRAYS_READ_OVER_WRITE_CONTRA: return "ARRAYS_READ_OVER_WRITE_CONTRA";
+
     case InferenceId::BAG_NON_NEGATIVE_COUNT: return "BAG_NON_NEGATIVE_COUNT";
     case InferenceId::BAG_MK_BAG_SAME_ELEMENT: return "BAG_MK_BAG_SAME_ELEMENT";
     case InferenceId::BAG_MK_BAG: return "BAG_MK_BAG";

diff --git a/src/theory/inference_id.h b/src/theory/inference_id.h
index f2192437aed7f449768781ba273c5492d6345186..f28faa0371030f5703a7cff6243b5e2ffb55d620 100644 (file)
--- a/src/theory/inference_id.h
+++ b/src/theory/inference_id.h
@@ -96,6 +96,10 @@ enum class InferenceId
   ARITH_NL_ICP_PROPAGATION,
   //-------------------- unknown
 
+  ARRAYS_EXT,
+  ARRAYS_READ_OVER_WRITE,
+  ARRAYS_READ_OVER_WRITE_1,
+  ARRAYS_READ_OVER_WRITE_CONTRA,
 
   BAG_NON_NEGATIVE_COUNT,
   BAG_MK_BAG_SAME_ELEMENT,