From 15131da522e1d9544df23b7d9915e70523e7eb39 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Wed, 31 Oct 2018 16:01:37 +0000 Subject: [PATCH 1/2] Make string_not_contains_constraintt a struct In particular it does not inherit from exprt anymore. Not inheriting from exprt, allows the class to be more structured. We have fields that have names describing what they contain, instead of having to define accessor methods. This also prevent us from mistakenly passing a constraint to an exprt function, which wouldn't know how to deal with a string_not_contains_constraintt. --- .../instantiate_not_contains.cpp | 115 +++++++---------- src/solvers/refinement/string_constraint.cpp | 40 ++++++ src/solvers/refinement/string_constraint.h | 122 ++++++------------ .../string_constraint_generator_indexof.cpp | 27 ++-- .../string_constraint_generator_testing.cpp | 4 +- .../string_constraint_instantiation.cpp | 17 +-- .../string_constraint_instantiation.h | 3 +- src/solvers/refinement/string_refinement.cpp | 48 +++---- 8 files changed, 178 insertions(+), 198 deletions(-) diff --git a/jbmc/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp b/jbmc/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp index 094d6850c93..9cc6ecef058 100644 --- a/jbmc/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp +++ b/jbmc/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp @@ -202,7 +202,7 @@ SCENARIO("instantiate_not_contains", std::string axioms; std::vector nc_axioms; - std::map witnesses; + std::unordered_map witnesses; std::accumulate( constraints.universal.begin(), @@ -218,12 +218,12 @@ SCENARIO("instantiate_not_contains", constraints.not_contains.end(), axioms, [&](const std::string &accu, string_not_contains_constraintt sc) { - simplify(sc, ns); + simplify(sc.premise, ns); + simplify(sc.s0, ns); + simplify(sc.s1, ns); witnesses[sc] = generator.fresh_symbol("w", t.witness_type()); nc_axioms.push_back(sc); - std::string s; - java_lang->from_expr(sc, s, ns); - return accu + s + "\n\n"; + return accu + to_string(sc) + "\n\n"; }); axioms = std::accumulate( @@ -282,26 +282,23 @@ SCENARIO("instantiate_not_contains", // { .=1, .={ (char)'a' } }[x+y] != { .=1, .={ (char)'b' } }[y] // ) // which is vacuously true. - string_not_contains_constraintt vacuous( - from_integer(0), - from_integer(0), - true_exprt(), - from_integer(0), - from_integer(1), - a_array, - a_array); + const string_not_contains_constraintt vacuous = {from_integer(0), + from_integer(0), + true_exprt(), + from_integer(0), + from_integer(1), + a_array, + a_array}; // Create witness for axiom symbol_tablet symtab; const namespacet empty_ns(symtab); string_constraint_generatort generator(ns); - std::map witnesses; + std::unordered_map witnesses; witnesses[vacuous] = generator.fresh_symbol("w", t.witness_type()); INFO("Original axiom:\n"); - std::string s; - java_lang->from_expr(vacuous, s, ns); - INFO(s + "\n\n"); + INFO(to_string(vacuous) + "\n\n"); WHEN("we instantiate and simplify") { @@ -337,26 +334,23 @@ SCENARIO("instantiate_not_contains", // { .=1, .={ (char)'a' } }[x+y] != { .=1, .={ (char)'b' } }[y] // ) // which is false. - string_not_contains_constraintt trivial( - from_integer(0), - from_integer(1), - true_exprt(), - from_integer(0), - from_integer(0), - a_array, - b_array); + const string_not_contains_constraintt trivial = {from_integer(0), + from_integer(1), + true_exprt(), + from_integer(0), + from_integer(0), + a_array, + b_array}; // Create witness for axiom symbol_tablet symtab; const namespacet ns(symtab); string_constraint_generatort generator(ns); - std::map witnesses; + std::unordered_map witnesses; witnesses[trivial] = generator.fresh_symbol("w", t.witness_type()); INFO("Original axiom:\n"); - std::string s; - java_lang->from_expr(trivial, s, ns); - INFO(s + "\n\n"); + INFO(to_string(trivial) + "\n\n"); WHEN("we instantiate and simplify") { @@ -393,26 +387,23 @@ SCENARIO("instantiate_not_contains", // { .=1, .={ (char)'a' } }[x+y] != { .=0, .={ } }[y] // ) // which is false. - string_not_contains_constraintt trivial( - from_integer(0), - from_integer(1), - true_exprt(), - from_integer(0), - from_integer(0), - a_array, - empty_array); + const string_not_contains_constraintt trivial = {from_integer(0), + from_integer(1), + true_exprt(), + from_integer(0), + from_integer(0), + a_array, + empty_array}; // Create witness for axiom symbol_tablet symtab; const namespacet empty_ns(symtab); string_constraint_generatort generator(ns); - std::map witnesses; + std::unordered_map witnesses; witnesses[trivial] = generator.fresh_symbol("w", t.witness_type()); INFO("Original axiom:\n"); - std::string s; - java_lang->from_expr(trivial, s, ns); - INFO(s + "\n\n"); + INFO(to_string(trivial) + "\n\n"); WHEN("we instantiate and simplify") { @@ -451,27 +442,24 @@ SCENARIO("instantiate_not_contains", // { .=2, .={ (char)'a', (char)'b'}[y] // ) // which is false (for x = 0). - string_not_contains_constraintt trivial( - from_integer(0), - from_integer(2), - true_exprt(), - from_integer(0), - from_integer(2), - ab_array, - ab_array); + const string_not_contains_constraintt trivial = {from_integer(0), + from_integer(2), + true_exprt(), + from_integer(0), + from_integer(2), + ab_array, + ab_array}; // Create witness for axiom symbol_tablet symtab; const namespacet empty_ns(symtab); string_constraint_generatort generator(ns); - std::map witnesses; + std::unordered_map witnesses; witnesses[trivial] = generator.fresh_symbol("w", t.witness_type()); INFO("Original axiom:\n"); - std::string s; - java_lang->from_expr(trivial, s, ns); - INFO(s + "\n\n"); + INFO(to_string(trivial) + "\n\n"); WHEN("we instantiate and simplify") { @@ -508,26 +496,23 @@ SCENARIO("instantiate_not_contains", // { .=2, .={ (char)'a', (char)'b'}[y] // ) // which is true. - string_not_contains_constraintt trivial( - from_integer(0), - from_integer(2), - true_exprt(), - from_integer(0), - from_integer(2), - ab_array, - cd_array); + const string_not_contains_constraintt trivial = {from_integer(0), + from_integer(2), + true_exprt(), + from_integer(0), + from_integer(2), + ab_array, + cd_array}; // Create witness for axiom symbol_tablet symtab; const namespacet empty_ns(symtab); string_constraint_generatort generator(ns); - std::map witnesses; + std::unordered_map witnesses; witnesses[trivial] = generator.fresh_symbol("w", t.witness_type()); INFO("Original axiom:\n"); - std::string s; - java_lang->from_expr(trivial, s, ns); - INFO(s + "\n\n"); + INFO(to_string(trivial) + "\n\n"); WHEN("we instantiate and simplify") { diff --git a/src/solvers/refinement/string_constraint.cpp b/src/solvers/refinement/string_constraint.cpp index 5fd34963693..b297a1bddb9 100644 --- a/src/solvers/refinement/string_constraint.cpp +++ b/src/solvers/refinement/string_constraint.cpp @@ -46,3 +46,43 @@ string_constraintt::string_constraintt( "String constraints must have non-negative upper bound.\n" + upper_bound.pretty()); } + +/// Used for debug printing. +/// \param [in] expr: constraint to render +/// \return rendered string +std::string to_string(const string_not_contains_constraintt &expr) +{ + std::ostringstream out; + out << "forall x in [" << format(expr.univ_lower_bound) << ", " + << format(expr.univ_upper_bound) << "). " << format(expr.premise) + << " => (" + << "exists y in [" << format(expr.exists_lower_bound) << ", " + << format(expr.exists_upper_bound) << "). " << format(expr.s0) + << "[x+y] != " << format(expr.s1) << "[y])"; + return out.str(); +} + +void replace( + const union_find_replacet &replace_map, + string_not_contains_constraintt &constraint) +{ + replace_map.replace_expr(constraint.univ_lower_bound); + replace_map.replace_expr(constraint.univ_upper_bound); + replace_map.replace_expr(constraint.premise); + replace_map.replace_expr(constraint.exists_lower_bound); + replace_map.replace_expr(constraint.exists_upper_bound); + replace_map.replace_expr(constraint.s0); + replace_map.replace_expr(constraint.s1); +} + +bool operator==( + const string_not_contains_constraintt &left, + const string_not_contains_constraintt &right) +{ + return left.univ_upper_bound == right.univ_upper_bound && + left.univ_lower_bound == right.univ_lower_bound && + left.exists_lower_bound == right.exists_lower_bound && + left.exists_upper_bound == right.exists_upper_bound && + left.premise == right.premise && left.s0 == right.s0 && + left.s1 == right.s1; +} diff --git a/src/solvers/refinement/string_constraint.h b/src/solvers/refinement/string_constraint.h index 2786f91e0e8..2b77ca6bb64 100644 --- a/src/solvers/refinement/string_constraint.h +++ b/src/solvers/refinement/string_constraint.h @@ -104,7 +104,7 @@ class string_constraintt final }; /// Used for debug printing. -/// \param [in] expr: constraint to render +/// \param expr: constraint to render /// \return rendered string inline std::string to_string(const string_constraintt &expr) { @@ -116,98 +116,50 @@ inline std::string to_string(const string_constraintt &expr) } /// Constraints to encode non containement of strings. -class string_not_contains_constraintt : public exprt +/// string_not contains_constraintt are formulas of the form: +/// ``` +/// forall x in [univ_lower_bound, univ_upper_bound[. +/// premise(x) => +/// exists y in [exists_lower_bound, exists_upper_bound[. s0[x+y] != s1[y] +/// ``` +struct string_not_contains_constraintt { -public: - // string_not contains_constraintt are formula of the form: - // forall x in [lb,ub[. p(x) => exists y in [lb,ub[. s0[x+y] != s1[y] - - string_not_contains_constraintt( - exprt univ_lower_bound, - exprt univ_bound_sup, - exprt premise, - exprt exists_bound_inf, - exprt exists_bound_sup, - const array_string_exprt &s0, - const array_string_exprt &s1) - : exprt(ID_string_not_contains_constraint) - { - copy_to_operands(univ_lower_bound, univ_bound_sup, premise); - copy_to_operands(exists_bound_inf, exists_bound_sup, s0); - copy_to_operands(s1); - }; - - const exprt &univ_lower_bound() const - { - return op0(); - } - - const exprt &univ_upper_bound() const - { - return op1(); - } - - const exprt &premise() const - { - return op2(); - } + exprt univ_lower_bound; + exprt univ_upper_bound; + exprt premise; + exprt exists_lower_bound; + exprt exists_upper_bound; + array_string_exprt s0; + array_string_exprt s1; +}; - const exprt &exists_lower_bound() const - { - return op3(); - } +std::string to_string(const string_not_contains_constraintt &expr); - const exprt &exists_upper_bound() const - { - return operands()[4]; - } +void replace( + const union_find_replacet &replace_map, + string_not_contains_constraintt &constraint); - const array_string_exprt &s0() const - { - return to_array_string_expr(operands()[5]); - } +bool operator==( + const string_not_contains_constraintt &left, + const string_not_contains_constraintt &right); - const array_string_exprt &s1() const +// NOLINTNEXTLINE [allow specialization within 'std'] +namespace std +{ +template <> +// NOLINTNEXTLINE [struct identifier 'hash' does not end in t] +struct hash +{ + size_t operator()(const string_not_contains_constraintt &constraint) const { - return to_array_string_expr(operands()[6]); + return irep_hash()(constraint.univ_lower_bound) ^ + irep_hash()(constraint.univ_upper_bound) ^ + irep_hash()(constraint.exists_lower_bound) ^ + irep_hash()(constraint.exists_upper_bound) ^ + irep_hash()(constraint.premise) ^ irep_hash()(constraint.s0) ^ + irep_hash()(constraint.s1); } }; - -/// Used for debug printing. -/// \param [in] expr: constraint to render -/// \return rendered string -inline std::string to_string(const string_not_contains_constraintt &expr) -{ - std::ostringstream out; - out << "forall x in [" << format(expr.univ_lower_bound()) << ", " - << format(expr.univ_upper_bound()) << "). " << format(expr.premise()) - << " => (" - << "exists y in [" << format(expr.exists_lower_bound()) << ", " - << format(expr.exists_upper_bound()) << "). " << format(expr.s0()) - << "[x+y] != " << format(expr.s1()) << "[y])"; - return out.str(); -} - -inline const string_not_contains_constraintt -&to_string_not_contains_constraint(const exprt &expr) -{ - PRECONDITION(expr.id()==ID_string_not_contains_constraint); - DATA_INVARIANT( - expr.operands().size()==7, - string_refinement_invariantt("string_not_contains_constraintt must have 7 " - "operands")); - return static_cast(expr); -} - -inline string_not_contains_constraintt -&to_string_not_contains_constraint(exprt &expr) -{ - PRECONDITION(expr.id()==ID_string_not_contains_constraint); - DATA_INVARIANT( - expr.operands().size()==7, - string_refinement_invariantt("string_not_contains_constraintt must have 7 " - "operands")); - return static_cast(expr); } #endif diff --git a/src/solvers/refinement/string_constraint_generator_indexof.cpp b/src/solvers/refinement/string_constraint_generator_indexof.cpp index 7b397490191..48e0366f018 100644 --- a/src/solvers/refinement/string_constraint_generator_indexof.cpp +++ b/src/solvers/refinement/string_constraint_generator_indexof.cpp @@ -142,17 +142,16 @@ std::pair add_axioms_for_index_of_string( // 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] - string_not_contains_constraintt a4( - from_index, - offset, - contains, - from_integer(0, index_type), - needle.length(), - haystack, - needle); + const string_not_contains_constraintt a4 = {from_index, + offset, + contains, + from_integer(0, index_type), + needle.length(), + haystack, + needle}; constraints.not_contains.push_back(a4); - string_not_contains_constraintt a5( + const string_not_contains_constraintt a5 = { from_index, plus_exprt( // Add 1 for inclusive upper bound. minus_exprt(haystack.length(), needle.length()), @@ -161,7 +160,7 @@ std::pair add_axioms_for_index_of_string( from_integer(0, index_type), needle.length(), haystack, - needle); + needle}; constraints.not_contains.push_back(a5); const implies_exprt a6( @@ -241,24 +240,24 @@ std::pair add_axioms_for_last_index_of_string( from_index, length_diff); - string_not_contains_constraintt a4( + const string_not_contains_constraintt a4 = { plus_exprt(offset, from_integer(1, index_type)), plus_exprt(end_index, from_integer(1, index_type)), contains, from_integer(0, index_type), needle.length(), haystack, - needle); + needle}; constraints.not_contains.push_back(a4); - string_not_contains_constraintt a5( + string_not_contains_constraintt a5 = { from_integer(0, index_type), plus_exprt(end_index, from_integer(1, index_type)), not_exprt(contains), from_integer(0, index_type), needle.length(), haystack, - needle); + needle}; constraints.not_contains.push_back(a5); const implies_exprt a6( diff --git a/src/solvers/refinement/string_constraint_generator_testing.cpp b/src/solvers/refinement/string_constraint_generator_testing.cpp index 2d495cfee11..fb862631ff2 100644 --- a/src/solvers/refinement/string_constraint_generator_testing.cpp +++ b/src/solvers/refinement/string_constraint_generator_testing.cpp @@ -266,14 +266,14 @@ std::pair add_axioms_for_contains( implies_exprt(contains, equal_exprt(s1[qvar], s0[qvar_shifted]))); constraints.universal.push_back(a4); - string_not_contains_constraintt a5( + const string_not_contains_constraintt a5 = { from_integer(0, index_type), plus_exprt(from_integer(1, index_type), length_diff), and_exprt(not_exprt(contains), s0.axiom_for_length_ge(s1.length())), from_integer(0, index_type), s1.length(), s0, - s1); + s1}; constraints.not_contains.push_back(a5); return {typecast_exprt(contains, f.type()), std::move(constraints)}; diff --git a/src/solvers/refinement/string_constraint_instantiation.cpp b/src/solvers/refinement/string_constraint_instantiation.cpp index 38d1384d1b6..965611724f4 100644 --- a/src/solvers/refinement/string_constraint_instantiation.cpp +++ b/src/solvers/refinement/string_constraint_instantiation.cpp @@ -21,12 +21,13 @@ Author: Jesse Sigal, jesse.sigal@diffblue.com std::vector instantiate_not_contains( const string_not_contains_constraintt &axiom, const std::set> &index_pairs, - const std::map &witnesses) + const std::unordered_map + &witnesses) { std::vector lemmas; - const array_string_exprt s0 = axiom.s0(); - const array_string_exprt s1 = axiom.s1(); + const array_string_exprt s0 = axiom.s0; + const array_string_exprt s1 = axiom.s1; for(const auto &pair : index_pairs) { @@ -36,16 +37,16 @@ std::vector instantiate_not_contains( const exprt &i1=pair.second; const minus_exprt val(i0, i1); const and_exprt universal_bound( - binary_relation_exprt(axiom.univ_lower_bound(), ID_le, val), - binary_relation_exprt(axiom.univ_upper_bound(), ID_gt, val)); + binary_relation_exprt(axiom.univ_lower_bound, ID_le, val), + binary_relation_exprt(axiom.univ_upper_bound, ID_gt, val)); const exprt f = index_exprt(witnesses.at(axiom), val); const equal_exprt relevancy(f, i1); - const and_exprt premise(relevancy, axiom.premise(), universal_bound); + const and_exprt premise(relevancy, axiom.premise, universal_bound); const notequal_exprt differ(s0[i0], s1[i1]); const and_exprt existential_bound( - binary_relation_exprt(axiom.exists_lower_bound(), ID_le, i1), - binary_relation_exprt(axiom.exists_upper_bound(), ID_gt, i1)); + binary_relation_exprt(axiom.exists_lower_bound, ID_le, i1), + binary_relation_exprt(axiom.exists_upper_bound, ID_gt, i1)); const and_exprt body(differ, existential_bound); const implies_exprt lemma(premise, body); diff --git a/src/solvers/refinement/string_constraint_instantiation.h b/src/solvers/refinement/string_constraint_instantiation.h index b473c74ae3d..c7c96375350 100644 --- a/src/solvers/refinement/string_constraint_instantiation.h +++ b/src/solvers/refinement/string_constraint_instantiation.h @@ -18,6 +18,7 @@ Author: Jesse Sigal, jesse.sigal@diffblue.com std::vector instantiate_not_contains( const string_not_contains_constraintt &axiom, const std::set> &index_pairs, - const std::map &witnesses); + const std::unordered_map + &witnesses); #endif // CPROVER_SOLVERS_REFINEMENT_STRING_CONSTRAINT_INSTANTIATION_H diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp index b2f772df520..798b8830dd5 100644 --- a/src/solvers/refinement/string_refinement.cpp +++ b/src/solvers/refinement/string_refinement.cpp @@ -64,7 +64,7 @@ static std::pair> check_axioms( const namespacet &ns, bool use_counter_example, const union_find_replacet &symbol_resolve, - const std::map + const std::unordered_map ¬_contain_witnesses); static void initial_index_set( @@ -113,7 +113,8 @@ static std::vector instantiate( const string_not_contains_constraintt &axiom, const index_set_pairt &index_set, const string_constraint_generatort &generator, - const std::map &witnesses); + const std::unordered_map + &witnesses); static optionalt get_array( const std::function &super_get, @@ -231,7 +232,7 @@ static std::vector generate_instantiations( const string_constraint_generatort &generator, const index_set_pairt &index_set, const string_axiomst &axioms, - const std::map + const std::unordered_map ¬_contain_witnesses) { std::vector lemmas; @@ -716,16 +717,17 @@ decision_proceduret::resultt string_refinementt::dec_solve() generator.constraints.not_contains.end(), std::back_inserter(axioms.not_contains), [&](string_not_contains_constraintt axiom) { - symbol_resolve.replace_expr(axiom); + replace(symbol_resolve, axiom); return axiom; }); // Used to store information about witnesses for not_contains constraints - std::map not_contain_witnesses; + std::unordered_map + not_contain_witnesses; for(const auto &nc_axiom : axioms.not_contains) { const auto &witness_type = [&] { - const auto &rtype = to_array_type(nc_axiom.s0().type()); + const auto &rtype = to_array_type(nc_axiom.s0.type()); const typet &index_type = rtype.size().type(); return array_typet(index_type, infinity_exprt(index_type)); }(); @@ -1194,12 +1196,12 @@ static exprt negation_of_not_contains_constraint( { // If the for all is vacuously true, the negation is false. const auto lbe = - numeric_cast_v(get(constraint.exists_lower_bound())); + numeric_cast_v(get(constraint.exists_lower_bound)); const auto ube = - numeric_cast_v(get(constraint.exists_upper_bound())); + numeric_cast_v(get(constraint.exists_upper_bound)); const auto univ_bounds = and_exprt( - binary_relation_exprt(get(constraint.univ_lower_bound()), ID_le, univ_var), - binary_relation_exprt(get(constraint.univ_upper_bound()), ID_gt, univ_var)); + binary_relation_exprt(get(constraint.univ_lower_bound), ID_le, univ_var), + binary_relation_exprt(get(constraint.univ_upper_bound), ID_gt, univ_var)); // The negated existential becomes an universal, and this is the unrolling of // that universal quantifier. @@ -1209,12 +1211,12 @@ static exprt negation_of_not_contains_constraint( { const constant_exprt i_expr = from_integer(i, univ_var.type()); const exprt s0_char = - get(index_exprt(constraint.s0(), plus_exprt(univ_var, i_expr))); - const exprt s1_char = get(index_exprt(constraint.s1(), i_expr)); + get(index_exprt(constraint.s0, plus_exprt(univ_var, i_expr))); + const exprt s1_char = get(index_exprt(constraint.s1, i_expr)); conjuncts.push_back(equal_exprt(s0_char, s1_char)); } const exprt equal_strings = conjunction(conjuncts); - return and_exprt(univ_bounds, get(constraint.premise()), equal_strings); + return and_exprt(univ_bounds, get(constraint.premise), equal_strings); } /// Debugging function which outputs the different steps an axiom goes through @@ -1249,7 +1251,7 @@ static std::pair> check_axioms( const namespacet &ns, bool use_counter_example, const union_find_replacet &symbol_resolve, - const std::map + const std::unordered_map ¬_contain_witnesses) { const auto eom=messaget::eom; @@ -1317,7 +1319,7 @@ static std::pair> check_axioms( { const string_not_contains_constraintt &nc_axiom=axioms.not_contains[i]; const symbol_exprt univ_var = generator.fresh_symbol( - "not_contains_univ_var", nc_axiom.s0().length().type()); + "not_contains_univ_var", nc_axiom.s0.length().type()); const exprt negated_axiom = negation_of_not_contains_constraint( nc_axiom, univ_var, [&](const exprt &expr) { return simplify_expr(get(expr), ns); }); @@ -1742,8 +1744,8 @@ static void initial_index_set( const namespacet &ns, const string_not_contains_constraintt &axiom) { - auto it=axiom.premise().depth_begin(); - const auto end=axiom.premise().depth_end(); + auto it = axiom.premise.depth_begin(); + const auto end = axiom.premise.depth_end(); while(it!=end) { if(it->id() == ID_index && is_char_type(it->type())) @@ -1761,9 +1763,8 @@ static void initial_index_set( } const minus_exprt kminus1( - axiom.exists_upper_bound(), - from_integer(1, axiom.exists_upper_bound().type())); - add_to_index_set(index_set, ns, axiom.s1().content(), kminus1); + axiom.exists_upper_bound, from_integer(1, axiom.exists_upper_bound.type())); + add_to_index_set(index_set, ns, axiom.s1.content(), kminus1); } /// Add to the index set all the indices that appear in the formula @@ -1887,10 +1888,11 @@ static std::vector instantiate( const string_not_contains_constraintt &axiom, const index_set_pairt &index_set, const string_constraint_generatort &generator, - const std::map &witnesses) + const std::unordered_map + &witnesses) { - const array_string_exprt &s0 = axiom.s0(); - const array_string_exprt &s1 = axiom.s1(); + const array_string_exprt &s0 = axiom.s0; + const array_string_exprt &s1 = axiom.s1; const auto &index_set0=index_set.cumulative.find(s0.content()); const auto &index_set1=index_set.cumulative.find(s1.content()); From 14057f508ef20271befbf920299c2dbe3903495c Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Fri, 2 Nov 2018 10:38:18 +0000 Subject: [PATCH 2/2] Remove unused ID_string_not_contains_constraint --- src/util/irep_ids.def | 1 - 1 file changed, 1 deletion(-) diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def index 595096bec87..4d2b2b4a43d 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -582,7 +582,6 @@ IREP_ID_ONE(push_catch) IREP_ID_ONE(pop_catch) IREP_ID_ONE(exception_landingpad) IREP_ID_ONE(length_upper_bound) -IREP_ID_ONE(string_not_contains_constraint) IREP_ID_ONE(cprover_associate_array_to_pointer_func) IREP_ID_ONE(cprover_associate_length_to_array_func) IREP_ID_ONE(cprover_char_literal_func)