Make decision procedure use piped solver

Author: thomasspriggs

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

@@ -2,11 +2,15 @@
 
 #include "smt2_incremental_decision_procedure.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)}
 {
 }
 
@@ -71,3 +75,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