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.

diff --git a/config/is_sorted.m4 b/config/is_sorted.m4
deleted file mode 100644 (file)
index 52b062d..0000000
--- a/config/is_sorted.m4
+++ /dev/null
@@ -1,20 +0,0 @@
-# CHECK_FOR_IS_SORTED
-# -------------------
-# Look for is_sorted in std:: and __gnu_cxx:: and define
-# some things to make it easy to find later.
-AC_DEFUN([CHECK_FOR_IS_SORTED], [
-AC_MSG_CHECKING([where we can find is_sorted])
-AC_LANG_PUSH([C++])
-is_sorted_result=
-AC_COMPILE_IFELSE([AC_LANG_PROGRAM([#include <algorithm>],
-                                   [std::is_sorted((int*)0L, (int*)0L);])],
-  [is_sorted_result=std],
-  [AC_COMPILE_IFELSE([AC_LANG_PROGRAM([#include <ext/algorithm>],
-                                      [__gnu_cxx::is_sorted((int*)0L, (int*)0L);])],
-    [is_sorted_result=__gnu_cxx],
-    [AC_MSG_FAILURE([cannot find std::is_sorted() or __gnu_cxx::is_sorted()])])])
-AC_LANG_POP([C++])
-AC_MSG_RESULT($is_sorted_result)
-if test "$is_sorted_result" = __gnu_cxx; then is_sorted_result=1; else is_sorted_result=0; fi
-AC_DEFINE_UNQUOTED([IS_SORTED_IN_GNUCXX_NAMESPACE], $is_sorted_result, [Define to 1 if __gnu_cxx::is_sorted() exists])
-])# CHECK_FOR_IS_SORTED

diff --git a/configure.ac b/configure.ac
index b321fef6b2d01ae3eeec6631e742a5db547829ab..c0cec382fabf9f214c41b80ed54302992894429e 100644 (file)
--- a/configure.ac
+++ b/configure.ac
@@ -1073,9 +1073,6 @@ AC_CHECK_DECLS([optreset], [], [], [#include <getopt.h>])
 # check with which standard strerror_r() complies
 AC_FUNC_STRERROR_R
 
-# is is_sorted() in std or __gnu_cxx?
-CHECK_FOR_IS_SORTED
-
 # require boost library
 BOOST_REQUIRE()
 

diff --git a/src/expr/node_self_iterator.h b/src/expr/node_self_iterator.h
index 8cccd9bfe625291ae17a1e3ee01c6f420195ee4a..6d655e1fe5b49ea5d54a3f75f08f4ca7ccb117cc 100644 (file)
--- 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 ef22e1c0d648f8b506a2c293c45a11fca86162d4..30b9ca0b5d8e7e56e51059363ce516ed7673846b 100644 (file)
--- 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 d8f5259fc631b6dd1159ba833034c55e8cab6e05..21301da91844a891193ed5be74de02d579fddb8e 100644 (file)
--- 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);
   }