Merge InferenceIds into one enum (#5892)

This PR is the first step in consolidating the various variants of Inferences, InferenceIds and InferenceManagers of the theories.
It merges all InferencedIds into one global enum and makes all theories use them.

13 files changed, 167 insertions, 555 deletions

diff --git a/src/theory/strings/base_solver.cpp b/src/theory/strings/base_solver.cpp
index 93803ea02..75ca3c77c 100644
--- a/src/theory/strings/base_solver.cpp
+++ b/src/theory/strings/base_solver.cpp
@@ -108,7 +108,7 @@ void BaseSolver::checkInit()
               {
                 // (seq.unit x) = C => false if |C| != 1.
                 d_im.sendInference(
-                    exp, d_false, Inference::UNIT_CONST_CONFLICT);
+                    exp, d_false, InferenceId::STRINGS_UNIT_CONST_CONFLICT);
                 return;
               }
             }
@@ -117,7 +117,7 @@ void BaseSolver::checkInit()
               // (seq.unit x) = (seq.unit y) => x=y, or
               // (seq.unit x) = (seq.unit c) => x=c
               Assert(s.getType() == t.getType());
-              d_im.sendInference(exp, s.eqNode(t), Inference::UNIT_INJ);
+              d_im.sendInference(exp, s.eqNode(t), InferenceId::STRINGS_UNIT_INJ);
             }
           }
           // update best content
@@ -187,7 +187,7 @@ void BaseSolver::checkInit()
                     }
                   }
                   // infer the equality
-                  d_im.sendInference(exp, n.eqNode(nc), Inference::I_NORM);
+                  d_im.sendInference(exp, n.eqNode(nc), InferenceId::STRINGS_I_NORM);
                 }
                 else
                 {
@@ -237,7 +237,7 @@ void BaseSolver::checkInit()
                   }
                   AlwaysAssert(foundNEmpty);
                   // infer the equality
-                  d_im.sendInference(exp, n.eqNode(ns), Inference::I_NORM_S);
+                  d_im.sendInference(exp, n.eqNode(ns), InferenceId::STRINGS_I_NORM_S);
                 }
                 d_congruent.insert(n);
                 congruentCount[k].first++;
@@ -440,7 +440,7 @@ void BaseSolver::checkConstantEquivalenceClasses(TermIndex* ti,
       }
       else if (d_state.hasTerm(c))
       {
-        d_im.sendInference(exp, n.eqNode(c), Inference::I_CONST_MERGE);
+        d_im.sendInference(exp, n.eqNode(c), InferenceId::STRINGS_I_CONST_MERGE);
         return;
       }
       else if (!d_im.hasProcessed())
@@ -473,7 +473,7 @@ void BaseSolver::checkConstantEquivalenceClasses(TermIndex* ti,
             exp.push_back(bei.d_exp);
             d_im.addToExplanation(n, bei.d_base, exp);
           }
-          d_im.sendInference(exp, d_false, Inference::I_CONST_CONFLICT);
+          d_im.sendInference(exp, d_false, InferenceId::STRINGS_I_CONST_CONFLICT);
           return;
         }
         else
@@ -622,7 +622,7 @@ void BaseSolver::checkCardinalityType(TypeNode tn,
         if (!d_state.areDisequal(*itr1, *itr2))
         {
           // add split lemma
-          if (d_im.sendSplit(*itr1, *itr2, Inference::CARD_SP))
+          if (d_im.sendSplit(*itr1, *itr2, InferenceId::STRINGS_CARD_SP))
           {
             return;
           }
@@ -660,7 +660,7 @@ void BaseSolver::checkCardinalityType(TypeNode tn,
       if (!cons.isConst() || !cons.getConst<bool>())
       {
         d_im.sendInference(
-            expn, expn, cons, Inference::CARDINALITY, false, true);
+            expn, expn, cons, InferenceId::STRINGS_CARDINALITY, false, true);
         return;
       }
     }
diff --git a/src/theory/strings/core_solver.cpp b/src/theory/strings/core_solver.cpp
index e95e79d68..343332da5 100644
--- a/src/theory/strings/core_solver.cpp
+++ b/src/theory/strings/core_solver.cpp
@@ -186,7 +186,7 @@ void CoreSolver::checkFlatForms()
             }
             d_bsolver.explainConstantEqc(n, eqc, exp);
             Node conc = d_false;
-            d_im.sendInference(exp, conc, Inference::F_NCTN);
+            d_im.sendInference(exp, conc, InferenceId::STRINGS_F_NCTN);
             return;
           }
         }
@@ -247,7 +247,7 @@ void CoreSolver::checkFlatForm(std::vector<Node>& eqc,
   {
     std::vector<Node> exp;
     Node conc;
-    Inference infType = Inference::NONE;
+    InferenceId infType = InferenceId::UNKNOWN;
     size_t eqc_size = eqc.size();
     size_t asize = d_flat_form[a].size();
     if (count == asize)
@@ -275,7 +275,7 @@ void CoreSolver::checkFlatForm(std::vector<Node>& eqc,
           }
           Assert(!conc_c.empty());
           conc = utils::mkAnd(conc_c);
-          infType = Inference::F_ENDPOINT_EMP;
+          infType = InferenceId::STRINGS_F_ENDPOINT_EMP;
           Assert(count > 0);
           // swap, will enforce is empty past current
           a = eqc[i];
@@ -315,7 +315,7 @@ void CoreSolver::checkFlatForm(std::vector<Node>& eqc,
           }
           Assert(!conc_c.empty());
           conc = utils::mkAnd(conc_c);
-          infType = Inference::F_ENDPOINT_EMP;
+          infType = InferenceId::STRINGS_F_ENDPOINT_EMP;
           Assert(count > 0);
           break;
         }
@@ -338,7 +338,7 @@ void CoreSolver::checkFlatForm(std::vector<Node>& eqc,
                 d_bsolver.explainConstantEqc(ac,curr,exp);
                 d_bsolver.explainConstantEqc(bc,cc,exp);
                 conc = d_false;
-                infType = Inference::F_CONST;
+                infType = InferenceId::STRINGS_F_CONST;
                 break;
               }
             }
@@ -346,7 +346,7 @@ void CoreSolver::checkFlatForm(std::vector<Node>& eqc,
                      && (d_flat_form[b].size() - 1) == count)
             {
               conc = ac.eqNode(bc);
-              infType = Inference::F_ENDPOINT_EQ;
+              infType = InferenceId::STRINGS_F_ENDPOINT_EQ;
               break;
             }
             else
@@ -380,7 +380,7 @@ void CoreSolver::checkFlatForm(std::vector<Node>& eqc,
                 d_im.addToExplanation(lcurr, lcc, lexpc);
                 lant = utils::mkAnd(lexpc);
                 conc = ac.eqNode(bc);
-                infType = Inference::F_UNIFY;
+                infType = InferenceId::STRINGS_F_UNIFY;
                 break;
               }
             }
@@ -406,8 +406,8 @@ void CoreSolver::checkFlatForm(std::vector<Node>& eqc,
       {
         Node c = t == 0 ? a : b;
         ssize_t jj;
-        if (infType == Inference::F_ENDPOINT_EQ
-            || (t == 1 && infType == Inference::F_ENDPOINT_EMP))
+        if (infType == InferenceId::STRINGS_F_ENDPOINT_EQ
+            || (t == 1 && infType == InferenceId::STRINGS_F_ENDPOINT_EMP))
         {
           // explain all the empty components for F_EndpointEq, all for
           // the short end for F_EndpointEmp
@@ -480,7 +480,7 @@ 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), Inference::I_CYCLE_E);
+                    exps, n[i].eqNode(emp), InferenceId::STRINGS_I_CYCLE_E);
                 return Node::null();
               }
             }else{
@@ -502,7 +502,7 @@ Node CoreSolver::checkCycles( Node eqc, std::vector< Node >& curr, std::vector<
                     if (j != i && !d_state.areEqual(n[j], emp))
                     {
                       d_im.sendInference(
-                          exp, n[j].eqNode(emp), Inference::I_CYCLE);
+                          exp, n[j].eqNode(emp), InferenceId::STRINGS_I_CYCLE);
                       return Node::null();
                     }
                   }
@@ -567,7 +567,7 @@ void CoreSolver::checkNormalFormsEq()
         nf_exp.push_back(eexp);
       }
       Node eq = nfe.d_base.eqNode(nfe_eq.d_base);
-      d_im.sendInference(nf_exp, eq, Inference::NORMAL_FORM);
+      d_im.sendInference(nf_exp, eq, InferenceId::STRINGS_NORMAL_FORM);
       if (d_im.hasProcessed())
       {
         return;
@@ -1105,7 +1105,7 @@ void CoreSolver::processNEqc(Node eqc,
           // Notice although not implemented, this can be minimized based on
           // firstc/lastc, normal_forms_exp_depend.
           d_bsolver.explainConstantEqc(n, eqc, exp);
-          d_im.sendInference(exp, d_false, Inference::N_NCTN);
+          d_im.sendInference(exp, d_false, InferenceId::STRINGS_N_NCTN);
           // conflict, finished
           return;
         }
@@ -1196,7 +1196,7 @@ void CoreSolver::processNEqc(Node eqc,
         exp.insert(exp.end(), nfi.d_exp.begin(), nfi.d_exp.end());
         exp.insert(exp.end(), nfj.d_exp.begin(), nfj.d_exp.end());
         exp.push_back(nfi.d_base.eqNode(nfj.d_base));
-        d_im.sendInference(exp, d_false, Inference::N_EQ_CONF);
+        d_im.sendInference(exp, d_false, InferenceId::STRINGS_N_EQ_CONF);
         return;
       }
     }
@@ -1215,7 +1215,7 @@ void CoreSolver::processNEqc(Node eqc,
   bool set_use_index = false;
   Trace("strings-solve") << "Possible inferences (" << pinfer.size()
                          << ") : " << std::endl;
-  Inference min_id = Inference::NONE;
+  InferenceId min_id = InferenceId::UNKNOWN;
   unsigned max_index = 0;
   for (unsigned i = 0, psize = pinfer.size(); i < psize; i++)
   {
@@ -1277,7 +1277,7 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi,
         // can infer that this string must be empty
         Node eq = nfkv[index_k].eqNode(emp);
         Assert(!d_state.areEqual(emp, nfkv[index_k]));
-        d_im.sendInference(curr_exp, eq, Inference::N_ENDPOINT_EMP, isRev);
+        d_im.sendInference(curr_exp, eq, InferenceId::STRINGS_N_ENDPOINT_EMP, isRev);
         index_k++;
       }
       break;
@@ -1320,7 +1320,7 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi,
       if (x.isConst() && y.isConst())
       {
         // if both are constant, it's just a constant conflict
-        d_im.sendInference(ant, d_false, Inference::N_CONST, isRev, true);
+        d_im.sendInference(ant, d_false, InferenceId::STRINGS_N_CONST, isRev, true);
         return;
       }
       // `x` and `y` have the same length. We infer that the two components
@@ -1335,7 +1335,7 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi,
       // set the explanation for length
       Node lant = utils::mkAnd(lenExp);
       ant.push_back(lant);
-      d_im.sendInference(ant, eq, Inference::N_UNIFY, isRev);
+      d_im.sendInference(ant, eq, InferenceId::STRINGS_N_UNIFY, isRev);
       break;
     }
     else if ((!x.isConst() && index == nfiv.size() - rproc - 1)
@@ -1375,7 +1375,7 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi,
         NormalForm::getExplanationForPrefixEq(nfi, nfj, -1, -1, antec);
         d_im.sendInference(antec,
                            eqn[0].eqNode(eqn[1]),
-                           Inference::N_ENDPOINT_EQ,
+                           InferenceId::STRINGS_N_ENDPOINT_EQ,
                            isRev,
                            true);
       }
@@ -1437,7 +1437,7 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi,
         // E.g. "abc" ++ ... = "bc" ++ ... ---> conflict
         std::vector<Node> antec;
         NormalForm::getExplanationForPrefixEq(nfi, nfj, index, index, antec);
-        d_im.sendInference(antec, d_false, Inference::N_CONST, isRev, true);
+        d_im.sendInference(antec, d_false, InferenceId::STRINGS_N_CONST, isRev, true);
         break;
       }
     }
@@ -1466,7 +1466,7 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi,
       Node lenEq = nm->mkNode(EQUAL, xLenTerm, yLenTerm);
       lenEq = Rewriter::rewrite(lenEq);
       iinfo.d_conc = nm->mkNode(OR, lenEq, lenEq.negate());
-      iinfo.d_id = Inference::LEN_SPLIT;
+      iinfo.d_id = InferenceId::STRINGS_LEN_SPLIT;
       info.d_pendingPhase[lenEq] = true;
       pinfer.push_back(info);
       break;
@@ -1546,12 +1546,12 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi,
           // inferred
           iinfo.d_conc = nm->mkNode(
               AND, p.eqNode(nc), !eq.getConst<bool>() ? pEq.negate() : pEq);
-          iinfo.d_id = Inference::INFER_EMP;
+          iinfo.d_id = InferenceId::STRINGS_INFER_EMP;
         }
         else
         {
           iinfo.d_conc = nm->mkNode(OR, eq, eq.negate());
-          iinfo.d_id = Inference::LEN_SPLIT_EMP;
+          iinfo.d_id = InferenceId::STRINGS_LEN_SPLIT_EMP;
         }
         pinfer.push_back(info);
         break;
@@ -1594,7 +1594,7 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi,
               xcv, stra, PfRule::CONCAT_CPROP, isRev, skc, newSkolems);
           Assert(newSkolems.size() == 1);
           iinfo.d_skolems[LENGTH_SPLIT].push_back(newSkolems[0]);
-          iinfo.d_id = Inference::SSPLIT_CST_PROP;
+          iinfo.d_id = InferenceId::STRINGS_SSPLIT_CST_PROP;
           iinfo.d_idRev = isRev;
           pinfer.push_back(info);
           break;
@@ -1614,7 +1614,7 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi,
       iinfo.d_premises.push_back(expNonEmpty);
       Assert(newSkolems.size() == 1);
       iinfo.d_skolems[LENGTH_SPLIT].push_back(newSkolems[0]);
-      iinfo.d_id = Inference::SSPLIT_CST;
+      iinfo.d_id = InferenceId::STRINGS_SSPLIT_CST;
       iinfo.d_idRev = isRev;
       pinfer.push_back(info);
       break;
@@ -1703,7 +1703,7 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi,
     // make the conclusion
     if (lentTestSuccess == -1)
     {
-      iinfo.d_id = Inference::SSPLIT_VAR;
+      iinfo.d_id = InferenceId::STRINGS_SSPLIT_VAR;
       iinfo.d_conc =
           getConclusion(x, y, PfRule::CONCAT_SPLIT, isRev, skc, newSkolems);
       if (options::stringUnifiedVSpt() && !options::stringLenConc())
@@ -1714,14 +1714,14 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi,
     }
     else if (lentTestSuccess == 0)
     {
-      iinfo.d_id = Inference::SSPLIT_VAR_PROP;
+      iinfo.d_id = InferenceId::STRINGS_SSPLIT_VAR_PROP;
       iinfo.d_conc =
           getConclusion(x, y, PfRule::CONCAT_LPROP, isRev, skc, newSkolems);
     }
     else
     {
       Assert(lentTestSuccess == 1);
-      iinfo.d_id = Inference::SSPLIT_VAR_PROP;
+      iinfo.d_id = InferenceId::STRINGS_SSPLIT_VAR_PROP;
       iinfo.d_conc =
           getConclusion(y, x, PfRule::CONCAT_LPROP, isRev, skc, newSkolems);
     }
@@ -1835,7 +1835,7 @@ CoreSolver::ProcessLoopResult CoreSolver::processLoop(NormalForm& nfi,
       Trace("strings-loop") << "Strings::Loop: tails are different."
                             << std::endl;
       d_im.sendInference(
-          iinfo.d_premises, conc, Inference::FLOOP_CONFLICT, false, true);
+          iinfo.d_premises, conc, InferenceId::STRINGS_FLOOP_CONFLICT, false, true);
       return ProcessLoopResult::CONFLICT;
     }
   }
@@ -1856,7 +1856,7 @@ CoreSolver::ProcessLoopResult CoreSolver::processLoop(NormalForm& nfi,
         iinfo.d_premises.clear();
         // try to make t equal to empty to avoid loop
         iinfo.d_conc = nm->mkNode(kind::OR, split_eq, split_eq.negate());
-        iinfo.d_id = Inference::LEN_SPLIT_EMP;
+        iinfo.d_id = InferenceId::STRINGS_LEN_SPLIT_EMP;
         return ProcessLoopResult::INFERENCE;
       }
       else
@@ -1973,7 +1973,7 @@ CoreSolver::ProcessLoopResult CoreSolver::processLoop(NormalForm& nfi,
 
   // we will be done
   iinfo.d_conc = conc;
-  iinfo.d_id = Inference::FLOOP;
+  iinfo.d_id = InferenceId::STRINGS_FLOOP;
   info.d_nfPair[0] = nfi.d_base;
   info.d_nfPair[1] = nfj.d_base;
   return ProcessLoopResult::INFERENCE;
@@ -2042,7 +2042,7 @@ void CoreSolver::processDeq(Node ni, Node nj)
       std::vector<Node> premises;
       premises.push_back(deq);
       Node conc = u[0].eqNode(vc).notNode();
-      d_im.sendInference(premises, conc, Inference::UNIT_INJ_DEQ, false, true);
+      d_im.sendInference(premises, conc, InferenceId::STRINGS_UNIT_INJ_DEQ, false, true);
       return;
     }
     Trace("strings-solve-debug") << "...trivial" << std::endl;
@@ -2135,7 +2135,7 @@ void CoreSolver::processDeq(Node ni, Node nj)
           // E.g. x ++ x' ++ ... != "abc" ++ y' ++ ... ^ len(x) != len(y) --->
           //      x = "" v x != ""
           Node emp = Word::mkEmptyWord(nck.getType());
-          d_im.sendSplit(nck, emp, Inference::DEQ_DISL_EMP_SPLIT);
+          d_im.sendSplit(nck, emp, InferenceId::STRINGS_DEQ_DISL_EMP_SPLIT);
           return;
         }
 
@@ -2163,7 +2163,7 @@ void CoreSolver::processDeq(Node ni, Node nj)
             //      x = "a" v x != "a"
             if (d_im.sendSplit(firstChar,
                                nck,
-                               Inference::DEQ_DISL_FIRST_CHAR_EQ_SPLIT,
+                               InferenceId::STRINGS_DEQ_DISL_FIRST_CHAR_EQ_SPLIT,
                                false))
             {
               return;
@@ -2195,7 +2195,7 @@ void CoreSolver::processDeq(Node ni, Node nj)
           d_im.sendInference(antecLen,
                              antecLen,
                              conc,
-                             Inference::DEQ_DISL_FIRST_CHAR_STRING_SPLIT,
+                             InferenceId::STRINGS_DEQ_DISL_FIRST_CHAR_STRING_SPLIT,
                              false,
                              true);
           return;
@@ -2240,7 +2240,7 @@ void CoreSolver::processDeq(Node ni, Node nj)
           d_im.sendInference(antecLen,
                              antecLen,
                              conc,
-                             Inference::DEQ_DISL_STRINGS_SPLIT,
+                             InferenceId::STRINGS_DEQ_DISL_STRINGS_SPLIT,
                              false,
                              true);
         }
@@ -2256,7 +2256,7 @@ void CoreSolver::processDeq(Node ni, Node nj)
       // E.g. x ++ x' ++ ... != y ++ y' ++ ... ^ len(x) = len(y) --->
       //      x = y v x != y
       Assert(!d_state.areDisequal(x, y));
-      if (d_im.sendSplit(x, y, Inference::DEQ_STRINGS_EQ, false))
+      if (d_im.sendSplit(x, y, InferenceId::STRINGS_DEQ_STRINGS_EQ, false))
       {
         return;
       }
@@ -2268,7 +2268,7 @@ void CoreSolver::processDeq(Node ni, Node nj)
       //
       // E.g. x ++ x' ++ ... != y ++ y' ++ ... --->
       //      len(x) = len(y) v len(x) != len(y)
-      if (d_im.sendSplit(xLenTerm, yLenTerm, Inference::DEQ_LENS_EQ))
+      if (d_im.sendSplit(xLenTerm, yLenTerm, InferenceId::STRINGS_DEQ_LENS_EQ))
       {
         return;
       }
@@ -2343,7 +2343,7 @@ bool CoreSolver::processSimpleDeq(std::vector<Node>& nfi,
       Node conc = cc.size() == 1
                       ? cc[0]
                       : NodeManager::currentNM()->mkNode(kind::AND, cc);
-      d_im.sendInference(ant, antn, conc, Inference::DEQ_NORM_EMP, isRev, true);
+      d_im.sendInference(ant, antn, conc, InferenceId::STRINGS_DEQ_NORM_EMP, isRev, true);
       return true;
     }
 
@@ -2519,7 +2519,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], Inference::DEQ_LENGTH_SP);
+        d_im.sendSplit(lt[0], lt[1], InferenceId::STRINGS_DEQ_LENGTH_SP);
       }
     }
   }
@@ -2627,7 +2627,7 @@ void CoreSolver::checkLengthsEqc() {
       {
         Node eq = llt.eqNode(lc);
         ei->d_normalizedLength.set(eq);
-        d_im.sendInference(ant, eq, Inference::LEN_NORM, false, true);
+        d_im.sendInference(ant, eq, InferenceId::STRINGS_LEN_NORM, false, true);
       }
     }
   }
diff --git a/src/theory/strings/extf_solver.cpp b/src/theory/strings/extf_solver.cpp
index 8db53c53e..c4e06e39c 100644
--- a/src/theory/strings/extf_solver.cpp
+++ b/src/theory/strings/extf_solver.cpp
@@ -128,7 +128,7 @@ bool ExtfSolver::doReduction(int effort, Node n)
             lexp.push_back(n.negate());
             Node xneqs = x.eqNode(s).negate();
             d_im.sendInference(
-                lexp, xneqs, Inference::CTN_NEG_EQUAL, false, true);
+                lexp, xneqs, InferenceId::STRINGS_CTN_NEG_EQUAL, false, true);
           }
           // this depends on the current assertions, so this
           // inference is context-dependent
@@ -177,7 +177,7 @@ bool ExtfSolver::doReduction(int effort, Node n)
     eq = eq[1];
     std::vector<Node> expn;
     expn.push_back(n);
-    d_im.sendInference(expn, expn, eq, Inference::CTN_POS, false, true);
+    d_im.sendInference(expn, expn, eq, InferenceId::STRINGS_CTN_POS, false, true);
     Trace("strings-extf-debug")
         << "  resolve extf : " << n << " based on positive contain reduction."
         << std::endl;
@@ -206,7 +206,7 @@ bool ExtfSolver::doReduction(int effort, Node n)
     Trace("strings-red-lemma") << "...from " << n << std::endl;
     Trace("strings-red-lemma")
         << "Reduction_" << effort << " rewritten : " << Rewriter::rewrite(nnlem) << std::endl;
-    d_im.sendInference(d_emptyVec, nnlem, Inference::REDUCTION, false, true);
+    d_im.sendInference(d_emptyVec, nnlem, InferenceId::STRINGS_REDUCTION, false, true);
     Trace("strings-extf-debug")
         << "  resolve extf : " << n << " based on reduction." << std::endl;
     // add as reduction lemma
@@ -387,7 +387,7 @@ void ExtfSolver::checkExtfEval(int effort)
           {
             Trace("strings-extf")
                 << "  resolve extf : " << sn << " -> " << nrc << std::endl;
-            Inference inf = effort == 0 ? Inference::EXTF : Inference::EXTF_N;
+            InferenceId inf = effort == 0 ? InferenceId::STRINGS_EXTF : InferenceId::STRINGS_EXTF_N;
             d_im.sendInference(einfo.d_exp, conc, inf, false, true);
             d_statistics.d_cdSimplifications << n.getKind();
           }
@@ -424,8 +424,8 @@ 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.
-          Inference infer =
-              effort == 0 ? Inference::EXTF_D : Inference::EXTF_D_N;
+          InferenceId infer =
+              effort == 0 ? InferenceId::STRINGS_EXTF_D : InferenceId::STRINGS_EXTF_D_N;
           d_im.sendInternalInference(einfo.d_exp, nrcAssert, infer);
         }
         to_reduce = nrc;
@@ -545,7 +545,7 @@ void ExtfSolver::checkExtfInference(Node n,
             if (d_state.areEqual(conc, d_false))
             {
               // we are in conflict
-              d_im.sendInference(in.d_exp, conc, Inference::CTN_DECOMPOSE);
+              d_im.sendInference(in.d_exp, conc, InferenceId::STRINGS_CTN_DECOMPOSE);
             }
             else if (d_extt.hasFunctionKind(conc.getKind()))
             {
@@ -622,7 +622,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, Inference::CTN_TRANS);
+              d_im.sendInference(exp_c, conc, InferenceId::STRINGS_CTN_TRANS);
             }
           }
         }
@@ -656,7 +656,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, Inference::EXTF_EQ_REW);
+    d_im.sendInternalInference(in.d_exp, inferEqrr, InferenceId::STRINGS_EXTF_EQ_REW);
   }
 }
 
diff --git a/src/theory/strings/infer_info.cpp b/src/theory/strings/infer_info.cpp
index 4cb072efb..c543de0e0 100644
--- a/src/theory/strings/infer_info.cpp
+++ b/src/theory/strings/infer_info.cpp
@@ -21,86 +21,7 @@ namespace CVC4 {
 namespace theory {
 namespace strings {
 
-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::UNIT_INJ: return "UNIT_INJ";
-    case Inference::UNIT_CONST_CONFLICT: return "UNIT_CONST_CONFLICT";
-    case Inference::UNIT_INJ_DEQ: return "UNIT_INJ_DEQ";
-    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_EQ_CONF: return "N_EQ_CONF";
-    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";
-    case Inference::N_CONST: return "N_CONST";
-    case Inference::INFER_EMP: return "INFER_EMP";
-    case Inference::SSPLIT_CST_PROP: return "SSPLIT_CST_PROP";
-    case Inference::SSPLIT_VAR_PROP: return "SSPLIT_VAR_PROP";
-    case Inference::LEN_SPLIT: return "LEN_SPLIT";
-    case Inference::LEN_SPLIT_EMP: return "LEN_SPLIT_EMP";
-    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";
-    case Inference::DEQ_DISL_FIRST_CHAR_STRING_SPLIT:
-      return "DEQ_DISL_FIRST_CHAR_STRING_SPLIT";
-    case Inference::DEQ_STRINGS_EQ: return "DEQ_STRINGS_EQ";
-    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";
-    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::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";
-    case Inference::CTN_POS: return "CTN_POS";
-    case Inference::REDUCTION: return "REDUCTION";
-    case Inference::PREFIX_CONFLICT: return "PREFIX_CONFLICT";
-    default: return "?";
-  }
-}
-
-std::ostream& operator<<(std::ostream& out, Inference i)
-{
-  out << toString(i);
-  return out;
-}
-
-InferInfo::InferInfo() : d_sim(nullptr), d_id(Inference::NONE), d_idRev(false)
+InferInfo::InferInfo() : d_sim(nullptr), d_id(InferenceId::UNKNOWN), d_idRev(false)
 {
 }
 
diff --git a/src/theory/strings/infer_info.h b/src/theory/strings/infer_info.h
index a6c4776eb..c0667e53c 100644
--- a/src/theory/strings/infer_info.h
+++ b/src/theory/strings/infer_info.h
@@ -21,6 +21,7 @@
 #include <vector>
 
 #include "expr/node.h"
+#include "theory/inference_id.h"
 #include "theory/theory_inference.h"
 #include "util/safe_print.h"
 
@@ -28,316 +29,6 @@ namespace CVC4 {
 namespace theory {
 namespace strings {
 
-/** Types of inferences used in the procedure
- *
- * These are variants of the inference rules in Figures 3-5 of Liang et al.
- * "A DPLL(T) Solver for a Theory of Strings and Regular Expressions", CAV 2014.
- *
- * Note: The order in this enum matters in certain cases (e.g. inferences
- * related to normal forms), inferences that come first are generally
- * preferred.
- *
- * Notice that an inference is intentionally distinct from PfRule. An
- * inference captures *why* we performed a reasoning step, and a PfRule
- * rule captures *what* reasoning step was used. For instance, the inference
- * LEN_SPLIT translates to PfRule::SPLIT. The use of stats on inferences allows
- * us to know that we performed N splits (PfRule::SPLIT) because we wanted
- * to split on lengths for string equalities (Inference::LEN_SPLIT).
- */
-enum class Inference : uint32_t
-{
-  BEGIN,
-  //-------------------------------------- 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
-  // concatenation 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,
-  // injectivity of seq.unit
-  // (seq.unit x) = (seq.unit y) => x=y, or
-  // (seq.unit x) = (seq.unit c) => x=c
-  UNIT_INJ,
-  // unit constant conflict
-  // (seq.unit x) = C => false if |C| != 1.
-  UNIT_CONST_CONFLICT,
-  // injectivity of seq.unit for disequality
-  // (seq.unit x) != (seq.unit y) => x != y, or
-  // (seq.unit x) != (seq.unit c) => x != c
-  UNIT_INJ_DEQ,
-  // 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,
-  // Normal form equality conflict
-  //   x = N[x] ^ y = N[y] ^ x=y => false
-  // where Rewriter::rewrite(N[x]=N[y]) = false.
-  N_EQ_CONF,
-  // 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 = ""
-  N_ENDPOINT_EMP,
-  // Given two normal forms, infers that two components have to be the same if
-  // they have the same length. For example:
-  //   If x1 ++ x2 = x3 ++ x4 and len(x1) = len(x3) then x1 = x3
-  N_UNIFY,
-  // Given two normal forms, infers that the endpoints have to be the same. For
-  // example:
-  //   If x1 ++ x2 = x3 ++ x4 ++ x5 and x1 = x3 then x2 = x4 ++ x5
-  N_ENDPOINT_EQ,
-  // Given two normal forms with constant endpoints, infers a conflict if the
-  // endpoints do not agree. For example:
-  //   If "abc" ++ ... = "bc" ++ ... then conflict
-  N_CONST,
-  // infer empty, for example:
-  //     (~) x = ""
-  // This is inferred when we encounter an x such that x = "" rewrites to a
-  // constant. This inference is used for instance when we otherwise would have
-  // split on the emptiness of x but the rewriter tells us the emptiness of x
-  // can be inferred.
-  INFER_EMP,
-  // string split constant propagation, for example:
-  //     x = y, x = "abc", y = y1 ++ "b" ++ y2
-  //       implies y1 = "a" ++ y1'
-  SSPLIT_CST_PROP,
-  // string split variable propagation, for example:
-  //     x = y, x = x1 ++ x2, y = y1 ++ y2, len( x1 ) >= len( y1 )
-  //       implies x1 = y1 ++ x1'
-  // This is inspired by Zheng et al CAV 2015.
-  SSPLIT_VAR_PROP,
-  // length split, for example:
-  //     len( x1 ) = len( y1 ) V len( x1 ) != len( y1 )
-  // This is inferred when e.g. x = y, x = x1 ++ x2, y = y1 ++ y2.
-  LEN_SPLIT,
-  // length split empty, for example:
-  //     z = "" V z != ""
-  // This is inferred when, e.g. x = y, x = z ++ x1, y = y1 ++ z
-  LEN_SPLIT_EMP,
-  // string split constant
-  //    x = y, x = "c" ++ x2, y = y1 ++ y2, y1 != ""
-  //      implies y1 = "c" ++ y1'
-  // This is a special case of F-Split in Figure 5 of Liang et al CAV 2014.
-  SSPLIT_CST,
-  // string split variable, for example:
-  //    x = y, x = x1 ++ x2, y = y1 ++ y2
-  //      implies x1 = y1 ++ x1' V y1 = x1 ++ y1'
-  // This is rule F-Split in Figure 5 of Liang et al CAV 2014.
-  SSPLIT_VAR,
-  // flat form loop, for example:
-  //    x = y, x = x1 ++ z, y = z ++ y2
-  //      implies z = u2 ++ u1, u in ( u1 ++ u2 )*, x1 = u2 ++ u, y2 = u ++ u1
-  //        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 != ""
-  DEQ_DISL_EMP_SPLIT,
-  // When x ++ x' ++ ... != "abc" ++ y' ++ ... ^ len(x) = 1, we apply the
-  // inference:
-  //   x = "a" v x != "a"
-  DEQ_DISL_FIRST_CHAR_EQ_SPLIT,
-  // When x ++ x' ++ ... != "abc" ++ y' ++ ... ^ len(x) != "", we apply the
-  // inference:
-  //   ni = x ++ x' ++ ... ^ nj = "abc" ++ y' ++ ... ^ x != "" --->
-  //     x = k1 ++ k2 ^ len(k1) = 1 ^ (k1 != "a" v x = "a" ++  k2)
-  DEQ_DISL_FIRST_CHAR_STRING_SPLIT,
-  // When x ++ x' ++ ... != y ++ y' ++ ... ^ len(x) != len(y), we apply the
-  // inference:
-  //   ni = x ++ x' ++ ... ^ nj = y ++ y' ++ ... ^ ni != nj ^ len(x) != len(y)
-  //     --->
-  //       len(k1) = len(x) ^ len(k2) = len(y) ^ (y = k1 ++ k3 v x = k1 ++ k2)
-  DEQ_DISL_STRINGS_SPLIT,
-  // When x ++ x' ++ ... != y ++ y' ++ ... ^ len(x) = len(y), we apply the
-  // inference:
-  //   x = y v x != y
-  DEQ_STRINGS_EQ,
-  // When x ++ x' ++ ... != y ++ y' ++ ... and we do not know how the lengths
-  // of x and y compare, we apply the inference:
-  //   len(x) = len(y) v len(x) != len(y)
-  DEQ_LENS_EQ,
-  // When px ++ x ++ ... != py ^ len(px ++ x ++ ...) = len(py), we apply the
-  // following inference that infers that the remainder of the longer normal
-  // form must be empty:
-  //   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
-  // 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
-  // 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,
-  // 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
-  //-------------------------------------- prefix conflict
-  // prefix conflict (coarse-grained)
-  PREFIX_CONFLICT,
-  //-------------------------------------- end prefix conflict
-  NONE,
-};
-
-/**
- * Converts an inference to a string. Note: This function is also used in
- * `safe_print()`. Changing this functions name or signature will result in
- * `safe_print()` printing "<unsupported>" instead of the proper strings for
- * the enum values.
- *
- * @param i The inference
- * @return The name of the inference
- */
-const char* toString(Inference i);
-
-/**
- * Writes an inference name to a stream.
- *
- * @param out The stream to write to
- * @param i The inference to write to the stream
- * @return The stream
- */
-std::ostream& operator<<(std::ostream& out, Inference i);
-
 /**
  * Length status, used for indicating the length constraints for Skolems
  * introduced by the theory of strings.
@@ -388,7 +79,7 @@ class InferInfo : public TheoryInference
   /** Pointer to the class used for processing this info */
   InferenceManager* d_sim;
   /** The inference identifier */
-  Inference d_id;
+  InferenceId d_id;
   /** Whether it is the reverse form of the above id */
   bool d_idRev;
   /** The conclusion */
diff --git a/src/theory/strings/infer_proof_cons.cpp b/src/theory/strings/infer_proof_cons.cpp
index 4df7ca36a..4817df39d 100644
--- a/src/theory/strings/infer_proof_cons.cpp
+++ b/src/theory/strings/infer_proof_cons.cpp
@@ -56,7 +56,7 @@ void InferProofCons::notifyFact(const InferInfo& ii)
   d_lazyFactMap.insert(ii.d_conc, iic);
 }
 
-void InferProofCons::convert(Inference infer,
+void InferProofCons::convert(InferenceId infer,
                              bool isRev,
                              Node conc,
                              const std::vector<Node>& exp,
@@ -93,12 +93,12 @@ void InferProofCons::convert(Inference infer,
   switch (infer)
   {
     // ========================== equal by substitution+rewriting
-    case Inference::I_NORM_S:
-    case Inference::I_CONST_MERGE:
-    case Inference::I_NORM:
-    case Inference::LEN_NORM:
-    case Inference::NORMAL_FORM:
-    case Inference::CODE_PROXY:
+    case InferenceId::STRINGS_I_NORM_S:
+    case InferenceId::STRINGS_I_CONST_MERGE:
+    case InferenceId::STRINGS_I_NORM:
+    case InferenceId::STRINGS_LEN_NORM:
+    case InferenceId::STRINGS_NORMAL_FORM:
+    case InferenceId::STRINGS_CODE_PROXY:
     {
       ps.d_args.push_back(conc);
       // will attempt this rule
@@ -106,13 +106,13 @@ void InferProofCons::convert(Inference infer,
     }
     break;
     // ========================== substitution + rewriting
-    case Inference::RE_NF_CONFLICT:
-    case Inference::EXTF:
-    case Inference::EXTF_N:
-    case Inference::EXTF_D:
-    case Inference::EXTF_D_N:
-    case Inference::I_CONST_CONFLICT:
-    case Inference::UNIT_CONST_CONFLICT:
+    case InferenceId::STRINGS_RE_NF_CONFLICT:
+    case InferenceId::STRINGS_EXTF:
+    case InferenceId::STRINGS_EXTF_N:
+    case InferenceId::STRINGS_EXTF_D:
+    case InferenceId::STRINGS_EXTF_D_N:
+    case InferenceId::STRINGS_I_CONST_CONFLICT:
+    case InferenceId::STRINGS_UNIT_CONST_CONFLICT:
     {
       if (!ps.d_children.empty())
       {
@@ -132,8 +132,8 @@ void InferProofCons::convert(Inference infer,
     }
     break;
     // ========================== rewrite pred
-    case Inference::EXTF_EQ_REW:
-    case Inference::INFER_EMP:
+    case InferenceId::STRINGS_EXTF_EQ_REW:
+    case InferenceId::STRINGS_INFER_EMP:
     {
       // the last child is the predicate we are operating on, move to front
       Node src = ps.d_children[ps.d_children.size() - 1];
@@ -159,21 +159,21 @@ void InferProofCons::convert(Inference infer,
     }
     break;
     // ========================== substitution+rewriting, CONCAT_EQ, ...
-    case Inference::F_CONST:
-    case Inference::F_UNIFY:
-    case Inference::F_ENDPOINT_EMP:
-    case Inference::F_ENDPOINT_EQ:
-    case Inference::F_NCTN:
-    case Inference::N_EQ_CONF:
-    case Inference::N_CONST:
-    case Inference::N_UNIFY:
-    case Inference::N_ENDPOINT_EMP:
-    case Inference::N_ENDPOINT_EQ:
-    case Inference::N_NCTN:
-    case Inference::SSPLIT_CST_PROP:
-    case Inference::SSPLIT_VAR_PROP:
-    case Inference::SSPLIT_CST:
-    case Inference::SSPLIT_VAR:
+    case InferenceId::STRINGS_F_CONST:
+    case InferenceId::STRINGS_F_UNIFY:
+    case InferenceId::STRINGS_F_ENDPOINT_EMP:
+    case InferenceId::STRINGS_F_ENDPOINT_EQ:
+    case InferenceId::STRINGS_F_NCTN:
+    case InferenceId::STRINGS_N_EQ_CONF:
+    case InferenceId::STRINGS_N_CONST:
+    case InferenceId::STRINGS_N_UNIFY:
+    case InferenceId::STRINGS_N_ENDPOINT_EMP:
+    case InferenceId::STRINGS_N_ENDPOINT_EQ:
+    case InferenceId::STRINGS_N_NCTN:
+    case InferenceId::STRINGS_SSPLIT_CST_PROP:
+    case InferenceId::STRINGS_SSPLIT_VAR_PROP:
+    case InferenceId::STRINGS_SSPLIT_CST:
+    case InferenceId::STRINGS_SSPLIT_VAR:
     {
       Trace("strings-ipc-core") << "Generate core rule for " << infer
                                 << " (rev=" << isRev << ")" << std::endl;
@@ -189,10 +189,10 @@ void InferProofCons::convert(Inference infer,
       // the length constraint
       std::vector<Node> lenConstraint;
       // these inferences have a length constraint as the last explain
-      if (infer == Inference::N_UNIFY || infer == Inference::F_UNIFY
-          || infer == Inference::SSPLIT_CST || infer == Inference::SSPLIT_VAR
-          || infer == Inference::SSPLIT_VAR_PROP
-          || infer == Inference::SSPLIT_CST_PROP)
+      if (infer == InferenceId::STRINGS_N_UNIFY || infer == InferenceId::STRINGS_F_UNIFY
+          || infer == InferenceId::STRINGS_SSPLIT_CST || infer == InferenceId::STRINGS_SSPLIT_VAR
+          || infer == InferenceId::STRINGS_SSPLIT_VAR_PROP
+          || infer == InferenceId::STRINGS_SSPLIT_CST_PROP)
       {
         if (exp.size() >= 2)
         {
@@ -269,10 +269,10 @@ void InferProofCons::convert(Inference infer,
       }
       // Now, mainEqCeq is an equality t ++ ... == s ++ ... where the
       // inference involved t and s.
-      if (infer == Inference::N_ENDPOINT_EQ
-          || infer == Inference::N_ENDPOINT_EMP
-          || infer == Inference::F_ENDPOINT_EQ
-          || infer == Inference::F_ENDPOINT_EMP)
+      if (infer == InferenceId::STRINGS_N_ENDPOINT_EQ
+          || infer == InferenceId::STRINGS_N_ENDPOINT_EMP
+          || infer == InferenceId::STRINGS_F_ENDPOINT_EQ
+          || infer == InferenceId::STRINGS_F_ENDPOINT_EMP)
       {
         // Should be equal to conclusion already, or rewrite to it.
         // Notice that this step is necessary to handle the "rproc"
@@ -295,8 +295,8 @@ void InferProofCons::convert(Inference infer,
         // t1 ++ ... ++ tn == "". However, these are very rarely applied, let
         // alone for 2+ children. This case is intentionally unhandled here.
       }
-      else if (infer == Inference::N_CONST || infer == Inference::F_CONST
-               || infer == Inference::N_EQ_CONF)
+      else if (infer == InferenceId::STRINGS_N_CONST || infer == InferenceId::STRINGS_F_CONST
+               || infer == InferenceId::STRINGS_N_EQ_CONF)
       {
         // should be a constant conflict
         std::vector<Node> childrenC;
@@ -320,15 +320,15 @@ void InferProofCons::convert(Inference infer,
         Node s0 = svec[isRev ? svec.size() - 1 : 0];
         bool applySym = false;
         // may need to apply symmetry
-        if ((infer == Inference::SSPLIT_CST
-             || infer == Inference::SSPLIT_CST_PROP)
+        if ((infer == InferenceId::STRINGS_SSPLIT_CST
+             || infer == InferenceId::STRINGS_SSPLIT_CST_PROP)
             && t0.isConst())
         {
           Assert(!s0.isConst());
           applySym = true;
           std::swap(t0, s0);
         }
-        if (infer == Inference::N_UNIFY || infer == Inference::F_UNIFY)
+        if (infer == InferenceId::STRINGS_N_UNIFY || infer == InferenceId::STRINGS_F_UNIFY)
         {
           if (conc.getKind() != EQUAL)
           {
@@ -347,7 +347,7 @@ void InferProofCons::convert(Inference infer,
         // the form of the required length constraint expected by the proof
         Node lenReq;
         bool lenSuccess = false;
-        if (infer == Inference::N_UNIFY || infer == Inference::F_UNIFY)
+        if (infer == InferenceId::STRINGS_N_UNIFY || infer == InferenceId::STRINGS_F_UNIFY)
         {
           // the required premise for unify is always len(x) = len(y),
           // however the explanation may not be literally this. Thus, we
@@ -359,7 +359,7 @@ void InferProofCons::convert(Inference infer,
           lenSuccess = convertLengthPf(lenReq, lenConstraint, psb);
           rule = PfRule::CONCAT_UNIFY;
         }
-        else if (infer == Inference::SSPLIT_VAR)
+        else if (infer == InferenceId::STRINGS_SSPLIT_VAR)
         {
           // it should be the case that lenConstraint => lenReq
           lenReq = nm->mkNode(STRING_LENGTH, t0)
@@ -368,7 +368,7 @@ void InferProofCons::convert(Inference infer,
           lenSuccess = convertLengthPf(lenReq, lenConstraint, psb);
           rule = PfRule::CONCAT_SPLIT;
         }
-        else if (infer == Inference::SSPLIT_CST)
+        else if (infer == InferenceId::STRINGS_SSPLIT_CST)
         {
           // it should be the case that lenConstraint => lenReq
           lenReq = nm->mkNode(STRING_LENGTH, t0)
@@ -377,7 +377,7 @@ void InferProofCons::convert(Inference infer,
           lenSuccess = convertLengthPf(lenReq, lenConstraint, psb);
           rule = PfRule::CONCAT_CSPLIT;
         }
-        else if (infer == Inference::SSPLIT_VAR_PROP)
+        else if (infer == InferenceId::STRINGS_SSPLIT_VAR_PROP)
         {
           // it should be the case that lenConstraint => lenReq
           for (unsigned r = 0; r < 2; r++)
@@ -399,7 +399,7 @@ void InferProofCons::convert(Inference infer,
           }
           rule = PfRule::CONCAT_LPROP;
         }
-        else if (infer == Inference::SSPLIT_CST_PROP)
+        else if (infer == InferenceId::STRINGS_SSPLIT_CST_PROP)
         {
           // it should be the case that lenConstraint => lenReq
           lenReq = nm->mkNode(STRING_LENGTH, t0)
@@ -465,8 +465,8 @@ void InferProofCons::convert(Inference infer,
     }
     break;
     // ========================== Disequalities
-    case Inference::DEQ_DISL_FIRST_CHAR_STRING_SPLIT:
-    case Inference::DEQ_DISL_STRINGS_SPLIT:
+    case InferenceId::STRINGS_DEQ_DISL_FIRST_CHAR_STRING_SPLIT:
+    case InferenceId::STRINGS_DEQ_DISL_STRINGS_SPLIT:
     {
       if (conc.getKind() != AND || conc.getNumChildren() != 2
           || conc[0].getKind() != EQUAL || !conc[0][0].getType().isStringLike()
@@ -506,14 +506,14 @@ void InferProofCons::convert(Inference infer,
     }
     break;
     // ========================== Boolean split
-    case Inference::CARD_SP:
-    case Inference::LEN_SPLIT:
-    case Inference::LEN_SPLIT_EMP:
-    case Inference::DEQ_DISL_EMP_SPLIT:
-    case Inference::DEQ_DISL_FIRST_CHAR_EQ_SPLIT:
-    case Inference::DEQ_STRINGS_EQ:
-    case Inference::DEQ_LENS_EQ:
-    case Inference::DEQ_LENGTH_SP:
+    case InferenceId::STRINGS_CARD_SP:
+    case InferenceId::STRINGS_LEN_SPLIT:
+    case InferenceId::STRINGS_LEN_SPLIT_EMP:
+    case InferenceId::STRINGS_DEQ_DISL_EMP_SPLIT:
+    case InferenceId::STRINGS_DEQ_DISL_FIRST_CHAR_EQ_SPLIT:
+    case InferenceId::STRINGS_DEQ_STRINGS_EQ:
+    case InferenceId::STRINGS_DEQ_LENS_EQ:
+    case InferenceId::STRINGS_DEQ_LENGTH_SP:
     {
       if (conc.getKind() != OR)
       {
@@ -530,10 +530,10 @@ void InferProofCons::convert(Inference infer,
     }
     break;
     // ========================== Regular expression unfolding
-    case Inference::RE_UNFOLD_POS:
-    case Inference::RE_UNFOLD_NEG:
+    case InferenceId::STRINGS_RE_UNFOLD_POS:
+    case InferenceId::STRINGS_RE_UNFOLD_NEG:
     {
-      if (infer == Inference::RE_UNFOLD_POS)
+      if (infer == InferenceId::STRINGS_RE_UNFOLD_POS)
       {
         ps.d_rule = PfRule::RE_UNFOLD_POS;
       }
@@ -559,8 +559,8 @@ void InferProofCons::convert(Inference infer,
     }
     break;
     // ========================== Reduction
-    case Inference::CTN_POS:
-    case Inference::CTN_NEG_EQUAL:
+    case InferenceId::STRINGS_CTN_POS:
+    case InferenceId::STRINGS_CTN_NEG_EQUAL:
     {
       if (ps.d_children.size() != 1)
       {
@@ -595,7 +595,7 @@ void InferProofCons::convert(Inference infer,
     }
     break;
 
-    case Inference::REDUCTION:
+    case InferenceId::STRINGS_REDUCTION:
     {
       size_t nchild = conc.getNumChildren();
       Node mainEq;
@@ -635,7 +635,7 @@ void InferProofCons::convert(Inference infer,
     }
     break;
     // ========================== code injectivity
-    case Inference::CODE_INJ:
+    case InferenceId::STRINGS_CODE_INJ:
     {
       ps.d_rule = PfRule::STRING_CODE_INJ;
       Assert(conc.getKind() == OR && conc.getNumChildren() == 3
@@ -645,11 +645,11 @@ void InferProofCons::convert(Inference infer,
     }
     break;
     // ========================== unit injectivity
-    case Inference::UNIT_INJ: { ps.d_rule = PfRule::STRING_SEQ_UNIT_INJ;
+    case InferenceId::STRINGS_UNIT_INJ: { ps.d_rule = PfRule::STRING_SEQ_UNIT_INJ;
     }
     break;
     // ========================== prefix conflict
-    case Inference::PREFIX_CONFLICT:
+    case InferenceId::STRINGS_PREFIX_CONFLICT:
     {
       Trace("strings-ipc-prefix") << "Prefix conflict..." << std::endl;
       std::vector<Node> eqs;
@@ -740,9 +740,9 @@ void InferProofCons::convert(Inference infer,
     }
     break;
     // ========================== regular expressions
-    case Inference::RE_INTER_INCLUDE:
-    case Inference::RE_INTER_CONF:
-    case Inference::RE_INTER_INFER:
+    case InferenceId::STRINGS_RE_INTER_INCLUDE:
+    case InferenceId::STRINGS_RE_INTER_CONF:
+    case InferenceId::STRINGS_RE_INTER_INFER:
     {
       std::vector<Node> reiExp;
       std::vector<Node> reis;
@@ -810,17 +810,17 @@ void InferProofCons::convert(Inference infer,
     }
     break;
     // ========================== unknown and currently unsupported
-    case Inference::CARDINALITY:
-    case Inference::I_CYCLE_E:
-    case Inference::I_CYCLE:
-    case Inference::RE_DELTA:
-    case Inference::RE_DELTA_CONF:
-    case Inference::RE_DERIVE:
-    case Inference::FLOOP:
-    case Inference::FLOOP_CONFLICT:
-    case Inference::DEQ_NORM_EMP:
-    case Inference::CTN_TRANS:
-    case Inference::CTN_DECOMPOSE:
+    case InferenceId::STRINGS_CARDINALITY:
+    case InferenceId::STRINGS_I_CYCLE_E:
+    case InferenceId::STRINGS_I_CYCLE:
+    case InferenceId::STRINGS_RE_DELTA:
+    case InferenceId::STRINGS_RE_DELTA_CONF:
+    case InferenceId::STRINGS_RE_DERIVE:
+    case InferenceId::STRINGS_FLOOP:
+    case InferenceId::STRINGS_FLOOP_CONFLICT:
+    case InferenceId::STRINGS_DEQ_NORM_EMP:
+    case InferenceId::STRINGS_CTN_TRANS:
+    case InferenceId::STRINGS_CTN_DECOMPOSE:
     default:
       // do nothing, these will be converted to STRING_TRUST below since the
       // rule is unknown.
diff --git a/src/theory/strings/infer_proof_cons.h b/src/theory/strings/infer_proof_cons.h
index 1b066b4b3..49fd338b5 100644
--- a/src/theory/strings/infer_proof_cons.h
+++ b/src/theory/strings/infer_proof_cons.h
@@ -100,7 +100,7 @@ class InferProofCons : public ProofGenerator
    * In particular, psb will contain a set of steps that form a proof
    * whose conclusion is ii.d_conc and whose free assumptions are ii.d_ant.
    */
-  void convert(Inference infer,
+  void convert(InferenceId infer,
                bool isRev,
                Node conc,
                const std::vector<Node>& exp,
diff --git a/src/theory/strings/inference_manager.cpp b/src/theory/strings/inference_manager.cpp
index 0c55d26e8..6a4fd55df 100644
--- a/src/theory/strings/inference_manager.cpp
+++ b/src/theory/strings/inference_manager.cpp
@@ -65,7 +65,7 @@ void InferenceManager::doPending()
 
 bool InferenceManager::sendInternalInference(std::vector<Node>& exp,
                                              Node conc,
-                                             Inference infer)
+                                             InferenceId infer)
 {
   if (conc.getKind() == AND
       || (conc.getKind() == NOT && conc[0].getKind() == OR))
@@ -125,7 +125,7 @@ bool InferenceManager::sendInternalInference(std::vector<Node>& exp,
 bool InferenceManager::sendInference(const std::vector<Node>& exp,
                                      const std::vector<Node>& noExplain,
                                      Node eq,
-                                     Inference infer,
+                                     InferenceId infer,
                                      bool isRev,
                                      bool asLemma)
 {
@@ -151,7 +151,7 @@ bool InferenceManager::sendInference(const std::vector<Node>& exp,
 
 bool InferenceManager::sendInference(const std::vector<Node>& exp,
                                      Node eq,
-                                     Inference infer,
+                                     InferenceId infer,
                                      bool isRev,
                                      bool asLemma)
 {
@@ -225,7 +225,7 @@ void InferenceManager::sendInference(InferInfo& ii, bool asLemma)
   addPendingFact(std::unique_ptr<InferInfo>(new InferInfo(ii)));
 }
 
-bool InferenceManager::sendSplit(Node a, Node b, Inference infer, bool preq)
+bool InferenceManager::sendSplit(Node a, Node b, InferenceId infer, bool preq)
 {
   Node eq = a.eqNode(b);
   eq = Rewriter::rewrite(eq);
@@ -412,7 +412,7 @@ bool InferenceManager::processLemma(InferInfo& ii)
     }
   }
   LemmaProperty p = LemmaProperty::NONE;
-  if (ii.d_id == Inference::REDUCTION)
+  if (ii.d_id == InferenceId::STRINGS_REDUCTION)
   {
     p |= LemmaProperty::NEEDS_JUSTIFY;
   }
diff --git a/src/theory/strings/inference_manager.h b/src/theory/strings/inference_manager.h
index 3280281bd..f16ce7183 100644
--- a/src/theory/strings/inference_manager.h
+++ b/src/theory/strings/inference_manager.h
@@ -114,7 +114,7 @@ class InferenceManager : public InferenceManagerBuffered
    */
   bool sendInternalInference(std::vector<Node>& exp,
                              Node conc,
-                             Inference infer);
+                             InferenceId infer);
 
   /** send inference
    *
@@ -164,13 +164,13 @@ class InferenceManager : public InferenceManagerBuffered
   bool sendInference(const std::vector<Node>& exp,
                      const std::vector<Node>& noExplain,
                      Node eq,
-                     Inference infer,
+                     InferenceId infer,
                      bool isRev = false,
                      bool asLemma = false);
   /** same as above, but where noExplain is empty */
   bool sendInference(const std::vector<Node>& exp,
                      Node eq,
-                     Inference infer,
+                     InferenceId infer,
                      bool isRev = false,
                      bool asLemma = false);
 
@@ -200,7 +200,7 @@ class InferenceManager : public InferenceManagerBuffered
    * 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, Inference infer, bool preq = true);
+  bool sendSplit(Node a, Node b, InferenceId infer, bool preq = true);
   /**
    * Set that we are incomplete for the current set of assertions (in other
    * words, we must answer "unknown" instead of "sat"); this calls the output
diff --git a/src/theory/strings/regexp_solver.cpp b/src/theory/strings/regexp_solver.cpp
index 46570df48..2892b2398 100644
--- a/src/theory/strings/regexp_solver.cpp
+++ b/src/theory/strings/regexp_solver.cpp
@@ -227,7 +227,7 @@ void RegExpSolver::check(const std::map<Node, std::vector<Node> >& mems)
               noExplain.push_back(assertion);
               Node conc = Node::null();
               d_im.sendInference(
-                  iexp, noExplain, conc, Inference::RE_NF_CONFLICT);
+                  iexp, noExplain, conc, InferenceId::STRINGS_RE_NF_CONFLICT);
               addedLemma = true;
               break;
             }
@@ -282,8 +282,8 @@ void RegExpSolver::check(const std::map<Node, std::vector<Node> >& mems)
             {
               d_statistics.d_regexpUnfoldingsNeg << atom[1].getKind();
             }
-            Inference inf =
-                polarity ? Inference::RE_UNFOLD_POS : Inference::RE_UNFOLD_NEG;
+            InferenceId inf =
+                polarity ? InferenceId::STRINGS_RE_UNFOLD_POS : InferenceId::STRINGS_RE_UNFOLD_NEG;
             d_im.sendInference(iexp, noExplain, conc, inf);
             addedLemma = true;
             if (changed)
@@ -404,7 +404,7 @@ bool RegExpSolver::checkEqcInclusion(std::vector<Node>& mems)
 
           Node conc;
           d_im.sendInference(
-              vec_nodes, conc, Inference::RE_INTER_INCLUDE, false, true);
+              vec_nodes, conc, InferenceId::STRINGS_RE_INTER_INCLUDE, false, true);
           return false;
         }
       }
@@ -486,7 +486,7 @@ bool RegExpSolver::checkEqcIntersect(const std::vector<Node>& mems)
       }
       Node conc;
       d_im.sendInference(
-          vec_nodes, conc, Inference::RE_INTER_CONF, false, true);
+          vec_nodes, conc, InferenceId::STRINGS_RE_INTER_CONF, false, true);
       // conflict, return
       return false;
     }
@@ -516,7 +516,7 @@ bool RegExpSolver::checkEqcIntersect(const std::vector<Node>& mems)
         vec_nodes.push_back(mi[0].eqNode(m[0]));
       }
       d_im.sendInference(
-          vec_nodes, mres, Inference::RE_INTER_INFER, false, true);
+          vec_nodes, mres, InferenceId::STRINGS_RE_INTER_INFER, false, true);
       // both are reduced
       d_im.markReduced(m);
       d_im.markReduced(mi);
@@ -542,7 +542,7 @@ bool RegExpSolver::checkPDerivative(
         noExplain.push_back(x.eqNode(d_emptyString));
         std::vector<Node> iexp = nf_exp;
         iexp.insert(iexp.end(), noExplain.begin(), noExplain.end());
-        d_im.sendInference(iexp, noExplain, exp, Inference::RE_DELTA);
+        d_im.sendInference(iexp, noExplain, exp, InferenceId::STRINGS_RE_DELTA);
         addedLemma = true;
         d_regexp_ccached.insert(atom);
         return false;
@@ -559,7 +559,7 @@ bool RegExpSolver::checkPDerivative(
         noExplain.push_back(x.eqNode(d_emptyString));
         std::vector<Node> iexp = nf_exp;
         iexp.insert(iexp.end(), noExplain.begin(), noExplain.end());
-        d_im.sendInference(iexp, noExplain, d_false, Inference::RE_DELTA_CONF);
+        d_im.sendInference(iexp, noExplain, d_false, InferenceId::STRINGS_RE_DELTA_CONF);
         addedLemma = true;
         d_regexp_ccached.insert(atom);
         return false;
@@ -652,7 +652,7 @@ bool RegExpSolver::deriveRegExp(Node x,
     std::vector<Node> noExplain;
     noExplain.push_back(atom);
     iexp.push_back(atom);
-    d_im.sendInference(iexp, noExplain, conc, Inference::RE_DERIVE);
+    d_im.sendInference(iexp, noExplain, conc, InferenceId::STRINGS_RE_DERIVE);
     return true;
   }
   return false;
diff --git a/src/theory/strings/sequences_stats.h b/src/theory/strings/sequences_stats.h
index e35d951f7..e7e45b18f 100644
--- a/src/theory/strings/sequences_stats.h
+++ b/src/theory/strings/sequences_stats.h
@@ -61,12 +61,12 @@ class SequencesStatistics
   IntStat d_strategyRuns;
   //--------------- inferences
   /** Counts the number of applications of each type of inference */
-  HistogramStat<Inference> d_inferences;
+  HistogramStat<InferenceId> d_inferences;
   /**
    * Counts the number of applications of each type of inference that were not
    * processed as a proof step. This is a subset of d_inferences.
    */
-  HistogramStat<Inference> d_inferencesNoPf;
+  HistogramStat<InferenceId> d_inferencesNoPf;
   /**
    * 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
diff --git a/src/theory/strings/solver_state.cpp b/src/theory/strings/solver_state.cpp
index f341e681d..b6e9c68f4 100644
--- a/src/theory/strings/solver_state.cpp
+++ b/src/theory/strings/solver_state.cpp
@@ -138,7 +138,7 @@ void SolverState::setPendingPrefixConflictWhen(Node conf)
     return;
   }
   InferInfo iiPrefixConf;
-  iiPrefixConf.d_id = Inference::PREFIX_CONFLICT;
+  iiPrefixConf.d_id = InferenceId::STRINGS_PREFIX_CONFLICT;
   iiPrefixConf.d_conc = d_false;
   utils::flattenOp(AND, conf, iiPrefixConf.d_premises);
   setPendingConflict(iiPrefixConf);
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index f25f9e29c..48d461f7a 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -921,7 +921,7 @@ void TheoryStrings::checkCodes()
         if (!d_state.areEqual(cc, vc))
         {
           std::vector<Node> emptyVec;
-          d_im.sendInference(emptyVec, cc.eqNode(vc), Inference::CODE_PROXY);
+          d_im.sendInference(emptyVec, cc.eqNode(vc), InferenceId::STRINGS_CODE_PROXY);
         }
         const_codes.push_back(vc);
       }
@@ -961,7 +961,7 @@ void TheoryStrings::checkCodes()
           deq = Rewriter::rewrite(deq);
           d_im.addPendingPhaseRequirement(deq, false);
           std::vector<Node> emptyVec;
-          d_im.sendInference(emptyVec, inj_lem, Inference::CODE_INJ);
+          d_im.sendInference(emptyVec, inj_lem, InferenceId::STRINGS_CODE_INJ);
         }
       }
     }