Merge pull request #1932 from romainbrenguier/stop-adding-counter-examples

[TG-2459] Only add counter examples when index set is exhausted

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()));
 }