(proof-new) Prepare the theory of strings for proof reconstruction (#4885)

This updates the internal data structure for strings inferences "InferInfo" such that it is amenable to proof reconstruction.

Currently, the explanation for a conclusion is in two parts:
(1) d_ant, the antecedents that can be explained by the current equality engine,
(2) d_antn, the antecedents that cannot.

For proof reconstruction, the order of some antecedents matters. This is difficult with the above data structure since elements in these two vectors are not given an ordering relative to each other. After this PR, we store:
(1) d_ant, all antecedants, which are ordered in a way that is amenable to proofs (to be introduced on following PRs),
(2) d_noExplain, the subset of d_ant that cannot be explained by the current equality engine.

This PR modifies calls to InferenceManager in preparation for extending it with a proof reconstructor InferProofCons which will convert strings::InferInfo into instructions for building ProofNode.

1 files changed, 22 insertions, 19 deletions

diff --git a/src/theory/strings/inference_manager.cpp b/src/theory/strings/inference_manager.cpp
index 91af2a434..88cf6d958 100644
--- a/src/theory/strings/inference_manager.cpp
+++ b/src/theory/strings/inference_manager.cpp
@@ -117,9 +117,10 @@ bool InferenceManager::sendInternalInference(std::vector<Node>& exp,
 }
 
 void InferenceManager::sendInference(const std::vector<Node>& exp,
-                                     const std::vector<Node>& expn,
+                                     const std::vector<Node>& noExplain,
                                      Node eq,
                                      Inference infer,
+                                     bool isRev,
                                      bool asLemma)
 {
   eq = eq.isNull() ? d_false : Rewriter::rewrite(eq);
@@ -130,19 +131,21 @@ void InferenceManager::sendInference(const std::vector<Node>& exp,
   // wrap in infer info and send below
   InferInfo ii;
   ii.d_id = infer;
+  ii.d_idRev = isRev;
   ii.d_conc = eq;
   ii.d_ant = exp;
-  ii.d_antn = expn;
+  ii.d_noExplain = noExplain;
   sendInference(ii, asLemma);
 }
 
 void InferenceManager::sendInference(const std::vector<Node>& exp,
                                      Node eq,
                                      Inference infer,
+                                     bool isRev,
                                      bool asLemma)
 {
-  std::vector<Node> expn;
-  sendInference(exp, expn, eq, infer, asLemma);
+  std::vector<Node> noExplain;
+  sendInference(exp, noExplain, eq, infer, isRev, asLemma);
 }
 
 void InferenceManager::sendInference(const InferInfo& ii, bool asLemma)
@@ -277,7 +280,7 @@ void InferenceManager::doPendingFacts()
     InferInfo& ii = d_pending[i];
     // At this point, ii should be a "fact", i.e. something whose conclusion
     // should be added as a normal equality or predicate to the equality engine
-    // with no new external assumptions (ii.d_antn).
+    // with no new external assumptions (ii.d_noExplain).
     Assert(ii.isFact());
     Node facts = ii.d_conc;
     Node exp = utils::mkAnd(ii.d_ant);
@@ -336,13 +339,12 @@ void InferenceManager::doPendingLemmas()
     Node eqExp;
     if (options::stringRExplainLemmas())
     {
-      eqExp = mkExplain(ii.d_ant, ii.d_antn);
+      eqExp = mkExplain(ii.d_ant, ii.d_noExplain);
     }
     else
     {
       std::vector<Node> ev;
       ev.insert(ev.end(), ii.d_ant.begin(), ii.d_ant.end());
-      ev.insert(ev.end(), ii.d_antn.begin(), ii.d_antn.end());
       eqExp = utils::mkAnd(ev);
     }
     // make the lemma node
@@ -455,12 +457,12 @@ bool InferenceManager::hasProcessed() const
 
 Node InferenceManager::mkExplain(const std::vector<Node>& a) const
 {
-  std::vector<Node> an;
-  return mkExplain(a, an);
+  std::vector<Node> noExplain;
+  return mkExplain(a, noExplain);
 }
 
 Node InferenceManager::mkExplain(const std::vector<Node>& a,
-                                 const std::vector<Node>& an) const
+                                 const std::vector<Node>& noExplain) const
 {
   std::vector<TNode> antec_exp;
   // copy to processing vector
@@ -472,6 +474,16 @@ Node InferenceManager::mkExplain(const std::vector<Node>& a,
   eq::EqualityEngine* ee = d_state.getEqualityEngine();
   for (const Node& apc : aconj)
   {
+    if (std::find(noExplain.begin(), noExplain.end(), apc) != noExplain.end())
+    {
+      if (std::find(antec_exp.begin(), antec_exp.end(), apc) == antec_exp.end())
+      {
+        Debug("strings-explain")
+            << "Add to explanation (new literal) " << apc << std::endl;
+        antec_exp.push_back(apc);
+      }
+      continue;
+    }
     Assert(apc.getKind() != AND);
     Debug("strings-explain") << "Add to explanation " << apc << std::endl;
     if (apc.getKind() == NOT && apc[0].getKind() == EQUAL)
@@ -485,15 +497,6 @@ Node InferenceManager::mkExplain(const std::vector<Node>& a,
     // now, explain
     explain(apc, antec_exp);
   }
-  for (const Node& anc : an)
-  {
-    if (std::find(antec_exp.begin(), antec_exp.end(), anc) == antec_exp.end())
-    {
-      Debug("strings-explain")
-          << "Add to explanation (new literal) " << anc << std::endl;
-      antec_exp.push_back(anc);
-    }
-  }
   Node ant;
   if (antec_exp.empty())
   {