Merge pull request #8089 from thomasspriggs/tas/smt_stl

Use the STL versions of `variant` and `optional` in incremental smt2 decision procedure

Author: thomasspriggs

src/solvers/smt2_incremental/ast/smt_commands.h

@@ -15,7 +15,7 @@ class smt_commandt : protected irept
 {
 public:
   // smt_commandt does not support the notion of an empty / null state. Use
-  // optionalt<smt_commandt> instead if an empty command is required.
+  // std::optional<smt_commandt> instead if an empty command is required.
   smt_commandt() = delete;
 
   using irept::pretty;

src/solvers/smt2_incremental/ast/smt_index.h

@@ -14,7 +14,7 @@ class smt_indext : protected irept
 {
 public:
   // smt_indext does not support the notion of an empty / null state. Use
-  // optionalt<smt_indext> instead if an empty index is required.
+  // std::optional<smt_indext> instead if an empty index is required.
   smt_indext() = delete;
 
   using irept::pretty;

src/solvers/smt2_incremental/ast/smt_logics.h

@@ -11,7 +11,7 @@ class smt_logict : protected irept
 {
 public:
   // smt_logict does not support the notion of an empty / null state. Use
-  // optionalt<smt_logict> instead if an empty logic is required.
+  // std::optional<smt_logict> instead if an empty logic is required.
   smt_logict() = delete;
 
   using irept::pretty;

src/solvers/smt2_incremental/ast/smt_options.h

@@ -11,7 +11,7 @@ class smt_optiont : protected irept
 {
 public:
   // smt_optiont does not support the notion of an empty / null state. Use
-  // optionalt<smt_optiont> instead if an empty option is required.
+  // std::optional<smt_optiont> instead if an empty option is required.
   smt_optiont() = delete;
 
   using irept::pretty;

src/solvers/smt2_incremental/ast/smt_responses.h

@@ -11,7 +11,7 @@ class smt_responset : 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.
+  // std::optional<smt_responset> instead if an empty response is required.
   smt_responset() = delete;
 
   using irept::pretty;
@@ -36,7 +36,7 @@ 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.
+  // std::optional<smt_responset> instead if an empty response is required.
   smt_check_sat_response_kindt() = delete;
 
   using irept::pretty;

src/solvers/smt2_incremental/ast/smt_sorts.cpp

@@ -24,7 +24,8 @@
 
 #define SORT_ID(the_id)                                                        \
   template <>                                                                  \
-  optionalt<smt_##the_id##_sortt> smt_sortt::cast<smt_##the_id##_sortt>() &&   \
+  std::optional<smt_##the_id##_sortt> smt_sortt::cast<smt_##the_id##_sortt>()  \
+    &&                                                                         \
   {                                                                            \
     if(id() == ID_smt_##the_id##_sort)                                         \
       return {std::move(*static_cast<const smt_##the_id##_sortt *>(this))};    \

src/solvers/smt2_incremental/ast/smt_sorts.h

@@ -8,8 +8,8 @@
 #define CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_SORTS_H
 
 #include <util/irep.h>
-#include <util/optional.h>
 
+#include <optional>
 #include <type_traits>
 
 class smt_sort_const_downcast_visitort;
@@ -18,7 +18,7 @@ class smt_sortt : protected irept
 {
 public:
   // smt_sortt does not support the notion of an empty / null state. Use
-  // optionalt<smt_sortt> instead if an empty sort is required.
+  // std::optional<smt_sortt> instead if an empty sort is required.
   smt_sortt() = delete;
 
   using irept::pretty;
@@ -47,7 +47,7 @@ class smt_sortt : protected irept
   const sub_classt *cast() const &;
 
   template <typename sub_classt>
-  optionalt<sub_classt> cast() &&;
+  std::optional<sub_classt> cast() &&;
 
 protected:
   using irept::irept;

src/solvers/smt2_incremental/ast/smt_terms.h

@@ -21,7 +21,7 @@ class smt_termt : protected irept, private smt_sortt::storert<smt_termt>
 {
 public:
   // smt_termt does not support the notion of an empty / null state. Use
-  // optionalt<smt_termt> instead if an empty term is required.
+  // std::optional<smt_termt> instead if an empty term is required.
   smt_termt() = delete;
 
   using irept::pretty;

src/solvers/smt2_incremental/construct_value_expr_from_smt.cpp

@@ -16,7 +16,7 @@ class value_expr_from_smt_factoryt : public smt_term_const_downcast_visitort
 private:
   const typet &type_to_construct;
   const namespacet &ns;
-  optionalt<exprt> result;
+  std::optional<exprt> result;
 
   explicit value_expr_from_smt_factoryt(
     const typet &type_to_construct,

src/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -206,7 +206,7 @@ struct sort_based_cast_to_bit_vector_convertert final
   const smt_termt &from_term;
   const typet &from_type;
   const bitvector_typet &to_type;
-  optionalt<smt_termt> result;
+  std::optional<smt_termt> result;
 
   sort_based_cast_to_bit_vector_convertert(
     const smt_termt &from_term,
@@ -299,7 +299,7 @@ static smt_termt convert_expr_to_smt(
 struct sort_based_literal_convertert : public smt_sort_const_downcast_visitort
 {
   const constant_exprt &member_input;
-  optionalt<smt_termt> result;
+  std::optional<smt_termt> result;
 
   explicit sort_based_literal_convertert(const constant_exprt &input)
     : member_input{input}
@@ -591,7 +591,7 @@ static smt_termt convert_relational_to_smt(
     binary_relation.pretty());
 }
 
-static optionalt<smt_termt> try_relational_conversion(
+static std::optional<smt_termt> try_relational_conversion(
   const exprt &expr,
   const sub_expression_mapt &converted)
 {

src/solvers/smt2_incremental/encoding/struct_encoding.cpp

@@ -15,6 +15,7 @@
 
 #include <algorithm>
 #include <numeric>
+#include <optional>
 #include <queue>
 
 struct_encodingt::struct_encodingt(const namespacet &ns)
@@ -33,7 +34,7 @@ struct_encodingt::~struct_encodingt() = default;
 /// If the given \p type needs re-encoding as a bit-vector then this function
 /// \returns the width of the new bitvector type. The width calculation is
 /// delegated to \p boolbv_width.
-static optionalt<std::size_t>
+static std::optional<std::size_t>
 needs_width(const typet &type, const boolbv_widtht &boolbv_width)
 {
   if(const auto struct_tag = type_try_dynamic_cast<struct_tag_typet>(type))
@@ -222,7 +223,7 @@ exprt struct_encodingt::encode(exprt expr) const
       if(can_cast_type<struct_tag_typet>(current.type()))
         current = ::encode(*with_expr, ns);
     current.type() = encode(current.type());
-    optionalt<exprt> update;
+    std::optional<exprt> update;
     if(const auto struct_expr = expr_try_dynamic_cast<struct_exprt>(current))
       update = ::encode(*struct_expr);
     if(const auto union_expr = expr_try_dynamic_cast<union_exprt>(current))

src/solvers/smt2_incremental/response_or_error.h

@@ -4,9 +4,9 @@
 #define CPROVER_SOLVERS_SMT2_INCREMENTAL_RESPONSE_OR_ERROR_H
 
 #include <util/invariant.h>
-#include <util/optional.h>
 
 #include <string>
+#include <variant>
 #include <vector>
 
 /// Holds either a valid parsed response or response sub-tree of type \tparam
@@ -16,49 +16,36 @@ template <class smtt>
 class response_or_errort final
 {
 public:
-  explicit response_or_errort(smtt smt) : smt{std::move(smt)}
+  explicit response_or_errort(smtt smt) : smt_or_messages{std::move(smt)}
   {
   }
 
   explicit response_or_errort(std::string message)
-    : messages{std::move(message)}
+    : smt_or_messages{std::vector<std::string>{std::move(message)}}
   {
   }
 
   explicit response_or_errort(std::vector<std::string> messages)
-    : messages{std::move(messages)}
+    : smt_or_messages{std::move(messages)}
   {
   }
 
   /// \brief Gets the smt response if the response is valid, or returns nullptr
   ///   otherwise.
   const smtt *get_if_valid() const
   {
-    INVARIANT(
-      smt.has_value() == messages.empty(),
-      "The response_or_errort class must be in the valid state or error state, "
-      "exclusively.");
-    return smt.has_value() ? &smt.value() : nullptr;
+    return std::get_if<smtt>(&smt_or_messages);
   }
 
   /// \brief Gets the error messages if the response is invalid, or returns
   ///   nullptr otherwise.
   const std::vector<std::string> *get_if_error() const
   {
-    INVARIANT(
-      smt.has_value() == messages.empty(),
-      "The response_or_errort class must be in the valid state or error state, "
-      "exclusively.");
-    return smt.has_value() ? nullptr : &messages;
+    return std::get_if<std::vector<std::string>>(&smt_or_messages);
   }
 
 private:
-  // The below two fields could be a single `std::variant` field, if there was
-  // an implementation of it available in the cbmc repository. However at the
-  // time of writing we are targeting C++11, `std::variant` was introduced in
-  // C++17 and we have no backported version.
-  optionalt<smtt> smt;
-  std::vector<std::string> messages;
+  std::variant<smtt, std::vector<std::string>> smt_or_messages;
 };
 
 #endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_RESPONSE_OR_ERROR_H

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

@@ -44,7 +44,7 @@ static smt_responset get_response_to_command(
 
 /// Returns a message string describing the problem in the case where the
 /// response from the solver is an error status. Returns empty otherwise.
-static optionalt<std::string>
+static std::optional<std::string>
 get_problem_messages(const smt_responset &response)
 {
   if(const auto error = response.cast<smt_error_responset>())
@@ -413,7 +413,7 @@ exprt smt2_incremental_decision_proceduret::handle(const exprt &expr)
   return expr;
 }
 
-optionalt<smt_termt>
+std::optional<smt_termt>
 smt2_incremental_decision_proceduret::get_identifier(const exprt &expr) const
 {
   // Lookup the non-lowered form first.
@@ -437,7 +437,7 @@ smt2_incremental_decision_proceduret::get_identifier(const exprt &expr) const
   return {};
 }
 
-optionalt<exprt> smt2_incremental_decision_proceduret::get_expr(
+std::optional<exprt> smt2_incremental_decision_proceduret::get_expr(
   const smt_termt &array,
   const array_typet &type) const
 {
@@ -467,7 +467,7 @@ optionalt<exprt> smt2_incremental_decision_proceduret::get_expr(
   return array_exprt{elements, type};
 }
 
-optionalt<exprt> smt2_incremental_decision_proceduret::get_expr(
+std::optional<exprt> smt2_incremental_decision_proceduret::get_expr(
   const smt_termt &struct_term,
   const struct_tag_typet &type) const
 {
@@ -478,7 +478,7 @@ optionalt<exprt> smt2_incremental_decision_proceduret::get_expr(
   return {struct_encoding.decode(*encoded_result, type)};
 }
 
-optionalt<exprt> smt2_incremental_decision_proceduret::get_expr(
+std::optional<exprt> smt2_incremental_decision_proceduret::get_expr(
   const smt_termt &union_term,
   const union_tag_typet &type) const
 {
@@ -489,7 +489,7 @@ optionalt<exprt> smt2_incremental_decision_proceduret::get_expr(
   return {struct_encoding.decode(*encoded_result, type)};
 }
 
-optionalt<exprt> smt2_incremental_decision_proceduret::get_expr(
+std::optional<exprt> smt2_incremental_decision_proceduret::get_expr(
   const smt_termt &descriptor,
   const typet &type) const
 {
@@ -556,7 +556,7 @@ exprt smt2_incremental_decision_proceduret::get(const exprt &expr) const
   log.conditional_output(log.debug(), [&](messaget::mstreamt &debug) {
     debug << "`get` - \n  " + expr.pretty(2, 0) << messaget::eom;
   });
-  auto descriptor = [&]() -> optionalt<smt_termt> {
+  auto descriptor = [&]() -> std::optional<smt_termt> {
     if(const auto index_expr = expr_try_dynamic_cast<index_exprt>(expr))
     {
       const auto array = get_identifier(index_expr->array());

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h

@@ -56,13 +56,13 @@ class smt2_incremental_decision_proceduret final
   /// Gets the value of \p descriptor from the solver and returns the solver
   /// response expressed as an exprt of type \p type. This is an implementation
   /// detail of the `get(exprt)` member function.
-  optionalt<exprt>
+  std::optional<exprt>
   get_expr(const smt_termt &descriptor, const typet &type) const;
-  optionalt<exprt>
+  std::optional<exprt>
   get_expr(const smt_termt &struct_term, const struct_tag_typet &type) const;
-  optionalt<exprt>
+  std::optional<exprt>
   get_expr(const smt_termt &union_term, const union_tag_typet &type) const;
-  optionalt<exprt>
+  std::optional<exprt>
   get_expr(const smt_termt &array, const array_typet &type) const;
 
 protected:
@@ -117,7 +117,7 @@ class smt2_incremental_decision_proceduret final
   /// possible expression forms by expressing these in terms of the remaining
   /// language features.
   exprt lower(exprt expression) const;
-  optionalt<smt_termt> get_identifier(const exprt &expr) const;
+  std::optional<smt_termt> get_identifier(const exprt &expr) const;
 
   /// Namespace for looking up the expressions which symbol_exprts relate to.
   /// This includes the symbols defined outside of the decision procedure but

src/solvers/smt2_incremental/smt_response_validation.cpp

@@ -125,7 +125,7 @@ validate_string_literal(const irept &parse_tree)
 /// \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>>
+static std::optional<response_or_errort<smt_responset>>
 valid_smt_error_response(const irept &parse_tree)
 {
   // Check if the parse tree looks to be an error response.
@@ -162,7 +162,7 @@ static bool all_subs_are_pairs(const irept &parse_tree)
 
 /// Checks for valid bit vector constants of the form `(_ bv(value) (width))`
 /// for example - `(_ bv4 64)`.
-static optionalt<smt_termt>
+static std::optional<smt_termt>
 valid_smt_indexed_bit_vector(const irept &parse_tree)
 {
   if(parse_tree.get_sub().size() != 3)
@@ -189,7 +189,7 @@ valid_smt_indexed_bit_vector(const irept &parse_tree)
   return smt_bit_vector_constant_termt{value, bit_width};
 }
 
-static optionalt<smt_termt> valid_smt_bool(const irept &parse_tree)
+static std::optional<smt_termt> valid_smt_bool(const irept &parse_tree)
 {
   if(!parse_tree.get_sub().empty())
     return {};
@@ -200,7 +200,7 @@ static optionalt<smt_termt> valid_smt_bool(const irept &parse_tree)
   return {};
 }
 
-static optionalt<smt_termt> valid_smt_binary(const std::string &text)
+static std::optional<smt_termt> valid_smt_binary(const std::string &text)
 {
   static const std::regex binary_format{"#b[01]+"};
   if(!std::regex_match(text, binary_format))
@@ -211,7 +211,7 @@ static optionalt<smt_termt> valid_smt_binary(const std::string &text)
   return {smt_bit_vector_constant_termt{value, width}};
 }
 
-static optionalt<smt_termt> valid_smt_hex(const std::string &text)
+static std::optional<smt_termt> valid_smt_hex(const std::string &text)
 {
   static const std::regex hex_format{"#x[0-9A-Za-z]+"};
   if(!std::regex_match(text, hex_format))
@@ -225,7 +225,7 @@ static optionalt<smt_termt> valid_smt_hex(const std::string &text)
   return {smt_bit_vector_constant_termt{value, width}};
 }
 
-static optionalt<smt_termt>
+static std::optional<smt_termt>
 valid_smt_bit_vector_constant(const irept &parse_tree)
 {
   if(const auto indexed = valid_smt_indexed_bit_vector(parse_tree))
@@ -240,7 +240,7 @@ valid_smt_bit_vector_constant(const irept &parse_tree)
   return {};
 }
 
-static optionalt<response_or_errort<smt_termt>> try_select_validation(
+static std::optional<response_or_errort<smt_termt>> try_select_validation(
   const irept &parse_tree,
   const std::unordered_map<irep_idt, smt_identifier_termt> &identifier_table)
 {
@@ -321,7 +321,7 @@ validate_valuation_pair(
 /// \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>>
+static std::optional<response_or_errort<smt_responset>>
 valid_smt_get_value_response(
   const irept &parse_tree,
   const std::unordered_map<irep_idt, smt_identifier_termt> &identifier_table)