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 <piotr.trojanek@gmail.com>

7 files changed, 58 insertions, 37 deletions

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<Node>::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<TNode>* 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<TNode>* list) {
   List<TNode>::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<TNode>* list) {
 void ArrayInfo::mergeLists(CTNodeList* la, const CTNodeList* lb) const{
   std::set<TNode> 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<int, Node>::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<int, TermProperties>::iterator it = prev_prop.begin();
+           it != prev_prop.end();
+           ++it)
+      {
         sf.d_props[it->first] = it->second;
       }
       for( unsigned i=0; i<new_non_basic.size(); i++ ){
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
index e7f447ca1..31131f23f 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
@@ -541,7 +541,7 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
       for (std::unordered_set<Node, NodeHashFunction>::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<Node>::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<Node>::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<Node>::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<Node>::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<Node>::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<Node, NodeHashFunction> > 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<Node, NodeHashFunction>::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<Node, NodeHashFunction> 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<Node, NodeHashFunction>::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<unsigned> &pcset, SetNodes &pvset)
     Trace("regexp-fset") << "END FSET(" << mkString(r) << ") = {";
     for (std::set<unsigned>::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<unsigned>::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<unsigned>::const_iterator itr = cset.begin();
              itr != cset.end();
-             itr++)
+             ++itr)
         {
           std::vector<unsigned> cvec;
           cvec.push_back(String::convertCodeToUnsignedInt(*itr));