diff options
author | Gereon Kremer <gereon.kremer@cs.rwth-aachen.de> | 2020-07-08 23:24:24 +0200 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-07-08 16:24:24 -0500 |
commit | a0a389a1f7c16b6a1fb56b3ce8ee519cf5717f04 (patch) | |
tree | 6908a4c3aed1be0100057c5b8f97a40673c99779 /src/main/time_limit.cpp | |
parent | 37801c1da918ad1c4de97e8a64ca7d1177b61de4 (diff) |
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)
Diffstat (limited to 'src/main/time_limit.cpp')
-rw-r--r-- | src/main/time_limit.cpp | 32 |
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 |