From a0a389a1f7c16b6a1fb56b3ce8ee519cf5717f04 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Wed, 8 Jul 2020 23:24:24 +0200 Subject: 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) --- src/main/driver_unified.cpp | 3 +++ 1 file changed, 3 insertions(+) (limited to 'src/main/driver_unified.cpp') 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 filenames = Options::parseOptions(&opts, argc, argv); + install_time_limit(opts); + string progNameStr = opts.getBinaryName(); progName = &progNameStr; -- cgit v1.2.3