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)
 {