cprover
Loading...
Searching...
No Matches
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
6class smt_commandt;
7
9#include <util/message.h>
10#include <util/piped_process.h>
11
12#include <sstream>
13#include <string>
14
16{
17public:
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{
31public:
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
48protected:
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 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
virtual const std::string & description()=0
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.
piped_processt process
The raw solver sub process.
Subprocess communication with pipes.