Update smt_response_validation to use std::optional

Author: thomasspriggs

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)