Refactor inference manager in strings to be amenable to proofs (#4363)

This is a key refactoring towards proofs for strings.

This ensures that InferInfo is maintained until just before facts, lemmas and conflicts are processed. This allows us both to:
(1) track more accurate stats and debug information,
(2) have enough information to ensure that proofs can be constructed at the moment facts, lemmas, and conflicts are processed.

Changes in this PR:

PendingInfer and InferInfo were merged, CoreInferInfo is now the previous equivalent of InferInfo, extended with core-solver-specific information, which is only used by CoreSolver.
sendInference( const InferInfo& info, ... ) is now the central method for sending inferences which is called by the other variants, not the other way around.
sendLemma is inlined into sendInference(...) for clarity.
doPendingLemmas and doPendingFacts are extended to process the side effects of the inference infos.
There is actually a further issue with pending inferences related to eagerly processing the side effect of CoreInferInfo before we know the lemma is sent. I believe this issue does not occur in practice based on our strategy. Further refactoring could tighten this, e.g. virtual void InferInfo::processSideEffect. I will do this in another PR.

Further refactoring can address whether asLemma should be a field of InferInfo (it probably should), and whether we should explicitly check for AND in conclusions instead of making it the responsibility of the user of this class.

1 files changed, 18 insertions, 42 deletions

diff --git a/src/theory/strings/inference_manager.h b/src/theory/strings/inference_manager.h
index 6e11bf85e..cebd88a7f 100644
--- a/src/theory/strings/inference_manager.h
+++ b/src/theory/strings/inference_manager.h
@@ -35,29 +35,6 @@ namespace CVC4 {
 namespace theory {
 namespace strings {
 
-/**
- * A pending inference. This is a helper class to track an unprocessed call to
- * InferenceManager::sendInference that is waiting to be asserted as a fact to
- * the equality engine.
- */
-struct PendingInfer
-{
-  PendingInfer(Inference i, Node fact, Node exp)
-      : d_infer(i), d_fact(fact), d_exp(exp)
-  {
-  }
-  ~PendingInfer() {}
-  /** The inference identifier */
-  Inference d_infer;
-  /** The conclusion */
-  Node d_fact;
-  /**
-   * Its explanation. This is a conjunction of literals that hold in the
-   * equality engine in the current context.
-   */
-  Node d_exp;
-};
-
 /** Inference Manager
  *
  * The purpose of this class is to process inference steps for strategies
@@ -139,7 +116,7 @@ class InferenceManager
    * equality engine of the theory of strings. On the other hand, the set
    * exp_n ("explanations new") contain nodes that are not explainable by the
    * theory of strings. This method may call sendLemma or otherwise add a
-   * PendingInfer to d_pending, indicating a fact should be asserted to the
+   * InferInfo to d_pending, indicating a fact should be asserted to the
    * equality engine. Overall, the result of this method is one of the
    * following:
    *
@@ -167,7 +144,7 @@ class InferenceManager
    * of each type.
    *
    * If the flag asLemma is true, then this method will send a lemma instead
-   * of an inference whenever applicable.
+   * of a fact whenever applicable.
    */
   void sendInference(const std::vector<Node>& exp,
                      const std::vector<Node>& exp_n,
@@ -182,10 +159,17 @@ class InferenceManager
 
   /** Send inference
    *
-   * Makes the appropriate call to send inference based on the infer info
-   * data structure (see sendInference documentation above).
+   * This implements the above methods for the InferInfo object. It is called
+   * by the methods above.
+   *
+   * The inference info ii should have a rewritten conclusion and should not be
+   * trivial (InferInfo::isTrivial). It is the responsibility of the caller to
+   * ensure this.
+   *
+   * If the flag asLemma is true, then this method will send a lemma instead
+   * of a fact whenever applicable.
    */
-  void sendInference(const InferInfo& i);
+  void sendInference(const InferInfo& ii, bool asLemma = false);
   /** Send split
    *
    * This requests that ( a = b V a != b ) is sent on the output channel as a
@@ -205,7 +189,10 @@ class InferenceManager
    *
    * This method is called to indicate this class should send a phase
    * requirement request to the output channel for literal lit to be
-   * decided with polarity pol.
+   * decided with polarity pol. This requirement is processed at the same time
+   * lemmas are sent on the output channel of this class during this call to
+   * check. This means if the current lemmas of this class are abandoned (due
+   * to a conflict), the phase requirement is not processed.
    */
   void sendPhaseRequirement(Node lit, bool pol);
   /**
@@ -304,17 +291,6 @@ class InferenceManager
    * of atom, including calls to registerTerm.
    */
   void assertPendingFact(Node atom, bool polarity, Node exp);
-  /**
-   * Indicates that ant => conc should be sent on the output channel of this
-   * class. This will either trigger an immediate call to the conflict
-   * method of the output channel of this class of conc is false, or adds the
-   * above lemma to the lemma cache d_pending_lem, which may be flushed
-   * later within the current call to TheoryStrings::check.
-   *
-   * The argument infer identifies the reason for inference, used for
-   * debugging.
-   */
-  void sendLemma(Node ant, Node conc, Inference infer);
   /** Reference to the solver state of the theory of strings. */
   SolverState& d_state;
   /** Reference to the term registry of theory of strings */
@@ -335,11 +311,11 @@ class InferenceManager
    * The list of pending literals to assert to the equality engine along with
    * their explanation.
    */
-  std::vector<PendingInfer> d_pending;
+  std::vector<InferInfo> d_pending;
   /** A map from literals to their pending phase requirement */
   std::map<Node, bool> d_pendingReqPhase;
   /** A list of pending lemmas to be sent on the output channel. */
-  std::vector<Node> d_pendingLem;
+  std::vector<InferInfo> d_pendingLem;
   /**
    * The keep set of this class. This set is maintained to ensure that
    * facts and their explanations are ref-counted. Since facts and their