Merge pull request #1258 from romainbrenguier/cleaning/string-expr-function-renaming

Rename string expr functions having misleading names

Author: mgudemann

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_concat.cpp

@@ -171,7 +171,7 @@ string_exprt string_constraint_generatort::add_axioms_for_concat_double(
   const function_application_exprt &f)
 {
   string_exprt s1=get_string_expr(args(f, 2)[0]);
-  PRECONDITION(refined_string_typet::is_refined_string_type(f.type()));
+  PRECONDITION(is_refined_string_type(f.type()));
   refined_string_typet ref_type=to_refined_string_type(f.type());
   string_exprt s2=add_axioms_for_string_of_float(args(f, 2)[1], ref_type);
   return add_axioms_for_concat(s1, s2);
@@ -184,7 +184,7 @@ string_exprt string_constraint_generatort::add_axioms_for_concat_float(
   const function_application_exprt &f)
 {
   string_exprt s1=get_string_expr(args(f, 2)[0]);
-  PRECONDITION(refined_string_typet::is_refined_string_type(f.type()));
+  PRECONDITION(is_refined_string_type(f.type()));
   refined_string_typet ref_type=to_refined_string_type(f.type());
   string_exprt s2=add_axioms_for_string_of_float(args(f, 2)[1], ref_type);
   return add_axioms_for_concat(s1, s2);

src/solvers/refinement/string_constraint_generator_constants.cpp

@@ -56,7 +56,7 @@ string_exprt string_constraint_generatort::add_axioms_for_empty_string(
   const function_application_exprt &f)
 {
   PRECONDITION(f.arguments().empty());
-  PRECONDITION(refined_string_typet::is_refined_string_type(f.type()));
+  PRECONDITION(is_refined_string_type(f.type()));
   const refined_string_typet &ref_type=to_refined_string_type(f.type());
   return empty_string(ref_type);
 }

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_indexof.cpp

@@ -252,7 +252,7 @@ exprt string_constraint_generatort::add_axioms_for_index_of(
   else
   {
     INVARIANT(
-      refined_string_typet::is_refined_string_type(c.type()),
+      is_refined_string_type(c.type()),
       string_refinement_invariantt("c can only be a (un)signedbv or a refined "
         "string and the (un)signedbv case is already handled"));
     string_exprt sub=get_string_expr(c);

src/solvers/refinement/string_constraint_generator_main.cpp

@@ -131,7 +131,7 @@ string_exprt string_constraint_generatort::fresh_string(
 /// \return a string expression
 string_exprt string_constraint_generatort::get_string_expr(const exprt &expr)
 {
-  PRECONDITION(refined_string_typet::is_refined_string_type(expr.type()));
+  PRECONDITION(is_refined_string_type(expr.type()));
 
   if(expr.id()==ID_symbol)
   {
@@ -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)
   {
@@ -180,7 +180,7 @@ void string_constraint_generatort::add_default_axioms(
 string_exprt string_constraint_generatort::add_axioms_for_refined_string(
   const exprt &string)
 {
-  PRECONDITION(refined_string_typet::is_refined_string_type(string.type()));
+  PRECONDITION(is_refined_string_type(string.type()));
   refined_string_typet type=to_refined_string_type(string.type());
 
   // Function applications should have been removed before
@@ -246,11 +246,9 @@ string_exprt string_constraint_generatort::add_axioms_for_refined_string(
 string_exprt string_constraint_generatort::add_axioms_for_if(
   const if_exprt &expr)
 {
-  PRECONDITION(
-    refined_string_typet::is_refined_string_type(expr.true_case().type()));
+  PRECONDITION(is_refined_string_type(expr.true_case().type()));
   string_exprt t=get_string_expr(expr.true_case());
-  PRECONDITION(
-    refined_string_typet::is_refined_string_type(expr.false_case().type()));
+  PRECONDITION(is_refined_string_type(expr.false_case().type()));
   string_exprt f=get_string_expr(expr.false_case());
   const refined_string_typet &ref_type=to_refined_string_type(t.type());
   const typet &index_type=ref_type.get_index_type();

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/solvers/refinement/string_refinement.cpp

@@ -162,7 +162,7 @@ void string_refinementt::add_symbol_to_symbol_map(
                rhs.id()==ID_array_of ||
                rhs.id()==ID_if ||
                (rhs.id()==ID_struct &&
-                refined_string_typet::is_refined_string_type(rhs.type())));
+                is_refined_string_type(rhs.type())));
 
   // We insert the mapped value of the rhs, if it exists.
   auto it=symbol_resolve.find(rhs);
@@ -279,7 +279,7 @@ bool string_refinementt::add_axioms_for_string_assigns(
       return true;
     }
   }
-  if(refined_string_typet::is_refined_string_type(rhs.type()))
+  if(is_refined_string_type(rhs.type()))
   {
     exprt refined_rhs=generator.add_axioms_for_refined_string(rhs);
     add_symbol_to_symbol_map(lhs, refined_rhs);
@@ -302,7 +302,7 @@ bool string_refinementt::add_axioms_for_string_assigns(
 ///          last value that has been initialized.
 void string_refinementt::concretize_string(const exprt &expr)
 {
-  if(refined_string_typet::is_refined_string_type(expr.type()))
+  if(is_refined_string_type(expr.type()))
   {
     string_exprt str=to_string_expr(expr);
     exprt length=get(str.length());
@@ -392,7 +392,7 @@ void string_refinementt::concretize_lengths()
 {
   for(const auto &it : symbol_resolve)
   {
-    if(refined_string_typet::is_refined_string_type(it.second.type()))
+    if(is_refined_string_type(it.second.type()))
     {
       string_exprt str=to_string_expr(it.second);
       exprt length=get(str.length());
@@ -403,7 +403,7 @@ void string_refinementt::concretize_lengths()
   }
   for(const auto &it : generator.created_strings)
   {
-    if(refined_string_typet::is_refined_string_type(it.type()))
+    if(is_refined_string_type(it.type()))
     {
       string_exprt str=to_string_expr(it);
       exprt length=get(str.length());
@@ -429,12 +429,10 @@ void string_refinementt::set_to(const exprt &expr, bool value)
 
     // The assignment of a string equality to false is not supported.
     PRECONDITION(value || !is_char_array(rhs.type()));
-    PRECONDITION(value ||
-      !refined_string_typet::is_refined_string_type(rhs.type()));
+    PRECONDITION(value || !is_refined_string_type(rhs.type()));
 
     PRECONDITION(lhs.id()==ID_symbol || !is_char_array(rhs.type()));
-    PRECONDITION(lhs.id()==ID_symbol ||
-      !refined_string_typet::is_refined_string_type(rhs.type()));
+    PRECONDITION(lhs.id()==ID_symbol || !is_refined_string_type(rhs.type()));
 
     // If lhs is not a symbol, let supert::set_to() handle it.
     if(lhs.id()!=ID_symbol)
@@ -811,7 +809,7 @@ void string_refinementt::debug_model()
   const std::string indent("  ");
   for(auto it : symbol_resolve)
   {
-    if(refined_string_typet::is_refined_string_type(it.second.type()))
+    if(is_refined_string_type(it.second.type()))
     {
       debug() << "- " << from_expr(ns, "", to_symbol_expr(it.first)) << ":\n";
       string_exprt refined=to_string_expr(it.second);
@@ -1684,8 +1682,7 @@ exprt string_refinementt::get(const exprt &expr) const
     if(it!=found_length.end())
       return get_array(ecopy, it->second);
   }
-  else if(refined_string_typet::is_refined_string_type(ecopy.type()) &&
-          ecopy.id()==ID_struct)
+  else if(is_refined_string_type(ecopy.type()) && ecopy.id()==ID_struct)
   {
     const string_exprt &string=to_string_expr(ecopy);
     const exprt &content=string.content();

src/util/refined_string_type.cpp

@@ -16,8 +16,6 @@ Author: Romain Brenguier, [email protected]
 ///   `content` of type `content_type`. This module also defines functions to
 ///   recognise the C and java string types.
 
-#include <util/cprover_prefix.h>
-
 #include "refined_string_type.h"
 
 refined_string_typet::refined_string_typet(
@@ -29,13 +27,3 @@ refined_string_typet::refined_string_typet(
   components().emplace_back("content", char_array);
   set_tag(CPROVER_PREFIX"refined_string_type");
 }
-
-/// \par parameters: a type
-/// \return Boolean telling whether the input is a refined string type
-bool refined_string_typet::is_refined_string_type(const typet &type)
-{
-  return
-    type.id()==ID_struct &&
-    to_struct_type(type).get_tag()==CPROVER_PREFIX"refined_string_type";
-}
-