Renaming string length comparing functions

The previous name used (like `axioms_for_is_longer_than`) could be
ambiguous and sometimes misleading.

Author: romainbrenguier

src/solvers/refinement/string_constraint_generator_comparison.cpp

@@ -175,7 +175,7 @@ exprt string_constraint_generatort::add_axioms_for_hash_code(
       and_exprt(
         not_exprt(equal_exprt(str[i], it.first[i])),
         and_exprt(
-          str.axiom_for_is_strictly_longer_than(i),
+          str.axiom_for_length_gt(i),
           axiom_for_is_positive_index(i))));
     axioms.push_back(or_exprt(c1, or_exprt(c2, c3)));
   }
@@ -229,16 +229,12 @@ exprt string_constraint_generatort::add_axioms_for_compare_to(
       typecast_exprt(s1.length(), return_type),
       typecast_exprt(s2.length(), return_type)));
   or_exprt guard1(
-    and_exprt(s1.axiom_for_is_shorter_than(s2),
-              s1.axiom_for_is_strictly_longer_than(x)),
-    and_exprt(s1.axiom_for_is_longer_than(s2),
-              s2.axiom_for_is_strictly_longer_than(x)));
+    and_exprt(s1.axiom_for_length_le(s2), s1.axiom_for_length_gt(x)),
+    and_exprt(s1.axiom_for_length_ge(s2), s2.axiom_for_length_gt(x)));
   and_exprt cond1(ret_char_diff, guard1);
   or_exprt guard2(
-    and_exprt(s2.axiom_for_is_strictly_longer_than(s1),
-              s1.axiom_for_has_length(x)),
-    and_exprt(s1.axiom_for_is_strictly_longer_than(s2),
-              s2.axiom_for_has_length(x)));
+    and_exprt(s2.axiom_for_length_gt(s1), s1.axiom_for_has_length(x)),
+    and_exprt(s1.axiom_for_length_gt(s2), s2.axiom_for_has_length(x)));
   and_exprt cond2(ret_length_diff, guard2);
 
   implies_exprt a3(
@@ -300,7 +296,7 @@ symbol_exprt string_constraint_generatort::add_axioms_for_intern(
               str.axiom_for_has_same_length_as(it.first),
               and_exprt(
                 not_exprt(equal_exprt(str[i], it.first[i])),
-                and_exprt(str.axiom_for_is_strictly_longer_than(i),
+                and_exprt(str.axiom_for_length_gt(i),
                           axiom_for_is_positive_index(i)))))));
     }
 

src/solvers/refinement/string_constraint_generator_float.cpp

@@ -235,8 +235,8 @@ string_exprt string_constraint_generatort::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)
 
-  and_exprt a1(res.axiom_for_is_strictly_longer_than(1),
-               res.axiom_for_is_shorter_than(max));
+  and_exprt a1(res.axiom_for_length_gt(1),
+               res.axiom_for_length_le(max));
   axioms.push_back(a1);
 
   equal_exprt starts_with_dot(res[0], from_integer('.', char_type));

src/solvers/refinement/string_constraint_generator_main.cpp

@@ -156,9 +156,9 @@ void string_constraint_generatort::add_default_axioms(
   const string_exprt &s)
 {
   axioms.push_back(
-    s.axiom_for_is_longer_than(from_integer(0, s.length().type())));
+    s.axiom_for_length_ge(from_integer(0, s.length().type())));
   if(max_string_length!=std::numeric_limits<size_t>::max())
-    axioms.push_back(s.axiom_for_is_shorter_than(max_string_length));
+    axioms.push_back(s.axiom_for_length_le(max_string_length));
 
   if(force_printable_characters)
   {

src/solvers/refinement/string_constraint_generator_testing.cpp

@@ -32,7 +32,7 @@ exprt string_constraint_generatort::add_axioms_for_is_prefix(
 
   implies_exprt a1(
     isprefix,
-    str.axiom_for_is_longer_than(plus_exprt_with_overflow_check(
+    str.axiom_for_length_ge(plus_exprt_with_overflow_check(
       prefix.length(), offset)));
   axioms.push_back(a1);
 
@@ -49,12 +49,12 @@ exprt string_constraint_generatort::add_axioms_for_is_prefix(
   and_exprt witness_diff(
     axiom_for_is_positive_index(witness),
     and_exprt(
-      prefix.axiom_for_is_strictly_longer_than(witness),
+      prefix.axiom_for_length_gt(witness),
       notequal_exprt(str[plus_exprt_with_overflow_check(witness, offset)],
                      prefix[witness])));
   or_exprt s0_notpref_s1(
     not_exprt(
-      str.axiom_for_is_longer_than(
+      str.axiom_for_length_ge(
         plus_exprt_with_overflow_check(prefix.length(), offset))),
     witness_diff);
 
@@ -132,7 +132,7 @@ exprt string_constraint_generatort::add_axioms_for_is_suffix(
   //     || (s1.length > witness>=0
   //       &&s1[witness]!=s0[witness + s0.length-s1.length]
 
-  implies_exprt a1(issuffix, s1.axiom_for_is_longer_than(s0));
+  implies_exprt a1(issuffix, s1.axiom_for_length_ge(s0));
   axioms.push_back(a1);
 
   symbol_exprt qvar=fresh_univ_index("QA_suffix", index_type);
@@ -146,12 +146,12 @@ exprt string_constraint_generatort::add_axioms_for_is_suffix(
   exprt shifted=plus_exprt(
     witness, minus_exprt(s1.length(), s0.length()));
   or_exprt constr3(
-    and_exprt(s0.axiom_for_is_strictly_longer_than(s1),
+    and_exprt(s0.axiom_for_length_gt(s1),
               equal_exprt(witness, from_integer(-1, index_type))),
     and_exprt(
       notequal_exprt(s0[witness], s1[shifted]),
       and_exprt(
-        s0.axiom_for_is_strictly_longer_than(witness),
+        s0.axiom_for_length_gt(witness),
         axiom_for_is_positive_index(witness))));
   implies_exprt a3(not_exprt(issuffix), constr3);
 
@@ -201,7 +201,7 @@ exprt string_constraint_generatort::add_axioms_for_contains(
   //      (forall startpos <= |s0| - |s1|.
   //         exists witness < |s1|. s1[witness] != s0[witness + startpos])
 
-  implies_exprt a1(contains, s0.axiom_for_is_longer_than(s1));
+  implies_exprt a1(contains, s0.axiom_for_length_ge(s1));
   axioms.push_back(a1);
 
   symbol_exprt startpos=fresh_exist_index("startpos_contains", index_type);
@@ -229,7 +229,7 @@ exprt string_constraint_generatort::add_axioms_for_contains(
   string_not_contains_constraintt a5(
     from_integer(0, index_type),
     plus_exprt(from_integer(1, index_type), length_diff),
-    and_exprt(not_exprt(contains), s0.axiom_for_is_longer_than(s1)),
+    and_exprt(not_exprt(contains), s0.axiom_for_length_ge(s1)),
     from_integer(0, index_type),
     s1.length(),
     s0,

src/solvers/refinement/string_constraint_generator_transformation.cpp

@@ -42,7 +42,7 @@ string_exprt string_constraint_generatort::add_axioms_for_set_length(
   string_constraintt a2(
     idx,
     res.length(),
-    s1.axiom_for_is_strictly_longer_than(idx),
+    s1.axiom_for_length_gt(idx),
     equal_exprt(s1[idx], res[idx]));
   axioms.push_back(a2);
 
@@ -51,7 +51,7 @@ string_exprt string_constraint_generatort::add_axioms_for_set_length(
   string_constraintt a3(
     idx2,
     res.length(),
-    s1.axiom_for_is_shorter_than(idx2),
+    s1.axiom_for_length_le(idx2),
     equal_exprt(res[idx2], constant_char(0, ref_type.get_char_type())));
   axioms.push_back(a3);
 
@@ -120,7 +120,7 @@ string_exprt string_constraint_generatort::add_axioms_for_substring(
   axioms.push_back(a2);
 
   // Warning: check what to do if the string is not long enough
-  axioms.push_back(str.axiom_for_is_longer_than(end));
+  axioms.push_back(str.axiom_for_length_ge(end));
 
   symbol_exprt idx=fresh_univ_index("QA_index_substring", index_type);
   string_constraintt a4(idx,
@@ -156,21 +156,21 @@ string_exprt string_constraint_generatort::add_axioms_for_trim(
   // a8 : forall n<|s1|, s[idx+n]=s1[n]
   // a9 : (s[m]>' ' &&s[m+|s1|-1]>' ') || m=|s|
 
-  exprt a1=str.axiom_for_is_longer_than(
+  exprt a1=str.axiom_for_length_ge(
     plus_exprt_with_overflow_check(idx, res.length()));
   axioms.push_back(a1);
 
   binary_relation_exprt a2(idx, ID_ge, from_integer(0, index_type));
   axioms.push_back(a2);
 
-  exprt a3=str.axiom_for_is_longer_than(idx);
+  exprt a3=str.axiom_for_length_ge(idx);
   axioms.push_back(a3);
 
-  exprt a4=res.axiom_for_is_longer_than(
+  exprt a4=res.axiom_for_length_ge(
     from_integer(0, index_type));
   axioms.push_back(a4);
 
-  exprt a5=res.axiom_for_is_shorter_than(str);
+  exprt a5=res.axiom_for_length_le(str);
   axioms.push_back(a5);
 
   symbol_exprt n=fresh_univ_index("QA_index_trim", index_type);

src/solvers/refinement/string_constraint_generator_valueof.cpp

@@ -222,8 +222,8 @@ string_exprt string_constraint_generatort::add_axioms_from_int_hex(
 
   size_t max_size=8;
   axioms.push_back(
-    and_exprt(res.axiom_for_is_strictly_longer_than(0),
-              res.axiom_for_is_shorter_than(max_size)));
+    and_exprt(res.axiom_for_length_gt(0),
+              res.axiom_for_length_le(max_size)));
 
   for(size_t size=1; size<=max_size; size++)
   {
@@ -322,8 +322,7 @@ void string_constraint_generatort::add_axioms_for_correct_number_format(
     is_digit_with_radix(chr, strict_formatting, radix_as_char, radix_ul);
 
   // |str| > 0
-  const exprt non_empty=
-    str.axiom_for_is_longer_than(from_integer(1, index_type));
+  const exprt non_empty=str.axiom_for_length_ge(from_integer(1, index_type));
   axioms.push_back(non_empty);
 
   if(strict_formatting)
@@ -343,11 +342,11 @@ void string_constraint_generatort::add_axioms_for_correct_number_format(
   // str[0]='+' or '-' ==> |str| > 1
   const implies_exprt contains_digit(
     or_exprt(starts_with_minus, starts_with_plus),
-    str.axiom_for_is_longer_than(from_integer(2, index_type)));
+    str.axiom_for_length_ge(from_integer(2, index_type)));
   axioms.push_back(contains_digit);
 
   // |str| <= max_size
-  axioms.push_back(str.axiom_for_is_shorter_than(max_size));
+  axioms.push_back(str.axiom_for_length_le(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
@@ -356,7 +355,7 @@ void string_constraint_generatort::add_axioms_for_correct_number_format(
   {
     /// index < length => is_digit_with_radix(str[index], radix)
     const implies_exprt character_at_index_is_digit(
-      str.axiom_for_is_longer_than(from_integer(index+1, index_type)),
+      str.axiom_for_length_ge(from_integer(index+1, index_type)),
       is_digit_with_radix(
         str[index], strict_formatting, radix_as_char, radix_ul));
     axioms.push_back(character_at_index_is_digit);

src/util/string_expr.h

@@ -53,59 +53,59 @@ class string_exprt: public struct_exprt
   }
 
   // Comparison on the length of the strings
-  binary_relation_exprt axiom_for_is_longer_than(
+  binary_relation_exprt axiom_for_length_ge(
     const string_exprt &rhs) const
   {
     return binary_relation_exprt(length(), ID_ge, rhs.length());
   }
 
-  binary_relation_exprt axiom_for_is_longer_than(
+  binary_relation_exprt axiom_for_length_ge(
     const exprt &rhs) const
   {
     return binary_relation_exprt(length(), ID_ge, rhs);
   }
 
-  binary_relation_exprt axiom_for_is_strictly_longer_than(
+  binary_relation_exprt axiom_for_length_gt(
     const exprt &rhs) const
   {
     return binary_relation_exprt(rhs, ID_lt, length());
   }
 
-  binary_relation_exprt axiom_for_is_strictly_longer_than(
+  binary_relation_exprt axiom_for_length_gt(
     const string_exprt &rhs) const
   {
     return binary_relation_exprt(rhs.length(), ID_lt, length());
   }
 
-  binary_relation_exprt axiom_for_is_strictly_longer_than(mp_integer i) const
+  binary_relation_exprt axiom_for_length_gt(mp_integer i) const
   {
-    return axiom_for_is_strictly_longer_than(from_integer(i, length().type()));
+    return axiom_for_length_gt(from_integer(i, length().type()));
   }
 
-  binary_relation_exprt axiom_for_is_shorter_than(
+  binary_relation_exprt axiom_for_length_le(
     const string_exprt &rhs) const
   {
     return binary_relation_exprt(length(), ID_le, rhs.length());
   }
 
-  binary_relation_exprt axiom_for_is_shorter_than(
+  binary_relation_exprt axiom_for_length_le(
     const exprt &rhs) const
   {
     return binary_relation_exprt(length(), ID_le, rhs);
   }
 
-  binary_relation_exprt axiom_for_is_shorter_than(mp_integer i) const
+  binary_relation_exprt axiom_for_length_le(mp_integer i) const
   {
-    return axiom_for_is_shorter_than(from_integer(i, length().type()));
+    return axiom_for_length_le(from_integer(i, length().type()));
   }
 
-  binary_relation_exprt axiom_for_is_strictly_shorter_than(
+  binary_relation_exprt axiom_for_length_lt(
     const string_exprt &rhs) const
   {
     return binary_relation_exprt(length(), ID_lt, rhs.length());
   }
 
-  binary_relation_exprt axiom_for_is_strictly_shorter_than(
+  binary_relation_exprt axiom_for_length_lt(
     const exprt &rhs) const
   {
     return binary_relation_exprt(length(), ID_lt, rhs);
@@ -132,15 +132,15 @@ class string_exprt: public struct_exprt
 
 inline string_exprt &to_string_expr(exprt &expr)
 {
-  assert(expr.id()==ID_struct);
-  assert(expr.operands().size()==2);
+  PRECONDITION(expr.id()==ID_struct);
+  PRECONDITION(expr.operands().size()==2);
   return static_cast<string_exprt &>(expr);
 }
 
 inline const string_exprt &to_string_expr(const exprt &expr)
 {
-  assert(expr.id()==ID_struct);
-  assert(expr.operands().size()==2);
+  PRECONDITION(expr.id()==ID_struct);
+  PRECONDITION(expr.operands().size()==2);
   return static_cast<const string_exprt &>(expr);
 }