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, 141 insertions, 138 deletions

diff --git a/src/theory/strings/inference_manager.cpp b/src/theory/strings/inference_manager.cpp
index 2a559faac..8e68913ac 100644
--- a/src/theory/strings/inference_manager.cpp
+++ b/src/theory/strings/inference_manager.cpp
@@ -117,83 +117,86 @@ bool InferenceManager::sendInternalInference(std::vector<Node>& exp,
 }
 
 void InferenceManager::sendInference(const std::vector<Node>& exp,
-                                     const std::vector<Node>& exp_n,
+                                     const std::vector<Node>& expn,
                                      Node eq,
                                      Inference infer,
                                      bool asLemma)
 {
   eq = eq.isNull() ? d_false : Rewriter::rewrite(eq);
-  if (Trace.isOn("strings-infer-debug"))
-  {
-    Trace("strings-infer-debug")
-        << "By " << infer << ", infer : " << eq << " from: " << std::endl;
-    for (unsigned i = 0; i < exp.size(); i++)
-    {
-      Trace("strings-infer-debug") << "  " << exp[i] << std::endl;
-    }
-    for (unsigned i = 0; i < exp_n.size(); i++)
-    {
-      Trace("strings-infer-debug") << "  N:" << exp_n[i] << std::endl;
-    }
-  }
   if (eq == d_true)
   {
     return;
   }
-  // only keep stats if not trivial conclusion
-  d_statistics.d_inferences << infer;
-  Node atom = eq.getKind() == NOT ? eq[0] : eq;
-  // check if we should send a lemma or an inference
-  if (asLemma || atom == d_false || atom.getKind() == OR || !exp_n.empty()
-      || options::stringInferAsLemmas())
+  // wrap in infer info and send below
+  InferInfo ii;
+  ii.d_id = infer;
+  ii.d_conc = eq;
+  ii.d_ant = exp;
+  ii.d_antn = expn;
+  sendInference(ii, asLemma);
+}
+
+void InferenceManager::sendInference(const std::vector<Node>& exp,
+                                     Node eq,
+                                     Inference infer,
+                                     bool asLemma)
+{
+  std::vector<Node> expn;
+  sendInference(exp, expn, eq, infer, asLemma);
+}
+
+void InferenceManager::sendInference(const InferInfo& ii, bool asLemma)
+{
+  Assert(!ii.isTrivial());
+  Trace("strings-infer-debug")
+      << "sendInference: " << ii << ", asLemma = " << asLemma << std::endl;
+  // check if we should send a conflict, lemma or a fact
+  if (asLemma || options::stringInferAsLemmas() || !ii.isFact())
   {
-    Node eq_exp;
-    if (options::stringRExplainLemmas())
+    if (ii.isConflict())
     {
-      eq_exp = mkExplain(exp, exp_n);
-    }
-    else
-    {
-      if (exp.empty())
-      {
-        eq_exp = utils::mkAnd(exp_n);
-      }
-      else if (exp_n.empty())
-      {
-        eq_exp = utils::mkAnd(exp);
-      }
-      else
-      {
-        std::vector<Node> ev;
-        ev.insert(ev.end(), exp.begin(), exp.end());
-        ev.insert(ev.end(), exp_n.begin(), exp_n.end());
-        eq_exp = NodeManager::currentNM()->mkNode(AND, ev);
-      }
-    }
-    // if we have unexplained literals, this lemma is not a conflict
-    if (eq == d_false && !exp_n.empty())
-    {
-      eq = eq_exp.negate();
-      eq_exp = d_true;
+      Trace("strings-infer-debug") << "...as conflict" << std::endl;
+      Trace("strings-lemma") << "Strings::Conflict: " << ii.d_ant << " by "
+                             << ii.d_id << std::endl;
+      Trace("strings-conflict") << "CONFLICT: inference conflict " << ii.d_ant
+                                << " by " << ii.d_id << std::endl;
+      // we must fully explain it
+      Node conf = mkExplain(ii.d_ant);
+      Trace("strings-assert") << "(assert (not " << conf << ")) ; conflict "
+                              << ii.d_id << std::endl;
+      ++(d_statistics.d_conflictsInfer);
+      // only keep stats if we process it here
+      d_statistics.d_inferences << ii.d_id;
+      d_out.conflict(conf);
+      d_state.setConflict();
+      return;
     }
-    sendLemma(eq_exp, eq, infer);
+    Trace("strings-infer-debug") << "...as lemma" << std::endl;
+    d_pendingLem.push_back(ii);
     return;
   }
-  Node eqExp = utils::mkAnd(exp);
   if (options::stringInferSym())
   {
     std::vector<Node> vars;
     std::vector<Node> subs;
     std::vector<Node> unproc;
-    d_termReg.inferSubstitutionProxyVars(eqExp, vars, subs, unproc);
+    for (const Node& ac : ii.d_ant)
+    {
+      d_termReg.inferSubstitutionProxyVars(ac, vars, subs, unproc);
+    }
     if (unproc.empty())
     {
-      Node eqs =
-          eq.substitute(vars.begin(), vars.end(), subs.begin(), subs.end());
+      Node eqs = ii.d_conc.substitute(
+          vars.begin(), vars.end(), subs.begin(), subs.end());
+      InferInfo iiSubsLem;
+      // keep the same id for now, since we are transforming the form of the
+      // inference, not the root reason.
+      iiSubsLem.d_id = ii.d_id;
+      iiSubsLem.d_conc = eqs;
       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 " << iiSubsLem << std::endl;
         Trace("strings-lemma-debug")
             << "Strings::Infer Alternate : " << eqs << std::endl;
         for (unsigned i = 0, nvars = vars.size(); i < nvars; i++)
@@ -202,7 +205,8 @@ void InferenceManager::sendInference(const std::vector<Node>& exp,
               << "  " << vars[i] << " -> " << subs[i] << std::endl;
         }
       }
-      sendLemma(d_true, eqs, infer);
+      Trace("strings-infer-debug") << "...as symbolic lemma" << std::endl;
+      d_pendingLem.push_back(iiSubsLem);
       return;
     }
     if (Trace.isOn("strings-lemma-debug"))
@@ -214,59 +218,11 @@ void InferenceManager::sendInference(const std::vector<Node>& exp,
       }
     }
   }
-  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,
-                                     Node eq,
-                                     Inference infer,
-                                     bool asLemma)
-{
-  std::vector<Node> exp_n;
-  sendInference(exp, exp_n, eq, infer, asLemma);
-}
-
-void InferenceManager::sendInference(const InferInfo& i)
-{
-  sendInference(i.d_ant, i.d_antn, i.d_conc, i.d_id, true);
-}
-
-void InferenceManager::sendLemma(Node ant, Node conc, Inference infer)
-{
-  if (conc.isNull() || conc == d_false)
-  {
-    Trace("strings-conflict")
-        << "Strings::Conflict : " << infer << " : " << ant << std::endl;
-    Trace("strings-lemma") << "Strings::Conflict : " << infer << " : " << ant
-                           << std::endl;
-    Trace("strings-assert")
-        << "(assert (not " << ant << ")) ; conflict " << infer << std::endl;
-    ++(d_statistics.d_conflictsInfer);
-    d_out.conflict(ant);
-    d_state.setConflict();
-    return;
-  }
-  Node lem;
-  if (ant == d_true)
-  {
-    lem = conc;
-  }
-  else
-  {
-    lem = NodeManager::currentNM()->mkNode(IMPLIES, ant, conc);
-  }
-  Trace("strings-lemma") << "Strings::Lemma " << infer << " : " << lem
-                         << std::endl;
-  Trace("strings-assert") << "(assert " << lem << ") ; lemma " << infer
-                          << std::endl;
-  d_pendingLem.push_back(lem);
+  Trace("strings-infer-debug") << "...as fact" << std::endl;
+  // add to pending, to be processed as a fact
+  d_pending.push_back(ii);
 }
 
-
 bool InferenceManager::sendSplit(Node a, Node b, Inference infer, bool preq)
 {
   Node eq = a.eqNode(b);
@@ -275,14 +231,12 @@ bool InferenceManager::sendSplit(Node a, Node b, Inference infer, bool preq)
   {
     return false;
   }
-  // update statistics
-  d_statistics.d_inferences << infer;
   NodeManager* nm = NodeManager::currentNM();
-  Node lemma_or = nm->mkNode(OR, eq, nm->mkNode(NOT, eq));
-  Trace("strings-lemma") << "Strings::Lemma " << infer
-                         << " SPLIT : " << lemma_or << std::endl;
-  d_pendingLem.push_back(lemma_or);
+  InferInfo iiSplit;
+  iiSplit.d_id = infer;
+  iiSplit.d_conc = nm->mkNode(OR, eq, nm->mkNode(NOT, eq));
   sendPhaseRequirement(eq, preq);
+  d_pendingLem.push_back(iiSplit);
   return true;
 }
 
@@ -320,23 +274,25 @@ void InferenceManager::doPendingFacts()
   size_t i = 0;
   while (!d_state.isInConflict() && i < d_pending.size())
   {
-    Node fact = d_pending[i].d_fact;
-    Node exp = d_pending[i].d_exp;
-    if (fact.getKind() == AND)
-    {
-      for (const Node& lit : fact)
-      {
-        bool polarity = lit.getKind() != NOT;
-        TNode atom = polarity ? lit : lit[0];
-        assertPendingFact(atom, polarity, exp);
-      }
-    }
-    else
-    {
-      bool polarity = fact.getKind() != NOT;
-      TNode atom = polarity ? fact : fact[0];
-      assertPendingFact(atom, polarity, exp);
-    }
+    InferInfo& ii = d_pending[i];
+    // At this point, ii should be a "fact", i.e. something whose conclusion
+    // should be added as a normal equality or predicate to the equality engine
+    // with no new external assumptions (ii.d_antn).
+    Assert(ii.isFact());
+    Node fact = ii.d_conc;
+    Node exp = utils::mkAnd(ii.d_ant);
+    Trace("strings-assert") << "(assert (=> " << exp << " " << fact
+                            << ")) ; fact " << ii.d_id << std::endl;
+    // only keep stats if we process it here
+    Trace("strings-lemma") << "Strings::Fact: " << fact << " from " << exp
+                           << " by " << ii.d_id << std::endl;
+    d_statistics.d_inferences << ii.d_id;
+    // assert it as a pending fact
+    bool polarity = fact.getKind() != NOT;
+    TNode atom = polarity ? fact : fact[0];
+    // no double negation or double (conjunctive) conclusions
+    Assert(atom.getKind() != NOT && atom.getKind() != AND);
+    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.
@@ -349,21 +305,68 @@ void InferenceManager::doPendingFacts()
 
 void InferenceManager::doPendingLemmas()
 {
-  if (!d_state.isInConflict())
+  if (d_state.isInConflict())
+  {
+    // just clear the pending vectors, nothing else to do
+    d_pendingLem.clear();
+    d_pendingReqPhase.clear();
+    return;
+  }
+  NodeManager* nm = NodeManager::currentNM();
+  for (unsigned i = 0, psize = d_pendingLem.size(); i < psize; i++)
   {
-    for (const Node& lc : d_pendingLem)
+    InferInfo& ii = d_pendingLem[i];
+    Assert(!ii.isTrivial());
+    Assert(!ii.isConflict());
+    // get the explanation
+    Node eqExp;
+    if (options::stringRExplainLemmas())
+    {
+      eqExp = mkExplain(ii.d_ant, ii.d_antn);
+    }
+    else
+    {
+      std::vector<Node> ev;
+      ev.insert(ev.end(), ii.d_ant.begin(), ii.d_ant.end());
+      ev.insert(ev.end(), ii.d_antn.begin(), ii.d_antn.end());
+      eqExp = utils::mkAnd(ev);
+    }
+    // make the lemma node
+    Node lem = ii.d_conc;
+    if (eqExp != d_true)
     {
-      Trace("strings-pending") << "Process pending lemma : " << lc << std::endl;
-      ++(d_statistics.d_lemmasInfer);
-      d_out.lemma(lc);
+      lem = nm->mkNode(IMPLIES, eqExp, lem);
     }
-    for (const std::pair<const Node, bool>& prp : d_pendingReqPhase)
+    Trace("strings-pending") << "Process pending lemma : " << lem << std::endl;
+    Trace("strings-assert")
+        << "(assert " << lem << ") ; lemma " << ii.d_id << std::endl;
+    Trace("strings-lemma") << "Strings::Lemma: " << lem << " by " << ii.d_id
+                           << std::endl;
+    // only keep stats if we process it here
+    d_statistics.d_inferences << ii.d_id;
+    ++(d_statistics.d_lemmasInfer);
+    d_out.lemma(lem);
+
+    // Process the side effects of the inference info.
+    // Register the new skolems from this inference. We register them here
+    // (lazily), since this is the moment when we have decided to process the
+    // inference.
+    for (const std::pair<const LengthStatus, std::vector<Node> >& sks :
+         ii.d_new_skolem)
     {
-      Trace("strings-pending") << "Require phase : " << prp.first
-                               << ", polarity = " << prp.second << std::endl;
-      d_out.requirePhase(prp.first, prp.second);
+      for (const Node& n : sks.second)
+      {
+        d_termReg.registerTermAtomic(n, sks.first);
+      }
     }
   }
+  // process the pending require phase calls
+  for (const std::pair<const Node, bool>& prp : d_pendingReqPhase)
+  {
+    Trace("strings-pending") << "Require phase : " << prp.first
+                             << ", polarity = " << prp.second << std::endl;
+    d_out.requirePhase(prp.first, prp.second);
+  }
   d_pendingLem.clear();
   d_pendingReqPhase.clear();
 }