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

diff --git a/src/theory/strings/infer_info.h b/src/theory/strings/infer_info.h
index 7fce2eaf2..fca528d1b 100644
--- a/src/theory/strings/infer_info.h
+++ b/src/theory/strings/infer_info.h
@@ -328,19 +328,18 @@ enum LengthStatus
 };
 
 /**
- * This data structure encapsulates an inference for strings. This includes
- * the form of the inference, as well as the side effects it generates.
+ * 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
+ * equality engine or sent on the output channel.
  */
 class InferInfo
 {
  public:
   InferInfo();
-  /**
-   * The identifier for the inference, indicating the kind of reasoning used
-   * for this conclusion.
-   */
+  ~InferInfo() {}
+  /** The inference identifier */
   Inference d_id;
-  /** The conclusion of the inference */
+  /** The conclusion */
   Node d_conc;
   /**
    * The antecedant(s) of the inference, interpreted conjunctively. These are
@@ -359,32 +358,30 @@ class InferInfo
    * can be assumed for them.
    */
   std::map<LengthStatus, std::vector<Node> > d_new_skolem;
+  /**  Is this infer info trivial? True if d_conc is true. */
+  bool isTrivial() const;
   /**
-   * The pending phase requirements, see InferenceManager::sendPhaseRequirement.
-   */
-  std::map<Node, bool> d_pending_phase;
-  /**
-   * The index in the normal forms under which this inference is addressing.
-   * For example, if the inference is inferring x = y from |x|=|y| and
-   *   w ++ x ++ ... = w ++ y ++ ...
-   * then d_index is 1, since x and y are at index 1 in these concat terms.
+   * Does this infer info correspond to a conflict? True if d_conc is false
+   * and it has no new antecedants (d_antn).
    */
-  unsigned d_index;
+  bool isConflict() const;
   /**
-   * The normal form pair that is cached as a result of this inference.
-   */
-  Node d_nf_pair[2];
-  /** for debugging
-   *
-   * The base pair of strings d_i/d_j that led to the inference, and whether
-   * (d_rev) we were processing the normal forms of these strings in reverse
-   * direction.
+   * 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).
    */
-  Node d_i;
-  Node d_j;
-  bool d_rev;
+  bool isFact() const;
 };
 
+/**
+ * Writes an inference info to a stream.
+ *
+ * @param out The stream to write to
+ * @param ii The inference info to write to the stream
+ * @return The stream
+ */
+std::ostream& operator<<(std::ostream& out, const InferInfo& ii);
+
 }  // namespace strings
 }  // namespace theory
 }  // namespace CVC4