Add smt response storage classes

src/solvers/Makefile

@@ -199,6 +199,7 @@ SRC = $(BOOLEFORCE_SRC) \
       smt2_incremental/smt_core_theory.cpp \
       smt2_incremental/smt_logics.cpp \
       smt2_incremental/smt_options.cpp \
+      smt2_incremental/smt_responses.cpp \
       smt2_incremental/smt_solver_process.cpp \
       smt2_incremental/smt_sorts.cpp \
       smt2_incremental/smt_terms.cpp \

src/solvers/smt2_incremental/smt_responses.cpp

@@ -0,0 +1,175 @@
+// Author: Diffblue Ltd.
+
+#include <solvers/smt2_incremental/smt_responses.h>
+
+#include <util/range.h>
+
+// Define the irep_idts for responses.
+#define RESPONSE_ID(the_id, the_base)                                          \
+  const irep_idt ID_smt_##the_id##_response{"smt_" #the_id "_response"};
+#include <solvers/smt2_incremental/smt_responses.def>
+#undef RESPONSE_ID
+
+bool smt_responset::operator==(const smt_responset &other) const
+{
+  return irept::operator==(other);
+}
+
+bool smt_responset::operator!=(const smt_responset &other) const
+{
+  return !(*this == other);
+}
+
+#define RESPONSE_ID(the_id, the_base)                                          \
+  template <>                                                                  \
+  const smt_##the_id##_responset *the_base::cast<smt_##the_id##_responset>()   \
+    const &                                                                    \
+  {                                                                            \
+    return id() == ID_smt_##the_id##_response                                  \
+             ? static_cast<const smt_##the_id##_responset *>(this)             \
+             : nullptr;                                                        \
+  }
+#include <solvers/smt2_incremental/smt_responses.def> // NOLINT(build/include)
+#undef RESPONSE_ID
+
+template <typename sub_classt>
+const sub_classt *smt_responset::cast() const &
+{
+  return nullptr;
+}
+
+bool smt_check_sat_response_kindt::
+operator==(const smt_check_sat_response_kindt &other) const
+{
+  return irept::operator==(other);
+}
+
+bool smt_check_sat_response_kindt::
+operator!=(const smt_check_sat_response_kindt &other) const
+{
+  return !(*this == other);
+}
+
+smt_success_responset::smt_success_responset()
+  : smt_responset{ID_smt_success_response}
+{
+}
+
+smt_sat_responset::smt_sat_responset()
+  : smt_check_sat_response_kindt{ID_smt_sat_response}
+{
+}
+
+smt_unsat_responset::smt_unsat_responset()
+  : smt_check_sat_response_kindt{ID_smt_unsat_response}
+{
+}
+
+smt_unknown_responset::smt_unknown_responset()
+  : smt_check_sat_response_kindt{ID_smt_unknown_response}
+{
+}
+
+template <typename derivedt>
+smt_check_sat_response_kindt::storert<derivedt>::storert()
+{
+  static_assert(
+    std::is_base_of<irept, derivedt>::value &&
+      std::is_base_of<storert<derivedt>, derivedt>::value,
+    "Only irept based classes need to upcast smt_termt to store it.");
+}
+
+template <typename derivedt>
+irept smt_check_sat_response_kindt::storert<derivedt>::upcast(
+  smt_check_sat_response_kindt check_sat_response_kind)
+{
+  return static_cast<irept &&>(std::move(check_sat_response_kind));
+}
+
+template <typename derivedt>
+const smt_check_sat_response_kindt &
+smt_check_sat_response_kindt::storert<derivedt>::downcast(const irept &irep)
+{
+  return static_cast<const smt_check_sat_response_kindt &>(irep);
+}
+
+smt_check_sat_responset::smt_check_sat_responset(
+  smt_check_sat_response_kindt kind)
+  : smt_responset{ID_smt_check_sat_response}
+{
+  set(ID_value, upcast(std::move(kind)));
+}
+
+const smt_check_sat_response_kindt &smt_check_sat_responset::kind() const
+{
+  return downcast(find(ID_value));
+}
+
+smt_get_value_responset::valuation_pairt::valuation_pairt(
+  smt_termt descriptor,
+  smt_termt value)
+{
+  get_sub().push_back(upcast(std::move(descriptor)));
+  get_sub().push_back(upcast(std::move(value)));
+}
+
+const smt_termt &smt_get_value_responset::valuation_pairt::descriptor() const
+{
+  return downcast(get_sub().at(0));
+}
+
+const smt_termt &smt_get_value_responset::valuation_pairt::value() const
+{
+  return downcast(get_sub().at(1));
+}
+
+bool smt_get_value_responset::valuation_pairt::
+operator==(const smt_get_value_responset::valuation_pairt &other) const
+{
+  return irept::operator==(other);
+}
+
+bool smt_get_value_responset::valuation_pairt::
+operator!=(const smt_get_value_responset::valuation_pairt &other) const
+{
+  return !(*this == other);
+}
+
+smt_get_value_responset::smt_get_value_responset(
+  std::vector<valuation_pairt> pairs)
+  : smt_responset(ID_smt_get_value_response)
+{
+  // SMT-LIB standard version 2.6 requires one or more pairs.
+  // See page 47, figure 3.9: Command responses.
+  INVARIANT(
+    !pairs.empty(), "Get value response must contain one or more pairs.");
+  for(auto &pair : pairs)
+  {
+    get_sub().push_back(std::move(pair));
+  }
+}
+
+std::vector<
+  std::reference_wrapper<const smt_get_value_responset::valuation_pairt>>
+smt_get_value_responset::pairs() const
+{
+  return make_range(get_sub()).map([](const irept &pair) {
+    return std::cref(static_cast<const valuation_pairt &>(pair));
+  });
+}
+
+smt_unsupported_responset::smt_unsupported_responset()
+  : smt_responset{ID_smt_unsupported_response}
+{
+}
+
+smt_error_responset::smt_error_responset(irep_idt message)
+  : smt_responset{ID_smt_error_response}
+{
+  set(ID_value, message);
+}
+
+const irep_idt &smt_error_responset::message() const
+{
+  return get(ID_value);
+}

src/solvers/smt2_incremental/smt_responses.def

@@ -0,0 +1,15 @@
+/// \file
+/// This set of definitions is used as part of the
+/// [X-macro](https://en.wikipedia.org/wiki/X_Macro) pattern. These define the
+/// set of responses which are implemented and it is used to automate repetitive
+/// parts of the implementation. These include -
+///  * The constant `irep_idt`s used to identify each of the response classes.
+///  * The public base classes used for implementing down casting.
+RESPONSE_ID(success, smt_responset)
+RESPONSE_ID(sat, smt_check_sat_response_kindt)
+RESPONSE_ID(unsat, smt_check_sat_response_kindt)
+RESPONSE_ID(unknown, smt_check_sat_response_kindt)
+RESPONSE_ID(check_sat, smt_responset)
+RESPONSE_ID(get_value, smt_responset)
+RESPONSE_ID(unsupported, smt_responset)
+RESPONSE_ID(error, smt_responset)

src/solvers/smt2_incremental/smt_responses.h

@@ -3,6 +3,7 @@
 #ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_RESPONSES_H
 #define CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_RESPONSES_H
 
+#include "smt_terms.h"
 #include <util/irep.h>
 
 class smt_responset : protected irept
@@ -14,8 +15,121 @@ class smt_responset : protected irept
 
   using irept::pretty;
 
+  bool operator==(const smt_responset &) const;
+  bool operator!=(const smt_responset &) const;
+
+  template <typename sub_classt>
+  const sub_classt *cast() const &;
+
 protected:
   using irept::irept;
 };
 
+class smt_success_responset : public smt_responset
+{
+public:
+  smt_success_responset();
+};
+
+class smt_check_sat_response_kindt : protected irept
+{
+public:
+  // smt_responset does not support the notion of an empty / null state. Use
+  // optionalt<smt_responset> instead if an empty response is required.
+  smt_check_sat_response_kindt() = delete;
+
+  using irept::pretty;
+
+  bool operator==(const smt_check_sat_response_kindt &) const;
+  bool operator!=(const smt_check_sat_response_kindt &) const;
+
+  template <typename sub_classt>
+  const sub_classt *cast() const &;
+
+  /// \brief Class for adding the ability to up and down cast
+  ///   smt_check_sat_response_kindt to and from irept. These casts are required
+  ///   by other irept derived classes in order to store instances of smt_termt
+  ///   inside them.
+  /// \tparam derivedt The type of class which derives from this class and from
+  ///   irept.
+  template <typename derivedt>
+  class storert
+  {
+  protected:
+    storert();
+    static irept upcast(smt_check_sat_response_kindt check_sat_response_kind);
+    static const smt_check_sat_response_kindt &downcast(const irept &);
+  };
+
+protected:
+  using irept::irept;
+};
+
+class smt_sat_responset : public smt_check_sat_response_kindt
+{
+public:
+  smt_sat_responset();
+};
+
+class smt_unsat_responset : public smt_check_sat_response_kindt
+{
+public:
+  smt_unsat_responset();
+};
+
+class smt_unknown_responset : public smt_check_sat_response_kindt
+{
+public:
+  smt_unknown_responset();
+};
+
+class smt_check_sat_responset
+  : public smt_responset,
+    private smt_check_sat_response_kindt::storert<smt_check_sat_responset>
+{
+public:
+  explicit smt_check_sat_responset(smt_check_sat_response_kindt kind);
+  const smt_check_sat_response_kindt &kind() const;
+};
+
+class smt_get_value_responset
+  : public smt_responset,
+    private smt_termt::storert<smt_get_value_responset>
+{
+public:
+  class valuation_pairt : private irept,
+                          private smt_termt::storert<valuation_pairt>
+  {
+  public:
+    valuation_pairt() = delete;
+    valuation_pairt(smt_termt descriptor, smt_termt value);
+
+    using irept::pretty;
+
+    bool operator==(const valuation_pairt &) const;
+    bool operator!=(const valuation_pairt &) const;
+
+    const smt_termt &descriptor() const;
+    const smt_termt &value() const;
+
+    friend smt_get_value_responset;
+  };
+
+  explicit smt_get_value_responset(std::vector<valuation_pairt> pairs);
+  std::vector<std::reference_wrapper<const valuation_pairt>> pairs() const;
+};
+
+class smt_unsupported_responset : public smt_responset
+{
+public:
+  smt_unsupported_responset();
+};
+
+class smt_error_responset : public smt_responset
+{
+public:
+  explicit smt_error_responset(irep_idt message);
+  const irep_idt &message() const;
+};
+
 #endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_RESPONSES_H

unit/Makefile

@@ -105,6 +105,7 @@ SRC += analyses/ai/ai.cpp \
        solvers/smt2_incremental/smt_bit_vector_theory.cpp \
        solvers/smt2_incremental/smt_commands.cpp \
        solvers/smt2_incremental/smt_core_theory.cpp \
+       solvers/smt2_incremental/smt_responses.cpp \
        solvers/smt2_incremental/smt_sorts.cpp \
        solvers/smt2_incremental/smt_terms.cpp \
        solvers/smt2_incremental/smt_to_smt2_string.cpp \

unit/count_tests.py

@@ -14,13 +14,22 @@ def __init__(self):
         self.separators = 0
 
     def read_text(self, text):
+        previous_character = None
+        in_quotes = False
         for character in text:
-            if character == '(' or character == '<':
-                self.bracket_depth += 1
-            elif character == ')' or character == '(':
-                self.bracket_depth -= 1
-            elif character == ',' and self.bracket_depth == 1:
-                self.separators += 1
+            if in_quotes:
+                if character == '"' and previous_character != "\\":
+                    in_quotes = False
+            else:
+                if character == '"':
+                    in_quotes = True
+                elif character == '(' or character == '<':
+                    self.bracket_depth += 1
+                elif character == ')' or character == '(':
+                    self.bracket_depth -= 1
+                elif character == ',' and self.bracket_depth == 1:
+                    self.separators += 1
+            previous_character = character
 
 
 def tests_in_file(file_path):