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/driver_unified.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/driver_unified.cpp')
| -rw-r--r-- | src/main/driver_unified.cpp | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp index 374f68257..955fa7b74 100644 --- a/src/main/driver_unified.cpp +++ b/src/main/driver_unified.cpp @@ -32,6 +32,7 @@ #include "main/command_executor.h" #include "main/interactive_shell.h" #include "main/main.h" +#include "main/time_limit.h" #include "options/options.h" #include "options/set_language.h" #include "parser/parser.h" @@ -98,6 +99,8 @@ int runCvc4(int argc, char* argv[], Options& opts) { // Parse the options vector<string> filenames = Options::parseOptions(&opts, argc, argv); + install_time_limit(opts); + string progNameStr = opts.getBinaryName(); progName = &progNameStr; |