From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 16 Jul 2020 17:10:58 +0000 (-0500)
Subject: Make ExtTheory a utility and not a member of Theory (#4753)
X-Git-Tag: cvc5-1.0.0~3099
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f7559c879d1ebc7d4d9b9f72b0858bdf42c9ed8c;p=cvc5.git

Make ExtTheory a utility and not a member of Theory (#4753)

Previously, we assumed that ExtTheory, the module for doing context-dependent simplification, was one-to-one with Theory. This design is not necessary. This makes this class a utility, which can be used as needed. This makes e.g. the initialization of TheoryStrings much easier, since the ExtTheory object can be created first.
---

diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp
index 97f0ce2c1..12772f4d2 100644
--- a/src/theory/arith/nl/nonlinear_extension.cpp
+++ b/src/theory/arith/nl/nonlinear_extension.cpp
@@ -37,12 +37,18 @@ NonlinearExtension::NonlinearExtension(TheoryArith& containing,
       d_containing(containing),
       d_ee(ee),
       d_needsLastCall(false),
+      d_extTheory(&containing),
       d_model(containing.getSatContext()),
       d_trSlv(d_model),
       d_nlSlv(containing, d_model),
       d_iandSlv(containing, d_model),
       d_builtModel(containing.getSatContext(), false)
 {
+  d_extTheory.addFunctionKind(kind::NONLINEAR_MULT);
+  d_extTheory.addFunctionKind(kind::EXPONENTIAL);
+  d_extTheory.addFunctionKind(kind::SINE);
+  d_extTheory.addFunctionKind(kind::PI);
+  d_extTheory.addFunctionKind(kind::IAND);
   d_true = NodeManager::currentNM()->mkConst(true);
   d_zero = NodeManager::currentNM()->mkConst(Rational(0));
   d_one = NodeManager::currentNM()->mkConst(Rational(1));
@@ -51,6 +57,13 @@ NonlinearExtension::NonlinearExtension(TheoryArith& containing,
 
 NonlinearExtension::~NonlinearExtension() {}
 
+void NonlinearExtension::preRegisterTerm(TNode n)
+{
+  // register terms with extended theory, to find extended terms that can be
+  // eliminated by context-depedendent simplification.
+  d_extTheory.registerTermRec(n);
+}
+
 bool NonlinearExtension::getCurrentSubstitution(
     int effort,
     const std::vector<Node>& vars,
@@ -596,12 +609,12 @@ void NonlinearExtension::check(Theory::Effort e)
                   << ", built model = " << d_builtModel.get() << std::endl;
   if (e == Theory::EFFORT_FULL)
   {
-    d_containing.getExtTheory()->clearCache();
+    d_extTheory.clearCache();
     d_needsLastCall = true;
     if (options::nlExtRewrites())
     {
       std::vector<Node> nred;
-      if (!d_containing.getExtTheory()->doInferences(0, nred))
+      if (!d_extTheory.doInferences(0, nred))
       {
         Trace("nl-ext") << "...sent no lemmas, # extf to reduce = "
                         << nred.size() << std::endl;
@@ -657,7 +670,7 @@ bool NonlinearExtension::modelBasedRefinement(std::vector<NlLemma>& mlems)
 
   // get the extended terms belonging to this theory
   std::vector<Node> xts;
-  d_containing.getExtTheory()->getTerms(xts);
+  d_extTheory.getTerms(xts);
 
   if (Trace.isOn("nl-ext-debug"))
   {
diff --git a/src/theory/arith/nl/nonlinear_extension.h b/src/theory/arith/nl/nonlinear_extension.h
index 69710265c..b4e5df976 100644
--- a/src/theory/arith/nl/nonlinear_extension.h
+++ b/src/theory/arith/nl/nonlinear_extension.h
@@ -32,6 +32,7 @@
 #include "theory/arith/nl/stats.h"
 #include "theory/arith/nl/transcendental_solver.h"
 #include "theory/arith/theory_arith.h"
+#include "theory/ext_theory.h"
 #include "theory/uf/equality_engine.h"
 
 namespace CVC4 {
@@ -70,6 +71,10 @@ class NonlinearExtension
  public:
   NonlinearExtension(TheoryArith& containing, eq::EqualityEngine* ee);
   ~NonlinearExtension();
+  /**
+   * Does non-context dependent setup for a node connected to a theory.
+   */
+  void preRegisterTerm(TNode n);
   /** Get current substitution
    *
    * This function and the one below are
@@ -289,6 +294,8 @@ class NonlinearExtension
   NlStats d_stats;
   // needs last call effort
   bool d_needsLastCall;
+  /** Extended theory, responsible for context-dependent simplification. */
+  ExtTheory d_extTheory;
   /** The non-linear model object
    *
    * This class is responsible for computing model values for arithmetic terms
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index eb5bf3685..fcbfd1baf 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -44,16 +44,6 @@ TheoryArith::TheoryArith(context::Context* c,
       d_proofRecorder(nullptr)
 {
   smtStatisticsRegistry()->registerStat(&d_ppRewriteTimer);
-  // if logic is non-linear
-  if (logicInfo.isTheoryEnabled(THEORY_ARITH) && !logicInfo.isLinear())
-  {
-    setupExtTheory();
-    getExtTheory()->addFunctionKind(kind::NONLINEAR_MULT);
-    getExtTheory()->addFunctionKind(kind::EXPONENTIAL);
-    getExtTheory()->addFunctionKind(kind::SINE);
-    getExtTheory()->addFunctionKind(kind::PI);
-    getExtTheory()->addFunctionKind(kind::IAND);
-  }
 }
 
 TheoryArith::~TheoryArith(){
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index d0da29e7a..39a3a6558 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -1447,7 +1447,7 @@ void TheoryArithPrivate::preRegisterTerm(TNode n) {
 
   if (d_nonlinearExtension != nullptr)
   {
-    d_containing.getExtTheory()->registerTermRec( n );
+    d_nonlinearExtension->preRegisterTerm(n);
   }
 
   try {
diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp
index 668d7b87e..02570b12c 100644
--- a/src/theory/bv/bv_subtheory_core.cpp
+++ b/src/theory/bv/bv_subtheory_core.cpp
@@ -32,17 +32,18 @@ using namespace CVC4::theory;
 using namespace CVC4::theory::bv;
 using namespace CVC4::theory::bv::utils;
 
-CoreSolver::CoreSolver(context::Context* c, TheoryBV* bv)
-  : SubtheorySolver(c, bv),
-    d_notify(*this),
-    d_equalityEngine(d_notify, c, "theory::bv::ee", true),
-    d_slicer(new Slicer()),
-    d_isComplete(c, true),
-    d_lemmaThreshold(16),
-    d_useSlicer(false),
-    d_preregisterCalled(false),
-    d_checkCalled(false),
-    d_reasons(c)
+CoreSolver::CoreSolver(context::Context* c, TheoryBV* bv, ExtTheory* extt)
+    : SubtheorySolver(c, bv),
+      d_notify(*this),
+      d_equalityEngine(d_notify, c, "theory::bv::ee", true),
+      d_slicer(new Slicer()),
+      d_isComplete(c, true),
+      d_lemmaThreshold(16),
+      d_useSlicer(false),
+      d_preregisterCalled(false),
+      d_checkCalled(false),
+      d_extTheory(extt),
+      d_reasons(c)
 {
   // The kinds we are treating as function application in congruence
   d_equalityEngine.addFunctionKind(kind::BITVECTOR_CONCAT, true);
@@ -411,10 +412,7 @@ void CoreSolver::conflict(TNode a, TNode b) {
   d_bv->setConflict(conflict);
 }
 
-void CoreSolver::eqNotifyNewClass(TNode t) {
-  Assert(d_bv->getExtTheory() != NULL);
-  d_bv->getExtTheory()->registerTerm( t );
-}
+void CoreSolver::eqNotifyNewClass(TNode t) { d_extTheory->registerTerm(t); }
 
 bool CoreSolver::isCompleteForTerm(TNode term, TNodeBoolMap& seen) {
   if (d_useSlicer)
diff --git a/src/theory/bv/bv_subtheory_core.h b/src/theory/bv/bv_subtheory_core.h
index a9ca57fb4..8f4f9089a 100644
--- a/src/theory/bv/bv_subtheory_core.h
+++ b/src/theory/bv/bv_subtheory_core.h
@@ -24,6 +24,7 @@
 #include "context/cdhashmap.h"
 #include "context/cdhashset.h"
 #include "theory/bv/bv_subtheory.h"
+#include "theory/ext_theory.h"
 
 namespace CVC4 {
 namespace theory {
@@ -90,7 +91,10 @@ class CoreSolver : public SubtheorySolver {
   bool d_useSlicer;
   bool d_preregisterCalled;
   bool d_checkCalled;
-  
+
+  /** Pointer to the extended theory module. */
+  ExtTheory* d_extTheory;
+
   /** To make sure we keep the explanations */
   context::CDHashSet<Node, NodeHashFunction> d_reasons;
   ModelValue d_modelValues;
@@ -101,18 +105,18 @@ class CoreSolver : public SubtheorySolver {
   bool isCompleteForTerm(TNode term, TNodeBoolMap& seen);
   Statistics d_statistics;
 public:
-  CoreSolver(context::Context* c, TheoryBV* bv);
-  ~CoreSolver();
-  bool isComplete() override { return d_isComplete; }
-  void  setMasterEqualityEngine(eq::EqualityEngine* eq);
-  void preRegister(TNode node) override;
-  bool check(Theory::Effort e) override;
-  void explain(TNode literal, std::vector<TNode>& assumptions) override;
-  bool collectModelInfo(TheoryModel* m, bool fullModel) override;
-  Node getModelValue(TNode var) override;
-  void addSharedTerm(TNode t) override
-  {
-    d_equalityEngine.addTriggerTerm(t, THEORY_BV);
+ CoreSolver(context::Context* c, TheoryBV* bv, ExtTheory* extt);
+ ~CoreSolver();
+ bool isComplete() override { return d_isComplete; }
+ void setMasterEqualityEngine(eq::EqualityEngine* eq);
+ void preRegister(TNode node) override;
+ bool check(Theory::Effort e) override;
+ void explain(TNode literal, std::vector<TNode>& assumptions) override;
+ bool collectModelInfo(TheoryModel* m, bool fullModel) override;
+ Node getModelValue(TNode var) override;
+ void addSharedTerm(TNode t) override
+ {
+   d_equalityEngine.addTriggerTerm(t, THEORY_BV);
   }
   EqualityStatus getEqualityStatus(TNode a, TNode b) override
   {
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index c8e585d88..0a4499c11 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -66,6 +66,7 @@ TheoryBV::TheoryBV(context::Context* c,
       d_invalidateModelCache(c, true),
       d_literalsToPropagate(c),
       d_literalsToPropagateIndex(c, 0),
+      d_extTheory(new ExtTheory(this)),
       d_propagatedBy(c),
       d_eagerSolver(),
       d_abstractionModule(new AbstractionModule(getStatsPrefix(THEORY_BV))),
@@ -75,9 +76,8 @@ TheoryBV::TheoryBV(context::Context* c,
       d_extf_range_infer(u),
       d_extf_collapse_infer(u)
 {
-  setupExtTheory();
-  getExtTheory()->addFunctionKind(kind::BITVECTOR_TO_NAT);
-  getExtTheory()->addFunctionKind(kind::INT_TO_BITVECTOR);
+  d_extTheory->addFunctionKind(kind::BITVECTOR_TO_NAT);
+  d_extTheory->addFunctionKind(kind::INT_TO_BITVECTOR);
   if (options::bitblastMode() == options::BitblastMode::EAGER)
   {
     d_eagerSolver.reset(new EagerBitblastSolver(c, this));
@@ -86,7 +86,7 @@ TheoryBV::TheoryBV(context::Context* c,
 
   if (options::bitvectorEqualitySolver() && !options::proof())
   {
-    d_subtheories.emplace_back(new CoreSolver(c, this));
+    d_subtheories.emplace_back(new CoreSolver(c, this, d_extTheory.get()));
     d_subtheoryMap[SUB_CORE] = d_subtheories.back().get();
   }
 
@@ -262,9 +262,10 @@ void TheoryBV::preRegisterTerm(TNode node) {
   for (unsigned i = 0; i < d_subtheories.size(); ++i) {
     d_subtheories[i]->preRegister(node);
   }
-  
-  // AJR : equality solver currently registers all terms to ExtTheory, if we want a lazy reduction without the bv equality solver, need to call this
-  //getExtTheory()->registerTermRec( node );
+
+  // AJR : equality solver currently registers all terms to ExtTheory, if we
+  // want a lazy reduction without the bv equality solver, need to call this
+  // d_extTheory->registerTermRec( node );
 }
 
 void TheoryBV::sendConflict() {
@@ -319,7 +320,7 @@ void TheoryBV::check(Effort e)
   
   //last call : do reductions on extended bitvector functions
   if (e == Theory::EFFORT_LAST_CALL) {
-    std::vector<Node> nred = getExtTheory()->getActive();
+    std::vector<Node> nred = d_extTheory->getActive();
     doExtfReductions(nred);
     return;
   }
@@ -404,7 +405,8 @@ void TheoryBV::check(Effort e)
   if (Theory::fullEffort(e)) {
     //do inferences (adds external lemmas)  TODO: this can be improved to add internal inferences
     std::vector< Node > nred;
-    if( getExtTheory()->doInferences( 0, nred ) ){
+    if (d_extTheory->doInferences(0, nred))
+    {
       return;
     }
     d_needsLastCallCheck = false;
@@ -513,7 +515,8 @@ bool TheoryBV::doExtfInferences(std::vector<Node>& terms)
 
 bool TheoryBV::doExtfReductions( std::vector< Node >& terms ) {
   std::vector< Node > nredr;
-  if( getExtTheory()->doReductions( 0, terms, nredr ) ){
+  if (d_extTheory->doReductions(0, terms, nredr))
+  {
     return true;
   }
   Assert(nredr.empty());
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index c98de0f18..b0991c8b0 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -38,10 +38,11 @@ namespace CVC4 {
 namespace proof {
 class BitVectorProof;
 }
-}  // namespace CVC4
 
-namespace CVC4 {
 namespace theory {
+
+class ExtTheory;
+
 namespace bv {
 
 class CoreSolver;
@@ -180,6 +181,9 @@ class TheoryBV : public Theory {
   /** Index of the next literal to propagate */
   context::CDO<unsigned> d_literalsToPropagateIndex;
 
+  /** Extended theory module, for context-dependent simplification. */
+  std::unique_ptr<ExtTheory> d_extTheory;
+
   /**
    * Keeps a map from nodes to the subtheory that propagated it so that we can explain it
    * properly.
diff --git a/src/theory/strings/extf_solver.cpp b/src/theory/strings/extf_solver.cpp
index 9b1b0e6dd..eff0b3d74 100644
--- a/src/theory/strings/extf_solver.cpp
+++ b/src/theory/strings/extf_solver.cpp
@@ -74,6 +74,8 @@ ExtfSolver::ExtfSolver(context::Context* c,
 
 ExtfSolver::~ExtfSolver() {}
 
+void ExtfSolver::addSharedTerm(TNode n) { d_extt.registerTermRec(n); }
+
 bool ExtfSolver::doReduction(int effort, Node n)
 {
   Assert(d_extfInfoTmp.find(n) != d_extfInfoTmp.end());
diff --git a/src/theory/strings/extf_solver.h b/src/theory/strings/extf_solver.h
index d99a881f6..80921550e 100644
--- a/src/theory/strings/extf_solver.h
+++ b/src/theory/strings/extf_solver.h
@@ -95,6 +95,11 @@ class ExtfSolver
              SequencesStatistics& statistics);
   ~ExtfSolver();
 
+  /**
+   * Called when a shared term is added to theory of strings, this registers
+   * n with the extended theory utility for context-depdendent simplification.
+   */
+  void addSharedTerm(TNode n);
   /** check extended functions evaluation
    *
    * This applies "context-dependent simplification" for all active extended
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 150ea8977..03f9d8d1c 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -46,35 +46,24 @@ TheoryStrings::TheoryStrings(context::Context* c,
       d_equalityEngine(d_notify, c, "theory::strings::ee", true),
       d_state(c, u, d_equalityEngine, d_valuation),
       d_termReg(d_state, d_equalityEngine, out, d_statistics, nullptr),
-      d_im(nullptr),
+      d_extTheory(this),
+      d_im(c, u, d_state, d_termReg, d_extTheory, out, d_statistics),
       d_rewriter(&d_statistics.d_rewrites),
-      d_bsolver(nullptr),
-      d_csolver(nullptr),
-      d_esolver(nullptr),
-      d_rsolver(nullptr),
+      d_bsolver(d_state, d_im),
+      d_csolver(c, u, d_state, d_im, d_termReg, d_bsolver),
+      d_esolver(c,
+                u,
+                d_state,
+                d_im,
+                d_termReg,
+                d_rewriter,
+                d_bsolver,
+                d_csolver,
+                d_extTheory,
+                d_statistics),
+      d_rsolver(d_state, d_im, d_csolver, d_esolver, d_statistics, c, u),
       d_stringsFmf(c, u, valuation, d_termReg)
 {
-  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(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_termReg,
-                                 d_rewriter,
-                                 *d_bsolver,
-                                 *d_csolver,
-                                 *extt,
-                                 d_statistics));
-  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);
   d_equalityEngine.addFunctionKind(kind::STRING_CONCAT);
@@ -152,7 +141,7 @@ void TheoryStrings::addSharedTerm(TNode t) {
   d_equalityEngine.addTriggerTerm(t, THEORY_STRINGS);
   if (options::stringExp())
   {
-    getExtTheory()->registerTermRec(t);
+    d_esolver.addSharedTerm(t);
   }
   Debug("strings") << "TheoryStrings::addSharedTerm() finished" << std::endl;
 }
@@ -195,7 +184,7 @@ TrustNode 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);
   Node ret;
   if( assumptions.empty() ){
     ret = d_true;
@@ -213,7 +202,7 @@ bool TheoryStrings::getCurrentSubstitution( int effort, std::vector< Node >& var
   for( unsigned i=0; i<vars.size(); i++ ){
     Node n = vars[i];
     Trace("strings-subs") << "  get subs for " << n << "..." << std::endl;
-    Node s = d_esolver->getCurrentSubstitutionFor(effort, n, exp[n]);
+    Node s = d_esolver.getCurrentSubstitutionFor(effort, n, exp[n]);
     subs.push_back(s);
   }
   return true;
@@ -364,7 +353,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)
         {
           // is it an equivalence class with a seq.unit term?
@@ -516,7 +505,7 @@ bool TheoryStrings::collectModelInfoType(
   {
     if (processed.find(rn) == processed.end())
     {
-      NormalForm& nf = d_csolver->getNormalForm(rn);
+      NormalForm& nf = d_csolver.getNormalForm(rn);
       if (Trace.isOn("strings-model"))
       {
         Trace("strings-model")
@@ -625,9 +614,9 @@ void TheoryStrings::check(Effort e) {
     TNode fact = assertion.d_assertion;
 
     Trace("strings-assertion") << "get assertion: " << fact << endl;
-    d_im->sendAssumption(fact);
+    d_im.sendAssumption(fact);
   }
-  d_im->doPendingFacts();
+  d_im.doPendingFacts();
 
   Assert(d_strat.isStrategyInit());
   if (!d_state.isInConflict() && !d_valuation.needCheck()
@@ -680,10 +669,10 @@ void TheoryStrings::check(Effort e) {
       Trace("strings-check") << "  * Run strategy..." << std::endl;
       runStrategy(e);
       // 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: ";
@@ -700,13 +689,13 @@ 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() {
   if( options::stringGuessModel() ){
-    return d_esolver->hasExtendedFunctions();
+    return d_esolver.hasExtendedFunctions();
   }
   return false;
 }
@@ -853,14 +842,14 @@ void TheoryStrings::computeCareGraph(){
 
 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);
       }
@@ -882,10 +871,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];
@@ -900,7 +889,7 @@ void TheoryStrings::checkCodes()
         if (!d_state.areEqual(cc, vc))
         {
           std::vector<Node> emptyVec;
-          d_im->sendInference(emptyVec, cc.eqNode(vc), Inference::CODE_PROXY);
+          d_im.sendInference(emptyVec, cc.eqNode(vc), Inference::CODE_PROXY);
         }
         const_codes.push_back(vc);
       }
@@ -914,7 +903,7 @@ void TheoryStrings::checkCodes()
         }
       }
     }
-    if (d_im->hasProcessed())
+    if (d_im.hasProcessed())
     {
       return;
     }
@@ -937,9 +926,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.sendPhaseRequirement(deq, false);
           std::vector<Node> emptyVec;
-          d_im->sendInference(emptyVec, inj_lem, Inference::CODE_INJ);
+          d_im.sendInference(emptyVec, inj_lem, Inference::CODE_INJ);
         }
       }
     }
@@ -948,10 +937,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();
@@ -982,7 +971,7 @@ TrustNode TheoryStrings::ppRewrite(TNode atom)
   if( !options::stringLazyPreproc() ){
     //eager preprocess here
     std::vector< Node > new_nodes;
-    StringsPreprocess* p = d_esolver->getPreprocess();
+    StringsPreprocess* p = d_esolver.getPreprocess();
     Node ret = p->processAssertion(atomRet, new_nodes);
     if (ret != atomRet)
     {
@@ -1018,25 +1007,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_EXTF_EVAL: d_esolver->checkExtfEval(effort); break;
-    case CHECK_CYCLES: d_csolver->checkCycles(); break;
-    case CHECK_FLAT_FORMS: d_csolver->checkFlatForms(); 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_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_EXTF_REDUCTION: d_esolver.checkExtfReductions(effort); break;
+    case CHECK_MEMBERSHIP: d_rsolver.checkMemberships(); 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;
 }
@@ -1053,7 +1042,7 @@ void TheoryStrings::runStrategy(Theory::Effort e)
     InferStep curr = it->first;
     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 dfaa99c06..29c3cd64c 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -25,6 +25,7 @@
 #include "context/cdhashset.h"
 #include "context/cdlist.h"
 #include "expr/node_trie.h"
+#include "theory/ext_theory.h"
 #include "theory/strings/base_solver.h"
 #include "theory/strings/core_solver.h"
 #include "theory/strings/extf_solver.h"
@@ -275,27 +276,29 @@ class TheoryStrings : public Theory {
   SolverState d_state;
   /** The term registry for this theory */
   TermRegistry d_termReg;
+  /** Extended theory, responsible for context-dependent simplification. */
+  ExtTheory d_extTheory;
   /** The (custom) output channel of the theory of strings */
-  std::unique_ptr<InferenceManager> d_im;
+  InferenceManager d_im;
   /** The theory rewriter for this theory. */
   StringsRewriter d_rewriter;
   /**
    * The base solver, responsible for reasoning about congruent terms and
    * inferring constants for equivalence classes.
    */
-  std::unique_ptr<BaseSolver> d_bsolver;
+  BaseSolver d_bsolver;
   /**
    * The core solver, responsible for reasoning about string concatenation
    * with length constraints.
    */
-  std::unique_ptr<CoreSolver> d_csolver;
+  CoreSolver d_csolver;
   /**
    * Extended function solver, responsible for reductions and simplifications
    * involving extended string functions.
    */
-  std::unique_ptr<ExtfSolver> d_esolver;
+  ExtfSolver d_esolver;
   /** regular expression solver module */
-  std::unique_ptr<RegExpSolver> d_rsolver;
+  RegExpSolver d_rsolver;
   /** regular expression elimination module */
   RegExpElimination d_regexp_elim;
   /** Strings finite model finding decision strategy */
diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp
index b0db8ab30..f6532b1e5 100644
--- a/src/theory/theory.cpp
+++ b/src/theory/theory.cpp
@@ -74,7 +74,6 @@ Theory::Theory(TheoryId id,
       d_careGraph(NULL),
       d_quantEngine(NULL),
       d_decManager(nullptr),
-      d_extTheory(NULL),
       d_checkTime(getStatsPrefix(id) + name + "::checkTime"),
       d_computeCareGraphTime(getStatsPrefix(id) + name
                              + "::computeCareGraphTime"),
@@ -90,8 +89,6 @@ Theory::Theory(TheoryId id,
 Theory::~Theory() {
   smtStatisticsRegistry()->unregisterStat(&d_checkTime);
   smtStatisticsRegistry()->unregisterStat(&d_computeCareGraphTime);
-
-  delete d_extTheory;
 }
 
 TheoryId Theory::theoryOf(options::TheoryOfMode mode, TNode node)
@@ -395,11 +392,6 @@ std::pair<bool, Node> Theory::entailmentCheck(TNode lit)
   return make_pair(false, Node::null());
 }
 
-ExtTheory* Theory::getExtTheory() {
-  Assert(d_extTheory != NULL);
-  return d_extTheory;
-}
-
 void Theory::addCarePair(TNode t1, TNode t2) {
   if (d_careGraph) {
     d_careGraph->insert(CarePair(t1, t2, d_id));
@@ -429,10 +421,5 @@ void Theory::setDecisionManager(DecisionManager* dm)
   d_decManager = dm;
 }
 
-void Theory::setupExtTheory() {
-  Assert(d_extTheory == NULL);
-  d_extTheory = new ExtTheory(this);
-}
-
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/theory.h b/src/theory/theory.h
index 1dead8183..fecdafb17 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -57,7 +57,6 @@ namespace theory {
 class QuantifiersEngine;
 class TheoryModel;
 class SubstitutionMap;
-class ExtTheory;
 class TheoryRewriter;
 
 namespace rrinst {
@@ -136,9 +135,6 @@ class Theory {
   /** Pointer to the decision manager. */
   DecisionManager* d_decManager;
 
-  /** Extended theory module or NULL. Owned by the theory. */
-  ExtTheory* d_extTheory;
-
  protected:
 
   // === STATISTICS ===
@@ -845,9 +841,6 @@ class Theory {
   /* equality engine TODO: use? */
   virtual eq::EqualityEngine* getEqualityEngine() { return NULL; }
 
-  /* Get extended theory if one has been installed. */
-  ExtTheory* getExtTheory();
-
   /* get current substitution at an effort
    *   input : vars
    *   output : subs, exp