Refactor strings to use an inference manager object (#3076)

9 files changed, 994 insertions, 512 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 885b26078..cc13dec6d 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -628,6 +628,8 @@ libcvc4_add_sources(
   theory/shared_terms_database.h
   theory/sort_inference.cpp
   theory/sort_inference.h
+  theory/strings/inference_manager.cpp
+  theory/strings/inference_manager.h
   theory/strings/normal_form.cpp
   theory/strings/normal_form.h
   theory/strings/regexp_elim.cpp
@@ -645,6 +647,8 @@ libcvc4_add_sources(
   theory/strings/theory_strings_rewriter.cpp
   theory/strings/theory_strings_rewriter.h
   theory/strings/theory_strings_type_rules.h
+  theory/strings/theory_strings_utils.cpp
+  theory/strings/theory_strings_utils.h
   theory/strings/type_enumerator.h
   theory/subs_minimize.cpp
   theory/subs_minimize.h
diff --git a/src/theory/strings/inference_manager.cpp b/src/theory/strings/inference_manager.cpp
new file mode 100644
index 000000000..ec144aa6d
--- /dev/null
+++ b/src/theory/strings/inference_manager.cpp
@@ -0,0 +1,407 @@
+/*********************                                                        */
+/*! \file inference_manager.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Implementation of the inference manager for the theory of strings.
+ **/
+
+#include "theory/strings/inference_manager.h"
+
+#include "expr/kind.h"
+#include "options/strings_options.h"
+#include "theory/rewriter.h"
+#include "theory/strings/theory_strings.h"
+#include "theory/strings/theory_strings_rewriter.h"
+#include "theory/strings/theory_strings_utils.h"
+
+using namespace std;
+using namespace CVC4::context;
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace theory {
+namespace strings {
+
+InferenceManager::InferenceManager(TheoryStrings& p,
+                                   context::Context* c,
+                                   context::UserContext* u,
+                                   eq::EqualityEngine& ee,
+                                   OutputChannel& out)
+    : d_parent(p), d_ee(ee), d_out(out), d_keep(c)
+{
+  d_true = NodeManager::currentNM()->mkConst(true);
+  d_false = NodeManager::currentNM()->mkConst(false);
+}
+
+bool InferenceManager::sendInternalInference(std::vector<Node>& exp,
+                                             Node conc,
+                                             const char* c)
+{
+  if (conc.getKind() == AND
+      || (conc.getKind() == NOT && conc[0].getKind() == OR))
+  {
+    Node conj = conc.getKind() == AND ? conc : conc[0];
+    bool pol = conc.getKind() == AND;
+    bool ret = true;
+    for (const Node& cc : conj)
+    {
+      bool retc = sendInternalInference(exp, pol ? cc : cc.negate(), c);
+      ret = ret && retc;
+    }
+    return ret;
+  }
+  bool pol = conc.getKind() != NOT;
+  Node lit = pol ? conc : conc[0];
+  if (lit.getKind() == EQUAL)
+  {
+    for (unsigned i = 0; i < 2; i++)
+    {
+      if (!lit[i].isConst() && !d_parent.hasTerm(lit[i]))
+      {
+        // introduces a new non-constant term, do not infer
+        return false;
+      }
+    }
+    // does it already hold?
+    if (pol ? d_parent.areEqual(lit[0], lit[1])
+            : d_parent.areDisequal(lit[0], lit[1]))
+    {
+      return true;
+    }
+  }
+  else if (lit.isConst())
+  {
+    if (lit.getConst<bool>())
+    {
+      Assert(pol);
+      // trivially holds
+      return true;
+    }
+  }
+  else if (!d_parent.hasTerm(lit))
+  {
+    // introduces a new non-constant term, do not infer
+    return false;
+  }
+  else if (d_parent.areEqual(lit, pol ? d_true : d_false))
+  {
+    // already holds
+    return true;
+  }
+  sendInference(exp, conc, c);
+  return true;
+}
+
+void InferenceManager::sendInference(std::vector<Node>& exp,
+                                     std::vector<Node>& exp_n,
+                                     Node eq,
+                                     const char* c,
+                                     bool asLemma)
+{
+  eq = eq.isNull() ? d_false : Rewriter::rewrite(eq);
+  if (eq == d_true)
+  {
+    return;
+  }
+  if (Trace.isOn("strings-infer-debug"))
+  {
+    Trace("strings-infer-debug")
+        << "By " << c << ", 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;
+    }
+  }
+  // check if we should send a lemma or an inference
+  if (asLemma || eq == d_false || eq.getKind() == OR || !exp_n.empty()
+      || options::stringInferAsLemmas())
+  {
+    Node eq_exp;
+    if (options::stringRExplainLemmas())
+    {
+      eq_exp = d_parent.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;
+    }
+    sendLemma(eq_exp, eq, c);
+  }
+  else
+  {
+    sendInfer(utils::mkAnd(exp), eq, c);
+  }
+}
+
+void InferenceManager::sendInference(std::vector<Node>& exp,
+                                     Node eq,
+                                     const char* c,
+                                     bool asLemma)
+{
+  std::vector<Node> exp_n;
+  sendInference(exp, exp_n, eq, c, asLemma);
+}
+
+void InferenceManager::sendLemma(Node ant, Node conc, const char* c)
+{
+  if (conc.isNull() || conc == d_false)
+  {
+    Trace("strings-conflict")
+        << "Strings::Conflict : " << c << " : " << ant << std::endl;
+    Trace("strings-lemma") << "Strings::Conflict : " << c << " : " << ant
+                           << std::endl;
+    Trace("strings-assert")
+        << "(assert (not " << ant << ")) ; conflict " << c << std::endl;
+    d_out.conflict(ant);
+    d_parent.d_conflict = true;
+    return;
+  }
+  Node lem;
+  if (ant == d_true)
+  {
+    lem = conc;
+  }
+  else
+  {
+    lem = NodeManager::currentNM()->mkNode(IMPLIES, ant, conc);
+  }
+  Trace("strings-lemma") << "Strings::Lemma " << c << " : " << lem << std::endl;
+  Trace("strings-assert") << "(assert " << lem << ") ; lemma " << c
+                          << std::endl;
+  d_pendingLem.push_back(lem);
+}
+
+void InferenceManager::sendInfer(Node eq_exp, Node eq, const char* c)
+{
+  if (options::stringInferSym())
+  {
+    std::vector<Node> vars;
+    std::vector<Node> subs;
+    std::vector<Node> unproc;
+    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 " << c << 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, c);
+      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 " << c << std::endl;
+  Trace("strings-assert") << "(assert (=> " << eq_exp << " " << eq
+                          << ")) ; infer " << c << 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, const char* c, bool preq)
+{
+  Node eq = a.eqNode(b);
+  eq = Rewriter::rewrite(eq);
+  if (eq.isConst())
+  {
+    return false;
+  }
+  NodeManager* nm = NodeManager::currentNM();
+  Node lemma_or = nm->mkNode(OR, eq, nm->mkNode(NOT, eq));
+  Trace("strings-lemma") << "Strings::Lemma " << c << " SPLIT : " << lemma_or
+                         << std::endl;
+  d_pendingLem.push_back(lemma_or);
+  sendPhaseRequirement(eq, preq);
+  return true;
+}
+
+void InferenceManager::sendPhaseRequirement(Node lit, bool pol)
+{
+  d_pendingReqPhase[lit] = pol;
+}
+
+void InferenceManager::doPendingFacts()
+{
+  size_t i = 0;
+  while (!hasConflict() && i < d_pending.size())
+  {
+    Node fact = d_pending[i];
+    Node exp = d_pendingExp[fact];
+    if (fact.getKind() == AND)
+    {
+      for (const Node& lit : fact)
+      {
+        bool polarity = lit.getKind() != NOT;
+        TNode atom = polarity ? lit : lit[0];
+        d_parent.assertPendingFact(atom, polarity, exp);
+      }
+    }
+    else
+    {
+      bool polarity = fact.getKind() != NOT;
+      TNode atom = polarity ? fact : fact[0];
+      d_parent.assertPendingFact(atom, polarity, exp);
+    }
+    i++;
+  }
+  d_pending.clear();
+  d_pendingExp.clear();
+}
+
+void InferenceManager::doPendingLemmas()
+{
+  if (!hasConflict())
+  {
+    for (const Node& lc : d_pendingLem)
+    {
+      Trace("strings-pending") << "Process pending lemma : " << lc << std::endl;
+      d_out.lemma(lc);
+    }
+    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();
+}
+
+bool InferenceManager::hasConflict() const { return d_parent.d_conflict; }
+
+void InferenceManager::inferSubstitutionProxyVars(
+    Node n,
+    std::vector<Node>& vars,
+    std::vector<Node>& subs,
+    std::vector<Node>& unproc) const
+{
+  if (n.getKind() == AND)
+  {
+    for (const Node& nc : n)
+    {
+      inferSubstitutionProxyVars(nc, vars, subs, unproc);
+    }
+    return;
+  }
+  if (n.getKind() == EQUAL)
+  {
+    Node ns = n.substitute(vars.begin(), vars.end(), subs.begin(), subs.end());
+    ns = Rewriter::rewrite(ns);
+    if (ns.getKind() == EQUAL)
+    {
+      Node s;
+      Node v;
+      for (unsigned i = 0; i < 2; i++)
+      {
+        Node ss;
+        // determine whether this side has a proxy variable
+        if (ns[i].getAttribute(StringsProxyVarAttribute()))
+        {
+          // it is a proxy variable
+          ss = ns[i];
+        }
+        else if (ns[i].isConst())
+        {
+          ss = d_parent.getProxyVariableFor(ns[i]);
+        }
+        if (!ss.isNull())
+        {
+          v = ns[1 - i];
+          // if the other side is a constant or variable
+          if (v.getNumChildren() == 0)
+          {
+            if (s.isNull())
+            {
+              s = ss;
+            }
+            else
+            {
+              // both sides of the equality correspond to a proxy variable
+              if (ss == s)
+              {
+                // it is a trivial equality, e.g. between a proxy variable
+                // and its definition
+                return;
+              }
+              else
+              {
+                // equality between proxy variables, non-trivial
+                s = Node::null();
+              }
+            }
+          }
+        }
+      }
+      if (!s.isNull())
+      {
+        // the equality can be turned into a substitution
+        subs.push_back(s);
+        vars.push_back(v);
+        return;
+      }
+    }
+    else
+    {
+      n = ns;
+    }
+  }
+  if (n != d_true)
+  {
+    unproc.push_back(n);
+  }
+}
+
+}  // namespace strings
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/strings/inference_manager.h b/src/theory/strings/inference_manager.h
new file mode 100644
index 000000000..71651f7df
--- /dev/null
+++ b/src/theory/strings/inference_manager.h
@@ -0,0 +1,292 @@
+/*********************                                                        */
+/*! \file inference_manager.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Customized inference manager for the theory of strings
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__STRINGS__INFERENCE_MANAGER_H
+#define CVC4__THEORY__STRINGS__INFERENCE_MANAGER_H
+
+#include <map>
+#include <vector>
+
+#include "context/cdhashset.h"
+#include "context/context.h"
+#include "expr/node.h"
+#include "theory/output_channel.h"
+#include "theory/uf/equality_engine.h"
+
+namespace CVC4 {
+namespace theory {
+namespace strings {
+
+class TheoryStrings;
+
+/** Inference Manager
+ *
+ * The purpose of this class is to process inference steps for strategies
+ * in the theory of strings.
+ *
+ * In particular, inferences are given to this class via calls to functions:
+ *
+ * sendInternalInference, sendInference, sendSplit
+ *
+ * This class decides how the conclusion of these calls will be processed.
+ * It primarily has to decide whether the conclusions will be processed:
+ *
+ * (1) Internally in the strings solver, via calls to equality engine's
+ * assertLiteral and assertPredicate commands. We refer to these literals as
+ * "facts",
+ * (2) Externally on the output channel of theory of strings as "lemmas",
+ * (3) External on the output channel as "conflicts" (when a conclusion of an
+ * inference is false).
+ *
+ * It buffers facts and lemmas in vectors d_pending and d_pending_lem
+ * respectively.
+ *
+ * When applicable, facts can be flushed to the equality engine via a call to
+ * doPendingFacts, and lemmas can be flushed to the output channel via a call
+ * to doPendingLemmas.
+ *
+ * It also manages other kinds of interaction with the output channel of the
+ * theory of strings, e.g. sendPhaseRequirement.
+ */
+class InferenceManager
+{
+  typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
+
+ public:
+  InferenceManager(TheoryStrings& p,
+                   context::Context* c,
+                   context::UserContext* u,
+                   eq::EqualityEngine& ee,
+                   OutputChannel& out);
+  ~InferenceManager() {}
+
+  /** send internal inferences
+   *
+   * This is called when we have inferred exp => conc, where exp is a set
+   * of equalities and disequalities that hold in the current equality engine.
+   * This method adds equalities and disequalities ~( s = t ) via
+   * sendInference such that both s and t are either constants or terms
+   * that already occur in the equality engine, and ~( s = t ) is a consequence
+   * of conc. This function can be seen as a "conservative" version of
+   * sendInference below in that it does not introduce any new non-constant
+   * terms to the state.
+   *
+   * The argument c is a string identifying the reason for the inference.
+   * This string is used for debugging purposes.
+   *
+   * Return true if the inference is complete, in the sense that we infer
+   * inferences that are equivalent to conc. This returns false e.g. if conc
+   * (or one of its conjuncts if it is a conjunction) was not inferred due
+   * to the criteria mentioned above.
+   */
+  bool sendInternalInference(std::vector<Node>& exp, Node conc, const char* c);
+  /** send inference
+   *
+   * This function should be called when ( exp ^ exp_n ) => eq. The set exp
+   * 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:
+   *
+   * [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,
+   *
+   * [3] (Lemma) Indicate that the lemma ( EXPLAIN(exp) ^ exp_n ) => eq should
+   * be sent on the output channel of the theory of strings, or
+   *
+   * [4] (Conflict) Immediately report a conflict EXPLAIN(exp) on the output
+   * channel of the theory of strings.
+   *
+   * Determining which case to apply depends on the form of eq and whether
+   * exp_n is empty. In particular, lemmas must be used whenever exp_n is
+   * non-empty, conflicts are used when exp_n is empty and eq is false.
+   *
+   * The argument c is a string identifying the reason for inference, used for
+   * debugging.
+   *
+   * If the flag asLemma is true, then this method will send a lemma instead
+   * of an inference whenever applicable.
+   */
+  void sendInference(std::vector<Node>& exp,
+                     std::vector<Node>& exp_n,
+                     Node eq,
+                     const char* c,
+                     bool asLemma = false);
+  /** same as above, but where exp_n is empty */
+  void sendInference(std::vector<Node>& exp,
+                     Node eq,
+                     const char* c,
+                     bool asLemma = false);
+  /** Send split
+   *
+   * This requests that ( a = b V a != b ) is sent on the output channel as a
+   * lemma. We additionally request a phase requirement for the equality a=b
+   * with polarity preq.
+   *
+   * The argument c is a string identifying the reason for inference, used for
+   * debugging.
+   *
+   * This method returns true if the split was non-trivial, and false
+   * otherwise. A split is trivial if a=b rewrites to a constant.
+   */
+  bool sendSplit(Node a, Node b, const char* c, 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.
+   */
+  void sendPhaseRequirement(Node lit, bool pol);
+  /** 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 in the theory of strings.
+   *
+   * 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
+  {
+    return hasConflict() || !d_pendingLem.empty() || !d_pending.empty();
+  }
+  /** 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(); }
+  /** Are we in conflict? */
+  bool hasConflict() const;
+
+ private:
+  /**
+   * 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 c is a string identifying the reason for inference, used for
+   * debugging.
+   */
+  void sendLemma(Node ant, Node conc, const char* c);
+  /**
+   * 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, const char* c);
+
+  /** the parent theory of strings object */
+  TheoryStrings& d_parent;
+  /** the equality engine
+   *
+   * This is a reference to the equality engine of the theory of strings.
+   */
+  eq::EqualityEngine& d_ee;
+  /** the output channel
+   *
+   * This is a reference to the output channel of the theory of strings.
+   */
+  OutputChannel& d_out;
+  /** Common constants */
+  Node d_true;
+  Node d_false;
+  /** 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;
+  /** 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;
+  /**
+   * The keep set of this class. This set is maintained to ensure that
+   * facts and their explanations are ref-counted. Since facts and their
+   * explanations are SAT-context-dependent, this set is also
+   * SAT-context-dependent.
+   */
+  NodeSet d_keep;
+  /** infer substitution proxy vars
+   *
+   * This method attempts to (partially) convert the formula n into a
+   * substitution of the form:
+   *   v1 -> s1, ..., vn -> sn
+   * where s1 ... sn are proxy variables and v1 ... vn are either variables
+   * or constants.
+   *
+   * This method ensures that P ^ v1 = s1 ^ ... ^ vn = sn ^ unproc is equivalent
+   * to P ^ n, where P is the conjunction of equalities corresponding to the
+   * definition of all proxy variables introduced by the theory of strings.
+   *
+   * For example, say that v1 was introduced as a proxy variable for "ABC", and
+   * v2 was introduced as a proxy variable for "AA".
+   *
+   * Given the input n := v1 = "ABC" ^ v2 = x ^ x = "AA", this method sets:
+   * vars = { x },
+   * subs = { v2 },
+   * unproc = {}.
+   * In particular, this says that the information content of n is essentially
+   * x = v2. The first and third conjunctions can be dropped from the
+   * explanation since these equalities simply correspond to definitions
+   * of proxy variables.
+   *
+   * This method is used as a performance heuristic. It can infer when the
+   * explanation of a fact depends only trivially on equalities corresponding
+   * to definitions of proxy variables, which can be omitted since they are
+   * assumed to hold globally.
+   */
+  void inferSubstitutionProxyVars(Node n,
+                                  std::vector<Node>& vars,
+                                  std::vector<Node>& subs,
+                                  std::vector<Node>& unproc) const;
+};
+
+}  // namespace strings
+}  // namespace theory
+}  // namespace CVC4
+
+#endif
diff --git a/src/theory/strings/regexp_solver.cpp b/src/theory/strings/regexp_solver.cpp
index bf3a170df..5079806ac 100644
--- a/src/theory/strings/regexp_solver.cpp
+++ b/src/theory/strings/regexp_solver.cpp
@@ -32,9 +32,11 @@ namespace theory {
 namespace strings {
 
 RegExpSolver::RegExpSolver(TheoryStrings& p,
+                           InferenceManager& im,
                            context::Context* c,
                            context::UserContext* u)
     : d_parent(p),
+      d_im(im),
       d_regexp_memberships(c),
       d_regexp_ucached(u),
       d_regexp_ccached(c),
@@ -147,17 +149,17 @@ void RegExpSolver::check()
               vec_nodes.push_back(n);
             }
             Node conc;
-            d_parent.sendInference(vec_nodes, conc, "INTERSECT CONFLICT", true);
+            d_im.sendInference(vec_nodes, conc, "INTERSECT CONFLICT", true);
             addedLemma = true;
             break;
           }
-          if (d_parent.inConflict())
+          if (d_im.hasConflict())
           {
             break;
           }
         }
         // updates
-        if (!d_parent.inConflict() && !spflag)
+        if (!d_im.hasConflict() && !spflag)
         {
           d_inter_cache[x] = r;
           d_inter_index[x] = (int)n_pmem;
@@ -235,7 +237,7 @@ void RegExpSolver::check()
             std::vector<Node> exp_n;
             exp_n.push_back(assertion);
             Node conc = Node::null();
-            d_parent.sendInference(rnfexp, exp_n, conc, "REGEXP NF Conflict");
+            d_im.sendInference(rnfexp, exp_n, conc, "REGEXP NF Conflict");
             addedLemma = true;
             break;
           }
@@ -280,7 +282,7 @@ void RegExpSolver::check()
           exp_n.push_back(assertion);
           Node conc = nvec.size() == 1 ? nvec[0] : nm->mkNode(AND, nvec);
           conc = Rewriter::rewrite(conc);
-          d_parent.sendInference(rnfexp, exp_n, conc, "REGEXP_Unfold");
+          d_im.sendInference(rnfexp, exp_n, conc, "REGEXP_Unfold");
           addedLemma = true;
           if (changed)
           {
@@ -298,7 +300,7 @@ void RegExpSolver::check()
             repUnfold.insert(x);
           }
         }
-        if (d_parent.inConflict())
+        if (d_im.hasConflict())
         {
           break;
         }
@@ -307,7 +309,7 @@ void RegExpSolver::check()
   }
   if (addedLemma)
   {
-    if (!d_parent.inConflict())
+    if (!d_im.hasConflict())
     {
       for (unsigned i = 0; i < processed.size(); i++)
       {
@@ -338,7 +340,7 @@ bool RegExpSolver::checkPDerivative(
         std::vector<Node> exp_n;
         exp_n.push_back(atom);
         exp_n.push_back(x.eqNode(d_emptyString));
-        d_parent.sendInference(nf_exp, exp_n, exp, "RegExp Delta");
+        d_im.sendInference(nf_exp, exp_n, exp, "RegExp Delta");
         addedLemma = true;
         d_regexp_ccached.insert(atom);
         return false;
@@ -354,7 +356,7 @@ bool RegExpSolver::checkPDerivative(
         exp_n.push_back(atom);
         exp_n.push_back(x.eqNode(d_emptyString));
         Node conc;
-        d_parent.sendInference(nf_exp, exp_n, conc, "RegExp Delta CONFLICT");
+        d_im.sendInference(nf_exp, exp_n, conc, "RegExp Delta CONFLICT");
         addedLemma = true;
         d_regexp_ccached.insert(atom);
         return false;
@@ -444,7 +446,7 @@ bool RegExpSolver::deriveRegExp(Node x,
     }
     std::vector<Node> exp_n;
     exp_n.push_back(atom);
-    d_parent.sendInference(ant, exp_n, conc, "RegExp-Derive");
+    d_im.sendInference(ant, exp_n, conc, "RegExp-Derive");
     return true;
   }
   return false;
diff --git a/src/theory/strings/regexp_solver.h b/src/theory/strings/regexp_solver.h
index 13b66557a..ec74d98cd 100644
--- a/src/theory/strings/regexp_solver.h
+++ b/src/theory/strings/regexp_solver.h
@@ -23,6 +23,7 @@
 #include "context/cdlist.h"
 #include "context/context.h"
 #include "expr/node.h"
+#include "theory/strings/inference_manager.h"
 #include "theory/strings/regexp_operation.h"
 #include "util/regexp.h"
 
@@ -42,7 +43,10 @@ class RegExpSolver
   typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
 
  public:
-  RegExpSolver(TheoryStrings& p, context::Context* c, context::UserContext* u);
+  RegExpSolver(TheoryStrings& p,
+               InferenceManager& im,
+               context::Context* c,
+               context::UserContext* u);
   ~RegExpSolver() {}
 
   /** add membership
@@ -69,6 +73,8 @@ class RegExpSolver
   Node d_false;
   /** the parent of this object */
   TheoryStrings& d_parent;
+  /** the output channel of the parent of this object */
+  InferenceManager& d_im;
   // check membership constraints
   Node mkAnd(Node c1, Node c2);
   bool checkPDerivative(
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 7b6bbdc99..ac6c0c102 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -26,6 +26,7 @@
 #include "theory/ext_theory.h"
 #include "theory/rewriter.h"
 #include "theory/strings/theory_strings_rewriter.h"
+#include "theory/strings/theory_strings_utils.h"
 #include "theory/strings/type_enumerator.h"
 #include "theory/theory_model.h"
 #include "theory/valuation.h"
@@ -104,9 +105,8 @@ TheoryStrings::TheoryStrings(context::Context* c,
     : Theory(THEORY_STRINGS, c, u, out, valuation, logicInfo),
       d_notify(*this),
       d_equalityEngine(d_notify, c, "theory::strings", true),
+      d_im(*this, c, u, d_equalityEngine, out),
       d_conflict(c, false),
-      d_infer(c),
-      d_infer_exp(c),
       d_nf_pairs(c),
       d_pregistered_terms_cache(u),
       d_registered_terms_cache(u),
@@ -121,7 +121,7 @@ TheoryStrings::TheoryStrings(context::Context* c,
       d_functionsTerms(c),
       d_has_extf(c, false),
       d_has_str_code(false),
-      d_regexp_solver(*this, c, u),
+      d_regexp_solver(*this, d_im, c, u),
       d_input_vars(u),
       d_input_var_lsum(u),
       d_cardinality_lits(u),
@@ -468,7 +468,7 @@ bool TheoryStrings::doReduction(int effort, Node n, bool& isCd)
             lexp.push_back(lenx.eqNode(lens));
             lexp.push_back(n.negate());
             Node xneqs = x.eqNode(s).negate();
-            sendInference(lexp, xneqs, "NEG-CTN-EQL", true);
+            d_im.sendInference(lexp, xneqs, "NEG-CTN-EQL", true);
           }
           // this depends on the current assertions, so we set that this
           // inference is context-dependent.
@@ -513,7 +513,7 @@ bool TheoryStrings::doReduction(int effort, Node n, bool& isCd)
     Node eq = Rewriter::rewrite(x.eqNode(mkConcat(sk1, s, sk2)));
     std::vector<Node> exp_vec;
     exp_vec.push_back(n);
-    sendInference(d_empty_vec, exp_vec, eq, "POS-CTN", true);
+    d_im.sendInference(d_empty_vec, exp_vec, eq, "POS-CTN", true);
     Trace("strings-extf-debug")
         << "  resolve extf : " << n << " based on positive contain reduction."
         << std::endl;
@@ -538,7 +538,7 @@ bool TheoryStrings::doReduction(int effort, Node n, bool& isCd)
     Trace("strings-red-lemma")
         << "Reduction_" << effort << " lemma : " << nnlem << std::endl;
     Trace("strings-red-lemma") << "...from " << n << std::endl;
-    sendInference(d_empty_vec, nnlem, "Reduction", true);
+    d_im.sendInference(d_empty_vec, nnlem, "Reduction", true);
     Trace("strings-extf-debug")
         << "  resolve extf : " << n << " based on reduction." << std::endl;
     isCd = false;
@@ -970,7 +970,7 @@ void TheoryStrings::check(Effort e) {
     //assert pending fact
     assertPendingFact( atom, polarity, fact );
   }
-  doPendingFacts();
+  d_im.doPendingFacts();
 
   Assert(d_strategy_init);
   std::map<Effort, std::pair<unsigned, unsigned> >::iterator itsr =
@@ -1016,18 +1016,18 @@ void TheoryStrings::check(Effort e) {
     do{
       runStrategy(sbegin, send);
       // flush the facts
-      addedFact = !d_pending.empty();
-      addedLemma = !d_lemma_cache.empty();
-      doPendingFacts();
-      doPendingLemmas();
+      addedFact = d_im.hasPendingFact();
+      addedLemma = d_im.hasPendingLemma();
+      d_im.doPendingFacts();
+      d_im.doPendingLemmas();
       // repeat if we did not add a lemma or conflict
     }while( !d_conflict && !addedLemma && addedFact );
 
     Trace("strings-check") << "Theory of strings done full effort check " << addedLemma << " " << d_conflict << std::endl;
   }
   Trace("strings-check") << "Theory of strings, done check : " << e << std::endl;
-  Assert( d_pending.empty() );
-  Assert( d_lemma_cache.empty() );
+  Assert(!d_im.hasPendingFact());
+  Assert(!d_im.hasPendingLemma());
 }
 
 bool TheoryStrings::needsCheckLastEffort() {
@@ -1056,7 +1056,7 @@ void TheoryStrings::checkExtfReductions( int effort ) {
     if (ret)
     {
       getExtTheory()->markReduced(extf[i], isCd);
-      if (hasProcessed())
+      if (d_im.hasProcessed())
       {
         return;
       }
@@ -1329,47 +1329,6 @@ void TheoryStrings::assertPendingFact(Node atom, bool polarity, Node exp) {
   Trace("strings-pending-debug") << "  Finished collect terms" << std::endl;
 }
 
-void TheoryStrings::doPendingFacts() {
-  size_t i=0;
-  while( !d_conflict && i<d_pending.size() ) {
-    Node fact = d_pending[i];
-    Node exp = d_pending_exp[ fact ];
-    if(fact.getKind() == kind::AND) {
-      for(size_t j=0; j<fact.getNumChildren(); j++) {
-        bool polarity = fact[j].getKind() != kind::NOT;
-        TNode atom = polarity ? fact[j] : fact[j][0];
-        assertPendingFact(atom, polarity, exp);
-      }
-    } else {
-      bool polarity = fact.getKind() != kind::NOT;
-      TNode atom = polarity ? fact : fact[0];
-      assertPendingFact(atom, polarity, exp);
-    }
-    i++;
-  }
-  d_pending.clear();
-  d_pending_exp.clear();
-}
-
-void TheoryStrings::doPendingLemmas() {
-  if( !d_conflict && !d_lemma_cache.empty() ){
-    for( unsigned i=0; i<d_lemma_cache.size(); i++ ){
-      Trace("strings-pending") << "Process pending lemma : " << d_lemma_cache[i] << std::endl;
-      d_out->lemma( d_lemma_cache[i] );
-    }
-    for( std::map< Node, bool >::iterator it = d_pending_req_phase.begin(); it != d_pending_req_phase.end(); ++it ){
-      Trace("strings-pending") << "Require phase : " << it->first << ", polarity = " << it->second << std::endl;
-      d_out->requirePhase( it->first, it->second );
-    }
-  }
-  d_lemma_cache.clear();
-  d_pending_req_phase.clear();
-}
-
-bool TheoryStrings::hasProcessed() {
-  return d_conflict || !d_lemma_cache.empty() || !d_pending.empty();
-}
-
 void TheoryStrings::addToExplanation( Node a, Node b, std::vector< Node >& exp ) {
   if( a!=b ){
     Debug("strings-explain") << "Add to explanation : " << a << " == " << b << std::endl;
@@ -1451,7 +1410,7 @@ void TheoryStrings::checkInit() {
                     }
                   }
                   //infer the equality
-                  sendInference( exp, n.eqNode( nc ), "I_Norm" );
+                  d_im.sendInference(exp, n.eqNode(nc), "I_Norm");
                 }else if( getExtTheory()->hasFunctionKind( n.getKind() ) ){
                   //mark as congruent : only process if neither has been reduced
                   getExtTheory()->markCongruent( nc, n );
@@ -1481,7 +1440,7 @@ void TheoryStrings::checkInit() {
                   }
                   AlwaysAssert( foundNEmpty );
                   //infer the equality
-                  sendInference(exp, n.eqNode(ns), "I_Norm_S");
+                  d_im.sendInference(exp, n.eqNode(ns), "I_Norm_S");
                 }
                 d_congruent.insert( n );
                 congruent[k]++;
@@ -1526,7 +1485,7 @@ void TheoryStrings::checkConstantEquivalenceClasses()
                                    << std::endl;
     prevSize = d_eqc_to_const.size();
     checkConstantEquivalenceClasses(&d_term_index[kind::STRING_CONCAT], vecc);
-  } while (!hasProcessed() && d_eqc_to_const.size() > prevSize);
+  } while (!d_im.hasProcessed() && d_eqc_to_const.size() > prevSize);
 }
 
 void TheoryStrings::checkConstantEquivalenceClasses( TermIndex* ti, std::vector< Node >& vecc ) {
@@ -1566,16 +1525,18 @@ void TheoryStrings::checkConstantEquivalenceClasses( TermIndex* ti, std::vector<
       //exp contains an explanation of n==c
       Assert( countc==vecc.size() );
       if( hasTerm( c ) ){
-        sendInference( exp, n.eqNode( c ), "I_CONST_MERGE" );
+        d_im.sendInference(exp, n.eqNode(c), "I_CONST_MERGE");
         return;
-      }else if( !hasProcessed() ){
+      }
+      else if (!d_im.hasProcessed())
+      {
         Node nr = getRepresentative( n );
         std::map< Node, Node >::iterator it = d_eqc_to_const.find( nr );
         if( it==d_eqc_to_const.end() ){
           Trace("strings-debug") << "Set eqc const " << n << " to " << c << std::endl;
           d_eqc_to_const[nr] = c;
           d_eqc_to_const_base[nr] = n;
-          d_eqc_to_const_exp[nr] = mkAnd( exp );
+          d_eqc_to_const_exp[nr] = utils::mkAnd(exp);
         }else if( c!=it->second ){
           //conflict
           Trace("strings-debug") << "Conflict, other constant was " << it->second << ", this constant was " << c << std::endl;
@@ -1587,7 +1548,7 @@ void TheoryStrings::checkConstantEquivalenceClasses( TermIndex* ti, std::vector<
             exp.push_back( d_eqc_to_const_exp[nr] );
             addToExplanation( n, d_eqc_to_const_base[nr], exp );
           }
-          sendInference( exp, d_false, "I_CONST_CONFLICT" );
+          d_im.sendInference(exp, d_false, "I_CONST_CONFLICT");
           return;
         }else{
           Trace("strings-debug") << "Duplicate constant." << std::endl;
@@ -1601,7 +1562,8 @@ void TheoryStrings::checkConstantEquivalenceClasses( TermIndex* ti, std::vector<
       vecc.push_back( itc->second );
       checkConstantEquivalenceClasses( &it->second, vecc );
       vecc.pop_back();
-      if( hasProcessed() ){
+      if (d_im.hasProcessed())
+      {
         break;
       }
     }
@@ -1698,7 +1660,7 @@ void TheoryStrings::checkExtfEval( int effort ) {
           }
           if( !conc.isNull() ){
             Trace("strings-extf") << "  resolve extf : " << sn << " -> " << nrc << std::endl;
-            sendInference(
+            d_im.sendInference(
                 einfo.d_exp, conc, effort == 0 ? "EXTF" : "EXTF-N", true);
             if( d_conflict ){
               Trace("strings-extf-debug") << "  conflict, return." << std::endl;
@@ -1731,7 +1693,7 @@ void TheoryStrings::checkExtfEval( int effort ) {
           // reduced since this argument may be circular: we may infer than n
           // can be reduced to something else, but that thing may argue that it
           // can be reduced to n, in theory.
-          sendInternalInference(
+          d_im.sendInternalInference(
               einfo.d_exp, nrcAssert, effort == 0 ? "EXTF_d" : "EXTF_d-N");
         }
         to_reduce = nrc;
@@ -1839,7 +1801,7 @@ void TheoryStrings::checkExtfInference( Node n, Node nr, ExtfInfoTmp& in, int ef
             if (areEqual(conc, d_false))
             {
               // we are in conflict
-              sendInference(in.d_exp, conc, "CTN_Decompose");
+              d_im.sendInference(in.d_exp, conc, "CTN_Decompose");
             }
             else if (getExtTheory()->hasFunctionKind(conc.getKind()))
             {
@@ -1912,7 +1874,7 @@ void TheoryStrings::checkExtfInference( Node n, Node nr, ExtfInfoTmp& in, int ef
             exp_c.insert(exp_c.end(),
                          d_extf_info_tmp[ofrom].d_exp.begin(),
                          d_extf_info_tmp[ofrom].d_exp.end());
-            sendInference(exp_c, conc, "CTN_Trans");
+            d_im.sendInference(exp_c, conc, "CTN_Trans");
           }
         }
       }
@@ -1945,23 +1907,34 @@ void TheoryStrings::checkExtfInference( Node n, Node nr, ExtfInfoTmp& in, int ef
     inferEqrr = Rewriter::rewrite(inferEqrr);
     Trace("strings-extf-infer") << "checkExtfInference: " << inferEq
                                 << " ...reduces to " << inferEqrr << std::endl;
-    sendInternalInference(in.d_exp, inferEqrr, "EXTF_equality_rew");
+    d_im.sendInternalInference(in.d_exp, inferEqrr, "EXTF_equality_rew");
   }
 }
 
-Node TheoryStrings::getSymbolicDefinition( Node n, std::vector< Node >& exp ) {
+Node TheoryStrings::getProxyVariableFor(Node n) const
+{
+  NodeNodeMap::const_iterator it = d_proxy_var.find(n);
+  if (it != d_proxy_var.end())
+  {
+    return (*it).second;
+  }
+  return Node::null();
+}
+Node TheoryStrings::getSymbolicDefinition(Node n, std::vector<Node>& exp) const
+{
   if( n.getNumChildren()==0 ){
-    NodeNodeMap::const_iterator it = d_proxy_var.find( n );
-    if( it==d_proxy_var.end() ){
+    Node pn = getProxyVariableFor(n);
+    if (pn.isNull())
+    {
       return Node::null();
-    }else{
-      Node eq = n.eqNode( (*it).second );
-      eq = Rewriter::rewrite( eq );
-      if( std::find( exp.begin(), exp.end(), eq )==exp.end() ){
-        exp.push_back( eq );
-      }
-      return (*it).second;
     }
+    Node eq = n.eqNode(pn);
+    eq = Rewriter::rewrite(eq);
+    if (std::find(exp.begin(), exp.end(), eq) == exp.end())
+    {
+      exp.push_back(eq);
+    }
+    return pn;
   }else{
     std::vector< Node > children;
     if (n.getMetaKind() == kind::metakind::PARAMETERIZED) {
@@ -2082,7 +2055,8 @@ void TheoryStrings::checkCycles()
     std::vector< Node > curr;
     std::vector< Node > exp;
     checkCycles( eqc[i], curr, exp );
-    if( hasProcessed() ){
+    if (d_im.hasProcessed())
+    {
       return;
     }
   }
@@ -2143,7 +2117,7 @@ void TheoryStrings::checkFlatForms()
               }
             }
             Node conc = d_false;
-            sendInference(exp, conc, "F_NCTN");
+            d_im.sendInference(exp, conc, "F_NCTN");
             return;
           }
         }
@@ -2212,7 +2186,7 @@ void TheoryStrings::checkFlatForm(std::vector<Node>& eqc,
                   b[d_flat_form_index[b][j]].eqNode(d_emptyString));
             }
             Assert(!conc_c.empty());
-            conc = mkAnd(conc_c);
+            conc = utils::mkAnd(conc_c);
             inf_type = 2;
             Assert(count > 0);
             // swap, will enforce is empty past current
@@ -2248,7 +2222,7 @@ void TheoryStrings::checkFlatForm(std::vector<Node>& eqc,
                   a[d_flat_form_index[a][j]].eqNode(d_emptyString));
             }
             Assert(!conc_c.empty());
-            conc = mkAnd(conc_c);
+            conc = utils::mkAnd(conc_c);
             inf_type = 2;
             Assert(count > 0);
             count--;
@@ -2368,13 +2342,13 @@ void TheoryStrings::checkFlatForm(std::vector<Node>& eqc,
       // strict prefix equality ( a.b = a ) where a,b non-empty
       //  is conflicting by arithmetic len(a.b)=len(a)+len(b)!=len(a)
       //  when len(b)!=0.
-      sendInference(
+      d_im.sendInference(
           exp,
           conc,
-          inf_type == 0
-              ? "F_Const"
-              : (inf_type == 1 ? "F_Unify" : (inf_type == 2 ? "F_EndpointEmp"
-                                                            : "F_EndpointEq")));
+          inf_type == 0 ? "F_Const"
+                        : (inf_type == 1 ? "F_Unify"
+                                         : (inf_type == 2 ? "F_EndpointEmp"
+                                                          : "F_EndpointEq")));
       if (d_conflict)
       {
         return;
@@ -2414,7 +2388,8 @@ Node TheoryStrings::checkCycles( Node eqc, std::vector< Node >& curr, std::vecto
               if( nr!=d_emptyString_r ){
                 std::vector< Node > exp;
                 exp.push_back( n.eqNode( d_emptyString ) );
-                sendInference( exp, n[i].eqNode( d_emptyString ), "I_CYCLE_E" );
+                d_im.sendInference(
+                    exp, n[i].eqNode(d_emptyString), "I_CYCLE_E");
                 return Node::null();
               }
             }else{
@@ -2433,7 +2408,8 @@ Node TheoryStrings::checkCycles( Node eqc, std::vector< Node >& curr, std::vecto
                   for( unsigned j=0; j<n.getNumChildren(); j++ ){
                     //take first non-empty
                     if( j!=i && !areEqual( n[j], d_emptyString ) ){
-                      sendInference( exp, n[j].eqNode( d_emptyString ), "I_CYCLE" );
+                      d_im.sendInference(
+                          exp, n[j].eqNode(d_emptyString), "I_CYCLE");
                       return Node::null();
                     }
                   }
@@ -2444,7 +2420,8 @@ Node TheoryStrings::checkCycles( Node eqc, std::vector< Node >& curr, std::vecto
                   return ncy;
                 }
               }else{
-                if( hasProcessed() ){
+                if (d_im.hasProcessed())
+                {
                   return Node::null();
                 }
               }
@@ -2479,7 +2456,7 @@ void TheoryStrings::checkNormalFormsEq()
     }
   }
 
-  if (hasProcessed())
+  if (d_im.hasProcessed())
   {
     return;
   }
@@ -2495,7 +2472,7 @@ void TheoryStrings::checkNormalFormsEq()
                                    << eqc << std::endl;
     normalizeEquivalenceClass(eqc);
     Trace("strings-debug") << "Finished normalizing eqc..." << std::endl;
-    if (hasProcessed())
+    if (d_im.hasProcessed())
     {
       return;
     }
@@ -2507,11 +2484,12 @@ void TheoryStrings::checkNormalFormsEq()
       NormalForm& nfe_eq = getNormalForm(itn->second);
       // two equivalence classes have same normal form, merge
       std::vector<Node> nf_exp;
-      nf_exp.push_back(mkAnd(nfe.d_exp));
+      nf_exp.push_back(utils::mkAnd(nfe.d_exp));
       nf_exp.push_back(eqc_to_exp[itn->second]);
       Node eq = nfe.d_base.eqNode(nfe_eq.d_base);
-      sendInference(nf_exp, eq, "Normal_Form");
-      if( hasProcessed() ){
+      d_im.sendInference(nf_exp, eq, "Normal_Form");
+      if (d_im.hasProcessed())
+      {
         return;
       }
     }
@@ -2519,7 +2497,7 @@ void TheoryStrings::checkNormalFormsEq()
     {
       nf_to_eqc[nf_term] = eqc;
       eqc_to_nf[eqc] = nf_term;
-      eqc_to_exp[eqc] = mkAnd(nfe.d_exp);
+      eqc_to_exp[eqc] = utils::mkAnd(nfe.d_exp);
     }
     Trace("strings-process-debug")
         << "Done verifying normal forms are the same for " << eqc << std::endl;
@@ -2564,12 +2542,12 @@ void TheoryStrings::checkCodes()
         Node cc = nm->mkNode(kind::STRING_CODE, c);
         cc = Rewriter::rewrite(cc);
         Assert(cc.isConst());
-        NodeNodeMap::const_iterator it = d_proxy_var.find(c);
-        AlwaysAssert(it != d_proxy_var.end());
-        Node vc = nm->mkNode(kind::STRING_CODE, (*it).second);
+        Node cp = getProxyVariableFor(c);
+        AlwaysAssert(!cp.isNull());
+        Node vc = nm->mkNode(STRING_CODE, cp);
         if (!areEqual(cc, vc))
         {
-          sendInference(d_empty_vec, cc.eqNode(vc), "Code_Proxy");
+          d_im.sendInference(d_empty_vec, cc.eqNode(vc), "Code_Proxy");
         }
         const_codes.push_back(vc);
       }
@@ -2583,7 +2561,7 @@ void TheoryStrings::checkCodes()
         }
       }
     }
-    if (hasProcessed())
+    if (d_im.hasProcessed())
     {
       return;
     }
@@ -2606,7 +2584,7 @@ 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);
-          sendInference(d_empty_vec, inj_lem, "Code_Inj");
+          d_im.sendInference(d_empty_vec, inj_lem, "Code_Inj");
         }
       }
     }
@@ -2637,12 +2615,14 @@ void TheoryStrings::normalizeEquivalenceClass( Node eqc ) {
     std::map<Node, unsigned> term_to_nf_index;
     // get the normal forms
     getNormalForms(eqc, normal_forms, term_to_nf_index);
-    if( hasProcessed() ){
+    if (d_im.hasProcessed())
+    {
       return;
     }
     // process the normal forms
     processNEqc(normal_forms);
-    if( hasProcessed() ){
+    if (d_im.hasProcessed())
+    {
       return;
     }
     // debugPrintNormalForms( "strings-solve", eqc, normal_forms );
@@ -2897,7 +2877,7 @@ void TheoryStrings::getNormalForms(Node eqc,
           //TODO: this can be minimized based on firstc/lastc, normal_forms_exp_depend
           exp.insert(exp.end(), nf.d_exp.begin(), nf.d_exp.end());
           Node conc = d_false;
-          sendInference( exp, conc, "N_NCTN" );
+          d_im.sendInference(exp, conc, "N_NCTN");
         }
       }
     }
@@ -2927,9 +2907,12 @@ void TheoryStrings::processNEqc(std::vector<NormalForm>& normal_forms)
         processSimpleNEq(nfi, nfj, rindex, true, 0, pinfer);
         nfi.reverse();
         nfj.reverse();
-        if( hasProcessed() ){
+        if (d_im.hasProcessed())
+        {
           return;
-        }else if( !pinfer.empty() && pinfer.back().d_id==1 ){
+        }
+        else if (!pinfer.empty() && pinfer.back().d_id == 1)
+        {
           break;
         }
         //AJR: for less aggressive endpoint inference
@@ -2937,9 +2920,12 @@ void TheoryStrings::processNEqc(std::vector<NormalForm>& normal_forms)
 
         unsigned index = 0;
         processSimpleNEq(nfi, nfj, index, false, rindex, pinfer);
-        if( hasProcessed() ){
+        if (d_im.hasProcessed())
+        {
           return;
-        }else if( !pinfer.empty() && pinfer.back().d_id==1 ){
+        }
+        else if (!pinfer.empty() && pinfer.back().d_id == 1)
+        {
           break;
         }
       }
@@ -2980,11 +2966,11 @@ void TheoryStrings::processNEqc(std::vector<NormalForm>& normal_forms)
   }
   std::stringstream ssi;
   ssi << pinfer[use_index].d_id;
-  sendInference(pinfer[use_index].d_ant,
-                pinfer[use_index].d_antn,
-                pinfer[use_index].d_conc,
-                ssi.str().c_str(),
-                pinfer[use_index].sendAsLemma());
+  d_im.sendInference(pinfer[use_index].d_ant,
+                     pinfer[use_index].d_antn,
+                     pinfer[use_index].d_conc,
+                     ssi.str().c_str(),
+                     pinfer[use_index].sendAsLemma());
   // Register the new skolems from this inference. We register them here
   // (lazily), since the code above has now decided to use the inference
   // at use_index that involves them.
@@ -3027,7 +3013,6 @@ void TheoryStrings::processSimpleNEq(NormalForm& nfi,
         NormalForm& nfk = index == (nfiv.size() - rproc) ? nfj : nfi;
         std::vector<Node>& nfkv = nfk.d_nf;
         unsigned index_k = index;
-        //Node eq_exp = mkAnd( curr_exp );
         std::vector< Node > curr_exp;
         NormalForm::getExplanationForPrefixEq(nfi, nfj, -1, -1, curr_exp);
         while (!d_conflict && index_k < (nfkv.size() - rproc))
@@ -3036,7 +3021,7 @@ void TheoryStrings::processSimpleNEq(NormalForm& nfi,
           Node eq = nfkv[index_k].eqNode(d_emptyString);
           //Trace("strings-lemma") << "Strings: Infer " << eq << " from " << eq_exp << std::endl;
           Assert(!areEqual(d_emptyString, nfkv[index_k]));
-          sendInference( curr_exp, eq, "N_EndpointEmp" );
+          d_im.sendInference(curr_exp, eq, "N_EndpointEmp");
           index_k++;
         }
       }
@@ -3063,7 +3048,7 @@ void TheoryStrings::processSimpleNEq(NormalForm& nfi,
           NormalForm::getExplanationForPrefixEq(
               nfi, nfj, index, index, temp_exp);
           temp_exp.push_back(length_eq);
-          sendInference( temp_exp, eq, "N_Unify" );
+          d_im.sendInference(temp_exp, eq, "N_Unify");
           return;
         }
         else if ((nfiv[index].getKind() != CONST_STRING
@@ -3093,7 +3078,8 @@ void TheoryStrings::processSimpleNEq(NormalForm& nfi,
             eqn.push_back( mkConcat( eqnc ) );
           }
           if( !areEqual( eqn[0], eqn[1] ) ){
-            sendInference( antec, eqn[0].eqNode( eqn[1] ), "N_EndpointEq", true );
+            d_im.sendInference(
+                antec, eqn[0].eqNode(eqn[1]), "N_EndpointEq", true);
             return;
           }else{
             Assert(nfiv.size() == nfjv.size());
@@ -3136,7 +3122,7 @@ void TheoryStrings::processSimpleNEq(NormalForm& nfi,
             std::vector< Node > antec;
             NormalForm::getExplanationForPrefixEq(
                 nfi, nfj, index, index, antec);
-            sendInference( antec, d_false, "N_Const", true );
+            d_im.sendInference(antec, d_false, "N_Const", true);
             return;
           }
         }else{
@@ -3477,7 +3463,7 @@ TheoryStrings::ProcessLoopResult TheoryStrings::processLoop(NormalForm& nfi,
     {
       Trace("strings-loop") << "Strings::Loop: tails are different."
                             << std::endl;
-      sendInference(info.d_ant, conc, "Loop Conflict", true);
+      d_im.sendInference(info.d_ant, conc, "Loop Conflict", true);
       return ProcessLoopResult::CONFLICT;
     }
   }
@@ -3623,6 +3609,7 @@ TheoryStrings::ProcessLoopResult TheoryStrings::processLoop(NormalForm& nfi,
 
 //return true for lemma, false if we succeed
 void TheoryStrings::processDeq( Node ni, Node nj ) {
+  NodeManager* nm = NodeManager::currentNM();
   //Assert( areDisequal( ni, nj ) );
   NormalForm& nfni = getNormalForm(ni);
   NormalForm& nfnj = getNormalForm(nj);
@@ -3667,7 +3654,7 @@ void TheoryStrings::processDeq( Node ni, Node nj ) {
               if( !d_equalityEngine.areDisequal( nconst_k, d_emptyString, true ) ){
                 Node eq = nconst_k.eqNode( d_emptyString );
                 Node conc = NodeManager::currentNM()->mkNode( kind::OR, eq, eq.negate() );
-                sendInference( d_empty_vec, conc, "D-DISL-Emp-Split" );
+                d_im.sendInference(d_empty_vec, conc, "D-DISL-Emp-Split");
                 return;
               }else{
                 //split on first character
@@ -3678,7 +3665,7 @@ void TheoryStrings::processDeq( Node ni, Node nj ) {
                     return;
                   }else if( !areEqual( firstChar, nconst_k ) ){
                     //splitting on demand : try to make them disequal
-                    if (sendSplit(
+                    if (d_im.sendSplit(
                             firstChar, nconst_k, "S-Split(DEQL-Const)", false))
                     {
                       return;
@@ -3701,9 +3688,14 @@ void TheoryStrings::processDeq( Node ni, Node nj ) {
                   antec.insert(
                       antec.end(), nfnj.d_exp.begin(), nfnj.d_exp.end());
                   antec.push_back( nconst_k.eqNode( d_emptyString ).negate() );
-                  sendInference( antec, NodeManager::currentNM()->mkNode( kind::OR, 
-                                          NodeManager::currentNM()->mkNode( kind::AND, eq1, sk.eqNode( firstChar ).negate() ), eq2 ), "D-DISL-CSplit" );
-                  d_pending_req_phase[ eq1 ] = true;
+                  d_im.sendInference(
+                      antec,
+                      nm->mkNode(
+                          OR,
+                          nm->mkNode(AND, eq1, sk.eqNode(firstChar).negate()),
+                          eq2),
+                      "D-DISL-CSplit");
+                  d_im.sendPhaseRequirement(eq1, true);
                   return;
                 }
               }
@@ -3736,20 +3728,21 @@ void TheoryStrings::processDeq( Node ni, Node nj ) {
               Node lsk2 = mkLength( sk2 );
               conc.push_back( lsk2.eqNode( lj ) );
               conc.push_back( NodeManager::currentNM()->mkNode( kind::OR, j.eqNode( mkConcat( sk1, sk3 ) ), i.eqNode( mkConcat( sk2, sk3 ) ) ) );
-              sendInference( antec, antec_new_lits, NodeManager::currentNM()->mkNode( kind::AND, conc ), "D-DISL-Split" );
+              d_im.sendInference(
+                  antec, antec_new_lits, nm->mkNode(AND, conc), "D-DISL-Split");
               ++(d_statistics.d_deq_splits);
               return;
             }
           }else if( areEqual( li, lj ) ){
             Assert( !areDisequal( i, j ) );
             //splitting on demand : try to make them disequal
-            if (sendSplit(i, j, "S-Split(DEQL)", false))
+            if (d_im.sendSplit(i, j, "S-Split(DEQL)", false))
             {
               return;
             }
           }else{
             //splitting on demand : try to make lengths equal
-            if (sendSplit(li, lj, "D-Split"))
+            if (d_im.sendSplit(li, lj, "D-Split"))
             {
               return;
             }
@@ -3819,7 +3812,7 @@ int TheoryStrings::processSimpleDeq( std::vector< Node >& nfi, std::vector< Node
       }
       Node conc = cc.size()==1 ? cc[0] : NodeManager::currentNM()->mkNode( kind::AND, cc );
       conc = Rewriter::rewrite( conc );
-      sendInference( ant, conc, "Disequality Normalize Empty", true);
+      d_im.sendInference(ant, conc, "Disequality Normalize Empty", true);
       return -1;
     }else{
       Node i = nfi[index];
@@ -4030,179 +4023,6 @@ void TheoryStrings::registerTerm( Node n, int effort ) {
   }
 }
 
-bool TheoryStrings::sendInternalInference(std::vector<Node>& exp,
-                                          Node conc,
-                                          const char* c)
-{
-  if (conc.getKind() == AND
-      || (conc.getKind() == NOT && conc[0].getKind() == OR))
-  {
-    Node conj = conc.getKind() == AND ? conc : conc[0];
-    bool pol = conc.getKind() == AND;
-    bool ret = true;
-    for (const Node& cc : conj)
-    {
-      bool retc = sendInternalInference(exp, pol ? cc : cc.negate(), c);
-      ret = ret && retc;
-    }
-    return ret;
-  }
-  bool pol = conc.getKind() != NOT;
-  Node lit = pol ? conc : conc[0];
-  if (lit.getKind() == EQUAL)
-  {
-    for (unsigned i = 0; i < 2; i++)
-    {
-      if (!lit[i].isConst() && !hasTerm(lit[i]))
-      {
-        // introduces a new non-constant term, do not infer
-        return false;
-      }
-    }
-    // does it already hold?
-    if (pol ? areEqual(lit[0], lit[1]) : areDisequal(lit[0], lit[1]))
-    {
-      return true;
-    }
-  }
-  else if (lit.isConst())
-  {
-    if (lit.getConst<bool>())
-    {
-      Assert(pol);
-      // trivially holds
-      return true;
-    }
-  }
-  else if (!hasTerm(lit))
-  {
-    // introduces a new non-constant term, do not infer
-    return false;
-  }
-  else if (areEqual(lit, pol ? d_true : d_false))
-  {
-    // already holds
-    return true;
-  }
-  sendInference(exp, conc, c);
-  return true;
-}
-
-void TheoryStrings::sendInference( std::vector< Node >& exp, std::vector< Node >& exp_n, Node eq, const char * c, bool asLemma ) {
-  eq = eq.isNull() ? d_false : Rewriter::rewrite( eq );
-  if( eq!=d_true ){
-    if( Trace.isOn("strings-infer-debug") ){
-      Trace("strings-infer-debug") << "By " << c << ", 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;
-      }
-      //Trace("strings-infer-debug") << "as lemma : " << asLemma << std::endl;
-    }
-    //check if we should send a lemma or an inference
-    if( asLemma || eq==d_false || eq.getKind()==kind::OR || !exp_n.empty() || options::stringInferAsLemmas() ){  
-      Node eq_exp;
-      if( options::stringRExplainLemmas() ){
-        eq_exp = mkExplain( exp, exp_n );
-      }else{
-        if( exp.empty() ){
-          eq_exp = mkAnd( exp_n );
-        }else if( exp_n.empty() ){
-          eq_exp = 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( kind::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;
-      }
-      sendLemma( eq_exp, eq, c );
-    }else{
-      sendInfer( mkAnd( exp ), eq, c );
-    }
-  }
-}
-
-void TheoryStrings::sendInference( std::vector< Node >& exp, Node eq, const char * c, bool asLemma ) {
-  std::vector< Node > exp_n;
-  sendInference( exp, exp_n, eq, c, asLemma );
-}
-
-void TheoryStrings::sendLemma( Node ant, Node conc, const char * c ) {
-  if( conc.isNull() || conc == d_false ) {
-    Trace("strings-conflict") << "Strings::Conflict : " << c << " : " << ant << std::endl;
-    Trace("strings-lemma") << "Strings::Conflict : " << c << " : " << ant << std::endl;
-    Trace("strings-assert") << "(assert (not " << ant << ")) ; conflict " << c << std::endl;
-    d_out->conflict(ant);
-    d_conflict = true;
-  } else {
-    Node lem;
-    if( ant == d_true ) {
-      lem = conc;
-    }else{
-      lem = NodeManager::currentNM()->mkNode( kind::IMPLIES, ant, conc );
-    }
-    Trace("strings-lemma") << "Strings::Lemma " << c << " : " << lem << std::endl;
-    Trace("strings-assert") << "(assert " << lem << ") ; lemma " << c << std::endl;
-    d_lemma_cache.push_back( lem );
-  }
-}
-
-void TheoryStrings::sendInfer( Node eq_exp, Node eq, const char * c ) {
-  if( options::stringInferSym() ){
-    std::vector< Node > vars;
-    std::vector< Node > subs;
-    std::vector< Node > unproc;
-    inferSubstitutionProxyVars( eq_exp, vars, subs, unproc );
-    if( unproc.empty() ){
-      Trace("strings-lemma-debug") << "Strings::Infer " << eq << " from " << eq_exp << " by " << c << std::endl;
-      Node eqs = eq.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
-      Trace("strings-lemma-debug") << "Strings::Infer Alternate : " << eqs << std::endl;
-      for( unsigned i=0; i<vars.size(); i++ ){
-        Trace("strings-lemma-debug") << "  " << vars[i] << " -> " << subs[i] << std::endl;
-      }
-      sendLemma( d_true, eqs, c );
-      return;
-    }else{
-      for( unsigned i=0; i<unproc.size(); i++ ){
-        Trace("strings-lemma-debug") << "  non-trivial exp : " << unproc[i] << std::endl;
-      }
-    }
-  }
-  Trace("strings-lemma") << "Strings::Infer " << eq << " from " << eq_exp << " by " << c << std::endl;
-  Trace("strings-assert") << "(assert (=> " << eq_exp << " " << eq << ")) ; infer " << c << std::endl;
-  d_pending.push_back( eq );
-  d_pending_exp[eq] = eq_exp;
-  d_infer.push_back( eq );
-  d_infer_exp.push_back( eq_exp );
-}
-
-bool TheoryStrings::sendSplit(Node a, Node b, const char* c, bool preq)
-{
-  Node eq = a.eqNode( b );
-  eq = Rewriter::rewrite( eq );
-  if (!eq.isConst())
-  {
-    Node neq = NodeManager::currentNM()->mkNode(kind::NOT, eq);
-    Node lemma_or = NodeManager::currentNM()->mkNode(kind::OR, eq, neq);
-    Trace("strings-lemma") << "Strings::Lemma " << c << " SPLIT : " << lemma_or
-                           << std::endl;
-    d_lemma_cache.push_back(lemma_or);
-    d_pending_req_phase[eq] = preq;
-    ++(d_statistics.d_splits);
-    return true;
-  }
-  return false;
-}
-
 void TheoryStrings::registerLength(Node n, LengthStatus s)
 {
   if (d_length_lemma_terms_cache.find(n) != d_length_lemma_terms_cache.end())
@@ -4284,59 +4104,6 @@ void TheoryStrings::registerLength(Node n, LengthStatus s)
   }
 }
 
-void TheoryStrings::inferSubstitutionProxyVars( Node n, std::vector< Node >& vars, std::vector< Node >& subs, std::vector< Node >& unproc ) {
-  if( n.getKind()==kind::AND ){
-    for( unsigned i=0; i<n.getNumChildren(); i++ ){
-      inferSubstitutionProxyVars( n[i], vars, subs, unproc );
-    }
-    return;
-  }else if( n.getKind()==kind::EQUAL ){
-    Node ns = n.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
-    ns = Rewriter::rewrite( ns );
-    if( ns.getKind()==kind::EQUAL ){
-      Node s;
-      Node v;
-      for( unsigned i=0; i<2; i++ ){
-        Node ss;
-        if( ns[i].getAttribute(StringsProxyVarAttribute()) ){
-          ss = ns[i];
-        }else if( ns[i].isConst() ){
-          NodeNodeMap::const_iterator it = d_proxy_var.find( ns[i] );
-          if( it!=d_proxy_var.end() ){
-            ss = (*it).second;
-          }
-        }
-        if( !ss.isNull() ){
-          v = ns[1-i];
-          if( v.getNumChildren()==0 ){
-            if( s.isNull() ){
-              s = ss;
-            }else{
-              //both sides involved in proxy var
-              if( ss==s ){
-                return;
-              }else{
-                s = Node::null();
-              }
-            }
-          }
-        }
-      }
-      if( !s.isNull() ){
-        subs.push_back( s );
-        vars.push_back( v );
-        return;
-      }
-    }else{
-      n = ns;
-    }
-  }
-  if( n!=d_true ){
-    unproc.push_back( n );
-  }
-}
-
-
 Node TheoryStrings::mkConcat( Node n1, Node n2 ) {
   return Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, n1, n2 ) );
 }
@@ -4411,22 +4178,6 @@ Node TheoryStrings::mkExplain( std::vector< Node >& a, std::vector< Node >& an )
   return ant;
 }
 
-Node TheoryStrings::mkAnd( std::vector< Node >& a ) {
-  std::vector< Node > au;
-  for( unsigned i=0; i<a.size(); i++ ){
-    if( std::find( au.begin(), au.end(), a[i] )==au.end() ){
-      au.push_back( a[i] );
-    }
-  }
-  if( au.empty() ) {
-    return d_true;
-  } else if( au.size() == 1 ) {
-    return au[0];
-  } else {
-    return NodeManager::currentNM()->mkNode( kind::AND, au );
-  }
-}
-
 void TheoryStrings::checkNormalFormsDeq()
 {
   std::vector< std::vector< Node > > cols;
@@ -4452,15 +4203,17 @@ void TheoryStrings::checkNormalFormsDeq()
         lt[i] = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, lt[i] );
       }
       if( !areEqual( lt[0], lt[1] ) && !areDisequal( lt[0], lt[1] ) ){
-        sendSplit( lt[0], lt[1], "DEQ-LENGTH-SP" );
+        d_im.sendSplit(lt[0], lt[1], "DEQ-LENGTH-SP");
       }
     }
   }
-  
-  if( !hasProcessed() ){
+
+  if (!d_im.hasProcessed())
+  {
     separateByLength( d_strings_eqc, cols, lts );
     for( unsigned i=0; i<cols.size(); i++ ){
-      if( cols[i].size()>1 && d_lemma_cache.empty() ){
+      if (cols[i].size() > 1 && !d_im.hasPendingLemma())
+      {
         if (Trace.isOn("strings-solve"))
         {
           Trace("strings-solve") << "- Verify disequalities are processed for "
@@ -4492,7 +4245,7 @@ void TheoryStrings::checkNormalFormsDeq()
                   Trace("strings-solve") << "..." << std::endl;
                 }
                 processDeq(cols[i][j], cols[i][k]);
-                if (hasProcessed())
+                if (d_im.hasProcessed())
                 {
                   return;
                 }
@@ -4540,7 +4293,7 @@ void TheoryStrings::checkLengthsEqc() {
           {
             Node eq = llt.eqNode(lcr);
             ei->d_normalized_length.set( eq );
-            sendInference( ant, eq, "LEN-NORM", true );
+            d_im.sendInference(ant, eq, "LEN-NORM", true);
           }
         }
       }else{
@@ -4548,18 +4301,6 @@ void TheoryStrings::checkLengthsEqc() {
         if( !options::stringEagerLen() ){
           Node c = mkConcat(nfi.d_nf);
           registerTerm( c, 3 );
-          /*
-          if( !c.isConst() ){
-            NodeNodeMap::const_iterator it = d_proxy_var.find( c );
-            if( it!=d_proxy_var.end() ){
-              Node pv = (*it).second;
-              Assert( d_proxy_var_to_length.find( pv )!=d_proxy_var_to_length.end() );
-              Node pvl = d_proxy_var_to_length[pv];
-              Node ceq = Rewriter::rewrite( mkLength( pv ).eqNode( pvl ) );
-              sendInference( d_empty_vec, ceq, "LEN-NORM-I", true );
-            }
-          }
-          */
         }
       }
       //} else {
@@ -4626,7 +4367,7 @@ void TheoryStrings::checkCardinality() {
             itr2 != cols[i].end(); ++itr2) {
             if(!areDisequal( *itr1, *itr2 )) {
               // add split lemma
-              if (sendSplit(*itr1, *itr2, "CARD-SP"))
+              if (d_im.sendSplit(*itr1, *itr2, "CARD-SP"))
               {
                 return;
               }
@@ -4654,7 +4395,8 @@ void TheoryStrings::checkCardinality() {
           cons = Rewriter::rewrite( cons );
           ei->d_cardinality_lem_k.set( int_k+1 );
           if( cons!=d_true ){
-            sendInference( d_empty_vec, vec_node, cons, "CARDINALITY", true );
+            d_im.sendInference(
+                d_empty_vec, vec_node, cons, "CARDINALITY", true);
             return;
           }
         }
@@ -4841,8 +4583,8 @@ void TheoryStrings::runInferStep(InferStep s, int effort)
     default: Unreachable(); break;
   }
   Trace("strings-process") << "Done " << s
-                           << ", addedFact = " << !d_pending.empty() << " "
-                           << !d_lemma_cache.empty()
+                           << ", addedFact = " << d_im.hasPendingFact()
+                           << ", addedLemma = " << d_im.hasPendingLemma()
                            << ", d_conflict = " << d_conflict << std::endl;
 }
 
@@ -4944,7 +4686,7 @@ void TheoryStrings::runStrategy(unsigned sbegin, unsigned send)
     InferStep curr = d_infer_steps[i];
     if (curr == BREAK)
     {
-      if (hasProcessed())
+      if (d_im.hasProcessed())
       {
         break;
       }
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index 8371a27ea..a83a6ad12 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -24,6 +24,7 @@
 #include "expr/attribute.h"
 #include "expr/node_trie.h"
 #include "theory/decision_manager.h"
+#include "theory/strings/inference_manager.h"
 #include "theory/strings/normal_form.h"
 #include "theory/strings/regexp_elim.h"
 #include "theory/strings/regexp_operation.h"
@@ -135,6 +136,7 @@ struct StringsProxyVarAttributeId {};
 typedef expr::Attribute< StringsProxyVarAttributeId, bool > StringsProxyVarAttribute;
 
 class TheoryStrings : public Theory {
+  friend class InferenceManager;
   typedef context::CDList<Node> NodeList;
   typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
   typedef context::CDHashMap<Node, int, NodeHashFunction> NodeIntMap;
@@ -298,16 +300,10 @@ class TheoryStrings : public Theory {
   NotifyClass d_notify;
   /** Equaltity engine */
   eq::EqualityEngine d_equalityEngine;
+  /** The (custom) output channel of the theory of strings */
+  InferenceManager d_im;
   /** Are we in conflict */
   context::CDO<bool> d_conflict;
-  //list of pairs of nodes to merge
-  std::map< Node, Node > d_pending_exp;
-  std::vector< Node > d_pending;
-  std::vector< Node > d_lemma_cache;
-  std::map< Node, bool > d_pending_req_phase;
-  /** inferences: maintained to ensure ref count for internally introduced nodes */
-  NodeList d_infer;
-  NodeList d_infer_exp;
   /** map from terms to their normal forms */
   std::map<Node, NormalForm> d_normal_form;
   /** get normal form */
@@ -421,8 +417,21 @@ private:
    * should currently be a representative of the equality engine of this class.
    */
   EqcInfo * getOrMakeEqcInfo( Node eqc, bool doMake = true );
-  //maintain which concat terms have the length lemma instantiated
+  /**
+   * Map string terms to their "proxy variables". Proxy variables are used are
+   * intermediate variables so that length information can be communicated for
+   * constants. For example, to communicate that "ABC" has length 3, we
+   * introduce a proxy variable v_{"ABC"} for "ABC", and assert:
+   *   v_{"ABC"} = "ABC" ^ len( v_{"ABC"} ) = 3
+   * Notice this is required since we cannot directly write len( "ABC" ) = 3,
+   * which rewrites to 3 = 3.
+   * In the above example, we store "ABC" -> v_{"ABC"} in this map.
+   */
   NodeNodeMap d_proxy_var;
+  /**
+   * Map from proxy variables to their normalized length. In the above example,
+   * we store "ABC" -> 3.
+   */
   NodeNodeMap d_proxy_var_to_length;
   /** All the function terms that the theory has seen */
   context::CDList<TNode> d_functionsTerms;
@@ -492,7 +501,23 @@ private:
   SkolemCache d_sk_cache;
 
   void checkConstantEquivalenceClasses( TermIndex* ti, std::vector< Node >& vecc );
-  Node getSymbolicDefinition( Node n, std::vector< Node >& exp );
+  /** Get proxy variable
+   *
+   * If this method returns the proxy variable for (string) term n if one
+   * exists, otherwise it returns null.
+   */
+  Node getProxyVariableFor(Node n) const;
+  /** Get symbolic definition
+   *
+   * This method returns the "symbolic definition" of n, call it n', and
+   * populates the vector exp with an explanation such that exp => n = n'.
+   *
+   * The symbolic definition of n is the term where (maximal) subterms of n
+   * are replaced by their proxy variables. For example, if we introduced
+   * proxy variable v for x ++ y, then given input x ++ y = w, this method
+   * returns v = w and adds v = x ++ y to exp.
+   */
+  Node getSymbolicDefinition(Node n, std::vector<Node>& exp) const;
 
   //--------------------------for checkExtfEval
   /**
@@ -704,11 +729,15 @@ private:
    */
   bool areCareDisequal(TNode x, TNode y);
 
-  // do pending merges
+  /** assert pending fact
+   *
+   * This asserts atom with polarity to the equality engine of this class,
+   * where exp is the explanation of why (~) atom holds.
+   *
+   * This call may trigger further initialization steps involving the terms
+   * of atom, including calls to registerTerm.
+   */
   void assertPendingFact(Node atom, bool polarity, Node exp);
-  void doPendingFacts();
-  void doPendingLemmas();
-  bool hasProcessed();
   /**
    * Adds equality a = b to the vector exp if a and b are distinct terms. It
    * must be the case that areEqual( a, b ) holds in this context.
@@ -736,98 +765,13 @@ private:
    * effort, the call to this method does nothing.
    */
   void registerTerm(Node n, int effort);
-  //-------------------------------------send inferences
- public:
-  /** send internal inferences
-   *
-   * This is called when we have inferred exp => conc, where exp is a set
-   * of equalities and disequalities that hold in the current equality engine.
-   * This method adds equalities and disequalities ~( s = t ) via
-   * sendInference such that both s and t are either constants or terms
-   * that already occur in the equality engine, and ~( s = t ) is a consequence
-   * of conc. This function can be seen as a "conservative" version of
-   * sendInference below in that it does not introduce any new non-constant
-   * terms to the state.
-   *
-   * The argument c is a string identifying the reason for the inference.
-   * This string is used for debugging purposes.
-   *
-   * Return true if the inference is complete, in the sense that we infer
-   * inferences that are equivalent to conc. This returns false e.g. if conc
-   * (or one of its conjuncts if it is a conjunction) was not inferred due
-   * to the criteria mentioned above.
-   */
-  bool sendInternalInference(std::vector<Node>& exp, Node conc, const char* c);
-  /** send inference
-   *
-   * This function should be called when ( exp ^ exp_n ) => eq. The set exp
-   * contains literals that are explainable by this class, i.e. those that
-   * hold in the equality engine of this class. On the other hand, the set
-   * exp_n ("explanations new") contain nodes that are not explainable by this
-   * class. This method may call sendInfer or sendLemma. 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 this
-   * class,
-   *
-   * [3] (Lemma) Indicate that the lemma ( EXPLAIN(exp) ^ exp_n ) => eq should
-   * be sent on the output channel of this class, or
-   *
-   * [4] (Conflict) Immediately report a conflict EXPLAIN(exp) on the output
-   * channel of this class.
-   *
-   * Determining which case to apply depends on the form of eq and whether
-   * exp_n is empty. In particular, lemmas must be used whenever exp_n is
-   * non-empty, conflicts are used when exp_n is empty and eq is false.
-   *
-   * The argument c is a string identifying the reason for inference, used for
-   * debugging.
-   *
-   * If the flag asLemma is true, then this method will send a lemma instead
-   * of an inference whenever applicable.
-   */
-  void sendInference(std::vector<Node>& exp,
-                     std::vector<Node>& exp_n,
-                     Node eq,
-                     const char* c,
-                     bool asLemma = false);
-  /** same as above, but where exp_n is empty */
-  void sendInference(std::vector<Node>& exp,
-                     Node eq,
-                     const char* c,
-                     bool asLemma = false);
+
   /**
    * Are we in conflict? This returns true if this theory has called its output
    * channel's conflict method in the current SAT context.
    */
   bool inConflict() const { return d_conflict; }
 
- protected:
-  /**
-   * 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_lemma_cache, which may be flushed
-   * later within the current call to TheoryStrings::check.
-   *
-   * The argument c is a string identifying the reason for inference, used for
-   * debugging.
-   */
-  void sendLemma(Node ant, Node conc, const char* c);
-  /**
-   * 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, const char* c);
-  bool sendSplit(Node a, Node b, const char* c, bool preq = true);
-  //-------------------------------------end send inferences
-
   /** mkConcat **/
   inline Node mkConcat(Node n1, Node n2);
   inline Node mkConcat(Node n1, Node n2, Node n3);
@@ -839,8 +783,6 @@ private:
   Node mkExplain(std::vector<Node>& a, std::vector<Node>& an);
 
  protected:
-  /** mkAnd **/
-  Node mkAnd(std::vector<Node>& a);
 
   /** get equivalence classes
    *
@@ -861,11 +803,6 @@ private:
                         std::vector<Node>& lts);
   void printConcat(std::vector<Node>& n, const char* c);
 
-  void inferSubstitutionProxyVars(Node n,
-                                  std::vector<Node>& vars,
-                                  std::vector<Node>& subs,
-                                  std::vector<Node>& unproc);
-
   // Symbolic Regular Expression
  private:
   /** regular expression solver module */
diff --git a/src/theory/strings/theory_strings_utils.cpp b/src/theory/strings/theory_strings_utils.cpp
new file mode 100644
index 000000000..42a8af5a1
--- /dev/null
+++ b/src/theory/strings/theory_strings_utils.cpp
@@ -0,0 +1,50 @@
+/*********************                                                        */
+/*! \file theory_strings_utils.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Util functions for theory strings.
+ **
+ ** Util functions for theory strings.
+ **/
+
+#include "theory/strings/theory_strings_utils.h"
+
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace theory {
+namespace strings {
+namespace utils {
+
+Node mkAnd(std::vector<Node>& a)
+{
+  std::vector<Node> au;
+  for (const Node& ai : a)
+  {
+    if (std::find(au.begin(), au.end(), ai) == au.end())
+    {
+      au.push_back(ai);
+    }
+  }
+  if (au.empty())
+  {
+    return NodeManager::currentNM()->mkConst(true);
+  }
+  else if (au.size() == 1)
+  {
+    return au[0];
+  }
+  return NodeManager::currentNM()->mkNode(AND, au);
+}
+
+}  // namespace utils
+}  // namespace strings
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/strings/theory_strings_utils.h b/src/theory/strings/theory_strings_utils.h
new file mode 100644
index 000000000..9e0779e16
--- /dev/null
+++ b/src/theory/strings/theory_strings_utils.h
@@ -0,0 +1,42 @@
+/*********************                                                        */
+/*! \file theory_strings_utils.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Util functions for theory strings.
+ **
+ ** Util functions for theory strings.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__STRINGS__THEORY_STRINGS_UTILS_H
+#define CVC4__THEORY__STRINGS__THEORY_STRINGS_UTILS_H
+
+#include <vector>
+
+#include "expr/node.h"
+
+namespace CVC4 {
+namespace theory {
+namespace strings {
+namespace utils {
+
+/**
+ * Make the conjunction of nodes in a. Removes duplicate conjuncts, returns
+ * true if a is empty, and a single literal if a has size 1.
+ */
+Node mkAnd(std::vector<Node>& a);
+
+}  // namespace utils
+}  // namespace strings
+}  // namespace theory
+}  // namespace CVC4
+
+#endif