Merge pull request #1728 from romainbrenguier/refactor/split-axiom-vectors

Split string generator axioms into separate vectors

Author: romainbrenguier

src/solvers/refinement/string_constraint_generator.h

@@ -48,7 +48,10 @@ class string_constraint_generatort final
 
   /// Axioms are of three kinds: universally quantified string constraint,
   /// not contains string constraints and simple formulas.
-  const std::vector<exprt> &get_axioms() const;
+  const std::vector<exprt> &get_lemmas() const;
+  const std::vector<string_constraintt> &get_constraints() const;
+  const std::vector<string_not_contains_constraintt> &
+  get_not_contains_constraints() const;
 
   /// Boolean symbols for the results of some string functions
   const std::vector<symbol_exprt> &get_boolean_symbols() const;
@@ -349,7 +352,9 @@ class string_constraint_generatort final
   unsigned symbol_count=0;
   const messaget message;
 
-  std::vector<exprt> axioms;
+  std::vector<exprt> lemmas;
+  std::vector<string_constraintt> constraints;
+  std::vector<string_not_contains_constraintt> not_contains_constraints;
   std::vector<symbol_exprt> boolean_symbols;
   std::vector<symbol_exprt> index_symbols;
   const namespacet ns;

src/solvers/refinement/string_constraint_generator_code_points.cpp

@@ -41,27 +41,27 @@ exprt string_constraint_generatort::add_axioms_for_code_point(
 
   binary_relation_exprt small(code_point, ID_lt, hex010000);
   implies_exprt a1(small, res.axiom_for_has_length(1));
-  axioms.push_back(a1);
+  lemmas.push_back(a1);
 
   implies_exprt a2(not_exprt(small), res.axiom_for_has_length(2));
-  axioms.push_back(a2);
+  lemmas.push_back(a2);
 
   typecast_exprt code_point_as_char(code_point, char_type);
   implies_exprt a3(small, equal_exprt(res[0], code_point_as_char));
-  axioms.push_back(a3);
+  lemmas.push_back(a3);
 
   plus_exprt first_char(
     hexD800, div_exprt(minus_exprt(code_point, hex010000), hex0400));
   implies_exprt a4(
     not_exprt(small),
     equal_exprt(res[0], typecast_exprt(first_char, char_type)));
-  axioms.push_back(a4);
+  lemmas.push_back(a4);
 
   plus_exprt second_char(hexDC00, mod_exprt(code_point, hex0400));
   implies_exprt a5(
     not_exprt(small),
     equal_exprt(res[1], typecast_exprt(second_char, char_type)));
-  axioms.push_back(a5);
+  lemmas.push_back(a5);
 
   return from_integer(0, get_return_code_type());
 }
@@ -136,8 +136,8 @@ exprt string_constraint_generatort::add_axioms_for_code_point_at(
     is_low_surrogate(str[plus_exprt_with_overflow_check(pos, index1)]);
   const and_exprt return_pair(is_high_surrogate(str[pos]), is_low);
 
-  axioms.push_back(implies_exprt(return_pair, equal_exprt(result, pair)));
-  axioms.push_back(
+  lemmas.push_back(implies_exprt(return_pair, equal_exprt(result, pair)));
+  lemmas.push_back(
     implies_exprt(not_exprt(return_pair), equal_exprt(result, char1_as_int)));
   return result;
 }
@@ -167,8 +167,8 @@ exprt string_constraint_generatort::add_axioms_for_code_point_before(
   const and_exprt return_pair(
     is_high_surrogate(char1), is_low_surrogate(char2));
 
-  axioms.push_back(implies_exprt(return_pair, equal_exprt(result, pair)));
-  axioms.push_back(
+  lemmas.push_back(implies_exprt(return_pair, equal_exprt(result, pair)));
+  lemmas.push_back(
     implies_exprt(not_exprt(return_pair), equal_exprt(result, char2_as_int)));
   return result;
 }
@@ -189,8 +189,8 @@ exprt string_constraint_generatort::add_axioms_for_code_point_count(
   const symbol_exprt result = fresh_symbol("code_point_count", return_type);
   const minus_exprt length(end, begin);
   const div_exprt minimum(length, from_integer(2, length.type()));
-  axioms.push_back(binary_relation_exprt(result, ID_le, length));
-  axioms.push_back(binary_relation_exprt(result, ID_ge, minimum));
+  lemmas.push_back(binary_relation_exprt(result, ID_le, length));
+  lemmas.push_back(binary_relation_exprt(result, ID_ge, minimum));
 
   return result;
 }
@@ -212,8 +212,8 @@ exprt string_constraint_generatort::add_axioms_for_offset_by_code_point(
 
   const exprt minimum = plus_exprt_with_overflow_check(index, offset);
   const exprt maximum = plus_exprt_with_overflow_check(minimum, offset);
-  axioms.push_back(binary_relation_exprt(result, ID_le, maximum));
-  axioms.push_back(binary_relation_exprt(result, ID_ge, minimum));
+  lemmas.push_back(binary_relation_exprt(result, ID_le, maximum));
+  lemmas.push_back(binary_relation_exprt(result, ID_ge, minimum));
 
   return result;
 }

src/solvers/refinement/string_constraint_generator_comparison.cpp

@@ -40,11 +40,11 @@ exprt string_constraint_generatort::add_axioms_for_equals(
 
 
   implies_exprt a1(eq, equal_exprt(s1.length(), s2.length()));
-  axioms.push_back(a1);
+  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]));
-  axioms.push_back(a2);
+  constraints.push_back(a2);
 
   symbol_exprt witness=fresh_exist_index("witness_unequal", index_type);
   exprt zero=from_integer(0, index_type);
@@ -56,7 +56,7 @@ exprt string_constraint_generatort::add_axioms_for_equals(
     notequal_exprt(s1.length(), s2.length()),
     equal_exprt(witness, from_integer(-1, index_type)));
   implies_exprt a3(not_exprt(eq), or_exprt(diff_length, witnessing));
-  axioms.push_back(a3);
+  lemmas.push_back(a3);
 
   return tc_eq;
 }
@@ -124,14 +124,14 @@ exprt string_constraint_generatort::add_axioms_for_equals_ignore_case(
   const typet index_type = s1.length().type();
 
   const implies_exprt a1(eq, equal_exprt(s1.length(), s2.length()));
-  axioms.push_back(a1);
+  lemmas.push_back(a1);
 
   const symbol_exprt qvar =
     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);
-  axioms.push_back(a2);
+  constraints.push_back(a2);
 
   const symbol_exprt witness =
     fresh_exist_index("witness_unequal_ignore_case", index_type);
@@ -147,7 +147,7 @@ exprt string_constraint_generatort::add_axioms_for_equals_ignore_case(
     or_exprt(
       notequal_exprt(s1.length(), s2.length()),
       and_exprt(bound_witness, witness_diff)));
-  axioms.push_back(a3);
+  lemmas.push_back(a3);
 
   return typecast_exprt(eq, f.type());
 }
@@ -183,7 +183,7 @@ exprt string_constraint_generatort::add_axioms_for_hash_code(
       and_exprt(
         notequal_exprt(str[i], it.first[i]),
         and_exprt(str.axiom_for_length_gt(i), axiom_for_is_positive_index(i))));
-    axioms.push_back(or_exprt(c1, or_exprt(c2, c3)));
+    lemmas.push_back(or_exprt(c1, or_exprt(c2, c3)));
   }
   return hash;
 }
@@ -220,12 +220,12 @@ exprt string_constraint_generatort::add_axioms_for_compare_to(
 
   const equal_exprt res_null(res, from_integer(0, return_type));
   const implies_exprt a1(res_null, equal_exprt(s1.length(), s2.length()));
-  axioms.push_back(a1);
+  lemmas.push_back(a1);
 
   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]));
-  axioms.push_back(a2);
+  constraints.push_back(a2);
 
   const symbol_exprt x = fresh_exist_index("index_compare_to", index_type);
   const equal_exprt ret_char_diff(
@@ -251,12 +251,12 @@ exprt string_constraint_generatort::add_axioms_for_compare_to(
     and_exprt(
       binary_relation_exprt(x, ID_ge, from_integer(0, return_type)),
       or_exprt(cond1, cond2)));
-  axioms.push_back(a3);
+  lemmas.push_back(a3);
 
   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]));
-  axioms.push_back(a4);
+  constraints.push_back(a4);
 
   return res;
 }
@@ -287,14 +287,14 @@ symbol_exprt string_constraint_generatort::add_axioms_for_intern(
   exprt::operandst disj;
   for(auto it : intern_of_string)
     disj.push_back(equal_exprt(intern, it.second));
-  axioms.push_back(disjunction(disj));
+  lemmas.push_back(disjunction(disj));
 
   // WARNING: the specification may be incomplete or incorrect
   for(auto it : intern_of_string)
     if(it.second!=str)
     {
       symbol_exprt i=fresh_exist_index("index_intern", index_type);
-      axioms.push_back(
+      lemmas.push_back(
         or_exprt(
           equal_exprt(it.second, intern),
           or_exprt(

src/solvers/refinement/string_constraint_generator_concat.cpp

@@ -49,20 +49,20 @@ exprt string_constraint_generatort::add_axioms_for_concat_substr(
   exprt res_length=plus_exprt_with_overflow_check(
     s1.length(), minus_exprt(end_index, start_index));
   implies_exprt a1(prem, equal_exprt(res.length(), res_length));
-  axioms.push_back(a1);
+  lemmas.push_back(a1);
 
   implies_exprt a2(not_exprt(prem), equal_exprt(res.length(), s1.length()));
-  axioms.push_back(a2);
+  lemmas.push_back(a2);
 
   symbol_exprt idx=fresh_univ_index("QA_index_concat", res.length().type());
   string_constraintt a3(idx, s1.length(), equal_exprt(s1[idx], res[idx]));
-  axioms.push_back(a3);
+  constraints.push_back(a3);
 
   symbol_exprt idx2=fresh_univ_index("QA_index_concat2", res.length().type());
   equal_exprt res_eq(
     res[plus_exprt(idx2, s1.length())], s2[plus_exprt(start_index, idx2)]);
   string_constraintt a4(idx2, minus_exprt(end_index, start_index), res_eq);
-  axioms.push_back(a4);
+  constraints.push_back(a4);
 
   // We should have a enum type for the possible error codes
   return from_integer(0, res.length().type());
@@ -87,14 +87,14 @@ exprt string_constraint_generatort::add_axioms_for_concat_char(
   const typet &index_type = res.length().type();
   const equal_exprt a1(
     res.length(), plus_exprt(s1.length(), from_integer(1, index_type)));
-  axioms.push_back(a1);
+  lemmas.push_back(a1);
 
   symbol_exprt idx = fresh_univ_index("QA_index_concat_char", index_type);
   string_constraintt a2(idx, s1.length(), equal_exprt(s1[idx], res[idx]));
-  axioms.push_back(a2);
+  constraints.push_back(a2);
 
   equal_exprt a3(res[s1.length()], c);
-  axioms.push_back(a3);
+  lemmas.push_back(a3);
 
   // We should have a enum type for the possible error codes
   return from_integer(0, get_return_code_type());

src/solvers/refinement/string_constraint_generator_constants.cpp

@@ -45,12 +45,12 @@ exprt string_constraint_generatort::add_axioms_for_constant(
     const exprt idx = from_integer(i, index_type);
     const exprt c = from_integer(str[i], char_type);
     const equal_exprt lemma(res[idx], c);
-    axioms.push_back(implies_exprt(guard, lemma));
+    lemmas.push_back(implies_exprt(guard, lemma));
   }
 
   const exprt s_length = from_integer(str.size(), index_type);
 
-  axioms.push_back(implies_exprt(guard, equal_exprt(res.length(), s_length)));
+  lemmas.push_back(implies_exprt(guard, equal_exprt(res.length(), s_length)));
   return from_integer(0, get_return_code_type());
 }
 
@@ -63,7 +63,7 @@ exprt string_constraint_generatort::add_axioms_for_empty_string(
 {
   PRECONDITION(f.arguments().size() == 2);
   exprt length = f.arguments()[0];
-  axioms.push_back(equal_exprt(length, from_integer(0, length.type())));
+  lemmas.push_back(equal_exprt(length, from_integer(0, length.type())));
   return from_integer(0, get_return_code_type());
 }
 

src/solvers/refinement/string_constraint_generator_float.cpp

@@ -251,7 +251,7 @@ exprt string_constraint_generatort::add_axioms_for_fractional_part(
 
   and_exprt a1(res.axiom_for_length_gt(1),
                res.axiom_for_length_le(max));
-  axioms.push_back(a1);
+  lemmas.push_back(a1);
 
   equal_exprt starts_with_dot(res[0], from_integer('.', char_type));
 
@@ -289,10 +289,10 @@ exprt string_constraint_generatort::add_axioms_for_fractional_part(
   }
 
   exprt a2=conjunction(digit_constraints);
-  axioms.push_back(a2);
+  lemmas.push_back(a2);
 
   equal_exprt a3(int_expr, sum);
-  axioms.push_back(a3);
+  lemmas.push_back(a3);
 
   return from_integer(0, signedbv_typet(32));
 }