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.

1 files changed, 9 insertions, 9 deletions

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);
   }
 }