Use is_sorted, merge, copy from std (#199)

Previously, we were checking whether we should use is_sorted
from std or __gnu_cxx. With C++11, std::is_sorted is
guaranteed to exist. This commit changes
arith/normal_form.{h,cpp} to always use std::is_sorted and
also removes the custom implementations for merge and copy by
using the std implementations instead.

3 files changed, 7 insertions, 70 deletions

diff --git a/src/expr/node_self_iterator.h b/src/expr/node_self_iterator.h
index 8cccd9bfe..6d655e1fe 100644
--- a/src/expr/node_self_iterator.h
+++ b/src/expr/node_self_iterator.h
@@ -27,7 +27,7 @@
 namespace CVC4 {
 namespace expr {
 
-class NodeSelfIterator : std::iterator<std::input_iterator_tag, Node> {
+class NodeSelfIterator : public std::iterator<std::input_iterator_tag, Node> {
   Node d_node;
   Node::const_iterator d_child;
 
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);
   }