From 865fb413bf91d395a90cf0cc502e1dbc7d2d8ebb Mon Sep 17 00:00:00 2001 From: mudathirmahgoub Date: Sun, 24 Jan 2021 18:18:12 -0600 Subject: [PATCH] rename InferInfo::d_newSkolem to InferInfo::d_skolems (#5799) Rename strings::InferInfo::d_newSkolem to InferInfo::d_skolems to match bags::InferInfo:d_skolems --- src/theory/strings/core_solver.cpp | 6 +++--- src/theory/strings/infer_info.h | 2 +- src/theory/strings/inference_manager.cpp | 2 +- 3 files changed, 5 insertions(+), 5 deletions(-) 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 > d_newSkolem; + std::map > 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 >& sks : - ii.d_newSkolem) + ii.d_skolems) { for (const Node& n : sks.second) { -- 2.30.2