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/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

@@ -2,12 +2,20 @@
 
 #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)
+  : solver_command{std::move(_solver_command)},
+    number_of_solver_calls{0},
+    solver_process{split_string(solver_command, ' ', false, true)}
 {
+  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 +79,9 @@ 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)
+{
+  solver_process.send(smt_to_smt2_string(command) + "\n");
+}

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h

@@ -7,6 +7,9 @@
 #define CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT2_INCREMENTAL_DECISION_PROCEDURE_H
 
 #include <solvers/stack_decision_procedure.h>
+#include <util/piped_process.h>
+
+class smt_commandt;
 
 class smt2_incremental_decision_proceduret final
   : public stack_decision_proceduret
@@ -32,10 +35,15 @@ 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;
 };
 
 #endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT2_INCREMENTAL_DECISION_PROCEDURE_H