diff --git a/misc/_rumur b/misc/_rumur index a61b0caa..9e62ba3a 100644 --- a/misc/_rumur +++ b/misc/_rumur @@ -17,6 +17,10 @@ _arguments \ '--sandbox[verifier privilege restriction]: :(on off)' \ {--set-capacity,-s}'[initial memory (in bytes) to allocate for the seen set]:SIZE' \ {--set-expand-threshold,-e}'[limit at which to expand the seen set]:occupancy percentage' \ + '--smt-arg[argument to pass to SMT solver]:ARG' \ + '--smt-budget[time allotment for SMT solver]:MILLISECONDS' \ + '--smt-path[path to SMT solver]:path:_cmdstring' \ + '--smt-simplification[disable or enable using SMT solver for simplification]: :(off on)' \ '--symmetry-reduction[symmetry reduction optimisation]: :(off heuristic exhaustive)' \ {--threads,-t}'[number of threads to use in the verifier]:count' \ '--trace[tracing messages to print in the verifier]: :(handle_reads handle_writes queue set symmetry_reduction all)' \ diff --git a/rumur/doc/rumur.1 b/rumur/doc/rumur.1 index bef5a313..d7426419 100644 --- a/rumur/doc/rumur.1 +++ b/rumur/doc/rumur.1 @@ -211,6 +211,62 @@ Output informational messages while generating the verifier. .RS Display version information and exit. .RE +.SH SMT OPTIONS +If you have a Satisfiability Modulo Theories (SMT) solver installed, Rumur can +use it to optimise your model while generating a verifier. This functionality is +not enabled by default, but you can use the following options to configure Rumur +to find and use your SMT solver. Some examples of solver configuration: +.PP +.RS +# for Z3 with a 5 second timeout +.br +\fBrumur --smt-simplification on --smt-path z3 --smt-arg=-smt2 --smt-arg=-in --smt-arg=-t:5000 ...\fR +.PP +# for CVC4 with a 5 second timeout +.br +\fBrumur --smt-simplification on --smt-path cvc4 --smt-arg=--lang=smt2 --smt-arg=--tlimit=5000 ...\fR +.RE +.PP +For other solvers, consult their manpages or documentation to determine what +command line parameters they accept. Then use the options described below to +instruct Rumur how to use them. Note that Rumur can only use a single SMT +solver and specifying the \fB--smt-path\fR option multiple times will only +retain the last path given. +.PP +\fB--smt-arg\fR \fBARG\fI +.RS +A command line argument to pass to the SMT solver. This option can be given +multiple times and arguments are passed in the order listed. E.g. if you specify +\fB--smt-arg=--tlimit\fR \fB--smt-arg=5000\fR the solver will be called with the +command line arguments \fB--tlimit\fR \fB5000\fR. +.RE +.PP +\fB--smt-budget\fR \fIMILLISECONDS\fR +.RS +Total time allotted for running the SMT solver. That is, the time the solver +will be allowed to run for over multiple executions. This defaults to +\fI30000\fR, 30 seconds. So if the solver runs for 10 seconds the first time it +is called, then 5 seconds the second time it is called, then 20 seconds the +third time it is called, it will not be called again. Note that Rumur trusts the +SMT solver to limit itself to a reasonable timeout per run, so its final run can +exceed the budget. You may want to use the \fB--smt-arg\fR option to pass the +SMT solver a timeout limit if it supports one. +.RE +.PP +\fB--smt-path\fR \fIPATH\fR +.RS +Command or path to the SMT solver. This will use your environment's \fBPATH\fR +variable, so if the solver is in one of your system directories you can simply +provide the name of its binary. Note that this option has no effect unless you +also pass \fB--smt-simplification\fR \fBon\fR. +.RE +.PP +\fB--smt-simplification\fR [\fBoff\fR | \fBon\fR] +.RS +Disable or enable using the SMT solver to simplify the input model. By default, +this is \fBoff\fR. Note that this option has no effect unless you also configure +a path to the SMT solver with \fB--smt-path\fR. +.RE .SH AUTHOR All comments, questions and complaints should be directed to Matthew Fernandez . diff --git a/rumur/src/main.cc b/rumur/src/main.cc index f42245b9..dc697a2f 100644 --- a/rumur/src/main.cc +++ b/rumur/src/main.cc @@ -12,6 +12,8 @@ #include #include "options.h" #include +#include "smt/except.h" +#include "smt/simplify.h" #include #include #include @@ -48,6 +50,10 @@ static void parse_args(int argc, char **argv) { OPT_MONOPOLISE, OPT_OUTPUT_FORMAT, OPT_SANDBOX, + OPT_SMT_ARG, + OPT_SMT_BUDGET, + OPT_SMT_PATH, + OPT_SMT_SIMPLIFICATION, OPT_SYMMETRY_REDUCTION, OPT_TRACE, OPT_VALUE_TYPE, @@ -71,6 +77,10 @@ static void parse_args(int argc, char **argv) { { "sandbox", required_argument, 0, OPT_SANDBOX }, { "set-capacity", required_argument, 0, 's' }, { "set-expand-threshold", required_argument, 0, 'e' }, + { "smt-arg", required_argument, 0, OPT_SMT_ARG }, + { "smt-budget", required_argument, 0, OPT_SMT_BUDGET }, + { "smt-path", required_argument, 0, OPT_SMT_PATH }, + { "smt-simplification", required_argument, 0, OPT_SMT_SIMPLIFICATION }, { "symmetry-reduction", required_argument, 0, OPT_SYMMETRY_REDUCTION }, { "threads", required_argument, 0, 't' }, { "trace", required_argument, 0, OPT_TRACE }, @@ -336,6 +346,42 @@ static void parse_args(int argc, char **argv) { options.value_type = optarg; break; + case OPT_SMT_ARG: // --smt-arg ... + options.smt.args.emplace_back(optarg); + break; + + case OPT_SMT_BUDGET: { // --smt-budget ... + bool valid = true; + try { + options.smt.budget = optarg; + if (options.smt.budget < 0) + valid = false; + } catch (std::invalid_argument&) { + valid = false; + } + if (!valid) { + std::cerr << "invalid --smt-budget, \"" << optarg << "\"\n"; + exit(EXIT_FAILURE); + } + break; + } + + case OPT_SMT_PATH: // --smt-path ... + options.smt.path = optarg; + break; + + case OPT_SMT_SIMPLIFICATION: // --smt-simplification ... + if (strcmp(optarg, "on") == 0) { + options.smt.simplification = true; + } else if (strcmp(optarg, "off") == 0) { + options.smt.simplification = false; + } else { + std::cerr << "invalid argument to --smt-simplification, \"" << optarg + << "\"\n"; + exit(EXIT_FAILURE); + } + break; + default: std::cerr << "unexpected error\n"; exit(EXIT_FAILURE); @@ -378,6 +424,20 @@ static void parse_args(int argc, char **argv) { options.threads = r; } } + + if (!options.smt.simplification) { + if (options.smt.path != "" || !options.smt.args.empty()) { + *warn << "a path and/or arguments to an SMT solver were provided but SMT " + "simplification was not enabled (--smt-simplification on) so the " + "solver will not be used\n"; + } + } + + if (options.smt.simplification && options.smt.path == "") { + *warn << "SMT simplification was enabled but no path was provided to the " + << "solver (--smt-path ...), so it will be disabled\n"; + options.smt.simplification = false; + } } template @@ -503,6 +563,17 @@ int main(int argc, char **argv) { if (!contains(m->rules, has_start_state)) *warn << "warning: model has no start state\n"; + // run SMT simplification if the user enabled it + if (options.smt.simplification) { + try { + smt::simplify(*m); + } catch (smt::BudgetExhausted&) { + *info << "SMT solver budget (" << options.smt.budget << "ms) exhausted\n"; + } catch (smt::Unsupported&) { + *info << "SMT solver encountered an unsupported expression\n"; + } + } + // get value_t to use in the checker std::pair value_types; try {