cprover
Loading...
Searching...
No Matches
smt_solver_process.cpp
Go to the documentation of this file.
1// Author: Diffblue Ltd.
2
4
9#include <util/invariant.h>
10#include <util/string_utils.h>
11
13 std::string command_line,
14 message_handlert &message_handler)
15 : command_line_description{"\"" + command_line + "\""},
16 process{split_string(command_line, ' ', false, true)},
17 log{message_handler}
18{
19}
20
25
27{
29 log.debug() << "Sending command to SMT2 solver - " << command_string
31 const auto response = process.send(command_string + "\n");
32 switch(response)
33 {
35 return;
37 throw analysis_exceptiont{"Sending to SMT solver sub process failed."};
39 throw analysis_exceptiont{"SMT solver sub process is in error state."};
40 }
42}
43
46 const std::vector<std::string> &validation_errors,
47 messaget &log)
48{
49 for(const std::string &message : validation_errors)
50 {
51 log.error() << message << messaget::eom;
52 }
53 throw analysis_exceptiont{"Invalid SMT response received from solver."};
54}
55
57{
58 const auto response_text = process.wait_receive();
59 log.debug() << "Solver response - " << response_text << messaget::eom;
61 const auto parse_tree = smt2irep(response_stream, log.get_message_handler());
62 if(!parse_tree)
63 throw deserialization_exceptiont{"Incomplete SMT response."};
64 const auto validation_result = validate_smt_response(*parse_tree);
65 if(const auto validation_errors = validation_result.get_if_error())
67 return *validation_result.get_if_valid();
68}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
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'.
Definition message.h:155
mstreamt & error() const
Definition message.h:399
mstreamt & debug() const
Definition message.h:429
message_handlert & get_message_handler()
Definition message.h:184
static eomt eom
Definition message.h:297
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...
Definition smt2irep.cpp:91
#define UNREACHABLE
This should be used to mark dead code.
Definition invariant.h:503
void split_string(const std::string &s, char delim, std::vector< std::string > &result, bool strip, bool remove_empty)