Log SMT formula to file for new incremental solver

Author: Enrico Steffinlongo

src/goto-checker/solver_factory.cpp

@@ -148,7 +148,10 @@ std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_solver()
   const auto incremental_smt2_solver =
     options.get_option("incremental-smt2-solver");
   if(!incremental_smt2_solver.empty())
-    return get_incremental_smt2(incremental_smt2_solver);
+  {
+    const auto out_filename = options.get_option("outfile");
+    return get_incremental_smt2(incremental_smt2_solver, out_filename);
+  }
   if(options.get_bool_option("smt2"))
     return get_smt2(get_smt2_solver_type());
   return get_default();
@@ -329,12 +332,30 @@ solver_factoryt::get_string_refinement()
     std::move(decision_procedure), std::move(prop));
 }
 
-std::unique_ptr<solver_factoryt::solvert>
-solver_factoryt::get_incremental_smt2(std::string solver_command)
+std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_incremental_smt2(
+  std::string solver_command,
+  std::string outfile)
 {
   no_beautification();
+
+  std::unique_ptr<std::ofstream> out = nullptr;
+  if(!outfile.empty())
+  {
+#ifdef _MSC_VER
+    out = util_make_unique<std::ofstream>(widen(outfile));
+#else
+    out = util_make_unique<std::ofstream>(outfile);
+#endif
+
+    if(!*out)
+    {
+      throw invalid_command_line_argument_exceptiont(
+        "failed to open file: " + outfile, "--outfile");
+    }
+  }
+
   auto solver_process = util_make_unique<smt_piped_solver_processt>(
-    std::move(solver_command), message_handler);
+    std::move(solver_command), message_handler, std::move(out));
 
   return util_make_unique<solvert>(
     util_make_unique<smt2_incremental_decision_proceduret>(

src/goto-checker/solver_factory.h

@@ -76,7 +76,8 @@ class solver_factoryt final
   std::unique_ptr<solvert> get_external_sat();
   std::unique_ptr<solvert> get_bv_refinement();
   std::unique_ptr<solvert> get_string_refinement();
-  std::unique_ptr<solvert> get_incremental_smt2(std::string solver_command);
+  std::unique_ptr<solvert>
+  get_incremental_smt2(std::string solver_command, std::string outfile);
   std::unique_ptr<solvert> get_smt2(smt2_dect::solvert solver);
 
   smt2_dect::solvert get_smt2_solver_type() const;

src/solvers/smt2_incremental/smt_solver_process.cpp

@@ -11,8 +11,10 @@
 
 smt_piped_solver_processt::smt_piped_solver_processt(
   std::string command_line,
-  message_handlert &message_handler)
+  message_handlert &message_handler,
+  std::unique_ptr<std::ostream> out_stream)
   : command_line_description{"\"" + command_line + "\""},
+    out_stream(std::move(out_stream)),
     process{split_string(command_line, ' ', false, true), message_handler},
     log{message_handler}
 {
@@ -28,6 +30,15 @@ void smt_piped_solver_processt::send(const smt_commandt &smt_command)
   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 to flush the stream as it is a debugging functionality,
+    // and we can 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)
   {

src/solvers/smt2_incremental/smt_solver_process.h

@@ -5,10 +5,12 @@
 
 class smt_commandt;
 
-#include <solvers/smt2_incremental/smt_responses.h>
 #include <util/message.h>
 #include <util/piped_process.h>
 
+#include <solvers/smt2_incremental/smt_responses.h>
+
+#include <memory>
 #include <sstream>
 #include <string>
 
@@ -35,9 +37,12 @@ class smt_piped_solver_processt : public smt_base_solver_processt
   ///   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);
+    message_handlert &message_handler,
+    std::unique_ptr<std::ostream> out_stream);
 
   const std::string &description() override;
 
@@ -52,6 +57,8 @@ class smt_piped_solver_processt : public smt_base_solver_processt
 protected:
   /// 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.