Remove handling of hash_code in string solver

This can no longer be produced by the preprocessing, so it is not needed
in the constraint generation.

Author: romainbrenguier

src/solvers/README.md

@@ -430,9 +430,6 @@ allocates a new string before calling a primitive.
   * `cprover_string_equals_ignore_case` :
   \copybrief add_axioms_for_equals_ignore_case(symbol_generatort &fresh_symbol,const function_application_exprt &f, array_poolt &array_pool)
   \link add_axioms_for_equals_ignore_case(symbol_generatort &fresh_symbol,const function_application_exprt &f, array_poolt &array_pool) More... \endlink
-  * `cprover_string_hash_code` :
-  \copybrief string_constraint_generatort::add_axioms_for_hash_code
-  \link string_constraint_generatort::add_axioms_for_hash_code More... \endlink
   * `cprover_string_is_prefix` :
   \copybrief add_axioms_for_is_prefix
   \link add_axioms_for_is_prefix More... \endlink

src/solvers/strings/string_constraint_generator.h

@@ -75,18 +75,8 @@ class string_constraint_generatort final
 
   exprt associate_length_to_array(const function_application_exprt &f);
 
-  // Add axioms corresponding to the String.hashCode java function
-  // The specification is partial: the actual value is not actually computed
-  // but we ensure that hash codes of equal strings are equal.
-  std::pair<exprt, string_constraintst>
-  add_axioms_for_hash_code(const function_application_exprt &f);
-
   // MEMBERS
   const messaget message;
-
-  // To each string on which hash_code was called we associate a symbol
-  // representing the return value of the hash_code function.
-  std::map<array_string_exprt, exprt> hash_code_of_string;
 };
 
 // Type used by primitives to signal errors

src/solvers/strings/string_constraint_generator_comparison.cpp

@@ -176,44 +176,6 @@ std::pair<exprt, string_constraintst> add_axioms_for_equals_ignore_case(
   return {typecast_exprt(eq, f.type()), std::move(constraints)};
 }
 
-/// Value that is identical for strings with the same content
-///
-/// Add axioms stating that if two strings are equal then the values
-/// returned by this function are equal.
-/// These axioms are, for each string `s` on which hash was called:
-///   * \f$ hash(str)=hash(s) \lor |str| \ne |s|
-///       \lor (|str|=|s| \land \exists i<|s|.\ s[i]\ne str[i]) \f$
-/// \param f: function application with argument refined_string `str`
-/// \return integer expression `hash(str)`
-std::pair<exprt, string_constraintst>
-string_constraint_generatort::add_axioms_for_hash_code(
-  const function_application_exprt &f)
-{
-  PRECONDITION(f.arguments().size() == 1);
-  string_constraintst hash_constraints;
-  const array_string_exprt str = get_string_expr(array_pool, f.arguments()[0]);
-  const typet &return_type = f.type();
-  const typet &index_type = str.length_type();
-
-  auto pair = hash_code_of_string.insert(
-    std::make_pair(str, fresh_symbol("hash", return_type)));
-  const exprt hash = pair.first->second;
-
-  for(auto it : hash_code_of_string)
-  {
-    const symbol_exprt i = fresh_symbol("index_hash", index_type);
-    const equal_exprt c1(it.second, hash);
-    const notequal_exprt c2(it.first.length(), str.length());
-    const and_exprt c3(
-      equal_exprt(it.first.length(), str.length()),
-      and_exprt(
-        notequal_exprt(str[i], it.first[i]),
-        and_exprt(greater_than(str.length(), i), is_positive(i))));
-    hash_constraints.existential.push_back(or_exprt(c1, or_exprt(c2, c3)));
-  }
-  return {hash, std::move(hash_constraints)};
-}
-
 /// Lexicographic comparison of two strings
 ///
 /// Add axioms ensuring the result corresponds to that of the `String.compareTo`

src/solvers/strings/string_constraint_generator_main.cpp

@@ -240,8 +240,6 @@ string_constraint_generatort::add_axioms_for_function_application(
     return add_axioms_for_is_suffix(fresh_symbol, expr, true, array_pool);
   else if(id == ID_cprover_string_contains_func)
     return add_axioms_for_contains(fresh_symbol, expr, array_pool);
-  else if(id == ID_cprover_string_hash_code_func)
-    return add_axioms_for_hash_code(expr);
   else if(id == ID_cprover_string_index_of_func)
     return add_axioms_for_index_of(fresh_symbol, expr, array_pool);
   else if(id == ID_cprover_string_last_index_of_func)

src/util/irep_ids.def

@@ -609,7 +609,6 @@ IREP_ID_ONE(cprover_string_equals_ignore_case_func)
 IREP_ID_ONE(cprover_string_empty_string_func)
 IREP_ID_ONE(cprover_string_endswith_func)
 IREP_ID_ONE(cprover_string_format_func)
-IREP_ID_ONE(cprover_string_hash_code_func)
 IREP_ID_ONE(cprover_string_index_of_func)
 IREP_ID_ONE(cprover_string_insert_func)
 IREP_ID_ONE(cprover_string_insert_int_func)