From: Andres Noetzli Date: Mon, 17 Jul 2017 12:07:59 +0000 (-0400) Subject: Use is_sorted, merge, copy from std (#199) X-Git-Tag: cvc5-1.0.0~5715 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=53a226a753e509e028c386072c87d94c0a1316be;p=cvc5.git 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 index 52b062d7e..000000000 --- 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 ], - [std::is_sorted((int*)0L, (int*)0L);])], - [is_sorted_result=std], - [AC_COMPILE_IFELSE([AC_LANG_PROGRAM([#include ], - [__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 b321fef6b..c0cec382f 100644 --- a/configure.ac +++ b/configure.ac @@ -1073,9 +1073,6 @@ AC_CHECK_DECLS([optreset], [], [], [#include ]) # 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 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 { +class NodeSelfIterator : public std::iterator { 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& list) { Polynomial Polynomial::operator+(const Polynomial& vl) const { std::vector 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 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 #include -#if IS_SORTED_IN_GNUCXX_NAMESPACE -# include -#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(Kind, iterator, iterator) */ - -template -static void copy_range(GetNodeIterator begin, GetNodeIterator end, std::vector& result){ - while(begin != end){ - result.push_back(*begin); - ++begin; - } -} - -template -static void merge_ranges(GetNodeIterator first1, - GetNodeIterator last1, - GetNodeIterator first2, - GetNodeIterator last2, - std::vector& 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 -static void merge_ranges(GetNodeIterator first1, - GetNodeIterator last1, - GetNodeIterator first2, - GetNodeIterator last2, - std::vector& 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& 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& m) { @@ -852,7 +794,7 @@ private: public: static bool isMember(TNode n); - class iterator { + class iterator : public std::iterator { private: internal_iterator d_iter; @@ -954,7 +896,7 @@ public: iterator tailStart = begin(); ++tailStart; std::vector subrange; - copy_range(tailStart, end(), subrange); + std::copy(tailStart, end(), std::back_inserter(subrange)); return mkPolynomial(subrange); }