Switch to C++17. (#5959)

Co-authored-by: Gereon Kremer <nafur42@gmail.com>

diff --git a/CMakeLists.txt b/CMakeLists.txt
index 4a90afa8bda2e9801c56e9a1e7d67edd43580954..3dd282a8de6ec5e313e06485e41ed37d0c57b5ba 100644 (file)
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -37,8 +37,9 @@ endif()
 
 set(CMAKE_MODULE_PATH ${PROJECT_SOURCE_DIR}/cmake)
 set(CMAKE_C_STANDARD 99)
-set(CMAKE_CXX_STANDARD 11)
+set(CMAKE_CXX_STANDARD 17)
 set(CMAKE_CXX_EXTENSIONS OFF)
+set(CMAKE_CXX_STANDARD_REQUIRED ON)
 
 # Generate compile_commands.json, which can be used for various code completion
 # plugins.

diff --git a/src/expr/node.h b/src/expr/node.h
index 75d4d2022da18d2fe73326cd8028c563a898f6e3..559ce5ddbb858eb3a50104642d6c4ab56f11ebd4 100644 (file)
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -1451,8 +1451,10 @@ NodeTemplate<ref_count>::substitute(Iterator substitutionsBegin,
   }
 
   // otherwise compute
-  Iterator j = find_if(substitutionsBegin, substitutionsEnd,
-                       bind2nd(first_equal_to<typename Iterator::value_type::first_type, typename Iterator::value_type::second_type>(), *this));
+  Iterator j = find_if(
+      substitutionsBegin,
+      substitutionsEnd,
+      [this](const auto& subst){ return subst.first == *this; });
   if(j != substitutionsEnd) {
     Node n = (*j).second;
     cache[*this] = n;

diff --git a/src/main/signal_handlers.cpp b/src/main/signal_handlers.cpp
index ee66b906bf099230ce686e6f2f5738e764862a97..a7d98ba060811c27f50f5c2f5bad3f600c408168 100644 (file)
--- a/src/main/signal_handlers.cpp
+++ b/src/main/signal_handlers.cpp
@@ -217,60 +217,6 @@ void ill_handler(int sig, siginfo_t* info, void*)
 
 static terminate_handler default_terminator;
 
-void cvc4unexpected()
-{
-#if defined(CVC4_DEBUG) && !defined(__WIN32__)
-  safe_print(STDERR_FILENO,
-             "\n"
-             "CVC4 threw an \"unexpected\" exception (one that wasn't properly "
-             "specified\nin the throws() specifier for the throwing function)."
-             "\n\n");
-
-  const char* lastContents = LastExceptionBuffer::currentContents();
-
-  if (lastContents == NULL)
-  {
-    safe_print(
-        STDERR_FILENO,
-        "The exception is unknown (maybe it's not a CVC4::Exception).\n\n");
-  }
-  else
-  {
-    safe_print(STDERR_FILENO, "The exception is:\n");
-    safe_print(STDERR_FILENO, lastContents);
-    safe_print(STDERR_FILENO, "\n\n");
-  }
-  if (!segvSpin)
-  {
-    print_statistics();
-    set_terminate(default_terminator);
-  }
-  else
-  {
-    safe_print(STDERR_FILENO,
-               "Spinning so that a debugger can be connected.\n");
-    safe_print(STDERR_FILENO, "Try:  gdb ");
-    safe_print(STDERR_FILENO, *progName);
-    safe_print(STDERR_FILENO, " ");
-    safe_print<int64_t>(STDERR_FILENO, getpid());
-    safe_print(STDERR_FILENO, "\n");
-    safe_print(STDERR_FILENO, " or:  gdb --pid=");
-    safe_print<int64_t>(STDERR_FILENO, getpid());
-    safe_print(STDERR_FILENO, " ");
-    safe_print(STDERR_FILENO, *progName);
-    safe_print(STDERR_FILENO, "\n");
-    for (;;)
-    {
-      sleep(60);
-    }
-  }
-#else  /* CVC4_DEBUG */
-  safe_print(STDERR_FILENO, "CVC4 threw an \"unexpected\" exception.\n");
-  print_statistics();
-  set_terminate(default_terminator);
-#endif /* CVC4_DEBUG */
-}
-
 void cvc4terminate()
 {
   set_terminate(default_terminator);
@@ -385,7 +331,6 @@ void install()
 
 #endif /* __WIN32__ */
 
-  std::set_unexpected(cvc4unexpected);
   default_terminator = set_terminate(cvc4terminate);
 }
 

diff --git a/src/main/signal_handlers.h b/src/main/signal_handlers.h
index 5eb3f24c76522dfe402275afd1e97127a4a2fd2a..394377d91995b6da6ac29bbc0c0e8782e3b03859 100644 (file)
--- a/src/main/signal_handlers.h
+++ b/src/main/signal_handlers.h
@@ -30,7 +30,7 @@ void timeout_handler();
 /**
  * Installs (almost) all signal handlers.
  * A handler for SIGALRM is set in time_limit.cpp.
- * Also sets callbacks via std::set_unexpected and std:set_terminate.
+ * Also sets callbacks via std:set_terminate.
  */
 void install();
 

diff --git a/src/util/utility.h b/src/util/utility.h
index 6cf8bb3f4c14d43deed17f0c468385849ab0695d..549b98d669bd30d38359615b355d825e94a96786 100644 (file)
--- a/src/util/utility.h
+++ b/src/util/utility.h
@@ -29,30 +29,6 @@
 namespace CVC4 {
 
 
-/**
- * Like std::equal_to<>, but tests equality between the first element
- * of a pair and an element.
- */
-template <class T, class U>
-struct first_equal_to : std::binary_function<std::pair<T, U>, T, bool> {
-  bool operator()(const std::pair<T, U>& pr, const T& x) const {
-    return pr.first == x;
-  }
-};/* struct first_equal_to<T> */
-
-
-/**
- * Like std::equal_to<>, but tests equality between the second element
- * of a pair and an element.
- */
-template <class T, class U>
-struct second_equal_to : std::binary_function<std::pair<T, U>, U, bool> {
-  bool operator()(const std::pair<T, U>& pr, const U& x) const {
-    return pr.second == x;
-  }
-};/* struct first_equal_to<T> */
-
-
 /**
  * Using std::find_if(), finds the first iterator in [first,last)
  * range that satisfies predicate.  If none, return last; otherwise,