Eliminate remaining references to parent TheoryStrings object (#4315)

This PR makes it so that the module dependencies in the theory of strings are acyclic. This is important for further organization towards proofs for strings.

The main change in this PR is to ensure that InferenceManager has a pointer to ExtTheory, which is needed for several of its methods. This required changing several solvers into unique_ptr to properly initialize.

8 files changed, 221 insertions, 196 deletions

diff --git a/src/theory/strings/extf_solver.cpp b/src/theory/strings/extf_solver.cpp
index 1bcd67cb4..775b4a796 100644
--- a/src/theory/strings/extf_solver.cpp
+++ b/src/theory/strings/extf_solver.cpp
@@ -35,7 +35,7 @@ ExtfSolver::ExtfSolver(context::Context* c,
                        StringsRewriter& rewriter,
                        BaseSolver& bs,
                        CoreSolver& cs,
-                       ExtTheory* et,
+                       ExtTheory& et,
                        SequencesStatistics& statistics)
     : d_state(s),
       d_im(im),
@@ -50,19 +50,19 @@ ExtfSolver::ExtfSolver(context::Context* c,
       d_extfInferCache(c),
       d_reduced(u)
 {
-  d_extt->addFunctionKind(kind::STRING_SUBSTR);
-  d_extt->addFunctionKind(kind::STRING_STRIDOF);
-  d_extt->addFunctionKind(kind::STRING_ITOS);
-  d_extt->addFunctionKind(kind::STRING_STOI);
-  d_extt->addFunctionKind(kind::STRING_STRREPL);
-  d_extt->addFunctionKind(kind::STRING_STRREPLALL);
-  d_extt->addFunctionKind(kind::STRING_STRCTN);
-  d_extt->addFunctionKind(kind::STRING_IN_REGEXP);
-  d_extt->addFunctionKind(kind::STRING_LEQ);
-  d_extt->addFunctionKind(kind::STRING_TO_CODE);
-  d_extt->addFunctionKind(kind::STRING_TOLOWER);
-  d_extt->addFunctionKind(kind::STRING_TOUPPER);
-  d_extt->addFunctionKind(kind::STRING_REV);
+  d_extt.addFunctionKind(kind::STRING_SUBSTR);
+  d_extt.addFunctionKind(kind::STRING_STRIDOF);
+  d_extt.addFunctionKind(kind::STRING_ITOS);
+  d_extt.addFunctionKind(kind::STRING_STOI);
+  d_extt.addFunctionKind(kind::STRING_STRREPL);
+  d_extt.addFunctionKind(kind::STRING_STRREPLALL);
+  d_extt.addFunctionKind(kind::STRING_STRCTN);
+  d_extt.addFunctionKind(kind::STRING_IN_REGEXP);
+  d_extt.addFunctionKind(kind::STRING_LEQ);
+  d_extt.addFunctionKind(kind::STRING_TO_CODE);
+  d_extt.addFunctionKind(kind::STRING_TOLOWER);
+  d_extt.addFunctionKind(kind::STRING_TOUPPER);
+  d_extt.addFunctionKind(kind::STRING_REV);
 
   d_true = NodeManager::currentNM()->mkConst(true);
   d_false = NodeManager::currentNM()->mkConst(false);
@@ -126,7 +126,7 @@ bool ExtfSolver::doReduction(int effort, Node n)
           }
           // this depends on the current assertions, so this
           // inference is context-dependent
-          d_extt->markReduced(n, true);
+          d_extt.markReduced(n, true);
           return true;
         }
         else
@@ -173,7 +173,7 @@ bool ExtfSolver::doReduction(int effort, Node n)
     Trace("strings-red-lemma") << "Reduction (positive contains) lemma : " << n
                                << " => " << eq << std::endl;
     // context-dependent because it depends on the polarity of n itself
-    d_extt->markReduced(n, true);
+    d_extt.markReduced(n, true);
   }
   else if (k != kind::STRING_TO_CODE)
   {
@@ -206,7 +206,7 @@ void ExtfSolver::checkExtfReductions(int effort)
   // Notice we don't make a standard call to ExtTheory::doReductions here,
   // since certain optimizations like context-dependent reductions and
   // stratifying effort levels are done in doReduction below.
-  std::vector<Node> extf = d_extt->getActive();
+  std::vector<Node> extf = d_extt.getActive();
   Trace("strings-process") << "  checking " << extf.size() << " active extf"
                            << std::endl;
   for (const Node& n : extf)
@@ -234,7 +234,7 @@ void ExtfSolver::checkExtfEval(int effort)
   d_extfInfoTmp.clear();
   NodeManager* nm = NodeManager::currentNM();
   bool has_nreduce = false;
-  std::vector<Node> terms = d_extt->getActive();
+  std::vector<Node> terms = d_extt.getActive();
   for (const Node& n : terms)
   {
     // Setup information about n, including if it is equal to a constant.
@@ -281,7 +281,7 @@ void ExtfSolver::checkExtfEval(int effort)
       {
         if (effort < 3)
         {
-          d_extt->markReduced(n);
+          d_extt.markReduced(n);
           Trace("strings-extf-debug")
               << "  resolvable by evaluation..." << std::endl;
           std::vector<Node> exps;
@@ -445,7 +445,7 @@ void ExtfSolver::checkExtfEval(int effort)
         }
         Trace("strings-extf-list") << std::endl;
       }
-      if (d_extt->isActive(n) && einfo.d_modelActive)
+      if (d_extt.isActive(n) && einfo.d_modelActive)
       {
         has_nreduce = true;
       }
@@ -525,10 +525,10 @@ void ExtfSolver::checkExtfInference(Node n,
               // we are in conflict
               d_im.sendInference(in.d_exp, conc, Inference::CTN_DECOMPOSE);
             }
-            else if (d_extt->hasFunctionKind(conc.getKind()))
+            else if (d_extt.hasFunctionKind(conc.getKind()))
             {
               // can mark as reduced, since model for n implies model for conc
-              d_extt->markReduced(conc);
+              d_extt.markReduced(conc);
             }
           }
         }
@@ -613,7 +613,7 @@ void ExtfSolver::checkExtfInference(Node n,
         // satisfied by all models of str.contains( x, y ) ^ x=z and thus can
         // be ignored.
         Trace("strings-extf-debug") << "  redundant." << std::endl;
-        d_extt->markReduced(n);
+        d_extt.markReduced(n);
       }
     }
     return;
@@ -680,7 +680,7 @@ bool ExtfSolver::hasExtendedFunctions() const { return d_hasExtf.get(); }
 
 std::vector<Node> ExtfSolver::getActive(Kind k) const
 {
-  return d_extt->getActive(k);
+  return d_extt.getActive(k);
 }
 
 }  // namespace strings
diff --git a/src/theory/strings/extf_solver.h b/src/theory/strings/extf_solver.h
index c5dd24f70..fb9b836db 100644
--- a/src/theory/strings/extf_solver.h
+++ b/src/theory/strings/extf_solver.h
@@ -91,7 +91,7 @@ class ExtfSolver
              StringsRewriter& rewriter,
              BaseSolver& bs,
              CoreSolver& cs,
-             ExtTheory* et,
+             ExtTheory& et,
              SequencesStatistics& statistics);
   ~ExtfSolver();
 
@@ -147,6 +147,7 @@ class ExtfSolver
    * checkExtfEval.
    */
   const std::map<Node, ExtfInfoTmp>& getInfo() const;
+  //---------------------------------- information about ExtTheory
   /** Are there any active extended functions? */
   bool hasExtendedFunctions() const;
   /**
@@ -154,7 +155,7 @@ class ExtfSolver
    * context (see ExtTheory::getActive).
    */
   std::vector<Node> getActive(Kind k) const;
-
+  //---------------------------------- end information about ExtTheory
  private:
   /** do reduction
    *
@@ -190,7 +191,7 @@ class ExtfSolver
   /** reference to the core solver, used for certain queries */
   CoreSolver& d_csolver;
   /** the extended theory object for the theory of strings */
-  ExtTheory* d_extt;
+  ExtTheory& d_extt;
   /** Reference to the statistics for the theory of strings/sequences. */
   SequencesStatistics& d_statistics;
   /** preprocessing utility, for performing strings reductions */
diff --git a/src/theory/strings/inference_manager.cpp b/src/theory/strings/inference_manager.cpp
index b6bbcb7df..9d1c6fac4 100644
--- a/src/theory/strings/inference_manager.cpp
+++ b/src/theory/strings/inference_manager.cpp
@@ -14,11 +14,9 @@
 
 #include "theory/strings/inference_manager.h"
 
-#include "expr/kind.h"
 #include "options/strings_options.h"
 #include "theory/ext_theory.h"
 #include "theory/rewriter.h"
-#include "theory/strings/theory_strings.h"
 #include "theory/strings/theory_strings_utils.h"
 #include "theory/strings/word.h"
 
@@ -30,16 +28,16 @@ namespace CVC4 {
 namespace theory {
 namespace strings {
 
-InferenceManager::InferenceManager(TheoryStrings& p,
-                                   context::Context* c,
+InferenceManager::InferenceManager(context::Context* c,
                                    context::UserContext* u,
                                    SolverState& s,
                                    TermRegistry& tr,
+                                   ExtTheory& e,
                                    OutputChannel& out,
                                    SequencesStatistics& statistics)
-    : d_parent(p),
-      d_state(s),
+    : d_state(s),
       d_termReg(tr),
+      d_extt(e),
       d_out(out),
       d_statistics(statistics),
       d_keep(c)
@@ -51,6 +49,14 @@ InferenceManager::InferenceManager(TheoryStrings& p,
   d_false = nm->mkConst(false);
 }
 
+void InferenceManager::sendAssumption(TNode lit)
+{
+  bool polarity = lit.getKind() != kind::NOT;
+  TNode atom = polarity ? lit : lit[0];
+  // assert pending fact
+  assertPendingFact(atom, polarity, lit);
+}
+
 bool InferenceManager::sendInternalInference(std::vector<Node>& exp,
                                              Node conc,
                                              Inference infer)
@@ -294,6 +300,8 @@ void InferenceManager::sendPhaseRequirement(Node lit, bool pol)
   d_pendingReqPhase[lit] = pol;
 }
 
+void InferenceManager::setIncomplete() { d_out.setIncomplete(); }
+
 void InferenceManager::addToExplanation(Node a,
                                         Node b,
                                         std::vector<Node>& exp) const
@@ -328,14 +336,14 @@ void InferenceManager::doPendingFacts()
       {
         bool polarity = lit.getKind() != NOT;
         TNode atom = polarity ? lit : lit[0];
-        d_parent.assertPendingFact(atom, polarity, exp);
+        assertPendingFact(atom, polarity, exp);
       }
     }
     else
     {
       bool polarity = fact.getKind() != NOT;
       TNode atom = polarity ? fact : fact[0];
-      d_parent.assertPendingFact(atom, polarity, exp);
+      assertPendingFact(atom, polarity, exp);
     }
     i++;
   }
@@ -364,6 +372,68 @@ void InferenceManager::doPendingLemmas()
   d_pendingReqPhase.clear();
 }
 
+void InferenceManager::assertPendingFact(Node atom, bool polarity, Node exp)
+{
+  eq::EqualityEngine* ee = d_state.getEqualityEngine();
+  Trace("strings-pending") << "Assert pending fact : " << atom << " "
+                           << polarity << " from " << exp << std::endl;
+  Assert(atom.getKind() != OR) << "Infer error: a split.";
+  if (atom.getKind() == EQUAL)
+  {
+    // we must ensure these terms are registered
+    Trace("strings-pending-debug") << "  Register term" << std::endl;
+    for (const Node& t : atom)
+    {
+      // terms in the equality engine are already registered, hence skip
+      // currently done for only string-like terms, but this could potentially
+      // be avoided.
+      if (!ee->hasTerm(t) && t.getType().isStringLike())
+      {
+        d_termReg.registerTerm(t, 0);
+      }
+    }
+    Trace("strings-pending-debug") << "  Now assert equality" << std::endl;
+    ee->assertEquality(atom, polarity, exp);
+    Trace("strings-pending-debug") << "  Finished assert equality" << std::endl;
+  }
+  else
+  {
+    ee->assertPredicate(atom, polarity, exp);
+    if (atom.getKind() == STRING_IN_REGEXP)
+    {
+      if (polarity && atom[1].getKind() == REGEXP_CONCAT)
+      {
+        Node eqc = ee->getRepresentative(atom[0]);
+        d_state.addEndpointsToEqcInfo(atom, atom[1], eqc);
+      }
+    }
+  }
+  // process the conflict
+  if (!d_state.isInConflict())
+  {
+    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 = mkExplain(a);
+      d_state.setConflict();
+      Trace("strings-conflict")
+          << "CONFLICT: Eager prefix : " << conflictNode << std::endl;
+      ++(d_statistics.d_conflictsEagerPrefix);
+      d_out.conflict(conflictNode);
+    }
+  }
+  Trace("strings-pending-debug") << "  Now collect terms" << std::endl;
+  // Collect extended function terms in the atom. Notice that we must register
+  // all extended functions occurring in assertions and shared terms. We
+  // make a similar call to registerTermRec in TheoryStrings::addSharedTerm.
+  d_extt.registerTermRec(atom);
+  Trace("strings-pending-debug") << "  Finished collect terms" << std::endl;
+}
+
 bool InferenceManager::hasProcessed() const
 {
   return d_state.isInConflict() || !d_pendingLem.empty() || !d_pending.empty();
@@ -421,7 +491,7 @@ Node InferenceManager::mkExplain(const std::vector<Node>& a,
   }
   else
   {
-    ant = NodeManager::currentNM()->mkNode(kind::AND, antec_exp);
+    ant = NodeManager::currentNM()->mkNode(AND, antec_exp);
   }
   return ant;
 }
@@ -466,18 +536,21 @@ void InferenceManager::explain(TNode literal,
     }
   }
 }
-void InferenceManager::setIncomplete() { d_out.setIncomplete(); }
 
 void InferenceManager::markCongruent(Node a, Node b)
 {
   Assert(a.getKind() == b.getKind());
-  ExtTheory* eth = d_parent.getExtTheory();
-  if (eth->hasFunctionKind(a.getKind()))
+  if (d_extt.hasFunctionKind(a.getKind()))
   {
-    eth->markCongruent(a, b);
+    d_extt.markCongruent(a, b);
   }
 }
 
+void InferenceManager::markReduced(Node n, bool contextDepend)
+{
+  d_extt.markReduced(n, contextDepend);
+}
+
 }  // namespace strings
 }  // namespace theory
 }  // namespace CVC4
diff --git a/src/theory/strings/inference_manager.h b/src/theory/strings/inference_manager.h
index c1550328c..041724d8d 100644
--- a/src/theory/strings/inference_manager.h
+++ b/src/theory/strings/inference_manager.h
@@ -23,6 +23,7 @@
 #include "context/cdhashset.h"
 #include "context/context.h"
 #include "expr/node.h"
+#include "theory/ext_theory.h"
 #include "theory/output_channel.h"
 #include "theory/strings/infer_info.h"
 #include "theory/strings/sequences_stats.h"
@@ -34,8 +35,6 @@ namespace CVC4 {
 namespace theory {
 namespace strings {
 
-class TheoryStrings;
-
 /** Inference Manager
  *
  * The purpose of this class is to process inference steps for strategies
@@ -72,15 +71,22 @@ class InferenceManager
   typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap;
 
  public:
-  InferenceManager(TheoryStrings& p,
-                   context::Context* c,
+  InferenceManager(context::Context* c,
                    context::UserContext* u,
                    SolverState& s,
                    TermRegistry& tr,
+                   ExtTheory& e,
                    OutputChannel& out,
                    SequencesStatistics& statistics);
   ~InferenceManager() {}
 
+  /** send assumption
+   *
+   * This is called when a fact is asserted to TheoryStrings. It adds lit
+   * to the equality engine maintained by this class immediately.
+   */
+  void sendAssumption(TNode lit);
+
   /** send internal inferences
    *
    * This is called when we have inferred exp => conc, where exp is a set
@@ -175,6 +181,12 @@ class InferenceManager
    * decided with polarity pol.
    */
   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
+   * channel's setIncomplete method.
+   */
+  void setIncomplete();
 
   //----------------------------constructing antecedants
   /**
@@ -189,7 +201,7 @@ class InferenceManager
    *
    * 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.
+   * to assertPendingFact.
    *
    * It terminates early if a conflict is encountered, for instance, by
    * equality reasoning within the equality engine.
@@ -239,12 +251,7 @@ class InferenceManager
    * the node corresponding to their conjunction.
    */
   void explain(TNode literal, std::vector<TNode>& assumptions) const;
-  /**
-   * 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
-   * channel's setIncomplete method.
-   */
-  void setIncomplete();
+  // ------------------------------------------------- extended theory
   /**
    * Mark that terms a and b are congruent in the current context.
    * This makes a call to markCongruent in the extended theory object of
@@ -252,8 +259,24 @@ class InferenceManager
    * theory.
    */
   void markCongruent(Node a, Node b);
+  /**
+   * Mark that extended function is reduced. If contextDepend is true,
+   * then this mark is SAT-context dependent, otherwise it is user-context
+   * dependent (see ExtTheory::markReduced).
+   */
+  void markReduced(Node n, bool contextDepend = true);
+  // ------------------------------------------------- end extended theory
 
  private:
+  /** 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);
   /**
    * Indicates that ant => conc should be sent on the output channel of this
    * class. This will either trigger an immediate call to the conflict
@@ -272,14 +295,13 @@ class InferenceManager
    * equality engine of this class.
    */
   void sendInfer(Node eq_exp, Node eq, Inference infer);
-
-  /** the parent theory of strings object */
-  TheoryStrings& d_parent;
   /** Reference to the solver state of the theory of strings. */
   SolverState& d_state;
   /** Reference to the term registry of theory of strings */
   TermRegistry& d_termReg;
-  /** Reference to the output channel of the theory of strings. */
+  /** the extended theory object for the theory of strings */
+  ExtTheory& d_extt;
+  /** A reference to the output channel of the theory of strings. */
   OutputChannel& d_out;
   /** Reference to the statistics for the theory of strings/sequences. */
   SequencesStatistics& d_statistics;
diff --git a/src/theory/strings/regexp_solver.cpp b/src/theory/strings/regexp_solver.cpp
index 540a10a9e..db7e2d836 100644
--- a/src/theory/strings/regexp_solver.cpp
+++ b/src/theory/strings/regexp_solver.cpp
@@ -20,7 +20,6 @@
 
 #include "options/strings_options.h"
 #include "theory/ext_theory.h"
-#include "theory/strings/theory_strings.h"
 #include "theory/strings/theory_strings_utils.h"
 #include "theory/theory_model.h"
 
@@ -32,16 +31,16 @@ namespace CVC4 {
 namespace theory {
 namespace strings {
 
-RegExpSolver::RegExpSolver(TheoryStrings& p,
-                           SolverState& s,
+RegExpSolver::RegExpSolver(SolverState& s,
                            InferenceManager& im,
+                           CoreSolver& cs,
                            ExtfSolver& es,
                            SequencesStatistics& stats,
                            context::Context* c,
                            context::UserContext* u)
-    : d_parent(p),
-      d_state(s),
+    : d_state(s),
       d_im(im),
+      d_csolver(cs),
       d_esolver(es),
       d_statistics(stats),
       d_regexp_ucached(u),
@@ -194,7 +193,7 @@ void RegExpSolver::check(const std::map<Node, std::vector<Node> >& mems)
         Node nx = x;
         if (!x.isConst())
         {
-          nx = d_parent.getNormalString(x, nfexp);
+          nx = d_csolver.getNormalString(x, nfexp);
         }
         // If r is not a constant regular expression, we update it based on
         // normal forms, which may concretize its variables.
@@ -303,7 +302,7 @@ void RegExpSolver::check(const std::map<Node, std::vector<Node> >& mems)
           else
           {
             // otherwise we are incomplete
-            d_parent.getOutputChannel().setIncomplete();
+            d_im.setIncomplete();
           }
         }
         if (d_state.isInConflict())
@@ -367,14 +366,14 @@ bool RegExpSolver::checkEqcInclusion(std::vector<Node>& mems)
           {
             // ~str.in.re(x, R1) includes ~str.in.re(x, R2) --->
             //   mark ~str.in.re(x, R2) as reduced
-            d_parent.getExtTheory()->markReduced(m2Lit);
+            d_im.markReduced(m2Lit);
             remove.insert(m2);
           }
           else
           {
             // str.in.re(x, R1) includes str.in.re(x, R2) --->
             //   mark str.in.re(x, R1) as reduced
-            d_parent.getExtTheory()->markReduced(m1Lit);
+            d_im.markReduced(m1Lit);
             remove.insert(m1);
 
             // We don't need to process m1 anymore
@@ -495,12 +494,12 @@ bool RegExpSolver::checkEqcIntersect(const std::vector<Node>& mems)
     {
       // if R1 = intersect( R1, R2 ), then x in R1 ^ x in R2 is equivalent
       // to x in R1, hence x in R2 can be marked redundant.
-      d_parent.getExtTheory()->markReduced(m);
+      d_im.markReduced(m);
     }
     else if (mres == m)
     {
       // same as above, opposite direction
-      d_parent.getExtTheory()->markReduced(mi);
+      d_im.markReduced(mi);
     }
     else
     {
@@ -515,8 +514,8 @@ bool RegExpSolver::checkEqcIntersect(const std::vector<Node>& mems)
       }
       d_im.sendInference(vec_nodes, mres, Inference::RE_INTER_INFER, true);
       // both are reduced
-      d_parent.getExtTheory()->markReduced(m);
-      d_parent.getExtTheory()->markReduced(mi);
+      d_im.markReduced(m);
+      d_im.markReduced(mi);
       // do not send more than one lemma for this class
       return true;
     }
@@ -660,7 +659,7 @@ Node RegExpSolver::getNormalSymRegExp(Node r, std::vector<Node>& nf_exp)
     {
       if (!r[0].isConst())
       {
-        Node tmp = d_parent.getNormalString(r[0], nf_exp);
+        Node tmp = d_csolver.getNormalString(r[0], nf_exp);
         if (tmp != r[0])
         {
           ret = NodeManager::currentNM()->mkNode(STRING_TO_REGEXP, tmp);
diff --git a/src/theory/strings/regexp_solver.h b/src/theory/strings/regexp_solver.h
index 1d065181b..b44c6c8d9 100644
--- a/src/theory/strings/regexp_solver.h
+++ b/src/theory/strings/regexp_solver.h
@@ -34,8 +34,6 @@ namespace CVC4 {
 namespace theory {
 namespace strings {
 
-class TheoryStrings;
-
 class RegExpSolver
 {
   typedef context::CDList<Node> NodeList;
@@ -46,9 +44,9 @@ class RegExpSolver
   typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
 
  public:
-  RegExpSolver(TheoryStrings& p,
-               SolverState& s,
+  RegExpSolver(SolverState& s,
                InferenceManager& im,
+               CoreSolver& cs,
                ExtfSolver& es,
                SequencesStatistics& stats,
                context::Context* c,
@@ -113,12 +111,12 @@ class RegExpSolver
   Node d_emptyRegexp;
   Node d_true;
   Node d_false;
-  /** the parent of this object */
-  TheoryStrings& d_parent;
   /** The solver state of the parent of this object */
   SolverState& d_state;
   /** the output channel of the parent of this object */
   InferenceManager& d_im;
+  /** reference to the core solver, used for certain queries */
+  CoreSolver& d_csolver;
   /** reference to the extended function solver of the parent */
   ExtfSolver& d_esolver;
   /** Reference to the statistics for the theory of strings/sequences. */
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 3e490f285..9e14d6a3f 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -73,10 +73,10 @@ TheoryStrings::TheoryStrings(context::Context* c,
       d_equalityEngine(d_notify, c, "theory::strings::ee", true),
       d_state(c, d_equalityEngine, d_valuation),
       d_termReg(c, u, d_equalityEngine, out, d_statistics),
-      d_im(*this, c, u, d_state, d_termReg, out, d_statistics),
+      d_im(nullptr),
       d_rewriter(&d_statistics.d_rewrites),
-      d_bsolver(c, u, d_state, d_im),
-      d_csolver(c, u, d_state, d_im, d_termReg, d_bsolver),
+      d_bsolver(nullptr),
+      d_csolver(nullptr),
       d_esolver(nullptr),
       d_rsolver(nullptr),
       d_stringsFmf(c, u, valuation, d_termReg),
@@ -84,18 +84,24 @@ TheoryStrings::TheoryStrings(context::Context* c,
 {
   setupExtTheory();
   ExtTheory* extt = getExtTheory();
+  // initialize the inference manager, which requires the extended theory
+  d_im.reset(
+      new InferenceManager(c, u, d_state, d_termReg, *extt, out, d_statistics));
+  // initialize the solvers
+  d_bsolver.reset(new BaseSolver(c, u, d_state, *d_im));
+  d_csolver.reset(new CoreSolver(c, u, d_state, *d_im, d_termReg, *d_bsolver));
   d_esolver.reset(new ExtfSolver(c,
                                  u,
                                  d_state,
-                                 d_im,
+                                 *d_im,
                                  d_termReg,
                                  d_rewriter,
-                                 d_bsolver,
-                                 d_csolver,
-                                 extt,
+                                 *d_bsolver,
+                                 *d_csolver,
+                                 *extt,
                                  d_statistics));
-  d_rsolver.reset(
-      new RegExpSolver(*this, d_state, d_im, *d_esolver, d_statistics, c, u));
+  d_rsolver.reset(new RegExpSolver(
+      d_state, *d_im, *d_csolver, *d_esolver, d_statistics, c, u));
 
   // The kinds we are treating as function application in congruence
   d_equalityEngine.addFunctionKind(kind::STRING_LENGTH);
@@ -143,11 +149,6 @@ bool TheoryStrings::areCareDisequal( TNode x, TNode y ) {
   return false;
 }
 
-Node TheoryStrings::getNormalString(Node x, std::vector<Node>& nf_exp)
-{
-  return d_csolver.getNormalString(x, nf_exp);
-}
-
 void TheoryStrings::setMasterEqualityEngine(eq::EqualityEngine* eq) {
   d_equalityEngine.setMasterEqualityEngine(eq);
 }
@@ -201,7 +202,7 @@ bool TheoryStrings::propagate(TNode literal) {
 Node TheoryStrings::explain( TNode literal ){
   Debug("strings-explain") << "explain called on " << literal << std::endl;
   std::vector< TNode > assumptions;
-  d_im.explain(literal, assumptions);
+  d_im->explain(literal, assumptions);
   if( assumptions.empty() ){
     return d_true;
   }else if( assumptions.size()==1 ){
@@ -365,7 +366,7 @@ bool TheoryStrings::collectModelInfoType(
       //check if col[i][j] has only variables
       if (!eqc.isConst())
       {
-        NormalForm& nfe = d_csolver.getNormalForm(eqc);
+        NormalForm& nfe = d_csolver->getNormalForm(eqc);
         if (nfe.d_nf.size() == 1)
         {
           // does it have a code and the length of these equivalence classes are
@@ -499,7 +500,7 @@ bool TheoryStrings::collectModelInfoType(
   //step 4 : assign constants to all other equivalence classes
   for( unsigned i=0; i<nodes.size(); i++ ){
     if( processed.find( nodes[i] )==processed.end() ){
-      NormalForm& nf = d_csolver.getNormalForm(nodes[i]);
+      NormalForm& nf = d_csolver->getNormalForm(nodes[i]);
       if (Trace.isOn("strings-model"))
       {
         Trace("strings-model")
@@ -586,8 +587,6 @@ void TheoryStrings::check(Effort e) {
 
   TimerStat::CodeTimer checkTimer(d_checkTime);
 
-  bool polarity;
-  TNode atom;
   // Trace("strings-process") << "Theory of strings, check : " << e << std::endl;
   Trace("strings-check-debug")
       << "Theory of strings, check : " << e << std::endl;
@@ -598,13 +597,9 @@ void TheoryStrings::check(Effort e) {
     TNode fact = assertion.d_assertion;
 
     Trace("strings-assertion") << "get assertion: " << fact << endl;
-    polarity = fact.getKind() != kind::NOT;
-    atom = polarity ? fact : fact[0];
-
-    //assert pending fact
-    assertPendingFact( atom, polarity, fact );
+    d_im->sendAssumption(fact);
   }
-  d_im.doPendingFacts();
+  d_im->doPendingFacts();
 
   Assert(d_strategy_init);
   std::map<Effort, std::pair<unsigned, unsigned> >::iterator itsr =
@@ -661,10 +656,10 @@ void TheoryStrings::check(Effort e) {
       Trace("strings-check") << "  * Run strategy..." << std::endl;
       runStrategy(sbegin, send);
       // flush the facts
-      addedFact = d_im.hasPendingFact();
-      addedLemma = d_im.hasPendingLemma();
-      d_im.doPendingFacts();
-      d_im.doPendingLemmas();
+      addedFact = d_im->hasPendingFact();
+      addedLemma = d_im->hasPendingLemma();
+      d_im->doPendingFacts();
+      d_im->doPendingLemmas();
       if (Trace.isOn("strings-check"))
       {
         Trace("strings-check") << "  ...finish run strategy: ";
@@ -681,8 +676,8 @@ void TheoryStrings::check(Effort e) {
     } while (!d_state.isInConflict() && !addedLemma && addedFact);
   }
   Trace("strings-check") << "Theory of strings, done check : " << e << std::endl;
-  Assert(!d_im.hasPendingFact());
-  Assert(!d_im.hasPendingLemma());
+  Assert(!d_im->hasPendingFact());
+  Assert(!d_im->hasPendingLemma());
 }
 
 bool TheoryStrings::needsCheckLastEffort() {
@@ -831,68 +826,16 @@ void TheoryStrings::computeCareGraph(){
   }
 }
 
-void TheoryStrings::assertPendingFact(Node atom, bool polarity, Node exp) {
-  Trace("strings-pending") << "Assert pending fact : " << atom << " " << polarity << " from " << exp << std::endl;
-  Assert(atom.getKind() != kind::OR) << "Infer error: a split.";
-  if( atom.getKind()==kind::EQUAL ){
-    Trace("strings-pending-debug") << "  Register term" << std::endl;
-    for( unsigned j=0; j<2; j++ ) {
-      if (!d_equalityEngine.hasTerm(atom[j])
-          && atom[j].getType().isStringLike())
-      {
-        d_termReg.registerTerm(atom[j], 0);
-      }
-    }
-    Trace("strings-pending-debug") << "  Now assert equality" << std::endl;
-    d_equalityEngine.assertEquality( atom, polarity, exp );
-    Trace("strings-pending-debug") << "  Finished assert equality" << std::endl;
-  } else {
-    d_equalityEngine.assertPredicate( atom, polarity, exp );
-    if (atom.getKind() == STRING_IN_REGEXP)
-    {
-      if (polarity && atom[1].getKind() == REGEXP_CONCAT)
-      {
-        Node eqc = d_equalityEngine.getRepresentative(atom[0]);
-        d_state.addEndpointsToEqcInfo(atom, atom[1], eqc);
-      }
-    }
-  }
-  // process the conflict
-  if (!d_state.isInConflict())
-  {
-    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);
-      d_state.setConflict();
-      Trace("strings-conflict")
-          << "CONFLICT: Eager prefix : " << conflictNode << std::endl;
-      ++(d_statistics.d_conflictsEagerPrefix);
-      d_out->conflict(conflictNode);
-    }
-  }
-  Trace("strings-pending-debug") << "  Now collect terms" << std::endl;
-  // Collect extended function terms in the atom. Notice that we must register
-  // all extended functions occurring in assertions and shared terms. We
-  // make a similar call to registerTermRec in addSharedTerm.
-  getExtTheory()->registerTermRec( atom );
-  Trace("strings-pending-debug") << "  Finished collect terms" << std::endl;
-}
-
 void TheoryStrings::checkRegisterTermsPreNormalForm()
 {
-  const std::vector<Node>& seqc = d_bsolver.getStringEqc();
+  const std::vector<Node>& seqc = d_bsolver->getStringEqc();
   for (const Node& eqc : seqc)
   {
     eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, &d_equalityEngine);
     while (!eqc_i.isFinished())
     {
       Node n = (*eqc_i);
-      if (!d_bsolver.isCongruent(n))
+      if (!d_bsolver->isCongruent(n))
       {
         d_termReg.registerTerm(n, 2);
       }
@@ -914,10 +857,10 @@ void TheoryStrings::checkCodes()
     // str.code applied to the proxy variables for each equivalence classes that
     // are constants of size one
     std::vector<Node> const_codes;
-    const std::vector<Node>& seqc = d_bsolver.getStringEqc();
+    const std::vector<Node>& seqc = d_bsolver->getStringEqc();
     for (const Node& eqc : seqc)
     {
-      NormalForm& nfe = d_csolver.getNormalForm(eqc);
+      NormalForm& nfe = d_csolver->getNormalForm(eqc);
       if (nfe.d_nf.size() == 1 && nfe.d_nf[0].isConst())
       {
         Node c = nfe.d_nf[0];
@@ -931,7 +874,8 @@ void TheoryStrings::checkCodes()
         Node vc = nm->mkNode(STRING_TO_CODE, cp);
         if (!d_state.areEqual(cc, vc))
         {
-          d_im.sendInference(d_empty_vec, cc.eqNode(vc), Inference::CODE_PROXY);
+          std::vector<Node> emptyVec;
+          d_im->sendInference(emptyVec, cc.eqNode(vc), Inference::CODE_PROXY);
         }
         const_codes.push_back(vc);
       }
@@ -945,7 +889,7 @@ void TheoryStrings::checkCodes()
         }
       }
     }
-    if (d_im.hasProcessed())
+    if (d_im->hasProcessed())
     {
       return;
     }
@@ -968,8 +912,9 @@ 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);
-          d_im.sendInference(d_empty_vec, inj_lem, Inference::CODE_INJ);
+          d_im->sendPhaseRequirement(deq, false);
+          std::vector<Node> emptyVec;
+          d_im->sendInference(emptyVec, inj_lem, Inference::CODE_INJ);
         }
       }
     }
@@ -978,10 +923,10 @@ void TheoryStrings::checkCodes()
 
 void TheoryStrings::checkRegisterTermsNormalForms()
 {
-  const std::vector<Node>& seqc = d_bsolver.getStringEqc();
+  const std::vector<Node>& seqc = d_bsolver->getStringEqc();
   for (const Node& eqc : seqc)
   {
-    NormalForm& nfi = d_csolver.getNormalForm(eqc);
+    NormalForm& nfi = d_csolver->getNormalForm(eqc);
     // check if there is a length term for this equivalence class
     EqcInfo* ei = d_state.getOrMakeEqcInfo(eqc, false);
     Node lt = ei ? ei->d_lengthTerm : Node::null();
@@ -1039,25 +984,25 @@ void TheoryStrings::runInferStep(InferStep s, int effort)
   Trace("strings-process") << "..." << std::endl;
   switch (s)
   {
-    case CHECK_INIT: d_bsolver.checkInit(); break;
-    case CHECK_CONST_EQC: d_bsolver.checkConstantEquivalenceClasses(); break;
+    case CHECK_INIT: d_bsolver->checkInit(); break;
+    case CHECK_CONST_EQC: d_bsolver->checkConstantEquivalenceClasses(); break;
     case CHECK_EXTF_EVAL: d_esolver->checkExtfEval(effort); break;
-    case CHECK_CYCLES: d_csolver.checkCycles(); break;
-    case CHECK_FLAT_FORMS: d_csolver.checkFlatForms(); break;
+    case CHECK_CYCLES: d_csolver->checkCycles(); break;
+    case CHECK_FLAT_FORMS: d_csolver->checkFlatForms(); break;
     case CHECK_REGISTER_TERMS_PRE_NF: checkRegisterTermsPreNormalForm(); break;
-    case CHECK_NORMAL_FORMS_EQ: d_csolver.checkNormalFormsEq(); break;
-    case CHECK_NORMAL_FORMS_DEQ: d_csolver.checkNormalFormsDeq(); break;
+    case CHECK_NORMAL_FORMS_EQ: d_csolver->checkNormalFormsEq(); break;
+    case CHECK_NORMAL_FORMS_DEQ: d_csolver->checkNormalFormsDeq(); break;
     case CHECK_CODES: checkCodes(); break;
-    case CHECK_LENGTH_EQC: d_csolver.checkLengthsEqc(); break;
+    case CHECK_LENGTH_EQC: d_csolver->checkLengthsEqc(); break;
     case CHECK_REGISTER_TERMS_NF: checkRegisterTermsNormalForms(); break;
     case CHECK_EXTF_REDUCTION: d_esolver->checkExtfReductions(effort); break;
     case CHECK_MEMBERSHIP: d_rsolver->checkMemberships(); break;
-    case CHECK_CARDINALITY: d_bsolver.checkCardinality(); break;
+    case CHECK_CARDINALITY: d_bsolver->checkCardinality(); break;
     default: Unreachable(); break;
   }
   Trace("strings-process") << "Done " << s
-                           << ", addedFact = " << d_im.hasPendingFact()
-                           << ", addedLemma = " << d_im.hasPendingLemma()
+                           << ", addedFact = " << d_im->hasPendingFact()
+                           << ", addedLemma = " << d_im->hasPendingLemma()
                            << ", conflict = " << d_state.isInConflict()
                            << std::endl;
 }
@@ -1165,7 +1110,7 @@ void TheoryStrings::runStrategy(unsigned sbegin, unsigned send)
     InferStep curr = d_infer_steps[i];
     if (curr == BREAK)
     {
-      if (d_im.hasProcessed())
+      if (d_im->hasProcessed())
       {
         break;
       }
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index 4a61730f4..2e78198e3 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -200,18 +200,6 @@ class TheoryStrings : public Theory {
     SolverState& d_state;
   };/* class TheoryStrings::NotifyClass */
 
-  //--------------------------- helper functions
-  /** get normal string
-   *
-   * This method returns the node that is equivalent to the normal form of x,
-   * and adds the corresponding explanation to nf_exp.
-   *
-   * For example, if x = y ++ z is an assertion in the current context, then
-   * this method returns the term y ++ z and adds x = y ++ z to nf_exp.
-   */
-  Node getNormalString(Node x, std::vector<Node>& nf_exp);
-  //-------------------------- end helper functions
-
  private:
   // Constants
   Node d_emptyString;
@@ -238,10 +226,9 @@ class TheoryStrings : public Theory {
   /** The term registry for this theory */
   TermRegistry d_termReg;
   /** The (custom) output channel of the theory of strings */
-  InferenceManager d_im;
-  std::vector< Node > d_empty_vec;
-private:
+  std::unique_ptr<InferenceManager> d_im;
 
+ private:
   std::map< Node, Node > d_eqc_to_len_term;
 
 
@@ -318,12 +305,12 @@ private:
    * The base solver, responsible for reasoning about congruent terms and
    * inferring constants for equivalence classes.
    */
-  BaseSolver d_bsolver;
+  std::unique_ptr<BaseSolver> d_bsolver;
   /**
    * The core solver, responsible for reasoning about string concatenation
    * with length constraints.
    */
-  CoreSolver d_csolver;
+  std::unique_ptr<CoreSolver> d_csolver;
   /**
    * Extended function solver, responsible for reductions and simplifications
    * involving extended string functions.