Split ext theory to own file and document (#1809)

11 files changed, 808 insertions, 501 deletions

diff --git a/src/Makefile.am b/src/Makefile.am
index 917fc6ef3..71a66db59 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -369,6 +369,8 @@ libcvc4_la_SOURCES = \
 	theory/datatypes/theory_datatypes_type_rules.h \
 	theory/datatypes/type_enumerator.cpp \
 	theory/datatypes/type_enumerator.h \
+	theory/ext_theory.cpp \
+	theory/ext_theory.h \
 	theory/fp/theory_fp.cpp \
 	theory/fp/theory_fp.h \
 	theory/fp/theory_fp_rewriter.cpp \
diff --git a/src/theory/arith/nonlinear_extension.cpp b/src/theory/arith/nonlinear_extension.cpp
index 98c426339..8380014f3 100644
--- a/src/theory/arith/nonlinear_extension.cpp
+++ b/src/theory/arith/nonlinear_extension.cpp
@@ -25,6 +25,7 @@
 #include "theory/arith/arith_msum.h"
 #include "theory/arith/arith_utilities.h"
 #include "theory/arith/theory_arith.h"
+#include "theory/ext_theory.h"
 #include "theory/quantifiers/quant_util.h"
 #include "theory/theory_model.h"
 
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 9a36f5eab..d7113b17d 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -21,6 +21,7 @@
 #include "smt/smt_statistics_registry.h"
 #include "theory/arith/infer_bounds.h"
 #include "theory/arith/theory_arith_private.h"
+#include "theory/ext_theory.h"
 
 using namespace std;
 using namespace CVC4::kind;
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index 81bf91992..ad0ce2e86 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -43,26 +43,22 @@
 #include "theory/arith/approx_simplex.h"
 #include "theory/arith/arith_ite_utils.h"
 #include "theory/arith/arith_rewriter.h"
-#include "theory/arith/arith_rewriter.h"
 #include "theory/arith/arith_static_learner.h"
 #include "theory/arith/arith_utilities.h"
 #include "theory/arith/arithvar.h"
 #include "theory/arith/congruence_manager.h"
 #include "theory/arith/constraint.h"
-#include "theory/arith/constraint.h"
 #include "theory/arith/cut_log.h"
 #include "theory/arith/delta_rational.h"
-#include "theory/arith/delta_rational.h"
 #include "theory/arith/dio_solver.h"
 #include "theory/arith/linear_equality.h"
 #include "theory/arith/matrix.h"
-#include "theory/arith/matrix.h"
 #include "theory/arith/nonlinear_extension.h"
 #include "theory/arith/normal_form.h"
 #include "theory/arith/partial_model.h"
-#include "theory/arith/partial_model.h"
 #include "theory/arith/simplex.h"
 #include "theory/arith/theory_arith.h"
+#include "theory/ext_theory.h"
 #include "theory/ite_utilities.h"
 #include "theory/quantifiers/fmf/bounded_integers.h"
 #include "theory/rewriter.h"
diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp
index d648997cb..b3c3f73f3 100644
--- a/src/theory/bv/bv_subtheory_core.cpp
+++ b/src/theory/bv/bv_subtheory_core.cpp
@@ -22,6 +22,7 @@
 #include "theory/bv/slicer.h"
 #include "theory/bv/theory_bv.h"
 #include "theory/bv/theory_bv_utils.h"
+#include "theory/ext_theory.h"
 #include "theory/theory_model.h"
 
 using namespace std;
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 3b434f143..7dc6d3710 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -17,6 +17,8 @@
 
 #include "options/bv_options.h"
 #include "options/smt_options.h"
+#include "proof/proof_manager.h"
+#include "proof/theory_proof.h"
 #include "smt/smt_statistics_registry.h"
 #include "theory/bv/abstraction.h"
 #include "theory/bv/bv_eager_solver.h"
@@ -29,9 +31,8 @@
 #include "theory/bv/theory_bv_rewrite_rules_simplification.h"
 #include "theory/bv/theory_bv_rewriter.h"
 #include "theory/bv/theory_bv_utils.h"
+#include "theory/ext_theory.h"
 #include "theory/theory_model.h"
-#include "proof/theory_proof.h"
-#include "proof/proof_manager.h"
 #include "theory/valuation.h"
 
 using namespace CVC4::context;
diff --git a/src/theory/ext_theory.cpp b/src/theory/ext_theory.cpp
new file mode 100644
index 000000000..7cc8627eb
--- /dev/null
+++ b/src/theory/ext_theory.cpp
@@ -0,0 +1,544 @@
+/*********************                                                        */
+/*! \file ext_theory.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Tim King, Andrew Reynolds, Dejan Jovanovic
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 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 Extended theory interface.
+ **
+ ** This implements a generic module, used by theory solvers, for performing
+ ** "context-dependent simplification", as described in Reynolds et al
+ ** "Designing Theory Solvers with Extensions", FroCoS 2017.
+ **/
+
+#include "theory/ext_theory.h"
+
+#include "base/cvc4_assert.h"
+#include "smt/smt_statistics_registry.h"
+#include "theory/quantifiers_engine.h"
+#include "theory/substitutions.h"
+
+using namespace std;
+
+namespace CVC4 {
+namespace theory {
+
+ExtTheory::ExtTheory(Theory* p, bool cacheEnabled)
+    : d_parent(p),
+      d_ext_func_terms(p->getSatContext()),
+      d_ci_inactive(p->getUserContext()),
+      d_has_extf(p->getSatContext()),
+      d_lemmas(p->getUserContext()),
+      d_pp_lemmas(p->getUserContext()),
+      d_cacheEnabled(cacheEnabled)
+{
+  d_true = NodeManager::currentNM()->mkConst(true);
+}
+
+// Gets all leaf terms in n.
+std::vector<Node> ExtTheory::collectVars(Node n)
+{
+  std::vector<Node> vars;
+  std::set<Node> visited;
+  std::vector<Node> worklist;
+  worklist.push_back(n);
+  while (!worklist.empty())
+  {
+    Node current = worklist.back();
+    worklist.pop_back();
+    if (current.isConst() || visited.count(current) > 0)
+    {
+      continue;
+    }
+    visited.insert(current);
+    // Treat terms not belonging to this theory as leaf
+    // note : chould include terms not belonging to this theory
+    // (commented below)
+    if (current.getNumChildren() > 0)
+    {
+      //&& Theory::theoryOf(n)==d_parent->getId() ){
+      worklist.insert(worklist.end(), current.begin(), current.end());
+    }
+    else
+    {
+      vars.push_back(current);
+    }
+  }
+  return vars;
+}
+
+Node ExtTheory::getSubstitutedTerm(int effort,
+                                   Node term,
+                                   std::vector<Node>& exp,
+                                   bool useCache)
+{
+  if (useCache)
+  {
+    Assert(d_gst_cache[effort].find(term) != d_gst_cache[effort].end());
+    exp.insert(exp.end(),
+               d_gst_cache[effort][term].d_exp.begin(),
+               d_gst_cache[effort][term].d_exp.end());
+    return d_gst_cache[effort][term].d_sterm;
+  }
+
+  std::vector<Node> terms;
+  terms.push_back(term);
+  std::vector<Node> sterms;
+  std::vector<std::vector<Node> > exps;
+  getSubstitutedTerms(effort, terms, sterms, exps, useCache);
+  Assert(sterms.size() == 1);
+  Assert(exps.size() == 1);
+  exp.insert(exp.end(), exps[0].begin(), exps[0].end());
+  return sterms[0];
+}
+
+// do inferences
+void ExtTheory::getSubstitutedTerms(int effort,
+                                    const std::vector<Node>& terms,
+                                    std::vector<Node>& sterms,
+                                    std::vector<std::vector<Node> >& exp,
+                                    bool useCache)
+{
+  if (useCache)
+  {
+    for (const Node& n : terms)
+    {
+      Assert(d_gst_cache[effort].find(n) != d_gst_cache[effort].end());
+      sterms.push_back(d_gst_cache[effort][n].d_sterm);
+      exp.push_back(std::vector<Node>());
+      exp[0].insert(exp[0].end(),
+                    d_gst_cache[effort][n].d_exp.begin(),
+                    d_gst_cache[effort][n].d_exp.end());
+    }
+  }
+  else
+  {
+    Trace("extt-debug") << "getSubstitutedTerms for " << terms.size() << " / "
+                        << d_ext_func_terms.size() << " extended functions."
+                        << std::endl;
+    if (!terms.empty())
+    {
+      // all variables we need to find a substitution for
+      std::vector<Node> vars;
+      std::vector<Node> sub;
+      std::map<Node, std::vector<Node> > expc;
+      for (const Node& n : terms)
+      {
+        // do substitution, rewrite
+        std::map<Node, ExtfInfo>::iterator iti = d_extf_info.find(n);
+        Assert(iti != d_extf_info.end());
+        for (const Node& v : iti->second.d_vars)
+        {
+          if (std::find(vars.begin(), vars.end(), v) == vars.end())
+          {
+            vars.push_back(v);
+          }
+        }
+      }
+      bool useSubs = d_parent->getCurrentSubstitution(effort, vars, sub, expc);
+      // get the current substitution for all variables
+      Assert(!useSubs || vars.size() == sub.size());
+      for (const Node& n : terms)
+      {
+        Node ns = n;
+        std::vector<Node> expn;
+        if (useSubs)
+        {
+          // do substitution
+          ns = n.substitute(vars.begin(), vars.end(), sub.begin(), sub.end());
+          if (ns != n)
+          {
+            // build explanation: explanation vars = sub for each vars in FV(n)
+            std::map<Node, ExtfInfo>::iterator iti = d_extf_info.find(n);
+            Assert(iti != d_extf_info.end());
+            for (const Node& v : iti->second.d_vars)
+            {
+              std::map<Node, std::vector<Node> >::iterator itx = expc.find(v);
+              if (itx != expc.end())
+              {
+                for (const Node& e : itx->second)
+                {
+                  if (std::find(expn.begin(), expn.end(), e) == expn.end())
+                  {
+                    expn.push_back(e);
+                  }
+                }
+              }
+            }
+          }
+          Trace("extt-debug")
+              << "  have " << n << " == " << ns << ", exp size=" << expn.size()
+              << "." << std::endl;
+        }
+        // add to vector
+        sterms.push_back(ns);
+        exp.push_back(expn);
+        // add to cache
+        if (d_cacheEnabled)
+        {
+          d_gst_cache[effort][n].d_sterm = ns;
+          d_gst_cache[effort][n].d_exp.clear();
+          d_gst_cache[effort][n].d_exp.insert(
+              d_gst_cache[effort][n].d_exp.end(), expn.begin(), expn.end());
+        }
+      }
+    }
+  }
+}
+
+bool ExtTheory::doInferencesInternal(int effort,
+                                     const std::vector<Node>& terms,
+                                     std::vector<Node>& nred,
+                                     bool batch,
+                                     bool isRed)
+{
+  if (batch)
+  {
+    bool addedLemma = false;
+    if (isRed)
+    {
+      for (const Node& n : terms)
+      {
+        Node nr;
+        // note: could do reduction with substitution here
+        int ret = d_parent->getReduction(effort, n, nr);
+        if (ret == 0)
+        {
+          nred.push_back(n);
+        }
+        else
+        {
+          if (!nr.isNull() && n != nr)
+          {
+            Node lem = NodeManager::currentNM()->mkNode(kind::EQUAL, n, nr);
+            if (sendLemma(lem, true))
+            {
+              Trace("extt-lemma")
+                  << "ExtTheory : reduction lemma : " << lem << std::endl;
+              addedLemma = true;
+            }
+          }
+          markReduced(n, ret < 0);
+        }
+      }
+    }
+    else
+    {
+      std::vector<Node> sterms;
+      std::vector<std::vector<Node> > exp;
+      getSubstitutedTerms(effort, terms, sterms, exp);
+      std::map<Node, unsigned> sterm_index;
+      for (unsigned i = 0, size = terms.size(); i < size; i++)
+      {
+        bool processed = false;
+        if (sterms[i] != terms[i])
+        {
+          Node sr = Rewriter::rewrite(sterms[i]);
+          // ask the theory if this term is reduced, e.g. is it constant or it
+          // is a non-extf term.
+          if (d_parent->isExtfReduced(effort, sr, terms[i], exp[i]))
+          {
+            processed = true;
+            markReduced(terms[i]);
+            Node eq = terms[i].eqNode(sr);
+            Node expn =
+                exp[i].size() > 1
+                    ? NodeManager::currentNM()->mkNode(kind::AND, exp[i])
+                    : (exp[i].size() == 1 ? exp[i][0] : d_true);
+            Trace("extt-debug") << "ExtTheory::doInferences : infer : " << eq
+                                << " by " << expn << std::endl;
+            Node lem =
+                NodeManager::currentNM()->mkNode(kind::IMPLIES, expn, eq);
+            Trace("extt-debug") << "...send lemma " << lem << std::endl;
+            if (sendLemma(lem))
+            {
+              Trace("extt-lemma")
+                  << "ExtTheory : substitution + rewrite lemma : " << lem
+                  << std::endl;
+              addedLemma = true;
+            }
+          }
+          else
+          {
+            // check if we have already reduced this
+            std::map<Node, unsigned>::iterator itsi = sterm_index.find(sr);
+            if (itsi == sterm_index.end())
+            {
+              sterm_index[sr] = i;
+            }
+            else
+            {
+              // unsigned j = itsi->second;
+              // note : can add (non-reducing) lemma :
+              //   exp[j] ^ exp[i] => sterms[i] = sterms[j]
+            }
+
+            Trace("extt-nred") << "Non-reduced term : " << sr << std::endl;
+          }
+        }
+        else
+        {
+          Trace("extt-nred") << "Non-reduced term : " << sterms[i] << std::endl;
+        }
+        if (!processed)
+        {
+          nred.push_back(terms[i]);
+        }
+      }
+    }
+    return addedLemma;
+  }
+  // non-batch
+  std::vector<Node> nnred;
+  if (terms.empty())
+  {
+    for (NodeBoolMap::iterator it = d_ext_func_terms.begin();
+         it != d_ext_func_terms.end();
+         ++it)
+    {
+      if ((*it).second && !isContextIndependentInactive((*it).first))
+      {
+        std::vector<Node> nterms;
+        nterms.push_back((*it).first);
+        if (doInferencesInternal(effort, nterms, nnred, true, isRed))
+        {
+          return true;
+        }
+      }
+    }
+  }
+  else
+  {
+    for (const Node& n : terms)
+    {
+      std::vector<Node> nterms;
+      nterms.push_back(n);
+      if (doInferencesInternal(effort, nterms, nnred, true, isRed))
+      {
+        return true;
+      }
+    }
+  }
+  return false;
+}
+
+bool ExtTheory::sendLemma(Node lem, bool preprocess)
+{
+  if (preprocess)
+  {
+    if (d_pp_lemmas.find(lem) == d_pp_lemmas.end())
+    {
+      d_pp_lemmas.insert(lem);
+      d_parent->getOutputChannel().lemma(lem, false, true);
+      return true;
+    }
+  }
+  else
+  {
+    if (d_lemmas.find(lem) == d_lemmas.end())
+    {
+      d_lemmas.insert(lem);
+      d_parent->getOutputChannel().lemma(lem);
+      return true;
+    }
+  }
+  return false;
+}
+
+bool ExtTheory::doInferences(int effort,
+                             const std::vector<Node>& terms,
+                             std::vector<Node>& nred,
+                             bool batch)
+{
+  if (!terms.empty())
+  {
+    return doInferencesInternal(effort, terms, nred, batch, false);
+  }
+  return false;
+}
+
+bool ExtTheory::doInferences(int effort, std::vector<Node>& nred, bool batch)
+{
+  std::vector<Node> terms = getActive();
+  return doInferencesInternal(effort, terms, nred, batch, false);
+}
+
+bool ExtTheory::doReductions(int effort,
+                             const std::vector<Node>& terms,
+                             std::vector<Node>& nred,
+                             bool batch)
+{
+  if (!terms.empty())
+  {
+    return doInferencesInternal(effort, terms, nred, batch, true);
+  }
+  return false;
+}
+
+bool ExtTheory::doReductions(int effort, std::vector<Node>& nred, bool batch)
+{
+  const std::vector<Node> terms = getActive();
+  return doInferencesInternal(effort, terms, nred, batch, true);
+}
+
+// Register term.
+void ExtTheory::registerTerm(Node n)
+{
+  if (d_extf_kind.find(n.getKind()) != d_extf_kind.end())
+  {
+    if (d_ext_func_terms.find(n) == d_ext_func_terms.end())
+    {
+      Trace("extt-debug") << "Found extended function : " << n << " in "
+                          << d_parent->getId() << std::endl;
+      d_ext_func_terms[n] = true;
+      d_has_extf = n;
+      d_extf_info[n].d_vars = collectVars(n);
+    }
+  }
+}
+
+void ExtTheory::registerTermRec(Node n)
+{
+  std::unordered_set<TNode, TNodeHashFunction> visited;
+  std::vector<TNode> visit;
+  TNode cur;
+  visit.push_back(n);
+  do
+  {
+    cur = visit.back();
+    visit.pop_back();
+    if (visited.find(cur) == visited.end())
+    {
+      visited.insert(cur);
+      registerTerm(cur);
+      for (const Node& cc : cur)
+      {
+        visit.push_back(cc);
+      }
+    }
+  } while (!visit.empty());
+}
+
+// mark reduced
+void ExtTheory::markReduced(Node n, bool contextDepend)
+{
+  registerTerm(n);
+  Assert(d_ext_func_terms.find(n) != d_ext_func_terms.end());
+  d_ext_func_terms[n] = false;
+  if (!contextDepend)
+  {
+    d_ci_inactive.insert(n);
+  }
+
+  // update has_extf
+  if (d_has_extf.get() == n)
+  {
+    for (NodeBoolMap::iterator it = d_ext_func_terms.begin();
+         it != d_ext_func_terms.end();
+         ++it)
+    {
+      // if not already reduced
+      if ((*it).second && !isContextIndependentInactive((*it).first))
+      {
+        d_has_extf = (*it).first;
+      }
+    }
+  }
+}
+
+// mark congruent
+void ExtTheory::markCongruent(Node a, Node b)
+{
+  Trace("extt-debug") << "Mark congruent : " << a << " " << b << std::endl;
+  registerTerm(a);
+  registerTerm(b);
+  NodeBoolMap::const_iterator it = d_ext_func_terms.find(b);
+  if (it != d_ext_func_terms.end())
+  {
+    if (d_ext_func_terms.find(a) != d_ext_func_terms.end())
+    {
+      d_ext_func_terms[a] = d_ext_func_terms[a] && (*it).second;
+    }
+    else
+    {
+      Assert(false);
+    }
+    d_ext_func_terms[b] = false;
+  }
+  else
+  {
+    Assert(false);
+  }
+}
+
+bool ExtTheory::isContextIndependentInactive(Node n) const
+{
+  return d_ci_inactive.find(n) != d_ci_inactive.end();
+}
+
+void ExtTheory::getTerms(std::vector<Node>& terms)
+{
+  for (NodeBoolMap::iterator it = d_ext_func_terms.begin();
+       it != d_ext_func_terms.end();
+       ++it)
+  {
+    terms.push_back((*it).first);
+  }
+}
+
+bool ExtTheory::hasActiveTerm() const { return !d_has_extf.get().isNull(); }
+
+// is active
+bool ExtTheory::isActive(Node n) const
+{
+  NodeBoolMap::const_iterator it = d_ext_func_terms.find(n);
+  if (it != d_ext_func_terms.end())
+  {
+    return (*it).second && !isContextIndependentInactive(n);
+  }
+  return false;
+}
+
+// get active
+std::vector<Node> ExtTheory::getActive() const
+{
+  std::vector<Node> active;
+  for (NodeBoolMap::iterator it = d_ext_func_terms.begin();
+       it != d_ext_func_terms.end();
+       ++it)
+  {
+    // if not already reduced
+    if ((*it).second && !isContextIndependentInactive((*it).first))
+    {
+      active.push_back((*it).first);
+    }
+  }
+  return active;
+}
+
+std::vector<Node> ExtTheory::getActive(Kind k) const
+{
+  std::vector<Node> active;
+  for (NodeBoolMap::iterator it = d_ext_func_terms.begin();
+       it != d_ext_func_terms.end();
+       ++it)
+  {
+    // if not already reduced
+    if ((*it).first.getKind() == k && (*it).second
+        && !isContextIndependentInactive((*it).first))
+    {
+      active.push_back((*it).first);
+    }
+  }
+  return active;
+}
+
+void ExtTheory::clearCache() { d_gst_cache.clear(); }
+
+} /* CVC4::theory namespace */
+} /* CVC4 namespace */
diff --git a/src/theory/ext_theory.h b/src/theory/ext_theory.h
new file mode 100644
index 000000000..8657d0fb8
--- /dev/null
+++ b/src/theory/ext_theory.h
@@ -0,0 +1,250 @@
+/*********************                                                        */
+/*! \file ext_theory.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 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 Extended theory interface.
+ **
+ ** This implements a generic module, used by theory solvers, for performing
+ ** "context-dependent simplification", as described in Reynolds et al
+ ** "Designing Theory Solvers with Extensions", FroCoS 2017.
+ **
+ ** At a high level, this technique implements a generic inference scheme based
+ ** on the combination of SAT-context-dependent equality reasoning and
+ ** SAT-context-indepedent rewriting.
+ **
+ ** As a simple example, say
+ ** (1) TheoryStrings tells us that the following facts hold in the SAT context:
+ **     x = "A" ^ str.contains( str.++( x, z ), "B" ) = true.
+ ** (2) The Rewriter tells us that:
+ **     str.contains( str.++( "A", z ), "B" ) ----> str.contains( z, "B" ).
+ ** From this, this class may infer that the following lemma is T-valid:
+ **   x = "A" ^ str.contains( str.++( x, z ), "B" ) => str.contains( z, "B" )
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__EXT_THEORY_H
+#define __CVC4__THEORY__EXT_THEORY_H
+
+#include <map>
+#include <set>
+
+#include "context/cdhashset.h"
+#include "context/context.h"
+#include "expr/node.h"
+#include "theory/theory.h"
+
+namespace CVC4 {
+namespace theory {
+
+/** Extended theory class
+ *
+ * This class is used for constructing generic extensions to theory solvers.
+ * In particular, it provides methods for "context-dependent simplification"
+ * and "model-based refinement". For details, see Reynolds et al "Design
+ * Theory Solvers with Extensions", FroCoS 2017.
+ *
+ * It maintains:
+ * (1) A set of "extended function" kinds (d_extf_kind),
+ * (2) A database of active/inactive extended function terms (d_ext_func_terms)
+ * that have been registered to the class.
+ *
+ * This class has methods doInferences/doReductions, which send out lemmas
+ * based on the current set of active extended function terms. The former
+ * is based on context-dependent simplification, where this class asks the
+ * underlying theory for a "derivable substitution", whereby extended functions
+ * may be reducable.
+ */
+class ExtTheory
+{
+  typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
+  typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
+
+ public:
+  /** constructor
+   *
+   * If cacheEnabled is false, we do not cache results of getSubstitutedTerm.
+   */
+  ExtTheory(Theory* p, bool cacheEnabled = false);
+  virtual ~ExtTheory() {}
+  /** Tells this class to treat terms with Kind k as extended functions */
+  void addFunctionKind(Kind k) { d_extf_kind[k] = true; }
+  /** Is kind k treated as an extended function by this class? */
+  bool hasFunctionKind(Kind k) const
+  {
+    return d_extf_kind.find(k) != d_extf_kind.end();
+  }
+  /** register term
+   *
+   * Registers term n with this class. Adds n to the set of extended function
+   * terms known by this class (d_ext_func_terms) if n is an extended function,
+   * that is, if addFunctionKind( n.getKind() ) was called.
+   */
+  void registerTerm(Node n);
+  /** register all subterms of n with this class */
+  void registerTermRec(Node n);
+  /** set n as reduced/inactive
+   *
+   * If contextDepend = false, then n remains inactive in the duration of this
+   * user-context level
+   */
+  void markReduced(Node n, bool contextDepend = true);
+  /**
+   * Mark that a and b are congruent terms. This sets b inactive, and sets a to
+   * inactive if b was inactive.
+   */
+  void markCongruent(Node a, Node b);
+  /** getSubstitutedTerms
+   *
+   *  input : effort, terms
+   *  output : sterms, exp, where ( exp[i] => terms[i] = sterms[i] ) for all i.
+   *
+   * For each i, sterms[i] = term[i] * sigma for some "derivable substitution"
+   * sigma. We obtain derivable substitutions and their explanations via calls
+   * to the underlying theory's Theory::getCurrentSubstitution method. This
+   * also
+   *
+   * If useCache is true, we cache the result in d_gst_cache. This is a context
+   * independent cache that can be cleared using clearCache() below.
+   */
+  void getSubstitutedTerms(int effort,
+                           const std::vector<Node>& terms,
+                           std::vector<Node>& sterms,
+                           std::vector<std::vector<Node> >& exp,
+                           bool useCache = false);
+  /**
+   * Same as above, but for a single term. We return the substituted form of
+   * term and add its explanation to exp.
+   */
+  Node getSubstitutedTerm(int effort,
+                          Node term,
+                          std::vector<Node>& exp,
+                          bool useCache = false);
+  /** clear the cache for getSubstitutedTerm */
+  void clearCache();
+  /** doInferences
+   *
+   * This function performs "context-dependent simplification". The method takes
+   * as input:
+   *  effort: an identifier used to determine which terms we reduce and the
+   *          form of the derivable substitution we will use,
+   *  terms: the set of terms to simplify,
+   *  batch: if this flag is true, we send lemmas for all terms; if it is false
+   *         we send a lemma for the first applicable term.
+   *
+   * Sends rewriting lemmas of the form ( exp => t = c ) where t is in terms
+   * and c is a constant, c = rewrite( t*sigma ) where exp |= sigma. These
+   * lemmas are determined by asking the underlying theory for a derivable
+   * substitution (through getCurrentSubstitution with getSubstitutedTerm)
+   * above, applying this substitution to terms in terms, rewriting
+   * the result and checking with the theory whether the resulting term is
+   * in reduced form (isExtfReduced).
+   *
+   * This method adds the extended terms that are still active to nred, and
+   * returns true if and only if a lemma of the above form was sent.
+   */
+  bool doInferences(int effort,
+                    const std::vector<Node>& terms,
+                    std::vector<Node>& nred,
+                    bool batch = true);
+  /**
+   * Calls the above function, where terms is getActive(), the set of currently
+   * active terms.
+   */
+  bool doInferences(int effort, std::vector<Node>& nred, bool batch = true);
+  /** doReductions
+   *
+   * This method has the same interface as doInferences. In contrast to
+   * doInfereces, this method will send reduction lemmas of the form ( t = t' )
+   * where t is in terms and t' is an equivalent reduced term.
+   */
+  bool doReductions(int effort,
+                    const std::vector<Node>& terms,
+                    std::vector<Node>& nred,
+                    bool batch = true);
+  bool doReductions(int effort, std::vector<Node>& nred, bool batch = true);
+
+  /** get the set of all extended function terms from d_ext_func_terms */
+  void getTerms(std::vector<Node>& terms);
+  /** is there at least one active extended function term? */
+  bool hasActiveTerm() const;
+  /** is n an active extended function term? */
+  bool isActive(Node n) const;
+  /** get the set of active terms from d_ext_func_terms */
+  std::vector<Node> getActive() const;
+  /** get the set of active terms from d_ext_func_terms of kind k */
+  std::vector<Node> getActive(Kind k) const;
+
+ private:
+  /** returns the set of variable subterms of n */
+  static std::vector<Node> collectVars(Node n);
+  /** is n context dependent inactive? */
+  bool isContextIndependentInactive(Node n) const;
+  /** do inferences internal */
+  bool doInferencesInternal(int effort,
+                            const std::vector<Node>& terms,
+                            std::vector<Node>& nred,
+                            bool batch,
+                            bool isRed);
+  /** send lemma on the output channel of d_parent */
+  bool sendLemma(Node lem, bool preprocess = false);
+  /** reference to the underlying theory */
+  Theory* d_parent;
+  /** the true node */
+  Node d_true;
+  /** extended function terms, map to whether they are active */
+  NodeBoolMap d_ext_func_terms;
+  /**
+   * The set of terms from d_ext_func_terms that are SAT-context-independent
+   * inactive. For instance, a term t is SAT-context-independent inactive if
+   * a reduction lemma of the form t = t' was added in this user-context level.
+   */
+  NodeSet d_ci_inactive;
+  /**
+   * Watched term for checking if any non-reduced extended functions exist.
+   * This is an arbitrary active member of d_ext_func_terms.
+   */
+  context::CDO<Node> d_has_extf;
+  /** the set of kinds we are treated as extended functions */
+  std::map<Kind, bool> d_extf_kind;
+  /** information for each term in d_ext_func_terms */
+  class ExtfInfo
+  {
+   public:
+    /** all variables in this term */
+    std::vector<Node> d_vars;
+  };
+  std::map<Node, ExtfInfo> d_extf_info;
+
+  // cache of all lemmas sent
+  NodeSet d_lemmas;
+  NodeSet d_pp_lemmas;
+  /** whether we enable caching for getSubstitutedTerm */
+  bool d_cacheEnabled;
+  /** Substituted term info */
+  class SubsTermInfo
+  {
+   public:
+    /** the substituted term */
+    Node d_sterm;
+    /** an explanation */
+    std::vector<Node> d_exp;
+  };
+  /**
+   * This maps an (effort, term) to the information above. It is used as a
+   * cache for getSubstitutedTerm when d_cacheEnabled is true.
+   */
+  std::map<int, std::map<Node, SubsTermInfo> > d_gst_cache;
+};
+
+} /* CVC4::theory namespace */
+} /* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__EXT_THEORY_H */
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 928df298c..cb1f006b3 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -20,15 +20,16 @@
 
 #include "expr/kind.h"
 #include "options/strings_options.h"
+#include "smt/command.h"
 #include "smt/logic_exception.h"
 #include "smt/smt_statistics_registry.h"
-#include "smt/command.h"
+#include "theory/ext_theory.h"
+#include "theory/quantifiers/term_database.h"
 #include "theory/rewriter.h"
 #include "theory/strings/theory_strings_rewriter.h"
 #include "theory/strings/type_enumerator.h"
 #include "theory/theory_model.h"
 #include "theory/valuation.h"
-#include "theory/quantifiers/term_database.h"
 
 using namespace std;
 using namespace CVC4::context;
diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp
index a08ac2da3..10504b487 100644
--- a/src/theory/theory.cpp
+++ b/src/theory/theory.cpp
@@ -23,9 +23,9 @@
 
 #include "base/cvc4_assert.h"
 #include "smt/smt_statistics_registry.h"
-#include "theory/substitutions.h"
+#include "theory/ext_theory.h"
 #include "theory/quantifiers_engine.h"
-
+#include "theory/substitutions.h"
 
 using namespace std;
 
@@ -355,391 +355,5 @@ TheoryId EntailmentCheckSideEffects::getTheoryId() const {
 EntailmentCheckSideEffects::~EntailmentCheckSideEffects() {
 }
 
-
-
-ExtTheory::ExtTheory( Theory * p, bool cacheEnabled ) : d_parent( p ), 
-d_ext_func_terms( p->getSatContext() ), d_ci_inactive( p->getUserContext() ), d_has_extf( p->getSatContext() ),
-d_lemmas( p->getUserContext() ), d_pp_lemmas( p->getUserContext() ), d_cacheEnabled( cacheEnabled ){
-  d_true = NodeManager::currentNM()->mkConst( true );
-}
-
-// Gets all leaf terms in n.
-std::vector<Node> ExtTheory::collectVars(Node n) {
-  std::vector<Node> vars;
-  std::set<Node> visited;
-  std::vector<Node> worklist;
-  worklist.push_back(n);
-  while (!worklist.empty()) {
-    Node current = worklist.back();
-    worklist.pop_back();
-    if (current.isConst() || visited.count(current) > 0) {
-      continue;
-    }
-    visited.insert(current);
-    // Treat terms not belonging to this theory as leaf
-    // AJR TODO : should include terms not belonging to this theory
-    // (commented below)
-    if (current.getNumChildren() > 0) {
-      //&& Theory::theoryOf(n)==d_parent->getId() ){
-      worklist.insert(worklist.end(), current.begin(), current.end());
-    } else {
-      vars.push_back(current);
-    }
-  }
-  return vars;
-}
-
-Node ExtTheory::getSubstitutedTerm( int effort, Node term, std::vector< Node >& exp, bool useCache ) {
-  if( useCache ){
-    Assert( d_gst_cache[effort].find( term )!=d_gst_cache[effort].end() );
-    exp.insert( exp.end(), d_gst_cache[effort][term].d_exp.begin(), d_gst_cache[effort][term].d_exp.end() );
-    return d_gst_cache[effort][term].d_sterm;
-  }else{
-    std::vector< Node > terms;
-    terms.push_back( term );
-    std::vector< Node > sterms;
-    std::vector< std::vector< Node > > exps;
-    getSubstitutedTerms( effort, terms, sterms, exps, useCache );
-    Assert( sterms.size()==1 );
-    Assert( exps.size()==1 );
-    exp.insert( exp.end(), exps[0].begin(), exps[0].end() );
-    return sterms[0];
-  }
-}
-
-//do inferences
-void ExtTheory::getSubstitutedTerms(int effort, const std::vector<Node>& terms,
-                                    std::vector<Node>& sterms,
-                                    std::vector<std::vector<Node> >& exp,
-                                    bool useCache) {
-  if (useCache) {
-    for( unsigned i=0; i<terms.size(); i++ ){
-      Node n = terms[i];
-      Assert( d_gst_cache[effort].find( n )!=d_gst_cache[effort].end() );
-      sterms.push_back( d_gst_cache[effort][n].d_sterm );
-      exp.push_back( std::vector< Node >() );
-      exp[0].insert( exp[0].end(), d_gst_cache[effort][n].d_exp.begin(), d_gst_cache[effort][n].d_exp.end() );
-    }
-  }else{
-    Trace("extt-debug") << "getSubstitutedTerms for " << terms.size() << " / " << d_ext_func_terms.size() << " extended functions." << std::endl;
-    if( !terms.empty() ){
-      //all variables we need to find a substitution for
-      std::vector< Node > vars;
-      std::vector< Node > sub;
-      std::map< Node, std::vector< Node > > expc;
-      for( unsigned i=0; i<terms.size(); i++ ){
-        //do substitution, rewrite
-        Node n = terms[i];
-        std::map< Node, ExtfInfo >::iterator iti = d_extf_info.find( n );
-        Assert( iti!=d_extf_info.end() );
-        for( unsigned i=0; i<iti->second.d_vars.size(); i++ ){
-          if( std::find( vars.begin(), vars.end(), iti->second.d_vars[i] )==vars.end() ){
-            vars.push_back( iti->second.d_vars[i] );
-          } 
-        }
-      }
-      bool useSubs = d_parent->getCurrentSubstitution( effort, vars, sub, expc );
-      //get the current substitution for all variables
-      Assert( !useSubs || vars.size()==sub.size() );
-      for( unsigned i=0; i<terms.size(); i++ ){
-        Node n = terms[i];
-        Node ns = n;
-        std::vector< Node > expn;
-        if( useSubs ){
-          //do substitution
-          ns = n.substitute( vars.begin(), vars.end(), sub.begin(), sub.end() );
-          if( ns!=n ){
-            //build explanation: explanation vars = sub for each vars in FV( n )
-            std::map< Node, ExtfInfo >::iterator iti = d_extf_info.find( n );
-            Assert( iti!=d_extf_info.end() );
-            for( unsigned j=0; j<iti->second.d_vars.size(); j++ ){
-              Node v = iti->second.d_vars[j];
-              std::map< Node, std::vector< Node > >::iterator itx = expc.find( v );
-              if( itx!=expc.end() ){
-                for( unsigned k=0; k<itx->second.size(); k++ ){
-                  if( std::find( expn.begin(), expn.end(), itx->second[k] )==expn.end() ){
-                    expn.push_back( itx->second[k] );
-                  }
-                }
-              }
-            }
-          }
-          Trace("extt-debug") << "  have " << n << " == " << ns << ", exp size=" << expn.size() << "." << std::endl;
-        }
-        //add to vector
-        sterms.push_back( ns );
-        exp.push_back( expn );
-        //add to cache
-        if( d_cacheEnabled ){
-          d_gst_cache[effort][n].d_sterm = ns;
-          d_gst_cache[effort][n].d_exp.clear();
-          d_gst_cache[effort][n].d_exp.insert( d_gst_cache[effort][n].d_exp.end(), expn.begin(), expn.end() );
-        }
-      }
-    }
-  }
-}
-
-bool ExtTheory::doInferencesInternal(int effort, const std::vector<Node>& terms,
-                                     std::vector<Node>& nred, bool batch,
-                                     bool isRed) {
-  if (batch) {
-    bool addedLemma = false;
-    if( isRed ){
-      for( unsigned i=0; i<terms.size(); i++ ){
-        Node n = terms[i];
-        Node nr;
-        //TODO: reduction with substitution?
-        int ret = d_parent->getReduction( effort, n, nr );
-        if( ret==0 ){
-          nred.push_back( n );
-        }else{
-          if( !nr.isNull() && n!=nr ){
-            Node lem = NodeManager::currentNM()->mkNode( kind::EQUAL, n, nr );
-            if( sendLemma( lem, true ) ){
-              Trace("extt-lemma") << "ExtTheory : reduction lemma : " << lem << std::endl;
-              addedLemma = true;
-            }
-          }
-          markReduced( terms[i], ret<0 );
-        }
-      }
-    }else{
-      std::vector< Node > sterms; 
-      std::vector< std::vector< Node > > exp;
-      getSubstitutedTerms( effort, terms, sterms, exp );
-      std::map< Node, unsigned > sterm_index;
-      for( unsigned i=0; i<terms.size(); i++ ){
-        bool processed = false;
-        if( sterms[i]!=terms[i] ){
-          Node sr = Rewriter::rewrite( sterms[i] );
-          //ask the theory if this term is reduced, e.g. is it constant or it is a non-extf term.
-          if( d_parent->isExtfReduced( effort, sr, terms[i], exp[i] ) ){
-            processed = true;
-            markReduced( terms[i] );
-            Node eq = terms[i].eqNode( sr );
-            Node expn = exp[i].size()>1 ? NodeManager::currentNM()->mkNode( kind::AND, exp[i] ) : ( exp[i].size()==1 ? exp[i][0] : d_true );
-            Trace("extt-debug") << "ExtTheory::doInferences : infer : " << eq << " by " << expn << std::endl;
-            Node lem = NodeManager::currentNM()->mkNode( kind::IMPLIES, expn, eq );
-            Trace("extt-debug") << "...send lemma " << lem << std::endl;
-            if( sendLemma( lem ) ){
-              Trace("extt-lemma") << "ExtTheory : substitution + rewrite lemma : " << lem << std::endl;
-              addedLemma = true;
-            }
-          }else{
-            //check if we have already reduced this
-            std::map< Node, unsigned >::iterator itsi = sterm_index.find( sr );
-            if( itsi!=sterm_index.end() ){
-              //unsigned j = itsi->second;
-              //can add (non-reducing) lemma : exp[j] ^ exp[i] => sterms[i] = sterms[j]
-              //TODO
-            }else{
-              sterm_index[sr] = i;
-            }
-            //check if we reduce to another active term?
-          
-            Trace("extt-nred") << "Non-reduced term : " << sr << std::endl;
-          }
-        }else{
-          Trace("extt-nred") << "Non-reduced term : " << sterms[i] << std::endl;
-        }
-        if( !processed ){
-          nred.push_back( terms[i] );
-        }
-      }
-    }
-    return addedLemma;
-  }else{
-    std::vector< Node > nnred;
-    if( terms.empty() ){
-      for( NodeBoolMap::iterator it = d_ext_func_terms.begin(); it != d_ext_func_terms.end(); ++it ){
-        if( (*it).second && !isContextIndependentInactive( (*it).first ) ){
-          std::vector< Node > nterms;
-          nterms.push_back( (*it).first );
-          if( doInferencesInternal( effort, nterms, nnred, true, isRed ) ){
-            return true;
-          }       
-        }
-      }
-    }else{
-      for( unsigned i=0; i<terms.size(); i++ ){
-        std::vector< Node > nterms;
-        nterms.push_back( terms[i] );
-        if( doInferencesInternal( effort, nterms, nnred, true, isRed ) ){
-          return true;
-        }   
-      }
-    }
-    return false;
-  }
-}
-
-bool ExtTheory::sendLemma( Node lem, bool preprocess ) {
-  if( preprocess ){
-    if( d_pp_lemmas.find( lem )==d_pp_lemmas.end() ){
-      d_pp_lemmas.insert( lem );
-      d_parent->getOutputChannel().lemma( lem, false, true );
-      return true;
-    }
-  }else{
-    if( d_lemmas.find( lem )==d_lemmas.end() ){
-      d_lemmas.insert( lem );
-      d_parent->getOutputChannel().lemma( lem );
-      return true;
-    }
-  }
-  return false;
-}
-
-bool ExtTheory::doInferences(int effort, const std::vector<Node>& terms,
-                             std::vector<Node>& nred, bool batch) {
-  if (!terms.empty()) {
-    return doInferencesInternal( effort, terms, nred, batch, false );
-  }else{
-    return false;
-  }
-}
-
-bool ExtTheory::doInferences( int effort, std::vector< Node >& nred, bool batch ) {
-  std::vector< Node > terms = getActive();
-  return doInferencesInternal( effort, terms, nred, batch, false );
-}
-
-bool ExtTheory::doReductions(int effort, const std::vector<Node>& terms,
-                             std::vector<Node>& nred, bool batch) {
-  if (!terms.empty()) {
-    return doInferencesInternal( effort, terms, nred, batch, true );
-  }else{
-    return false;
-  }
-}
-
-bool ExtTheory::doReductions(int effort, std::vector<Node>& nred, bool batch) {
-  const std::vector<Node> terms = getActive();
-  return doInferencesInternal(effort, terms, nred, batch, true);
-}
-
-// Register term.
-void ExtTheory::registerTerm(Node n) {
-  if (d_extf_kind.find(n.getKind()) != d_extf_kind.end()) {
-    if (d_ext_func_terms.find(n) == d_ext_func_terms.end()) {
-      Trace("extt-debug") << "Found extended function : " << n << " in "
-                          << d_parent->getId() << std::endl;
-      d_ext_func_terms[n] = true;
-      d_has_extf = n;
-      d_extf_info[n].d_vars = collectVars(n);
-    }
-  }
-}
-
-void ExtTheory::registerTermRec(Node n) {
-  std::set<Node> visited;
-  registerTermRec(n, &visited);
-}
-
-void ExtTheory::registerTermRec(Node n, std::set<Node>* visited) {
-  if (visited->find(n) == visited->end()) {
-    visited->insert(n);
-    registerTerm(n);
-    for (unsigned i = 0; i < n.getNumChildren(); i++) {
-      registerTermRec(n[i], visited);
-    }
-  }
-}
-
-//mark reduced
-void ExtTheory::markReduced( Node n, bool contextDepend ) {
-  registerTerm( n );
-  Assert( d_ext_func_terms.find( n )!=d_ext_func_terms.end() );
-  d_ext_func_terms[n] = false;
-  if( !contextDepend ){
-    d_ci_inactive.insert( n );
-  }
-  
-  //update has_extf
-  if( d_has_extf.get()==n ){
-    for( NodeBoolMap::iterator it = d_ext_func_terms.begin(); it != d_ext_func_terms.end(); ++it ){
-      //if not already reduced
-      if( (*it).second && !isContextIndependentInactive( (*it).first ) ){
-         d_has_extf = (*it).first;
-      }
-    }
-  
-  }
-}
-
-//mark congruent
-void ExtTheory::markCongruent( Node a, Node b ) {
-  Trace("extt-debug") << "Mark congruent : " << a << " " << b << std::endl;
-  registerTerm( a );
-  registerTerm( b );
-  NodeBoolMap::const_iterator it = d_ext_func_terms.find( b );
-  if( it!=d_ext_func_terms.end() ){
-    if( d_ext_func_terms.find( a )!=d_ext_func_terms.end() ){
-      d_ext_func_terms[a] = d_ext_func_terms[a] && (*it).second;
-    }else{
-      Assert( false );
-    }
-    d_ext_func_terms[b] = false;
-  }else{
-    Assert( false );
-  }
-}
-
-bool ExtTheory::isContextIndependentInactive(Node n) const {
-  return d_ci_inactive.find(n) != d_ci_inactive.end();
-}
-
-
-void ExtTheory::getTerms( std::vector< Node >& terms ) {
-  for( NodeBoolMap::iterator it = d_ext_func_terms.begin(); it != d_ext_func_terms.end(); ++it ){
-    terms.push_back( (*it).first );
-  }
-}
-
-bool ExtTheory::hasActiveTerm() {
-  return !d_has_extf.get().isNull();
-}
-  
-//is active
-bool ExtTheory::isActive( Node n ) {
-  NodeBoolMap::const_iterator it = d_ext_func_terms.find( n );
-  if( it!=d_ext_func_terms.end() ){
-    return (*it).second && !isContextIndependentInactive( n );
-  }else{
-    return false;
-  }
-}
-
-// get active
-std::vector<Node> ExtTheory::getActive() const {
-  std::vector<Node> active;
-  for (NodeBoolMap::iterator it = d_ext_func_terms.begin();
-       it != d_ext_func_terms.end(); ++it) {
-    // if not already reduced
-    if ((*it).second && !isContextIndependentInactive((*it).first)) {
-      active.push_back((*it).first);
-    }
-  }
-  return active;
-}
-
-std::vector<Node> ExtTheory::getActive(Kind k) const {
-  std::vector<Node> active;
-  for (NodeBoolMap::iterator it = d_ext_func_terms.begin();
-       it != d_ext_func_terms.end(); ++it) {
-    // if not already reduced
-    if ((*it).first.getKind() == k && (*it).second &&
-        !isContextIndependentInactive((*it).first)) {
-      active.push_back((*it).first);
-    }
-  }
-  return active;
-}
-
-void ExtTheory::clearCache() {
-  d_gst_cache.clear();
-}
-
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/theory.h b/src/theory/theory.h
index 231a56967..3721806ad 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -900,110 +900,6 @@ public:
   virtual ~EntailmentCheckSideEffects();
 };/* class EntailmentCheckSideEffects */
 
-
-class ExtTheory {
-  typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
-  typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
-private:
-  // collect variables
-  static std::vector<Node> collectVars(Node n);
-  // is context dependent inactive
-  bool isContextIndependentInactive( Node n ) const;
-  //do inferences internal
-  bool doInferencesInternal(int effort, const std::vector<Node>& terms,
-                            std::vector<Node>& nred, bool batch, bool isRed);
-  // send lemma
-  bool sendLemma( Node lem, bool preprocess = false );
-  // register term (recursive)
-  void registerTermRec(Node n, std::set<Node>* visited);
-
-  Theory * d_parent;
-  Node d_true;
-  //extended string terms, map to whether they are active
-  NodeBoolMap d_ext_func_terms;
-  //set of terms from d_ext_func_terms that are SAT-context-independently inactive 
-  //  (e.g. term t when a reduction lemma of the form t = t' was added)
-  NodeSet d_ci_inactive;
-  //watched term for checking if any non-reduced extended functions exist 
-  context::CDO< Node > d_has_extf;
-  //extf kind
-  std::map< Kind, bool > d_extf_kind;
-  //information for each term in d_ext_func_terms
-  class ExtfInfo {
-  public:
-    //all variables in this term
-    std::vector< Node > d_vars;
-  };
-  std::map< Node, ExtfInfo > d_extf_info;
-
-  //cache of all lemmas sent
-  NodeSet d_lemmas;
-  NodeSet d_pp_lemmas;
-  bool d_cacheEnabled;
-  // if d_cacheEnabled=true :
-  //cache for getSubstitutedTerms 
-  class SubsTermInfo {
-  public:
-    Node d_sterm;
-    std::vector< Node > d_exp;
-  };
-  std::map< int, std::map< Node, SubsTermInfo > > d_gst_cache;
-
- public:
-  ExtTheory(Theory* p, bool cacheEnabled = false );
-  virtual ~ExtTheory() {}
-  // add extf kind
-  void addFunctionKind(Kind k) { d_extf_kind[k] = true; }
-  bool hasFunctionKind(Kind k) const {
-    return d_extf_kind.find(k) != d_extf_kind.end();
-  }
-  // register term
-  //  adds n to d_ext_func_terms if addFunctionKind( n.getKind() ) was called
-  void registerTerm( Node n );
-  void registerTermRec( Node n );
-  // set n as reduced/inactive
-  //   if contextDepend = false, then n remains inactive in the duration of this user-context level
-  void markReduced( Node n, bool contextDepend = true );
-  // mark that a and b are congruent terms: set b inactive, set a to inactive if b was inactive
-  void markCongruent( Node a, Node b );
-  //getSubstitutedTerms
-  //  input : effort, terms
-  //  output : sterms, exp, where ( exp[i] => terms[i] = sterms[i] ) for all i
-  Node getSubstitutedTerm( int effort, Node term, std::vector< Node >& exp, bool useCache = false );
-  void getSubstitutedTerms(int effort, const std::vector<Node>& terms,
-                           std::vector<Node>& sterms,
-                           std::vector<std::vector<Node> >& exp, bool useCache = false);
-  // doInferences
-  //  * input : effort, terms, batch (whether to send one lemma or lemmas for
-  //    all terms)
-  //  * sends rewriting lemmas of the form ( exp => t = c ) where t is in terms
-  //    and c is a constant, c = rewrite( t*sigma ) where exp |= sigma
-  //  * output : nred (the terms that are still active)
-  //  * return : true iff lemma is sent
-  bool doInferences(int effort, const std::vector<Node>& terms,
-                    std::vector<Node>& nred, bool batch = true);
-  bool doInferences(int effort, std::vector<Node>& nred, bool batch = true);
-  //doReductions 
-  // same as doInferences, but will send reduction lemmas of the form ( t = t' )
-  // where t is in terms, t' is equivalent, reduced term.
-  bool doReductions(int effort, const std::vector<Node>& terms,
-                    std::vector<Node>& nred, bool batch = true);
-  bool doReductions(int effort, std::vector<Node>& nred, bool batch = true);
-
-  //get the set of terms from d_ext_func_terms
-  void getTerms( std::vector< Node >& terms );
-  // has active term
-  bool hasActiveTerm();
-  // is n active
-  bool isActive(Node n);
-  // get the set of active terms from d_ext_func_terms
-  std::vector<Node> getActive() const;
-  // get the set of active terms from d_ext_func_terms of kind k
-  std::vector<Node> getActive(Kind k) const;
-  //clear cache 
-  void clearCache();
-};
-
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */