diff options
| author | mudathirmahgoub <mudathirmahgoub@gmail.com> | 2021-01-24 18:18:12 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-01-24 18:18:12 -0600 |
| commit | 865fb413bf91d395a90cf0cc502e1dbc7d2d8ebb (patch) | |
| tree | d97b36e3b33a2ef151aa12a3ee38a96375e8a184 /src/theory | |
| parent | ae541bb35e7b627f28b13eede29f5870f42b078e (diff) | |
rename InferInfo::d_newSkolem to InferInfo::d_skolems (#5799)
Rename strings::InferInfo::d_newSkolem to InferInfo::d_skolems to match bags::InferInfo:d_skolems
Diffstat (limited to 'src/theory')
| -rw-r--r-- | src/theory/strings/core_solver.cpp | 6 | ||||
| -rw-r--r-- | src/theory/strings/infer_info.h | 2 | ||||
| -rw-r--r-- | 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<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) { |