13 std::string command_line,
31 log.debug() <<
"Sending command to SMT2 solver - " << command_string
42 const auto response =
process.send(command_string +
"\n");
57 const std::vector<std::string> &validation_errors,
60 for(
const std::string &message : validation_errors)
68 const std::unordered_map<irep_idt, smt_identifier_termt> &identifier_table)
70 const auto response_text =
process.wait_receive();
76 const auto validation_result =
78 if(
const auto validation_errors = validation_result.get_if_error())
80 return *validation_result.get_if_valid();
104 const std::unordered_map<irep_idt, smt_identifier_termt> &identifier_table)
Thrown when an unexpected error occurs during the analysis (e.g., when the SAT solver returns an erro...
Thrown when failing to deserialize a value from some low level format, like JSON or raw bytes.
Class that provides messages with a built-in verbosity 'level'.
const std::string & description() override
smt_responset receive_response(const std::unordered_map< irep_idt, smt_identifier_termt > &identifier_table) override
void send(const smt_commandt &smt_command) override
Converts given SMT2 command to SMT2 string and sends it to the solver process.
std::unique_ptr< std::ostream > file_stream
Pointer to the file stream to print the SMT formula.
std::ostream & out_stream
The output stream reference to print the SMT formula to.
messaget log
For debug printing.
smt_incremental_dry_run_solvert(message_handlert &message_handler, std::ostream &out_stream, std::unique_ptr< std::ostream > file_stream)
const std::string desc
Description of the current solver.
messaget log
For debug printing.
std::string command_line_description
The command line used to start the process.
void send(const smt_commandt &smt_command) override
Converts given SMT2 command to SMT2 string and sends it to the solver process.
const std::string & description() override
std::stringstream response_stream
For buffering / combining communications from the solver to cbmc.
smt_piped_solver_processt(std::string command_line, message_handlert &message_handler, std::unique_ptr< std::ostream > out_stream)
smt_responset receive_response(const std::unordered_map< irep_idt, smt_identifier_termt > &identifier_table) override
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.
response_or_errort< smt_responset > validate_smt_response(const irept &parse_tree, const std::unordered_map< irep_idt, smt_identifier_termt > &identifier_table)
static void handle_invalid_smt(const std::vector< std::string > &validation_errors, messaget &log)
Log messages and throw exception.
std::string smt_to_smt2_string(const smt_indext &index)
Streaming SMT data structures to a string based output stream.
std::optional< irept > smt2irep(std::istream &in, message_handlert &message_handler)
returns an irep for an SMT-LIB2 expression read from a given stream returns {} when EOF is encountere...
#define UNREACHABLE
This should be used to mark dead code.
void split_string(const std::string &s, char delim, std::vector< std::string > &result, bool strip, bool remove_empty)