Add template for node construction with validation propagation

For each non-leaf node in the `smt_responset` tree, the same logic is
required where the child nodes are validated and we construct the
non-leaf node if there are no errors, or collect and propagate the
errors upwards if there are errors validating the child nodes.

The template in this commit abstracts this logic out, so that it doesn't
need to be duplicated for each type of node we construct.

Author: thomasspriggs

src/solvers/smt2_incremental/smt_response_validation.cpp

@@ -13,6 +13,12 @@ response_or_errort<smtt>::response_or_errort(std::string message)
 {
 }
 
+template <class smtt>
+response_or_errort<smtt>::response_or_errort(std::vector<std::string> messages)
+  : messages{std::move(messages)}
+{
+}
+
 template <class smtt>
 const smtt *response_or_errort<smtt>::get_if_valid() const
 {
@@ -35,6 +41,114 @@ const std::vector<std::string> *response_or_errort<smtt>::get_if_error() const
 
 template class response_or_errort<smt_responset>;
 
+// Implementation detail of `collect_messages` below.
+template <typename argumentt, typename... argumentst>
+void collect_messages_impl(
+  std::vector<std::string> &collected_messages,
+  argumentt &&argument)
+{
+  if(const auto messages = argument.get_if_error())
+  {
+    collected_messages.insert(
+      collected_messages.end(), messages->cbegin(), messages->end());
+  }
+}
+
+// Implementation detail of `collect_messages` below.
+template <typename argumentt, typename... argumentst>
+void collect_messages_impl(
+  std::vector<std::string> &collected_messages,
+  argumentt &&argument,
+  argumentst &&... arguments)
+{
+  collect_messages_impl(collected_messages, argument);
+  collect_messages_impl(collected_messages, arguments...);
+}
+
+/// Builds a collection of messages composed all messages in the
+/// `response_or_errort` typed arguments in \p arguments. This is a templated
+/// function in order to handle `response_or_errort` instances which are
+/// specialised differently.
+template <typename... argumentst>
+std::vector<std::string> collect_messages(argumentst &&... arguments)
+{
+  std::vector<std::string> collected_messages;
+  collect_messages_impl(collected_messages, arguments...);
+  return collected_messages;
+}
+
+/// \brief Given a class to construct and a set of arguments to its constructor
+///   which may include errors, either return the collected errors if there are
+///   any or construct the class otherwise.
+/// \tparam smt_to_constructt
+///   The class to construct.
+/// \tparam smt_baset
+///   If the class to construct should be upcast to a base class before being
+///   stored in the `response_or_errort`, then the base class should be supplied
+///   in this parameter. If no upcast is required, then this should be left
+///   empty.
+/// \tparam argumentst
+///   The pack of argument types matching the constructor of
+///   `smt_to_constructt`. These must each be packed into an instance of
+///   `response_or_errort`.
+template <
+  typename smt_to_constructt,
+  typename smt_baset = smt_to_constructt,
+  typename... argumentst>
+response_or_errort<smt_baset> validation_propagating(argumentst &&... arguments)
+{
+  const auto collected_messages = collect_messages(arguments...);
+  if(!collected_messages.empty())
+    return response_or_errort<smt_baset>(collected_messages);
+  else
+  {
+    return response_or_errort<smt_baset>{
+      smt_to_constructt{(*arguments.get_if_valid())...}};
+  }
+}
+
+static response_or_errort<irep_idt>
+validate_string_literal(const irept &parse_tree)
+{
+  if(!parse_tree.get_sub().empty())
+  {
+    return response_or_errort<irep_idt>(
+      "Expected string literal, found \"" + parse_tree.pretty(0, 0) + "\".");
+  }
+  return response_or_errort<irep_idt>{parse_tree.id()};
+}
+
+/// \returns: A response or error in the case where the parse tree appears to be
+///   a get-value command. Returns empty otherwise.
+/// \note: Because this kind of response does not start with an identifying
+///   keyword, it will be considered that the response is intended to be a
+///   get-value response if it is composed of a collection of one or more pairs.
+static optionalt<response_or_errort<smt_responset>>
+valid_smt_error_response(const irept &parse_tree)
+{
+  // Check if the parse tree looks to be an error response.
+  if(!parse_tree.id().empty())
+    return {};
+  if(parse_tree.get_sub().empty())
+    return {};
+  if(parse_tree.get_sub().at(0).id() != "error")
+    return {};
+  // Parse tree is now considered to be an error response and anything
+  // unexpected in the parse tree is now considered to be an invalid response.
+  if(parse_tree.get_sub().size() == 1)
+  {
+    return {response_or_errort<smt_responset>{
+      "Error response is missing the error message."}};
+  }
+  if(parse_tree.get_sub().size() > 2)
+  {
+    return {response_or_errort<smt_responset>{
+      "Error response has multiple error messages."}};
+  }
+  return validation_propagating<smt_error_responset, smt_responset>(
+    validate_string_literal(parse_tree.get_sub()[1]));
+}
+
 response_or_errort<smt_responset> validate_smt_response(const irept &parse_tree)
 {
   if(parse_tree.id() == "sat")
@@ -46,6 +160,8 @@ response_or_errort<smt_responset> validate_smt_response(const irept &parse_tree)
   if(parse_tree.id() == "unknown")
     return response_or_errort<smt_responset>{
       smt_check_sat_responset{smt_unknown_responset{}}};
+  if(const auto error_response = valid_smt_error_response(parse_tree))
+    return *error_response;
   if(parse_tree.id() == "success")
     return response_or_errort<smt_responset>{smt_success_responset{}};
   if(parse_tree.id() == "unsupported")

src/solvers/smt2_incremental/smt_response_validation.h

@@ -19,6 +19,7 @@ class response_or_errort final
 public:
   explicit response_or_errort(smtt smt);
   explicit response_or_errort(std::string message);
+  explicit response_or_errort(std::vector<std::string> messages);
 
   /// \brief Gets the smt response if the response is valid, or returns nullptr
   ///   otherwise.

unit/solvers/smt2_incremental/smt_response_validation.cpp

@@ -74,3 +74,20 @@ TEST_CASE(
       std::vector<std::string>{"Invalid SMT response \"\""});
   }
 }
+
+TEST_CASE("Validation of SMT error response", "[core][smt2_incremental]")
+{
+  CHECK(
+    *validate_smt_response(
+       *smt2irep("(error \"Test error message.\")").parsed_output)
+       .get_if_valid() == smt_error_responset{"Test error message."});
+  CHECK(
+    *validate_smt_response(*smt2irep("(error)").parsed_output).get_if_error() ==
+    std::vector<std::string>{"Error response is missing the error message."});
+  CHECK(
+    *validate_smt_response(
+       *smt2irep("(error \"Test error message1.\" \"Test error message2.\")")
+          .parsed_output)
+       .get_if_error() ==
+    std::vector<std::string>{"Error response has multiple error messages."});
+}