13 std::string command_line,
15 : command_line_description{
"\"" + command_line +
"\""},
29 log.
debug() <<
"Sending command to SMT2 solver - " << command_string
31 const auto response =
process.
send(command_string +
"\n");
46 const std::vector<std::string> &validation_errors,
49 for(
const std::string &message : validation_errors)
65 if(
const auto validation_errors = validation_result.get_if_error())
67 return *validation_result.get_if_valid();
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'.
message_handlert & get_message_handler()
send_responset send(const std::string &message)
Send a string message (command) to the child process.
std::string wait_receive()
Wait until a string is available and read a string from the child process' output.
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.
smt_responset receive_response() override
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)
piped_processt process
The raw solver sub process.
response_or_errort< smt_responset > validate_smt_response(const irept &parse_tree)
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_sortt &sort)
Streaming SMT data structures to a string based output stream.
optionalt< 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)