smt_incremental_dry_run_solvert Class Reference

Class for an incremental SMT solver used in combination with --outfile argument where the solver is never run. More...

#include <smt_solver_process.h>

Inheritance diagram for smt_incremental_dry_run_solvert:

Collaboration diagram for smt_incremental_dry_run_solvert:

Public Member Functions
	smt_incremental_dry_run_solvert (message_handlert &message_handler, std::ostream &out_stream, std::unique_ptr< std::ostream > file_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_incremental_dry_run_solvert () override=default
Public Member Functions inherited from smt_base_solver_processt
virtual	~smt_base_solver_processt ()=default

Protected Attributes
std::unique_ptr< std::ostream >	file_stream
	Pointer to the file stream to print the SMT formula. More...
std::ostream &	out_stream
	The output stream reference to print the SMT formula to. More...
messaget	log
	For debug printing. More...
const std::string	desc = "SMT2 incremental dry-run"
	Description of the current solver. More...

Detailed Description

Class for an incremental SMT solver used in combination with --outfile argument where the solver is never run.

Definition at line 72 of file smt_solver_process.h.

Constructor & Destructor Documentation

smt_incremental_dry_run_solvert()

smt_incremental_dry_run_solvert::smt_incremental_dry_run_solvert	(	message_handlert &	message_handler,
		std::ostream &	out_stream,
		std::unique_ptr< std::ostream >	file_stream
	)

Parameters

message_handler	The messaging system to be used for logging purposes.
out_stream	Reference to the stream to print the SMT formula.
file_stream	Pointer to the file stream to print the SMT formula into. nullptr if output is to std::cout.

Definition at line 83 of file smt_solver_process.cpp.

~smt_incremental_dry_run_solvert()

smt_incremental_dry_run_solvert::~smt_incremental_dry_run_solvert ( )

overridedefault

Member Function Documentation

description()

const std::string & smt_incremental_dry_run_solvert::description ( )

overridevirtual

Implements smt_base_solver_processt.

Definition at line 93 of file smt_solver_process.cpp.

receive_response()

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

overridevirtual

Note

This function returns always a valid unsat response.

Implements smt_base_solver_processt.

Definition at line 103 of file smt_solver_process.cpp.

send()

void smt_incremental_dry_run_solvert::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 98 of file smt_solver_process.cpp.

Member Data Documentation

desc

const std::string smt_incremental_dry_run_solvert::desc = "SMT2 incremental dry-run"

protected

Description of the current solver.

Definition at line 108 of file smt_solver_process.h.

file_stream

std::unique_ptr<std::ostream> smt_incremental_dry_run_solvert::file_stream

protected

Pointer to the file stream to print the SMT formula.

nullptr if output is to std::cout.

Definition at line 101 of file smt_solver_process.h.

log

messaget smt_incremental_dry_run_solvert::log

protected

For debug printing.

Definition at line 105 of file smt_solver_process.h.

out_stream

std::ostream& smt_incremental_dry_run_solvert::out_stream

protected

The output stream reference to print the SMT formula to.

Definition at line 103 of file smt_solver_process.h.

---

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

• /home/runner/work/cbmc/cbmc/src/solvers/smt2_incremental/smt_solver_process.h
• /home/runner/work/cbmc/cbmc/src/solvers/smt2_incremental/smt_solver_process.cpp