|
cprover
|
#include <smt_solver_process.h>
Inheritance diagram for smt_piped_solver_processt:
Collaboration diagram for smt_piped_solver_processt: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 | |
Public Member Functions inherited from smt_base_solver_processt | |
| 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.