From: Piotr Trojanek Date: Thu, 22 Aug 2019 21:22:51 +0000 (+0200) Subject: prefer prefix ++ operator for iterators X-Git-Tag: cvc5-1.0.0~3905 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e7929d2cd241d8b4974d26b9e11f1378ba30b0e7;p=cvc5.git prefer prefix ++ operator for iterators Detected with cppcheck static analyser, which said: (performance) Prefer prefix ++/-- operators for non-primitive types. Reformat with clang-format as needed. Signed-off-by: Piotr Trojanek --- diff --git a/src/theory/arith/arith_ite_utils.cpp b/src/theory/arith/arith_ite_utils.cpp index 3980b41b8..454d6c11f 100644 --- a/src/theory/arith/arith_ite_utils.cpp +++ b/src/theory/arith/arith_ite_utils.cpp @@ -374,7 +374,8 @@ Node ArithIteUtils::findIteCnd(TNode tb, TNode fb) const{ // (not y) => (not x) // (not z) => x std::set::const_iterator ci = negtimp.begin(), cend = negtimp.end(); - for(; ci != cend; ci++){ + for (; ci != cend; ++ci) + { Node impliedByNotTB = *ci; Node impliedByNotTBNeg = impliedByNotTB.negate(); if(negfimp.find(impliedByNotTBNeg) != negfimp.end()){ diff --git a/src/theory/arrays/array_info.cpp b/src/theory/arrays/array_info.cpp index e92947c7f..0d1095a23 100644 --- a/src/theory/arrays/array_info.cpp +++ b/src/theory/arrays/array_info.cpp @@ -68,7 +68,8 @@ ArrayInfo::ArrayInfo(context::Context* c, Backtracker* b, std::string sta ArrayInfo::~ArrayInfo() { CNodeInfoMap::iterator it = info_map.begin(); - for( ; it != info_map.end(); it++ ) { + for (; it != info_map.end(); ++it) + { if((*it).second!= emptyInfo) { delete (*it).second; } @@ -87,7 +88,8 @@ ArrayInfo::~ArrayInfo() { bool inList(const CTNodeList* l, const TNode el) { CTNodeList::const_iterator it = l->begin(); - for ( ; it!= l->end(); it ++) { + for (; it != l->end(); ++it) + { if(*it == el) return true; } @@ -97,7 +99,8 @@ bool inList(const CTNodeList* l, const TNode el) { void printList (CTNodeList* list) { CTNodeList::const_iterator it = list->begin(); Trace("arrays-info")<<" [ "; - for(; it != list->end(); it++ ) { + for (; it != list->end(); ++it) + { Trace("arrays-info")<<(*it)<<" "; } Trace("arrays-info")<<"] \n"; @@ -106,7 +109,8 @@ void printList (CTNodeList* list) { void printList (List* list) { List::const_iterator it = list->begin(); Trace("arrays-info")<<" [ "; - for(; it != list->end(); it++ ) { + for (; it != list->end(); ++it) + { Trace("arrays-info")<<(*it)<<" "; } Trace("arrays-info")<<"] \n"; @@ -115,11 +119,13 @@ void printList (List* list) { void ArrayInfo::mergeLists(CTNodeList* la, const CTNodeList* lb) const{ std::set temp; CTNodeList::const_iterator it; - for(it = la->begin() ; it != la->end(); it++ ) { + for (it = la->begin(); it != la->end(); ++it) + { temp.insert((*it)); } - for(it = lb->begin() ; it!= lb->end(); it++ ) { + for (it = lb->begin(); it != lb->end(); ++it) + { if(temp.count(*it) == 0) { la->push_back(*it); } diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp index 63736b53c..c52666dad 100644 --- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp @@ -1053,10 +1053,16 @@ bool CegInstantiator::constructInstantiationInc(Node pv, }else{ Trace("cbqi-inst-debug2") << "Revert substitutions..." << std::endl; //revert substitution information - for( std::map< int, Node >::iterator it = prev_subs.begin(); it != prev_subs.end(); it++ ){ + for (std::map::iterator it = prev_subs.begin(); + it != prev_subs.end(); + ++it) + { sf.d_subs[it->first] = it->second; } - for( std::map< int, TermProperties >::iterator it = prev_prop.begin(); it != prev_prop.end(); it++ ){ + for (std::map::iterator it = prev_prop.begin(); + it != prev_prop.end(); + ++it) + { sf.d_props[it->first] = it->second; } for( unsigned i=0; i::iterator set_it = itec->second.begin(); set_it != itec->second.end(); - set_it++) + ++set_it) { if (std::find(consts.begin(), consts.end(), *set_it) == consts.end()) { diff --git a/src/theory/sets/theory_sets_rels.cpp b/src/theory/sets/theory_sets_rels.cpp index e2b779cbd..382cb671b 100644 --- a/src/theory/sets/theory_sets_rels.cpp +++ b/src/theory/sets/theory_sets_rels.cpp @@ -119,7 +119,7 @@ void TheorySetsRels::check(Theory::Effort level) } } } - m_it++; + ++m_it; } TERM_IT t_it = d_terms_cache.begin(); @@ -133,37 +133,37 @@ void TheorySetsRels::check(Theory::Effort level) std::vector::iterator term_it = k_t_it->second.begin(); while(term_it != k_t_it->second.end()) { computeMembersForBinOpRel( *term_it ); - term_it++; + ++term_it; } } else if( k_t_it->first == kind::TRANSPOSE ) { std::vector::iterator term_it = k_t_it->second.begin(); while( term_it != k_t_it->second.end() ) { computeMembersForUnaryOpRel( *term_it ); - term_it++; + ++term_it; } } else if ( k_t_it->first == kind::TCLOSURE ) { std::vector::iterator term_it = k_t_it->second.begin(); while( term_it != k_t_it->second.end() ) { buildTCGraphForRel( *term_it ); - term_it++; + ++term_it; } } else if( k_t_it->first == kind::JOIN_IMAGE ) { std::vector::iterator term_it = k_t_it->second.begin(); while( term_it != k_t_it->second.end() ) { computeMembersForJoinImageTerm( *term_it ); - term_it++; + ++term_it; } } else if( k_t_it->first == kind::IDEN ) { std::vector::iterator term_it = k_t_it->second.begin(); while( term_it != k_t_it->second.end() ) { computeMembersForIdenTerm( *term_it ); - term_it++; + ++term_it; } } - k_t_it++; + ++k_t_it; } } - t_it++; + ++t_it; } doTCInference(); @@ -604,7 +604,7 @@ void TheorySetsRels::check(Theory::Effort level) if( hasSeen.find(*set_it) == hasSeen.end() ) { isTCReachable( *set_it, dest, hasSeen, tc_graph, isReachable ); } - set_it++; + ++set_it; } } } @@ -645,9 +645,15 @@ void TheorySetsRels::check(Theory::Effort level) void TheorySetsRels::doTCInference( std::map< Node, std::unordered_set > rel_tc_graph, std::map< Node, Node > rel_tc_graph_exps, Node tc_rel ) { Trace("rels-debug") << "[Theory::Rels] ****** doTCInference !" << std::endl; - for( TC_GRAPH_IT tc_graph_it = rel_tc_graph.begin(); tc_graph_it != rel_tc_graph.end(); tc_graph_it++ ) { - for( std::unordered_set< Node, NodeHashFunction >::iterator snd_elements_it = tc_graph_it->second.begin(); - snd_elements_it != tc_graph_it->second.end(); snd_elements_it++ ) { + for (TC_GRAPH_IT tc_graph_it = rel_tc_graph.begin(); + tc_graph_it != rel_tc_graph.end(); + ++tc_graph_it) + { + for (std::unordered_set::iterator + snd_elements_it = tc_graph_it->second.begin(); + snd_elements_it != tc_graph_it->second.end(); + ++snd_elements_it) + { std::vector< Node > reasons; std::unordered_set seen; Node tuple = RelsUtils::constructPair( tc_rel, getRepresentative( tc_graph_it->first ), getRepresentative( *snd_elements_it) ); @@ -698,8 +704,11 @@ void TheorySetsRels::check(Theory::Effort level) seen.insert( cur_node_rep ); TC_GRAPH_IT cur_set = tc_graph.find( cur_node_rep ); if( cur_set != tc_graph.end() ) { - for( std::unordered_set< Node, NodeHashFunction >::iterator set_it = cur_set->second.begin(); - set_it != cur_set->second.end(); set_it++ ) { + for (std::unordered_set::iterator set_it = + cur_set->second.begin(); + set_it != cur_set->second.end(); + ++set_it) + { Node new_pair = RelsUtils::constructPair( tc_rel, cur_node_rep, *set_it ); std::vector< Node > new_reasons( reasons ); new_reasons.push_back( rel_tc_graph_exps.find( new_pair )->second ); @@ -889,7 +898,7 @@ void TheorySetsRels::check(Theory::Effort level) while( tc_graph_it != d_tcr_tcGraph.end() ) { Assert ( d_tcr_tcGraph_exps.find(tc_graph_it->first) != d_tcr_tcGraph_exps.end() ); doTCInference( tc_graph_it->second, d_tcr_tcGraph_exps.find(tc_graph_it->first)->second, tc_graph_it->first ); - tc_graph_it++; + ++tc_graph_it; } Trace("rels-debug") << "[Theory::Rels] ****** Done with finalizing transitive closure inferences!" << std::endl; } @@ -1114,7 +1123,6 @@ void TheorySetsRels::check(Theory::Effort level) } bool TheorySetsRels::hasTerm(Node a) { return d_ee.hasTerm(a); } - bool TheorySetsRels::areEqual( Node a, Node b ){ Assert(a.getType() == b.getType()); Trace("rels-eq") << "[sets-rels]**** checking equality between " << a << " and " << b << std::endl; @@ -1151,7 +1159,7 @@ void TheorySetsRels::check(Theory::Effort level) if(areEqual(*mems, member)) { return false; } - mems++; + ++mems; } map[rel_rep].push_back(member); return true; @@ -1216,7 +1224,7 @@ void TheorySetsRels::check(Theory::Effort level) it = d_data.begin(); while(it != d_data.end()) { nodes.push_back(it->first); - it++; + ++it; } } return nodes; @@ -1238,7 +1246,7 @@ void TheorySetsRels::check(Theory::Effort level) it = d_data.begin(); while(it != d_data.end()) { nodes.push_back(it->first); - it++; + ++it; } return nodes; }else{ diff --git a/src/theory/sets/theory_sets_rewriter.cpp b/src/theory/sets/theory_sets_rewriter.cpp index 15cec0856..5d654e7d5 100644 --- a/src/theory/sets/theory_sets_rewriter.cpp +++ b/src/theory/sets/theory_sets_rewriter.cpp @@ -248,7 +248,7 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) { while(tuple_it != tuple_set.end()) { new_tuple_set.insert(RelsUtils::reverseTuple(*tuple_it)); - tuple_it++; + ++tuple_it; } Node new_node = NormalForm::elementsToSet(new_tuple_set, node.getType()); Assert(new_node.isConst()); @@ -296,9 +296,9 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) { new_tuple.insert(new_tuple.end(), right_tuple.begin(), right_tuple.end()); Node composed_tuple = NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, new_tuple); new_tuple_set.insert(composed_tuple); - right_it++; + ++right_it; } - left_it++; + ++left_it; } Node new_node = NormalForm::elementsToSet(new_tuple_set, node.getType()); Assert(new_node.isConst()); @@ -340,9 +340,9 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) { Node composed_tuple = NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, new_tuple); new_tuple_set.insert(composed_tuple); } - right_it++; + ++right_it; } - left_it++; + ++left_it; } Node new_node = NormalForm::elementsToSet(new_tuple_set, node.getType()); Assert(new_node.isConst()); diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp index eaf016862..d2505f4f4 100644 --- a/src/theory/strings/regexp_operation.cpp +++ b/src/theory/strings/regexp_operation.cpp @@ -782,7 +782,7 @@ void RegExpOpr::firstChars(Node r, std::set &pcset, SetNodes &pvset) Trace("regexp-fset") << "END FSET(" << mkString(r) << ") = {"; for (std::set::const_iterator itr = pcset.begin(); itr != pcset.end(); - itr++) + ++itr) { if (itr != pcset.begin()) { @@ -1406,7 +1406,7 @@ Node RegExpOpr::intersectInternal( Node r1, Node r2, std::map< PairNodes, Node > Trace("regexp-int-debug") << "Try CSET(" << cset.size() << ") = {"; for (std::vector::const_iterator itr = cset.begin(); itr != cset.end(); - itr++) + ++itr) { //CVC4::String c( *itr ); if(itr != cset.begin()) { @@ -1419,7 +1419,7 @@ Node RegExpOpr::intersectInternal( Node r1, Node r2, std::map< PairNodes, Node > std::map< PairNodes, Node > cacheX; for (std::vector::const_iterator itr = cset.begin(); itr != cset.end(); - itr++) + ++itr) { std::vector cvec; cvec.push_back(String::convertCodeToUnsignedInt(*itr));