diff options
author | Mathias Preiner <mathias.preiner@gmail.com> | 2020-03-05 11:42:54 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-03-05 11:42:54 -0800 |
commit | 04039407e6308070c148de0d5e93640ec1b0a341 (patch) | |
tree | b66f63d49df0713b1ca2a440bec89f1d60af32a4 /src/theory/theory_model.cpp | |
parent | 18fe192c29a9a2c37d1925730af01e906b9888c5 (diff) |
Enable -Wshadow and fix warnings. (#3909)
Fixes all -Wshadow warnings and enables the -Wshadow compile flag globally.
Co-authored-by: Clark Barrett <barrett@cs.stanford.edu>
Co-authored-by: Andres Noetzli <andres.noetzli@gmail.com>
Co-authored-by: Aina Niemetz <aina.niemetz@gmail.com>
Co-authored-by: Alex Ozdemir <aozdemir@hmc.edu>
Co-authored-by: makaimann <makaim@stanford.edu>
Co-authored-by: yoni206 <yoni206@users.noreply.github.com>
Co-authored-by: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Co-authored-by: AleksandarZeljic <zeljic@stanford.edu>
Co-authored-by: Caleb Donovick <cdonovick@users.noreply.github.com>
Co-authored-by: Amalee <amaleewilson@gmail.com>
Co-authored-by: Scott Kovach <dskovach@gmail.com>
Co-authored-by: ntsis <nekuna@gmail.com>
Diffstat (limited to 'src/theory/theory_model.cpp')
-rw-r--r-- | src/theory/theory_model.cpp | 13 |
1 files changed, 6 insertions, 7 deletions
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index 399695131..bf0a82a20 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -267,9 +267,9 @@ Node TheoryModel::getModelValue(TNode n, bool hasBoundVars) const // choice z. P(z). Node v = nm->mkBoundVar(n.getType()); Node bvl = nm->mkNode(BOUND_VAR_LIST, v); - Node ret = nm->mkNode(CHOICE, bvl, ita->second.substitute(n, v)); - d_modelCache[n] = ret; - return ret; + Node answer = nm->mkNode(CHOICE, bvl, ita->second.substitute(n, v)); + d_modelCache[n] = answer; + return answer; } // must rewrite the term at this point ret = Rewriter::rewrite(n); @@ -315,11 +315,11 @@ Node TheoryModel::getModelValue(TNode n, bool hasBoundVars) const { if (d_enableFuncModels) { - std::map<Node, Node>::const_iterator it = d_uf_models.find(n); - if (it != d_uf_models.end()) + std::map<Node, Node>::const_iterator entry = d_uf_models.find(n); + if (entry != d_uf_models.end()) { // Existing function - ret = it->second; + ret = entry->second; d_modelCache[n] = ret; return ret; } @@ -327,7 +327,6 @@ Node TheoryModel::getModelValue(TNode n, bool hasBoundVars) const // constant in the enumeration of the range type vector<TypeNode> argTypes = t.getArgTypes(); vector<Node> args; - NodeManager* nm = NodeManager::currentNM(); for (unsigned i = 0, size = argTypes.size(); i < size; ++i) { args.push_back(nm->mkBoundVar(argTypes[i])); |