cprover
|
#include <smt_solver_process.h>
Public Member Functions | |
smt_piped_solver_processt (std::string command_line, message_handlert &message_handler) | |
const std::string & | description () override |
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 | |
![]() | |
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_responset | receive_response ()=0 |
virtual | ~smt_base_solver_processt ()=default |
Protected Attributes | |
std::string | command_line_description |
The command line used to start the process. | |
piped_processt | process |
The raw solver sub process. | |
std::stringstream | response_stream |
For buffering / combining communications from the solver to cbmc. | |
messaget | log |
For debug printing. | |
Definition at line 29 of file smt_solver_process.h.
smt_piped_solver_processt::smt_piped_solver_processt | ( | std::string | command_line, |
message_handlert & | message_handler | ||
) |
command_line | The command and arguments for invoking the smt2 solver. |
message_handler | The messaging system to be used for logging purposes. |
Definition at line 12 of file smt_solver_process.cpp.
|
overridedefault |
|
overridevirtual |
Implements smt_base_solver_processt.
Definition at line 21 of file smt_solver_process.cpp.
|
overridevirtual |
Implements smt_base_solver_processt.
Definition at line 56 of file smt_solver_process.cpp.
|
overridevirtual |
Converts given SMT2 command to SMT2 string and sends it to the solver process.
Implements smt_base_solver_processt.
Definition at line 26 of file smt_solver_process.cpp.
|
protected |
The command line used to start the process.
Definition at line 50 of file smt_solver_process.h.
|
protected |
For debug printing.
Definition at line 56 of file smt_solver_process.h.
|
protected |
The raw solver sub process.
Definition at line 52 of file smt_solver_process.h.
|
protected |
For buffering / combining communications from the solver to cbmc.
Definition at line 54 of file smt_solver_process.h.