Define function for array_pointer_association

This allows the constraint generator to do a pass on equations without
adding axioms but just adding the assaciation between pointer and arrays.

Author: romainbrenguier

src/solvers/refinement/string_constraint_generator.h

@@ -136,6 +136,12 @@ class string_constraint_generatort final
 
   array_poolt array_pool;
 
+  /// Associate array to pointer, and array to length
+  /// \return an expression if the given function application is one of
+  ///   associate pointer and associate length
+  optionalt<exprt>
+  make_array_pointer_association(const function_application_exprt &expr);
+
   // Type used by primitives to signal errors
   const signedbv_typet get_return_code_type()
   {

src/solvers/refinement/string_constraint_generator_main.cpp

@@ -438,6 +438,17 @@ static irep_idt get_function_name(const function_application_exprt &expr)
                            : to_symbol_expr(name).get_identifier();
 }
 
+optionalt<exprt> string_constraint_generatort::make_array_pointer_association(
+  const function_application_exprt &expr)
+{
+  const irep_idt &id = get_function_name(expr);
+  if(id == ID_cprover_associate_array_to_pointer_func)
+    return associate_array_to_pointer(expr);
+  else if(id == ID_cprover_associate_length_to_array_func)
+    return associate_length_to_array(expr);
+  return {};
+}
+
 /// strings contained in this call are converted to objects of type
 /// `string_exprt`, through adding axioms. Axioms are then added to enforce that
 /// the result corresponds to the function application.