From: mudathirmahgoub <mudathirmahgoub@gmail.com>
Date: Mon, 25 Jan 2021 00:18:12 +0000 (-0600)
Subject: rename InferInfo::d_newSkolem to InferInfo::d_skolems (#5799)
X-Git-Tag: cvc5-1.0.0~2361
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=865fb413bf91d395a90cf0cc502e1dbc7d2d8ebb;p=cvc5.git

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 38396bc63..6f7c97037 100644
--- 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 b586609ad..863f1ab06 100644
--- 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 05937cf56..cf90c8fbe 100644
--- 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)
     {