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.
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.
std::unique_ptr< std::ostream >	out_stream
	Pointer to the stream to print the SMT formula. nullptr if no output.
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.

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_line	The command and arguments for invoking the smt2 solver.
message_handler	The messaging system to be used for logging purposes.
out_stream	Pointer 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:

• solvers/smt2_incremental/smt_solver_process.h
• solvers/smt2_incremental/smt_solver_process.cpp