Add SMT get-value response validation for bool sorts

Author: thomasspriggs

src/solvers/smt2_incremental/smt_response_validation.cpp

@@ -176,6 +176,88 @@ valid_smt_error_response(const irept &parse_tree)
     validate_string_literal(parse_tree.get_sub()[1]));
 }
 
+static bool all_subs_are_pairs(const irept &parse_tree)
+{
+  return std::all_of(
+    parse_tree.get_sub().cbegin(),
+    parse_tree.get_sub().cend(),
+    [](const irept &sub) { return sub.get_sub().size() == 2; });
+}
+
+static response_or_errort<irep_idt>
+validate_smt_identifier(const irept &parse_tree)
+{
+  if(!parse_tree.get_sub().empty() || parse_tree.id().empty())
+  {
+    return response_or_errort<irep_idt>(
+      "Expected identifier, found - \"" + print_parse_tree(parse_tree) + "\".");
+  }
+  return response_or_errort<irep_idt>(parse_tree.id());
+}
+
+static optionalt<smt_termt> valid_smt_bool(const irept &parse_tree)
+{
+  if(!parse_tree.get_sub().empty())
+    return {};
+  if(parse_tree.id() == ID_true)
+    return {smt_bool_literal_termt{true}};
+  if(parse_tree.id() == ID_false)
+    return {smt_bool_literal_termt{false}};
+  return {};
+}
+
+static response_or_errort<smt_termt> validate_term(const irept &parse_tree)
+{
+  if(const auto smt_bool = valid_smt_bool(parse_tree))
+    return response_or_errort<smt_termt>{*smt_bool};
+  return response_or_errort<smt_termt>{"Unrecognised SMT term - \"" +
+                                       print_parse_tree(parse_tree) + "\"."};
+}
+
+static response_or_errort<smt_get_value_responset::valuation_pairt>
+validate_valuation_pair(const irept &pair_parse_tree)
+{
+  PRECONDITION(pair_parse_tree.get_sub().size() == 2);
+  const auto &descriptor = pair_parse_tree.get_sub()[0];
+  const auto &value = pair_parse_tree.get_sub()[1];
+  return validation_propagating<smt_get_value_responset::valuation_pairt>(
+    validate_smt_identifier(descriptor), validate_term(value));
+}
+
+/// \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_get_value_response(const irept &parse_tree)
+{
+  // Shape matching for does this look like a get value response?
+  if(!parse_tree.id().empty())
+    return {};
+  if(parse_tree.get_sub().empty())
+    return {};
+  if(!all_subs_are_pairs(parse_tree))
+    return {};
+  std::vector<std::string> error_messages;
+  std::vector<smt_get_value_responset::valuation_pairt> valuation_pairs;
+  for(const auto &pair : parse_tree.get_sub())
+  {
+    const auto pair_validation_result = validate_valuation_pair(pair);
+    if(const auto error = pair_validation_result.get_if_error())
+      error_messages.insert(error_messages.end(), error->begin(), error->end());
+    if(const auto valid_pair = pair_validation_result.get_if_valid())
+      valuation_pairs.push_back(*valid_pair);
+  }
+  if(!error_messages.empty())
+    return {response_or_errort<smt_responset>{std::move(error_messages)}};
+  else
+  {
+    return {response_or_errort<smt_responset>{
+      smt_get_value_responset{valuation_pairs}}};
+  }
+}
+
 response_or_errort<smt_responset> validate_smt_response(const irept &parse_tree)
 {
   if(parse_tree.id() == "sat")
@@ -193,6 +275,8 @@ response_or_errort<smt_responset> validate_smt_response(const irept &parse_tree)
     return response_or_errort<smt_responset>{smt_success_responset{}};
   if(parse_tree.id() == "unsupported")
     return response_or_errort<smt_responset>{smt_unsupported_responset{}};
+  if(const auto get_value_response = valid_smt_get_value_response(parse_tree))
+    return *get_value_response;
   return response_or_errort<smt_responset>{"Invalid SMT response \"" +
                                            id2string(parse_tree.id()) + "\""};
 }

src/solvers/smt2_incremental/smt_responses.cpp

@@ -109,10 +109,20 @@ smt_get_value_responset::valuation_pairt::valuation_pairt(
   smt_termt descriptor,
   smt_termt value)
 {
+  INVARIANT(
+    descriptor.get_sort() == value.get_sort(),
+    "SMT valuation pair must have matching sort for the descriptor and value.");
   get_sub().push_back(upcast(std::move(descriptor)));
   get_sub().push_back(upcast(std::move(value)));
 }
 
+smt_get_value_responset::valuation_pairt::valuation_pairt(
+  irep_idt descriptor,
+  const smt_termt &value)
+  : valuation_pairt(smt_identifier_termt{descriptor, value.get_sort()}, value)
+{
+}
+
 const smt_termt &smt_get_value_responset::valuation_pairt::descriptor() const
 {
   return downcast(get_sub().at(0));

src/solvers/smt2_incremental/smt_responses.h

@@ -103,6 +103,7 @@ class smt_get_value_responset
   public:
     valuation_pairt() = delete;
     valuation_pairt(smt_termt descriptor, smt_termt value);
+    valuation_pairt(irep_idt descriptor, const smt_termt &value);
 
     using irept::pretty;
 

unit/solvers/smt2_incremental/smt_response_validation.cpp

@@ -91,3 +91,24 @@ TEST_CASE("Validation of SMT error response", "[core][smt2_incremental]")
        .get_if_error() ==
     std::vector<std::string>{"Error response has multiple error messages."});
 }
+
+TEST_CASE("smt get-value response validation", "[core][smt2_incremental]")
+{
+  SECTION("Boolean sorted values.")
+  {
+    const response_or_errort<smt_responset> true_response =
+      validate_smt_response(*smt2irep("((a true))").parsed_output);
+    CHECK(
+      *true_response.get_if_valid() ==
+      smt_get_value_responset{{smt_get_value_responset::valuation_pairt{
+        smt_identifier_termt{"a", smt_bool_sortt{}},
+        smt_bool_literal_termt{true}}}});
+    const response_or_errort<smt_responset> false_response =
+      validate_smt_response(*smt2irep("((a false))").parsed_output);
+    CHECK(
+      *false_response.get_if_valid() ==
+      smt_get_value_responset{{smt_get_value_responset::valuation_pairt{
+        smt_identifier_termt{"a", smt_bool_sortt{}},
+        smt_bool_literal_termt{false}}}});
+  }
+}