From: Mathias Preiner <mathias.preiner@gmail.com>
Date: Tue, 23 Feb 2021 23:56:16 +0000 (-0800)
Subject: Switch to C++17. (#5959)
X-Git-Tag: cvc5-1.0.0~2231
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4c0dbb8ec7871ff114a9e66233cd8c8dd853f0b4;p=cvc5.git

Switch to C++17. (#5959)

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

diff --git a/CMakeLists.txt b/CMakeLists.txt
index 4a90afa8b..3dd282a8d 100644
--- 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 75d4d2022..559ce5ddb 100644
--- 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 ee66b906b..a7d98ba06 100644
--- 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 5eb3f24c7..394377d91 100644
--- 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 6cf8bb3f4..549b98d66 100644
--- 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,