Add debug logging of commands sent to SMT2 solver

So that we can see the text sent to the solver when debugging and so
that the text can be checked in regression tests. The commands are shown
as debug output messages rather than written to file because a file
based approach is not well suited to incremental solving.

Author: thomasspriggs

src/goto-checker/solver_factory.cpp

@@ -333,7 +333,7 @@ solver_factoryt::get_incremental_smt2(std::string solver_command)
 
   return util_make_unique<solvert>(
     util_make_unique<smt2_incremental_decision_proceduret>(
-      std::move(solver_command)));
+      std::move(solver_command), message_handler));
 }
 
 std::unique_ptr<solver_factoryt::solvert>

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

@@ -8,10 +8,12 @@
 #include <util/string_utils.h>
 
 smt2_incremental_decision_proceduret::smt2_incremental_decision_proceduret(
-  std::string _solver_command)
-  : solver_command{std::move(_solver_command)},
+  std::string _solver_command,
+  message_handlert &message_handler)
+  : solver_command(std::move(_solver_command)),
     number_of_solver_calls{0},
-    solver_process{split_string(solver_command, ' ', false, true)}
+    solver_process{split_string(solver_command, ' ', false, true)},
+    log{message_handler}
 {
   send_to_solver(smt_set_option_commandt{smt_option_produce_modelst{true}});
   send_to_solver(smt_set_logic_commandt{
@@ -83,5 +85,8 @@ decision_proceduret::resultt smt2_incremental_decision_proceduret::dec_solve()
 void smt2_incremental_decision_proceduret::send_to_solver(
   const smt_commandt &command)
 {
-  solver_process.send(smt_to_smt2_string(command) + "\n");
+  const std::string command_string = smt_to_smt2_string(command);
+  log.debug() << "Sending command to SMT2 solver - " << command_string
+              << messaget::eom;
+  solver_process.send(command_string + "\n");
 }

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h

@@ -7,17 +7,23 @@
 #define CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT2_INCREMENTAL_DECISION_PROCEDURE_H
 
 #include <solvers/stack_decision_procedure.h>
+#include <util/message.h>
 #include <util/piped_process.h>
 
 class smt_commandt;
+class message_handlert;
 
 class smt2_incremental_decision_proceduret final
   : public stack_decision_proceduret
 {
 public:
-  /// \param solver_command: The command and arguments for invoking the smt2
-  ///                        solver.
-  explicit smt2_incremental_decision_proceduret(std::string solver_command);
+  /// \param solver_command:
+  ///   The command and arguments for invoking the smt2 solver.
+  /// \param message_handler:
+  ///   The messaging system to be used for logging purposes.
+  explicit smt2_incremental_decision_proceduret(
+    std::string solver_command,
+    message_handlert &message_handler);
 
   // Implementation of public decision_proceduret member functions.
   exprt handle(const exprt &expr) override;
@@ -44,6 +50,7 @@ class smt2_incremental_decision_proceduret final
   size_t number_of_solver_calls;
 
   piped_processt solver_process;
+  messaget log;
 };
 
 #endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT2_INCREMENTAL_DECISION_PROCEDURE_H