cprover
smt_solver_process.h
Go to the documentation of this file.
1 // Author: Diffblue Ltd.
2 
3 #ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_SOLVER_PROCESS_H
4 #define CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_SOLVER_PROCESS_H
5 
6 class smt_commandt;
7 
9 #include <util/message.h>
10 #include <util/piped_process.h>
11 
12 #include <sstream>
13 #include <string>
14 
16 {
17 public:
18  virtual const std::string &description() = 0;
19 
22  virtual void send(const smt_commandt &command) = 0;
23 
25 
26  virtual ~smt_base_solver_processt() = default;
27 };
28 
30 {
31 public:
37  std::string command_line,
38  message_handlert &message_handler);
39 
40  const std::string &description() override;
41 
42  void send(const smt_commandt &smt_command) override;
43 
45 
46  ~smt_piped_solver_processt() override = default;
47 
48 protected:
54  std::stringstream response_stream;
57 };
58 
59 #endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_SOLVER_PROCESS_H
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
virtual smt_responset receive_response()=0
virtual const std::string & description()=0
virtual void send(const smt_commandt &command)=0
Converts given SMT2 command to SMT2 string and sends it to the solver process.
virtual ~smt_base_solver_processt()=default
messaget log
For debug printing.
std::string command_line_description
The command line used to start the process.
void send(const smt_commandt &smt_command) override
Converts given SMT2 command to SMT2 string and sends it to the solver process.
smt_responset receive_response() override
~smt_piped_solver_processt() override=default
const std::string & description() override
std::stringstream response_stream
For buffering / combining communications from the solver to cbmc.
smt_piped_solver_processt(std::string command_line, message_handlert &message_handler)
piped_processt process
The raw solver sub process.
Subprocess communication with pipes.