Track inference id for pending facts in strings (#4331)

This improves our tracking of pending inferences in strings so that we record pending inferences as a triple (id, fact, exp). This will ensure that proof steps can be constructed at the time we decide to process facts. It also inlines the sendInfer method into sendInference for simplicity.

This also improves the policy for reference counting facts and their explanations: we add them to d_keep when they are added to the equality engine. Previously, we were adding them when they were registered as pending. This means we would collect facts in this pending set that were added but later abandoned, which is unnecessary.

2 files changed, 84 insertions, 67 deletions

diff --git a/src/theory/strings/inference_manager.cpp b/src/theory/strings/inference_manager.cpp
index 9d1c6fac4..2a559faac 100644
--- a/src/theory/strings/inference_manager.cpp
+++ b/src/theory/strings/inference_manager.cpp
@@ -177,11 +177,48 @@ void InferenceManager::sendInference(const std::vector<Node>& exp,
       eq_exp = d_true;
     }
     sendLemma(eq_exp, eq, infer);
+    return;
   }
-  else
+  Node eqExp = utils::mkAnd(exp);
+  if (options::stringInferSym())
   {
-    sendInfer(utils::mkAnd(exp), eq, infer);
+    std::vector<Node> vars;
+    std::vector<Node> subs;
+    std::vector<Node> unproc;
+    d_termReg.inferSubstitutionProxyVars(eqExp, vars, subs, unproc);
+    if (unproc.empty())
+    {
+      Node eqs =
+          eq.substitute(vars.begin(), vars.end(), subs.begin(), subs.end());
+      if (Trace.isOn("strings-lemma-debug"))
+      {
+        Trace("strings-lemma-debug") << "Strings::Infer " << eq << " from "
+                                     << eqExp << " by " << infer << std::endl;
+        Trace("strings-lemma-debug")
+            << "Strings::Infer Alternate : " << eqs << std::endl;
+        for (unsigned i = 0, nvars = vars.size(); i < nvars; i++)
+        {
+          Trace("strings-lemma-debug")
+              << "  " << vars[i] << " -> " << subs[i] << std::endl;
+        }
+      }
+      sendLemma(d_true, eqs, infer);
+      return;
+    }
+    if (Trace.isOn("strings-lemma-debug"))
+    {
+      for (const Node& u : unproc)
+      {
+        Trace("strings-lemma-debug")
+            << "  non-trivial exp : " << u << std::endl;
+      }
+    }
   }
+  Trace("strings-lemma") << "Strings::Infer " << eq << " from " << eqExp
+                         << " by " << infer << std::endl;
+  Trace("strings-assert") << "(assert (=> " << eqExp << " " << eq
+                          << ")) ; infer " << infer << std::endl;
+  d_pending.push_back(PendingInfer(infer, eq, eqExp));
 }
 
 void InferenceManager::sendInference(const std::vector<Node>& exp,
@@ -229,51 +266,6 @@ void InferenceManager::sendLemma(Node ant, Node conc, Inference infer)
   d_pendingLem.push_back(lem);
 }
 
-void InferenceManager::sendInfer(Node eq_exp, Node eq, Inference infer)
-{
-  if (options::stringInferSym())
-  {
-    std::vector<Node> vars;
-    std::vector<Node> subs;
-    std::vector<Node> unproc;
-    d_termReg.inferSubstitutionProxyVars(eq_exp, vars, subs, unproc);
-    if (unproc.empty())
-    {
-      Node eqs =
-          eq.substitute(vars.begin(), vars.end(), subs.begin(), subs.end());
-      if (Trace.isOn("strings-lemma-debug"))
-      {
-        Trace("strings-lemma-debug") << "Strings::Infer " << eq << " from "
-                                     << eq_exp << " by " << infer << std::endl;
-        Trace("strings-lemma-debug")
-            << "Strings::Infer Alternate : " << eqs << std::endl;
-        for (unsigned i = 0, nvars = vars.size(); i < nvars; i++)
-        {
-          Trace("strings-lemma-debug")
-              << "  " << vars[i] << " -> " << subs[i] << std::endl;
-        }
-      }
-      sendLemma(d_true, eqs, infer);
-      return;
-    }
-    if (Trace.isOn("strings-lemma-debug"))
-    {
-      for (const Node& u : unproc)
-      {
-        Trace("strings-lemma-debug")
-            << "  non-trivial exp : " << u << std::endl;
-      }
-    }
-  }
-  Trace("strings-lemma") << "Strings::Infer " << eq << " from " << eq_exp
-                         << " by " << infer << std::endl;
-  Trace("strings-assert") << "(assert (=> " << eq_exp << " " << eq
-                          << ")) ; infer " << infer << std::endl;
-  d_pending.push_back(eq);
-  d_pendingExp[eq] = eq_exp;
-  d_keep.insert(eq);
-  d_keep.insert(eq_exp);
-}
 
 bool InferenceManager::sendSplit(Node a, Node b, Inference infer, bool preq)
 {
@@ -328,8 +320,8 @@ void InferenceManager::doPendingFacts()
   size_t i = 0;
   while (!d_state.isInConflict() && i < d_pending.size())
   {
-    Node fact = d_pending[i];
-    Node exp = d_pendingExp[fact];
+    Node fact = d_pending[i].d_fact;
+    Node exp = d_pending[i].d_exp;
     if (fact.getKind() == AND)
     {
       for (const Node& lit : fact)
@@ -345,10 +337,14 @@ void InferenceManager::doPendingFacts()
       TNode atom = polarity ? fact : fact[0];
       assertPendingFact(atom, polarity, exp);
     }
+    // Must reference count the equality and its explanation, which is not done
+    // by the equality engine. Notice that we do not need to do this for
+    // external assertions, which enter as facts through sendAssumption.
+    d_keep.insert(fact);
+    d_keep.insert(exp);
     i++;
   }
   d_pending.clear();
-  d_pendingExp.clear();
 }
 
 void InferenceManager::doPendingLemmas()
diff --git a/src/theory/strings/inference_manager.h b/src/theory/strings/inference_manager.h
index 041724d8d..6e11bf85e 100644
--- a/src/theory/strings/inference_manager.h
+++ b/src/theory/strings/inference_manager.h
@@ -35,6 +35,29 @@ 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
@@ -115,18 +138,22 @@ class InferenceManager
    * contains literals that are explainable, i.e. those that hold in the
    * 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 sendInfer or sendLemma. Overall,
-   * the result of this method is one of the following:
+   * theory of strings. This method may call sendLemma or otherwise add a
+   * PendingInfer to d_pending, indicating a fact should be asserted to the
+   * equality engine. Overall, the result of this method is one of the
+   * following:
    *
    * [1] (No-op) Do nothing if eq is true,
    *
    * [2] (Infer) Indicate that eq should be added to the equality engine of this
-   * class with explanation EXPLAIN(exp), where EXPLAIN returns the
-   * explanation of the node in exp in terms of the literals asserted to the
-   * theory of strings,
+   * class with explanation exp, where exp is a set of literals that currently
+   * hold in the equality engine. We add this to the pending vector d_pending.
    *
    * [3] (Lemma) Indicate that the lemma ( EXPLAIN(exp) ^ exp_n ) => eq should
-   * be sent on the output channel of the theory of strings, or
+   * be sent on the output channel of the theory of strings, where EXPLAIN
+   * returns the explanation of the node in exp in terms of the literals
+   * asserted to the theory of strings, as computed by the equality engine.
+   * This is also added to a pending vector, d_pendingLem.
    *
    * [4] (Conflict) Immediately report a conflict EXPLAIN(exp) on the output
    * channel of the theory of strings.
@@ -288,13 +315,6 @@ class InferenceManager
    * debugging.
    */
   void sendLemma(Node ant, Node conc, Inference infer);
-  /**
-   * Indicates that conc should be added to the equality engine of this class
-   * with explanation eq_exp. It must be the case that eq_exp is a (conjunction
-   * of) literals that each are explainable, i.e. they already hold in the
-   * equality engine of this class.
-   */
-  void sendInfer(Node eq_exp, Node eq, Inference infer);
   /** Reference to the solver state of the theory of strings. */
   SolverState& d_state;
   /** Reference to the term registry of theory of strings */
@@ -311,10 +331,11 @@ class InferenceManager
   Node d_false;
   Node d_zero;
   Node d_one;
-  /** The list of pending literals to assert to the equality engine */
-  std::vector<Node> d_pending;
-  /** A map from the literals in the above vector to their explanation */
-  std::map<Node, Node> d_pendingExp;
+  /**
+   * The list of pending literals to assert to the equality engine along with
+   * their explanation.
+   */
+  std::vector<PendingInfer> 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. */