Get rid of default axioms for strings

These default axioms where too strict and where applied even for strings
that may never be creted in the actual program.
This could for instance lead to problematic contradiction for a Java
object which could be casted either to a string or an int:
the axiom added there would apply both on the string and on the integer.

Author: romainbrenguier

src/solvers/refinement/string_constraint_generator.h

@@ -184,7 +184,6 @@ class string_constraint_generatort final
   array_string_exprt
   char_array_of_pointer(const exprt &pointer, const exprt &length);
 
-  void add_default_axioms(const array_string_exprt &s);
   exprt axiom_for_is_positive_index(const exprt &x);
 
   void add_constraint_on_characters(

src/solvers/refinement/string_constraint_generator_main.cpp

@@ -172,7 +172,6 @@ array_string_exprt string_constraint_generatort::fresh_string(
   symbol_exprt content = fresh_symbol("string_content", array_type);
   array_string_exprt str = to_array_string_expr(content);
   created_strings.insert(str);
-  add_default_axioms(str);
   return str;
 }
 
@@ -279,7 +278,7 @@ exprt string_constraint_generatort::associate_array_to_pointer(
 
   const exprt &pointer_expr = f.arguments()[1];
   array_pool.insert(pointer_expr, array_expr);
-  add_default_axioms(to_array_string_expr(array_expr));
+  created_strings.emplace(to_array_string_expr(array_expr));
   return from_integer(0, f.type());
 }
 
@@ -319,27 +318,6 @@ void string_constraint_generatort::clear_constraints()
   not_contains_constraints.clear();
 }
 
-/// adds standard axioms about the length of the string and its content: * its
-/// length should be positive * it should not exceed max_string_length * if
-/// force_printable_characters is true then all characters should belong to the
-/// range of ASCII characters between ' ' and '~'
-/// \param s: a string expression
-/// \return a string expression that is linked to the argument through axioms
-///   that are added to the list
-void string_constraint_generatort::add_default_axioms(
-  const array_string_exprt &s)
-{
-  // If `s` was already added we do nothing.
-  if(!created_strings.insert(s).second)
-    return;
-
-  const exprt index_zero = from_integer(0, s.length().type());
-  lemmas.push_back(s.axiom_for_length_ge(index_zero));
-
-  if(max_string_length!=std::numeric_limits<size_t>::max())
-    lemmas.push_back(s.axiom_for_length_le(max_string_length));
-}
-
 /// Add constraint on characters of a string.
 ///
 /// This constraint is
@@ -409,13 +387,14 @@ array_string_exprt array_poolt::find(const exprt &pointer, const exprt &length)
 }
 
 /// Adds creates a new array if it does not already exists
-/// \todo This should be replaced by associate_char_array_to_char_pointer
+/// \todo This should be replaced
+/// by array_poolt.make_char_array_for_char_pointer
 array_string_exprt string_constraint_generatort::char_array_of_pointer(
   const exprt &pointer,
   const exprt &length)
 {
   const array_string_exprt array = array_pool.find(pointer, length);
-  add_default_axioms(array);
+  created_strings.insert(array);
   return array;
 }