Refactor length_le to less_than_or_equal_to

Binary relations on string lengths do not need the string itself.
Refactor to delegate dereferencing the length to the caller.
This is necessary for upcoming changes in which accessing the length
always involves accessing the array_pool.

Author: Joel Allred

src/solvers/strings/string_constraint_generator_comparison.cpp

@@ -271,7 +271,9 @@ std::pair<exprt, string_constraintst> add_axioms_for_compare_to(
       typecast_exprt(s1.length(), return_type),
       typecast_exprt(s2.length(), return_type)));
   const or_exprt guard1(
-    and_exprt(length_le(s1, s2.length()), greater_than(s1.length(), x)),
+    and_exprt(
+      less_than_or_equal_to(s1.length(), s2.length()),
+      greater_than(s1.length(), x)),
     and_exprt(
       greater_or_equal_to(s1.length(), s2.length()),
       greater_than(s2.length(), x)));

src/solvers/strings/string_constraint_generator_float.cpp

@@ -278,7 +278,8 @@ std::pair<exprt, string_constraintst> add_axioms_for_fractional_part(
   // no_trailing_zero: forall j:[2, max_size[. !(|res| = j+1 && res[j] = '0')
   // a3 : int_expr = sum_j 10^j (j < |res| ? res[j] - '0' : 0)
 
-  const and_exprt a1(greater_than(res.length(), 1), length_le(res, max));
+  const and_exprt a1(
+    greater_than(res.length(), 1), less_than_or_equal_to(res.length(), max));
   constraints.existential.push_back(a1);
 
   equal_exprt starts_with_dot(res[0], from_integer('.', char_type));

src/solvers/strings/string_constraint_generator_transformation.cpp

@@ -209,7 +209,7 @@ std::pair<exprt, string_constraintst> add_axioms_for_trim(
     greater_or_equal_to(res.length(), from_integer(0, index_type));
   constraints.existential.push_back(a4);
 
-  const exprt a5 = length_le(res, str.length());
+  const exprt a5 = less_than_or_equal_to(res.length(), str.length());
   constraints.existential.push_back(a5);
 
   symbol_exprt n = fresh_symbol("QA_index_trim", index_type);

src/solvers/strings/string_constraint_generator_valueof.cpp

@@ -230,8 +230,9 @@ add_axioms_from_int_hex(const array_string_exprt &res, const exprt &i)
   exprt f_char = from_integer('f', char_type);
 
   size_t max_size = 8;
-  constraints.existential.push_back(
-    and_exprt(greater_than(res.length(), 0), length_le(res, max_size)));
+  constraints.existential.push_back(and_exprt(
+    greater_than(res.length(), 0),
+    less_than_or_equal_to(res.length(), max_size)));
 
   for(size_t size = 1; size <= max_size; size++)
   {
@@ -370,7 +371,8 @@ string_constraintst add_axioms_for_correct_number_format(
   constraints.existential.push_back(contains_digit);
 
   // |str| <= max_size
-  constraints.existential.push_back(length_le(str, max_size));
+  constraints.existential.push_back(
+    less_than_or_equal_to(str.length(), max_size));
 
   // forall 1 <= i < |str| . is_digit_with_radix(str[i], radix)
   // We unfold the above because we know that it will be used for all i up to

src/util/string_expr.h

@@ -34,17 +34,17 @@ inline binary_relation_exprt greater_than(const exprt &lhs, mp_integer i)
   return greater_than(lhs, from_integer(i, lhs.type()));
 }
 
-template <typename T>
-binary_relation_exprt length_le(const T &lhs, const exprt &rhs)
+inline binary_relation_exprt
+less_than_or_equal_to(const exprt &lhs, const exprt &rhs)
 {
-  PRECONDITION(rhs.type() == lhs.length().type());
-  return binary_relation_exprt(lhs.length(), ID_le, rhs);
+  PRECONDITION(rhs.type() == lhs.type());
+  return binary_relation_exprt(lhs, ID_le, rhs);
 }
 
-template <typename T>
-binary_relation_exprt length_le(const T &lhs, mp_integer i)
+inline binary_relation_exprt
+less_than_or_equal_to(const exprt &lhs, mp_integer i)
 {
-  return length_le(lhs, from_integer(i, lhs.length().type()));
+  return less_than_or_equal_to(lhs, from_integer(i, lhs.type()));
 }
 
 inline equal_exprt equal_to(const exprt &lhs, const exprt &rhs)