(proof-new) Update the strings inference manager for proofs (#5220)

This updates the inference manager in strings in two ways:
(1) It now inherits from InferenceManagerBuffered, meaning that the custom methods for process the current pending lemma/fact vectors are removed in favor of the standard ones.
(2) It has support for proof generation via the InferProofCons utility.

This PR standardizes three methods processFact, processLemma, and processConflict which take InferInfo and processes any string-specific behavior pertaining to processing facts, lemmas and conflicts with the inference manager. These methods are intended to preserve the previous behavior of this class.

1 files changed, 8 insertions, 1 deletions

diff --git a/src/theory/strings/infer_info.h b/src/theory/strings/infer_info.h
index 13e9a3f64..4c5674d2b 100644
--- a/src/theory/strings/infer_info.h
+++ b/src/theory/strings/infer_info.h
@@ -21,6 +21,7 @@
 #include <vector>
 
 #include "expr/node.h"
+#include "theory/theory_inference.h"
 #include "util/safe_print.h"
 
 namespace CVC4 {
@@ -347,6 +348,8 @@ enum LengthStatus
   LENGTH_GEQ_ONE
 };
 
+class InferenceManager;
+
 /**
  * An inference. This is a class to track an unprocessed call to either
  * send a fact, lemma, or conflict that is waiting to be asserted to the
@@ -368,11 +371,15 @@ enum LengthStatus
  * - (main equality) x ++ y ++ v1 = z ++ w ++ v2,
  * - (length constraint) len(y) = len(w).
  */
-class InferInfo
+class InferInfo : public TheoryInference
 {
  public:
   InferInfo();
   ~InferInfo() {}
+  /** Process this inference */
+  bool process(TheoryInferenceManager* im, bool asLemma) override;
+  /** Pointer to the class used for processing this info */
+  InferenceManager* d_sim;
   /** The inference identifier */
   Inference d_id;
   /** Whether it is the reverse form of the above id */