summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--config/is_sorted.m420
-rw-r--r--configure.ac3
-rw-r--r--src/expr/node_self_iterator.h2
-rw-r--r--src/theory/arith/normal_form.cpp9
-rw-r--r--src/theory/arith/normal_form.h66
5 files changed, 7 insertions, 93 deletions
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 <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 b321fef6b..c0cec382f 100644
--- 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 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);
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback