cprover
smt_solver_process.cpp
Go to the documentation of this file.
1 // Author: Diffblue Ltd.
2 
4 
8 #include <util/exception_utils.h>
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 
22 {
24 }
25 
27 {
28  const std::string command_string = smt_to_smt2_string(smt_command);
29  log.debug() << "Sending command to SMT2 solver - " << command_string
30  << messaget::eom;
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 
45 static void handle_invalid_smt(
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;
60  response_stream << response_text;
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())
66  handle_invalid_smt(*validation_errors, log);
67  return *validation_result.get_if_valid();
68 }
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)