Utility functions for getting array from arguments

Author: romainbrenguier

src/solvers/refinement/string_refinement_util.cpp

@@ -75,6 +75,21 @@ bool has_char_array_subexpr(const exprt &expr, const namespacet &ns)
   return false;
 }
 
+optionalt<refined_string_exprt> get_char_array_of_argument(const exprt &expr)
+{
+  if(!is_refined_string_type(expr.type()))
+    return {};
+  if(const auto e = expr_try_dynamic_cast<refined_string_exprt>(expr))
+    return *e;
+  return {};
+}
+
+refined_string_exprt get_refined_string_expr_value(const exprt &expr)
+{
+  PRECONDITION(is_refined_string_type(expr.type()));
+  return expr_dynamic_cast<refined_string_exprt>(expr);
+}
+
 sparse_arrayt::sparse_arrayt(const with_exprt &expr)
 {
   auto ref = std::ref(static_cast<const exprt &>(expr));

src/solvers/refinement/string_refinement_util.h

@@ -67,6 +67,16 @@ bool has_string_subtype(const typet &type);
 /// \return true if a subexpression of `expr` is an array of characters
 bool has_char_array_subexpr(const exprt &expr, const namespacet &ns);
 
+/// \param expr: an expression
+/// \return a refined_string_exprt if expr is of type refined_string_type and
+///   has the right structure for a refined_string_exprt
+optionalt<refined_string_exprt> get_char_array_of_argument(const exprt &expr);
+
+/// \param expr: an expression
+/// \return a refined_string_exprt, an invariant will fail if expr is of type
+///   refined_string_type or cannot be cast to a refined_string_exprt
+refined_string_exprt get_refined_string_expr_value(const exprt &expr);
+
 struct index_set_pairt
 {
   std::map<exprt, std::set<exprt>> cumulative;