Merge pull request #4608 from allredj/clean-up/strings-refactor-binary-relations

Clean-up string solver: refactor binary relations [TG-7439]

Author: Joel Allred

src/solvers/strings/string_constraint_generator_code_points.cpp

@@ -41,10 +41,10 @@ std::pair<exprt, string_constraintst> add_axioms_for_code_point(
   exprt hex0400 = from_integer(0x0400, type);
 
   binary_relation_exprt small(code_point, ID_lt, hex010000);
-  implies_exprt a1(small, length_eq(res, 1));
+  implies_exprt a1(small, equal_to(res.length(), 1));
   constraints.existential.push_back(a1);
 
-  implies_exprt a2(not_exprt(small), length_eq(res, 2));
+  implies_exprt a2(not_exprt(small), equal_to(res.length(), 2));
   constraints.existential.push_back(a2);
 
   typecast_exprt code_point_as_char(code_point, char_type);

src/solvers/strings/string_constraint_generator_comparison.cpp

@@ -208,7 +208,7 @@ string_constraint_generatort::add_axioms_for_hash_code(
       equal_exprt(it.first.length(), str.length()),
       and_exprt(
         notequal_exprt(str[i], it.first[i]),
-        and_exprt(length_gt(str, i), is_positive(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)};
@@ -271,12 +271,17 @@ 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()), length_gt(s1, x)),
-    and_exprt(length_ge(s1, s2.length()), length_gt(s2, 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)));
   const and_exprt cond1(ret_char_diff, guard1);
   const or_exprt guard2(
-    and_exprt(length_gt(s2, s1.length()), length_eq(s1, x)),
-    and_exprt(length_gt(s1, s2.length()), length_eq(s2, x)));
+    and_exprt(greater_than(s2.length(), s1.length()), equal_to(s1.length(), x)),
+    and_exprt(
+      greater_than(s1.length(), s2.length()), equal_to(s2.length(), x)));
   const and_exprt cond2(ret_length_diff, guard2);
 
   const implies_exprt a3(

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(length_gt(res, 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_testing.cpp

@@ -68,11 +68,12 @@ std::pair<exprt, string_constraintst> add_axioms_for_is_prefix(
     const exprt witness = fresh_symbol("witness_not_isprefix", index_type);
     const exprt strings_differ_at_witness = and_exprt(
       is_positive(witness),
-      length_gt(prefix, witness),
+      greater_than(prefix.length(), witness),
       notequal_exprt(str[plus_exprt(witness, offset)], prefix[witness]));
     const exprt s1_does_not_start_with_s0 = or_exprt(
       not_exprt(offset_within_bounds),
-      not_exprt(length_ge(str, plus_exprt(prefix.length(), offset))),
+      not_exprt(
+        greater_or_equal_to(str.length(), plus_exprt(prefix.length(), offset))),
       strings_differ_at_witness);
     return implies_exprt(not_exprt(isprefix), s1_does_not_start_with_s0);
   }());
@@ -138,8 +139,8 @@ std::pair<exprt, string_constraintst> add_axioms_for_is_empty(
   symbol_exprt is_empty = fresh_symbol("is_empty");
   array_string_exprt s0 = get_string_expr(array_pool, f.arguments()[0]);
   string_constraintst constraints;
-  constraints.existential = {implies_exprt(is_empty, length_eq(s0, 0)),
-                             implies_exprt(length_eq(s0, 0), is_empty)};
+  constraints.existential = {implies_exprt(is_empty, equal_to(s0.length(), 0)),
+                             implies_exprt(equal_to(s0.length(), 0), is_empty)};
   return {typecast_exprt(is_empty, f.type()), std::move(constraints)};
 }
 
@@ -186,7 +187,7 @@ std::pair<exprt, string_constraintst> add_axioms_for_is_suffix(
     get_string_expr(array_pool, args[swap_arguments ? 0u : 1u]);
   const typet &index_type = s0.length().type();
 
-  implies_exprt a1(issuffix, length_ge(s1, s0.length()));
+  implies_exprt a1(issuffix, greater_or_equal_to(s1.length(), s0.length()));
   constraints.existential.push_back(a1);
 
   symbol_exprt qvar = fresh_symbol("QA_suffix", index_type);
@@ -201,11 +202,11 @@ std::pair<exprt, string_constraintst> add_axioms_for_is_suffix(
   const plus_exprt shifted(witness, minus_exprt(s1.length(), s0.length()));
   or_exprt constr3(
     and_exprt(
-      length_gt(s0, s1.length()),
+      greater_than(s0.length(), s1.length()),
       equal_exprt(witness, from_integer(-1, index_type))),
     and_exprt(
       notequal_exprt(s0[witness], s1[shifted]),
-      and_exprt(length_gt(s0, witness), is_positive(witness))));
+      and_exprt(greater_than(s0.length(), witness), is_positive(witness))));
   implies_exprt a3(not_exprt(issuffix), constr3);
 
   constraints.existential.push_back(a3);
@@ -246,7 +247,8 @@ std::pair<exprt, string_constraintst> add_axioms_for_contains(
   const symbol_exprt contains = fresh_symbol("contains");
   const symbol_exprt startpos = fresh_symbol("startpos_contains", index_type);
 
-  const implies_exprt a1(contains, length_ge(s0, s1.length()));
+  const implies_exprt a1(
+    contains, greater_or_equal_to(s0.length(), s1.length()));
   constraints.existential.push_back(a1);
 
   minus_exprt length_diff(s0.length(), s1.length());
@@ -270,7 +272,8 @@ std::pair<exprt, string_constraintst> add_axioms_for_contains(
   const string_not_contains_constraintt a5 = {
     from_integer(0, index_type),
     plus_exprt(from_integer(1, index_type), length_diff),
-    and_exprt(not_exprt(contains), length_ge(s0, s1.length())),
+    and_exprt(
+      not_exprt(contains), greater_or_equal_to(s0.length(), s1.length())),
     from_integer(0, index_type),
     s1.length(),
     s0,

src/solvers/strings/string_constraint_generator_transformation.cpp

@@ -54,7 +54,7 @@ std::pair<exprt, string_constraintst> add_axioms_for_set_length(
   // a2 : forall i< min(|s1|, k) .res[i] = s1[i]
   // a3 : forall |s1| <= i < |res|. res[i] = 0
 
-  constraints.existential.push_back(length_eq(res, k));
+  constraints.existential.push_back(equal_to(res.length(), k));
 
   const symbol_exprt idx = fresh_symbol("QA_index_set_length", index_type);
   const string_constraintt a2(
@@ -197,18 +197,19 @@ std::pair<exprt, string_constraintst> add_axioms_for_trim(
 
   // Axiom 1.
   constraints.existential.push_back(
-    length_ge(str, plus_exprt(idx, res.length())));
+    greater_or_equal_to(str.length(), plus_exprt(idx, res.length())));
 
   binary_relation_exprt a2(idx, ID_ge, from_integer(0, index_type));
   constraints.existential.push_back(a2);
 
-  const exprt a3 = length_ge(str, idx);
+  const exprt a3 = greater_or_equal_to(str.length(), idx);
   constraints.existential.push_back(a3);
 
-  const exprt a4 = length_ge(res, from_integer(0, index_type));
+  const exprt a4 =
+    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

@@ -96,7 +96,7 @@ add_axioms_from_bool(const array_string_exprt &res, const exprt &b)
   // a4 : forall i < |"false"|. !eq => res[i]="false"[i]
 
   std::string str_true = "true";
-  const implies_exprt a1(eq, length_eq(res, str_true.length()));
+  const implies_exprt a1(eq, equal_to(res.length(), str_true.length()));
   constraints.existential.push_back(a1);
 
   for(std::size_t i = 0; i < str_true.length(); i++)
@@ -107,7 +107,8 @@ add_axioms_from_bool(const array_string_exprt &res, const exprt &b)
   }
 
   std::string str_false = "false";
-  const implies_exprt a3(not_exprt(eq), length_eq(res, str_false.length()));
+  const implies_exprt a3(
+    not_exprt(eq), equal_to(res.length(), str_false.length()));
   constraints.existential.push_back(a3);
 
   for(std::size_t i = 0; i < str_false.length(); i++)
@@ -229,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(length_gt(res, 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++)
   {
@@ -253,7 +255,7 @@ add_axioms_from_int_hex(const array_string_exprt &res, const exprt &i)
       all_numbers = and_exprt(all_numbers, is_number);
     }
 
-    const equal_exprt premise = length_eq(res, size);
+    const equal_exprt premise = equal_to(res.length(), size);
     constraints.existential.push_back(
       implies_exprt(premise, and_exprt(equal_exprt(i, sum), all_numbers)));
 
@@ -312,7 +314,7 @@ add_axioms_from_char(const array_string_exprt &res, const exprt &c)
 {
   string_constraintst constraints;
   constraints.existential = {
-    and_exprt(equal_exprt(res[0], c), length_eq(res, 1))};
+    and_exprt(equal_exprt(res[0], c), equal_to(res.length(), 1))};
   return {from_integer(0, get_return_code_type()), std::move(constraints)};
 }
 
@@ -344,7 +346,8 @@ string_constraintst add_axioms_for_correct_number_format(
     is_digit_with_radix(chr, strict_formatting, radix_as_char, radix_ul);
 
   // |str| > 0
-  const exprt non_empty = length_ge(str, from_integer(1, index_type));
+  const exprt non_empty =
+    greater_or_equal_to(str.length(), from_integer(1, index_type));
   constraints.existential.push_back(non_empty);
 
   if(strict_formatting)
@@ -364,11 +367,12 @@ string_constraintst add_axioms_for_correct_number_format(
   // str[0]='+' or '-' ==> |str| > 1
   const implies_exprt contains_digit(
     or_exprt(starts_with_minus, starts_with_plus),
-    length_ge(str, from_integer(2, index_type)));
+    greater_or_equal_to(str.length(), from_integer(2, index_type)));
   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
@@ -377,7 +381,7 @@ string_constraintst add_axioms_for_correct_number_format(
   {
     /// index < length => is_digit_with_radix(str[index], radix)
     const implies_exprt character_at_index_is_digit(
-      length_ge(str, from_integer(index + 1, index_type)),
+      greater_or_equal_to(str.length(), from_integer(index + 1, index_type)),
       is_digit_with_radix(
         str[index], strict_formatting, radix_as_char, radix_ul));
     constraints.existential.push_back(character_at_index_is_digit);
@@ -389,7 +393,8 @@ string_constraintst add_axioms_for_correct_number_format(
 
     // no_leading_zero : str[0] = '0' => |str| = 1
     const implies_exprt no_leading_zero(
-      equal_exprt(chr, zero_char), length_eq(str, from_integer(1, index_type)));
+      equal_exprt(chr, zero_char),
+      equal_to(str.length(), from_integer(1, index_type)));
     constraints.existential.push_back(no_leading_zero);
 
     // no_leading_zero_after_minus : str[0]='-' => str[1]!='0'
@@ -435,7 +440,7 @@ string_constraintst add_axioms_for_characters_in_integer_string(
   /// add_axioms_for_correct_number_format which say that the string must
   /// contain at least one digit, so we don't have to worry about "+" or "-".
   constraints.existential.push_back(
-    implies_exprt(length_eq(str, 1), equal_exprt(input_int, sum)));
+    implies_exprt(equal_to(str.length(), 1), equal_exprt(input_int, sum)));
 
   for(size_t size = 2; size <= max_string_length; size++)
   {
@@ -473,7 +478,7 @@ string_constraintst add_axioms_for_characters_in_integer_string(
     }
     sum = new_sum;
 
-    const equal_exprt premise = length_eq(str, size);
+    const equal_exprt premise = equal_to(str.length(), size);
 
     if(!digit_constraints.empty())
     {

src/util/string_expr.h

@@ -16,51 +16,44 @@ Author: Romain Brenguier, [email protected]
 #include "refined_string_type.h"
 #include "std_expr.h"
 
-// Comparison on the length of the strings
-template <typename T>
-binary_relation_exprt length_ge(const T &lhs, const exprt &rhs)
+inline binary_relation_exprt greater_or_equal_to(exprt lhs, exprt rhs)
 {
-  PRECONDITION(rhs.type() == lhs.length().type());
-  return binary_relation_exprt(lhs.length(), ID_ge, rhs);
+  PRECONDITION(rhs.type() == lhs.type());
+  return binary_relation_exprt(std::move(lhs), ID_ge, std::move(rhs));
 }
 
-template <typename T>
-binary_relation_exprt length_gt(const T &lhs, const exprt &rhs)
+inline binary_relation_exprt greater_than(exprt lhs, exprt rhs)
 {
-  PRECONDITION(rhs.type() == lhs.length().type());
-  return binary_relation_exprt(rhs, ID_lt, lhs.length());
+  PRECONDITION(rhs.type() == lhs.type());
+  return binary_relation_exprt(std::move(rhs), ID_lt, std::move(lhs));
 }
 
-template <typename T>
-binary_relation_exprt length_gt(const T &lhs, mp_integer i)
+inline binary_relation_exprt greater_than(const exprt &lhs, mp_integer i)
 {
-  return length_gt(lhs, from_integer(i, lhs.length().type()));
+  return binary_relation_exprt(from_integer(i, lhs.type()), ID_lt, lhs);
 }
 
-template <typename T>
-binary_relation_exprt length_le(const T &lhs, const exprt &rhs)
+inline binary_relation_exprt less_than_or_equal_to(exprt lhs, 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(std::move(lhs), ID_le, std::move(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 binary_relation_exprt(lhs, ID_le, from_integer(i, lhs.type()));
 }
 
-template <typename T>
-equal_exprt length_eq(const T &lhs, const exprt &rhs)
+inline equal_exprt equal_to(exprt lhs, exprt rhs)
 {
-  PRECONDITION(rhs.type() == lhs.length().type());
-  return equal_exprt(lhs.length(), rhs);
+  PRECONDITION(rhs.type() == lhs.type());
+  return equal_exprt(std::move(lhs), std::move(rhs));
 }
 
-template <typename T>
-equal_exprt length_eq(const T &lhs, mp_integer i)
+inline equal_exprt equal_to(const exprt &lhs, mp_integer i)
 {
-  return length_eq(lhs, from_integer(i, lhs.length().type()));
+  return equal_exprt(lhs, from_integer(i, lhs.type()));
 }
 
 // Representation of strings as arrays