Re-implement handling of --tlimit (#4655)

As a first step within this project, this PR provides a new implementation that backs --tlimit. It uses setitimer (as timer_settime is not available on MacOS) to make the OS send a signal after the given wall clock time has passed.
In more detail, this PR:

removes the current handling of --tlimit (TlimitListener and its integration in the NodeManager)
adds a new TimeLimitListener that lives in src/main
uses TimeLimitListener directly in runCvc4()
adds a signal handler for SIGALRM (that also uses the existing timeout_handler)

1 files changed, 32 insertions, 0 deletions

diff --git a/src/main/time_limit.cpp b/src/main/time_limit.cpp
new file mode 100644
index 000000000..973d48f6f
--- /dev/null
+++ b/src/main/time_limit.cpp
@@ -0,0 +1,32 @@
+#include "time_limit.h"
+
+#include <sys/time.h>
+
+#include <cerrno>
+#include <cstring>
+
+namespace CVC4 {
+namespace main {
+
+void install_time_limit(const Options& opts)
+{
+  unsigned long ms = opts.getCumulativeTimeLimit();
+  if (ms == 0) return;
+
+  // Check https://linux.die.net/man/2/setitimer
+  struct itimerval timerspec;
+  timerspec.it_value.tv_sec = ms / 1000;
+  timerspec.it_value.tv_usec = (ms % 1000) * 1000;
+  timerspec.it_interval.tv_sec = 0;
+  timerspec.it_interval.tv_usec = 0;
+  // Argument 1: which timer to set, we want the real time
+  // Argument 2: timer configuration, relative to current time
+  // Argument 3: old timer configuration, we don't want to know
+  if (setitimer(ITIMER_REAL, &timerspec, nullptr))
+  {
+    throw Exception(std::string("timer_settime() failure: ") + strerror(errno));
+  }
+}
+
+}  // namespace main
+}  // namespace CVC4