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/bv | |
| 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/bv')
| -rw-r--r-- | src/theory/bv/abstraction.cpp | 14 | ||||
| -rw-r--r-- | src/theory/bv/bv_subtheory_algebraic.cpp | 7 |
2 files changed, 11 insertions, 10 deletions
diff --git a/src/theory/bv/abstraction.cpp b/src/theory/bv/abstraction.cpp index d3aeb5c37..f2f12a548 100644 --- a/src/theory/bv/abstraction.cpp +++ b/src/theory/bv/abstraction.cpp @@ -95,10 +95,10 @@ bool AbstractionModule::applyAbstraction(const std::vector<Node>& assertions, // we did not change anything return false; } - NodeNodeMap seen; + NodeNodeMap seen_rev; for (unsigned i = 0; i < new_assertions.size(); ++i) { - new_assertions[i] = reverseAbstraction(new_assertions[i], seen); + new_assertions[i] = reverseAbstraction(new_assertions[i], seen_rev); } // we undo the abstraction functions so the logic is QF_BV still return true; @@ -235,13 +235,15 @@ void AbstractionModule::skolemizeArguments(std::vector<Node>& assertions) // enumerate arguments assignments std::vector<Node> or_assignments; - for (ArgsTableEntry::iterator it = args.begin(); it != args.end(); ++it) + for (const ArgsVec& av : args) + // for (ArgsTableEntry::iterator it = args.begin(); it != args.end(); + // ++it) { NodeBuilder<> arg_assignment(kind::AND); - ArgsVec& args = *it; - for (unsigned k = 0; k < args.size(); ++k) + // ArgsVec& args = *it; + for (unsigned k = 0; k < av.size(); ++k) { - Node eq = nm->mkNode(kind::EQUAL, args[k], skolem_args[k]); + Node eq = nm->mkNode(kind::EQUAL, av[k], skolem_args[k]); arg_assignment << eq; } or_assignments.push_back(arg_assignment); diff --git a/src/theory/bv/bv_subtheory_algebraic.cpp b/src/theory/bv/bv_subtheory_algebraic.cpp index 14753deec..de8a0e11e 100644 --- a/src/theory/bv/bv_subtheory_algebraic.cpp +++ b/src/theory/bv/bv_subtheory_algebraic.cpp @@ -984,10 +984,9 @@ Node mergeExplanations(const std::vector<Node>& expls) { TNode expl = expls[i]; Assert(expl.getType().isBoolean()); if (expl.getKind() == kind::AND) { - for (unsigned i = 0; i < expl.getNumChildren(); ++i) { - TNode child = expl[i]; - if (child == utils::mkTrue()) - continue; + for (const TNode& child : expl) + { + if (child == utils::mkTrue()) continue; literals.insert(child); } } else if (expl != utils::mkTrue()) { |