(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, 13 insertions, 4 deletions

diff --git a/src/theory/strings/infer_info.cpp b/src/theory/strings/infer_info.cpp
index 174bbe2b7..ca5e8320d 100644
--- a/src/theory/strings/infer_info.cpp
+++ b/src/theory/strings/infer_info.cpp
@@ -14,6 +14,8 @@
 
 #include "theory/strings/infer_info.h"
 
+#include "theory/strings/theory_strings_utils.h"
+
 namespace CVC4 {
 namespace theory {
 namespace strings {
@@ -85,6 +87,7 @@ const char* toString(Inference i)
     case Inference::CTN_NEG_EQUAL: return "CTN_NEG_EQUAL";
     case Inference::CTN_POS: return "CTN_POS";
     case Inference::REDUCTION: return "REDUCTION";
+    case Inference::PREFIX_CONFLICT: return "PREFIX_CONFLICT";
     default: return "?";
   }
 }
@@ -106,14 +109,20 @@ bool InferInfo::isTrivial() const
 bool InferInfo::isConflict() const
 {
   Assert(!d_conc.isNull());
-  return d_conc.isConst() && !d_conc.getConst<bool>() && d_antn.empty();
+  return d_conc.isConst() && !d_conc.getConst<bool>() && d_noExplain.empty();
 }
 
 bool InferInfo::isFact() const
 {
   Assert(!d_conc.isNull());
   TNode atom = d_conc.getKind() == kind::NOT ? d_conc[0] : d_conc;
-  return !atom.isConst() && atom.getKind() != kind::OR && d_antn.empty();
+  return !atom.isConst() && atom.getKind() != kind::OR && d_noExplain.empty();
+}
+
+Node InferInfo::getAntecedant() const
+{
+  // d_noExplain is a subset of d_ant
+  return utils::mkAnd(d_ant);
 }
 
 std::ostream& operator<<(std::ostream& out, const InferInfo& ii)
@@ -127,9 +136,9 @@ std::ostream& operator<<(std::ostream& out, const InferInfo& ii)
   {
     out << " :ant (" << ii.d_ant << ")";
   }
-  if (!ii.d_antn.empty())
+  if (!ii.d_noExplain.empty())
   {
-    out << " :antn (" << ii.d_antn << ")";
+    out << " :no-explain (" << ii.d_noExplain << ")";
   }
   out << ")";
   return out;