Re-implement handling of --tlimit (#4655)
authorGereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Wed, 8 Jul 2020 21:24:24 +0000 (23:24 +0200)
committerGitHub <noreply@github.com>
Wed, 8 Jul 2020 21:24:24 +0000 (16:24 -0500)
commita0a389a1f7c16b6a1fb56b3ce8ee519cf5717f04
tree6908a4c3aed1be0100057c5b8f97a40673c99779
parent37801c1da918ad1c4de97e8a64ca7d1177b61de4
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/CMakeLists.txt
src/main/driver_unified.cpp
src/main/time_limit.cpp [new file with mode: 0644]
src/main/time_limit.h [new file with mode: 0644]
src/main/util.cpp
src/options/options.h
src/options/options_public_functions.cpp
src/options/smt_options.toml