(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.

10 files changed, 316 insertions, 368 deletions

diff --git a/src/theory/strings/core_solver.cpp b/src/theory/strings/core_solver.cpp
index ef3b978ef..edd00c954 100644
--- a/src/theory/strings/core_solver.cpp
+++ b/src/theory/strings/core_solver.cpp
@@ -2577,7 +2577,8 @@ bool CoreSolver::processInferInfo(CoreInferInfo& cii)
   // send phase requirements
   for (const std::pair<const Node, bool> pp : cii.d_pendingPhase)
   {
-    d_im.sendPhaseRequirement(pp.first, pp.second);
+    Node ppr = Rewriter::rewrite(pp.first);
+    d_im.addPendingPhaseRequirement(ppr, pp.second);
   }
 
   // send the inference, which is a lemma
diff --git a/src/theory/strings/infer_info.cpp b/src/theory/strings/infer_info.cpp
index c4514a33b..0d2f94f91 100644
--- a/src/theory/strings/infer_info.cpp
+++ b/src/theory/strings/infer_info.cpp
@@ -14,6 +14,7 @@
 
 #include "theory/strings/infer_info.h"
 
+#include "theory/strings/inference_manager.h"
 #include "theory/strings/theory_strings_utils.h"
 
 namespace CVC4 {
@@ -98,7 +99,18 @@ std::ostream& operator<<(std::ostream& out, Inference i)
   return out;
 }
 
-InferInfo::InferInfo() : d_id(Inference::NONE), d_idRev(false) {}
+InferInfo::InferInfo() : d_sim(nullptr), d_id(Inference::NONE), d_idRev(false)
+{
+}
+
+bool InferInfo::process(TheoryInferenceManager* im, bool asLemma)
+{
+  if (asLemma)
+  {
+    return d_sim->processLemma(*this);
+  }
+  return d_sim->processFact(*this);
+}
 
 bool InferInfo::isTrivial() const
 {
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 */
diff --git a/src/theory/strings/inference_manager.cpp b/src/theory/strings/inference_manager.cpp
index a465916e4..e324689f5 100644
--- a/src/theory/strings/inference_manager.cpp
+++ b/src/theory/strings/inference_manager.cpp
@@ -34,11 +34,13 @@ InferenceManager::InferenceManager(Theory& t,
                                    ExtTheory& e,
                                    SequencesStatistics& statistics,
                                    ProofNodeManager* pnm)
-    : TheoryInferenceManager(t, s, pnm),
+    : InferenceManagerBuffered(t, s, pnm),
       d_state(s),
       d_termReg(tr),
       d_extt(e),
-      d_statistics(statistics)
+      d_statistics(statistics),
+      d_ipc(pnm ? new InferProofCons(d_state.getSatContext(), pnm, d_statistics)
+                : nullptr)
 {
   NodeManager* nm = NodeManager::currentNM();
   d_zero = nm->mkConst(Rational(0));
@@ -47,6 +49,20 @@ InferenceManager::InferenceManager(Theory& t,
   d_false = nm->mkConst(false);
 }
 
+void InferenceManager::doPending()
+{
+  doPendingFacts();
+  if (d_state.isInConflict())
+  {
+    // just clear the pending vectors, nothing else to do
+    clearPendingLemmas();
+    clearPendingPhaseRequirements();
+    return;
+  }
+  doPendingLemmas();
+  doPendingPhaseRequirements();
+}
+
 bool InferenceManager::sendInternalInference(std::vector<Node>& exp,
                                              Node conc,
                                              Inference infer)
@@ -106,17 +122,21 @@ bool InferenceManager::sendInternalInference(std::vector<Node>& exp,
   return true;
 }
 
-void InferenceManager::sendInference(const std::vector<Node>& exp,
+bool InferenceManager::sendInference(const std::vector<Node>& exp,
                                      const std::vector<Node>& noExplain,
                                      Node eq,
                                      Inference infer,
                                      bool isRev,
                                      bool asLemma)
 {
-  eq = eq.isNull() ? d_false : Rewriter::rewrite(eq);
-  if (eq == d_true)
+  if (eq.isNull())
   {
-    return;
+    eq = d_false;
+  }
+  else if (Rewriter::rewrite(eq) == d_true)
+  {
+    // if trivial, return
+    return false;
   }
   // wrap in infer info and send below
   InferInfo ii;
@@ -126,46 +146,43 @@ void InferenceManager::sendInference(const std::vector<Node>& exp,
   ii.d_ant = exp;
   ii.d_noExplain = noExplain;
   sendInference(ii, asLemma);
+  return true;
 }
 
-void InferenceManager::sendInference(const std::vector<Node>& exp,
+bool InferenceManager::sendInference(const std::vector<Node>& exp,
                                      Node eq,
                                      Inference infer,
                                      bool isRev,
                                      bool asLemma)
 {
   std::vector<Node> noExplain;
-  sendInference(exp, noExplain, eq, infer, isRev, asLemma);
+  return sendInference(exp, noExplain, eq, infer, isRev, asLemma);
 }
 
-void InferenceManager::sendInference(const InferInfo& ii, bool asLemma)
+void InferenceManager::sendInference(InferInfo& ii, bool asLemma)
 {
   Assert(!ii.isTrivial());
+  // set that this inference manager will be processing this inference
+  ii.d_sim = this;
   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())
+  if (ii.isConflict())
+  {
+    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;
+    ++(d_statistics.d_conflictsInfer);
+    // process the conflict immediately
+    processConflict(ii);
+    return;
+  }
+  else if (asLemma || options::stringInferAsLemmas() || !ii.isFact())
   {
-    if (ii.isConflict())
-    {
-      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.notifyInConflict();
-      return;
-    }
     Trace("strings-infer-debug") << "...as lemma" << std::endl;
-    d_pendingLem.push_back(ii);
+    addPendingLemma(std::unique_ptr<InferInfo>(new InferInfo(ii)));
     return;
   }
   if (options::stringInferSym())
@@ -182,6 +199,7 @@ void InferenceManager::sendInference(const InferInfo& ii, bool asLemma)
       Node eqs = ii.d_conc.substitute(
           vars.begin(), vars.end(), subs.begin(), subs.end());
       InferInfo iiSubsLem;
+      iiSubsLem.d_sim = this;
       // 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;
@@ -199,7 +217,7 @@ void InferenceManager::sendInference(const InferInfo& ii, bool asLemma)
         }
       }
       Trace("strings-infer-debug") << "...as symbolic lemma" << std::endl;
-      d_pendingLem.push_back(iiSubsLem);
+      addPendingLemma(std::unique_ptr<InferInfo>(new InferInfo(iiSubsLem)));
       return;
     }
     if (Trace.isOn("strings-lemma-debug"))
@@ -207,13 +225,13 @@ void InferenceManager::sendInference(const InferInfo& ii, bool asLemma)
       for (const Node& u : unproc)
       {
         Trace("strings-lemma-debug")
-            << "  non-trivial exp : " << u << std::endl;
+            << "  non-trivial explanation : " << u << std::endl;
       }
     }
   }
   Trace("strings-infer-debug") << "...as fact" << std::endl;
-  // add to pending, to be processed as a fact
-  d_pending.push_back(ii);
+  // add to pending to be processed as a fact
+  addPendingFact(std::unique_ptr<InferInfo>(new InferInfo(ii)));
 }
 
 bool InferenceManager::sendSplit(Node a, Node b, Inference infer, bool preq)
@@ -226,19 +244,15 @@ bool InferenceManager::sendSplit(Node a, Node b, Inference infer, bool preq)
   }
   NodeManager* nm = NodeManager::currentNM();
   InferInfo iiSplit;
+  iiSplit.d_sim = this;
   iiSplit.d_id = infer;
   iiSplit.d_conc = nm->mkNode(OR, eq, nm->mkNode(NOT, eq));
-  sendPhaseRequirement(eq, preq);
-  d_pendingLem.push_back(iiSplit);
+  eq = Rewriter::rewrite(eq);
+  addPendingPhaseRequirement(eq, preq);
+  addPendingLemma(std::unique_ptr<InferInfo>(new InferInfo(iiSplit)));
   return true;
 }
 
-void InferenceManager::sendPhaseRequirement(Node lit, bool pol)
-{
-  lit = Rewriter::rewrite(lit);
-  d_pendingReqPhase[lit] = pol;
-}
-
 void InferenceManager::setIncomplete() { d_out.setIncomplete(); }
 
 void InferenceManager::addToExplanation(Node a,
@@ -258,239 +272,167 @@ void InferenceManager::addToExplanation(Node lit, std::vector<Node>& exp) const
 {
   if (!lit.isNull())
   {
+    Assert(!lit.isConst());
     exp.push_back(lit);
   }
 }
 
-void InferenceManager::doPendingFacts()
+bool InferenceManager::hasProcessed() const
 {
-  size_t i = 0;
-  while (!d_state.isInConflict() && i < d_pending.size())
-  {
-    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_noExplain).
-    Assert(ii.isFact());
-    Node facts = ii.d_conc;
-    Node exp = utils::mkAnd(ii.d_ant);
-    Trace("strings-assert") << "(assert (=> " << exp << " " << facts
-                            << ")) ; fact " << ii.d_id << std::endl;
-    // only keep stats if we process it here
-    Trace("strings-lemma") << "Strings::Fact: " << facts << " from " << exp
-                           << " by " << ii.d_id << std::endl;
-    d_statistics.d_inferences << ii.d_id;
-    // assert it as a pending fact
-    if (facts.getKind() == AND)
-    {
-      for (const Node& fact : facts)
-      {
-        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);
-        assertInternalFact(atom, polarity, exp);
-      }
-    }
-    else
-    {
-      bool polarity = facts.getKind() != NOT;
-      TNode atom = polarity ? facts : facts[0];
-      // no double negation or double (conjunctive) conclusions
-      Assert(atom.getKind() != NOT && atom.getKind() != AND);
-      assertInternalFact(atom, polarity, exp);
-    }
-    i++;
-  }
-  d_pending.clear();
+  return d_state.isInConflict() || hasPending();
 }
 
-void InferenceManager::doPendingLemmas()
+void InferenceManager::markCongruent(Node a, Node b)
 {
-  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++)
-  {
-    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_noExplain);
-    }
-    else
-    {
-      std::vector<Node> ev;
-      ev.insert(ev.end(), ii.d_ant.begin(), ii.d_ant.end());
-      eqExp = utils::mkAnd(ev);
-    }
-    // make the lemma node
-    Node lem = ii.d_conc;
-    if (eqExp != d_true)
-    {
-      lem = nm->mkNode(IMPLIES, eqExp, lem);
-    }
-    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);
-
-    // 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)
-    {
-      for (const Node& n : sks.second)
-      {
-        d_termReg.registerTermAtomic(n, sks.first);
-      }
-    }
-    LemmaProperty p = LemmaProperty::NONE;
-    if (ii.d_id == Inference::REDUCTION)
-    {
-      p |= LemmaProperty::NEEDS_JUSTIFY;
-    }
-    d_out.lemma(lem, p);
-  }
-  // process the pending require phase calls
-  for (const std::pair<const Node, bool>& prp : d_pendingReqPhase)
+  Assert(a.getKind() == b.getKind());
+  if (d_extt.hasFunctionKind(a.getKind()))
   {
-    Trace("strings-pending") << "Require phase : " << prp.first
-                             << ", polarity = " << prp.second << std::endl;
-    d_out.requirePhase(prp.first, prp.second);
+    d_extt.markCongruent(a, b);
   }
-  d_pendingLem.clear();
-  d_pendingReqPhase.clear();
 }
 
-bool InferenceManager::hasProcessed() const
+void InferenceManager::markReduced(Node n, bool contextDepend)
 {
-  return d_state.isInConflict() || !d_pendingLem.empty() || !d_pending.empty();
+  d_extt.markReduced(n, contextDepend);
 }
 
-Node InferenceManager::mkExplain(const std::vector<Node>& a) const
+void InferenceManager::processConflict(const InferInfo& ii)
 {
-  std::vector<Node> noExplain;
-  return mkExplain(a, noExplain);
+  Assert(!d_state.isInConflict());
+  // setup the fact to reproduce the proof in the call below
+  d_statistics.d_inferences << ii.d_id;
+  if (d_ipc != nullptr)
+  {
+    d_ipc->notifyFact(ii);
+  }
+  // make the trust node
+  TrustNode tconf = mkConflictExp(ii.d_ant, d_ipc.get());
+  Assert(tconf.getKind() == TrustNodeKind::CONFLICT);
+  Trace("strings-assert") << "(assert (not " << tconf.getNode()
+                          << ")) ; conflict " << ii.d_id << std::endl;
+  // send the trusted conflict
+  trustedConflict(tconf);
 }
 
-Node InferenceManager::mkExplain(const std::vector<Node>& a,
-                                 const std::vector<Node>& noExplain) const
+bool InferenceManager::processFact(InferInfo& ii)
 {
-  std::vector<TNode> antec_exp;
-  // copy to processing vector
-  std::vector<Node> aconj;
-  for (const Node& ac : a)
-  {
-    utils::flattenOp(AND, ac, aconj);
-  }
-  for (const Node& apc : aconj)
+  // Get the fact(s). There are multiple facts if the conclusion is an AND
+  std::vector<Node> facts;
+  if (ii.d_conc.getKind() == AND)
   {
-    if (std::find(noExplain.begin(), noExplain.end(), apc) != noExplain.end())
+    for (const Node& cc : ii.d_conc)
     {
-      if (std::find(antec_exp.begin(), antec_exp.end(), apc) == antec_exp.end())
-      {
-        Debug("strings-explain")
-            << "Add to explanation (new literal) " << apc << std::endl;
-        antec_exp.push_back(apc);
-      }
-      continue;
+      facts.push_back(cc);
     }
-    Assert(apc.getKind() != AND);
-    Debug("strings-explain") << "Add to explanation " << apc << std::endl;
-    if (apc.getKind() == NOT && apc[0].getKind() == EQUAL)
-    {
-      Assert(d_ee->hasTerm(apc[0][0]));
-      Assert(d_ee->hasTerm(apc[0][1]));
-      // ensure that we are ready to explain the disequality
-      AlwaysAssert(d_ee->areDisequal(apc[0][0], apc[0][1], true));
-    }
-    Assert(apc.getKind() != EQUAL || d_ee->areEqual(apc[0], apc[1]));
-    // now, explain
-    explain(apc, antec_exp);
   }
-  Node ant;
-  if (antec_exp.empty())
+  else
   {
-    ant = d_true;
+    facts.push_back(ii.d_conc);
   }
-  else if (antec_exp.size() == 1)
+  Trace("strings-assert") << "(assert (=> " << ii.getAntecedant() << " "
+                          << ii.d_conc << ")) ; fact " << ii.d_id << std::endl;
+  Trace("strings-lemma") << "Strings::Fact: " << ii.d_conc << " from "
+                         << ii.getAntecedant() << " by " << ii.d_id
+                         << std::endl;
+  std::vector<Node> exp;
+  for (const Node& ec : ii.d_ant)
   {
-    ant = antec_exp[0];
+    utils::flattenOp(AND, ec, exp);
   }
-  else
+  bool ret = false;
+  // convert for each fact
+  for (const Node& fact : facts)
   {
-    ant = NodeManager::currentNM()->mkNode(AND, antec_exp);
+    ii.d_conc = fact;
+    d_statistics.d_inferences << ii.d_id;
+    bool polarity = fact.getKind() != NOT;
+    TNode atom = polarity ? fact : fact[0];
+    bool curRet = false;
+    if (d_ipc != nullptr)
+    {
+      // ensure the proof generator is ready to explain this fact in the
+      // current SAT context
+      d_ipc->notifyFact(ii);
+      // now, assert the internal fact with d_ipc as proof generator
+      curRet = assertInternalFact(atom, polarity, exp, d_ipc.get());
+    }
+    else
+    {
+      Node cexp = utils::mkAnd(exp);
+      // without proof generator
+      curRet = assertInternalFact(atom, polarity, cexp);
+    }
+    ret = ret || curRet;
+    // may be in conflict
+    if (d_state.isInConflict())
+    {
+      break;
+    }
   }
-  return ant;
+  return ret;
 }
 
-void InferenceManager::explain(TNode literal,
-                               std::vector<TNode>& assumptions) const
+bool InferenceManager::processLemma(InferInfo& ii)
 {
-  Debug("strings-explain") << "Explain " << literal << " "
-                           << d_state.isInConflict() << std::endl;
-  bool polarity = literal.getKind() != NOT;
-  TNode atom = polarity ? literal : literal[0];
-  std::vector<TNode> tassumptions;
-  if (atom.getKind() == EQUAL)
+  Assert(!ii.isTrivial());
+  Assert(!ii.isConflict());
+  // set up the explanation and no-explanation
+  std::vector<Node> exp;
+  for (const Node& ec : ii.d_ant)
   {
-    if (atom[0] != atom[1])
-    {
-      Assert(d_ee->hasTerm(atom[0]));
-      Assert(d_ee->hasTerm(atom[1]));
-      d_ee->explainEquality(atom[0], atom[1], polarity, tassumptions);
-    }
+    utils::flattenOp(AND, ec, exp);
   }
-  else
+  std::vector<Node> noExplain;
+  if (!options::stringRExplainLemmas())
   {
-    d_ee->explainPredicate(atom, polarity, tassumptions);
+    // if we aren't regressing the explanation, we add all literals to
+    // noExplain and ignore ii.d_ant.
+    noExplain.insert(noExplain.end(), exp.begin(), exp.end());
   }
-  for (const TNode a : tassumptions)
+  else
   {
-    if (std::find(assumptions.begin(), assumptions.end(), a)
-        == assumptions.end())
+    // otherwise, the no-explain literals are those provided
+    for (const Node& ecn : ii.d_noExplain)
     {
-      assumptions.push_back(a);
+      utils::flattenOp(AND, ecn, noExplain);
     }
   }
-  if (Debug.isOn("strings-explain-debug"))
+  // ensure that the proof generator is ready to explain the final conclusion
+  // of the lemma (ii.d_conc).
+  d_statistics.d_inferences << ii.d_id;
+  if (d_ipc != nullptr)
+  {
+    d_ipc->notifyFact(ii);
+  }
+  TrustNode tlem = mkLemmaExp(ii.d_conc, exp, noExplain, d_ipc.get());
+  Trace("strings-pending") << "Process pending lemma : " << tlem.getNode()
+                           << std::endl;
+
+  // 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)
   {
-    Debug("strings-explain-debug")
-        << "Explanation for " << literal << " was " << std::endl;
-    for (const TNode a : tassumptions)
+    for (const Node& n : sks.second)
     {
-      Debug("strings-explain-debug") << "   " << a << std::endl;
+      d_termReg.registerTermAtomic(n, sks.first);
     }
   }
-}
-
-void InferenceManager::markCongruent(Node a, Node b)
-{
-  Assert(a.getKind() == b.getKind());
-  if (d_extt.hasFunctionKind(a.getKind()))
+  LemmaProperty p = LemmaProperty::NONE;
+  if (ii.d_id == Inference::REDUCTION)
   {
-    d_extt.markCongruent(a, b);
+    p |= LemmaProperty::NEEDS_JUSTIFY;
   }
-}
+  Trace("strings-assert") << "(assert " << tlem.getNode() << ") ; lemma "
+                          << ii.d_id << std::endl;
+  Trace("strings-lemma") << "Strings::Lemma: " << tlem.getNode() << " by "
+                         << ii.d_id << std::endl;
+  ++(d_statistics.d_lemmasInfer);
 
-void InferenceManager::markReduced(Node n, bool contextDepend)
-{
-  d_extt.markReduced(n, contextDepend);
+  // call the trusted lemma, without caching
+  return trustedLemma(tlem, p, false);
 }
 
 }  // namespace strings
diff --git a/src/theory/strings/inference_manager.h b/src/theory/strings/inference_manager.h
index 9abc776e6..3280281bd 100644
--- a/src/theory/strings/inference_manager.h
+++ b/src/theory/strings/inference_manager.h
@@ -23,9 +23,12 @@
 #include "context/cdhashset.h"
 #include "context/context.h"
 #include "expr/node.h"
+#include "expr/proof_node_manager.h"
 #include "theory/ext_theory.h"
+#include "theory/inference_manager_buffered.h"
 #include "theory/output_channel.h"
 #include "theory/strings/infer_info.h"
+#include "theory/strings/infer_proof_cons.h"
 #include "theory/strings/sequences_stats.h"
 #include "theory/strings/solver_state.h"
 #include "theory/strings/term_registry.h"
@@ -66,10 +69,11 @@ namespace strings {
  * theory of strings, e.g. sendPhaseRequirement, setIncomplete, and
  * with the extended theory object e.g. markCongruent.
  */
-class InferenceManager : public TheoryInferenceManager
+class InferenceManager : public InferenceManagerBuffered
 {
   typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
   typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap;
+  friend class InferInfo;
 
  public:
   InferenceManager(Theory& t,
@@ -80,6 +84,15 @@ class InferenceManager : public TheoryInferenceManager
                    ProofNodeManager* pnm);
   ~InferenceManager() {}
 
+  /**
+   * Do pending method. This processes all pending facts, lemmas and pending
+   * phase requests based on the policy of this manager. This means that
+   * we process the pending facts first and abort if in conflict. Otherwise, we
+   * process the pending lemmas and then the pending phase requirements.
+   * Notice that we process the pending lemmas even if there were facts.
+   */
+  void doPending();
+
   /** send internal inferences
    *
    * This is called when we have inferred exp => conc, where exp is a set
@@ -145,15 +158,17 @@ class InferenceManager : public TheoryInferenceManager
    * is used as a hint for proof reconstruction.
    * @param asLemma If true, then this method will send a lemma instead
    * of a fact whenever applicable.
+   * @return true if the inference was not trivial (e.g. its conclusion did
+   * not rewrite to true).
    */
-  void sendInference(const std::vector<Node>& exp,
+  bool sendInference(const std::vector<Node>& exp,
                      const std::vector<Node>& noExplain,
                      Node eq,
                      Inference infer,
                      bool isRev = false,
                      bool asLemma = false);
   /** same as above, but where noExplain is empty */
-  void sendInference(const std::vector<Node>& exp,
+  bool sendInference(const std::vector<Node>& exp,
                      Node eq,
                      Inference infer,
                      bool isRev = false,
@@ -171,7 +186,7 @@ class InferenceManager : public TheoryInferenceManager
    * If the flag asLemma is true, then this method will send a lemma instead
    * of a fact whenever applicable.
    */
-  void sendInference(const InferInfo& ii, bool asLemma = false);
+  void sendInference(InferInfo& ii, bool asLemma = false);
   /** Send split
    *
    * This requests that ( a = b V a != b ) is sent on the output channel as a
@@ -186,17 +201,6 @@ class InferenceManager : public TheoryInferenceManager
    * otherwise. A split is trivial if a=b rewrites to a constant.
    */
   bool sendSplit(Node a, Node b, Inference infer, bool preq = true);
-
-  /** Send phase requirement
-   *
-   * 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. 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);
   /**
    * Set that we are incomplete for the current set of assertions (in other
    * words, we must answer "unknown" instead of "sat"); this calls the output
@@ -213,61 +217,13 @@ class InferenceManager : public TheoryInferenceManager
   /** Adds lit to the vector exp if it is non-null */
   void addToExplanation(Node lit, std::vector<Node>& exp) const;
   //----------------------------end constructing antecedants
-  /** Do pending facts
-   *
-   * This method asserts pending facts (d_pending) with explanations
-   * (d_pendingExp) to the equality engine of the theory of strings via calls
-   * to assertPendingFact.
-   *
-   * It terminates early if a conflict is encountered, for instance, by
-   * equality reasoning within the equality engine.
-   *
-   * Regardless of whether a conflict is encountered, the vector d_pending
-   * and map d_pendingExp are cleared.
-   */
-  void doPendingFacts();
-  /** Do pending lemmas
-   *
-   * This method flushes all pending lemmas (d_pending_lem) to the output
-   * channel of theory of strings.
-   *
-   * Like doPendingFacts, this function will terminate early if a conflict
-   * has already been encountered by the theory of strings. The vector
-   * d_pending_lem is cleared regardless of whether a conflict is discovered.
-   *
-   * Notice that as a result of the above design, some lemmas may be "dropped"
-   * if a conflict is discovered in between when a lemma is added to the
-   * pending vector of this class (via a sendInference call). Lemmas
-   * e.g. those that are required for initialization should not be sent via
-   * this class, since they should never be dropped.
-   */
-  void doPendingLemmas();
   /**
    * Have we processed an inference during this call to check? In particular,
    * this returns true if we have a pending fact or lemma, or have encountered
    * a conflict.
    */
   bool hasProcessed() const;
-  /** Do we have a pending fact to add to the equality engine? */
-  bool hasPendingFact() const { return !d_pending.empty(); }
-  /** Do we have a pending lemma to send on the output channel? */
-  bool hasPendingLemma() const { return !d_pendingLem.empty(); }
 
-  /** make explanation
-   *
-   * This returns a node corresponding to the explanation of formulas in a,
-   * interpreted conjunctively. The returned node is a conjunction of literals
-   * that have been asserted to the equality engine.
-   */
-  Node mkExplain(const std::vector<Node>& a) const;
-  /** Same as above, but with a subset noExplain that should not be explained */
-  Node mkExplain(const std::vector<Node>& a,
-                 const std::vector<Node>& noExplain) const;
-  /**
-   * Explain literal l, add conjuncts to assumptions vector instead of making
-   * the node corresponding to their conjunction.
-   */
-  void explain(TNode literal, std::vector<TNode>& assumptions) const;
   // ------------------------------------------------- extended theory
   /**
    * Mark that terms a and b are congruent in the current context.
@@ -284,7 +240,18 @@ class InferenceManager : public TheoryInferenceManager
   void markReduced(Node n, bool contextDepend = true);
   // ------------------------------------------------- end extended theory
 
+  /**
+   * Called when ii is ready to be processed as a conflict. This makes a
+   * trusted node whose generator is the underlying proof equality engine
+   * (if it exists), and sends it on the output channel.
+   */
+  void processConflict(const InferInfo& ii);
+
  private:
+  /** Called when ii is ready to be processed as a fact */
+  bool processFact(InferInfo& ii);
+  /** Called when ii is ready to be processed as a lemma */
+  bool processLemma(InferInfo& ii);
   /** Reference to the solver state of the theory of strings. */
   SolverState& d_state;
   /** Reference to the term registry of theory of strings */
@@ -293,21 +260,13 @@ class InferenceManager : public TheoryInferenceManager
   ExtTheory& d_extt;
   /** Reference to the statistics for the theory of strings/sequences. */
   SequencesStatistics& d_statistics;
-
+  /** Conversion from inferences to proofs */
+  std::unique_ptr<InferProofCons> d_ipc;
   /** Common constants */
   Node d_true;
   Node d_false;
   Node d_zero;
   Node d_one;
-  /**
-   * The list of pending literals to assert to the equality engine along with
-   * their explanation.
-   */
-  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<InferInfo> d_pendingLem;
 };
 
 }  // namespace strings
diff --git a/src/theory/strings/sequences_stats.cpp b/src/theory/strings/sequences_stats.cpp
index 80221cbcc..fe6bc548e 100644
--- a/src/theory/strings/sequences_stats.cpp
+++ b/src/theory/strings/sequences_stats.cpp
@@ -32,7 +32,7 @@ SequencesStatistics::SequencesStatistics()
       d_regexpUnfoldingsNeg("theory::strings::regexpUnfoldingsNeg"),
       d_rewrites("theory::strings::rewrites"),
       d_conflictsEqEngine("theory::strings::conflictsEqEngine", 0),
-      d_conflictsEagerPrefix("theory::strings::conflictsEagerPrefix", 0),
+      d_conflictsEager("theory::strings::conflictsEager", 0),
       d_conflictsInfer("theory::strings::conflictsInfer", 0),
       d_lemmasEagerPreproc("theory::strings::lemmasEagerPreproc", 0),
       d_lemmasCmiSplit("theory::strings::lemmasCmiSplit", 0),
@@ -51,7 +51,7 @@ SequencesStatistics::SequencesStatistics()
   smtStatisticsRegistry()->registerStat(&d_regexpUnfoldingsNeg);
   smtStatisticsRegistry()->registerStat(&d_rewrites);
   smtStatisticsRegistry()->registerStat(&d_conflictsEqEngine);
-  smtStatisticsRegistry()->registerStat(&d_conflictsEagerPrefix);
+  smtStatisticsRegistry()->registerStat(&d_conflictsEager);
   smtStatisticsRegistry()->registerStat(&d_conflictsInfer);
   smtStatisticsRegistry()->registerStat(&d_lemmasEagerPreproc);
   smtStatisticsRegistry()->registerStat(&d_lemmasCmiSplit);
@@ -72,7 +72,7 @@ SequencesStatistics::~SequencesStatistics()
   smtStatisticsRegistry()->unregisterStat(&d_regexpUnfoldingsNeg);
   smtStatisticsRegistry()->unregisterStat(&d_rewrites);
   smtStatisticsRegistry()->unregisterStat(&d_conflictsEqEngine);
-  smtStatisticsRegistry()->unregisterStat(&d_conflictsEagerPrefix);
+  smtStatisticsRegistry()->unregisterStat(&d_conflictsEager);
   smtStatisticsRegistry()->unregisterStat(&d_conflictsInfer);
   smtStatisticsRegistry()->unregisterStat(&d_lemmasEagerPreproc);
   smtStatisticsRegistry()->unregisterStat(&d_lemmasCmiSplit);
diff --git a/src/theory/strings/sequences_stats.h b/src/theory/strings/sequences_stats.h
index b205310ed..e35d951f7 100644
--- a/src/theory/strings/sequences_stats.h
+++ b/src/theory/strings/sequences_stats.h
@@ -92,8 +92,8 @@ class SequencesStatistics
   //--------------- conflicts, partition of calls to OutputChannel::conflict
   /** Number of equality engine conflicts */
   IntStat d_conflictsEqEngine;
-  /** Number of eager prefix conflicts */
-  IntStat d_conflictsEagerPrefix;
+  /** Number of eager conflicts */
+  IntStat d_conflictsEager;
   /** Number of inference conflicts */
   IntStat d_conflictsInfer;
   //--------------- end of conflicts
diff --git a/src/theory/strings/solver_state.cpp b/src/theory/strings/solver_state.cpp
index 426d37392..40edb88cf 100644
--- a/src/theory/strings/solver_state.cpp
+++ b/src/theory/strings/solver_state.cpp
@@ -28,9 +28,10 @@ namespace strings {
 SolverState::SolverState(context::Context* c,
                          context::UserContext* u,
                          Valuation& v)
-    : TheoryState(c, u, v), d_eeDisequalities(c), d_pendingConflict(c)
+    : TheoryState(c, u, v), d_eeDisequalities(c), d_pendingConflictSet(c, false)
 {
   d_zero = NodeManager::currentNM()->mkConst(Rational(0));
+  d_false = NodeManager::currentNM()->mkConst(false);
 }
 
 SolverState::~SolverState()
@@ -95,12 +96,12 @@ void SolverState::eqNotifyMerge(TNode t1, TNode t2)
     }
     if (!e2->d_prefixC.get().isNull())
     {
-      setPendingConflictWhen(
+      setPendingPrefixConflictWhen(
           e1->addEndpointConst(e2->d_prefixC, Node::null(), false));
     }
     if (!e2->d_suffixC.get().isNull())
     {
-      setPendingConflictWhen(
+      setPendingPrefixConflictWhen(
           e1->addEndpointConst(e2->d_suffixC, Node::null(), true));
     }
     if (e2->d_cardinalityLemK.get() > e1->d_cardinalityLemK.get())
@@ -161,7 +162,7 @@ void SolverState::addEndpointsToEqcInfo(Node t, Node concat, Node eqc)
       Trace("strings-eager-pconf-debug")
           << "New term: " << concat << " for " << t << " with prefix " << c
           << " (" << (r == 1) << ")" << std::endl;
-      setPendingConflictWhen(ei->addEndpointConst(t, c, r == 1));
+      setPendingPrefixConflictWhen(ei->addEndpointConst(t, c, r == 1));
     }
   }
 }
@@ -227,15 +228,38 @@ bool SolverState::isEqualEmptyWord(Node s, Node& emps)
   return false;
 }
 
-void SolverState::setPendingConflictWhen(Node conf)
+void SolverState::setPendingPrefixConflictWhen(Node conf)
 {
-  if (!conf.isNull() && d_pendingConflict.get().isNull())
+  if (conf.isNull() || d_pendingConflictSet.get())
   {
-    d_pendingConflict = conf;
+    return;
   }
+  InferInfo iiPrefixConf;
+  iiPrefixConf.d_id = Inference::PREFIX_CONFLICT;
+  iiPrefixConf.d_conc = d_false;
+  utils::flattenOp(AND, conf, iiPrefixConf.d_ant);
+  setPendingConflict(iiPrefixConf);
 }
 
-Node SolverState::getPendingConflict() const { return d_pendingConflict; }
+void SolverState::setPendingConflict(InferInfo& ii)
+{
+  if (!d_pendingConflictSet.get())
+  {
+    d_pendingConflict = ii;
+  }
+}
+
+bool SolverState::hasPendingConflict() const { return d_pendingConflictSet; }
+
+bool SolverState::getPendingConflict(InferInfo& ii) const
+{
+  if (d_pendingConflictSet)
+  {
+    ii = d_pendingConflict;
+    return true;
+  }
+  return false;
+}
 
 std::pair<bool, Node> SolverState::entailmentCheck(options::TheoryOfMode mode,
                                                    TNode lit)
diff --git a/src/theory/strings/solver_state.h b/src/theory/strings/solver_state.h
index e6839760f..291a15feb 100644
--- a/src/theory/strings/solver_state.h
+++ b/src/theory/strings/solver_state.h
@@ -23,6 +23,7 @@
 #include "context/context.h"
 #include "expr/node.h"
 #include "theory/strings/eqc_info.h"
+#include "theory/strings/infer_info.h"
 #include "theory/theory_model.h"
 #include "theory/theory_state.h"
 #include "theory/uf/equality_engine.h"
@@ -66,7 +67,7 @@ class SolverState : public TheoryState
   void eqNotifyDisequal(TNode t1, TNode t2, TNode reason);
   //-------------------------------------- end notifications for equalities
   //------------------------------------------ conflicts
-  /** set pending conflict
+  /** set pending prefix conflict
    *
    * If conf is non-null, this is called when conf is a conjunction of literals
    * that hold in the current context that are unsatisfiable. It is set as the
@@ -76,9 +77,16 @@ class SolverState : public TheoryState
    * during a merge operation, when the equality engine is not in a state to
    * provide explanations.
    */
-  void setPendingConflictWhen(Node conf);
+  void setPendingPrefixConflictWhen(Node conf);
+  /**
+   * Set pending conflict, infer info version. Called when we are in conflict
+   * based on the inference ii. This generalizes the above method.
+   */
+  void setPendingConflict(InferInfo& ii);
+  /** return true if we have a pending conflict */
+  bool hasPendingConflict() const;
   /** get the pending conflict, or null if none exist */
-  Node getPendingConflict() const;
+  bool getPendingConflict(InferInfo& ii) const;
   //------------------------------------------ end conflicts
   /** get length with explanation
    *
@@ -152,13 +160,16 @@ class SolverState : public TheoryState
  private:
   /** Common constants */
   Node d_zero;
+  Node d_false;
   /**
    * The (SAT-context-dependent) list of disequalities that have been asserted
    * to the equality engine above.
    */
   NodeList d_eeDisequalities;
   /** The pending conflict if one exists */
-  context::CDO<Node> d_pendingConflict;
+  context::CDO<bool> d_pendingConflictSet;
+  /** The pending conflict, valid if the above flag is true */
+  InferInfo d_pendingConflict;
   /** Map from representatives to their equivalence class information */
   std::map<Node, EqcInfo*> d_eqcInfo;
 }; /* class TheoryStrings */
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 2b2c25333..1dc19deb1 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -15,6 +15,7 @@
 #include "theory/strings/theory_strings.h"
 
 #include "expr/kind.h"
+#include "options/smt_options.h"
 #include "options/strings_options.h"
 #include "options/theory_options.h"
 #include "smt/logic_exception.h"
@@ -44,7 +45,7 @@ TheoryStrings::TheoryStrings(context::Context* c,
       d_notify(*this),
       d_statistics(),
       d_state(c, u, d_valuation),
-      d_termReg(d_state, out, d_statistics, nullptr),
+      d_termReg(d_state, out, d_statistics, pnm),
       d_extTheoryCb(),
       d_extTheory(d_extTheoryCb, c, u, out),
       d_im(*this, d_state, d_termReg, d_extTheory, d_statistics, pnm),
@@ -194,17 +195,7 @@ bool TheoryStrings::propagateLit(TNode literal)
 TrustNode TheoryStrings::explain(TNode literal)
 {
   Debug("strings-explain") << "explain called on " << literal << std::endl;
-  std::vector< TNode > assumptions;
-  d_im.explain(literal, assumptions);
-  Node ret;
-  if( assumptions.empty() ){
-    ret = d_true;
-  }else if( assumptions.size()==1 ){
-    ret = assumptions[0];
-  }else{
-    ret = NodeManager::currentNM()->mkNode(kind::AND, assumptions);
-  }
-  return TrustNode::mkTrustPropExp(literal, ret, nullptr);
+  return d_im.explainLit(literal);
 }
 
 void TheoryStrings::presolve() {
@@ -618,22 +609,18 @@ void TheoryStrings::notifyFact(TNode atom,
     }
   }
   // process pending conflicts due to reasoning about endpoints
-  if (!d_state.isInConflict())
+  if (!d_state.isInConflict() && d_state.hasPendingConflict())
   {
-    Node pc = d_state.getPendingConflict();
-    if (!pc.isNull())
-    {
-      std::vector<Node> a;
-      a.push_back(pc);
-      Trace("strings-pending")
-          << "Process pending conflict " << pc << std::endl;
-      Node conflictNode = d_im.mkExplain(a);
-      Trace("strings-conflict")
-          << "CONFLICT: Eager prefix : " << conflictNode << std::endl;
-      ++(d_statistics.d_conflictsEagerPrefix);
-      d_im.conflict(conflictNode);
-      return;
-    }
+    InferInfo iiPendingConf;
+    d_state.getPendingConflict(iiPendingConf);
+    Trace("strings-pending")
+        << "Process pending conflict " << iiPendingConf.d_ant << std::endl;
+    Trace("strings-conflict")
+        << "CONFLICT: Eager : " << iiPendingConf.d_ant << std::endl;
+    ++(d_statistics.d_conflictsEager);
+    // call the inference manager to send the conflict
+    d_im.processConflict(iiPendingConf);
+    return;
   }
   Trace("strings-pending-debug") << "  Now collect terms" << std::endl;
   // Collect extended function terms in the atom. Notice that we must register
@@ -693,34 +680,41 @@ void TheoryStrings::postCheck(Effort e)
       Trace("strings-eqc") << std::endl;
     }
     ++(d_statistics.d_checkRuns);
-    bool addedLemma = false;
-    bool addedFact;
+    bool sentLemma = false;
+    bool hadPending = false;
     Trace("strings-check") << "Full effort check..." << std::endl;
     do{
+      d_im.reset();
       ++(d_statistics.d_strategyRuns);
       Trace("strings-check") << "  * Run strategy..." << std::endl;
       runStrategy(e);
+      // remember if we had pending facts or lemmas
+      hadPending = d_im.hasPending();
       // Send the facts *and* the lemmas. We send lemmas regardless of whether
       // we send facts since some lemmas cannot be dropped. Other lemmas are
       // otherwise avoided by aborting the strategy when a fact is ready.
-      addedFact = d_im.hasPendingFact();
-      addedLemma = d_im.hasPendingLemma();
-      d_im.doPendingFacts();
-      d_im.doPendingLemmas();
+      d_im.doPending();
+      // Did we successfully send a lemma? Notice that if hasPending = true
+      // and sentLemma = false, then the above call may have:
+      // (1) had no pending lemmas, but successfully processed pending facts,
+      // (2) unsuccessfully processed pending lemmas.
+      // In either case, we repeat the strategy if we are not in conflict.
+      sentLemma = d_im.hasSentLemma();
       if (Trace.isOn("strings-check"))
       {
         Trace("strings-check") << "  ...finish run strategy: ";
-        Trace("strings-check") << (addedFact ? "addedFact " : "");
-        Trace("strings-check") << (addedLemma ? "addedLemma " : "");
+        Trace("strings-check") << (hadPending ? "hadPending " : "");
+        Trace("strings-check") << (sentLemma ? "sentLemma " : "");
         Trace("strings-check") << (d_state.isInConflict() ? "conflict " : "");
-        if (!addedFact && !addedLemma && !d_state.isInConflict())
+        if (!hadPending && !sentLemma && !d_state.isInConflict())
         {
           Trace("strings-check") << "(none)";
         }
         Trace("strings-check") << std::endl;
       }
-      // repeat if we did not add a lemma or conflict
-    } while (!d_state.isInConflict() && !addedLemma && addedFact);
+      // repeat if we did not add a lemma or conflict, and we had pending
+      // facts or lemmas.
+    } while (!d_state.isInConflict() && !sentLemma && hadPending);
   }
   Trace("strings-check") << "Theory of strings, done check : " << e << std::endl;
   Assert(!d_im.hasPendingFact());
@@ -736,17 +730,14 @@ bool TheoryStrings::needsCheckLastEffort() {
 
 /** Conflict when merging two constants */
 void TheoryStrings::conflict(TNode a, TNode b){
-  if (!d_state.isInConflict())
+  if (d_state.isInConflict())
   {
-    Debug("strings-conflict") << "Making conflict..." << std::endl;
-    d_state.notifyInConflict();
-    TrustNode conflictNode = explain(a.eqNode(b));
-    Trace("strings-conflict")
-        << "CONFLICT: Eq engine conflict : " << conflictNode.getNode()
-        << std::endl;
-    ++(d_statistics.d_conflictsEqEngine);
-    d_out->conflict(conflictNode.getNode());
+    // already in conflict
+    return;
   }
+  d_im.conflictEqConstantMerge(a, b);
+  Trace("strings-conflict") << "CONFLICT: Eq engine conflict" << std::endl;
+  ++(d_statistics.d_conflictsEqEngine);
 }
 
 void TheoryStrings::eqNotifyNewClass(TNode t){
@@ -967,7 +958,8 @@ void TheoryStrings::checkCodes()
           Node eqn = c1[0].eqNode(c2[0]);
           // str.code(x)==-1 V str.code(x)!=str.code(y) V x==y
           Node inj_lem = nm->mkNode(kind::OR, eq_no, deq, eqn);
-          d_im.sendPhaseRequirement(deq, false);
+          deq = Rewriter::rewrite(deq);
+          d_im.addPendingPhaseRequirement(deq, false);
           std::vector<Node> emptyVec;
           d_im.sendInference(emptyVec, inj_lem, Inference::CODE_INJ);
         }