Implement sending commands to solver in incremental SMT2 backend

regression/cbmc-incr-smt2/nondeterministic-int-assert/incremental_solver_called.desc

@@ -1,7 +1,7 @@
 CORE
 test.c
---incremental-smt2-solver z3
-Passing problem to incremental SMT2 solving via "z3"
+--incremental-smt2-solver "z3 --smt2 -in"
+Passing problem to incremental SMT2 solving via "z3 --smt2 -in"
 ^EXIT=(0|127|134|137)$
 ^SIGNAL=0$
 identifier: main::1::x

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

@@ -2,12 +2,22 @@
 
 #include "smt2_incremental_decision_procedure.h"
 
+#include <solvers/smt2_incremental/smt_commands.h>
+#include <solvers/smt2_incremental/smt_to_smt2_string.h>
 #include <util/expr.h>
+#include <util/string_utils.h>
 
 smt2_incremental_decision_proceduret::smt2_incremental_decision_proceduret(
-  std::string solver_command)
-  : solver_command{std::move(solver_command)}, number_of_solver_calls{0}
+  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)},
+    log{message_handler}
 {
+  send_to_solver(smt_set_option_commandt{smt_option_produce_modelst{true}});
+  send_to_solver(smt_set_logic_commandt{
+    smt_logic_quantifier_free_uninterpreted_functions_bit_vectorst{}});
 }
 
 exprt smt2_incremental_decision_proceduret::handle(const exprt &expr)
@@ -71,3 +81,12 @@ decision_proceduret::resultt smt2_incremental_decision_proceduret::dec_solve()
   ++number_of_solver_calls;
   UNIMPLEMENTED_FEATURE("solving.");
 }
+
+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");
+}

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h

@@ -7,14 +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;
@@ -32,10 +41,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);
 
   /// 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;
+  messaget log;
 };
 
 #endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT2_INCREMENTAL_DECISION_PROCEDURE_H