Clean the header file of TheoryStrings (#4272)

Now conforms to coding guidelines. For the sake of ensuring that the aspects related to the strategy were maintained in one place, I split this to its own file, strategy.h/cpp.

5 files changed, 397 insertions, 334 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index c50578c46..d16164562 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -716,6 +716,8 @@ libcvc4_add_sources(
   theory/strings/skolem_cache.h
   theory/strings/solver_state.cpp
   theory/strings/solver_state.h
+  theory/strings/strategy.cpp
+  theory/strings/strategy.h
   theory/strings/strings_entail.cpp
   theory/strings/strings_entail.h
   theory/strings/strings_fmf.cpp
diff --git a/src/theory/strings/strategy.cpp b/src/theory/strings/strategy.cpp
new file mode 100644
index 000000000..549bba9d6
--- /dev/null
+++ b/src/theory/strings/strategy.cpp
@@ -0,0 +1,161 @@
+/*********************                                                        */
+/*! \file strategy.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds, Tianyi Liang, Morgan Deters
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Implementation of the strategy of the theory of strings.
+ **/
+
+#include "theory/strings/strategy.h"
+
+#include "options/strings_options.h"
+
+namespace CVC4 {
+namespace theory {
+namespace strings {
+
+std::ostream& operator<<(std::ostream& out, InferStep s)
+{
+  switch (s)
+  {
+    case BREAK: out << "break"; break;
+    case CHECK_INIT: out << "check_init"; break;
+    case CHECK_CONST_EQC: out << "check_const_eqc"; break;
+    case CHECK_EXTF_EVAL: out << "check_extf_eval"; break;
+    case CHECK_CYCLES: out << "check_cycles"; break;
+    case CHECK_FLAT_FORMS: out << "check_flat_forms"; break;
+    case CHECK_NORMAL_FORMS_EQ: out << "check_normal_forms_eq"; break;
+    case CHECK_NORMAL_FORMS_DEQ: out << "check_normal_forms_deq"; break;
+    case CHECK_CODES: out << "check_codes"; break;
+    case CHECK_LENGTH_EQC: out << "check_length_eqc"; break;
+    case CHECK_EXTF_REDUCTION: out << "check_extf_reduction"; break;
+    case CHECK_MEMBERSHIP: out << "check_membership"; break;
+    case CHECK_CARDINALITY: out << "check_cardinality"; break;
+    default: out << "?"; break;
+  }
+  return out;
+}
+
+Strategy::Strategy() : d_strategy_init(false) {}
+
+Strategy::~Strategy() {}
+
+bool Strategy::isStrategyInit() const { return d_strategy_init; }
+
+bool Strategy::hasStrategyEffort(Theory::Effort e) const
+{
+  return d_strat_steps.find(e) != d_strat_steps.end();
+}
+
+std::vector<std::pair<InferStep, int> >::iterator Strategy::stepBegin(
+    Theory::Effort e)
+{
+  std::map<Theory::Effort, std::pair<unsigned, unsigned> >::const_iterator it =
+      d_strat_steps.find(e);
+  Assert(it != d_strat_steps.end());
+  return d_infer_steps.begin() + it->second.first;
+}
+
+std::vector<std::pair<InferStep, int> >::iterator Strategy::stepEnd(
+    Theory::Effort e)
+{
+  std::map<Theory::Effort, std::pair<unsigned, unsigned> >::const_iterator it =
+      d_strat_steps.find(e);
+  Assert(it != d_strat_steps.end());
+  return d_infer_steps.begin() + it->second.second;
+}
+
+void Strategy::addStrategyStep(InferStep s, int effort, bool addBreak)
+{
+  // must run check init first
+  Assert((s == CHECK_INIT) == d_infer_steps.empty());
+  d_infer_steps.push_back(std::pair<InferStep, int>(s, effort));
+  if (addBreak)
+  {
+    d_infer_steps.push_back(std::pair<InferStep, int>(BREAK, 0));
+  }
+}
+
+void Strategy::initializeStrategy()
+{
+  // initialize the strategy if not already done so
+  if (!d_strategy_init)
+  {
+    std::map<Theory::Effort, unsigned> step_begin;
+    std::map<Theory::Effort, unsigned> step_end;
+    d_strategy_init = true;
+    // beginning indices
+    step_begin[Theory::EFFORT_FULL] = 0;
+    if (options::stringEager())
+    {
+      step_begin[Theory::EFFORT_STANDARD] = 0;
+    }
+    // add the inference steps
+    addStrategyStep(CHECK_INIT);
+    addStrategyStep(CHECK_CONST_EQC);
+    addStrategyStep(CHECK_EXTF_EVAL, 0);
+    // we must check cycles before using flat forms
+    addStrategyStep(CHECK_CYCLES);
+    if (options::stringFlatForms())
+    {
+      addStrategyStep(CHECK_FLAT_FORMS);
+    }
+    addStrategyStep(CHECK_EXTF_REDUCTION, 1);
+    if (options::stringEager())
+    {
+      // do only the above inferences at standard effort, if applicable
+      step_end[Theory::EFFORT_STANDARD] = d_infer_steps.size() - 1;
+    }
+    if (!options::stringEagerLen())
+    {
+      addStrategyStep(CHECK_REGISTER_TERMS_PRE_NF);
+    }
+    addStrategyStep(CHECK_NORMAL_FORMS_EQ);
+    addStrategyStep(CHECK_EXTF_EVAL, 1);
+    if (!options::stringEagerLen() && options::stringLenNorm())
+    {
+      addStrategyStep(CHECK_LENGTH_EQC, 0, false);
+      addStrategyStep(CHECK_REGISTER_TERMS_NF);
+    }
+    addStrategyStep(CHECK_NORMAL_FORMS_DEQ);
+    addStrategyStep(CHECK_CODES);
+    if (options::stringEagerLen() && options::stringLenNorm())
+    {
+      addStrategyStep(CHECK_LENGTH_EQC);
+    }
+    if (options::stringExp() && !options::stringGuessModel())
+    {
+      addStrategyStep(CHECK_EXTF_REDUCTION, 2);
+    }
+    addStrategyStep(CHECK_MEMBERSHIP);
+    addStrategyStep(CHECK_CARDINALITY);
+    step_end[Theory::EFFORT_FULL] = d_infer_steps.size() - 1;
+    if (options::stringExp() && options::stringGuessModel())
+    {
+      step_begin[Theory::EFFORT_LAST_CALL] = d_infer_steps.size();
+      // these two steps are run in parallel
+      addStrategyStep(CHECK_EXTF_REDUCTION, 2, false);
+      addStrategyStep(CHECK_EXTF_EVAL, 3);
+      step_end[Theory::EFFORT_LAST_CALL] = d_infer_steps.size() - 1;
+    }
+    // set the beginning/ending ranges
+    for (const std::pair<const Theory::Effort, unsigned>& it_begin : step_begin)
+    {
+      Theory::Effort e = it_begin.first;
+      std::map<Theory::Effort, unsigned>::iterator it_end = step_end.find(e);
+      Assert(it_end != step_end.end());
+      d_strat_steps[e] =
+          std::pair<unsigned, unsigned>(it_begin.second, it_end->second);
+    }
+  }
+}
+
+}  // namespace strings
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/strings/strategy.h b/src/theory/strings/strategy.h
new file mode 100644
index 000000000..9afb6a92f
--- /dev/null
+++ b/src/theory/strings/strategy.h
@@ -0,0 +1,116 @@
+/*********************                                                        */
+/*! \file strategy.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 Strategy of the theory of strings
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__STRINGS__STRATEGY_H
+#define CVC4__THEORY__STRINGS__STRATEGY_H
+
+#include <map>
+#include <vector>
+
+#include "theory/theory.h"
+
+namespace CVC4 {
+namespace theory {
+namespace strings {
+
+/** inference steps
+ *
+ * Corresponds to a step in the overall strategy of the strings solver. For
+ * details on the individual steps, see documentation on the inference schemas
+ * within Strategy.
+ */
+enum InferStep
+{
+  // indicates that the strategy should break if lemmas or facts are added
+  BREAK,
+  // check initial
+  CHECK_INIT,
+  // check constant equivalence classes
+  CHECK_CONST_EQC,
+  // check extended function evaluation
+  CHECK_EXTF_EVAL,
+  // check cycles
+  CHECK_CYCLES,
+  // check flat forms
+  CHECK_FLAT_FORMS,
+  // check register terms pre-normal forms
+  CHECK_REGISTER_TERMS_PRE_NF,
+  // check normal forms equalities
+  CHECK_NORMAL_FORMS_EQ,
+  // check normal forms disequalities
+  CHECK_NORMAL_FORMS_DEQ,
+  // check codes
+  CHECK_CODES,
+  // check lengths for equivalence classes
+  CHECK_LENGTH_EQC,
+  // check register terms for normal forms
+  CHECK_REGISTER_TERMS_NF,
+  // check extended function reductions
+  CHECK_EXTF_REDUCTION,
+  // check regular expression memberships
+  CHECK_MEMBERSHIP,
+  // check cardinality
+  CHECK_CARDINALITY,
+};
+std::ostream& operator<<(std::ostream& out, InferStep i);
+
+/**
+ * The strategy of theory of strings.
+ *
+ * This stores a sequence of the above enum that indicates the calls to
+ * runInferStep to make on the theory of strings, given by parent.
+ */
+class Strategy
+{
+ public:
+  Strategy();
+  ~Strategy();
+  /** is this strategy initialized? */
+  bool isStrategyInit() const;
+  /** do we have a strategy for effort e? */
+  bool hasStrategyEffort(Theory::Effort e) const;
+  /** begin and end iterators for effort e */
+  std::vector<std::pair<InferStep, int> >::iterator stepBegin(Theory::Effort e);
+  std::vector<std::pair<InferStep, int> >::iterator stepEnd(Theory::Effort e);
+  /** initialize the strategy
+   *
+   * This initializes the above information based on the options. This makes
+   * a series of calls to addStrategyStep above.
+   */
+  void initializeStrategy();
+
+ private:
+  /** add strategy step
+   *
+   * This adds (s,effort) as a strategy step to the vectors d_infer_steps and
+   * d_infer_step_effort. This indicates that a call to runInferStep should
+   * be run as the next step in the strategy. If addBreak is true, we add
+   * a BREAK to the strategy following this step.
+   */
+  void addStrategyStep(InferStep s, int effort = 0, bool addBreak = true);
+  /** is strategy initialized */
+  bool d_strategy_init;
+  /** the strategy */
+  std::vector<std::pair<InferStep, int> > d_infer_steps;
+  /** the range (begin, end) of steps to run at given efforts */
+  std::map<Theory::Effort, std::pair<unsigned, unsigned> > d_strat_steps;
+}; /* class Strategy */
+
+}  // namespace strings
+}  // namespace theory
+}  // namespace CVC4
+
+#endif /* CVC4__THEORY__STRINGS__STRATEGY_H */
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 8b9eb7124..562d8eab8 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -10,20 +10,14 @@
  ** directory for licensing information.\endverbatim
  **
  ** \brief Implementation of the theory of strings.
- **
- ** Implementation of the theory of strings.
  **/
 
 #include "theory/strings/theory_strings.h"
 
-#include <cmath>
-
 #include "expr/kind.h"
 #include "options/strings_options.h"
 #include "options/theory_options.h"
-#include "smt/command.h"
 #include "smt/logic_exception.h"
-#include "smt/smt_statistics_registry.h"
 #include "theory/ext_theory.h"
 #include "theory/rewriter.h"
 #include "theory/strings/theory_strings_utils.h"
@@ -40,28 +34,6 @@ namespace CVC4 {
 namespace theory {
 namespace strings {
 
-std::ostream& operator<<(std::ostream& out, InferStep s)
-{
-  switch (s)
-  {
-    case BREAK: out << "break"; break;
-    case CHECK_INIT: out << "check_init"; break;
-    case CHECK_CONST_EQC: out << "check_const_eqc"; break;
-    case CHECK_EXTF_EVAL: out << "check_extf_eval"; break;
-    case CHECK_CYCLES: out << "check_cycles"; break;
-    case CHECK_FLAT_FORMS: out << "check_flat_forms"; break;
-    case CHECK_NORMAL_FORMS_EQ: out << "check_normal_forms_eq"; break;
-    case CHECK_NORMAL_FORMS_DEQ: out << "check_normal_forms_deq"; break;
-    case CHECK_CODES: out << "check_codes"; break;
-    case CHECK_LENGTH_EQC: out << "check_length_eqc"; break;
-    case CHECK_EXTF_REDUCTION: out << "check_extf_reduction"; break;
-    case CHECK_MEMBERSHIP: out << "check_membership"; break;
-    case CHECK_CARDINALITY: out << "check_cardinality"; break;
-    default: out << "?"; break;
-  }
-  return out;
-}
-
 TheoryStrings::TheoryStrings(context::Context* c,
                              context::UserContext* u,
                              OutputChannel& out,
@@ -79,8 +51,7 @@ TheoryStrings::TheoryStrings(context::Context* c,
       d_csolver(nullptr),
       d_esolver(nullptr),
       d_rsolver(nullptr),
-      d_stringsFmf(c, u, valuation, d_termReg),
-      d_strategy_init(false)
+      d_stringsFmf(c, u, valuation, d_termReg)
 {
   setupExtTheory();
   ExtTheory* extt = getExtTheory();
@@ -139,6 +110,15 @@ TheoryStrings::~TheoryStrings() {
 
 }
 
+TheoryRewriter* TheoryStrings::getTheoryRewriter() { return &d_rewriter; }
+std::string TheoryStrings::identify() const
+{
+  return std::string("TheoryStrings");
+}
+eq::EqualityEngine* TheoryStrings::getEqualityEngine()
+{
+  return &d_equalityEngine;
+}
 void TheoryStrings::finishInit()
 {
   TheoryModel* tm = d_valuation.getModel();
@@ -235,14 +215,9 @@ bool TheoryStrings::getCurrentSubstitution( int effort, std::vector< Node >& var
   return true;
 }
 
-/////////////////////////////////////////////////////////////////////////////
-// NOTIFICATIONS
-/////////////////////////////////////////////////////////////////////////////
-
-
 void TheoryStrings::presolve() {
   Debug("strings-presolve") << "TheoryStrings::Presolving : get fmf options " << (options::stringFMF() ? "true" : "false") << std::endl;
-  initializeStrategy();
+  d_strat.initializeStrategy();
 
   // if strings fmf is enabled, register the strategy
   if (options::stringFMF())
@@ -639,11 +614,9 @@ void TheoryStrings::check(Effort e) {
   }
   d_im->doPendingFacts();
 
-  Assert(d_strategy_init);
-  std::map<Effort, std::pair<unsigned, unsigned> >::iterator itsr =
-      d_strat_steps.find(e);
+  Assert(d_strat.isStrategyInit());
   if (!d_state.isInConflict() && !d_valuation.needCheck()
-      && itsr != d_strat_steps.end())
+      && d_strat.hasStrategyEffort(e))
   {
     Trace("strings-check-debug")
         << "Theory of strings " << e << " effort check " << std::endl;
@@ -684,15 +657,13 @@ void TheoryStrings::check(Effort e) {
       Trace("strings-eqc") << std::endl;
     }
     ++(d_statistics.d_checkRuns);
-    unsigned sbegin = itsr->second.first;
-    unsigned send = itsr->second.second;
     bool addedLemma = false;
     bool addedFact;
     Trace("strings-check") << "Full effort check..." << std::endl;
     do{
       ++(d_statistics.d_strategyRuns);
       Trace("strings-check") << "  * Run strategy..." << std::endl;
-      runStrategy(sbegin, send);
+      runStrategy(e);
       // flush the facts
       addedFact = d_im->hasPendingFact();
       addedLemma = d_im->hasPendingLemma();
@@ -1045,107 +1016,16 @@ void TheoryStrings::runInferStep(InferStep s, int effort)
                            << std::endl;
 }
 
-bool TheoryStrings::hasStrategyEffort(Effort e) const
-{
-  return d_strat_steps.find(e) != d_strat_steps.end();
-}
-
-void TheoryStrings::addStrategyStep(InferStep s, int effort, bool addBreak)
-{
-  // must run check init first
-  Assert((s == CHECK_INIT) == d_infer_steps.empty());
-  // must use check cycles when using flat forms
-  Assert(s != CHECK_FLAT_FORMS
-         || std::find(d_infer_steps.begin(), d_infer_steps.end(), CHECK_CYCLES)
-                != d_infer_steps.end());
-  d_infer_steps.push_back(s);
-  d_infer_step_effort.push_back(effort);
-  if (addBreak)
-  {
-    d_infer_steps.push_back(BREAK);
-    d_infer_step_effort.push_back(0);
-  }
-}
-
-void TheoryStrings::initializeStrategy()
+void TheoryStrings::runStrategy(Theory::Effort e)
 {
-  // initialize the strategy if not already done so
-  if (!d_strategy_init)
-  {
-    std::map<Effort, unsigned> step_begin;
-    std::map<Effort, unsigned> step_end;
-    d_strategy_init = true;
-    // beginning indices
-    step_begin[EFFORT_FULL] = 0;
-    if (options::stringEager())
-    {
-      step_begin[EFFORT_STANDARD] = 0;
-    }
-    // add the inference steps
-    addStrategyStep(CHECK_INIT);
-    addStrategyStep(CHECK_CONST_EQC);
-    addStrategyStep(CHECK_EXTF_EVAL, 0);
-    addStrategyStep(CHECK_CYCLES);
-    if (options::stringFlatForms())
-    {
-      addStrategyStep(CHECK_FLAT_FORMS);
-    }
-    addStrategyStep(CHECK_EXTF_REDUCTION, 1);
-    if (options::stringEager())
-    {
-      // do only the above inferences at standard effort, if applicable
-      step_end[EFFORT_STANDARD] = d_infer_steps.size() - 1;
-    }
-    if (!options::stringEagerLen())
-    {
-      addStrategyStep(CHECK_REGISTER_TERMS_PRE_NF);
-    }
-    addStrategyStep(CHECK_NORMAL_FORMS_EQ);
-    addStrategyStep(CHECK_EXTF_EVAL, 1);
-    if (!options::stringEagerLen() && options::stringLenNorm())
-    {
-      addStrategyStep(CHECK_LENGTH_EQC, 0, false);
-      addStrategyStep(CHECK_REGISTER_TERMS_NF);
-    }
-    addStrategyStep(CHECK_NORMAL_FORMS_DEQ);
-    addStrategyStep(CHECK_CODES);
-    if (options::stringEagerLen() && options::stringLenNorm())
-    {
-      addStrategyStep(CHECK_LENGTH_EQC);
-    }
-    if (options::stringExp() && !options::stringGuessModel())
-    {
-      addStrategyStep(CHECK_EXTF_REDUCTION, 2);
-    }
-    addStrategyStep(CHECK_MEMBERSHIP);
-    addStrategyStep(CHECK_CARDINALITY);
-    step_end[EFFORT_FULL] = d_infer_steps.size() - 1;
-    if (options::stringExp() && options::stringGuessModel())
-    {
-      step_begin[EFFORT_LAST_CALL] = d_infer_steps.size();
-      // these two steps are run in parallel
-      addStrategyStep(CHECK_EXTF_REDUCTION, 2, false);
-      addStrategyStep(CHECK_EXTF_EVAL, 3);
-      step_end[EFFORT_LAST_CALL] = d_infer_steps.size() - 1;
-    }
-    // set the beginning/ending ranges
-    for (const std::pair<const Effort, unsigned>& it_begin : step_begin)
-    {
-      Effort e = it_begin.first;
-      std::map<Effort, unsigned>::iterator it_end = step_end.find(e);
-      Assert(it_end != step_end.end());
-      d_strat_steps[e] =
-          std::pair<unsigned, unsigned>(it_begin.second, it_end->second);
-    }
-  }
-}
+  std::vector<std::pair<InferStep, int> >::iterator it = d_strat.stepBegin(e);
+  std::vector<std::pair<InferStep, int> >::iterator stepEnd =
+      d_strat.stepEnd(e);
 
-void TheoryStrings::runStrategy(unsigned sbegin, unsigned send)
-{
   Trace("strings-process") << "----check, next round---" << std::endl;
-  for (unsigned i = sbegin; i <= send; i++)
+  while (it != stepEnd)
   {
-    InferStep curr = d_infer_steps[i];
+    InferStep curr = it->first;
     if (curr == BREAK)
     {
       if (d_im->hasProcessed())
@@ -1155,12 +1035,13 @@ void TheoryStrings::runStrategy(unsigned sbegin, unsigned send)
     }
     else
     {
-      runInferStep(curr, d_infer_step_effort[i]);
+      runInferStep(curr, it->second);
       if (d_state.isInConflict())
       {
         break;
       }
     }
+    ++it;
   }
   Trace("strings-process") << "----finished round---" << std::endl;
 }
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index 90a97fe3c..368c13a2d 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -35,8 +35,8 @@
 #include "theory/strings/regexp_operation.h"
 #include "theory/strings/regexp_solver.h"
 #include "theory/strings/sequences_stats.h"
-#include "theory/strings/skolem_cache.h"
 #include "theory/strings/solver_state.h"
+#include "theory/strings/strategy.h"
 #include "theory/strings/strings_fmf.h"
 #include "theory/strings/strings_rewriter.h"
 #include "theory/strings/term_registry.h"
@@ -48,91 +48,72 @@ namespace theory {
 namespace strings {
 
 /**
- * Decision procedure for strings.
- *
+ * A theory solver for strings. At a high level, the solver implements
+ * techniques described in:
+ * - Liang et al, CAV 2014,
+ * - Reynolds et al, CAV 2017,
+ * - Reynolds et al, IJCAR 2020.
+ * Its rewriter is described in:
+ * - Reynolds et al, CAV 2019.
  */
-
-/** inference steps
- *
- * Corresponds to a step in the overall strategy of the strings solver. For
- * details on the individual steps, see documentation on the inference schemas
- * within TheoryStrings.
- */
-enum InferStep
-{
-  // indicates that the strategy should break if lemmas or facts are added
-  BREAK,
-  // check initial
-  CHECK_INIT,
-  // check constant equivalence classes
-  CHECK_CONST_EQC,
-  // check extended function evaluation
-  CHECK_EXTF_EVAL,
-  // check cycles
-  CHECK_CYCLES,
-  // check flat forms
-  CHECK_FLAT_FORMS,
-  // check register terms pre-normal forms
-  CHECK_REGISTER_TERMS_PRE_NF,
-  // check normal forms equalities
-  CHECK_NORMAL_FORMS_EQ,
-  // check normal forms disequalities
-  CHECK_NORMAL_FORMS_DEQ,
-  // check codes
-  CHECK_CODES,
-  // check lengths for equivalence classes
-  CHECK_LENGTH_EQC,
-  // check register terms for normal forms
-  CHECK_REGISTER_TERMS_NF,
-  // check extended function reductions
-  CHECK_EXTF_REDUCTION,
-  // check regular expression memberships
-  CHECK_MEMBERSHIP,
-  // check cardinality
-  CHECK_CARDINALITY,
-};
-std::ostream& operator<<(std::ostream& out, Inference i);
-
 class TheoryStrings : public Theory {
   friend class InferenceManager;
-  typedef context::CDList<Node> NodeList;
-  typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
-  typedef context::CDHashMap<Node, int, NodeHashFunction> NodeIntMap;
-  typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap;
   typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
   typedef context::CDHashSet<TypeNode, TypeNodeHashFunction> TypeNodeSet;
-
  public:
   TheoryStrings(context::Context* c, context::UserContext* u,
                 OutputChannel& out, Valuation valuation,
                 const LogicInfo& logicInfo);
   ~TheoryStrings();
-
   /** finish initialization */
   void finishInit() override;
-
-  TheoryRewriter* getTheoryRewriter() override { return &d_rewriter; }
-
+  /** Get the theory rewriter of this class */
+  TheoryRewriter* getTheoryRewriter() override;
+  /** Set the master equality engine */
   void setMasterEqualityEngine(eq::EqualityEngine* eq) override;
-
-  std::string identify() const override { return std::string("TheoryStrings"); }
-
- public:
+  /** Identify this theory */
+  std::string identify() const override;
+  /** Propagate */
   void propagate(Effort e) override;
-  bool propagate(TNode literal);
+  /** Explain */
   Node explain(TNode literal) override;
-  eq::EqualityEngine* getEqualityEngine() override { return &d_equalityEngine; }
+  /** Get the equality engine */
+  eq::EqualityEngine* getEqualityEngine() override;
+  /** Get current substitution */
   bool getCurrentSubstitution(int effort,
                               std::vector<Node>& vars,
                               std::vector<Node>& subs,
                               std::map<Node, std::vector<Node> >& exp) override;
+  /** presolve */
+  void presolve() override;
+  /** shutdown */
+  void shutdown() override {}
+  /** add shared term */
+  void addSharedTerm(TNode n) override;
+  /** get equality status */
+  EqualityStatus getEqualityStatus(TNode a, TNode b) override;
+  /** preregister term */
+  void preRegisterTerm(TNode n) override;
+  /** Expand definition */
+  Node expandDefinition(Node n) override;
+  /** Check at effort e */
+  void check(Effort e) override;
+  /** needs check last effort */
+  bool needsCheckLastEffort() override;
+  /** Conflict when merging two constants */
+  void conflict(TNode a, TNode b);
+  /** called when a new equivalence class is created */
+  void eqNotifyNewClass(TNode t);
+  /** preprocess rewrite */
+  Node ppRewrite(TNode atom) override;
   /**
    * Get all relevant information in this theory regarding the current
    * model. Return false if a contradiction is discovered.
    */
   bool collectModelInfo(TheoryModel* m) override;
 
-  // NotifyClass for equality engine
+ private:
+  /** NotifyClass for equality engine */
   class NotifyClass : public eq::EqualityEngineNotify {
   public:
    NotifyClass(TheoryStrings& ts) : d_str(ts), d_state(ts.d_state) {}
@@ -202,74 +183,8 @@ class TheoryStrings : public Theory {
     /** The solver state of the theory of strings */
     SolverState& d_state;
   };/* class TheoryStrings::NotifyClass */
-
- private:
-  // Constants
-  Node d_emptyString;
-  Node d_true;
-  Node d_false;
-  Node d_zero;
-  Node d_one;
-  Node d_neg_one;
-  /** the cardinality of the alphabet */
-  uint32_t d_cardSize;
-  /** The notify class */
-  NotifyClass d_notify;
-
-  /**
-   * Statistics for the theory of strings/sequences. All statistics for these
-   * theories is collected in this object.
-   */
-  SequencesStatistics d_statistics;
-
-  /** Equaltity engine */
-  eq::EqualityEngine d_equalityEngine;
-  /** The solver state object */
-  SolverState d_state;
-  /** The term registry for this theory */
-  TermRegistry d_termReg;
-  /** The (custom) output channel of the theory of strings */
-  std::unique_ptr<InferenceManager> d_im;
-
- private:
-  std::map< Node, Node > d_eqc_to_len_term;
-
-
-  /////////////////////////////////////////////////////////////////////////////
-  // NOTIFICATIONS
-  /////////////////////////////////////////////////////////////////////////////
- public:
-  void presolve() override;
-  void shutdown() override {}
-
-  /////////////////////////////////////////////////////////////////////////////
-  // MAIN SOLVER
-  /////////////////////////////////////////////////////////////////////////////
- private:
-  void addSharedTerm(TNode n) override;
-  EqualityStatus getEqualityStatus(TNode a, TNode b) override;
-
- private:
-  void addCarePairs(TNodeTrie* t1,
-                    TNodeTrie* t2,
-                    unsigned arity,
-                    unsigned depth);
-
- public:
-  /** preregister term */
-  void preRegisterTerm(TNode n) override;
-  /** Expand definition */
-  Node expandDefinition(Node n) override;
-  /** Check at effort e */
-  void check(Effort e) override;
-  /** needs check last effort */
-  bool needsCheckLastEffort() override;
-  /** Conflict when merging two constants */
-  void conflict(TNode a, TNode b);
-  /** called when a new equivalence class is created */
-  void eqNotifyNewClass(TNode t);
-
- protected:
+  /** propagate method */
+  bool propagate(TNode literal);
   /** compute care graph */
   void computeCareGraph() override;
   /**
@@ -277,7 +192,11 @@ class TheoryStrings : public Theory {
    * the care graph in the above function.
    */
   bool areCareDisequal(TNode x, TNode y);
-
+  /** Add care pairs */
+  void addCarePairs(TNodeTrie* t1,
+                    TNodeTrie* t2,
+                    unsigned arity,
+                    unsigned depth);
   /** Collect model info for type tn
    *
    * Assigns model values (in m) to all relevant terms of the string-like type
@@ -303,38 +222,6 @@ class TheoryStrings : public Theory {
    * of atom, including calls to registerTerm.
    */
   void assertPendingFact(Node atom, bool polarity, Node exp);
-
-  // Symbolic Regular Expression
- private:
-  /** The theory rewriter for this theory. */
-  StringsRewriter d_rewriter;
-  /**
-   * The base solver, responsible for reasoning about congruent terms and
-   * inferring constants for equivalence classes.
-   */
-  std::unique_ptr<BaseSolver> d_bsolver;
-  /**
-   * The core solver, responsible for reasoning about string concatenation
-   * with length constraints.
-   */
-  std::unique_ptr<CoreSolver> d_csolver;
-  /**
-   * Extended function solver, responsible for reductions and simplifications
-   * involving extended string functions.
-   */
-  std::unique_ptr<ExtfSolver> d_esolver;
-  /** regular expression solver module */
-  std::unique_ptr<RegExpSolver> d_rsolver;
-  /** regular expression elimination module */
-  RegExpElimination d_regexp_elim;
-  /** Strings finite model finding decision strategy */
-  StringsFmf d_stringsFmf;
-
- public:
-  // ppRewrite
-  Node ppRewrite(TNode atom) override;
-
- private:
   //-----------------------inference steps
   /** check register terms pre-normal forms
    *
@@ -360,42 +247,58 @@ class TheoryStrings : public Theory {
    */
   void checkRegisterTermsNormalForms();
   //-----------------------end inference steps
-
-  //-----------------------representation of the strategy
-  /** is strategy initialized */
-  bool d_strategy_init;
   /** run the given inference step */
   void runInferStep(InferStep s, int effort);
-  /** the strategy */
-  std::vector<InferStep> d_infer_steps;
-  /** the effort levels */
-  std::vector<int> d_infer_step_effort;
-  /** the range (begin, end) of steps to run at given efforts */
-  std::map<Effort, std::pair<unsigned, unsigned> > d_strat_steps;
-  /** do we have a strategy for effort e? */
-  bool hasStrategyEffort(Effort e) const;
-  /** initialize the strategy
-   *
-   * This adds (s,effort) as a strategy step to the vectors d_infer_steps and
-   * d_infer_step_effort. This indicates that a call to runInferStep should
-   * be run as the next step in the strategy. If addBreak is true, we add
-   * a BREAK to the strategy following this step.
+  /** run strategy for effort e */
+  void runStrategy(Theory::Effort e);
+  /** Commonly used constants */
+  Node d_true;
+  Node d_false;
+  Node d_zero;
+  Node d_one;
+  Node d_neg_one;
+  /** the cardinality of the alphabet */
+  uint32_t d_cardSize;
+  /** The notify class */
+  NotifyClass d_notify;
+  /**
+   * Statistics for the theory of strings/sequences. All statistics for these
+   * theories is collected in this object.
    */
-  void addStrategyStep(InferStep s, int effort = 0, bool addBreak = true);
-  /** initialize the strategy
-   *
-   * This initializes the above information based on the options. This makes
-   * a series of calls to addStrategyStep above.
+  SequencesStatistics d_statistics;
+  /** Equaltity engine */
+  eq::EqualityEngine d_equalityEngine;
+  /** The solver state object */
+  SolverState d_state;
+  /** The term registry for this theory */
+  TermRegistry d_termReg;
+  /** The (custom) output channel of the theory of strings */
+  std::unique_ptr<InferenceManager> d_im;
+  /** The theory rewriter for this theory. */
+  StringsRewriter d_rewriter;
+  /**
+   * The base solver, responsible for reasoning about congruent terms and
+   * inferring constants for equivalence classes.
    */
-  void initializeStrategy();
-  /** run strategy
-   *
-   * This executes the inference steps starting at index sbegin and ending at
-   * index send. We exit if any step in this sequence adds a lemma or infers a
-   * fact.
+  std::unique_ptr<BaseSolver> d_bsolver;
+  /**
+   * The core solver, responsible for reasoning about string concatenation
+   * with length constraints.
    */
-  void runStrategy(unsigned sbegin, unsigned send);
-  //-----------------------end representation of the strategy
+  std::unique_ptr<CoreSolver> d_csolver;
+  /**
+   * Extended function solver, responsible for reductions and simplifications
+   * involving extended string functions.
+   */
+  std::unique_ptr<ExtfSolver> d_esolver;
+  /** regular expression solver module */
+  std::unique_ptr<RegExpSolver> d_rsolver;
+  /** regular expression elimination module */
+  RegExpElimination d_regexp_elim;
+  /** Strings finite model finding decision strategy */
+  StringsFmf d_stringsFmf;
+  /** The representation of the strategy */
+  Strategy d_strat;
 };/* class TheoryStrings */
 
 }/* CVC4::theory::strings namespace */