From 1843e441f41737c813f6c24972aa58e90e47d8b4 Mon Sep 17 00:00:00 2001 From: "Lukasz A.J. Wrona" Date: Fri, 15 Sep 2017 11:31:15 +0100 Subject: [PATCH 1/3] 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. --- .../refinement/string_constraint_generator.h | 9 ++- ...tring_constraint_generator_code_points.cpp | 26 ++++---- ...string_constraint_generator_comparison.cpp | 26 ++++---- .../string_constraint_generator_concat.cpp | 14 ++--- .../string_constraint_generator_constants.cpp | 6 +- .../string_constraint_generator_float.cpp | 6 +- .../string_constraint_generator_indexof.cpp | 44 ++++++------- .../string_constraint_generator_main.cpp | 28 ++++++--- .../string_constraint_generator_testing.cpp | 26 ++++---- ...ng_constraint_generator_transformation.cpp | 55 +++++++++-------- .../string_constraint_generator_valueof.cpp | 43 +++++++------ src/solvers/refinement/string_refinement.cpp | 61 +++++++++++-------- 12 files changed, 187 insertions(+), 157 deletions(-) diff --git a/src/solvers/refinement/string_constraint_generator.h b/src/solvers/refinement/string_constraint_generator.h index d2c76eb6faa..74d341a24c9 100644 --- a/src/solvers/refinement/string_constraint_generator.h +++ b/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 &get_axioms() const; + const std::vector &get_lemmas() const; + const std::vector &get_constraints() const; + const std::vector & + get_not_contains_constraints() const; /// Boolean symbols for the results of some string functions const std::vector &get_boolean_symbols() const; @@ -349,7 +352,9 @@ class string_constraint_generatort final unsigned symbol_count=0; const messaget message; - std::vector axioms; + std::vector lemmas; + std::vector constraints; + std::vector not_contains_constraints; std::vector boolean_symbols; std::vector index_symbols; const namespacet ns; diff --git a/src/solvers/refinement/string_constraint_generator_code_points.cpp b/src/solvers/refinement/string_constraint_generator_code_points.cpp index a2e67a3ea82..1f61a769208 100644 --- a/src/solvers/refinement/string_constraint_generator_code_points.cpp +++ b/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; } diff --git a/src/solvers/refinement/string_constraint_generator_comparison.cpp b/src/solvers/refinement/string_constraint_generator_comparison.cpp index e59e8ef4ba7..7b8590e7836 100644 --- a/src/solvers/refinement/string_constraint_generator_comparison.cpp +++ b/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( diff --git a/src/solvers/refinement/string_constraint_generator_concat.cpp b/src/solvers/refinement/string_constraint_generator_concat.cpp index 1c002590ef2..fa38ac46bc1 100644 --- a/src/solvers/refinement/string_constraint_generator_concat.cpp +++ b/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()); diff --git a/src/solvers/refinement/string_constraint_generator_constants.cpp b/src/solvers/refinement/string_constraint_generator_constants.cpp index fad3a2d9e3d..0ed64b37a95 100644 --- a/src/solvers/refinement/string_constraint_generator_constants.cpp +++ b/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()); } diff --git a/src/solvers/refinement/string_constraint_generator_float.cpp b/src/solvers/refinement/string_constraint_generator_float.cpp index cd1518b5dd9..7e084f872f8 100644 --- a/src/solvers/refinement/string_constraint_generator_float.cpp +++ b/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)); } diff --git a/src/solvers/refinement/string_constraint_generator_indexof.cpp b/src/solvers/refinement/string_constraint_generator_indexof.cpp index 295c18df903..77086d849f3 100644 --- a/src/solvers/refinement/string_constraint_generator_indexof.cpp +++ b/src/solvers/refinement/string_constraint_generator_indexof.cpp @@ -47,17 +47,17 @@ exprt string_constraint_generatort::add_axioms_for_index_of( and_exprt a1( binary_relation_exprt(index, ID_ge, minus1), binary_relation_exprt(index, ID_lt, str.length())); - axioms.push_back(a1); + lemmas.push_back(a1); equal_exprt a2(not_exprt(contains), equal_exprt(index, minus1)); - axioms.push_back(a2); + lemmas.push_back(a2); implies_exprt a3( contains, and_exprt( binary_relation_exprt(from_index, ID_le, index), equal_exprt(str[index], c))); - axioms.push_back(a3); + lemmas.push_back(a3); const auto zero = from_integer(0, index_type); const if_exprt lower_bound( @@ -66,7 +66,7 @@ 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))); - axioms.push_back(a4); + constraints.push_back(a4); symbol_exprt m=fresh_univ_index("QA_index_of", index_type); string_constraintt a5( @@ -75,7 +75,7 @@ exprt string_constraint_generatort::add_axioms_for_index_of( str.length(), not_exprt(contains), not_exprt(equal_exprt(str[m], c))); - axioms.push_back(a5); + constraints.push_back(a5); return index; } @@ -119,12 +119,12 @@ exprt string_constraint_generatort::add_axioms_for_index_of_string( binary_relation_exprt(from_index, ID_le, offset), binary_relation_exprt( offset, ID_le, minus_exprt(haystack.length(), needle.length())))); - axioms.push_back(a1); + lemmas.push_back(a1); equal_exprt a2( not_exprt(contains), equal_exprt(offset, from_integer(-1, index_type))); - axioms.push_back(a2); + lemmas.push_back(a2); symbol_exprt qvar=fresh_univ_index("QA_index_of_string", index_type); string_constraintt a3( @@ -132,7 +132,7 @@ exprt string_constraint_generatort::add_axioms_for_index_of_string( needle.length(), contains, equal_exprt(haystack[plus_exprt(qvar, offset)], needle[qvar])); - axioms.push_back(a3); + constraints.push_back(a3); // string_not contains_constraintt are formulas of the form: // forall x in [lb,ub[. p(x) => exists y in [lb,ub[. s1[x+y] != s2[y] @@ -144,7 +144,7 @@ exprt string_constraint_generatort::add_axioms_for_index_of_string( needle.length(), haystack, needle); - axioms.push_back(a4); + not_contains_constraints.push_back(a4); string_not_contains_constraintt a5( from_index, @@ -156,12 +156,12 @@ exprt string_constraint_generatort::add_axioms_for_index_of_string( needle.length(), haystack, needle); - axioms.push_back(a5); + not_contains_constraints.push_back(a5); const implies_exprt a6( equal_exprt(needle.length(), from_integer(0, index_type)), equal_exprt(offset, from_index)); - axioms.push_back(a6); + lemmas.push_back(a6); return offset; } @@ -212,17 +212,17 @@ exprt string_constraint_generatort::add_axioms_for_last_index_of_string( binary_relation_exprt( offset, ID_le, minus_exprt(haystack.length(), needle.length())), binary_relation_exprt(offset, ID_le, from_index))); - axioms.push_back(a1); + lemmas.push_back(a1); equal_exprt a2( not_exprt(contains), equal_exprt(offset, from_integer(-1, index_type))); - axioms.push_back(a2); + lemmas.push_back(a2); 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); - axioms.push_back(a3); + constraints.push_back(a3); // end_index is min(from_index, |str| - |substring|) minus_exprt length_diff(haystack.length(), needle.length()); @@ -239,7 +239,7 @@ exprt string_constraint_generatort::add_axioms_for_last_index_of_string( needle.length(), haystack, needle); - axioms.push_back(a4); + not_contains_constraints.push_back(a4); string_not_contains_constraintt a5( from_integer(0, index_type), @@ -249,12 +249,12 @@ exprt string_constraint_generatort::add_axioms_for_last_index_of_string( needle.length(), haystack, needle); - axioms.push_back(a5); + not_contains_constraints.push_back(a5); const implies_exprt a6( equal_exprt(needle.length(), from_integer(0, index_type)), equal_exprt(offset, from_index)); - axioms.push_back(a6); + lemmas.push_back(a6); return offset; } @@ -343,13 +343,13 @@ exprt string_constraint_generatort::add_axioms_for_last_index_of( binary_relation_exprt(index, ID_ge, minus1), binary_relation_exprt(index, ID_le, from_index), binary_relation_exprt(index, ID_lt, str.length())); - axioms.push_back(a1); + lemmas.push_back(a1); const notequal_exprt a2(contains, equal_exprt(index, minus1)); - axioms.push_back(a2); + lemmas.push_back(a2); const implies_exprt a3(contains, equal_exprt(str[index], c)); - axioms.push_back(a3); + lemmas.push_back(a3); const exprt index1 = from_integer(1, index_type); const exprt from_index_plus_one = @@ -366,12 +366,12 @@ exprt string_constraint_generatort::add_axioms_for_last_index_of( end_index, contains, notequal_exprt(str[n], c)); - axioms.push_back(a4); + 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)); - axioms.push_back(a5); + constraints.push_back(a5); return index; } diff --git a/src/solvers/refinement/string_constraint_generator_main.cpp b/src/solvers/refinement/string_constraint_generator_main.cpp index c73e450fdbd..77d6d600a68 100644 --- a/src/solvers/refinement/string_constraint_generator_main.cpp +++ b/src/solvers/refinement/string_constraint_generator_main.cpp @@ -35,9 +35,21 @@ string_constraint_generatort::string_constraint_generatort( { } -const std::vector &string_constraint_generatort::get_axioms() const +const std::vector &string_constraint_generatort::get_lemmas() const { - return axioms; + return lemmas; +} + +const std::vector & +string_constraint_generatort::get_constraints() const +{ + return constraints; +} + +const std::vector & +string_constraint_generatort::get_not_contains_constraints() const +{ + return not_contains_constraints; } const std::vector & @@ -136,7 +148,7 @@ plus_exprt string_constraint_generatort::plus_exprt_with_overflow_check( implies_exprt no_overflow(equal_exprt(neg1, neg2), equal_exprt(neg1, neg_sum)); - axioms.push_back(no_overflow); + lemmas.push_back(no_overflow); return sum; } @@ -291,7 +303,7 @@ exprt string_constraint_generatort::associate_length_to_array( const exprt &new_length = f.arguments()[1]; const auto &length = get_length_of_string_array(array_expr); - axioms.push_back(equal_exprt(length, new_length)); + lemmas.push_back(equal_exprt(length, new_length)); return from_integer(0, f.type()); } @@ -322,10 +334,10 @@ void string_constraint_generatort::add_default_axioms( return; const exprt index_zero = from_integer(0, s.length().type()); - axioms.push_back(s.axiom_for_length_ge(index_zero)); + lemmas.push_back(s.axiom_for_length_ge(index_zero)); if(max_string_length!=std::numeric_limits::max()) - axioms.push_back(s.axiom_for_length_le(max_string_length)); + lemmas.push_back(s.axiom_for_length_le(max_string_length)); } /// Add constraint on characters of a string. @@ -359,7 +371,7 @@ void string_constraint_generatort::add_constraint_on_characters( 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); - axioms.push_back(sc); + constraints.push_back(sc); } /// Add axioms to ensure all characters of a string belong to a given set. @@ -620,6 +632,6 @@ exprt string_constraint_generatort::add_axioms_for_char_at( PRECONDITION(f.arguments().size() == 2); array_string_exprt str = get_string_expr(f.arguments()[0]); symbol_exprt char_sym = fresh_symbol("char", str.type().subtype()); - axioms.push_back(equal_exprt(char_sym, str[f.arguments()[1]])); + lemmas.push_back(equal_exprt(char_sym, str[f.arguments()[1]])); return char_sym; } diff --git a/src/solvers/refinement/string_constraint_generator_testing.cpp b/src/solvers/refinement/string_constraint_generator_testing.cpp index 3186451e32e..6a2c7d0d8a3 100644 --- a/src/solvers/refinement/string_constraint_generator_testing.cpp +++ b/src/solvers/refinement/string_constraint_generator_testing.cpp @@ -40,7 +40,7 @@ exprt string_constraint_generatort::add_axioms_for_is_prefix( isprefix, str.axiom_for_length_ge(plus_exprt_with_overflow_check( prefix.length(), offset))); - axioms.push_back(a1); + lemmas.push_back(a1); symbol_exprt qvar=fresh_univ_index("QA_isprefix", index_type); string_constraintt a2( @@ -48,7 +48,7 @@ exprt string_constraint_generatort::add_axioms_for_is_prefix( prefix.length(), isprefix, equal_exprt(str[plus_exprt(qvar, offset)], prefix[qvar])); - axioms.push_back(a2); + constraints.push_back(a2); symbol_exprt witness=fresh_exist_index("witness_not_isprefix", index_type); and_exprt witness_diff( @@ -61,7 +61,7 @@ exprt string_constraint_generatort::add_axioms_for_is_prefix( witness_diff); implies_exprt a3(not_exprt(isprefix), s0_notpref_s1); - axioms.push_back(a3); + lemmas.push_back(a3); return isprefix; } @@ -109,8 +109,8 @@ exprt string_constraint_generatort::add_axioms_for_is_empty( symbol_exprt is_empty=fresh_boolean("is_empty"); array_string_exprt s0 = get_string_expr(f.arguments()[0]); - axioms.push_back(implies_exprt(is_empty, s0.axiom_for_has_length(0))); - axioms.push_back(implies_exprt(s0.axiom_for_has_length(0), is_empty)); + lemmas.push_back(implies_exprt(is_empty, s0.axiom_for_has_length(0))); + lemmas.push_back(implies_exprt(s0.axiom_for_has_length(0), is_empty)); return typecast_exprt(is_empty, f.type()); } @@ -148,14 +148,14 @@ exprt string_constraint_generatort::add_axioms_for_is_suffix( const typet &index_type=s0.length().type(); implies_exprt a1(issuffix, s1.axiom_for_length_ge(s0.length())); - axioms.push_back(a1); + lemmas.push_back(a1); symbol_exprt qvar=fresh_univ_index("QA_suffix", index_type); exprt qvar_shifted=plus_exprt( qvar, minus_exprt(s1.length(), s0.length())); string_constraintt a2( qvar, s0.length(), issuffix, equal_exprt(s0[qvar], s1[qvar_shifted])); - axioms.push_back(a2); + constraints.push_back(a2); symbol_exprt witness=fresh_exist_index("witness_not_suffix", index_type); exprt shifted=plus_exprt( @@ -171,7 +171,7 @@ exprt string_constraint_generatort::add_axioms_for_is_suffix( axiom_for_is_positive_index(witness)))); implies_exprt a3(not_exprt(issuffix), constr3); - axioms.push_back(a3); + lemmas.push_back(a3); return tc_issuffix; } @@ -206,25 +206,25 @@ exprt string_constraint_generatort::add_axioms_for_contains( fresh_exist_index("startpos_contains", index_type); const implies_exprt a1(contains, s0.axiom_for_length_ge(s1.length())); - axioms.push_back(a1); + lemmas.push_back(a1); minus_exprt length_diff(s0.length(), s1.length()); and_exprt bounds( axiom_for_is_positive_index(startpos), binary_relation_exprt(startpos, ID_le, length_diff)); implies_exprt a2(contains, bounds); - axioms.push_back(a2); + lemmas.push_back(a2); implies_exprt a3( not_exprt(contains), equal_exprt(startpos, from_integer(-1, index_type))); - axioms.push_back(a3); + lemmas.push_back(a3); symbol_exprt qvar=fresh_univ_index("QA_contains", index_type); exprt qvar_shifted=plus_exprt(qvar, startpos); string_constraintt a4( qvar, s1.length(), contains, equal_exprt(s1[qvar], s0[qvar_shifted])); - axioms.push_back(a4); + constraints.push_back(a4); string_not_contains_constraintt a5( from_integer(0, index_type), @@ -234,7 +234,7 @@ exprt string_constraint_generatort::add_axioms_for_contains( s1.length(), s0, s1); - axioms.push_back(a5); + not_contains_constraints.push_back(a5); return typecast_exprt(contains, f.type()); } diff --git a/src/solvers/refinement/string_constraint_generator_transformation.cpp b/src/solvers/refinement/string_constraint_generator_transformation.cpp index c865699b4dd..e589ff5c65d 100644 --- a/src/solvers/refinement/string_constraint_generator_transformation.cpp +++ b/src/solvers/refinement/string_constraint_generator_transformation.cpp @@ -48,7 +48,7 @@ exprt string_constraint_generatort::add_axioms_for_set_length( // a2 : forall i<|res|. i < |s1| ==> res[i] = s1[i] // a3 : forall i<|res|. i >= |s1| ==> res[i] = 0 - axioms.push_back(res.axiom_for_has_length(k)); + lemmas.push_back(res.axiom_for_has_length(k)); symbol_exprt idx = fresh_univ_index("QA_index_set_length", index_type); string_constraintt a2( @@ -56,7 +56,7 @@ exprt string_constraint_generatort::add_axioms_for_set_length( res.length(), s1.axiom_for_length_gt(idx), equal_exprt(s1[idx], res[idx])); - axioms.push_back(a2); + constraints.push_back(a2); symbol_exprt idx2 = fresh_univ_index("QA_index_set_length2", index_type); string_constraintt a3( @@ -64,7 +64,7 @@ exprt string_constraint_generatort::add_axioms_for_set_length( res.length(), s1.axiom_for_length_le(idx2), equal_exprt(res[idx2], constant_char(0, char_type))); - axioms.push_back(a3); + constraints.push_back(a3); return from_integer(0, signedbv_typet(32)); } @@ -131,21 +131,21 @@ exprt string_constraint_generatort::add_axioms_for_substring( implies_exprt a1( binary_relation_exprt(start, ID_lt, end), res.axiom_for_has_length(minus_exprt(end, start))); - axioms.push_back(a1); + lemmas.push_back(a1); exprt is_empty=res.axiom_for_has_length(from_integer(0, index_type)); implies_exprt a2(binary_relation_exprt(start, ID_ge, end), is_empty); - axioms.push_back(a2); + lemmas.push_back(a2); // Warning: check what to do if the string is not long enough - axioms.push_back(str.axiom_for_length_ge(end)); + lemmas.push_back(str.axiom_for_length_ge(end)); symbol_exprt idx=fresh_univ_index("QA_index_substring", index_type); string_constraintt a4(idx, res.length(), equal_exprt(res[idx], str[plus_exprt(start, idx)])); - axioms.push_back(a4); + constraints.push_back(a4); return from_integer(0, signedbv_typet(32)); } @@ -189,25 +189,25 @@ exprt string_constraint_generatort::add_axioms_for_trim( exprt a1=str.axiom_for_length_ge( plus_exprt_with_overflow_check(idx, res.length())); - axioms.push_back(a1); + lemmas.push_back(a1); binary_relation_exprt a2(idx, ID_ge, from_integer(0, index_type)); - axioms.push_back(a2); + lemmas.push_back(a2); exprt a3=str.axiom_for_length_ge(idx); - axioms.push_back(a3); + lemmas.push_back(a3); exprt a4=res.axiom_for_length_ge( from_integer(0, index_type)); - axioms.push_back(a4); + lemmas.push_back(a4); exprt a5 = res.axiom_for_length_le(str.length()); - axioms.push_back(a5); + lemmas.push_back(a5); symbol_exprt n=fresh_univ_index("QA_index_trim", index_type); binary_relation_exprt non_print(str[n], ID_le, space_char); string_constraintt a6(n, idx, non_print); - axioms.push_back(a6); + constraints.push_back(a6); symbol_exprt n2=fresh_univ_index("QA_index_trim2", index_type); minus_exprt bound(str.length(), plus_exprt_with_overflow_check(idx, @@ -218,12 +218,12 @@ exprt string_constraint_generatort::add_axioms_for_trim( space_char); string_constraintt a7(n2, bound, eqn2); - axioms.push_back(a7); + constraints.push_back(a7); symbol_exprt n3=fresh_univ_index("QA_index_trim3", index_type); equal_exprt eqn3(res[n3], str[plus_exprt(n3, idx)]); string_constraintt a8(n3, res.length(), eqn3); - axioms.push_back(a8); + constraints.push_back(a8); minus_exprt index_before( plus_exprt_with_overflow_check(idx, res.length()), @@ -234,7 +234,7 @@ exprt string_constraint_generatort::add_axioms_for_trim( and_exprt( binary_relation_exprt(str[idx], ID_gt, space_char), no_space_before)); - axioms.push_back(a9); + lemmas.push_back(a9); return from_integer(0, f.type()); } @@ -273,7 +273,7 @@ exprt string_constraint_generatort::add_axioms_for_to_lower_case( // information from the UnicodeData file. equal_exprt a1(res.length(), str.length()); - axioms.push_back(a1); + lemmas.push_back(a1); symbol_exprt idx=fresh_univ_index("QA_lower_case", index_type); exprt::operandst upper_case; @@ -306,7 +306,7 @@ exprt string_constraint_generatort::add_axioms_for_to_lower_case( if_exprt conditional_convert(is_upper_case, converted, non_converted); string_constraintt a2(idx, res.length(), conditional_convert); - axioms.push_back(a2); + constraints.push_back(a2); return from_integer(0, f.type()); } @@ -343,7 +343,7 @@ exprt string_constraint_generatort::add_axioms_for_to_upper_case( // from the UnicodeData file. equal_exprt a1(res.length(), str.length()); - axioms.push_back(a1); + lemmas.push_back(a1); symbol_exprt idx1=fresh_univ_index("QA_upper_case1", index_type); exprt is_lower_case=and_exprt( @@ -353,7 +353,7 @@ exprt string_constraint_generatort::add_axioms_for_to_upper_case( equal_exprt convert(res[idx1], plus_exprt(str[idx1], diff)); implies_exprt body1(is_lower_case, convert); string_constraintt a2(idx1, res.length(), body1); - axioms.push_back(a2); + constraints.push_back(a2); symbol_exprt idx2=fresh_univ_index("QA_upper_case2", index_type); exprt is_not_lower_case=not_exprt(and_exprt( @@ -362,7 +362,7 @@ exprt string_constraint_generatort::add_axioms_for_to_upper_case( equal_exprt eq(res[idx2], str[idx2]); implies_exprt body2(is_not_lower_case, eq); string_constraintt a3(idx2, res.length(), body2); - axioms.push_back(a3); + constraints.push_back(a3); return from_integer(0, signedbv_typet(32)); } @@ -412,13 +412,14 @@ 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()); - axioms.push_back(equal_exprt(res.length(), str.length())); - axioms.push_back(equal_exprt(res[position], character)); + lemmas.push_back(equal_exprt(res.length(), str.length())); + lemmas.push_back(equal_exprt(res[position], character)); 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); - axioms.push_back(string_constraintt( - q, from_integer(0, q.type()), res.length(), a3_guard, a3_body)); + constraints.push_back( + string_constraintt( + q, from_integer(0, q.type()), res.length(), a3_guard, a3_body)); return if_exprt( out_of_bounds, from_integer(1, f.type()), from_integer(0, f.type())); } @@ -484,7 +485,7 @@ exprt string_constraint_generatort::add_axioms_for_replace( const auto old_char=maybe_chars->first; const auto new_char=maybe_chars->second; - axioms.push_back(equal_exprt(res.length(), str.length())); + lemmas.push_back(equal_exprt(res.length(), str.length())); symbol_exprt qvar = fresh_univ_index("QA_replace", str.length().type()); implies_exprt case1( @@ -494,7 +495,7 @@ exprt string_constraint_generatort::add_axioms_for_replace( not_exprt(equal_exprt(str[qvar], old_char)), equal_exprt(res[qvar], str[qvar])); string_constraintt a2(qvar, res.length(), and_exprt(case1, case2)); - axioms.push_back(a2); + constraints.push_back(a2); return from_integer(0, f.type()); } return from_integer(1, f.type()); diff --git a/src/solvers/refinement/string_constraint_generator_valueof.cpp b/src/solvers/refinement/string_constraint_generator_valueof.cpp index 45c8799fca1..920f0de801a 100644 --- a/src/solvers/refinement/string_constraint_generator_valueof.cpp +++ b/src/solvers/refinement/string_constraint_generator_valueof.cpp @@ -89,24 +89,24 @@ exprt string_constraint_generatort::add_axioms_from_bool( std::string str_true="true"; implies_exprt a1(eq, res.axiom_for_has_length(str_true.length())); - axioms.push_back(a1); + lemmas.push_back(a1); for(std::size_t i=0; i1) - axioms.push_back( + lemmas.push_back( implies_exprt(premise, not_exprt(equal_exprt(res[0], zero_char)))); } return from_integer(0, get_return_code_type()); @@ -296,7 +295,7 @@ exprt string_constraint_generatort::add_axioms_from_char( const exprt &c) { and_exprt lemma(equal_exprt(res[0], c), res.axiom_for_has_length(1)); - axioms.push_back(lemma); + lemmas.push_back(lemma); return from_integer(0, get_return_code_type()); } @@ -330,30 +329,30 @@ void string_constraint_generatort::add_axioms_for_correct_number_format( // |str| > 0 const exprt non_empty=str.axiom_for_length_ge(from_integer(1, index_type)); - axioms.push_back(non_empty); + lemmas.push_back(non_empty); if(strict_formatting) { // str[0] = '-' || is_digit_with_radix(str[0], radix) const or_exprt correct_first(starts_with_minus, starts_with_digit); - axioms.push_back(correct_first); + lemmas.push_back(correct_first); } else { // str[0] = '-' || str[0] = '+' || is_digit_with_radix(str[0], radix) const or_exprt correct_first( starts_with_minus, starts_with_digit, starts_with_plus); - axioms.push_back(correct_first); + lemmas.push_back(correct_first); } // str[0]='+' or '-' ==> |str| > 1 const implies_exprt contains_digit( or_exprt(starts_with_minus, starts_with_plus), str.axiom_for_length_ge(from_integer(2, index_type))); - axioms.push_back(contains_digit); + lemmas.push_back(contains_digit); // |str| <= max_size - axioms.push_back(str.axiom_for_length_le(max_size)); + lemmas.push_back(str.axiom_for_length_le(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 @@ -365,7 +364,7 @@ void string_constraint_generatort::add_axioms_for_correct_number_format( str.axiom_for_length_ge(from_integer(index+1, index_type)), is_digit_with_radix( str[index], strict_formatting, radix_as_char, radix_ul)); - axioms.push_back(character_at_index_is_digit); + lemmas.push_back(character_at_index_is_digit); } if(strict_formatting) @@ -376,12 +375,12 @@ void string_constraint_generatort::add_axioms_for_correct_number_format( const implies_exprt no_leading_zero( equal_exprt(chr, zero_char), str.axiom_for_has_length(from_integer(1, index_type))); - axioms.push_back(no_leading_zero); + lemmas.push_back(no_leading_zero); // no_leading_zero_after_minus : str[0]='-' => str[1]!='0' implies_exprt no_leading_zero_after_minus( starts_with_minus, not_exprt(equal_exprt(str[1], zero_char))); - axioms.push_back(no_leading_zero_after_minus); + lemmas.push_back(no_leading_zero_after_minus); } } @@ -418,7 +417,7 @@ void string_constraint_generatort::add_axioms_for_characters_in_integer_string( /// Deal with size==1 case separately. There are axioms from /// 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 "-". - axioms.push_back( + lemmas.push_back( implies_exprt(str.axiom_for_has_length(1), equal_exprt(input_int, sum))); for(size_t size=2; size<=max_string_length; size++) @@ -462,18 +461,18 @@ void string_constraint_generatort::add_axioms_for_characters_in_integer_string( if(!digit_constraints.empty()) { const implies_exprt a5(premise, conjunction(digit_constraints)); - axioms.push_back(a5); + lemmas.push_back(a5); } const implies_exprt a6( and_exprt(premise, not_exprt(starts_with_minus)), equal_exprt(input_int, sum)); - axioms.push_back(a6); + lemmas.push_back(a6); const implies_exprt a7( and_exprt(premise, starts_with_minus), equal_exprt(input_int, unary_minus_exprt(sum))); - axioms.push_back(a7); + lemmas.push_back(a7); } } diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp index 3e3ed3a9479..712e80acad9 100644 --- a/src/solvers/refinement/string_refinement.cpp +++ b/src/solvers/refinement/string_refinement.cpp @@ -811,37 +811,50 @@ decision_proceduret::resultt string_refinementt::dec_solve() supert::set_to(eq, true); } - const auto get = [this](const exprt &expr) { return this->get(expr); }; - for(exprt axiom : generator.get_axioms()) - { - symbol_resolve.replace_expr(axiom); - if(axiom.id()==ID_string_constraint) - { - string_constraintt univ_axiom = to_string_constraint(axiom); + const auto constraints = generator.get_constraints(); + std::transform( + constraints.begin(), + constraints.end(), + std::back_inserter(axioms.universal), + [&](string_constraintt constraint) { // NOLINT + symbol_resolve.replace_expr(constraint); DATA_INVARIANT( - is_valid_string_constraint(error(), ns, univ_axiom), + is_valid_string_constraint(error(), ns, constraint), string_refinement_invariantt( "string constraints satisfy their invariant")); - axioms.universal.push_back(univ_axiom); - } - else if(axiom.id()==ID_string_not_contains_constraint) - { - string_not_contains_constraintt nc_axiom= - to_string_not_contains_constraint(axiom); - array_typet rtype = to_array_type(nc_axiom.s0().type()); + return constraint; + }); + + const auto not_contains_constraints = + generator.get_not_contains_constraints(); + std::transform( + not_contains_constraints.begin(), + not_contains_constraints.end(), + std::back_inserter(axioms.not_contains), + [&](string_not_contains_constraintt axiom) { // NOLINT + symbol_resolve.replace_expr(axiom); + return axiom; + }); + + for(const auto &nc_axiom : axioms.not_contains) + { + const auto &witness_type = [&] { // NOLINT + const auto &rtype = to_array_type(nc_axiom.s0().type()); const typet &index_type = rtype.size().type(); - array_typet witness_type(index_type, infinity_exprt(index_type)); - generator.witness[nc_axiom]= - generator.fresh_symbol("not_contains_witness", witness_type); - axioms.not_contains.push_back(nc_axiom); - } - else - { - add_lemma(axiom); - } + return array_typet(index_type, infinity_exprt(index_type)); + }(); + generator.witness[nc_axiom] = + generator.fresh_symbol("not_contains_witness", witness_type); + } + + for(exprt lemma : generator.get_lemmas()) + { + symbol_resolve.replace_expr(lemma); + add_lemma(lemma); } // Initial try without index set + const auto get = [this](const exprt &expr) { return this->get(expr); }; const decision_proceduret::resultt res=supert::dec_solve(); if(res==resultt::D_SATISFIABLE) { From 51d86f579ee25af2fa3a222475618aa275941ace Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Fri, 12 Jan 2018 09:05:58 +0000 Subject: [PATCH 2/3] Adapt unit tests for splitted axiom vectors --- .../instantiate_not_contains.cpp | 60 +++++++++++-------- 1 file changed, 36 insertions(+), 24 deletions(-) diff --git a/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp b/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp index fe4d6d6bbe0..a5aa7eb4028 100644 --- a/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp +++ b/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp @@ -8,12 +8,12 @@ #include -#include - -#include +#include +#include #include #include -#include +#include +#include #include #include @@ -193,28 +193,40 @@ SCENARIO("instantiate_not_contains", exprt res=generator.add_axioms_for_function_application(func); std::string axioms; std::vector nc_axioms; - for(exprt axiom : generator.get_axioms()) - { - simplify(axiom, ns); - if(axiom.id()==ID_string_constraint) - { - string_constraintt sc=to_string_constraint(axiom); - axioms+=from_expr(ns, "", sc); - } - else if(axiom.id()==ID_string_not_contains_constraint) - { - string_not_contains_constraintt sc= - to_string_not_contains_constraint(axiom); - axioms+=from_expr(ns, "", sc); - generator.witness[sc]= - generator.fresh_symbol("w", t.witness_type()); + + const auto constraints = generator.get_constraints(); + std::accumulate( + constraints.begin(), + constraints.end(), + axioms, + [&](const std::string &accu, string_constraintt sc) { // NOLINT + simplify(sc, ns); + return accu + from_expr(ns, "", sc) + "\n\n"; + }); + + const auto nc_contraints = generator.get_not_contains_constraints(); + axioms = std::accumulate( + nc_contraints.begin(), + nc_contraints.end(), + axioms, + [&]( + const std::string &accu, string_not_contains_constraintt sc) { // NOLINT + simplify(sc, ns); + generator.witness[sc] = generator.fresh_symbol("w", t.witness_type()); nc_axioms.push_back(sc); - } - else - axioms+=from_expr(ns, "", axiom); + return accu + from_expr(ns, "", sc) + "\n\n"; + }); + + const auto lemmas = generator.get_lemmas(); + axioms = std::accumulate( + lemmas.begin(), + lemmas.end(), + axioms, + [&](const std::string &accu, exprt axiom) { // NOLINT + simplify(axiom, ns); + return accu + from_expr(ns, "", axiom) + "\n\n"; + }); - axioms+="\n\n"; - } INFO("Original axioms:\n"); INFO(axioms); From 857fcf94b5a7630f01b41243a506435592aea67d Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Fri, 12 Jan 2018 09:41:00 +0000 Subject: [PATCH 3/3] Cleanup unused fields in string refinement --- src/solvers/refinement/string_refinement.h | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) diff --git a/src/solvers/refinement/string_refinement.h b/src/solvers/refinement/string_refinement.h index cab3aff3328..17149166e2a 100644 --- a/src/solvers/refinement/string_refinement.h +++ b/src/solvers/refinement/string_refinement.h @@ -94,12 +94,8 @@ class string_refinementt final: public bv_refinementt union_find_replacet symbol_resolve; std::vector equations; - std::list> non_string_axioms; - // Map pointers to array symbols - std::map pointer_map; - - void add_lemma(const exprt &lemma, const bool _simplify = true); + void add_lemma(const exprt &lemma, bool simplify_lemma = true); }; exprt substitute_array_lists(exprt expr, std::size_t string_max_length);