changed flag from sat-solver-invocation to external-sat-solver

Author: fbbotero-aws

src/cbmc/cbmc_parse_options.cpp

@@ -437,10 +437,10 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
     options.set_option("smt2", true);
   }
 
-  if(cmdline.isset("sat-solver-invocation"))
+  if(cmdline.isset("external-sat-solver"))
   {
     options.set_option(
-      "sat-solver-invocation", cmdline.get_value("sat-solver-invocation")),
+      "external-sat-solver", cmdline.get_value("external-sat-solver")),
       solver_set = true;
   }
 
@@ -1116,7 +1116,7 @@ void cbmc_parse_optionst::help()
     " --yices                      use Yices\n"
     " --z3                         use Z3\n"
     " --refine                     use refinement procedure (experimental)\n"
-    " --sat-solver-invocation cmd  command to invoke SAT solver process\n"
+    " --external-sat-solver cmd    command to invoke SAT solver process\n"
     HELP_STRING_REFINEMENT_CBMC
     " --outfile filename           output formula to given file\n"
     " --arrays-uf-never            never turn arrays into uninterpreted functions\n" // NOLINT(*)

src/cbmc/cbmc_parse_options.h

@@ -57,7 +57,7 @@ class optionst;
   OPT_JSON_INTERFACE \
   "(smt1)(smt2)(fpa)(cvc3)(cvc4)(boolector)(yices)(z3)(mathsat)" \
   "(cprover-smt2)" \
-  "(sat-solver-invocation):" \
+  "(external-sat-solver):" \
   "(no-sat-preprocessor)" \
   "(beautify)" \
   "(dimacs)(refine)(max-node-refinement):(refine-arrays)(refine-arithmetic)"\

src/goto-checker/solver_factory.cpp

@@ -132,7 +132,7 @@ std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_solver()
 {
   if(options.get_bool_option("dimacs"))
     return get_dimacs();
-  if(options.is_set("sat-solver-invocation"))
+  if(options.is_set("external-sat-solver"))
     return get_external_sat();
   if(
     options.get_bool_option("refine") &&
@@ -241,10 +241,10 @@ std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_external_sat()
   no_beautification();
   no_incremental_check();
 
-  std::string sat_solver_invocation =
-    options.get_option("sat-solver-invocation");
+  std::string external_sat_solver =
+    options.get_option("external-sat-solver");
   auto prop =
-    util_make_unique<external_satt>(message_handler, sat_solver_invocation);
+    util_make_unique<external_satt>(message_handler, external_sat_solver);
 
   auto bv_pointers = util_make_unique<bv_pointerst>(ns, *prop, message_handler);
 
@@ -421,4 +421,4 @@ void solver_factoryt::no_incremental_check()
       "the chosen solver does not support incremental solving",
       "--incremental-check");
   }
-}
+}

src/goto-checker/solver_factory.h

@@ -90,4 +90,4 @@ class solver_factoryt
   void no_incremental_check();
 };
 
-#endif // CPROVER_GOTO_CHECKER_SOLVER_FACTORY_H
+#endif // CPROVER_GOTO_CHECKER_SOLVER_FACTORY_H

src/solvers/sat/external_sat.cpp

@@ -1,5 +1,5 @@
 /// \file
-/// Allows call an external SAT solver to allow faster integration of 
+/// Allows call an external SAT solver to allow faster integration of
 /// newer SAT solvers
 /// \author Francis Botero <fbbotero@amazon.com>
 

src/solvers/sat/external_sat.h

@@ -1,5 +1,5 @@
 /// \file
-/// Allows call an external SAT solver to allow faster integration of 
+/// Allows calling an external SAT solver to allow faster integration of
 /// newer SAT solvers
 /// \author Francis Botero <fbbotero@amazon.com>
 
@@ -31,11 +31,9 @@ class external_satt : public cnf_clause_list_assignmentt
 protected:
   resultt do_prop_solve() override;
   std::string solver_cmd;
-
-private:
-  inline void write_cnf_file(std::string);
-  inline std::string execute_solver(std::string);
-  inline resultt parse_result(std::string);
+  void write_cnf_file(std::string);
+  std::string execute_solver(std::string);
+  resultt parse_result(std::string);
 };
 
 #endif // CPROVER_SOLVERS_SAT_EXTERNAL_SAT_H