plumb SMT functionality to command line options

Github: related to #130 "interact with SMT solver"

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)' \

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
 <[email protected]>.

rumur/src/main.cc

@@ -12,6 +12,8 @@
 #include <memory>
 #include "options.h"
 #include <rumur/rumur.h>
+#include "smt/except.h"
+#include "smt/simplify.h"
 #include <sstream>
 #include <string>
 #include <sys/stat.h>
@@ -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<typename T, typename U>
@@ -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<ValueType, ValueType> value_types;
   try {