Split base solver from the theory of strings (#3680)

5 files changed, 678 insertions, 429 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 560f79976..26cc5bbcc 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -664,6 +664,8 @@ libcvc4_add_sources(
   theory/shared_terms_database.h
   theory/sort_inference.cpp
   theory/sort_inference.h
+  theory/strings/base_solver.cpp
+  theory/strings/base_solver.h
   theory/strings/infer_info.cpp
   theory/strings/infer_info.h
   theory/strings/inference_manager.cpp
diff --git a/src/theory/strings/base_solver.cpp b/src/theory/strings/base_solver.cpp
new file mode 100644
index 000000000..2f5bc8e2b
--- /dev/null
+++ b/src/theory/strings/base_solver.cpp
@@ -0,0 +1,427 @@
+/*********************                                                        */
+/*! \file base_solver.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Base solver for the theory of strings. This class implements term
+ ** indexing and constant inference for the theory of strings.
+ **/
+
+#include "theory/strings/base_solver.h"
+
+#include "options/strings_options.h"
+#include "theory/strings/theory_strings_rewriter.h"
+#include "theory/strings/theory_strings_utils.h"
+
+using namespace std;
+using namespace CVC4::context;
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace theory {
+namespace strings {
+
+BaseSolver::BaseSolver(context::Context* c,
+                       context::UserContext* u,
+                       SolverState& s,
+                       InferenceManager& im)
+    : d_state(s), d_im(im), d_congruent(c)
+{
+  d_emptyString = NodeManager::currentNM()->mkConst(::CVC4::String(""));
+  d_false = NodeManager::currentNM()->mkConst(false);
+}
+
+BaseSolver::~BaseSolver() {}
+
+void BaseSolver::checkInit()
+{
+  // build term index
+  d_eqcToConst.clear();
+  d_eqcToConstBase.clear();
+  d_eqcToConstExp.clear();
+  d_termIndex.clear();
+  d_stringsEqc.clear();
+
+  std::map<Kind, uint32_t> ncongruent;
+  std::map<Kind, uint32_t> congruent;
+  eq::EqualityEngine* ee = d_state.getEqualityEngine();
+  Assert(d_state.getRepresentative(d_emptyString) == d_emptyString);
+  eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(ee);
+  while (!eqcs_i.isFinished())
+  {
+    Node eqc = (*eqcs_i);
+    TypeNode tn = eqc.getType();
+    if (!tn.isRegExp())
+    {
+      if (tn.isString())
+      {
+        d_stringsEqc.push_back(eqc);
+      }
+      Node var;
+      eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, ee);
+      while (!eqc_i.isFinished())
+      {
+        Node n = *eqc_i;
+        if (n.isConst())
+        {
+          d_eqcToConst[eqc] = n;
+          d_eqcToConstBase[eqc] = n;
+          d_eqcToConstExp[eqc] = Node::null();
+        }
+        else if (tn.isInteger())
+        {
+          // do nothing
+        }
+        else if (n.getNumChildren() > 0)
+        {
+          Kind k = n.getKind();
+          if (k != EQUAL)
+          {
+            if (d_congruent.find(n) == d_congruent.end())
+            {
+              std::vector<Node> c;
+              Node nc = d_termIndex[k].add(n, 0, d_state, d_emptyString, c);
+              if (nc != n)
+              {
+                // check if we have inferred a new equality by removal of empty
+                // components
+                if (n.getKind() == STRING_CONCAT && !d_state.areEqual(nc, n))
+                {
+                  std::vector<Node> exp;
+                  size_t count[2] = {0, 0};
+                  while (count[0] < nc.getNumChildren()
+                         || count[1] < n.getNumChildren())
+                  {
+                    // explain empty prefixes
+                    for (unsigned t = 0; t < 2; t++)
+                    {
+                      Node nn = t == 0 ? nc : n;
+                      while (
+                          count[t] < nn.getNumChildren()
+                          && (nn[count[t]] == d_emptyString
+                              || d_state.areEqual(nn[count[t]], d_emptyString)))
+                      {
+                        if (nn[count[t]] != d_emptyString)
+                        {
+                          exp.push_back(nn[count[t]].eqNode(d_emptyString));
+                        }
+                        count[t]++;
+                      }
+                    }
+                    // explain equal components
+                    if (count[0] < nc.getNumChildren())
+                    {
+                      Assert(count[1] < n.getNumChildren());
+                      if (nc[count[0]] != n[count[1]])
+                      {
+                        exp.push_back(nc[count[0]].eqNode(n[count[1]]));
+                      }
+                      count[0]++;
+                      count[1]++;
+                    }
+                  }
+                  // infer the equality
+                  d_im.sendInference(exp, n.eqNode(nc), "I_Norm");
+                }
+                else
+                {
+                  // mark as congruent : only process if neither has been
+                  // reduced
+                  d_im.markCongruent(nc, n);
+                }
+                // this node is congruent to another one, we can ignore it
+                Trace("strings-process-debug")
+                    << "  congruent term : " << n << " (via " << nc << ")"
+                    << std::endl;
+                d_congruent.insert(n);
+                congruent[k]++;
+              }
+              else if (k == STRING_CONCAT && c.size() == 1)
+              {
+                Trace("strings-process-debug")
+                    << "  congruent term by singular : " << n << " " << c[0]
+                    << std::endl;
+                // singular case
+                if (!d_state.areEqual(c[0], n))
+                {
+                  Node ns;
+                  std::vector<Node> exp;
+                  // explain empty components
+                  bool foundNEmpty = false;
+                  for (const Node& nc : n)
+                  {
+                    if (d_state.areEqual(nc, d_emptyString))
+                    {
+                      if (nc != d_emptyString)
+                      {
+                        exp.push_back(nc.eqNode(d_emptyString));
+                      }
+                    }
+                    else
+                    {
+                      Assert(!foundNEmpty);
+                      ns = nc;
+                      foundNEmpty = true;
+                    }
+                  }
+                  AlwaysAssert(foundNEmpty);
+                  // infer the equality
+                  d_im.sendInference(exp, n.eqNode(ns), "I_Norm_S");
+                }
+                d_congruent.insert(n);
+                congruent[k]++;
+              }
+              else
+              {
+                ncongruent[k]++;
+              }
+            }
+            else
+            {
+              congruent[k]++;
+            }
+          }
+        }
+        else
+        {
+          if (d_congruent.find(n) == d_congruent.end())
+          {
+            // We mark all but the oldest variable in the equivalence class as
+            // congruent.
+            if (var.isNull())
+            {
+              var = n;
+            }
+            else if (var > n)
+            {
+              Trace("strings-process-debug")
+                  << "  congruent variable : " << var << std::endl;
+              d_congruent.insert(var);
+              var = n;
+            }
+            else
+            {
+              Trace("strings-process-debug")
+                  << "  congruent variable : " << n << std::endl;
+              d_congruent.insert(n);
+            }
+          }
+        }
+        ++eqc_i;
+      }
+    }
+    ++eqcs_i;
+  }
+  if (Trace.isOn("strings-process"))
+  {
+    for (std::map<Kind, TermIndex>::iterator it = d_termIndex.begin();
+         it != d_termIndex.end();
+         ++it)
+    {
+      Trace("strings-process")
+          << "  Terms[" << it->first << "] = " << ncongruent[it->first] << "/"
+          << (congruent[it->first] + ncongruent[it->first]) << std::endl;
+    }
+  }
+}
+
+void BaseSolver::checkConstantEquivalenceClasses()
+{
+  // do fixed point
+  size_t prevSize = 0;
+  std::vector<Node> vecc;
+  do
+  {
+    vecc.clear();
+    Trace("strings-process-debug")
+        << "Check constant equivalence classes..." << std::endl;
+    prevSize = d_eqcToConst.size();
+    checkConstantEquivalenceClasses(&d_termIndex[STRING_CONCAT], vecc);
+  } while (!d_im.hasProcessed() && d_eqcToConst.size() > prevSize);
+}
+
+void BaseSolver::checkConstantEquivalenceClasses(TermIndex* ti,
+                                                 std::vector<Node>& vecc)
+{
+  Node n = ti->d_data;
+  if (!n.isNull())
+  {
+    // construct the constant
+    Node c = utils::mkNConcat(vecc);
+    if (!d_state.areEqual(n, c))
+    {
+      if (Trace.isOn("strings-debug"))
+      {
+        Trace("strings-debug")
+            << "Constant eqc : " << c << " for " << n << std::endl;
+        Trace("strings-debug") << "  ";
+        for (const Node& v : vecc)
+        {
+          Trace("strings-debug") << v << " ";
+        }
+        Trace("strings-debug") << std::endl;
+      }
+      size_t count = 0;
+      size_t countc = 0;
+      std::vector<Node> exp;
+      while (count < n.getNumChildren())
+      {
+        while (count < n.getNumChildren()
+               && d_state.areEqual(n[count], d_emptyString))
+        {
+          d_im.addToExplanation(n[count], d_emptyString, exp);
+          count++;
+        }
+        if (count < n.getNumChildren())
+        {
+          Trace("strings-debug")
+              << "...explain " << n[count] << " " << vecc[countc] << std::endl;
+          if (!d_state.areEqual(n[count], vecc[countc]))
+          {
+            Node nrr = d_state.getRepresentative(n[count]);
+            Assert(!d_eqcToConstExp[nrr].isNull());
+            d_im.addToExplanation(n[count], d_eqcToConstBase[nrr], exp);
+            exp.push_back(d_eqcToConstExp[nrr]);
+          }
+          else
+          {
+            d_im.addToExplanation(n[count], vecc[countc], exp);
+          }
+          countc++;
+          count++;
+        }
+      }
+      // exp contains an explanation of n==c
+      Assert(countc == vecc.size());
+      if (d_state.hasTerm(c))
+      {
+        d_im.sendInference(exp, n.eqNode(c), "I_CONST_MERGE");
+        return;
+      }
+      else if (!d_im.hasProcessed())
+      {
+        Node nr = d_state.getRepresentative(n);
+        std::map<Node, Node>::iterator it = d_eqcToConst.find(nr);
+        if (it == d_eqcToConst.end())
+        {
+          Trace("strings-debug")
+              << "Set eqc const " << n << " to " << c << std::endl;
+          d_eqcToConst[nr] = c;
+          d_eqcToConstBase[nr] = n;
+          d_eqcToConstExp[nr] = utils::mkAnd(exp);
+        }
+        else if (c != it->second)
+        {
+          // conflict
+          Trace("strings-debug")
+              << "Conflict, other constant was " << it->second
+              << ", this constant was " << c << std::endl;
+          if (d_eqcToConstExp[nr].isNull())
+          {
+            // n==c ^ n == c' => false
+            d_im.addToExplanation(n, it->second, exp);
+          }
+          else
+          {
+            // n==c ^ n == d_eqcToConstBase[nr] == c' => false
+            exp.push_back(d_eqcToConstExp[nr]);
+            d_im.addToExplanation(n, d_eqcToConstBase[nr], exp);
+          }
+          d_im.sendInference(exp, d_false, "I_CONST_CONFLICT");
+          return;
+        }
+        else
+        {
+          Trace("strings-debug") << "Duplicate constant." << std::endl;
+        }
+      }
+    }
+  }
+  for (std::pair<const TNode, TermIndex>& p : ti->d_children)
+  {
+    std::map<Node, Node>::iterator itc = d_eqcToConst.find(p.first);
+    if (itc != d_eqcToConst.end())
+    {
+      vecc.push_back(itc->second);
+      checkConstantEquivalenceClasses(&p.second, vecc);
+      vecc.pop_back();
+      if (d_im.hasProcessed())
+      {
+        break;
+      }
+    }
+  }
+}
+
+bool BaseSolver::isCongruent(Node n)
+{
+  return d_congruent.find(n) != d_congruent.end();
+}
+
+Node BaseSolver::getConstantEqc(Node eqc)
+{
+  std::map<Node, Node>::iterator it = d_eqcToConst.find(eqc);
+  if (it != d_eqcToConst.end())
+  {
+    return it->second;
+  }
+  return Node::null();
+}
+
+Node BaseSolver::explainConstantEqc(Node n, Node eqc, std::vector<Node>& exp)
+{
+  std::map<Node, Node>::iterator it = d_eqcToConst.find(eqc);
+  if (it != d_eqcToConst.end())
+  {
+    if (!d_eqcToConstExp[eqc].isNull())
+    {
+      exp.push_back(d_eqcToConstExp[eqc]);
+    }
+    if (!d_eqcToConstBase[eqc].isNull())
+    {
+      d_im.addToExplanation(n, d_eqcToConstBase[eqc], exp);
+    }
+    return it->second;
+  }
+  return Node::null();
+}
+
+const std::vector<Node>& BaseSolver::getStringEqc() const
+{
+  return d_stringsEqc;
+}
+
+Node BaseSolver::TermIndex::add(TNode n,
+                                unsigned index,
+                                const SolverState& s,
+                                Node er,
+                                std::vector<Node>& c)
+{
+  if (index == n.getNumChildren())
+  {
+    if (d_data.isNull())
+    {
+      d_data = n;
+    }
+    return d_data;
+  }
+  Assert(index < n.getNumChildren());
+  TNode nir = s.getRepresentative(n[index]);
+  // if it is empty, and doing CONCAT, ignore
+  if (nir == er && n.getKind() == STRING_CONCAT)
+  {
+    return add(n, index + 1, s, er, c);
+  }
+  c.push_back(nir);
+  return d_children[nir].add(n, index + 1, s, er, c);
+}
+
+}  // namespace strings
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/strings/base_solver.h b/src/theory/strings/base_solver.h
new file mode 100644
index 000000000..c87a3af9e
--- /dev/null
+++ b/src/theory/strings/base_solver.h
@@ -0,0 +1,191 @@
+/*********************                                                        */
+/*! \file base_solver.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Base solver for term indexing and constant inference for the
+ ** theory of strings.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__STRINGS__BASE_SOLVER_H
+#define CVC4__THEORY__STRINGS__BASE_SOLVER_H
+
+#include "context/cdhashset.h"
+#include "context/cdlist.h"
+#include "theory/strings/infer_info.h"
+#include "theory/strings/inference_manager.h"
+#include "theory/strings/normal_form.h"
+#include "theory/strings/skolem_cache.h"
+#include "theory/strings/solver_state.h"
+
+namespace CVC4 {
+namespace theory {
+namespace strings {
+
+/** The base solver for the theory of strings
+ *
+ * This implements techniques for inferring when terms are congruent in the
+ * current context, and techniques for inferring when equivalence classes
+ * are equivalent to constants.
+ */
+class BaseSolver
+{
+  using NodeSet = context::CDHashSet<Node, NodeHashFunction>;
+
+ public:
+  BaseSolver(context::Context* c,
+             context::UserContext* u,
+             SolverState& s,
+             InferenceManager& im);
+  ~BaseSolver();
+
+  //-----------------------inference steps
+  /** check initial
+   *
+   * This function initializes term indices for each strings function symbol.
+   * One key aspect of this construction is that concat terms are indexed by
+   * their list of non-empty components. For example, if x = "" is an equality
+   * asserted in this SAT context, then y ++ x ++ z may be indexed by (y,z).
+   * This method may infer various facts while building these term indices, for
+   * instance, based on congruence. An example would be inferring:
+   *   y ++ x ++ z = y ++ z
+   * if both terms are registered in this SAT context.
+   *
+   * This function should be called as a first step of any strategy.
+   */
+  void checkInit();
+  /** check constant equivalence classes
+   *
+   * This function infers whether CONCAT terms can be simplified to constants.
+   * For example, if x = "a" and y = "b" are equalities in the current SAT
+   * context, then we may infer x ++ "c" ++ y is equivalent to "acb". In this
+   * case, we infer the fact x ++ "c" ++ y = "acb".
+   */
+  void checkConstantEquivalenceClasses();
+  //-----------------------end inference steps
+
+  //-----------------------query functions
+  /**
+   * Is n congruent to another term in the current context that has not been
+   * marked congruent? If so, we can ignore n.
+   *
+   * Note this and the functions in this block below are valid during a full
+   * effort check after a call to checkInit.
+   */
+  bool isCongruent(Node n);
+  /**
+   * Get the constant that the equivalence class eqc is entailed to be equal
+   * to, or null if none exist.
+   */
+  Node getConstantEqc(Node eqc);
+  /**
+   * Same as above, where the explanation for n = c is added to exp if c is
+   * the (non-null) return value of this function, where n is a term in the
+   * equivalence class of eqc.
+   */
+  Node explainConstantEqc(Node n, Node eqc, std::vector<Node>& exp);
+  /**
+   * Get the set of equivalence classes of type string.
+   */
+  const std::vector<Node>& getStringEqc() const;
+  //-----------------------end query functions
+
+ private:
+  /**
+   * A term index that considers terms modulo flattening and constant merging
+   * for concatenation terms.
+   */
+  class TermIndex
+  {
+   public:
+    /** Add n to this trie
+     *
+     * A term is indexed by flattening arguments of concatenation terms,
+     * and replacing them by (non-empty) constants when possible, for example
+     * if n is (str.++ x y z) and x = "abc" and y = "" are asserted, then n is
+     * indexed by ("abc", z).
+     *
+     * index: the child of n we are currently processing,
+     * s : reference to solver state,
+     * er : the representative of the empty equivalence class.
+     *
+     * We store the vector of terms that n was indexed by in the vector c.
+     */
+    Node add(TNode n,
+             unsigned index,
+             const SolverState& s,
+             Node er,
+             std::vector<Node>& c);
+    /** Clear this trie */
+    void clear() { d_children.clear(); }
+    /** The data at this node of the trie */
+    Node d_data;
+    /** The children of this node of the trie */
+    std::map<TNode, TermIndex> d_children;
+  };
+  /**
+   * This method is called as we are traversing the term index ti, where vecc
+   * accumulates the list of constants in the path to ti. If ti has a non-null
+   * data n, then we have inferred that d_data is equivalent to the
+   * constant specified by vecc.
+   */
+  void checkConstantEquivalenceClasses(TermIndex* ti, std::vector<Node>& vecc);
+  /** The solver state object */
+  SolverState& d_state;
+  /** The (custom) output channel of the theory of strings */
+  InferenceManager& d_im;
+  /** Commonly used constants */
+  Node d_emptyString;
+  Node d_false;
+  /**
+   * A congruence class is a set of terms f( t1 ), ..., f( tn ) where
+   * t1 = ... = tn. Congruence classes are important since all but
+   * one of the above terms (the representative of the congruence class)
+   * can be ignored by the solver.
+   *
+   * This set contains a set of nodes that are not representatives of their
+   * congruence class. This set is used to skip reasoning about terms in
+   * various inference schemas implemnted by this class.
+   */
+  NodeSet d_congruent;
+  /**
+   * The following three vectors are used for tracking constants that each
+   * equivalence class is entailed to be equal to.
+   * - The map d_eqcToConst maps (representatives) r of equivalence classes to
+   * the constant that that equivalence class is entailed to be equal to,
+   * - The term d_eqcToConstBase[r] is the term in the equivalence class r
+   * that is entailed to be equal to the constant d_eqcToConst[r],
+   * - The term d_eqcToConstExp[r] is the explanation of why
+   * d_eqcToConstBase[r] is equal to d_eqcToConst[r].
+   *
+   * For example, consider the equivalence class { r, x++"a"++y, x++z }, and
+   * assume x = "" and y = "bb" in the current context. We have that
+   *   d_eqcToConst[r] = "abb",
+   *   d_eqcToConstBase[r] = x++"a"++y
+   *   d_eqcToConstExp[r] = ( x = "" AND y = "bb" )
+   *
+   * This information is computed during checkInit and is used during various
+   * inference schemas for deriving inferences.
+   */
+  std::map<Node, Node> d_eqcToConst;
+  std::map<Node, Node> d_eqcToConstBase;
+  std::map<Node, Node> d_eqcToConstExp;
+  /** The list of equivalence classes of type string */
+  std::vector<Node> d_stringsEqc;
+  /** A term index for each function kind */
+  std::map<Kind, TermIndex> d_termIndex;
+}; /* class BaseSolver */
+
+}  // namespace strings
+}  // namespace theory
+}  // namespace CVC4
+
+#endif /* CVC4__THEORY__STRINGS__BASE_SOLVER_H */
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index c3a67aec9..7ebc5f35f 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -62,30 +62,6 @@ std::ostream& operator<<(std::ostream& out, InferStep s)
   return out;
 }
 
-Node TheoryStrings::TermIndex::add(TNode n,
-                                   unsigned index,
-                                   const SolverState& s,
-                                   Node er,
-                                   std::vector<Node>& c)
-{
-  if( index==n.getNumChildren() ){
-    if( d_data.isNull() ){
-      d_data = n;
-    }
-    return d_data;
-  }else{
-    Assert(index < n.getNumChildren());
-    TNode nir = s.getRepresentative(n[index]);
-    //if it is empty, and doing CONCAT, ignore
-    if( nir==er && n.getKind()==kind::STRING_CONCAT ){
-      return add(n, index + 1, s, er, c);
-    }else{
-      c.push_back( nir );
-      return d_children[nir].add(n, index + 1, s, er, c);
-    }
-  }
-}
-
 TheoryStrings::TheoryStrings(context::Context* c,
                              context::UserContext* u,
                              OutputChannel& out,
@@ -101,12 +77,12 @@ TheoryStrings::TheoryStrings(context::Context* c,
       d_registered_terms_cache(u),
       d_preproc(&d_sk_cache, u),
       d_extf_infer_cache(c),
-      d_congruent(c),
       d_proxy_var(u),
       d_proxy_var_to_length(u),
       d_functionsTerms(c),
       d_has_extf(c, false),
       d_has_str_code(false),
+      d_bsolver(c, u, d_state, d_im),
       d_regexp_solver(*this, d_state, d_im, c, u),
       d_input_vars(u),
       d_input_var_lsum(u),
@@ -297,22 +273,10 @@ Node TheoryStrings::getCurrentSubstitutionFor(int effort,
     return mv;
   }
   Node nr = d_state.getRepresentative(n);
-  std::map<Node, Node>::iterator itc = d_eqc_to_const.find(nr);
-  if (itc != d_eqc_to_const.end())
+  Node c = d_bsolver.explainConstantEqc(n, nr, exp);
+  if (!c.isNull())
   {
-    // constant equivalence classes
-    Trace("strings-subs") << "   constant eqc : " << d_eqc_to_const_exp[nr]
-                          << " " << d_eqc_to_const_base[nr] << " " << nr
-                          << std::endl;
-    if (!d_eqc_to_const_exp[nr].isNull())
-    {
-      exp.push_back(d_eqc_to_const_exp[nr]);
-    }
-    if (!d_eqc_to_const_base[nr].isNull())
-    {
-      d_im.addToExplanation(n, d_eqc_to_const_base[nr], exp);
-    }
-    return itc->second;
+    return c;
   }
   else if (effort >= 1 && n.getType().isString())
   {
@@ -1244,266 +1208,6 @@ void TheoryStrings::assertPendingFact(Node atom, bool polarity, Node exp) {
   Trace("strings-pending-debug") << "  Finished collect terms" << std::endl;
 }
 
-void TheoryStrings::checkInit() {
-  //build term index
-  d_eqc_to_const.clear();
-  d_eqc_to_const_base.clear();
-  d_eqc_to_const_exp.clear();
-  d_eqc_to_len_term.clear();
-  d_term_index.clear();
-  d_strings_eqc.clear();
-
-  std::map< Kind, unsigned > ncongruent;
-  std::map< Kind, unsigned > congruent;
-  d_emptyString_r = d_state.getRepresentative(d_emptyString);
-  eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
-  while( !eqcs_i.isFinished() ){
-    Node eqc = (*eqcs_i);
-    TypeNode tn = eqc.getType();
-    if( !tn.isRegExp() ){
-      if( tn.isString() ){
-        d_strings_eqc.push_back( eqc );
-      }
-      Node var;
-      eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine );
-      while( !eqc_i.isFinished() ) {
-        Node n = *eqc_i;
-        if( n.isConst() ){
-          d_eqc_to_const[eqc] = n;
-          d_eqc_to_const_base[eqc] = n;
-          d_eqc_to_const_exp[eqc] = Node::null();
-        }else if( tn.isInteger() ){
-          if( n.getKind()==kind::STRING_LENGTH ){
-            Node nr = d_state.getRepresentative(n[0]);
-            d_eqc_to_len_term[nr] = n[0];
-          }
-        }else if( n.getNumChildren()>0 ){
-          Kind k = n.getKind();
-          if( k!=kind::EQUAL ){
-            if( d_congruent.find( n )==d_congruent.end() ){
-              std::vector< Node > c;
-              Node nc = d_term_index[k].add(n, 0, d_state, d_emptyString_r, c);
-              if( nc!=n ){
-                //check if we have inferred a new equality by removal of empty components
-                if (n.getKind() == kind::STRING_CONCAT
-                    && !d_state.areEqual(nc, n))
-                {
-                  std::vector< Node > exp;
-                  unsigned count[2] = { 0, 0 };
-                  while( count[0]<nc.getNumChildren() || count[1]<n.getNumChildren() ){
-                    //explain empty prefixes
-                    for( unsigned t=0; t<2; t++ ){
-                      Node nn = t==0 ? nc : n;
-                      while (
-                          count[t] < nn.getNumChildren()
-                          && (nn[count[t]] == d_emptyString
-                              || d_state.areEqual(nn[count[t]], d_emptyString)))
-                      {
-                        if( nn[count[t]]!=d_emptyString ){
-                          exp.push_back( nn[count[t]].eqNode( d_emptyString ) );
-                        }
-                        count[t]++;
-                      }
-                    }
-                    //explain equal components
-                    if( count[0]<nc.getNumChildren() ){
-                      Assert(count[1] < n.getNumChildren());
-                      if( nc[count[0]]!=n[count[1]] ){
-                        exp.push_back( nc[count[0]].eqNode( n[count[1]] ) );
-                      }
-                      count[0]++;
-                      count[1]++;
-                    }
-                  }
-                  //infer the equality
-                  d_im.sendInference(exp, n.eqNode(nc), "I_Norm");
-                }
-                else if (getExtTheory()->hasFunctionKind(n.getKind()))
-                {
-                  //mark as congruent : only process if neither has been reduced
-                  getExtTheory()->markCongruent( nc, n );
-                }
-                //this node is congruent to another one, we can ignore it
-                Trace("strings-process-debug")
-                    << "  congruent term : " << n << " (via " << nc << ")"
-                    << std::endl;
-                d_congruent.insert( n );
-                congruent[k]++;
-              }else if( k==kind::STRING_CONCAT && c.size()==1 ){
-                Trace("strings-process-debug") << "  congruent term by singular : " << n << " " << c[0] << std::endl;
-                //singular case
-                if (!d_state.areEqual(c[0], n))
-                {
-                  Node ns;
-                  std::vector< Node > exp;
-                  //explain empty components
-                  bool foundNEmpty = false;
-                  for( unsigned i=0; i<n.getNumChildren(); i++ ){
-                    if (d_state.areEqual(n[i], d_emptyString))
-                    {
-                      if( n[i]!=d_emptyString ){
-                        exp.push_back( n[i].eqNode( d_emptyString ) );
-                      }
-                    }
-                    else
-                    {
-                      Assert(!foundNEmpty);
-                      ns = n[i];
-                      foundNEmpty = true;
-                    }
-                  }
-                  AlwaysAssert(foundNEmpty);
-                  //infer the equality
-                  d_im.sendInference(exp, n.eqNode(ns), "I_Norm_S");
-                }
-                d_congruent.insert( n );
-                congruent[k]++;
-              }else{
-                ncongruent[k]++;
-              }
-            }else{
-              congruent[k]++;
-            }
-          }
-        }else{
-          if( d_congruent.find( n )==d_congruent.end() ){
-            // We mark all but the oldest variable in the equivalence class as
-            // congruent.
-            if (var.isNull())
-            {
-              var = n;
-            }
-            else if (var > n)
-            {
-              Trace("strings-process-debug")
-                  << "  congruent variable : " << var << std::endl;
-              d_congruent.insert(var);
-              var = n;
-            }
-            else
-            {
-              Trace("strings-process-debug")
-                  << "  congruent variable : " << n << std::endl;
-              d_congruent.insert(n);
-            }
-          }
-        }
-        ++eqc_i;
-      }
-    }
-    ++eqcs_i;
-  }
-  if( Trace.isOn("strings-process") ){
-    for( std::map< Kind, TermIndex >::iterator it = d_term_index.begin(); it != d_term_index.end(); ++it ){
-      Trace("strings-process") << "  Terms[" << it->first << "] = " << ncongruent[it->first] << "/" << (congruent[it->first]+ncongruent[it->first]) << std::endl;
-    }
-  }
-}
-
-void TheoryStrings::checkConstantEquivalenceClasses()
-{
-  // do fixed point
-  unsigned prevSize;
-  std::vector<Node> vecc;
-  do
-  {
-    vecc.clear();
-    Trace("strings-process-debug") << "Check constant equivalence classes..."
-                                   << std::endl;
-    prevSize = d_eqc_to_const.size();
-    checkConstantEquivalenceClasses(&d_term_index[kind::STRING_CONCAT], vecc);
-  } while (!d_im.hasProcessed() && d_eqc_to_const.size() > prevSize);
-}
-
-void TheoryStrings::checkConstantEquivalenceClasses( TermIndex* ti, std::vector< Node >& vecc ) {
-  Node n = ti->d_data;
-  if( !n.isNull() ){
-    //construct the constant
-    Node c = utils::mkNConcat(vecc);
-    if (!d_state.areEqual(n, c))
-    {
-      Trace("strings-debug") << "Constant eqc : " << c << " for " << n << std::endl;
-      Trace("strings-debug") << "  ";
-      for( unsigned i=0; i<vecc.size(); i++ ){
-        Trace("strings-debug") << vecc[i] << " ";
-      }
-      Trace("strings-debug") << std::endl;
-      unsigned count = 0;
-      unsigned countc = 0;
-      std::vector< Node > exp;
-      while( count<n.getNumChildren() ){
-        while (count < n.getNumChildren()
-               && d_state.areEqual(n[count], d_emptyString))
-        {
-          d_im.addToExplanation(n[count], d_emptyString, exp);
-          count++;
-        }
-        if( count<n.getNumChildren() ){
-          Trace("strings-debug") << "...explain " << n[count] << " " << vecc[countc] << std::endl;
-          if (!d_state.areEqual(n[count], vecc[countc]))
-          {
-            Node nrr = d_state.getRepresentative(n[count]);
-            Assert(!d_eqc_to_const_exp[nrr].isNull());
-            d_im.addToExplanation(n[count], d_eqc_to_const_base[nrr], exp);
-            exp.push_back( d_eqc_to_const_exp[nrr] );
-          }
-          else
-          {
-            d_im.addToExplanation(n[count], vecc[countc], exp);
-          }
-          countc++;
-          count++;
-        }
-      }
-      //exp contains an explanation of n==c
-      Assert(countc == vecc.size());
-      if (d_state.hasTerm(c))
-      {
-        d_im.sendInference(exp, n.eqNode(c), "I_CONST_MERGE");
-        return;
-      }
-      else if (!d_im.hasProcessed())
-      {
-        Node nr = d_state.getRepresentative(n);
-        std::map< Node, Node >::iterator it = d_eqc_to_const.find( nr );
-        if( it==d_eqc_to_const.end() ){
-          Trace("strings-debug") << "Set eqc const " << n << " to " << c << std::endl;
-          d_eqc_to_const[nr] = c;
-          d_eqc_to_const_base[nr] = n;
-          d_eqc_to_const_exp[nr] = utils::mkAnd(exp);
-        }else if( c!=it->second ){
-          //conflict
-          Trace("strings-debug") << "Conflict, other constant was " << it->second << ", this constant was " << c << std::endl;
-          if( d_eqc_to_const_exp[nr].isNull() ){
-            // n==c ^ n == c' => false
-            d_im.addToExplanation(n, it->second, exp);
-          }else{
-            // n==c ^ n == d_eqc_to_const_base[nr] == c' => false
-            exp.push_back( d_eqc_to_const_exp[nr] );
-            d_im.addToExplanation(n, d_eqc_to_const_base[nr], exp);
-          }
-          d_im.sendInference(exp, d_false, "I_CONST_CONFLICT");
-          return;
-        }else{
-          Trace("strings-debug") << "Duplicate constant." << std::endl;
-        }
-      }
-    }
-  }
-  for( std::map< TNode, TermIndex >::iterator it = ti->d_children.begin(); it != ti->d_children.end(); ++it ){
-    std::map< Node, Node >::iterator itc = d_eqc_to_const.find( it->first );
-    if( itc!=d_eqc_to_const.end() ){
-      vecc.push_back( itc->second );
-      checkConstantEquivalenceClasses( &it->second, vecc );
-      vecc.pop_back();
-      if (d_im.hasProcessed())
-      {
-        break;
-      }
-    }
-  }
-}
-
 void TheoryStrings::checkExtfEval( int effort ) {
   Trace("strings-extf-list") << "Active extended functions, effort=" << effort << " : " << std::endl;
   d_extf_info_tmp.clear();
@@ -1515,11 +1219,7 @@ void TheoryStrings::checkExtfEval( int effort ) {
     // Setup information about n, including if it is equal to a constant.
     ExtfInfoTmp& einfo = d_extf_info_tmp[n];
     Node r = d_state.getRepresentative(n);
-    std::map<Node, Node>::iterator itcit = d_eqc_to_const.find(r);
-    if (itcit != d_eqc_to_const.end())
-    {
-      einfo.d_const = itcit->second;
-    }
+    einfo.d_const = d_bsolver.getConstantEqc(r);
     // Get the current values of the children of n.
     // Notice that we look up the value of the direct children of n, and not
     // their free variables. In other words, given a term:
@@ -1718,16 +1418,8 @@ void TheoryStrings::checkExtfInference( Node n, Node nr, ExtfInfoTmp& in, int ef
   {
     // otherwise, must explain via base node
     Node r = d_state.getRepresentative(n);
-    // we have that:
-    //   d_eqc_to_const_exp[r] => d_eqc_to_const_base[r] = in.d_const
-    // thus:
-    //   n = d_eqc_to_const_base[r] ^ d_eqc_to_const_exp[r] => n = in.d_const
-    Assert(d_eqc_to_const_base.find(r) != d_eqc_to_const_base.end());
-    d_im.addToExplanation(n, d_eqc_to_const_base[r], in.d_exp);
-    Assert(d_eqc_to_const_exp.find(r) != d_eqc_to_const_exp.end());
-    in.d_exp.insert(in.d_exp.end(),
-                    d_eqc_to_const_exp[r].begin(),
-                    d_eqc_to_const_exp[r].end());
+    // explain using the base solver
+    d_bsolver.explainConstantEqc(n, r, in.d_exp);
   }
 
   // d_extf_infer_cache stores whether we have made the inferences associated
@@ -1932,15 +1624,6 @@ Node TheoryStrings::getSymbolicDefinition(Node n, std::vector<Node>& exp) const
   }
 }
 
-Node TheoryStrings::getConstantEqc( Node eqc ) {
-  std::map< Node, Node >::iterator it = d_eqc_to_const.find( eqc );
-  if( it!=d_eqc_to_const.end() ){
-    return it->second;
-  }else{
-    return Node::null();
-  }
-}
-
 void TheoryStrings::debugPrintFlatForms( const char * tc ){
   for( unsigned k=0; k<d_strings_eqc.size(); k++ ){
     Node eqc = d_strings_eqc[k];
@@ -1949,9 +1632,10 @@ void TheoryStrings::debugPrintFlatForms( const char * tc ){
     }else{
       Trace( tc ) << "eqc [" << eqc << "]";
     }
-    std::map< Node, Node >::iterator itc = d_eqc_to_const.find( eqc );
-    if( itc!=d_eqc_to_const.end() ){
-      Trace( tc ) << "  C: " << itc->second;
+    Node c = d_bsolver.getConstantEqc(eqc);
+    if (!c.isNull())
+    {
+      Trace(tc) << "  C: " << c;
       if( d_eqc[eqc].size()>1 ){
         Trace( tc ) << std::endl;
       }
@@ -1962,11 +1646,14 @@ void TheoryStrings::debugPrintFlatForms( const char * tc ){
         Trace( tc ) << "    ";
         for( unsigned j=0; j<d_flat_form[n].size(); j++ ){
           Node fc = d_flat_form[n][j];
-          itc = d_eqc_to_const.find( fc );
+          Node fcc = d_bsolver.getConstantEqc(fc);
           Trace( tc ) << " ";
-          if( itc!=d_eqc_to_const.end() ){
-            Trace( tc ) << itc->second;
-          }else{
+          if (!fcc.isNull())
+          {
+            Trace(tc) << fcc;
+          }
+          else
+          {
             Trace( tc ) << fc;
           }
         }
@@ -2009,17 +1696,18 @@ void TheoryStrings::checkCycles()
   d_flat_form.clear();
   d_flat_form_index.clear();
   d_eqc.clear();
-  //rebuild strings eqc based on acyclic ordering
-  std::vector< Node > eqc;
-  eqc.insert( eqc.end(), d_strings_eqc.begin(), d_strings_eqc.end() );
+  // Rebuild strings eqc based on acyclic ordering, first copy the equivalence
+  // classes from the base solver.
+  std::vector<Node> eqc = d_bsolver.getStringEqc();
   d_strings_eqc.clear();
   if( options::stringBinaryCsp() ){
     //sort: process smallest constants first (necessary if doing binary splits)
     sortConstLength scl;
     for( unsigned i=0; i<eqc.size(); i++ ){
-      std::map< Node, Node >::iterator itc = d_eqc_to_const.find( eqc[i] );
-      if( itc!=d_eqc_to_const.end() ){
-        scl.d_const_length[eqc[i]] = itc->second.getConst<String>().size();
+      Node ci = d_bsolver.getConstantEqc(eqc[i]);
+      if (!ci.isNull())
+      {
+        scl.d_const_length[eqc[i]] = ci.getConst<String>().size();
       }
     }
     std::sort( eqc.begin(), eqc.end(), scl );
@@ -2049,7 +1737,7 @@ void TheoryStrings::checkFlatForms()
   //(1) approximate equality by containment, infer conflicts
   for (const Node& eqc : d_strings_eqc)
   {
-    Node c = getConstantEqc(eqc);
+    Node c = d_bsolver.getConstantEqc(eqc);
     if (!c.isNull())
     {
       // if equivalence class is constant, all component constants in flat forms
@@ -2071,13 +1759,7 @@ void TheoryStrings::checkFlatForms()
             // conflict, explanation is n = base ^ base = c ^ relevant portion
             // of ( n = f[n] )
             std::vector<Node> exp;
-            Assert(d_eqc_to_const_base.find(eqc) != d_eqc_to_const_base.end());
-            d_im.addToExplanation(n, d_eqc_to_const_base[eqc], exp);
-            Assert(d_eqc_to_const_exp.find(eqc) != d_eqc_to_const_exp.end());
-            if (!d_eqc_to_const_exp[eqc].isNull())
-            {
-              exp.push_back(d_eqc_to_const_exp[eqc]);
-            }
+            d_bsolver.explainConstantEqc(n, eqc, exp);
             for (int e = firstc; e <= lastc; e++)
             {
               if (d_flat_form[n][e].isConst())
@@ -2216,7 +1898,7 @@ void TheoryStrings::checkFlatForm(std::vector<Node>& eqc,
     else
     {
       Node curr = d_flat_form[a][count];
-      Node curr_c = getConstantEqc(curr);
+      Node curr_c = d_bsolver.getConstantEqc(curr);
       Node ac = a[d_flat_form_index[a][count]];
       std::vector<Node> lexp;
       Node lcurr = d_state.getLength(ac, lexp);
@@ -2254,7 +1936,7 @@ void TheoryStrings::checkFlatForm(std::vector<Node>& eqc,
             Node bc = b[d_flat_form_index[b][count]];
             inelig.push_back(b);
             Assert(!d_state.areEqual(curr, cc));
-            Node cc_c = getConstantEqc(cc);
+            Node cc_c = d_bsolver.getConstantEqc(cc);
             if (!curr_c.isNull() && !cc_c.isNull())
             {
               // check for constant conflict
@@ -2263,10 +1945,8 @@ void TheoryStrings::checkFlatForm(std::vector<Node>& eqc,
                   cc_c, curr_c, index, isRev);
               if (s.isNull())
               {
-                d_im.addToExplanation(ac, d_eqc_to_const_base[curr], exp);
-                d_im.addToExplanation(d_eqc_to_const_exp[curr], exp);
-                d_im.addToExplanation(bc, d_eqc_to_const_base[cc], exp);
-                d_im.addToExplanation(d_eqc_to_const_exp[cc], exp);
+                d_bsolver.explainConstantEqc(ac, curr, exp);
+                d_bsolver.explainConstantEqc(bc, cc, exp);
                 conc = d_false;
                 infType = FlatFormInfer::CONST;
                 break;
@@ -2386,25 +2066,32 @@ Node TheoryStrings::checkCycles( Node eqc, std::vector< Node >& curr, std::vecto
     eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine );
     while( !eqc_i.isFinished() ) {
       Node n = (*eqc_i);
-      if( d_congruent.find( n )==d_congruent.end() ){
+      if (!d_bsolver.isCongruent(n))
+      {
         if( n.getKind() == kind::STRING_CONCAT ){
           Trace("strings-cycle") << eqc << " check term : " << n << " in " << eqc << std::endl;
-          if( eqc!=d_emptyString_r ){
+          if (eqc != d_emptyString)
+          {
             d_eqc[eqc].push_back( n );
           }
           for( unsigned i=0; i<n.getNumChildren(); i++ ){
             Node nr = d_state.getRepresentative(n[i]);
-            if( eqc==d_emptyString_r ){
+            if (eqc == d_emptyString)
+            {
               //for empty eqc, ensure all components are empty
-              if( nr!=d_emptyString_r ){
+              if (nr != d_emptyString)
+              {
                 std::vector< Node > exp;
                 exp.push_back( n.eqNode( d_emptyString ) );
                 d_im.sendInference(
                     exp, n[i].eqNode(d_emptyString), "I_CYCLE_E");
                 return Node::null();
               }
-            }else{
-              if( nr!=d_emptyString_r ){
+            }
+            else
+            {
+              if (nr != d_emptyString)
+              {
                 d_flat_form[n].push_back( nr );
                 d_flat_form_index[n].push_back( i );
               }
@@ -2460,7 +2147,7 @@ void TheoryStrings::checkRegisterTermsPreNormalForm()
     while (!eqc_i.isFinished())
     {
       Node n = (*eqc_i);
-      if (d_congruent.find(n) == d_congruent.end())
+      if (!d_bsolver.isCongruent(n))
       {
         registerTerm(n, 2);
       }
@@ -2686,7 +2373,8 @@ void TheoryStrings::getNormalForms(Node eqc,
   eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine );
   while( !eqc_i.isFinished() ){
     Node n = (*eqc_i);
-    if( d_congruent.find( n )==d_congruent.end() ){
+    if (!d_bsolver.isCongruent(n))
+    {
       if (n.getKind() == CONST_STRING || n.getKind() == STRING_CONCAT)
       {
         Trace("strings-process-debug") << "Get Normal Form : Process term " << n << " in eqc " << eqc << std::endl;
@@ -2867,7 +2555,7 @@ void TheoryStrings::getNormalForms(Node eqc,
     }
     
     //if equivalence class is constant, approximate as containment, infer conflicts
-    Node c = getConstantEqc( eqc );
+    Node c = d_bsolver.getConstantEqc(eqc);
     if( !c.isNull() ){
       Trace("strings-solve") << "Eqc is constant " << c << std::endl;
       for (unsigned i = 0, size = normal_forms.size(); i < size; i++)
@@ -2882,12 +2570,7 @@ void TheoryStrings::getNormalForms(Node eqc,
           Trace("strings-solve") << "Normal form for " << n << " cannot be contained in constant " << c << std::endl;
           //conflict, explanation is n = base ^ base = c ^ relevant porition of ( n = N[n] )
           std::vector< Node > exp;
-          Assert(d_eqc_to_const_base.find(eqc) != d_eqc_to_const_base.end());
-          d_im.addToExplanation(n, d_eqc_to_const_base[eqc], exp);
-          Assert(d_eqc_to_const_exp.find(eqc) != d_eqc_to_const_exp.end());
-          if( !d_eqc_to_const_exp[eqc].isNull() ){
-            exp.push_back( d_eqc_to_const_exp[eqc] );
-          }
+          d_bsolver.explainConstantEqc(n, eqc, exp);
           //TODO: this can be minimized based on firstc/lastc, normal_forms_exp_depend
           exp.insert(exp.end(), nf.d_exp.begin(), nf.d_exp.end());
           Node conc = d_false;
@@ -3850,7 +3533,7 @@ int TheoryStrings::processSimpleDeq( std::vector< Node >& nfi, std::vector< Node
   {
     for (unsigned i = 0; i < 2; i++)
     {
-      Node c = getConstantEqc(i == 0 ? ni : nj);
+      Node c = d_bsolver.getConstantEqc(i == 0 ? ni : nj);
       if (!c.isNull())
       {
         int findex, lindex;
@@ -4465,8 +4148,8 @@ void TheoryStrings::runInferStep(InferStep s, int effort)
   Trace("strings-process") << "..." << std::endl;
   switch (s)
   {
-    case CHECK_INIT: checkInit(); break;
-    case CHECK_CONST_EQC: checkConstantEquivalenceClasses(); break;
+    case CHECK_INIT: d_bsolver.checkInit(); break;
+    case CHECK_CONST_EQC: d_bsolver.checkConstantEquivalenceClasses(); break;
     case CHECK_EXTF_EVAL: checkExtfEval(effort); break;
     case CHECK_CYCLES: checkCycles(); break;
     case CHECK_FLAT_FORMS: checkFlatForms(); break;
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index ce92ada86..3b53fcded 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -24,6 +24,7 @@
 #include "expr/attribute.h"
 #include "expr/node_trie.h"
 #include "theory/decision_manager.h"
+#include "theory/strings/base_solver.h"
 #include "theory/strings/infer_info.h"
 #include "theory/strings/inference_manager.h"
 #include "theory/strings/normal_form.h"
@@ -244,30 +245,6 @@ class TheoryStrings : public Theory {
   NodeSet d_extf_infer_cache;
   std::vector< Node > d_empty_vec;
 private:
-  NodeSet d_congruent;
-  /**
-   * The following three vectors are used for tracking constants that each
-   * equivalence class is entailed to be equal to.
-   * - The map d_eqc_to_const maps (representatives) r of equivalence classes to
-   * the constant that that equivalence class is entailed to be equal to,
-   * - The term d_eqc_to_const_base[r] is the term in the equivalence class r
-   * that is entailed to be equal to the constant d_eqc_to_const[r],
-   * - The term d_eqc_to_const_exp[r] is the explanation of why
-   * d_eqc_to_const_base[r] is equal to d_eqc_to_const[r].
-   *
-   * For example, consider the equivalence class { r, x++"a"++y, x++z }, and
-   * assume x = "" and y = "bb" in the current context. We have that
-   *   d_eqc_to_const[r] = "abb",
-   *   d_eqc_to_const_base[r] = x++"a"++y
-   *   d_eqc_to_const_exp[r] = ( x = "" AND y = "bb" )
-   *
-   * This information is computed during checkInit and is used during various
-   * inference schemas for deriving inferences.
-   */
-  std::map< Node, Node > d_eqc_to_const;
-  std::map< Node, Node > d_eqc_to_const_base;
-  std::map< Node, Node > d_eqc_to_const_exp;
-  Node getConstantEqc( Node eqc );
   /**
    * Get the current substitution for term n.
    *
@@ -285,19 +262,6 @@ private:
 
   std::map< Node, Node > d_eqc_to_len_term;
   std::vector< Node > d_strings_eqc;
-  Node d_emptyString_r;
-  class TermIndex {
-  public:
-    Node d_data;
-    std::map< TNode, TermIndex > d_children;
-    Node add(TNode n,
-             unsigned index,
-             const SolverState& s,
-             Node er,
-             std::vector<Node>& c);
-    void clear(){ d_children.clear(); }
-  };
-  std::map< Kind, TermIndex > d_term_index;
   //list of non-congruent concat terms in each eqc
   std::map< Node, std::vector< Node > > d_eqc;
   std::map< Node, std::vector< Node > > d_flat_form;
@@ -360,7 +324,6 @@ private:
   /** cache of all skolems */
   SkolemCache d_sk_cache;
 
-  void checkConstantEquivalenceClasses( TermIndex* ti, std::vector< Node >& vecc );
   /** Get proxy variable
    *
    * If this method returns the proxy variable for (string) term n if one
@@ -619,6 +582,11 @@ private:
 
   // Symbolic Regular Expression
  private:
+  /**
+   * The base solver, responsible for reasoning about congruent terms and
+   * inferring constants for equivalence classes.
+   */
+  BaseSolver d_bsolver;
   /** regular expression solver module */
   RegExpSolver d_regexp_solver;
   /** regular expression elimination module */
@@ -688,28 +656,6 @@ private:
 
  private:
   //-----------------------inference steps
-  /** check initial
-   *
-   * This function initializes term indices for each strings function symbol.
-   * One key aspect of this construction is that concat terms are indexed by
-   * their list of non-empty components. For example, if x = "" is an equality
-   * asserted in this SAT context, then y ++ x ++ z may be indexed by (y,z).
-   * This method may infer various facts while building these term indices, for
-   * instance, based on congruence. An example would be inferring:
-   *   y ++ x ++ z = y ++ z
-   * if both terms are registered in this SAT context.
-   *
-   * This function should be called as a first step of any strategy.
-   */
-  void checkInit();
-  /** check constant equivalence classes
-   *
-   * This function infers whether CONCAT terms can be simplified to constants.
-   * For example, if x = "a" and y = "b" are equalities in the current SAT
-   * context, then we may infer x ++ "c" ++ y is equivalent to "acb". In this
-   * case, we infer the fact x ++ "c" ++ y = "acb".
-   */
-  void checkConstantEquivalenceClasses();
   /** check extended functions evaluation
    *
    * This applies "context-dependent simplification" for all active extended