(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.h b/src/theory/strings/infer_info.h
index 7d41dca98..31a74784e 100644
--- a/src/theory/strings/infer_info.h
+++ b/src/theory/strings/infer_info.h
@@ -38,6 +38,7 @@ namespace strings {
  */
 enum class Inference : uint32_t
 {
+  BEGIN,
   //-------------------------------------- base solver
   // initial normalize singular
   //   x1 = "" ^ ... ^ x_{i-1} = "" ^ x_{i+1} = "" ^ ... ^ xn = "" =>
@@ -295,6 +296,10 @@ enum class Inference : uint32_t
   // (see theory_strings_preprocess).
   REDUCTION,
   //-------------------------------------- end extended function solver
+  //-------------------------------------- prefix conflict
+  // prefix conflict (coarse-grained)
+  PREFIX_CONFLICT,
+  //-------------------------------------- end prefix conflict
   NONE,
 };
 
@@ -359,9 +364,11 @@ class InferInfo
   /**
    * The "new literal" antecedant(s) of the inference, interpreted
    * conjunctively. These are literals that were needed to show the conclusion
-   * but do not currently hold in the equality engine.
+   * but do not currently hold in the equality engine. These should be a subset
+   * of d_ant. In other words, antecedants that are not explained are stored
+   * in *both* d_ant and d_noExplain.
    */
-  std::vector<Node> d_antn;
+  std::vector<Node> d_noExplain;
   /**
    * A list of new skolems introduced as a result of this inference. They
    * are mapped to by a length status, indicating the length constraint that
@@ -372,15 +379,17 @@ class InferInfo
   bool isTrivial() const;
   /**
    * Does this infer info correspond to a conflict? True if d_conc is false
-   * and it has no new antecedants (d_antn).
+   * and it has no new antecedants (d_noExplain).
    */
   bool isConflict() const;
   /**
    * Does this infer info correspond to a "fact". A fact is an inference whose
    * conclusion should be added as an equality or predicate to the equality
-   * engine with no new external antecedants (d_antn).
+   * engine with no new external antecedants (d_noExplain).
    */
   bool isFact() const;
+  /** Get antecedant */
+  Node getAntecedant() const;
 };
 
 /**