Remove redundant primitive

There is no need to have a primitive for getting the length of a string,
as this is in the associated refined string expr

Author: thk123

src/solvers/strings/string_constraint_generator_main.cpp

@@ -215,8 +215,6 @@ string_constraint_generatort::add_axioms_for_function_application(
 
   if(id == ID_cprover_char_literal_func)
     return add_axioms_for_char_literal(expr);
-  else if(id == ID_cprover_string_length_func)
-    return add_axioms_for_length(expr);
   else if(id == ID_cprover_string_equal_func)
     return add_axioms_for_equals(expr);
   else if(id == ID_cprover_string_equals_ignore_case_func)

src/util/irep_ids.def

@@ -615,7 +615,6 @@ IREP_ID_ONE(cprover_string_is_prefix_func)
 IREP_ID_ONE(cprover_string_is_suffix_func)
 IREP_ID_ONE(cprover_string_is_empty_func)
 IREP_ID_ONE(cprover_string_last_index_of_func)
-IREP_ID_ONE(cprover_string_length_func)
 IREP_ID_ONE(cprover_string_of_int_func)
 IREP_ID_ONE(cprover_string_of_int_hex_func)
 IREP_ID_ONE(cprover_string_of_long_func)

unit/solvers/strings/string_refinement/string_refinement.cpp

@@ -59,11 +59,6 @@ SCENARIO("string refinement", "[core][solvers][strings][string_refinement]")
       ID_cprover_associate_length_to_array_func,
       mathematical_function_typet{{int_type, char_array_type}, int_type}};
 
-    // length_function : (string) -> int
-    const symbol_exprt length_function{
-      ID_cprover_string_length_func,
-      mathematical_function_typet{{string_type}, int_type}};
-
     // char_at_function : (string, int) -> char
     const symbol_exprt char_at_function{
       ID_cprover_string_char_at_func,