Enum for all remaining string inferences (#4220)

Merges the Flat Form inferences enum into Inferences. Adds documentation for (most of) these inferences. Removes the old infrastructure for inferences based on a debug string in InferenceManager.

8 files changed, 158 insertions, 143 deletions

diff --git a/src/theory/strings/base_solver.cpp b/src/theory/strings/base_solver.cpp
index 076fc1cc5..1f8d2f49c 100644
--- a/src/theory/strings/base_solver.cpp
+++ b/src/theory/strings/base_solver.cpp
@@ -445,7 +445,7 @@ void BaseSolver::checkCardinality()
         if (!d_state.areDisequal(*itr1, *itr2))
         {
           // add split lemma
-          if (d_im.sendSplit(*itr1, *itr2, "CARD-SP"))
+          if (d_im.sendSplit(*itr1, *itr2, Inference::CARD_SP))
           {
             return;
           }
diff --git a/src/theory/strings/core_solver.cpp b/src/theory/strings/core_solver.cpp
index cc92b0379..89d4a6f0c 100644
--- a/src/theory/strings/core_solver.cpp
+++ b/src/theory/strings/core_solver.cpp
@@ -179,7 +179,7 @@ void CoreSolver::checkFlatForms()
               }
             }
             Node conc = d_false;
-            d_im.sendInference(exp, conc, "F_NCTN");
+            d_im.sendInference(exp, conc, Inference::F_NCTN);
             return;
           }
         }
@@ -218,33 +218,6 @@ void CoreSolver::checkFlatForms()
   }
 }
 
-namespace {
-
-enum class FlatFormInfer
-{
-  NONE,
-  CONST,
-  UNIFY,
-  ENDPOINT_EMP,
-  ENDPOINT_EQ,
-};
-
-std::ostream& operator<<(std::ostream& os, FlatFormInfer inf)
-{
-  switch (inf)
-  {
-    case FlatFormInfer::NONE: os << "<None>"; break;
-    case FlatFormInfer::CONST: os << "F_Const"; break;
-    case FlatFormInfer::UNIFY: os << "F_Unify"; break;
-    case FlatFormInfer::ENDPOINT_EMP: os << "F_EndpointEmp"; break;
-    case FlatFormInfer::ENDPOINT_EQ: os << "F_EndpointEq"; break;
-    default: os << "<Unknown>"; break;
-  }
-  return os;
-}
-
-}  // namespace
-
 void CoreSolver::checkFlatForm(std::vector<Node>& eqc,
                                   size_t start,
                                   bool isRev)
@@ -265,7 +238,7 @@ void CoreSolver::checkFlatForm(std::vector<Node>& eqc,
   {
     std::vector<Node> exp;
     Node conc;
-    FlatFormInfer infType = FlatFormInfer::NONE;
+    Inference infType = Inference::NONE;
     size_t eqc_size = eqc.size();
     size_t asize = d_flat_form[a].size();
     if (count == asize)
@@ -293,7 +266,7 @@ void CoreSolver::checkFlatForm(std::vector<Node>& eqc,
           }
           Assert(!conc_c.empty());
           conc = utils::mkAnd(conc_c);
-          infType = FlatFormInfer::ENDPOINT_EMP;
+          infType = Inference::F_ENDPOINT_EMP;
           Assert(count > 0);
           // swap, will enforce is empty past current
           a = eqc[i];
@@ -333,7 +306,7 @@ void CoreSolver::checkFlatForm(std::vector<Node>& eqc,
           }
           Assert(!conc_c.empty());
           conc = utils::mkAnd(conc_c);
-          infType = FlatFormInfer::ENDPOINT_EMP;
+          infType = Inference::F_ENDPOINT_EMP;
           Assert(count > 0);
           break;
         }
@@ -356,7 +329,7 @@ void CoreSolver::checkFlatForm(std::vector<Node>& eqc,
                 d_bsolver.explainConstantEqc(ac,curr,exp);
                 d_bsolver.explainConstantEqc(bc,cc,exp);
                 conc = d_false;
-                infType = FlatFormInfer::CONST;
+                infType = Inference::F_CONST;
                 break;
               }
             }
@@ -364,7 +337,7 @@ void CoreSolver::checkFlatForm(std::vector<Node>& eqc,
                      && (d_flat_form[b].size() - 1) == count)
             {
               conc = ac.eqNode(bc);
-              infType = FlatFormInfer::ENDPOINT_EQ;
+              infType = Inference::F_ENDPOINT_EQ;
               break;
             }
             else
@@ -397,7 +370,7 @@ void CoreSolver::checkFlatForm(std::vector<Node>& eqc,
                 exp.insert(exp.end(), lexp2.begin(), lexp2.end());
                 d_im.addToExplanation(lcurr, lcc, exp);
                 conc = ac.eqNode(bc);
-                infType = FlatFormInfer::UNIFY;
+                infType = Inference::F_UNIFY;
                 break;
               }
             }
@@ -424,8 +397,8 @@ void CoreSolver::checkFlatForm(std::vector<Node>& eqc,
       {
         Node c = t == 0 ? a : b;
         ssize_t jj;
-        if (infType == FlatFormInfer::ENDPOINT_EQ
-            || (t == 1 && infType == FlatFormInfer::ENDPOINT_EMP))
+        if (infType == Inference::F_ENDPOINT_EQ
+            || (t == 1 && infType == Inference::F_ENDPOINT_EMP))
         {
           // explain all the empty components for F_EndpointEq, all for
           // the short end for F_EndpointEmp
@@ -452,9 +425,7 @@ void CoreSolver::checkFlatForm(std::vector<Node>& eqc,
       // is conflicting by arithmetic len(a.b)=len(a)+len(b)!=len(a)
       // when len(b)!=0. Although if we do not infer this conflict eagerly,
       // it may be applied (see #3272).
-      std::stringstream ss;
-      ss << infType;
-      d_im.sendInference(exp, conc, ss.str().c_str());
+      d_im.sendInference(exp, conc, infType);
       if (d_state.isInConflict())
       {
         return;
@@ -493,7 +464,8 @@ Node CoreSolver::checkCycles( Node eqc, std::vector< Node >& curr, std::vector<
               {
                 std::vector<Node> exps;
                 exps.push_back(n.eqNode(emp));
-                d_im.sendInference(exps, n[i].eqNode(emp), "I_CYCLE_E");
+                d_im.sendInference(
+                    exps, n[i].eqNode(emp), Inference::I_CYCLE_E);
                 return Node::null();
               }
             }else{
@@ -514,7 +486,8 @@ Node CoreSolver::checkCycles( Node eqc, std::vector< Node >& curr, std::vector<
                     //take first non-empty
                     if (j != i && !d_state.areEqual(n[j], emp))
                     {
-                      d_im.sendInference(exp, n[j].eqNode(emp), "I_CYCLE");
+                      d_im.sendInference(
+                          exp, n[j].eqNode(emp), Inference::I_CYCLE);
                       return Node::null();
                     }
                   }
@@ -575,7 +548,7 @@ void CoreSolver::checkNormalFormsEq()
       nf_exp.push_back(utils::mkAnd(nfe.d_exp));
       nf_exp.push_back(eqc_to_exp[itn->second]);
       Node eq = nfe.d_base.eqNode(nfe_eq.d_base);
-      d_im.sendInference(nf_exp, eq, "Normal_Form");
+      d_im.sendInference(nf_exp, eq, Inference::NORMAL_FORM);
       if (d_im.hasProcessed())
       {
         return;
@@ -927,7 +900,7 @@ void CoreSolver::getNormalForms(Node eqc,
           // firstc/lastc, normal_forms_exp_depend.
           exp.insert(exp.end(), nf.d_exp.begin(), nf.d_exp.end());
           Node conc = d_false;
-          d_im.sendInference(exp, conc, "N_NCTN");
+          d_im.sendInference(exp, conc, Inference::N_NCTN);
         }
       }
     }
@@ -1579,7 +1552,7 @@ CoreSolver::ProcessLoopResult CoreSolver::processLoop(NormalForm& nfi,
     {
       Trace("strings-loop") << "Strings::Loop: tails are different."
                             << std::endl;
-      d_im.sendInference(info.d_ant, conc, "Loop Conflict", true);
+      d_im.sendInference(info.d_ant, conc, Inference::FLOOP_CONFLICT, true);
       return ProcessLoopResult::CONFLICT;
     }
   }
@@ -2195,7 +2168,7 @@ void CoreSolver::checkNormalFormsDeq()
       }
       if (!d_state.areEqual(lt[0], lt[1]) && !d_state.areDisequal(lt[0], lt[1]))
       {
-        d_im.sendSplit(lt[0], lt[1], "DEQ-LENGTH-SP");
+        d_im.sendSplit(lt[0], lt[1], Inference::DEQ_LENGTH_SP);
       }
     }
   }
@@ -2295,7 +2268,7 @@ void CoreSolver::checkLengthsEqc() {
       {
         Node eq = llt.eqNode(lcr);
         ei->d_normalizedLength.set(eq);
-        d_im.sendInference(ant, eq, "LEN-NORM", true);
+        d_im.sendInference(ant, eq, Inference::LEN_NORM, true);
       }
     }
   }
diff --git a/src/theory/strings/extf_solver.cpp b/src/theory/strings/extf_solver.cpp
index 0c46881e7..8ce2a3e81 100644
--- a/src/theory/strings/extf_solver.cpp
+++ b/src/theory/strings/extf_solver.cpp
@@ -407,8 +407,9 @@ void ExtfSolver::checkExtfEval(int effort)
           // reduced since this argument may be circular: we may infer than n
           // can be reduced to something else, but that thing may argue that it
           // can be reduced to n, in theory.
-          d_im.sendInternalInference(
-              einfo.d_exp, nrcAssert, effort == 0 ? "EXTF_d" : "EXTF_d-N");
+          Inference infer =
+              effort == 0 ? Inference::EXTF_D : Inference::EXTF_D_N;
+          d_im.sendInternalInference(einfo.d_exp, nrcAssert, infer);
         }
         to_reduce = nrc;
       }
@@ -629,7 +630,7 @@ void ExtfSolver::checkExtfInference(Node n,
     inferEqrr = Rewriter::rewrite(inferEqrr);
     Trace("strings-extf-infer") << "checkExtfInference: " << inferEq
                                 << " ...reduces to " << inferEqrr << std::endl;
-    d_im.sendInternalInference(in.d_exp, inferEqrr, "EXTF_equality_rew");
+    d_im.sendInternalInference(in.d_exp, inferEqrr, Inference::EXTF_EQ_REW);
   }
 }
 
diff --git a/src/theory/strings/infer_info.cpp b/src/theory/strings/infer_info.cpp
index 07c67e167..6881970ef 100644
--- a/src/theory/strings/infer_info.cpp
+++ b/src/theory/strings/infer_info.cpp
@@ -26,7 +26,15 @@ const char* toString(Inference i)
     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::CARD_SP: return "CARD_SP";
     case Inference::CARDINALITY: return "CARDINALITY";
+    case Inference::I_CYCLE_E: return "I_CYCLE_E";
+    case Inference::I_CYCLE: return "I_CYCLE";
+    case Inference::F_CONST: return "F_CONST";
+    case Inference::F_UNIFY: return "F_UNIFY";
+    case Inference::F_ENDPOINT_EMP: return "F_ENDPOINT_EMP";
+    case Inference::F_ENDPOINT_EQ: return "F_ENDPOINT_EQ";
+    case Inference::F_NCTN: return "F_NCTN";
     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";
@@ -39,6 +47,10 @@ 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::FLOOP_CONFLICT: return "FLOOP_CONFLICT";
+    case Inference::NORMAL_FORM: return "NORMAL_FORM";
+    case Inference::N_NCTN: return "N_NCTN";
+    case Inference::LEN_NORM: return "LEN_NORM";
     case Inference::DEQ_DISL_EMP_SPLIT: return "DEQ_DISL_EMP_SPLIT";
     case Inference::DEQ_DISL_FIRST_CHAR_EQ_SPLIT:
       return "DEQ_DISL_FIRST_CHAR_EQ_SPLIT";
@@ -48,6 +60,9 @@ const char* toString(Inference i)
     case Inference::DEQ_DISL_STRINGS_SPLIT: return "DEQ_DISL_STRINGS_SPLIT";
     case Inference::DEQ_LENS_EQ: return "DEQ_LENS_EQ";
     case Inference::DEQ_NORM_EMP: return "DEQ_NORM_EMP";
+    case Inference::DEQ_LENGTH_SP: return "DEQ_LENGTH_SP";
+    case Inference::CODE_PROXY: return "CODE_PROXY";
+    case Inference::CODE_INJ: return "CODE_INJ";
     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";
@@ -59,6 +74,9 @@ const char* toString(Inference i)
     case Inference::RE_DERIVE: return "RE_DERIVE";
     case Inference::EXTF: return "EXTF";
     case Inference::EXTF_N: return "EXTF_N";
+    case Inference::EXTF_D: return "EXTF_D";
+    case Inference::EXTF_D_N: return "EXTF_D_N";
+    case Inference::EXTF_EQ_REW: return "EXTF_EQ_REW";
     case Inference::CTN_TRANS: return "CTN_TRANS";
     case Inference::CTN_DECOMPOSE: return "CTN_DECOMPOSE";
     case Inference::CTN_NEG_EQUAL: return "CTN_NEG_EQUAL";
diff --git a/src/theory/strings/infer_info.h b/src/theory/strings/infer_info.h
index 3ce673967..7fce2eaf2 100644
--- a/src/theory/strings/infer_info.h
+++ b/src/theory/strings/infer_info.h
@@ -59,10 +59,39 @@ enum class Inference : uint32_t
   // equal after e.g. removing strings that are currently empty. For example:
   //   y = "" ^ z = "" => x ++ y = z ++ x
   I_NORM,
+  // A split due to cardinality
+  CARD_SP,
   // The cardinality inference for strings, see Liang et al CAV 2014.
   CARDINALITY,
   //-------------------------------------- end base solver
   //-------------------------------------- core solver
+  // A cycle in the empty string equivalence class, e.g.:
+  //   x ++ y = "" => x = ""
+  // This is typically not applied due to length constraints implying emptiness.
+  I_CYCLE_E,
+  // A cycle in the containment ordering.
+  //   x = y ++ x => y = "" or
+  //   x = y ++ z ^ y = x ++ w => z = "" ^ w = ""
+  // This is typically not applied due to length constraints implying emptiness.
+  I_CYCLE,
+  // Flat form constant
+  //   x = y ^ x = z ++ c ... ^ y = z ++ d => false
+  // where c and d are distinct constants.
+  F_CONST,
+  // Flat form unify
+  //   x = y ^ x = z ++ x' ... ^ y = z ++ y' ^ len(x') = len(y') => x' = y'
+  // Notice flat form instances are similar to normal form inferences but do
+  // not involve recursive explanations.
+  F_UNIFY,
+  // Flat form endpoint empty
+  //   x = y ^ x = z ^ y = z ++ y' => y' = ""
+  F_ENDPOINT_EMP,
+  // Flat form endpoint equal
+  //   x = y ^ x = z ++ x' ^ y = z ++ y' => x' = y'
+  F_ENDPOINT_EQ,
+  // Flat form not contained
+  // x = c ^ x = y => false when rewrite( contains( y, c ) ) = false
+  F_NCTN,
   // 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 = ""
@@ -119,6 +148,18 @@ 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,
+  // loop conflict ???
+  FLOOP_CONFLICT,
+  // Normal form inference
+  // x = y ^ z = y => x = z
+  // This is applied when y is the normal form of both x and z.
+  NORMAL_FORM,
+  // Normal form not contained, same as FFROM_NCTN but for normal forms
+  N_NCTN,
+  // Length normalization
+  //   x = y => len( x ) = len( y )
+  // Typically applied when y is the normal form of x.
+  LEN_NORM,
   // When x ++ x' ++ ... != "abc" ++ y' ++ ... ^ len(x) != len(y), we apply the
   // inference:
   //   x = "" v x != ""
@@ -152,7 +193,18 @@ enum class Inference : uint32_t
   //   ni = px ++ x ++ ... ^ nj = py ^ len(ni) = len(nj) --->
   //     x = "" ^ ...
   DEQ_NORM_EMP,
+  // When two strings are disequal s != t and the comparison of their lengths
+  // is unknown, we apply the inference:
+  //   len(s) != len(t) V len(s) = len(t)
+  DEQ_LENGTH_SP,
   //-------------------------------------- end core solver
+  //-------------------------------------- codes solver
+  // str.to_code( v ) = rewrite( str.to_code(c) )
+  // where v is the proxy variable for c.
+  CODE_PROXY,
+  // str.code(x) = -1 V str.code(x) != str.code(y) V x = y
+  CODE_INJ,
+  //-------------------------------------- end codes solver
   //-------------------------------------- regexp solver
   // regular expression normal form conflict
   //   ( x in R ^ x = y ^ rewrite((str.in_re y R)) = false ) => false
@@ -190,14 +242,30 @@ enum class Inference : uint32_t
   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
+  // Standard 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,
+  // Decompositions based on extended function inferences from context-dependent
+  // rewriting produced by constant substitutions. This is like the above, but
+  // handles cases where the inferred predicate is not necessarily an equality
+  // involving f(X). For example:
+  //   x = "A" ^ contains( y ++ x, "B" ) => contains( y, "B" )
+  // This is generally only inferred if contains( y, "B" ) is a known term in
+  // the current context.
+  EXTF_D,
+  // Same as above, for normal form substitutions.
+  EXTF_D_N,
+  // Extended function equality rewrite. This is an inference of the form:
+  //   t = s => P
+  // where P is a predicate implied by rewrite( t = s ).
+  // Typically, t is an application of an extended function and s is a constant.
+  // It is generally only inferred if P is a predicate over known terms.
+  EXTF_EQ_REW,
   // contain transitive
   //   ( str.contains( s, t ) ^ ~contains( s, r ) ) => ~contains( t, r ).
   CTN_TRANS,
diff --git a/src/theory/strings/inference_manager.cpp b/src/theory/strings/inference_manager.cpp
index 94051a2bb..f262a2c7d 100644
--- a/src/theory/strings/inference_manager.cpp
+++ b/src/theory/strings/inference_manager.cpp
@@ -57,7 +57,7 @@ InferenceManager::InferenceManager(TheoryStrings& p,
 
 bool InferenceManager::sendInternalInference(std::vector<Node>& exp,
                                              Node conc,
-                                             const char* c)
+                                             Inference infer)
 {
   if (conc.getKind() == AND
       || (conc.getKind() == NOT && conc[0].getKind() == OR))
@@ -67,7 +67,7 @@ bool InferenceManager::sendInternalInference(std::vector<Node>& exp,
     bool ret = true;
     for (const Node& cc : conj)
     {
-      bool retc = sendInternalInference(exp, pol ? cc : cc.negate(), c);
+      bool retc = sendInternalInference(exp, pol ? cc : cc.negate(), infer);
       ret = ret && retc;
     }
     return ret;
@@ -110,21 +110,21 @@ bool InferenceManager::sendInternalInference(std::vector<Node>& exp,
     // already holds
     return true;
   }
-  sendInference(exp, conc, c);
+  sendInference(exp, conc, infer);
   return true;
 }
 
 void InferenceManager::sendInference(const std::vector<Node>& exp,
                                      const std::vector<Node>& exp_n,
                                      Node eq,
-                                     const char* c,
+                                     Inference infer,
                                      bool asLemma)
 {
   eq = eq.isNull() ? d_false : Rewriter::rewrite(eq);
   if (Trace.isOn("strings-infer-debug"))
   {
     Trace("strings-infer-debug")
-        << "By " << c << ", infer : " << eq << " from: " << std::endl;
+        << "By " << infer << ", infer : " << eq << " from: " << std::endl;
     for (unsigned i = 0; i < exp.size(); i++)
     {
       Trace("strings-infer-debug") << "  " << exp[i] << std::endl;
@@ -138,6 +138,8 @@ void InferenceManager::sendInference(const std::vector<Node>& exp,
   {
     return;
   }
+  // only keep stats if not trivial conclusion
+  d_statistics.d_inferences << infer;
   Node atom = eq.getKind() == NOT ? eq[0] : eq;
   // check if we should send a lemma or an inference
   if (asLemma || atom == d_false || atom.getKind() == OR || !exp_n.empty()
@@ -172,58 +174,38 @@ void InferenceManager::sendInference(const std::vector<Node>& exp,
       eq = eq_exp.negate();
       eq_exp = d_true;
     }
-    sendLemma(eq_exp, eq, c);
+    sendLemma(eq_exp, eq, infer);
   }
   else
   {
-    sendInfer(utils::mkAnd(exp), eq, c);
+    sendInfer(utils::mkAnd(exp), eq, infer);
   }
 }
 
 void InferenceManager::sendInference(const std::vector<Node>& exp,
                                      Node eq,
-                                     const char* c,
-                                     bool asLemma)
-{
-  std::vector<Node> exp_n;
-  sendInference(exp, exp_n, eq, c, asLemma);
-}
-
-void InferenceManager::sendInference(const std::vector<Node>& exp,
-                                     const std::vector<Node>& exp_n,
-                                     Node eq,
-                                     Inference infer,
-                                     bool asLemma)
-{
-  d_statistics.d_inferences << infer;
-  std::stringstream ss;
-  ss << infer;
-  sendInference(exp, exp_n, eq, ss.str().c_str(), asLemma);
-}
-
-void InferenceManager::sendInference(const std::vector<Node>& exp,
-                                     Node eq,
                                      Inference infer,
                                      bool asLemma)
 {
-  d_statistics.d_inferences << infer;
-  sendInference(exp, eq, toString(infer), asLemma);
+  std::vector<Node> exp_n;
+  sendInference(exp, exp_n, eq, infer, asLemma);
 }
 
 void InferenceManager::sendInference(const InferInfo& i)
 {
   sendInference(i.d_ant, i.d_antn, i.d_conc, i.d_id, true);
 }
-void InferenceManager::sendLemma(Node ant, Node conc, const char* c)
+
+void InferenceManager::sendLemma(Node ant, Node conc, Inference infer)
 {
   if (conc.isNull() || conc == d_false)
   {
     Trace("strings-conflict")
-        << "Strings::Conflict : " << c << " : " << ant << std::endl;
-    Trace("strings-lemma") << "Strings::Conflict : " << c << " : " << ant
+        << "Strings::Conflict : " << infer << " : " << ant << std::endl;
+    Trace("strings-lemma") << "Strings::Conflict : " << infer << " : " << ant
                            << std::endl;
     Trace("strings-assert")
-        << "(assert (not " << ant << ")) ; conflict " << c << std::endl;
+        << "(assert (not " << ant << ")) ; conflict " << infer << std::endl;
     ++(d_statistics.d_conflictsInfer);
     d_out.conflict(ant);
     d_state.setConflict();
@@ -238,13 +220,14 @@ void InferenceManager::sendLemma(Node ant, Node conc, const char* c)
   {
     lem = NodeManager::currentNM()->mkNode(IMPLIES, ant, conc);
   }
-  Trace("strings-lemma") << "Strings::Lemma " << c << " : " << lem << std::endl;
-  Trace("strings-assert") << "(assert " << lem << ") ; lemma " << c
+  Trace("strings-lemma") << "Strings::Lemma " << infer << " : " << lem
+                         << std::endl;
+  Trace("strings-assert") << "(assert " << lem << ") ; lemma " << infer
                           << std::endl;
   d_pendingLem.push_back(lem);
 }
 
-void InferenceManager::sendInfer(Node eq_exp, Node eq, const char* c)
+void InferenceManager::sendInfer(Node eq_exp, Node eq, Inference infer)
 {
   if (options::stringInferSym())
   {
@@ -259,7 +242,7 @@ void InferenceManager::sendInfer(Node eq_exp, Node eq, const char* c)
       if (Trace.isOn("strings-lemma-debug"))
       {
         Trace("strings-lemma-debug") << "Strings::Infer " << eq << " from "
-                                     << eq_exp << " by " << c << std::endl;
+                                     << eq_exp << " by " << infer << std::endl;
         Trace("strings-lemma-debug")
             << "Strings::Infer Alternate : " << eqs << std::endl;
         for (unsigned i = 0, nvars = vars.size(); i < nvars; i++)
@@ -268,7 +251,7 @@ void InferenceManager::sendInfer(Node eq_exp, Node eq, const char* c)
               << "  " << vars[i] << " -> " << subs[i] << std::endl;
         }
       }
-      sendLemma(d_true, eqs, c);
+      sendLemma(d_true, eqs, infer);
       return;
     }
     if (Trace.isOn("strings-lemma-debug"))
@@ -281,16 +264,16 @@ void InferenceManager::sendInfer(Node eq_exp, Node eq, const char* c)
     }
   }
   Trace("strings-lemma") << "Strings::Infer " << eq << " from " << eq_exp
-                         << " by " << c << std::endl;
+                         << " by " << infer << std::endl;
   Trace("strings-assert") << "(assert (=> " << eq_exp << " " << eq
-                          << ")) ; infer " << c << std::endl;
+                          << ")) ; infer " << infer << std::endl;
   d_pending.push_back(eq);
   d_pendingExp[eq] = eq_exp;
   d_keep.insert(eq);
   d_keep.insert(eq_exp);
 }
 
-bool InferenceManager::sendSplit(Node a, Node b, const char* c, bool preq)
+bool InferenceManager::sendSplit(Node a, Node b, Inference infer, bool preq)
 {
   Node eq = a.eqNode(b);
   eq = Rewriter::rewrite(eq);
@@ -298,21 +281,17 @@ bool InferenceManager::sendSplit(Node a, Node b, const char* c, bool preq)
   {
     return false;
   }
+  // update statistics
+  d_statistics.d_inferences << infer;
   NodeManager* nm = NodeManager::currentNM();
   Node lemma_or = nm->mkNode(OR, eq, nm->mkNode(NOT, eq));
-  Trace("strings-lemma") << "Strings::Lemma " << c << " SPLIT : " << lemma_or
-                         << std::endl;
+  Trace("strings-lemma") << "Strings::Lemma " << infer
+                         << " SPLIT : " << lemma_or << std::endl;
   d_pendingLem.push_back(lemma_or);
   sendPhaseRequirement(eq, preq);
   return true;
 }
 
-bool InferenceManager::sendSplit(Node a, Node b, Inference infer, bool preq)
-{
-  d_statistics.d_inferences << infer;
-  return sendSplit(a, b, toString(infer), preq);
-}
-
 void InferenceManager::sendPhaseRequirement(Node lit, bool pol)
 {
   lit = Rewriter::rewrite(lit);
diff --git a/src/theory/strings/inference_manager.h b/src/theory/strings/inference_manager.h
index 2a361aa44..af1f28a23 100644
--- a/src/theory/strings/inference_manager.h
+++ b/src/theory/strings/inference_manager.h
@@ -92,15 +92,17 @@ class InferenceManager
    * sendInference below in that it does not introduce any new non-constant
    * terms to the state.
    *
-   * The argument c is a string identifying the reason for the inference.
-   * This string is used for debugging purposes.
+   * The argument infer identifies the reason for the inference.
+   * This is used for debugging and statistics purposes.
    *
    * Return true if the inference is complete, in the sense that we infer
    * inferences that are equivalent to conc. This returns false e.g. if conc
    * (or one of its conjuncts if it is a conjunction) was not inferred due
    * to the criteria mentioned above.
    */
-  bool sendInternalInference(std::vector<Node>& exp, Node conc, const char* c);
+  bool sendInternalInference(std::vector<Node>& exp,
+                             Node conc,
+                             Inference infer);
   /** send inference
    *
    * This function should be called when ( exp ^ exp_n ) => eq. The set exp
@@ -127,8 +129,9 @@ class InferenceManager
    * exp_n is empty. In particular, lemmas must be used whenever exp_n is
    * non-empty, conflicts are used when exp_n is empty and eq is false.
    *
-   * The argument c is a string identifying the reason for inference, used for
-   * debugging.
+   * The argument infer identifies the reason for inference, used for
+   * debugging. This updates the statistics about the number of inferences made
+   * of each type.
    *
    * If the flag asLemma is true, then this method will send a lemma instead
    * of an inference whenever applicable.
@@ -136,30 +139,9 @@ class InferenceManager
   void sendInference(const std::vector<Node>& exp,
                      const std::vector<Node>& exp_n,
                      Node eq,
-                     const char* c,
-                     bool asLemma = false);
-  /** same as above, but where exp_n is empty */
-  void sendInference(const std::vector<Node>& exp,
-                     Node eq,
-                     const char* c,
-                     bool asLemma = false);
-
-  /**
-   * The same as `sendInference()` above but with an `Inference` instead of a
-   * string. This variant updates the statistics about the number of inferences
-   * made of each type.
-   */
-  void sendInference(const std::vector<Node>& exp,
-                     const std::vector<Node>& exp_n,
-                     Node eq,
                      Inference infer,
                      bool asLemma = false);
-
-  /**
-   * The same as `sendInference()` above but with an `Inference` instead of a
-   * string. This variant updates the statistics about the number of inferences
-   * made of each type.
-   */
+  /** same as above, but where exp_n is empty */
   void sendInference(const std::vector<Node>& exp,
                      Node eq,
                      Inference infer,
@@ -177,19 +159,13 @@ class InferenceManager
    * lemma. We additionally request a phase requirement for the equality a=b
    * with polarity preq.
    *
-   * The argument c is a string identifying the reason for inference, used for
-   * debugging.
+   * The argument infer identifies the reason for inference, used for
+   * debugging. This updates the statistics about the number of
+   * inferences made of each type.
    *
    * This method returns true if the split was non-trivial, and false
    * otherwise. A split is trivial if a=b rewrites to a constant.
    */
-  bool sendSplit(Node a, Node b, const char* c, bool preq = true);
-
-  /**
-   * The same as `sendSplit()` above but with an `Inference` instead of a
-   * string.  This variant updates the statistics about the number of
-   * inferences made of each type.
-   */
   bool sendSplit(Node a, Node b, Inference infer, bool preq = true);
 
   /** Send phase requirement
@@ -339,17 +315,17 @@ class InferenceManager
    * above lemma to the lemma cache d_pending_lem, which may be flushed
    * later within the current call to TheoryStrings::check.
    *
-   * The argument c is a string identifying the reason for inference, used for
+   * The argument infer identifies the reason for inference, used for
    * debugging.
    */
-  void sendLemma(Node ant, Node conc, const char* c);
+  void sendLemma(Node ant, Node conc, Inference infer);
   /**
    * Indicates that conc should be added to the equality engine of this class
    * with explanation eq_exp. It must be the case that eq_exp is a (conjunction
    * of) literals that each are explainable, i.e. they already hold in the
    * equality engine of this class.
    */
-  void sendInfer(Node eq_exp, Node eq, const char* c);
+  void sendInfer(Node eq_exp, Node eq, Inference infer);
   /**
    * Get the lemma required for registering the length information for
    * atomic term n given length status s. For details, see registerTermAtomic.
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 92116582f..da8c3583d 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -1014,7 +1014,7 @@ void TheoryStrings::checkCodes()
         Node vc = nm->mkNode(STRING_TO_CODE, cp);
         if (!d_state.areEqual(cc, vc))
         {
-          d_im.sendInference(d_empty_vec, cc.eqNode(vc), "Code_Proxy");
+          d_im.sendInference(d_empty_vec, cc.eqNode(vc), Inference::CODE_PROXY);
         }
         const_codes.push_back(vc);
       }
@@ -1052,7 +1052,7 @@ void TheoryStrings::checkCodes()
           // str.code(x)==-1 V str.code(x)!=str.code(y) V x==y
           Node inj_lem = nm->mkNode(kind::OR, eq_no, deq, eqn);
           d_im.sendPhaseRequirement(deq, false);
-          d_im.sendInference(d_empty_vec, inj_lem, "Code_Inj");
+          d_im.sendInference(d_empty_vec, inj_lem, Inference::CODE_INJ);
         }
       }
     }