Merge branch 'master' into cleanup-regexp

3 files changed, 9 insertions, 75 deletions

diff --git a/src/theory/arith/normal_form.cpp b/src/theory/arith/normal_form.cpp
index ef22e1c0d..30b9ca0b5 100644
--- a/src/theory/arith/normal_form.cpp
+++ b/src/theory/arith/normal_form.cpp
@@ -105,11 +105,7 @@ bool Variable::isTranscendentalMember(Node n) {
 
 
 bool VarList::isSorted(iterator start, iterator end) {
-#if IS_SORTED_IN_GNUCXX_NAMESPACE
-  return __gnu_cxx::is_sorted(start, end);
-#else /* IS_SORTED_IN_GNUCXX_NAMESPACE */
   return std::is_sorted(start, end);
-#endif /* IS_SORTED_IN_GNUCXX_NAMESPACE */
 }
 
 bool VarList::isMember(Node n) {
@@ -198,8 +194,7 @@ VarList VarList::operator*(const VarList& other) const {
       otherEnd = other.internalEnd();
 
     Variable::VariableNodeCmp cmp;
-
-    merge_ranges(thisBegin, thisEnd, otherBegin, otherEnd, result, cmp);
+    std::merge(thisBegin, thisEnd, otherBegin, otherEnd, std::back_inserter(result), cmp);
 
     Assert(result.size() >= 2);
     Node mult = NodeManager::currentNM()->mkNode(kind::NONLINEAR_MULT, result);
@@ -356,7 +351,7 @@ void Monomial::printList(const std::vector<Monomial>& list) {
 Polynomial Polynomial::operator+(const Polynomial& vl) const {
 
   std::vector<Monomial> sortedMonos;
-  merge_ranges(begin(), end(), vl.begin(), vl.end(), sortedMonos);
+  std::merge(begin(), end(), vl.begin(), vl.end(), std::back_inserter(sortedMonos));
 
   Monomial::combineAdjacentMonomials(sortedMonos);
   //std::vector<Monomial> combined = Monomial::sumLikeTerms(sortedMonos);
diff --git a/src/theory/arith/normal_form.h b/src/theory/arith/normal_form.h
index d8f5259fc..21301da91 100644
--- a/src/theory/arith/normal_form.h
+++ b/src/theory/arith/normal_form.h
@@ -23,10 +23,6 @@
 #include <algorithm>
 #include <list>
 
-#if IS_SORTED_IN_GNUCXX_NAMESPACE
-#  include <ext/algorithm>
-#endif /* IS_SORTED_IN_GNUCXX_NAMESPACE */
-
 #include "base/output.h"
 #include "expr/node.h"
 #include "expr/node_self_iterator.h"
@@ -284,7 +280,7 @@ public:
   }
 
   struct VariableNodeCmp {
-    static inline int cmp(Node n, Node m) {
+    static inline int cmp(const Node& n, const Node& m) {
       if ( n == m ) { return 0; }
 
       // this is now slightly off of the old variable order.
@@ -320,7 +316,7 @@ public:
       }
     }
 
-    bool operator()(Node n, Node m) const {
+    bool operator()(const Node& n, const Node& m) const {
       return VariableNodeCmp::cmp(n,m) < 0;
     }
   };
@@ -431,56 +427,6 @@ inline Node makeNode(Kind k, GetNodeIterator start, GetNodeIterator end) {
   return Node(nb);
 }/* makeNode<GetNodeIterator>(Kind, iterator, iterator) */
 
-
-template <class GetNodeIterator, class T>
-static void copy_range(GetNodeIterator begin, GetNodeIterator end, std::vector<T>& result){
-  while(begin != end){
-    result.push_back(*begin);
-    ++begin;
-  }
-}
-
-template <class GetNodeIterator, class T>
-static void merge_ranges(GetNodeIterator first1,
-                  GetNodeIterator last1,
-                  GetNodeIterator first2,
-                  GetNodeIterator last2,
-                  std::vector<T>& result) {
-
-  while(first1 != last1 && first2 != last2){
-    if( (*first1) < (*first2) ){
-      result.push_back(*first1);
-      ++ first1;
-    }else{
-      result.push_back(*first2);
-      ++ first2;
-    }
-  }
-  copy_range(first1, last1, result);
-  copy_range(first2, last2, result);
-}
-
-template <class GetNodeIterator, class T, class Cmp>
-static void merge_ranges(GetNodeIterator first1,
-                         GetNodeIterator last1,
-                         GetNodeIterator first2,
-                         GetNodeIterator last2,
-                         std::vector<T>& result,
-                         const Cmp& cmp) {
-
-  while(first1 != last1 && first2 != last2){
-    if( cmp(*first1, *first2) ){
-      result.push_back(*first1);
-      ++ first1;
-    }else{
-      result.push_back(*first2);
-      ++ first2;
-    }
-  }
-  copy_range(first1, last1, result);
-  copy_range(first2, last2, result);
-}
-
 /**
  * A VarList is a sorted list of variables representing a product.
  * If the VarList is empty, it represents an empty product or 1.
@@ -749,11 +695,7 @@ public:
   }
 
   static bool isSorted(const std::vector<Monomial>& m) {
-#if IS_SORTED_IN_GNUCXX_NAMESPACE
-    return __gnu_cxx::is_sorted(m.begin(), m.end());
-#else /* IS_SORTED_IN_GNUCXX_NAMESPACE */
     return std::is_sorted(m.begin(), m.end());
-#endif /* IS_SORTED_IN_GNUCXX_NAMESPACE */
   }
 
   static bool isStrictlySorted(const std::vector<Monomial>& m) {
@@ -852,7 +794,7 @@ private:
 public:
   static bool isMember(TNode n);
 
-  class iterator {
+  class iterator : public std::iterator<std::input_iterator_tag, Monomial> {
   private:
     internal_iterator d_iter;
 
@@ -954,7 +896,7 @@ public:
     iterator tailStart = begin();
     ++tailStart;
     std::vector<Monomial> subrange;
-    copy_range(tailStart, end(), subrange);
+    std::copy(tailStart, end(), std::back_inserter(subrange));
     return mkPolynomial(subrange);
   }
 
diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index f70db9823..a2a56e137 100644
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -17,8 +17,6 @@
 #include <algorithm>
 #include "theory/sets/theory_sets_private.h"
 
-#include <boost/foreach.hpp>
-
 #include "expr/emptyset.h"
 #include "options/sets_options.h"
 #include "smt/smt_statistics_registry.h"
@@ -56,7 +54,7 @@ TheorySetsPrivate::TheorySetsPrivate(TheorySets& external,
 {
 
   d_rels = new TheorySetsRels(c, u, &d_equalityEngine, &d_conflict, external);
-  
+
   d_true = NodeManager::currentNM()->mkConst( true );
   d_false = NodeManager::currentNM()->mkConst( false );
   d_zero = NodeManager::currentNM()->mkConst( Rational(0) );
@@ -79,9 +77,8 @@ TheorySetsPrivate::TheorySetsPrivate(TheorySets& external,
 
 TheorySetsPrivate::~TheorySetsPrivate(){
   delete d_rels;
-  for(std::map< Node, EqcInfo* >::iterator i = d_eqc_info.begin(), iend = d_eqc_info.end(); i != iend; ++i){
-    EqcInfo* current = (*i).second;
-    delete current;
+  for (std::pair<const Node, EqcInfo*>& current_pair : d_eqc_info) {
+    delete current_pair.second;
   }
 }/* TheorySetsPrivate::~TheorySetsPrivate() */