Merge pull request #8726 from tautschnig/smt-solver-command

Add --external-smt2-solver for custom solver path or custom options

Author: tautschnig

doc/man/cbmc.1

@@ -516,6 +516,10 @@ use Z3
 \fB\-\-fpa\fR
 use theory of floating\-point arithmetic
 .TP
+\fB\-\-external\-smt2\-solver\fR \fIcmd\fR
+Use \fIcmd\fR to invoke the SMT2 solver. Combine with one of the solver choices
+for solver-specific constraints.
+.TP
 \fB\-\-refine\fR
 use refinement procedure (experimental)
 .TP

doc/man/goto-synthesizer.1

@@ -82,6 +82,10 @@ use Z3
 \fB\-\-fpa\fR
 use theory of floating\-point arithmetic
 .TP
+\fB\-\-external\-smt2\-solver\fR \fIcmd\fR
+Use \fIcmd\fR to invoke the SMT2 solver. Combine with one of the solver choices
+for solver-specific constraints.
+.TP
 \fB\-\-refine\fR
 use refinement procedure (experimental)
 .TP

doc/man/jbmc.1

@@ -434,6 +434,10 @@ use Z3
 \fB\-\-fpa\fR
 use theory of floating\-point arithmetic
 .TP
+\fB\-\-external\-smt2\-solver\fR \fIcmd\fR
+Use \fIcmd\fR to invoke the SMT2 solver. Combine with one of the solver choices
+for solver-specific constraints.
+.TP
 \fB\-\-refine\fR
 use refinement procedure (experimental)
 .TP

regression/cbmc/Failing_Assert1/external-smt-solver.desc

@@ -0,0 +1,8 @@
+CORE smt-backend broken-cprover-smt-backend no-new-smt
+main.c
+--z3 --external-smt2-solver z3 --trace
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring

scripts/bash-autocomplete/cbmc.sh.template

@@ -40,7 +40,7 @@ _cbmc_autocomplete()
      _filedir -d
      return 0
      ;;
-   --external-sat-solver|--incremental-smt2-solver)
+   --external-sat-solver|--incremental-smt2-solver|--external-smt2-solver)
      #a switch that takes a file parameter of which we don't know an extension
      _filedir -f
      return 0

src/goto-checker/solver_factory.cpp

@@ -515,6 +515,7 @@ solver_factoryt::get_smt2(smt2_dect::solvert solver)
       std::string("Generated by CBMC ") + CBMC_VERSION,
       "QF_AUFBV",
       solver,
+      options.get_option("external-smt2-solver"),
       message_handler);
 
     if(options.get_bool_option("fpa"))
@@ -672,6 +673,14 @@ static void parse_smt2_options(const cmdlinet &cmdline, optionst &options)
     options.set_option("smt2", true);
   }
 
+  if(cmdline.isset("external-smt2-solver"))
+  {
+    options.set_option(
+      "external-smt2-solver", cmdline.get_value("external-smt2-solver"));
+    solver_set = true;
+    options.set_option("smt2", true);
+  }
+
   if(cmdline.isset("smt2") && !solver_set)
   {
     if(cmdline.isset("outfile"))

src/goto-checker/solver_factory.h

@@ -104,6 +104,7 @@ void parse_solver_options(const cmdlinet &cmdline, optionst &options);
   "(mathsat)"                                                                  \
   "(cprover-smt2)"                                                             \
   "(incremental-smt2-solver):"                                                 \
+  "(external-smt2-solver):"                                                    \
   "(sat-solver):"                                                              \
   "(external-sat-solver):"                                                     \
   "(no-sat-preprocessor)"                                                      \
@@ -135,6 +136,8 @@ void parse_solver_options(const cmdlinet &cmdline, optionst &options);
   " {y--yices} \t use Yices\n"                                                 \
   " {y--z3} \t use Z3\n"                                                       \
   " {y--fpa} \t use theory of floating-point arithmetic\n"                     \
+  " {y--external-smt2-solver} {ucmd} \t command to invoke SMT2 solver "        \
+  "(combine with one of the solver choices for solver-specific constraints)\n" \
   " {y--refine} \t use refinement procedure (experimental)\n"                  \
   " {y--refine-arrays} \t use refinement for arrays only\n"                    \
   " {y--refine-arithmetic} \t refinement of arithmetic expressions only\n"     \

src/goto-instrument/accelerate/scratch_program.h

@@ -74,7 +74,7 @@ class scratch_programt:public goto_programt
       symex(mh, symbol_table, equation, options, path_storage, guard_manager),
       satcheck(std::make_unique<satcheckt>(mh)),
       satchecker(ns, *satcheck, mh),
-      z3(ns, "accelerate", "", "", smt2_dect::solvert::Z3, mh),
+      z3(ns, "accelerate", "", "", smt2_dect::solvert::Z3, "", mh),
       checker(&z3) // checker(&satchecker)
   {
   }

src/solvers/smt2/smt2_dec.cpp

@@ -65,76 +65,90 @@ decision_proceduret::resultt smt2_dect::dec_solve(const exprt &assumption)
   std::vector<std::string> argv;
   std::string stdin_filename;
 
+  auto solver_binary_name = [this](const std::string &solver_name)
+  {
+    if(solver_binary_or_empty.empty())
+      return solver_name;
+    else
+      return solver_binary_or_empty;
+  };
+
   switch(solver)
   {
   case solvert::BITWUZLA:
-    argv = {"bitwuzla", temp_file_problem()};
+    argv = {solver_binary_name("bitwuzla"), temp_file_problem()};
     break;
 
   case solvert::BOOLECTOR:
-    argv = {"boolector", "--smt2", temp_file_problem(), "-m"};
+    argv = {
+      solver_binary_name("boolector"), "--smt2", temp_file_problem(), "-m"};
     break;
 
   case solvert::CPROVER_SMT2:
-    argv = {"smt2_solver"};
+    argv = {solver_binary_name("smt2_solver")};
     stdin_filename = temp_file_problem();
     break;
 
   case solvert::CVC3:
-    argv = {"cvc3",
-            "+model",
-            "-lang",
-            "smtlib",
-            "-output-lang",
-            "smtlib",
-            temp_file_problem()};
+    argv = {
+      solver_binary_name("cvc3"),
+      "+model",
+      "-lang",
+      "smtlib",
+      "-output-lang",
+      "smtlib",
+      temp_file_problem()};
     break;
 
   case solvert::CVC4:
     // The flags --bitblast=eager --bv-div-zero-const help but only
     // work for pure bit-vector formulas.
-    argv = {"cvc4", "-L", "smt2", temp_file_problem()};
+    argv = {solver_binary_name("cvc4"), "-L", "smt2", temp_file_problem()};
     break;
 
   case solvert::CVC5:
-    argv = {"cvc5", "--lang", "smtlib", temp_file_problem()};
+    argv = {
+      solver_binary_name("cvc5"), "--lang", "smtlib", temp_file_problem()};
     break;
 
   case solvert::MATHSAT:
     // The options below were recommended by Alberto Griggio
     // on 10 July 2013
 
-    argv = {"mathsat",
-            "-input=smt2",
-            "-preprocessor.toplevel_propagation=true",
-            "-preprocessor.simplification=7",
-            "-dpll.branching_random_frequency=0.01",
-            "-dpll.branching_random_invalidate_phase_cache=true",
-            "-dpll.restart_strategy=3",
-            "-dpll.glucose_var_activity=true",
-            "-dpll.glucose_learnt_minimization=true",
-            "-theory.bv.eager=true",
-            "-theory.bv.bit_blast_mode=1",
-            "-theory.bv.delay_propagated_eqs=true",
-            "-theory.fp.mode=1",
-            "-theory.fp.bit_blast_mode=2",
-            "-theory.arr.mode=1"};
+    argv = {
+      solver_binary_name("mathsat"),
+      "-input=smt2",
+      "-preprocessor.toplevel_propagation=true",
+      "-preprocessor.simplification=7",
+      "-dpll.branching_random_frequency=0.01",
+      "-dpll.branching_random_invalidate_phase_cache=true",
+      "-dpll.restart_strategy=3",
+      "-dpll.glucose_var_activity=true",
+      "-dpll.glucose_learnt_minimization=true",
+      "-theory.bv.eager=true",
+      "-theory.bv.bit_blast_mode=1",
+      "-theory.bv.delay_propagated_eqs=true",
+      "-theory.fp.mode=1",
+      "-theory.fp.bit_blast_mode=2",
+      "-theory.arr.mode=1"};
 
     stdin_filename = temp_file_problem();
     break;
 
   case solvert::YICES:
     //    command = "yices -smt -e "   // Calling convention for older versions
     // Convention for 2.2.1
-    argv = {"yices-smt2", temp_file_problem()};
+    argv = {solver_binary_name("yices-smt2"), temp_file_problem()};
     break;
 
   case solvert::Z3:
-    argv = {"z3", "-smt2", temp_file_problem()};
+    argv = {solver_binary_name("z3"), "-smt2", temp_file_problem()};
     break;
 
   case solvert::GENERIC:
-    UNREACHABLE;
+    PRECONDITION(!solver_binary_or_empty.empty());
+    argv = {solver_binary_or_empty, temp_file_problem()};
+    break;
   }
 
   int res =

src/solvers/smt2/smt2_dec.h

@@ -31,15 +31,18 @@ class smt2_dect : protected smt2_stringstreamt, public smt2_convt
     const std::string &_notes,
     const std::string &_logic,
     solvert _solver,
+    const std::string &_solver_binary_or_empty,
     message_handlert &_message_handler)
     : smt2_convt(_ns, _benchmark, _notes, _logic, _solver, stringstream),
+      solver_binary_or_empty(_solver_binary_or_empty),
       message_handler(_message_handler)
   {
   }
 
   std::string decision_procedure_text() const override;
 
 protected:
+  std::string solver_binary_or_empty;
   message_handlert &message_handler;
   resultt dec_solve(const exprt &) override;