rename InferInfo::d_newSkolem to InferInfo::d_skolems (#5799)

Rename strings::InferInfo::d_newSkolem to InferInfo::d_skolems to match bags::InferInfo:d_skolems

diff --git a/src/theory/strings/core_solver.cpp b/src/theory/strings/core_solver.cpp
index 38396bc633e909f8978ad99621fc2ede8288db6c..6f7c97037c641b0bff6a24493cbfed3ab96c2797 100644 (file)
--- a/src/theory/strings/core_solver.cpp
+++ b/src/theory/strings/core_solver.cpp
@@ -1593,7 +1593,7 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi,
           iinfo.d_conc = getConclusion(
               xcv, stra, PfRule::CONCAT_CPROP, isRev, skc, newSkolems);
           Assert(newSkolems.size() == 1);
-          iinfo.d_newSkolem[LENGTH_SPLIT].push_back(newSkolems[0]);
+          iinfo.d_skolems[LENGTH_SPLIT].push_back(newSkolems[0]);
           iinfo.d_id = Inference::SSPLIT_CST_PROP;
           iinfo.d_idRev = isRev;
           pinfer.push_back(info);
@@ -1613,7 +1613,7 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi,
           nfi, nfj, index, index, iinfo.d_premises);
       iinfo.d_premises.push_back(expNonEmpty);
       Assert(newSkolems.size() == 1);
-      iinfo.d_newSkolem[LENGTH_SPLIT].push_back(newSkolems[0]);
+      iinfo.d_skolems[LENGTH_SPLIT].push_back(newSkolems[0]);
       iinfo.d_id = Inference::SSPLIT_CST;
       iinfo.d_idRev = isRev;
       pinfer.push_back(info);
@@ -1709,7 +1709,7 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi,
       if (options::stringUnifiedVSpt() && !options::stringLenConc())
       {
         Assert(newSkolems.size() == 1);
-        iinfo.d_newSkolem[LENGTH_GEQ_ONE].push_back(newSkolems[0]);
+        iinfo.d_skolems[LENGTH_GEQ_ONE].push_back(newSkolems[0]);
       }
     }
     else if (lentTestSuccess == 0)

diff --git a/src/theory/strings/infer_info.h b/src/theory/strings/infer_info.h
index b586609ada73a85c6b31d48cf64d1938bb00fdb7..863f1ab06e824ad661ee56fde393193fc6588555 100644 (file)
--- a/src/theory/strings/infer_info.h
+++ b/src/theory/strings/infer_info.h
@@ -404,7 +404,7 @@ class InferInfo : public TheoryInference
    * are mapped to by a length status, indicating the length constraint that
    * can be assumed for them.
    */
-  std::map<LengthStatus, std::vector<Node> > d_newSkolem;
+  std::map<LengthStatus, std::vector<Node> > d_skolems;
   /**  Is this infer info trivial? True if d_conc is true. */
   bool isTrivial() const;
   /**

diff --git a/src/theory/strings/inference_manager.cpp b/src/theory/strings/inference_manager.cpp
index 05937cf56bd75d443d8f4ef9030614d1f3360ab1..cf90c8fbe19e882f3fc9467e60ed816e2c3c5a5c 100644 (file)
--- a/src/theory/strings/inference_manager.cpp
+++ b/src/theory/strings/inference_manager.cpp
@@ -412,7 +412,7 @@ bool InferenceManager::processLemma(InferInfo& ii)
   // (lazily), since this is the moment when we have decided to process the
   // inference.
   for (const std::pair<const LengthStatus, std::vector<Node> >& sks :
-       ii.d_newSkolem)
+       ii.d_skolems)
   {
     for (const Node& n : sks.second)
     {