From cc6e04b4572180596ae25001d4a1b99884030a62 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Thu, 10 Dec 2020 01:10:36 +0100 Subject: [PATCH] Fixed a bunch of clang warnings. (#5637) --- src/expr/dtype.cpp | 2 +- src/expr/lazy_proof_chain.cpp | 4 ++-- src/prop/minisat/minisat.cpp | 20 +++++++++---------- src/smt/proof_manager.cpp | 2 +- src/smt/smt_solver.h | 2 +- src/theory/arith/nl/iand_utils.cpp | 2 +- src/theory/arith/nl/nonlinear_extension.cpp | 1 - src/theory/arith/nl/nonlinear_extension.h | 2 -- .../transcendental/transcendental_state.cpp | 15 -------------- src/theory/arrays/theory_arrays.cpp | 6 +++--- src/theory/arrays/theory_arrays.h | 2 +- src/theory/bv/theory_bv_utils.h | 4 ++-- src/theory/datatypes/sygus_extension.cpp | 4 ++-- .../quantifiers/conjecture_generator.cpp | 2 +- .../quantifiers/quantifiers_rewriter.cpp | 4 ++-- src/theory/quantifiers/query_generator.cpp | 2 +- .../sygus/enum_stream_substitution.cpp | 4 ++-- src/theory/quantifiers/sygus_sampler.cpp | 2 +- src/theory/quantifiers/term_database.cpp | 8 ++++---- src/theory/sep/theory_sep.cpp | 2 +- src/theory/sets/cardinality_extension.cpp | 2 +- src/theory/sets/theory_sets_private.cpp | 2 +- src/theory/strings/core_solver.cpp | 2 +- src/theory/strings/normal_form.cpp | 4 ++-- src/theory/theory_engine.cpp | 2 +- src/theory/uf/equality_engine.cpp | 2 +- src/theory/uf/proof_equality_engine.cpp | 2 +- src/theory/uf/symmetry_breaker.cpp | 4 ++-- 28 files changed, 46 insertions(+), 64 deletions(-) diff --git a/src/expr/dtype.cpp b/src/expr/dtype.cpp index 657298491..4c93e5727 100644 --- a/src/expr/dtype.cpp +++ b/src/expr/dtype.cpp @@ -171,7 +171,7 @@ bool DType::resolve(const std::map& resolutions, d_involvesExt = false; d_involvesUt = false; - for (const std::shared_ptr ctor : d_constructors) + for (const std::shared_ptr& ctor : d_constructors) { if (ctor->involvesExternalType()) { diff --git a/src/expr/lazy_proof_chain.cpp b/src/expr/lazy_proof_chain.cpp index c58bb78e4..665e68d28 100644 --- a/src/expr/lazy_proof_chain.cpp +++ b/src/expr/lazy_proof_chain.cpp @@ -41,7 +41,7 @@ const std::map> LazyCDProofChain::getLinks() const { std::map> links; - for (const std::pair& link : d_gens) + for (const std::pair& link : d_gens) { Assert(link.second); std::shared_ptr pfn = link.second->getProofFor(link.first); @@ -269,7 +269,7 @@ void LazyCDProofChain::addLazyStep(Node expected, std::shared_ptr pfn = pg->getProofFor(expected); std::vector allowedLeaves{assumptions.begin(), assumptions.end()}; // add all current links in the chain - for (const std::pair& link : d_gens) + for (const std::pair& link : d_gens) { allowedLeaves.push_back(link.first); } diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp index fa31eb41c..aae347caf 100644 --- a/src/prop/minisat/minisat.cpp +++ b/src/prop/minisat/minisat.cpp @@ -271,16 +271,16 @@ MinisatSatSolver::Statistics::~Statistics() { d_registry->unregisterStat(&d_statTotLiterals); } -void MinisatSatSolver::Statistics::init(Minisat::SimpSolver* d_minisat){ - d_statStarts.setData(d_minisat->starts); - d_statDecisions.setData(d_minisat->decisions); - d_statRndDecisions.setData(d_minisat->rnd_decisions); - d_statPropagations.setData(d_minisat->propagations); - d_statConflicts.setData(d_minisat->conflicts); - d_statClausesLiterals.setData(d_minisat->clauses_literals); - d_statLearntsLiterals.setData(d_minisat->learnts_literals); - d_statMaxLiterals.setData(d_minisat->max_literals); - d_statTotLiterals.setData(d_minisat->tot_literals); +void MinisatSatSolver::Statistics::init(Minisat::SimpSolver* minisat){ + d_statStarts.setData(minisat->starts); + d_statDecisions.setData(minisat->decisions); + d_statRndDecisions.setData(minisat->rnd_decisions); + d_statPropagations.setData(minisat->propagations); + d_statConflicts.setData(minisat->conflicts); + d_statClausesLiterals.setData(minisat->clauses_literals); + d_statLearntsLiterals.setData(minisat->learnts_literals); + d_statMaxLiterals.setData(minisat->max_literals); + d_statTotLiterals.setData(minisat->tot_literals); } } /* namespace CVC4::prop */ diff --git a/src/smt/proof_manager.cpp b/src/smt/proof_manager.cpp index 6bdc4ced0..ce9b4923c 100644 --- a/src/smt/proof_manager.cpp +++ b/src/smt/proof_manager.cpp @@ -161,7 +161,7 @@ void PfManager::getAssertions(Assertions& as, assertions.push_back(*i); } NodeManager* nm = NodeManager::currentNM(); - for (const std::pair& dfn : df) + for (const std::pair& dfn : df) { Node def = dfn.second.getFormula(); const std::vector& formals = dfn.second.getFormals(); diff --git a/src/smt/smt_solver.h b/src/smt/smt_solver.h index e3cbea152..8b6ca3021 100644 --- a/src/smt/smt_solver.h +++ b/src/smt/smt_solver.h @@ -39,7 +39,7 @@ namespace smt { class Assertions; class SmtEngineState; class Preprocessor; -class SmtEngineStatistics; +struct SmtEngineStatistics; /** * A solver for SMT queries. diff --git a/src/theory/arith/nl/iand_utils.cpp b/src/theory/arith/nl/iand_utils.cpp index 8f0441c28..17eb518a2 100644 --- a/src/theory/arith/nl/iand_utils.cpp +++ b/src/theory/arith/nl/iand_utils.cpp @@ -228,7 +228,7 @@ void IAndUtils::addDefaultValue( { counters[i] = 0; } - for (const std::pair, uint64_t>& element : table) + for (const auto& element : table) { uint64_t result = element.second; counters[result]++; diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp index 9434a0491..dff43e568 100644 --- a/src/theory/arith/nl/nonlinear_extension.cpp +++ b/src/theory/arith/nl/nonlinear_extension.cpp @@ -38,7 +38,6 @@ NonlinearExtension::NonlinearExtension(TheoryArith& containing, eq::EqualityEngine* ee) : d_containing(containing), d_im(containing.getInferenceManager()), - d_ee(ee), d_needsLastCall(false), d_checkCounter(0), d_extTheoryCb(ee), diff --git a/src/theory/arith/nl/nonlinear_extension.h b/src/theory/arith/nl/nonlinear_extension.h index 88706350b..2de5daeb6 100644 --- a/src/theory/arith/nl/nonlinear_extension.h +++ b/src/theory/arith/nl/nonlinear_extension.h @@ -226,8 +226,6 @@ class NonlinearExtension // The theory of arithmetic containing this extension. TheoryArith& d_containing; InferenceManager& d_im; - // pointer to used equality engine - eq::EqualityEngine* d_ee; /** The statistics class */ NlStats d_stats; // needs last call effort diff --git a/src/theory/arith/nl/transcendental/transcendental_state.cpp b/src/theory/arith/nl/transcendental/transcendental_state.cpp index ba60b6a0e..6dbb847a6 100644 --- a/src/theory/arith/nl/transcendental/transcendental_state.cpp +++ b/src/theory/arith/nl/transcendental/transcendental_state.cpp @@ -23,21 +23,6 @@ namespace arith { namespace nl { namespace transcendental { -namespace { - -/** - * Ensure a is in the main phase: - * -pi <= a <= pi - */ -inline Node mkValidPhase(TNode a, TNode pi) -{ - return mkBounded( - NodeManager::currentNM()->mkNode(Kind::MULT, mkRationalNode(-1), pi), - a, - pi); -} -} // namespace - TranscendentalState::TranscendentalState(InferenceManager& im, NlModel& model) : d_im(im), d_model(model) { diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 4d4ec89b4..b13bd6926 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -1758,7 +1758,7 @@ void TheoryArrays::checkRowLemmas(TNode a, TNode b) Trace("arrays-crl")<<"Arrays::checkLemmas done.\n"; } -void TheoryArrays::propagate(RowLemmaType lem) +void TheoryArrays::propagateRowLemma(RowLemmaType lem) { Debug("pf::array") << "TheoryArrays: RowLemma Propagate called. options::arraysPropagate() = " << options::arraysPropagate() << std::endl; @@ -1845,7 +1845,7 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem) // If propagating, check propagations int prop = options::arraysPropagate(); if (prop > 0) { - propagate(lem); + propagateRowLemma(lem); } // Prefer equality between indexes so as not to introduce new read terms @@ -1975,7 +1975,7 @@ bool TheoryArrays::dischargeLemmas() int prop = options::arraysPropagate(); if (prop > 0) { - propagate(l); + propagateRowLemma(l); if (d_state.isInConflict()) { return true; diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index 5236324bc..7e4f0e36c 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -442,7 +442,7 @@ class TheoryArrays : public Theory { void checkStore(TNode a); void checkRowForIndex(TNode i, TNode a); void checkRowLemmas(TNode a, TNode b); - void propagate(RowLemmaType lem); + void propagateRowLemma(RowLemmaType lem); void queueRowLemma(RowLemmaType lem); bool dischargeLemmas(); diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h index dbee65d8c..69500fea0 100644 --- a/src/theory/bv/theory_bv_utils.h +++ b/src/theory/bv/theory_bv_utils.h @@ -142,7 +142,7 @@ Node mkAnd(const std::vector>& conjunctions) if (all.size() == 1) { return conjunctions[0]; } NodeBuilder<> conjunction(kind::AND); - for (const Node& n : all) { conjunction << n; } + for (TNode n : all) { conjunction << n; } return conjunction; } @@ -161,7 +161,7 @@ Node mkOr(const std::vector>& nodes) if (all.size() == 1) { return nodes[0]; } NodeBuilder<> disjunction(kind::OR); - for (const Node& n : all) { disjunction << n; } + for (TNode n : all) { disjunction << n; } return disjunction; } /* Create node of kind XOR. */ diff --git a/src/theory/datatypes/sygus_extension.cpp b/src/theory/datatypes/sygus_extension.cpp index fde28fd26..18b75e631 100644 --- a/src/theory/datatypes/sygus_extension.cpp +++ b/src/theory/datatypes/sygus_extension.cpp @@ -1196,7 +1196,7 @@ void SygusExtension::registerSymBreakLemma( TypeNode tn, Node lem, unsigned sz, sca.d_search_terms[tn].find(d); if (itt != sca.d_search_terms[tn].end()) { - for (const TNode& t : itt->second) + for (const Node& t : itt->second) { if (!options::sygusSymBreakLazy() || d_active_terms.find(t) != d_active_terms.end()) @@ -1469,7 +1469,7 @@ void SygusExtension::incrementCurrentSearchSize( Node m, std::vector< Node >& le int new_depth = ((int)itsz->second->d_curr_search_size) - ((int)sz); std::map< unsigned, std::vector< Node > >::iterator itt = itc->second.d_search_terms[tn].find( new_depth ); if( itt!=itc->second.d_search_terms[tn].end() ){ - for (const TNode& t : itt->second) + for (const Node& t : itt->second) { if (!options::sygusSymBreakLazy() || (d_active_terms.find(t) != d_active_terms.end() diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp index eeaa678d4..e13902077 100644 --- a/src/theory/quantifiers/conjecture_generator.cpp +++ b/src/theory/quantifiers/conjecture_generator.cpp @@ -905,7 +905,7 @@ unsigned ConjectureGenerator::flushWaitingConjectures( unsigned& addedLemmas, in d_conj_count++; }else{ std::vector< Node > bvs; - for (const std::pair& lhs_pattern : + for (const std::pair& lhs_pattern : d_pattern_var_id[lhs]) { for (unsigned j = 0; j <= lhs_pattern.second; j++) diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 20d807793..1f45fd85f 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -1114,7 +1114,7 @@ bool QuantifiersRewriter::getVarElimIneq(Node body, std::vector inactive_vars; std::map > visited; std::map exclude; - for (const std::pair& pr : qpr.d_phase_reqs) + for (const std::pair& pr : qpr.d_phase_reqs) { if (pr.first.getKind() == GEQ) { @@ -1188,7 +1188,7 @@ bool QuantifiersRewriter::getVarElimIneq(Node body, } while (!evisit.empty() && !elig_vars.empty()); bool ret = false; - for (const std::pair& ev : elig_vars) + for (const std::pair& ev : elig_vars) { Node v = ev.first; Trace("var-elim-ineq-debug") diff --git a/src/theory/quantifiers/query_generator.cpp b/src/theory/quantifiers/query_generator.cpp index 55beea4ca..f0999a5da 100644 --- a/src/theory/quantifiers/query_generator.cpp +++ b/src/theory/quantifiers/query_generator.cpp @@ -83,7 +83,7 @@ bool QueryGenerator::addTerm(Node n, std::ostream& out) } if (threshCount < 2) { - for (const std::pair>& etp : ev_to_pt) + for (const auto& etp : ev_to_pt) { if (etp.second.size() < d_deqThresh) { diff --git a/src/theory/quantifiers/sygus/enum_stream_substitution.cpp b/src/theory/quantifiers/sygus/enum_stream_substitution.cpp index 098af62a7..360476399 100644 --- a/src/theory/quantifiers/sygus/enum_stream_substitution.cpp +++ b/src/theory/quantifiers/sygus/enum_stream_substitution.cpp @@ -88,7 +88,7 @@ void EnumStreamPermutation::reset(Node value) d_var_classes[ti.getSubclassForVar(var)].push_back(var); } } - for (const std::pair>& p : d_var_classes) + for (const std::pair>& p : d_var_classes) { d_perm_state_class.push_back(PermutationState(p.second)); if (Trace.isOn("synth-stream-concrete")) @@ -383,7 +383,7 @@ void EnumStreamSubstitution::resetValue(Node value) d_curr_ind = 0; d_comb_state_class.clear(); Trace("synth-stream-concrete") << " ..combining vars :"; - for (const std::pair>& p : d_var_classes) + for (const std::pair>& p : d_var_classes) { // ignore classes without variables being permuted unsigned perm_var_class_sz = d_stream_permutations.getVarClassSize(p.first); diff --git a/src/theory/quantifiers/sygus_sampler.cpp b/src/theory/quantifiers/sygus_sampler.cpp index 92754ebfe..62eef124a 100644 --- a/src/theory/quantifiers/sygus_sampler.cpp +++ b/src/theory/quantifiers/sygus_sampler.cpp @@ -126,7 +126,7 @@ void SygusSampler::initializeSygus(TermDbSygus* tds, { TypeNode svt = sv.getType(); // is it equivalent to a previous variable? - for (const std::pair& v : var_to_type_id) + for (const auto& v : var_to_type_id) { Node svc = v.first; if (svc.getType() == svt) diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 42677fa3f..f91cda36b 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -276,14 +276,14 @@ void TermDb::computeUfEqcTerms( TNode f ) { ops.insert(ops.end(), d_ho_op_slaves[f].begin(), d_ho_op_slaves[f].end()); } eq::EqualityEngine* ee = d_quantEngine->getMasterEqualityEngine(); - for (const Node& ff : ops) + for (TNode ff : ops) { - for (const TNode& n : d_op_map[ff]) + for (const Node& n : d_op_map[ff]) { if (hasTermCurrent(n) && isTermActive(n)) { computeArgReps(n); - TNode r = ee->hasTerm(n) ? ee->getRepresentative(n) : n; + TNode r = ee->hasTerm(n) ? ee->getRepresentative(n) : TNode(n); d_func_map_eqc_trie[f].d_data[r].addTerm(n, d_arg_reps[n]); } } @@ -312,7 +312,7 @@ void TermDb::computeUfTerms( TNode f ) { unsigned relevantCount = 0; eq::EqualityEngine* ee = d_quantEngine->getMasterEqualityEngine(); NodeManager* nm = NodeManager::currentNM(); - for (const Node& ff : ops) + for (TNode ff : ops) { std::map >::iterator it = d_op_map.find(ff); if (it == d_op_map.end()) diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp index d03cc8570..d9d9415fc 100644 --- a/src/theory/sep/theory_sep.cpp +++ b/src/theory/sep/theory_sep.cpp @@ -755,7 +755,7 @@ void TheorySep::postCheck(Effort level) // get model values std::map mvals; - for (const std::pair& sub_element : d_label_map[satom][slbl]) + for (const std::pair& sub_element : d_label_map[satom][slbl]) { int sub_index = sub_element.first; Node sub_lbl = sub_element.second; diff --git a/src/theory/sets/cardinality_extension.cpp b/src/theory/sets/cardinality_extension.cpp index cb0540b86..5997d1217 100644 --- a/src/theory/sets/cardinality_extension.cpp +++ b/src/theory/sets/cardinality_extension.cpp @@ -165,7 +165,7 @@ void CardinalityExtension::checkCardinalityExtended(TypeNode& t) const std::map& negativeMembers = d_state.getNegativeMembers(representative); - for (const std::pair& negativeMember : negativeMembers) + for (const auto& negativeMember : negativeMembers) { Node member = nm->mkNode(MEMBER, negativeMember.first, univ); // negativeMember.second is the reason for the negative membership and diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index e44c3c7a6..4390b3e6e 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -1163,7 +1163,7 @@ bool TheorySetsPrivate::collectModelValues(TheoryModel* m, { const std::map >& slackElements = d_cardSolver->getFiniteTypeSlackElements(); - for (const std::pair >& pair : slackElements) + for (const auto& pair : slackElements) { const std::vector& members = d_cardSolver->getFiniteTypeMembers(pair.first); diff --git a/src/theory/strings/core_solver.cpp b/src/theory/strings/core_solver.cpp index edd00c954..48116bc24 100644 --- a/src/theory/strings/core_solver.cpp +++ b/src/theory/strings/core_solver.cpp @@ -2575,7 +2575,7 @@ bool CoreSolver::processInferInfo(CoreInferInfo& cii) addNormalFormPair(cii.d_nfPair[0], cii.d_nfPair[1]); } // send phase requirements - for (const std::pair pp : cii.d_pendingPhase) + for (const std::pair& pp : cii.d_pendingPhase) { Node ppr = Rewriter::rewrite(pp.first); d_im.addPendingPhaseRequirement(ppr, pp.second); diff --git a/src/theory/strings/normal_form.cpp b/src/theory/strings/normal_form.cpp index 7724b5137..5beaa4a00 100644 --- a/src/theory/strings/normal_form.cpp +++ b/src/theory/strings/normal_form.cpp @@ -61,9 +61,9 @@ void NormalForm::splitConstant(unsigned index, Node c1, Node c2) // notice this is not critical for soundness: not doing the below incrementing // will only lead to overapproximating when antecedants are required in // explanations - for (const std::pair >& pe : d_expDep) + for (const std::pair >& pe : d_expDep) { - for (const std::pair& pep : pe.second) + for (const auto& pep : pe.second) { // See if this can be incremented: it can if this literal is not relevant // to the current index, and hence it is not relevant for both c1 and c2. diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index c8812b160..7b38bd844 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -1823,7 +1823,7 @@ theory::TrustNode TheoryEngine::getExplanation( if (Trace.isOn("te-proof-exp")) { Trace("te-proof-exp") << "Explanation is:" << std::endl; - for (const Node& e : exp) + for (TNode e : exp) { Trace("te-proof-exp") << " " << e << std::endl; } diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp index f04ebbb60..2173c6922 100644 --- a/src/theory/uf/equality_engine.cpp +++ b/src/theory/uf/equality_engine.cpp @@ -1286,7 +1286,7 @@ void EqualityEngine::explainLit(TNode lit, std::vector& assumptions) explainPredicate(atom, polarity, tassumptions); } // ensure that duplicates are removed - for (const TNode a : tassumptions) + for (TNode a : tassumptions) { if (std::find(assumptions.begin(), assumptions.end(), a) == assumptions.end()) diff --git a/src/theory/uf/proof_equality_engine.cpp b/src/theory/uf/proof_equality_engine.cpp index 6377f78b6..f04bc5ec1 100644 --- a/src/theory/uf/proof_equality_engine.cpp +++ b/src/theory/uf/proof_equality_engine.cpp @@ -518,7 +518,7 @@ void ProofEqEngine::explainWithProof(Node lit, } Trace("pfee-proof") << "...got " << tassumps << std::endl; // avoid duplicates - for (const TNode a : tassumps) + for (TNode a : tassumps) { if (a == lit) { diff --git a/src/theory/uf/symmetry_breaker.cpp b/src/theory/uf/symmetry_breaker.cpp index c4d6c9c82..2e0a9adf5 100644 --- a/src/theory/uf/symmetry_breaker.cpp +++ b/src/theory/uf/symmetry_breaker.cpp @@ -594,7 +594,7 @@ bool SymmetryBreaker::invariantByPermutations(const Permutation& p) { subs.push_back(p1); repls.push_back(p1); repls.push_back(p0); - for (const Node nn : d_phi) + for (const Node& nn : d_phi) { Node s = nn.substitute(subs.begin(), subs.end(), repls.begin(), repls.end()); @@ -629,7 +629,7 @@ bool SymmetryBreaker::invariantByPermutations(const Permutation& p) { subs.clear(); repls.clear(); bool first = true; - for (const Node& nn : p) + for (TNode nn : p) { subs.push_back(nn); if(!first) { -- 2.30.2