Add interpretation of SMT check-sat responses

So that CBMC can report something useful rather than just reaching an
UNIMPLEMENTED, when solving is complete.

Author: thomasspriggs

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

@@ -5,10 +5,12 @@
 #include <solvers/smt2_incremental/convert_expr_to_smt.h>
 #include <solvers/smt2_incremental/smt_commands.h>
 #include <solvers/smt2_incremental/smt_core_theory.h>
+#include <solvers/smt2_incremental/smt_responses.h>
 #include <solvers/smt2_incremental/smt_solver_process.h>
 #include <solvers/smt2_incremental/smt_terms.h>
 #include <util/expr.h>
 #include <util/namespace.h>
+#include <util/nodiscard.h>
 #include <util/range.h>
 #include <util/std_expr.h>
 #include <util/string_utils.h>
@@ -196,10 +198,29 @@ void smt2_incremental_decision_proceduret::pop()
   UNIMPLEMENTED_FEATURE("`pop`.");
 }
 
+NODISCARD
+static decision_proceduret::resultt lookup_decision_procedure_result(
+  const smt_check_sat_response_kindt &response_kind)
+{
+  if(response_kind.cast<smt_sat_responset>())
+    return decision_proceduret::resultt::D_SATISFIABLE;
+  if(response_kind.cast<smt_unsat_responset>())
+    return decision_proceduret::resultt::D_UNSATISFIABLE;
+  if(response_kind.cast<smt_unknown_responset>())
+    return decision_proceduret::resultt::D_ERROR;
+  UNREACHABLE;
+}
+
 decision_proceduret::resultt smt2_incremental_decision_proceduret::dec_solve()
 {
   ++number_of_solver_calls;
   solver_process->send(smt_check_sat_commandt{});
   const smt_responset result = solver_process->receive_response();
+  if(const auto check_sat_response = result.cast<smt_check_sat_responset>())
+  {
+    if(check_sat_response->kind().cast<smt_unknown_responset>())
+      log.error() << "SMT2 solver returned \"unknown\"" << messaget::eom;
+    return lookup_decision_procedure_result(check_sat_response->kind());
+  }
   UNIMPLEMENTED_FEATURE("handling solver response.");
 }

src/solvers/smt2_incremental/smt_solver_process.cpp

@@ -2,7 +2,10 @@
 
 #include <solvers/smt2_incremental/smt_solver_process.h>
 
+#include <solvers/smt2/smt2irep.h>
+#include <solvers/smt2_incremental/smt_response_validation.h>
 #include <solvers/smt2_incremental/smt_to_smt2_string.h>
+#include <util/exception_utils.h>
 #include <util/invariant.h>
 #include <util/string_utils.h>
 
@@ -28,9 +31,28 @@ void smt_piped_solver_processt::send(const smt_commandt &smt_command)
   process.send(command_string + "\n");
 }
 
+/// Log messages and throw exception.
+static void handle_invalid_smt(
+  const std::vector<std::string> &validation_errors,
+  messaget &log)
+{
+  for(const std::string &message : validation_errors)
+  {
+    log.error() << message << messaget::eom;
+  }
+  throw analysis_exceptiont{"Invalid SMT response received from solver."};
+}
+
 smt_responset smt_piped_solver_processt::receive_response()
 {
   const auto response_text = process.wait_receive();
   log.debug() << "Solver response - " << response_text << messaget::eom;
-  UNIMPLEMENTED_FEATURE("parsing of solver response.");
+  response_stream << response_text;
+  const auto parse_tree = smt2irep(response_stream, log.get_message_handler());
+  if(!parse_tree)
+    throw deserialization_exceptiont{"Incomplete SMT response."};
+  const auto validation_result = validate_smt_response(*parse_tree);
+  if(const auto validation_errors = validation_result.get_if_error())
+    handle_invalid_smt(*validation_errors, log);
+  return *validation_result.get_if_valid();
 }

src/solvers/smt2_incremental/smt_solver_process.h

@@ -9,6 +9,7 @@ class smt_commandt;
 #include <util/message.h>
 #include <util/piped_process.h>
 
+#include <sstream>
 #include <string>
 
 class smt_base_solver_processt
@@ -49,6 +50,8 @@ class smt_piped_solver_processt : public smt_base_solver_processt
   std::string command_line_description;
   /// The raw solver sub process.
   piped_processt process;
+  /// For buffering / combining communications from the solver to cbmc.
+  std::stringstream response_stream;
   /// For debug printing.
   messaget log;
 };