Move combined smt sub-process and dumping into separate class

In order to deduplicate code which had been cut and paste into 2
classes.

Author: thomasspriggs

src/goto-checker/solver_factory.cpp

@@ -382,17 +382,20 @@ solver_factoryt::get_incremental_smt2(std::string solver_command)
     solver_process = util_make_unique<smt_incremental_dry_run_solvert>(
       on_std_out ? std::cout : *outfile, std::move(outfile));
   }
-  else
+  else if(!dump_smt_formula.empty())
   {
-    const auto out_filename = options.get_option("dump-smt-formula");
-
     // If no out_filename is provided `open_outfile_and_check` will return
     // `nullptr`, and the solver will work normally without any logging.
-    solver_process = util_make_unique<smt_piped_solver_processt>(
+    solver_process = util_make_unique<smt_piped_solver_process_with_dumpt>(
       std::move(solver_command),
       message_handler,
       open_outfile_and_check(
-        out_filename, message_handler, "--dump-smt-formula"));
+        dump_smt_formula, message_handler, "--dump-smt-formula"));
+  }
+  else
+  {
+    solver_process = util_make_unique<smt_piped_solver_processt>(
+      std::move(solver_command), message_handler);
   }
 
   return util_make_unique<solvert>(

src/solvers/smt2_incremental/smt_solver_process.cpp

@@ -9,12 +9,16 @@
 #include <util/invariant.h>
 #include <util/string_utils.h>
 
+void smt_base_solver_processt::send(const smt_commandt &smt_command)
+{
+  const std::string command_string = smt_to_smt2_string(smt_command);
+  send(command_string);
+}
+
 smt_piped_solver_processt::smt_piped_solver_processt(
   std::string command_line,
-  message_handlert &message_handler,
-  std::unique_ptr<std::ostream> out_stream)
+  message_handlert &message_handler)
   : command_line_description{"\"" + command_line + "\""},
-    out_stream(std::move(out_stream)),
     process{split_string(command_line, ' ', false, true), message_handler},
     log{message_handler}
 {
@@ -25,20 +29,10 @@ std::string smt_piped_solver_processt::description()
   return command_line_description;
 }
 
-void smt_piped_solver_processt::send(const smt_commandt &smt_command)
+void smt_piped_solver_processt::send(const std::string &command_string)
 {
-  const std::string command_string = smt_to_smt2_string(smt_command);
   log.debug() << "Sending command to SMT2 solver - " << command_string
               << messaget::eom;
-
-  if(out_stream != nullptr)
-  {
-    // Using `std::endl` instead of '\n' to also flush the stream as it is a
-    // debugging functionality, to guarantee a consistent output in case of
-    // hanging after `(check-sat)`
-    *out_stream << command_string << std::endl;
-  }
-
   const auto response = process.send(command_string + "\n");
   switch(response)
   {
@@ -92,9 +86,9 @@ std::string smt_incremental_dry_run_solvert::description()
   return "SMT2 incremental dry-run";
 }
 
-void smt_incremental_dry_run_solvert::send(const smt_commandt &smt_command)
+void smt_incremental_dry_run_solvert::send(const std::string &smt_command)
 {
-  out_stream << smt_to_smt2_string(smt_command) << '\n';
+  out_stream << smt_command << '\n';
 }
 
 smt_responset smt_incremental_dry_run_solvert::receive_response(
@@ -106,3 +100,29 @@ smt_responset smt_incremental_dry_run_solvert::receive_response(
   // (as a `smt_sat_responset` answer will trigger).
   return smt_check_sat_responset{smt_unsat_responset{}};
 }
+
+smt_piped_solver_process_with_dumpt::smt_piped_solver_process_with_dumpt(
+  std::string command_line,
+  message_handlert &message_handler,
+  std::unique_ptr<std::ostream> out_stream)
+  : smt_piped_solver_processt{std::move(command_line), message_handler},
+    smt_incremental_dry_run_solvert{*out_stream, std::move(out_stream)}
+{
+}
+
+void smt_piped_solver_process_with_dumpt::send(const std::string &command)
+{
+  smt_incremental_dry_run_solvert::send(command);
+  smt_piped_solver_processt::send(command);
+}
+
+std::string smt_piped_solver_process_with_dumpt::description()
+{
+  return smt_piped_solver_processt::description();
+}
+
+smt_responset smt_piped_solver_process_with_dumpt::receive_response(
+  const std::unordered_map<irep_idt, smt_identifier_termt> &identifier_table)
+{
+  return smt_piped_solver_processt::receive_response(identifier_table);
+}

src/solvers/smt2_incremental/smt_solver_process.h

@@ -21,44 +21,44 @@ class smt_base_solver_processt
 
   /// \brief Converts given SMT2 command to SMT2 string and sends it to the
   ///    solver process.
-  virtual void send(const smt_commandt &command) = 0;
+  virtual void send(const smt_commandt &smt_command);
 
   virtual smt_responset
   receive_response(const std::unordered_map<irep_idt, smt_identifier_termt>
                      &identifier_table) = 0;
 
   virtual ~smt_base_solver_processt() = default;
+
+protected:
+  virtual void send(const std::string &)
+  {
+  }
 };
 
-class smt_piped_solver_processt : public smt_base_solver_processt
+class smt_piped_solver_processt : public virtual smt_base_solver_processt
 {
 public:
   /// \param command_line:
   ///   The command and arguments for invoking the smt2 solver.
   /// \param message_handler:
   ///   The messaging system to be used for logging purposes.
-  /// \param out_stream:
-  ///   Pointer to the stream to print the SMT formula. `nullptr` if no output.
   smt_piped_solver_processt(
     std::string command_line,
-    message_handlert &message_handler,
-    std::unique_ptr<std::ostream> out_stream);
+    message_handlert &message_handler);
 
   std::string description() override;
 
-  void send(const smt_commandt &smt_command) override;
-
   smt_responset receive_response(
     const std::unordered_map<irep_idt, smt_identifier_termt> &identifier_table)
     override;
 
   ~smt_piped_solver_processt() override = default;
 
 protected:
+  void send(const std::string &command_string) override;
+
   /// The command line used to start the process.
   std::string command_line_description;
-  /// Pointer to the stream to print the SMT formula. `nullptr` if no output.
-  std::unique_ptr<std::ostream> out_stream;
   /// The raw solver sub process.
   piped_processt process;
   /// For buffering / combining communications from the solver to cbmc.
@@ -69,7 +69,7 @@ class smt_piped_solver_processt : public smt_base_solver_processt
 
 /// Class for an incremental SMT solver used in combination with `--outfile`
 ///    argument where the solver is never run.
-class smt_incremental_dry_run_solvert : public smt_base_solver_processt
+class smt_incremental_dry_run_solvert : public virtual smt_base_solver_processt
 {
 public:
   /// \param message_handler:
@@ -85,8 +85,6 @@ class smt_incremental_dry_run_solvert : public smt_base_solver_processt
 
   std::string description() override;
 
-  void send(const smt_commandt &smt_command) override;
-
   /// \note This function returns always a valid unsat response.
   smt_responset receive_response(
     const std::unordered_map<irep_idt, smt_identifier_termt> &identifier_table)
@@ -95,11 +93,39 @@ class smt_incremental_dry_run_solvert : public smt_base_solver_processt
   ~smt_incremental_dry_run_solvert() override = default;
 
 protected:
+  void send(const std::string &smt_command) override;
+
   /// Pointer to the file stream to print the SMT formula. `nullptr` if output
   ///    is to `std::cout`.
   std::unique_ptr<std::ostream> file_stream;
   /// The output stream reference to print the SMT formula to.
   std::ostream &out_stream;
 };
 
+class smt_piped_solver_process_with_dumpt : public smt_piped_solver_processt,
+                                            smt_incremental_dry_run_solvert
+{
+public:
+  /// \param command_line:
+  ///   The command and arguments for invoking the smt2 solver.
+  /// \param message_handler:
+  ///   The messaging system to be used for logging purposes.
+  /// \param out_stream:
+  ///   Pointer to the stream to print the SMT formula.
+  smt_piped_solver_process_with_dumpt(
+    std::string command_line,
+    message_handlert &message_handler,
+    std::unique_ptr<std::ostream> out_stream);
+
+  void send(const std::string &smt_command) override;
+
+  std::string description() override;
+
+  smt_responset receive_response(
+    const std::unordered_map<irep_idt, smt_identifier_termt> &identifier_table)
+    override;
+
+  ~smt_piped_solver_process_with_dumpt() override = default;
+};
+
 #endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_SOLVER_PROCESS_H