Log SMT formula to file for new incremental solver

Author: Enrico Steffinlongo

src/goto-checker/solver_factory.cpp

@@ -329,12 +329,54 @@ solver_factoryt::get_string_refinement()
     std::move(decision_procedure), std::move(prop));
 }
 
+std::unique_ptr<std::ofstream> open_outfile_and_check(
+  const std::string &filename,
+  message_handlert &message_handler)
+{
+  if(filename.empty())
+    return nullptr;
+
+#ifdef _MSC_VER
+  auto out = util_make_unique<std::ofstream>(widen(filename));
+#else
+  auto out = util_make_unique<std::ofstream>(filename);
+#endif
+
+  if(!*out)
+  {
+    throw invalid_command_line_argument_exceptiont(
+      "failed to open file: " + filename, "--outfile");
+  }
+
+  messaget log(message_handler);
+  log.status() << "Outputting SMTLib formula to file: " << filename
+               << messaget::eom;
+  return out;
+}
+
 std::unique_ptr<solver_factoryt::solvert>
 solver_factoryt::get_incremental_smt2(std::string solver_command)
 {
   no_beautification();
-  auto solver_process = util_make_unique<smt_piped_solver_processt>(
-    std::move(solver_command), message_handler);
+
+  const std::string outfile_arg = options.get_option("outfile");
+
+  std::unique_ptr<smt_base_solver_processt> solver_process = nullptr;
+
+  if(!outfile_arg.empty())
+  {
+    bool on_std_out = outfile_arg == "-";
+    std::unique_ptr<std::ostream> outfile =
+      on_std_out ? nullptr
+                 : open_outfile_and_check(outfile_arg, message_handler);
+    solver_process = util_make_unique<smt_incremental_dry_run_solvert>(
+      message_handler, on_std_out ? std::cout : *outfile, std::move(outfile));
+  }
+  else
+  {
+    solver_process = util_make_unique<smt_piped_solver_processt>(
+      std::move(solver_command), message_handler);
+  }
 
   return util_make_unique<solvert>(
     util_make_unique<smt2_incremental_decision_proceduret>(
@@ -390,17 +432,7 @@ solver_factoryt::get_smt2(smt2_dect::solvert solver)
   }
   else
   {
-#ifdef _MSC_VER
-    auto out = util_make_unique<std::ofstream>(widen(filename));
-#else
-    auto out = util_make_unique<std::ofstream>(filename);
-#endif
-
-    if(!*out)
-    {
-      throw invalid_command_line_argument_exceptiont(
-        "failed to open file: " + filename, "--outfile");
-    }
+    auto out = open_outfile_and_check(filename, message_handler);
 
     auto smt2_conv = util_make_unique<smt2_convt>(
       ns,

src/solvers/smt2_incremental/smt_solver_process.cpp

@@ -68,3 +68,33 @@ smt_responset smt_piped_solver_processt::receive_response(
     handle_invalid_smt(*validation_errors, log);
   return *validation_result.get_if_valid();
 }
+
+smt_incremental_dry_run_solvert::smt_incremental_dry_run_solvert(
+  message_handlert &message_handler,
+  std::ostream &out_stream,
+  std::unique_ptr<std::ostream> file_stream)
+  : file_stream(std::move(file_stream)),
+    out_stream(out_stream),
+    log(message_handler)
+{
+}
+
+const std::string &smt_incremental_dry_run_solvert::description()
+{
+  return desc;
+}
+
+void smt_incremental_dry_run_solvert::send(const smt_commandt &smt_command)
+{
+  out_stream << smt_to_smt2_string(smt_command) << '\n';
+}
+
+smt_responset smt_incremental_dry_run_solvert::receive_response(
+  const std::unordered_map<irep_idt, smt_identifier_termt> &identifier_table)
+{
+  // Using `smt_unsat_responset` as response because the decision-procedure will
+  // terminate anyway (stop-on-fail), it is not reported to the user as for
+  // `unknown`, and does not trigger a subsequent invocation to get the model
+  // (as a `smt_sat_responset` answer will trigger).
+  return smt_check_sat_responset{smt_unsat_responset{}};
+}

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>
 
@@ -60,4 +62,45 @@ class smt_piped_solver_processt : public smt_base_solver_processt
   messaget log;
 };
 
+/// 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
+{
+public:
+  /// \param message_handler:
+  ///   The messaging system to be used for logging purposes.
+  /// \param out_stream:
+  ///   Reference to the stream to print the SMT formula.
+  /// \param file_stream:
+  ///   Pointer to the file stream to print the SMT formula into. `nullptr` if
+  ///     output is to `std::cout`.
+  smt_incremental_dry_run_solvert(
+    message_handlert &message_handler,
+    std::ostream &out_stream,
+    std::unique_ptr<std::ostream> file_stream);
+
+  const 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)
+    override;
+
+  ~smt_incremental_dry_run_solvert() override = default;
+
+protected:
+  /// 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;
+  /// For debug printing.
+  messaget log;
+
+  /// Description of the current solver
+  const std::string desc = "SMT2 incremental dry-run";
+};
+
 #endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_SOLVER_PROCESS_H