Split string generator axioms into separate vectors

These axioms used to be all added in the same exprt vector by the constraint
generator and then filtered by the solver according to their type.
We now make the constraint generator add to appropriate vector
according to the type of axiom (simple lemma, string constraint or "not
contains" constraint).
This has mainly two advantages:

  * there is no need for filtering the vector in the solver since they
    are already prefiltered
  * string_constraintt and string_not_contains_constraintt no longer
    need to inherit from exprt since they are not stored in the same
    vector.

Author: Lukasz A.J. Wrona

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