Introduce enums for all string inferences, excluding the core solver (#4195)

Introduce enum values for all calls to sendInference outside of the core solver.

This included some minor refactoring.

11 files changed, 215 insertions, 26 deletions

diff --git a/src/theory/strings/base_solver.cpp b/src/theory/strings/base_solver.cpp
index af0e7cc37..076fc1cc5 100644
--- a/src/theory/strings/base_solver.cpp
+++ b/src/theory/strings/base_solver.cpp
@@ -127,7 +127,7 @@ void BaseSolver::checkInit()
                     }
                   }
                   // infer the equality
-                  d_im.sendInference(exp, n.eqNode(nc), "I_Norm");
+                  d_im.sendInference(exp, n.eqNode(nc), Inference::I_NORM);
                 }
                 else
                 {
@@ -172,7 +172,7 @@ void BaseSolver::checkInit()
                   }
                   AlwaysAssert(foundNEmpty);
                   // infer the equality
-                  d_im.sendInference(exp, n.eqNode(ns), "I_Norm_S");
+                  d_im.sendInference(exp, n.eqNode(ns), Inference::I_NORM_S);
                 }
                 d_congruent.insert(n);
                 congruent[k]++;
@@ -301,7 +301,7 @@ void BaseSolver::checkConstantEquivalenceClasses(TermIndex* ti,
       Assert(countc == vecc.size());
       if (d_state.hasTerm(c))
       {
-        d_im.sendInference(exp, n.eqNode(c), "I_CONST_MERGE");
+        d_im.sendInference(exp, n.eqNode(c), Inference::I_CONST_MERGE);
         return;
       }
       else if (!d_im.hasProcessed())
@@ -333,7 +333,7 @@ void BaseSolver::checkConstantEquivalenceClasses(TermIndex* ti,
             exp.push_back(d_eqcToConstExp[nr]);
             d_im.addToExplanation(n, d_eqcToConstBase[nr], exp);
           }
-          d_im.sendInference(exp, d_false, "I_CONST_CONFLICT");
+          d_im.sendInference(exp, d_false, Inference::I_CONST_CONFLICT);
           return;
         }
         else
@@ -483,7 +483,8 @@ void BaseSolver::checkCardinality()
       if (!cons.isConst() || !cons.getConst<bool>())
       {
         std::vector<Node> emptyVec;
-        d_im.sendInference(emptyVec, vec_node, cons, "CARDINALITY", true);
+        d_im.sendInference(
+            emptyVec, vec_node, cons, Inference::CARDINALITY, true);
         return;
       }
     }
diff --git a/src/theory/strings/extf_solver.cpp b/src/theory/strings/extf_solver.cpp
index 47f36af4c..a1c04848a 100644
--- a/src/theory/strings/extf_solver.cpp
+++ b/src/theory/strings/extf_solver.cpp
@@ -42,6 +42,7 @@ ExtfSolver::ExtfSolver(context::Context* c,
       d_bsolver(bs),
       d_csolver(cs),
       d_extt(et),
+      d_statistics(stats),
       d_preproc(&skc, u, stats),
       d_hasExtf(c, false),
       d_extfInferCache(c)
@@ -113,7 +114,7 @@ bool ExtfSolver::doReduction(int effort, Node n, bool& isCd)
             lexp.push_back(lenx.eqNode(lens));
             lexp.push_back(n.negate());
             Node xneqs = x.eqNode(s).negate();
-            d_im.sendInference(lexp, xneqs, "NEG-CTN-EQL", true);
+            d_im.sendInference(lexp, xneqs, Inference::CTN_NEG_EQUAL, true);
           }
           // this depends on the current assertions, so we set that this
           // inference is context-dependent.
@@ -158,7 +159,7 @@ bool ExtfSolver::doReduction(int effort, Node n, bool& isCd)
     Node eq = Rewriter::rewrite(x.eqNode(utils::mkNConcat(sk1, s, sk2)));
     std::vector<Node> exp_vec;
     exp_vec.push_back(n);
-    d_im.sendInference(d_emptyVec, exp_vec, eq, "POS-CTN", true);
+    d_im.sendInference(d_emptyVec, exp_vec, eq, Inference::CTN_POS, true);
     Trace("strings-extf-debug")
         << "  resolve extf : " << n << " based on positive contain reduction."
         << std::endl;
@@ -184,7 +185,7 @@ bool ExtfSolver::doReduction(int effort, Node n, bool& isCd)
     Trace("strings-red-lemma")
         << "Reduction_" << effort << " lemma : " << nnlem << std::endl;
     Trace("strings-red-lemma") << "...from " << n << std::endl;
-    d_im.sendInference(d_emptyVec, nnlem, "Reduction", true);
+    d_im.sendInference(d_emptyVec, nnlem, Inference::REDUCTION, true);
     Trace("strings-extf-debug")
         << "  resolve extf : " << n << " based on reduction." << std::endl;
     isCd = false;
@@ -363,8 +364,9 @@ void ExtfSolver::checkExtfEval(int effort)
           {
             Trace("strings-extf")
                 << "  resolve extf : " << sn << " -> " << nrc << std::endl;
-            d_im.sendInference(
-                einfo.d_exp, conc, effort == 0 ? "EXTF" : "EXTF-N", true);
+            Inference inf = effort == 0 ? Inference::EXTF : Inference::EXTF_N;
+            d_im.sendInference(einfo.d_exp, conc, inf, true);
+            d_statistics.d_cdSimplifications << n.getKind();
             if (d_state.isInConflict())
             {
               Trace("strings-extf-debug") << "  conflict, return." << std::endl;
@@ -514,7 +516,7 @@ void ExtfSolver::checkExtfInference(Node n,
             if (d_state.areEqual(conc, d_false))
             {
               // we are in conflict
-              d_im.sendInference(in.d_exp, conc, "CTN_Decompose");
+              d_im.sendInference(in.d_exp, conc, Inference::CTN_DECOMPOSE);
             }
             else if (d_extt->hasFunctionKind(conc.getKind()))
             {
@@ -591,7 +593,7 @@ void ExtfSolver::checkExtfInference(Node n,
               exp_c.insert(exp_c.end(),
                            d_extfInfoTmp[ofrom].d_exp.begin(),
                            d_extfInfoTmp[ofrom].d_exp.end());
-              d_im.sendInference(exp_c, conc, "CTN_Trans");
+              d_im.sendInference(exp_c, conc, Inference::CTN_TRANS);
             }
           }
         }
diff --git a/src/theory/strings/extf_solver.h b/src/theory/strings/extf_solver.h
index 040871ffa..9ca72fed2 100644
--- a/src/theory/strings/extf_solver.h
+++ b/src/theory/strings/extf_solver.h
@@ -186,6 +186,8 @@ class ExtfSolver
   CoreSolver& d_csolver;
   /** the extended theory object for the theory of strings */
   ExtTheory* d_extt;
+  /** Reference to the statistics for the theory of strings/sequences. */
+  SequencesStatistics& d_statistics;
   /** preprocessing utility, for performing strings reductions */
   StringsPreprocess d_preproc;
   /** Common constants */
diff --git a/src/theory/strings/infer_info.cpp b/src/theory/strings/infer_info.cpp
index 3b4a6b857..1d0ee30ad 100644
--- a/src/theory/strings/infer_info.cpp
+++ b/src/theory/strings/infer_info.cpp
@@ -22,6 +22,11 @@ const char* toString(Inference i)
 {
   switch (i)
   {
+    case Inference::I_NORM_S: return "I_NORM_S";
+    case Inference::I_CONST_MERGE: return "I_CONST_MERGE";
+    case Inference::I_CONST_CONFLICT: return "I_CONST_CONFLICT";
+    case Inference::I_NORM: return "I_NORM";
+    case Inference::CARDINALITY: return "CARDINALITY";
     case Inference::N_ENDPOINT_EMP: return "N_ENDPOINT_EMP";
     case Inference::N_UNIFY: return "N_UNIFY";
     case Inference::N_ENDPOINT_EQ: return "N_ENDPOINT_EQ";
@@ -34,6 +39,22 @@ const char* toString(Inference i)
     case Inference::SSPLIT_CST: return "SSPLIT_CST";
     case Inference::SSPLIT_VAR: return "SSPLIT_VAR";
     case Inference::FLOOP: return "FLOOP";
+    case Inference::RE_NF_CONFLICT: return "RE_NF_CONFLICT";
+    case Inference::RE_UNFOLD_POS: return "RE_UNFOLD_POS";
+    case Inference::RE_UNFOLD_NEG: return "RE_UNFOLD_NEG";
+    case Inference::RE_INTER_INCLUDE: return "RE_INTER_INCLUDE";
+    case Inference::RE_INTER_CONF: return "RE_INTER_CONF";
+    case Inference::RE_INTER_INFER: return "RE_INTER_INFER";
+    case Inference::RE_DELTA: return "RE_DELTA";
+    case Inference::RE_DELTA_CONF: return "RE_DELTA_CONF";
+    case Inference::RE_DERIVE: return "RE_DERIVE";
+    case Inference::EXTF: return "EXTF";
+    case Inference::EXTF_N: return "EXTF_N";
+    case Inference::CTN_TRANS: return "CTN_TRANS";
+    case Inference::CTN_DECOMPOSE: return "CTN_DECOMPOSE";
+    case Inference::CTN_NEG_EQUAL: return "CTN_NEG_EQUAL";
+    case Inference::CTN_POS: return "CTN_POS";
+    case Inference::REDUCTION: return "REDUCTION";
     default: return "?";
   }
 }
diff --git a/src/theory/strings/infer_info.h b/src/theory/strings/infer_info.h
index e13a5a2ff..252445cb4 100644
--- a/src/theory/strings/infer_info.h
+++ b/src/theory/strings/infer_info.h
@@ -38,6 +38,31 @@ namespace strings {
  */
 enum class Inference : uint32_t
 {
+  //-------------------------------------- base solver
+  // initial normalize singular
+  //   x1 = "" ^ ... ^ x_{i-1} = "" ^ x_{i+1} = "" ^ ... ^ xn = "" =>
+  //   x1 ++ ... ++ xn = xi
+  I_NORM_S,
+  // initial constant merge
+  //   explain_constant(x, c) => x = c
+  // Above, explain_constant(x,c) is a basic explanation of why x must be equal
+  // to string constant c, which is computed by taking arguments of
+  // concatentation terms that are entailed to be constants. For example:
+  //  ( y = "AB" ^ z = "C" ) => y ++ z = "ABC"
+  I_CONST_MERGE,
+  // initial constant conflict
+  //    ( explain_constant(x, c1) ^ explain_constant(x, c2) ^ x = y) => false
+  // where c1 != c2.
+  I_CONST_CONFLICT,
+  // initial normalize
+  // Given two concatenation terms, this is applied when we find that they are
+  // equal after e.g. removing strings that are currently empty. For example:
+  //   y = "" ^ z = "" => x ++ y = z ++ x
+  I_NORM,
+  // The cardinality inference for strings, see Liang et al CAV 2014.
+  CARDINALITY,
+  //-------------------------------------- end base solver
+  //-------------------------------------- core solver
   // Given two normal forms, infers that the remainder one of them has to be
   // empty. For example:
   //    If x1 ++ x2 = y1 and x1 = y1, then x2 = ""
@@ -94,6 +119,73 @@ enum class Inference : uint32_t
   //        for fresh u, u1, u2.
   // This is the rule F-Loop from Figure 5 of Liang et al CAV 2014.
   FLOOP,
+  //-------------------------------------- end core solver
+  //-------------------------------------- regexp solver
+  // regular expression normal form conflict
+  //   ( x in R ^ x = y ^ rewrite((str.in_re y R)) = false ) => false
+  // where y is the normal form computed for x.
+  RE_NF_CONFLICT,
+  // regular expression unfolding
+  // This is a general class of inferences of the form:
+  //   (x in R) => F
+  // where F is formula expressing the next step of checking whether x is in
+  // R.  For example:
+  //   (x in (R)*) =>
+  //   x = "" V x in R V ( x = x1 ++ x2 ++ x3 ^ x1 in R ^ x2 in (R)* ^ x3 in R)
+  RE_UNFOLD_POS,
+  // Same as above, for negative memberships
+  RE_UNFOLD_NEG,
+  // intersection inclusion conflict
+  //   (x in R1 ^ ~ x in R2) => false  where [[includes(R2,R1)]]
+  // Where includes(R2,R1) is a heuristic check for whether R2 includes R1.
+  RE_INTER_INCLUDE,
+  // intersection conflict, using regexp intersection computation
+  //   (x in R1 ^ x in R2) => false   where [[intersect(R1, R2) = empty]]
+  RE_INTER_CONF,
+  // intersection inference
+  //   (x in R1 ^ y in R2 ^ x = y) => (x in re.inter(R1,R2))
+  RE_INTER_INFER,
+  // regular expression delta
+  //   (x = "" ^ x in R) => C
+  // where "" in R holds if and only if C holds.
+  RE_DELTA,
+  // regular expression delta conflict
+  //   (x = "" ^ x in R) => false
+  // where R does not accept the empty string.
+  RE_DELTA_CONF,
+  // regular expression derive ???
+  RE_DERIVE,
+  //-------------------------------------- end regexp solver
+  //-------------------------------------- extended function solver
+  // All extended function inferences from context-dependent rewriting produced
+  // by constant substitutions. See Reynolds et al CAV 2017. These are
+  // inferences of the form:
+  //   X = Y => f(X) = t   when   rewrite( f(Y) ) = t
+  // where X = Y is a vector of equalities, where some of Y may be constants.
+  EXTF,
+  // Same as above, for normal form substitutions.
+  EXTF_N,
+  // contain transitive
+  //   ( str.contains( s, t ) ^ ~contains( s, r ) ) => ~contains( t, r ).
+  CTN_TRANS,
+  // contain decompose
+  //  str.contains( x, str.++( y1, ..., yn ) ) => str.contains( x, yi ) or
+  //  ~str.contains( str.++( x1, ..., xn ), y ) => ~str.contains( xi, y )
+  CTN_DECOMPOSE,
+  // contain neg equal
+  //   ( len( x ) = len( s ) ^ ~contains( x, s ) ) => x != s
+  CTN_NEG_EQUAL,
+  // contain positive
+  //   str.contains( x, y ) => x = w1 ++ y ++ w2
+  // where w1 and w2 are skolem variables.
+  CTN_POS,
+  // All reduction inferences of the form:
+  //   f(x1, .., xn) = y ^ P(x1, ..., xn, y)
+  // where f is an extended function, y is the purification variable for
+  // f(x1, .., xn) and P is the reduction predicate for f
+  // (see theory_strings_preprocess).
+  REDUCTION,
+  //-------------------------------------- end extended function solver
   NONE,
 };
 
diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp
index 6453e1909..d104f3ade 100644
--- a/src/theory/strings/regexp_operation.cpp
+++ b/src/theory/strings/regexp_operation.cpp
@@ -844,8 +844,8 @@ void RegExpOpr::firstChars(Node r, std::set<unsigned> &pcset, SetNodes &pvset)
 void RegExpOpr::simplify(Node t, std::vector< Node > &new_nodes, bool polarity) {
   Trace("strings-regexp-simpl") << "RegExp-Simpl starts with " << t << ", polarity=" << polarity << std::endl;
   Assert(t.getKind() == kind::STRING_IN_REGEXP);
-  Node str = Rewriter::rewrite(t[0]);
-  Node re  = Rewriter::rewrite(t[1]);
+  Node str = t[0];
+  Node re = t[1];
   if(polarity) {
     simplifyPRegExp( str, re, new_nodes );
   } else {
diff --git a/src/theory/strings/regexp_solver.cpp b/src/theory/strings/regexp_solver.cpp
index 30f9c4a73..f6ef92b4d 100644
--- a/src/theory/strings/regexp_solver.cpp
+++ b/src/theory/strings/regexp_solver.cpp
@@ -36,12 +36,14 @@ RegExpSolver::RegExpSolver(TheoryStrings& p,
                            SolverState& s,
                            InferenceManager& im,
                            ExtfSolver& es,
+                           SequencesStatistics& stats,
                            context::Context* c,
                            context::UserContext* u)
     : d_parent(p),
       d_state(s),
       d_im(im),
       d_esolver(es),
+      d_statistics(stats),
       d_regexp_ucached(u),
       d_regexp_ccached(c),
       d_processed_memberships(c)
@@ -160,6 +162,7 @@ void RegExpSolver::check(const std::map<Node, std::vector<Node> >& mems)
             << "We have regular expression assertion : " << assertion
             << std::endl;
         Node atom = assertion.getKind() == NOT ? assertion[0] : assertion;
+        Assert(atom == Rewriter::rewrite(atom));
         bool polarity = assertion.getKind() != NOT;
         if (polarity != (e == 0))
         {
@@ -222,7 +225,7 @@ void RegExpSolver::check(const std::map<Node, std::vector<Node> >& mems)
               std::vector<Node> exp_n;
               exp_n.push_back(assertion);
               Node conc = Node::null();
-              d_im.sendInference(nfexp, exp_n, conc, "REGEXP NF Conflict");
+              d_im.sendInference(nfexp, exp_n, conc, Inference::RE_NF_CONFLICT);
               addedLemma = true;
               break;
             }
@@ -268,7 +271,18 @@ void RegExpSolver::check(const std::map<Node, std::vector<Node> >& mems)
             std::vector<Node> exp_n;
             exp_n.push_back(assertion);
             Node conc = nvec.size() == 1 ? nvec[0] : nm->mkNode(AND, nvec);
-            d_im.sendInference(rnfexp, exp_n, conc, "REGEXP_Unfold");
+            Assert(atom.getKind() == STRING_IN_REGEXP);
+            if (polarity)
+            {
+              d_statistics.d_regexpUnfoldingsPos << atom[1].getKind();
+            }
+            else
+            {
+              d_statistics.d_regexpUnfoldingsNeg << atom[1].getKind();
+            }
+            Inference inf =
+                polarity ? Inference::RE_UNFOLD_POS : Inference::RE_UNFOLD_NEG;
+            d_im.sendInference(rnfexp, exp_n, conc, inf);
             addedLemma = true;
             if (changed)
             {
@@ -387,7 +401,8 @@ bool RegExpSolver::checkEqcInclusion(std::vector<Node>& mems)
           }
 
           Node conc;
-          d_im.sendInference(vec_nodes, conc, "Intersect inclusion", true);
+          d_im.sendInference(
+              vec_nodes, conc, Inference::RE_INTER_INCLUDE, true);
           return false;
         }
       }
@@ -470,7 +485,7 @@ bool RegExpSolver::checkEqcIntersect(const std::vector<Node>& mems)
         vec_nodes.push_back(mi[0].eqNode(m[0]));
       }
       Node conc;
-      d_im.sendInference(vec_nodes, conc, "INTERSECT CONFLICT", true);
+      d_im.sendInference(vec_nodes, conc, Inference::RE_INTER_CONF, true);
       // conflict, return
       return false;
     }
@@ -490,7 +505,7 @@ bool RegExpSolver::checkEqcIntersect(const std::vector<Node>& mems)
     else
     {
       // new conclusion
-      // (x in R ^ y in R2 ^ x = y) => (x in intersect(R1,R2))
+      // (x in R1 ^ y in R2 ^ x = y) => (x in intersect(R1,R2))
       std::vector<Node> vec_nodes;
       vec_nodes.push_back(mi);
       vec_nodes.push_back(m);
@@ -498,7 +513,7 @@ bool RegExpSolver::checkEqcIntersect(const std::vector<Node>& mems)
       {
         vec_nodes.push_back(mi[0].eqNode(m[0]));
       }
-      d_im.sendInference(vec_nodes, mres, "INTERSECT INFER", true);
+      d_im.sendInference(vec_nodes, mres, Inference::RE_INTER_INFER, true);
       // both are reduced
       d_parent.getExtTheory()->markReduced(m);
       d_parent.getExtTheory()->markReduced(mi);
@@ -522,7 +537,7 @@ bool RegExpSolver::checkPDerivative(
         std::vector<Node> exp_n;
         exp_n.push_back(atom);
         exp_n.push_back(x.eqNode(d_emptyString));
-        d_im.sendInference(nf_exp, exp_n, exp, "RegExp Delta");
+        d_im.sendInference(nf_exp, exp_n, exp, Inference::RE_DELTA);
         addedLemma = true;
         d_regexp_ccached.insert(atom);
         return false;
@@ -538,7 +553,7 @@ bool RegExpSolver::checkPDerivative(
         exp_n.push_back(atom);
         exp_n.push_back(x.eqNode(d_emptyString));
         Node conc;
-        d_im.sendInference(nf_exp, exp_n, conc, "RegExp Delta CONFLICT");
+        d_im.sendInference(nf_exp, exp_n, conc, Inference::RE_DELTA_CONF);
         addedLemma = true;
         d_regexp_ccached.insert(atom);
         return false;
@@ -628,7 +643,7 @@ bool RegExpSolver::deriveRegExp(Node x,
     }
     std::vector<Node> exp_n;
     exp_n.push_back(atom);
-    d_im.sendInference(ant, exp_n, conc, "RegExp-Derive");
+    d_im.sendInference(ant, exp_n, conc, Inference::RE_DERIVE);
     return true;
   }
   return false;
diff --git a/src/theory/strings/regexp_solver.h b/src/theory/strings/regexp_solver.h
index d18604752..1d065181b 100644
--- a/src/theory/strings/regexp_solver.h
+++ b/src/theory/strings/regexp_solver.h
@@ -26,6 +26,7 @@
 #include "theory/strings/extf_solver.h"
 #include "theory/strings/inference_manager.h"
 #include "theory/strings/regexp_operation.h"
+#include "theory/strings/sequences_stats.h"
 #include "theory/strings/solver_state.h"
 #include "util/string.h"
 
@@ -49,6 +50,7 @@ class RegExpSolver
                SolverState& s,
                InferenceManager& im,
                ExtfSolver& es,
+               SequencesStatistics& stats,
                context::Context* c,
                context::UserContext* u);
   ~RegExpSolver() {}
@@ -119,6 +121,8 @@ class RegExpSolver
   InferenceManager& d_im;
   /** reference to the extended function solver of the parent */
   ExtfSolver& d_esolver;
+  /** Reference to the statistics for the theory of strings/sequences. */
+  SequencesStatistics& d_statistics;
   // check membership constraints
   Node mkAnd(Node c1, Node c2);
   /**
diff --git a/src/theory/strings/sequences_stats.cpp b/src/theory/strings/sequences_stats.cpp
index fb13cdab2..5cd844290 100644
--- a/src/theory/strings/sequences_stats.cpp
+++ b/src/theory/strings/sequences_stats.cpp
@@ -23,7 +23,10 @@ namespace strings {
 
 SequencesStatistics::SequencesStatistics()
     : d_inferences("theory::strings::inferences"),
+      d_cdSimplifications("theory::strings::cdSimplifications"),
       d_reductions("theory::strings::reductions"),
+      d_regexpUnfoldingsPos("theory::strings::regexpUnfoldingsPos"),
+      d_regexpUnfoldingsNeg("theory::strings::regexpUnfoldingsNeg"),
       d_conflictsEqEngine("theory::strings::conflictsEqEngine", 0),
       d_conflictsEagerPrefix("theory::strings::conflictsEagerPrefix", 0),
       d_conflictsInfer("theory::strings::conflictsInfer", 0),
@@ -35,7 +38,10 @@ SequencesStatistics::SequencesStatistics()
       d_lemmasInfer("theory::strings::lemmasInfer", 0)
 {
   smtStatisticsRegistry()->registerStat(&d_inferences);
+  smtStatisticsRegistry()->registerStat(&d_cdSimplifications);
   smtStatisticsRegistry()->registerStat(&d_reductions);
+  smtStatisticsRegistry()->registerStat(&d_regexpUnfoldingsPos);
+  smtStatisticsRegistry()->registerStat(&d_regexpUnfoldingsNeg);
   smtStatisticsRegistry()->registerStat(&d_conflictsEqEngine);
   smtStatisticsRegistry()->registerStat(&d_conflictsEagerPrefix);
   smtStatisticsRegistry()->registerStat(&d_conflictsInfer);
@@ -49,7 +55,10 @@ SequencesStatistics::SequencesStatistics()
 SequencesStatistics::~SequencesStatistics()
 {
   smtStatisticsRegistry()->unregisterStat(&d_inferences);
+  smtStatisticsRegistry()->unregisterStat(&d_cdSimplifications);
   smtStatisticsRegistry()->unregisterStat(&d_reductions);
+  smtStatisticsRegistry()->unregisterStat(&d_regexpUnfoldingsPos);
+  smtStatisticsRegistry()->unregisterStat(&d_regexpUnfoldingsNeg);
   smtStatisticsRegistry()->unregisterStat(&d_conflictsEqEngine);
   smtStatisticsRegistry()->unregisterStat(&d_conflictsEagerPrefix);
   smtStatisticsRegistry()->unregisterStat(&d_conflictsInfer);
diff --git a/src/theory/strings/sequences_stats.h b/src/theory/strings/sequences_stats.h
index 83a16cb23..65f50dbbc 100644
--- a/src/theory/strings/sequences_stats.h
+++ b/src/theory/strings/sequences_stats.h
@@ -25,16 +25,58 @@ namespace CVC4 {
 namespace theory {
 namespace strings {
 
+/**
+ * Statistics for the theory of strings.
+ *
+ * This is roughly broken up into the following parts:
+ * (1) Inferences,
+ * (2) Conflicts,
+ * (3) Lemmas.
+ *
+ * "Inferences" (1) are steps invoked during solving, which either trigger:
+ * (a) An internal update to the state of the solver (e.g. adding an inferred
+ * equality to the equality engine),
+ * (b) A call to OutputChannel::conflict,
+ * (c) A call to OutputChannel::lemma.
+ * For details, see InferenceManager. We track stats on each kind of
+ * inference that have been indicated by the solvers in TheoryStrings.
+ * Some kinds of inferences are further distinguished by the Kind of the node
+ * they operate on (see d_cdSimplifications, d_reductions, d_regexpUnfoldings).
+ *
+ * "Conflicts" (2) arise from various kinds of reasoning, listed below,
+ * where inferences are one of the possible methods for deriving conflicts.
+ *
+ * "Lemmas" (3) also arise from various kinds of reasoning, listed below,
+ * where inferences are one of the possible methods for deriving lemmas.
+ */
 class SequencesStatistics
 {
  public:
   SequencesStatistics();
   ~SequencesStatistics();
-
+  //--------------- inferences
   /** Counts the number of applications of each type of inference */
   HistogramStat<Inference> d_inferences;
-  /** Counts the number of applications of each type of reduction */
+  /**
+   * Counts the number of applications of each type of context-dependent
+   * simplification. The sum of this map is equal to the number of EXTF or
+   * EXTF_N inferences.
+   */
+  HistogramStat<Kind> d_cdSimplifications;
+  /**
+   * Counts the number of applications of each type of reduction. The sum of
+   * this map is equal to the number of REDUCTION inferences (when
+   * options::stringLazyPreproc is true).
+   */
   HistogramStat<Kind> d_reductions;
+  /**
+   * Counts the number of applications of each type of regular expression
+   * positive (resp. negative) unfoldings. The sum of this map is equal to the
+   * number of RE_UNFOLD_POS (resp. RE_UNFOLD_NEG) inferences.
+   */
+  HistogramStat<Kind> d_regexpUnfoldingsPos;
+  HistogramStat<Kind> d_regexpUnfoldingsNeg;
+  //--------------- end of inferences
   //--------------- conflicts, partition of calls to OutputChannel::conflict
   /** Number of equality engine conflicts */
   IntStat d_conflictsEqEngine;
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index f9eeb2010..d5eb2dbbd 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -95,7 +95,8 @@ TheoryStrings::TheoryStrings(context::Context* c,
                                  d_csolver,
                                  extt,
                                  d_statistics));
-  d_rsolver.reset(new RegExpSolver(*this, d_state, d_im, *d_esolver, c, u));
+  d_rsolver.reset(
+      new RegExpSolver(*this, d_state, d_im, *d_esolver, d_statistics, c, u));
 
   // The kinds we are treating as function application in congruence
   d_equalityEngine.addFunctionKind(kind::STRING_LENGTH);