CBMC
Public Member Functions | Protected Attributes | List of all members
smt_piped_solver_processt Class Reference

#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, std::unique_ptr< std::ostream > out_stream)
 
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. More...
 
smt_responset receive_response (const std::unordered_map< irep_idt, smt_identifier_termt > &identifier_table) override
 
 ~smt_piped_solver_processt () override=default
 
- Public Member Functions inherited from smt_base_solver_processt
virtual ~smt_base_solver_processt ()=default
 

Protected Attributes

std::string command_line_description
 The command line used to start the process. More...
 
std::unique_ptr< std::ostream > out_stream
 Pointer to the stream to print the SMT formula. nullptr if no output. More...
 
piped_processt process
 The raw solver sub process. More...
 
std::stringstream response_stream
 For buffering / combining communications from the solver to cbmc. More...
 
messaget log
 For debug printing. More...
 

Detailed Description

Definition at line 33 of file smt_solver_process.h.

Constructor & Destructor Documentation

◆ smt_piped_solver_processt()

smt_piped_solver_processt::smt_piped_solver_processt ( std::string  command_line,
message_handlert &  message_handler,
std::unique_ptr< std::ostream >  out_stream 
)
Parameters
command_lineThe command and arguments for invoking the smt2 solver.
message_handlerThe messaging system to be used for logging purposes.
out_streamPointer to the stream to print the SMT formula. nullptr if no output.

Definition at line 12 of file smt_solver_process.cpp.

◆ ~smt_piped_solver_processt()

smt_piped_solver_processt::~smt_piped_solver_processt ( )
overridedefault

Member Function Documentation

◆ description()

const std::string & smt_piped_solver_processt::description ( )
overridevirtual

Implements smt_base_solver_processt.

Definition at line 23 of file smt_solver_process.cpp.

◆ receive_response()

smt_responset smt_piped_solver_processt::receive_response ( const std::unordered_map< irep_idt, smt_identifier_termt > &  identifier_table)
overridevirtual

Implements smt_base_solver_processt.

Definition at line 67 of file smt_solver_process.cpp.

◆ send()

void smt_piped_solver_processt::send ( const smt_commandt &  command)
overridevirtual

Converts given SMT2 command to SMT2 string and sends it to the solver process.

Implements smt_base_solver_processt.

Definition at line 28 of file smt_solver_process.cpp.

Member Data Documentation

◆ command_line_description

std::string smt_piped_solver_processt::command_line_description
protected

The command line used to start the process.

Definition at line 59 of file smt_solver_process.h.

◆ log

messaget smt_piped_solver_processt::log
protected

For debug printing.

Definition at line 67 of file smt_solver_process.h.

◆ out_stream

std::unique_ptr<std::ostream> smt_piped_solver_processt::out_stream
protected

Pointer to the stream to print the SMT formula. nullptr if no output.

Definition at line 61 of file smt_solver_process.h.

◆ process

piped_processt smt_piped_solver_processt::process
protected

The raw solver sub process.

Definition at line 63 of file smt_solver_process.h.

◆ response_stream

std::stringstream smt_piped_solver_processt::response_stream
protected

For buffering / combining communications from the solver to cbmc.

Definition at line 65 of file smt_solver_process.h.

The documentation for this class was generated from the following files: