Refactor to separate solver communication from decision process

So that `smt2_incremental_decision_proceduret` can be unit tested in
isolation using a mock smt solver process.

Author: thomasspriggs

src/goto-checker/solver_factory.cpp

@@ -33,6 +33,7 @@ Author: Daniel Kroening, Peter Schrammel
 #include <solvers/sat/external_sat.h>
 #include <solvers/sat/satcheck.h>
 #include <solvers/smt2_incremental/smt2_incremental_decision_procedure.h>
+#include <solvers/smt2_incremental/smt_solver_process.h>
 #include <solvers/strings/string_refinement.h>
 
 solver_factoryt::solver_factoryt(
@@ -330,10 +331,12 @@ 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);
 
   return util_make_unique<solvert>(
     util_make_unique<smt2_incremental_decision_proceduret>(
-      ns, std::move(solver_command), message_handler));
+      ns, std::move(solver_process), message_handler));
 }
 
 std::unique_ptr<solver_factoryt::solvert>

src/solvers/Makefile

@@ -199,6 +199,7 @@ SRC = $(BOOLEFORCE_SRC) \
       smt2_incremental/smt_core_theory.cpp \
       smt2_incremental/smt_logics.cpp \
       smt2_incremental/smt_options.cpp \
+      smt2_incremental/smt_solver_process.cpp \
       smt2_incremental/smt_sorts.cpp \
       smt2_incremental/smt_terms.cpp \
       smt2_incremental/smt_to_smt2_string.cpp \

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

@@ -5,8 +5,8 @@
 #include <solvers/smt2_incremental/convert_expr_to_smt.h>
 #include <solvers/smt2_incremental/smt_commands.h>
 #include <solvers/smt2_incremental/smt_core_theory.h>
+#include <solvers/smt2_incremental/smt_solver_process.h>
 #include <solvers/smt2_incremental/smt_terms.h>
-#include <solvers/smt2_incremental/smt_to_smt2_string.h>
 #include <util/expr.h>
 #include <util/namespace.h>
 #include <util/range.h>
@@ -74,7 +74,7 @@ void smt2_incremental_decision_proceduret::define_dependent_functions(
         const smt_define_function_commandt function{
           symbol->name, {}, convert_expr_to_smt(symbol->value)};
         expression_identifiers.emplace(*symbol_expr, function.identifier());
-        send_to_solver(function);
+        solver_process->send(function);
       }
       else
       {
@@ -83,7 +83,7 @@ void smt2_incremental_decision_proceduret::define_dependent_functions(
             identifier, convert_type_to_smt_sort(symbol_expr->type())),
           {}};
         expression_identifiers.emplace(*symbol_expr, function.identifier());
-        send_to_solver(function);
+        solver_process->send(function);
       }
     }
     to_be_defined.pop();
@@ -92,16 +92,16 @@ void smt2_incremental_decision_proceduret::define_dependent_functions(
 
 smt2_incremental_decision_proceduret::smt2_incremental_decision_proceduret(
   const namespacet &_ns,
-  std::string _solver_command,
+  std::unique_ptr<smt_base_solver_processt> _solver_process,
   message_handlert &message_handler)
   : ns{_ns},
-    solver_command(std::move(_solver_command)),
     number_of_solver_calls{0},
-    solver_process{split_string(solver_command, ' ', false, true)},
+    solver_process(std::move(_solver_process)),
     log{message_handler}
 {
-  send_to_solver(smt_set_option_commandt{smt_option_produce_modelst{true}});
-  send_to_solver(smt_set_logic_commandt{
+  solver_process->send(
+    smt_set_option_commandt{smt_option_produce_modelst{true}});
+  solver_process->send(smt_set_logic_commandt{
     smt_logic_quantifier_free_uninterpreted_functions_bit_vectorst{}});
 }
 
@@ -119,7 +119,7 @@ void smt2_incremental_decision_proceduret::ensure_handle_for_expr_defined(
   smt_define_function_commandt function{
     "B" + std::to_string(handle_sequence()), {}, convert_expr_to_smt(expr)};
   expression_handle_identifiers.emplace(expr, function.identifier());
-  send_to_solver(function);
+  solver_process->send(function);
 }
 
 exprt smt2_incremental_decision_proceduret::handle(const exprt &expr)
@@ -143,7 +143,7 @@ void smt2_incremental_decision_proceduret::print_assignment(
 std::string
 smt2_incremental_decision_proceduret::decision_procedure_text() const
 {
-  return "incremental SMT2 solving via \"" + solver_command + "\"";
+  return "incremental SMT2 solving via " + solver_process->description();
 }
 
 std::size_t
@@ -169,7 +169,7 @@ void smt2_incremental_decision_proceduret::set_to(const exprt &expr, bool value)
   }();
   if(!value)
     converted_term = smt_core_theoryt::make_not(converted_term);
-  send_to_solver(smt_assert_commandt{converted_term});
+  solver_process->send(smt_assert_commandt{converted_term});
 }
 
 void smt2_incremental_decision_proceduret::push(
@@ -196,17 +196,7 @@ void smt2_incremental_decision_proceduret::pop()
 decision_proceduret::resultt smt2_incremental_decision_proceduret::dec_solve()
 {
   ++number_of_solver_calls;
-  send_to_solver(smt_check_sat_commandt{});
-  const auto result = solver_process.wait_receive();
-  log.debug() << "Solver response - " << result << messaget::eom;
-  UNIMPLEMENTED_FEATURE("parsing of solver response.");
-}
-
-void smt2_incremental_decision_proceduret::send_to_solver(
-  const smt_commandt &command)
-{
-  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");
+  solver_process->send(smt_check_sat_commandt{});
+  const smt_responset result = solver_process->receive_response();
+  UNIMPLEMENTED_FEATURE("handling solver response.");
 }

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h

@@ -9,29 +9,30 @@
 #include <solvers/smt2_incremental/smt_terms.h>
 #include <solvers/stack_decision_procedure.h>
 #include <util/message.h>
-#include <util/piped_process.h>
 #include <util/std_expr.h>
 
+#include <memory>
 #include <unordered_map>
 #include <unordered_set>
 
 class smt_commandt;
 class message_handlert;
 class namespacet;
+class smt_base_solver_processt;
 
 class smt2_incremental_decision_proceduret final
   : public stack_decision_proceduret
 {
 public:
   /// \param _ns: Namespace for looking up the expressions which symbol_exprts
   ///   relate to.
-  /// \param solver_command:
-  ///   The command and arguments for invoking the smt2 solver.
+  /// \param solver_process:
+  ///   The smt2 solver process communication interface.
   /// \param message_handler:
   ///   The messaging system to be used for logging purposes.
   explicit smt2_incremental_decision_proceduret(
     const namespacet &_ns,
-    std::string solver_command,
+    std::unique_ptr<smt_base_solver_processt> solver_process,
     message_handlert &message_handler);
 
   // Implementation of public decision_proceduret member functions.
@@ -50,21 +51,16 @@ class smt2_incremental_decision_proceduret final
 protected:
   // Implementation of protected decision_proceduret member function.
   resultt dec_solve() override;
-  /// \brief Converts given SMT2 command to SMT2 string and sends it to the
-  ///    solver process.
-  void send_to_solver(const smt_commandt &command);
   /// \brief Defines any functions which \p expr depends on, which have not yet
   ///   been defined, along with their dependencies in turn.
   void define_dependent_functions(const exprt &expr);
   void ensure_handle_for_expr_defined(const exprt &expr);
 
   const namespacet &ns;
 
-  /// This is where we store the solver command for reporting the solver used.
-  std::string solver_command;
   size_t number_of_solver_calls;
 
-  piped_processt solver_process;
+  std::unique_ptr<smt_base_solver_processt> solver_process;
   messaget log;
 
   class sequencet

src/solvers/smt2_incremental/smt_responses.h

@@ -0,0 +1,21 @@
+// Author: Diffblue Ltd.
+
+#ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_RESPONSES_H
+#define CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_RESPONSES_H
+
+#include <util/irep.h>
+
+class smt_responset : protected irept
+{
+public:
+  // smt_responset does not support the notion of an empty / null state. Use
+  // optionalt<smt_responset> instead if an empty response is required.
+  smt_responset() = delete;
+
+  using irept::pretty;
+
+protected:
+  using irept::irept;
+};
+
+#endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_RESPONSES_H

src/solvers/smt2_incremental/smt_solver_process.cpp

@@ -0,0 +1,36 @@
+// Author: Diffblue Ltd.
+
+#include <solvers/smt2_incremental/smt_solver_process.h>
+
+#include <solvers/smt2_incremental/smt_to_smt2_string.h>
+#include <util/invariant.h>
+#include <util/string_utils.h>
+
+smt_piped_solver_processt::smt_piped_solver_processt(
+  std::string command_line,
+  message_handlert &message_handler)
+  : command_line_description{"\"" + command_line + "\""},
+    process{split_string(command_line, ' ', false, true)},
+    log{message_handler}
+{
+}
+
+const std::string &smt_piped_solver_processt::description()
+{
+  return command_line_description;
+}
+
+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;
+  process.send(command_string + "\n");
+}
+
+smt_responset smt_piped_solver_processt::receive_response()
+{
+  const auto response_text = process.wait_receive();
+  log.debug() << "Solver response - " << response_text << messaget::eom;
+  UNIMPLEMENTED_FEATURE("parsing of solver response.");
+}

src/solvers/smt2_incremental/smt_solver_process.h

@@ -0,0 +1,56 @@
+// Author: Diffblue Ltd.
+
+#ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_SOLVER_PROCESS_H
+#define CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_SOLVER_PROCESS_H
+
+class smt_commandt;
+
+#include <solvers/smt2_incremental/smt_responses.h>
+#include <util/message.h>
+#include <util/piped_process.h>
+
+#include <string>
+
+class smt_base_solver_processt
+{
+public:
+  virtual const std::string &description() = 0;
+
+  /// \brief Converts given SMT2 command to SMT2 string and sends it to the
+  ///    solver process.
+  virtual void send(const smt_commandt &command) = 0;
+
+  virtual smt_responset receive_response() = 0;
+
+  virtual ~smt_base_solver_processt() = default;
+};
+
+class smt_piped_solver_processt : public 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.
+  smt_piped_solver_processt(
+    std::string command_line,
+    message_handlert &message_handler);
+
+  const std::string &description() override;
+
+  void send(const smt_commandt &smt_command) override;
+
+  smt_responset receive_response() override;
+
+  ~smt_piped_solver_processt() override = default;
+
+protected:
+  /// The command line used to start the process.
+  std::string command_line_description;
+  /// The raw solver sub process.
+  piped_processt process;
+  /// For debug printing.
+  messaget log;
+};
+
+#endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_SOLVER_PROCESS_H