diff options
| -rw-r--r-- | config/is_sorted.m4 | 20 | ||||
| -rw-r--r-- | configure.ac | 3 | ||||
| -rw-r--r-- | src/theory/arith/normal_form.cpp | 4 | ||||
| -rw-r--r-- | src/theory/arith/normal_form.h | 8 |
4 files changed, 35 insertions, 0 deletions
diff --git a/config/is_sorted.m4 b/config/is_sorted.m4 new file mode 100644 index 000000000..52b062d7e --- /dev/null +++ b/config/is_sorted.m4 @@ -0,0 +1,20 @@ +# 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 e30c12a6f..629e1625b 100644 --- a/configure.ac +++ b/configure.ac @@ -1002,6 +1002,9 @@ 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/theory/arith/normal_form.cpp b/src/theory/arith/normal_form.cpp index ce0bd9d30..5334abbbf 100644 --- a/src/theory/arith/normal_form.cpp +++ b/src/theory/arith/normal_form.cpp @@ -90,7 +90,11 @@ bool Variable::isDivMember(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) { diff --git a/src/theory/arith/normal_form.h b/src/theory/arith/normal_form.h index 8d37bed23..1a3327e8f 100644 --- a/src/theory/arith/normal_form.h +++ b/src/theory/arith/normal_form.h @@ -29,6 +29,10 @@ #include <list> #include <algorithm> +#if IS_SORTED_IN_GNUCXX_NAMESPACE +# include <ext/algorithm> +#endif /* IS_SORTED_IN_GNUCXX_NAMESPACE */ + namespace CVC4 { namespace theory { namespace arith { @@ -731,7 +735,11 @@ 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) { |