Fix string constraints

For the PASS algorithm, the premise should be of a form that can be
analyzed by the index set construction.
For now the index set only works with the explicit bounds of the string
constraints, so the premise should not be used for now.

Author: romainbrenguier

src/solvers/refinement/string_constraint.h

@@ -93,36 +93,25 @@ class string_constraintt : public exprt
     const symbol_exprt &_univ_var,
     const exprt &bound_inf,
     const exprt &bound_sup,
-    const exprt &prem,
     const exprt &body):
     exprt(ID_string_constraint)
   {
-    copy_to_operands(prem, body);
+    copy_to_operands(true_exprt(), body);
     copy_to_operands(_univ_var, bound_sup, bound_inf);
   }
 
   // Default bound inferior is 0
   string_constraintt(
     const symbol_exprt &_univ_var,
     const exprt &bound_sup,
-    const exprt &prem,
     const exprt &body):
     string_constraintt(
       _univ_var,
       from_integer(0, _univ_var.type()),
       bound_sup,
-      prem,
       body)
   {}
 
-  // Default premise is true
-  string_constraintt(
-    const symbol_exprt &_univ_var,
-    const exprt &bound_sup,
-    const exprt &body):
-    string_constraintt(_univ_var, bound_sup, true_exprt(), body)
-  {}
-
   exprt univ_within_bounds() const
   {
     return and_exprt(

src/solvers/refinement/string_constraint_generator.h

@@ -436,4 +436,7 @@ size_t max_printed_string_length(const typet &type, unsigned long ul_radix);
 std::string
 utf16_constant_array_to_java(const array_exprt &arr, std::size_t length);
 
+/// \return expression representing the minimum of two expressions
+exprt minimum(const exprt &a, const exprt &b);
+
 #endif

src/solvers/refinement/string_constraint_generator_comparison.cpp

@@ -43,7 +43,8 @@ exprt string_constraint_generatort::add_axioms_for_equals(
   lemmas.push_back(a1);
 
   symbol_exprt qvar=fresh_univ_index("QA_equal", index_type);
-  string_constraintt a2(qvar, s1.length(), eq, equal_exprt(s1[qvar], s2[qvar]));
+  string_constraintt a2(
+    qvar, s1.length(), implies_exprt(eq, equal_exprt(s1[qvar], s2[qvar])));
   constraints.push_back(a2);
 
   symbol_exprt witness=fresh_exist_index("witness_unequal", index_type);
@@ -130,7 +131,7 @@ exprt string_constraint_generatort::add_axioms_for_equals_ignore_case(
     fresh_univ_index("QA_equal_ignore_case", index_type);
   const exprt constr2 =
     character_equals_ignore_case(s1[qvar], s2[qvar], char_a, char_A, char_Z);
-  const string_constraintt a2(qvar, s1.length(), eq, constr2);
+  const string_constraintt a2(qvar, s1.length(), implies_exprt(eq, constr2));
   constraints.push_back(a2);
 
   const symbol_exprt witness =
@@ -224,7 +225,7 @@ exprt string_constraint_generatort::add_axioms_for_compare_to(
 
   const symbol_exprt i = fresh_univ_index("QA_compare_to", index_type);
   const string_constraintt a2(
-    i, s1.length(), res_null, equal_exprt(s1[i], s2[i]));
+    i, s1.length(), implies_exprt(res_null, equal_exprt(s1[i], s2[i])));
   constraints.push_back(a2);
 
   const symbol_exprt x = fresh_exist_index("index_compare_to", index_type);
@@ -255,7 +256,7 @@ exprt string_constraint_generatort::add_axioms_for_compare_to(
 
   const symbol_exprt i2 = fresh_univ_index("QA_compare_to", index_type);
   const string_constraintt a4(
-    i2, x, not_exprt(res_null), equal_exprt(s1[i2], s2[i2]));
+    i2, x, implies_exprt(not_exprt(res_null), equal_exprt(s1[i2], s2[i2])));
   constraints.push_back(a4);
 
   return res;

src/solvers/refinement/string_constraint_generator_indexof.cpp

@@ -65,16 +65,15 @@ exprt string_constraint_generatort::add_axioms_for_index_of(
 
   symbol_exprt n=fresh_univ_index("QA_index_of", index_type);
   string_constraintt a4(
-    n, lower_bound, index, contains, not_exprt(equal_exprt(str[n], c)));
+    n, lower_bound, index, implies_exprt(contains, notequal_exprt(str[n], c)));
   constraints.push_back(a4);
 
   symbol_exprt m=fresh_univ_index("QA_index_of", index_type);
   string_constraintt a5(
     m,
     lower_bound,
     str.length(),
-    not_exprt(contains),
-    not_exprt(equal_exprt(str[m], c)));
+    implies_exprt(not_exprt(contains), not_exprt(equal_exprt(str[m], c))));
   constraints.push_back(a5);
 
   return index;
@@ -130,8 +129,8 @@ exprt string_constraint_generatort::add_axioms_for_index_of_string(
   string_constraintt a3(
     qvar,
     needle.length(),
-    contains,
-    equal_exprt(haystack[plus_exprt(qvar, offset)], needle[qvar]));
+    implies_exprt(
+      contains, equal_exprt(haystack[plus_exprt(qvar, offset)], needle[qvar])));
   constraints.push_back(a3);
 
   // string_not contains_constraintt are formulas of the form:
@@ -221,7 +220,8 @@ exprt string_constraint_generatort::add_axioms_for_last_index_of_string(
 
   symbol_exprt qvar=fresh_univ_index("QA_index_of_string", index_type);
   equal_exprt constr3(haystack[plus_exprt(qvar, offset)], needle[qvar]);
-  string_constraintt a3(qvar, needle.length(), contains, constr3);
+  const string_constraintt a3(
+    qvar, needle.length(), implies_exprt(contains, constr3));
   constraints.push_back(a3);
 
   // end_index is min(from_index, |str| - |substring|)
@@ -364,13 +364,14 @@ exprt string_constraint_generatort::add_axioms_for_last_index_of(
     n,
     plus_exprt(index, index1),
     end_index,
-    contains,
-    notequal_exprt(str[n], c));
+    implies_exprt(contains, notequal_exprt(str[n], c)));
   constraints.push_back(a4);
 
   const symbol_exprt m = fresh_univ_index("QA_last_index_of2", index_type);
   const string_constraintt a5(
-    m, end_index, not_exprt(contains), notequal_exprt(str[m], c));
+    m,
+    end_index,
+    implies_exprt(not_exprt(contains), notequal_exprt(str[m], c)));
   constraints.push_back(a5);
 
   return index;

src/solvers/refinement/string_constraint_generator_main.cpp

@@ -369,7 +369,7 @@ void string_constraint_generatort::add_constraint_on_characters(
   const and_exprt char_in_set(
     binary_relation_exprt(chr, ID_ge, from_integer(low_char, chr.type())),
     binary_relation_exprt(chr, ID_le, from_integer(high_char, chr.type())));
-  const string_constraintt sc(qvar, start, end, true_exprt(), char_in_set);
+  const string_constraintt sc(qvar, start, end, char_in_set);
   constraints.push_back(sc);
 }
 
@@ -662,3 +662,8 @@ exprt string_constraint_generatort::add_axioms_for_char_at(
   lemmas.push_back(equal_exprt(char_sym, str[f.arguments()[1]]));
   return char_sym;
 }
+
+exprt minimum(const exprt &a, const exprt &b)
+{
+  return if_exprt(binary_relation_exprt(a, ID_le, b), a, b);
+}

src/solvers/refinement/string_constraint_generator_testing.cpp

@@ -46,8 +46,8 @@ exprt string_constraint_generatort::add_axioms_for_is_prefix(
   string_constraintt a2(
     qvar,
     prefix.length(),
-    isprefix,
-    equal_exprt(str[plus_exprt(qvar, offset)], prefix[qvar]));
+    implies_exprt(
+      isprefix, equal_exprt(str[plus_exprt(qvar, offset)], prefix[qvar])));
   constraints.push_back(a2);
 
   symbol_exprt witness=fresh_exist_index("witness_not_isprefix", index_type);
@@ -153,7 +153,9 @@ exprt string_constraint_generatort::add_axioms_for_is_suffix(
   symbol_exprt qvar=fresh_univ_index("QA_suffix", index_type);
   const plus_exprt qvar_shifted(qvar, minus_exprt(s1.length(), s0.length()));
   string_constraintt a2(
-    qvar, s0.length(), issuffix, equal_exprt(s0[qvar], s1[qvar_shifted]));
+    qvar,
+    s0.length(),
+    implies_exprt(issuffix, equal_exprt(s0[qvar], s1[qvar_shifted])));
   constraints.push_back(a2);
 
   symbol_exprt witness=fresh_exist_index("witness_not_suffix", index_type);
@@ -221,7 +223,9 @@ exprt string_constraint_generatort::add_axioms_for_contains(
   symbol_exprt qvar=fresh_univ_index("QA_contains", index_type);
   const plus_exprt qvar_shifted(qvar, startpos);
   string_constraintt a4(
-    qvar, s1.length(), contains, equal_exprt(s1[qvar], s0[qvar_shifted]));
+    qvar,
+    s1.length(),
+    implies_exprt(contains, equal_exprt(s1[qvar], s0[qvar_shifted])));
   constraints.push_back(a4);
 
   string_not_contains_constraintt a5(

src/solvers/refinement/string_constraint_generator_transformation.cpp

@@ -45,24 +45,21 @@ exprt string_constraint_generatort::add_axioms_for_set_length(
 
   // We add axioms:
   // a1 : |res|=k
-  // a2 : forall i<|res|. i < |s1|  ==> res[i] = s1[i]
-  // a3 : forall i<|res|. i >= |s1| ==> res[i] = 0
+  // a2 : forall i< min(|s1|, k) .res[i] = s1[i]
+  // a3 : forall |s1| <= i < |res|. res[i] = 0
 
   lemmas.push_back(res.axiom_for_has_length(k));
 
-  symbol_exprt idx = fresh_univ_index("QA_index_set_length", index_type);
-  string_constraintt a2(
-    idx,
-    res.length(),
-    s1.axiom_for_length_gt(idx),
-    equal_exprt(s1[idx], res[idx]));
+  const symbol_exprt idx = fresh_univ_index("QA_index_set_length", index_type);
+  const string_constraintt a2(
+    idx, minimum(s1.length(), k), equal_exprt(s1[idx], res[idx]));
   constraints.push_back(a2);
 
   symbol_exprt idx2 = fresh_univ_index("QA_index_set_length2", index_type);
   string_constraintt a3(
     idx2,
+    s1.length(),
     res.length(),
-    s1.axiom_for_length_le(idx2),
     equal_exprt(res[idx2], constant_char(0, char_type)));
   constraints.push_back(a3);
 
@@ -395,8 +392,8 @@ exprt string_constraint_generatort::add_axioms_for_to_upper_case(
 /// These axioms are:
 ///   1. \f$ |{\tt res}| = |{\tt str}|\f$
 ///   2. \f$ {\tt res}[{\tt pos}]={\tt char}\f$
-///   3. \f$ \forall i<|{\tt res}|.\ i \ne {\tt pos}
-///          \Rightarrow {\tt res}[i] = {\tt str}[i]\f$
+///   3. \f$ \forall i < min(|{\tt res}|, pos). {\tt res}[i] = {\tt str}[i]\f$
+///   4. \f$ \forall pos+1 <= i < |{\tt res}|.\ {\tt res}[i] = {\tt str}[i]\f$
 /// \param f: function application with arguments integer `|res|`, character
 ///           pointer `&res[0]`, refined_string `str`, integer `pos`,
 ///           and character `char`
@@ -413,14 +410,22 @@ exprt string_constraint_generatort::add_axioms_for_char_set(
   const exprt &character = f.arguments()[4];
 
   const binary_relation_exprt out_of_bounds(position, ID_ge, str.length());
-  lemmas.push_back(equal_exprt(res.length(), str.length()));
-  lemmas.push_back(equal_exprt(res[position], character));
+  const equal_exprt a1(res.length(), str.length());
+  lemmas.push_back(a1);
+  const equal_exprt a2(res[position], character);
+  lemmas.push_back(a2);
+
   const symbol_exprt q = fresh_univ_index("QA_char_set", position.type());
-  equal_exprt a3_body(res[q], str[q]);
-  notequal_exprt a3_guard(q, position);
-  constraints.push_back(
-    string_constraintt(
-      q, from_integer(0, q.type()), res.length(), a3_guard, a3_body));
+  const equal_exprt a3_body(res[q], str[q]);
+  const string_constraintt a3(q, minimum(res.length(), position), a3_body);
+  constraints.push_back(a3);
+
+  const symbol_exprt q2 = fresh_univ_index("QA_char_set2", position.type());
+  const plus_exprt lower_bound(position, from_integer(1, position.type()));
+  const equal_exprt a4_body(res[q2], str[q2]);
+  const string_constraintt a4(q2, lower_bound, res.length(), a4_body);
+  constraints.push_back(a4);
+
   return if_exprt(
     out_of_bounds, from_integer(1, f.type()), from_integer(0, f.type()));
 }

src/solvers/refinement/string_refinement.cpp

@@ -1549,10 +1549,12 @@ static std::pair<bool, std::vector<exprt>> check_axioms(
     const exprt &bound_inf=axiom.lower_bound();
     const exprt &bound_sup=axiom.upper_bound();
     const exprt &prem=axiom.premise();
+    INVARIANT(
+      prem == true_exprt(), "string constraint premises are not supported");
     const exprt &body=axiom.body();
 
     const string_constraintt axiom_in_model(
-      univ_var, get(bound_inf), get(bound_sup), get(prem), get(body));
+      univ_var, get(bound_inf), get(bound_sup), get(body));
 
     exprt negaxiom=negation_of_constraint(axiom_in_model);
     negaxiom = simplify_expr(negaxiom, ns);