Skip to content

Commit

Permalink
Adds --abort-on-int cmdline flag to yices executable.
Browse files Browse the repository at this point in the history
We use the yices executable (and not the yices_smt2 executable) as a
sub-process solver from our primary application.  Our application
expects normal cleanup to the foreground process group to occur on
Ctrl-C / SIGINT, but currently it will exit and leave the yices
process running in the background because yices does not exit on this
event.

This small patch adds the cmdline flag that we can use from our
application to run yices in a mode that will exit on these events.
The default is the current behavior so this change should be fully
backward-compatible.
  • Loading branch information
kquick committed Jan 22, 2021
1 parent 8ee16b9 commit d90d27a
Showing 1 changed file with 15 additions and 1 deletion.
16 changes: 15 additions & 1 deletion src/frontend/yices/yices_reval.c
Original file line number Diff line number Diff line change
Expand Up @@ -128,6 +128,8 @@
* and we don't exit on error.
* - print_success: if this flag is true, we print "ok" after every
* command that would otherwise print nothing.
* - abort_on_int: if true then exit when SIGINT is received instead
* of returning to input processing (the default).
* - verbosity: verbosity level
* - done: set to true when exit is called, or if there's an error and
* interactive is false (i.e., we exit on the first error unless we're
Expand All @@ -145,6 +147,10 @@
* by default, these are NULL
* - mcsat_requested: option --mscat (this forces use of the MC-SAT solver
* for logic where MC-SAT is not the default).
* - print-success: print success for commands that would otherwise
* complete silently
* - abort-on-int: abort execution on SIGINT instead of returning to
* input processing
*
* CONTEXT CONFIGURATION
* - logic_code = code for the logic_name (default is SMT_UNKNNOW)
Expand All @@ -164,6 +170,7 @@ static uint32_t include_depth;
static bool interactive;
static bool done;
static bool print_success;
static bool abort_on_int;
static int32_t verbosity;
static tracer_t *tracer;

Expand Down Expand Up @@ -269,6 +276,7 @@ enum {
version_flag,
help_flag,
print_success_flag,
abort_on_int_flag,
verbosity_option,
};

Expand All @@ -282,6 +290,7 @@ static option_desc_t options[NUM_OPTIONS] = {
{ "version", 'V', FLAG_OPTION, version_flag },
{ "help", 'h', FLAG_OPTION, help_flag },
{ "print-success", '\0', FLAG_OPTION, print_success_flag },
{ "abort-on-int", '\0', FLAG_OPTION, abort_on_int_flag },
{ "verbosity", 'v', MANDATORY_INT, verbosity_option },
};

Expand Down Expand Up @@ -412,6 +421,7 @@ static void process_command_line(int argc, char *argv[]) {
mcsat_requested = false;
verbosity = 0;
print_success = false;
abort_on_int = false;
tracer = NULL;
logic_code = SMT_UNKNOWN;
arith_code = ARITH_SIMPLEX;
Expand Down Expand Up @@ -495,6 +505,10 @@ static void process_command_line(int argc, char *argv[]) {
print_success = true;
break;

case abort_on_int_flag:
abort_on_int = true;
break;

case verbosity_option:
v = elem.i_value;
if (v < 0) {
Expand Down Expand Up @@ -792,7 +806,7 @@ static void default_handler(int signum) {
* Initialize the signal handlers
*/
static void init_handlers(void) {
signal(SIGINT, sigint_handler);
signal(SIGINT, abort_on_int ? default_handler : sigint_handler);
signal(SIGABRT, default_handler);
#ifndef MINGW
signal(SIGXCPU, default_handler);
Expand Down

0 comments on commit d90d27a

Please sign in to comment.