Add struct support to smt2_incremental_decision_proceduret::get

Author: thomasspriggs

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

@@ -397,6 +397,17 @@ optionalt<exprt> smt2_incremental_decision_proceduret::get_expr(
   return array_exprt{elements, type};
 }
 
+optionalt<exprt> smt2_incremental_decision_proceduret::get_expr(
+  const smt_termt &struct_term,
+  const struct_tag_typet &type) const
+{
+  const auto encoded_result =
+    get_expr(struct_term, struct_encoding.encode(type));
+  if(!encoded_result)
+    return {};
+  return {struct_encoding.decode(*encoded_result, type)};
+}
+
 optionalt<exprt> smt2_incremental_decision_proceduret::get_expr(
   const smt_termt &descriptor,
   const typet &type) const
@@ -407,6 +418,10 @@ optionalt<exprt> smt2_incremental_decision_proceduret::get_expr(
       return {};
     return get_expr(descriptor, *array_type);
   }
+  if(const auto struct_type = type_try_dynamic_cast<struct_tag_typet>(type))
+  {
+    return get_expr(descriptor, *struct_type);
+  }
   const smt_get_value_commandt get_value_command{descriptor};
   const smt_responset response = get_response_to_command(
     *solver_process, get_value_command, identifier_table);

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h

@@ -57,6 +57,8 @@ class smt2_incremental_decision_proceduret final
   optionalt<exprt>
   get_expr(const smt_termt &descriptor, const typet &type) const;
   optionalt<exprt>
+  get_expr(const smt_termt &struct_term, const struct_tag_typet &type) const;
+  optionalt<exprt>
   get_expr(const smt_termt &array, const array_typet &type) const;
 
 protected: