(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, 37 insertions, 24 deletions

diff --git a/src/theory/strings/regexp_solver.cpp b/src/theory/strings/regexp_solver.cpp
index c5d6df601..62127d5c0 100644
--- a/src/theory/strings/regexp_solver.cpp
+++ b/src/theory/strings/regexp_solver.cpp
@@ -221,10 +221,13 @@ void RegExpSolver::check(const std::map<Node, std::vector<Node> >& mems)
             else
             {
               // we have a conflict
-              std::vector<Node> exp_n;
-              exp_n.push_back(assertion);
+              std::vector<Node> iexp = nfexp;
+              std::vector<Node> noExplain;
+              iexp.push_back(assertion);
+              noExplain.push_back(assertion);
               Node conc = Node::null();
-              d_im.sendInference(nfexp, exp_n, conc, Inference::RE_NF_CONFLICT);
+              d_im.sendInference(
+                  iexp, noExplain, conc, Inference::RE_NF_CONFLICT);
               addedLemma = true;
               break;
             }
@@ -266,8 +269,10 @@ void RegExpSolver::check(const std::map<Node, std::vector<Node> >& mems)
           // if simplifying successfully generated a lemma
           if (!conc.isNull())
           {
-            std::vector<Node> exp_n;
-            exp_n.push_back(assertion);
+            std::vector<Node> iexp = rnfexp;
+            std::vector<Node> noExplain;
+            iexp.push_back(assertion);
+            noExplain.push_back(assertion);
             Assert(atom.getKind() == STRING_IN_REGEXP);
             if (polarity)
             {
@@ -279,7 +284,7 @@ void RegExpSolver::check(const std::map<Node, std::vector<Node> >& mems)
             }
             Inference inf =
                 polarity ? Inference::RE_UNFOLD_POS : Inference::RE_UNFOLD_NEG;
-            d_im.sendInference(rnfexp, exp_n, conc, inf);
+            d_im.sendInference(iexp, noExplain, conc, inf);
             addedLemma = true;
             if (changed)
             {
@@ -399,7 +404,7 @@ bool RegExpSolver::checkEqcInclusion(std::vector<Node>& mems)
 
           Node conc;
           d_im.sendInference(
-              vec_nodes, conc, Inference::RE_INTER_INCLUDE, true);
+              vec_nodes, conc, Inference::RE_INTER_INCLUDE, false, true);
           return false;
         }
       }
@@ -480,19 +485,21 @@ bool RegExpSolver::checkEqcIntersect(const std::vector<Node>& mems)
         vec_nodes.push_back(mi[0].eqNode(m[0]));
       }
       Node conc;
-      d_im.sendInference(vec_nodes, conc, Inference::RE_INTER_CONF, true);
+      d_im.sendInference(
+          vec_nodes, conc, Inference::RE_INTER_CONF, false, true);
       // conflict, return
       return false;
     }
     // rewrite to ensure the equality checks below are precise
-    Node mres = Rewriter::rewrite(nm->mkNode(STRING_IN_REGEXP, mi[0], resR));
-    if (mres == mi)
+    Node mres = nm->mkNode(STRING_IN_REGEXP, mi[0], resR);
+    Node mresr = Rewriter::rewrite(mres);
+    if (mresr == mi)
     {
       // if R1 = intersect( R1, R2 ), then x in R1 ^ x in R2 is equivalent
       // to x in R1, hence x in R2 can be marked redundant.
       d_im.markReduced(m);
     }
-    else if (mres == m)
+    else if (mresr == m)
     {
       // same as above, opposite direction
       d_im.markReduced(mi);
@@ -508,7 +515,8 @@ bool RegExpSolver::checkEqcIntersect(const std::vector<Node>& mems)
       {
         vec_nodes.push_back(mi[0].eqNode(m[0]));
       }
-      d_im.sendInference(vec_nodes, mres, Inference::RE_INTER_INFER, true);
+      d_im.sendInference(
+          vec_nodes, mres, Inference::RE_INTER_INFER, false, true);
       // both are reduced
       d_im.markReduced(m);
       d_im.markReduced(mi);
@@ -529,10 +537,12 @@ bool RegExpSolver::checkPDerivative(
     {
       case 0:
       {
-        std::vector<Node> exp_n;
-        exp_n.push_back(atom);
-        exp_n.push_back(x.eqNode(d_emptyString));
-        d_im.sendInference(nf_exp, exp_n, exp, Inference::RE_DELTA);
+        std::vector<Node> noExplain;
+        noExplain.push_back(atom);
+        noExplain.push_back(x.eqNode(d_emptyString));
+        std::vector<Node> iexp = nf_exp;
+        iexp.insert(iexp.end(), noExplain.begin(), noExplain.end());
+        d_im.sendInference(iexp, noExplain, exp, Inference::RE_DELTA);
         addedLemma = true;
         d_regexp_ccached.insert(atom);
         return false;
@@ -544,11 +554,12 @@ bool RegExpSolver::checkPDerivative(
       }
       case 2:
       {
-        std::vector<Node> exp_n;
-        exp_n.push_back(atom);
-        exp_n.push_back(x.eqNode(d_emptyString));
-        Node conc;
-        d_im.sendInference(nf_exp, exp_n, conc, Inference::RE_DELTA_CONF);
+        std::vector<Node> noExplain;
+        noExplain.push_back(atom);
+        noExplain.push_back(x.eqNode(d_emptyString));
+        std::vector<Node> iexp = nf_exp;
+        iexp.insert(iexp.end(), noExplain.begin(), noExplain.end());
+        d_im.sendInference(iexp, noExplain, d_false, Inference::RE_DELTA_CONF);
         addedLemma = true;
         d_regexp_ccached.insert(atom);
         return false;
@@ -637,9 +648,11 @@ bool RegExpSolver::deriveRegExp(Node x,
         conc = NodeManager::currentNM()->mkNode(STRING_IN_REGEXP, left, dc);
       }
     }
-    std::vector<Node> exp_n;
-    exp_n.push_back(atom);
-    d_im.sendInference(ant, exp_n, conc, Inference::RE_DERIVE);
+    std::vector<Node> iexp = ant;
+    std::vector<Node> noExplain;
+    noExplain.push_back(atom);
+    iexp.push_back(atom);
+    d_im.sendInference(iexp, noExplain, conc, Inference::RE_DERIVE);
     return true;
   }
   return false;