diff --git a/src/solvers/refinement/string_constraint_instantiation.cpp b/src/solvers/refinement/string_constraint_instantiation.cpp index ca3a63861a2..7a99bb0e969 100644 --- a/src/solvers/refinement/string_constraint_instantiation.cpp +++ b/src/solvers/refinement/string_constraint_instantiation.cpp @@ -11,61 +11,46 @@ Author: Jesse Sigal, jesse.sigal@diffblue.com #include -#include -#include -#include - /// Instantiates a quantified formula representing `not_contains` by /// substituting the quantifiers and generating axioms. /// \related string_refinementt /// \param [in] axiom: the axiom to instantiate -/// \param [in] index_set0: the index set for `axiom.s0()` -/// \param [in] index_set1: the index set for `axiom.s1()` +/// \param [in] index_pairs: the pairs of indices to at which to instantiate /// \param [in] generator: generator to be used to get `axiom`'s witness /// \return the lemmas produced through instantiation std::vector instantiate_not_contains( const string_not_contains_constraintt &axiom, - const std::set &index_set0, - const std::set &index_set1, + const std::set> &index_pairs, const string_constraint_generatort &generator) { std::vector lemmas; - const string_exprt s0=to_string_expr(axiom.s0()); - const string_exprt s1=to_string_expr(axiom.s1()); - - for(const auto &i0 : index_set0) - for(const auto &i1 : index_set1) - { - const minus_exprt val(i0, i1); - const exprt witness=generator.get_witness_of(axiom, val); - const and_exprt prem_and_is_witness( - axiom.premise(), - equal_exprt(witness, i1)); - - const not_exprt differ(equal_exprt(s0[i0], s1[i1])); - const implies_exprt lemma(prem_and_is_witness, differ); - lemmas.push_back(lemma); - - // we put bounds on the witnesses: - // 0 <= v <= |s0| - |s1| ==> 0 <= v+w[v] < |s0| && 0 <= w[v] < |s1| - const exprt zero=from_integer(0, val.type()); - const binary_relation_exprt c1(zero, ID_le, plus_exprt(val, witness)); - const binary_relation_exprt c2( - s0.length(), ID_gt, plus_exprt(val, witness)); - const binary_relation_exprt c3(s1.length(), ID_gt, witness); - const binary_relation_exprt c4(zero, ID_le, witness); - - const minus_exprt diff(s0.length(), s1.length()); - - const and_exprt premise( - binary_relation_exprt(zero, ID_le, val), - binary_relation_exprt(diff, ID_ge, val)); - const implies_exprt witness_bounds( - premise, - and_exprt(and_exprt(c1, c2), and_exprt(c3, c4))); - lemmas.push_back(witness_bounds); - } + const string_exprt &s0=to_string_expr(axiom.s0()); + const string_exprt &s1=to_string_expr(axiom.s1()); + + for(const auto &pair : index_pairs) + { + // We have s0[x+f(x)] and s1[f(x)], so to have i0 indexing s0 and i1 + // indexing s1, we need x = i0 - i1 and f(i0 - i1) = f(x) = i1. + const exprt &i0=pair.first; + 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)); + const exprt f=generator.get_witness_of(axiom, val); + const equal_exprt relevancy(f, i1); + 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)); + const and_exprt body(differ, existential_bound); + + const implies_exprt lemma(premise, body); + lemmas.push_back(lemma); + } return lemmas; } diff --git a/src/solvers/refinement/string_constraint_instantiation.h b/src/solvers/refinement/string_constraint_instantiation.h index f4918e7e8d9..05779b37ddd 100644 --- a/src/solvers/refinement/string_constraint_instantiation.h +++ b/src/solvers/refinement/string_constraint_instantiation.h @@ -17,8 +17,7 @@ Author: Jesse Sigal, jesse.sigal@diffblue.com std::vector instantiate_not_contains( const string_not_contains_constraintt &axiom, - const std::set &index_set0, - const std::set &index_set1, + const std::set> &index_pairs, const string_constraint_generatort &generator); #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 483eb07ac30..edace2724da 100644 --- a/src/solvers/refinement/string_refinement.cpp +++ b/src/solvers/refinement/string_refinement.cpp @@ -99,6 +99,7 @@ static std::vector instantiate_not_contains( const namespacet &ns, const string_not_contains_constraintt &axiom, const std::map> &index_set, + const std::map> ¤t_index_set, const string_constraint_generatort &generator); static exprt get_array( @@ -850,7 +851,12 @@ decision_proceduret::resultt string_refinementt::dec_solve() debug() << "constraint " << i << '\n'; const std::vector lemmas= instantiate_not_contains( - debug(), ns, not_contains_axioms[i], index_set, generator); + debug(), + ns, + not_contains_axioms[i], + index_set, + current_index_set, + generator); for(const exprt &lemma : lemmas) add_lemma(lemma); } @@ -1510,23 +1516,26 @@ static std::pair> check_axioms( if(use_counter_example) { - // TODO: add counter examples for not_contains? + stream << "Adding counter-examples: " << eom; + // TODO: add counter-examples for universal constraints? - // Checking if the current solution satisfies the constraints std::vector lemmas; - for(const auto &v : violated) + for(const auto &v : violated_not_contains) { const exprt &val=v.second; - const string_constraintt &axiom=universal_axioms[v.first]; - - exprt premise(axiom.premise()); - exprt body(axiom.body()); - implies_exprt instance(premise, body); - replace_expr(symbol_resolve, instance); - replace_expr(axiom.univ_var(), val, instance); - stream << "adding counter example " << from_expr(ns, "", instance) - << eom; - lemmas.push_back(instance); + const string_not_contains_constraintt &axiom= + not_contains_axioms[v.first]; + + const exprt func_val=generator.get_witness_of(axiom, val); + const exprt comp_val=simplify_sum(plus_exprt(val, func_val)); + + std::set> indices; + indices.insert(std::pair(comp_val, func_val)); + const exprt counter=::instantiate_not_contains( + axiom, indices, generator)[0]; + + stream << " - " << from_expr(ns, "", counter) << eom; + lemmas.push_back(counter); } return { false, lemmas }; } @@ -1960,19 +1969,36 @@ static std::vector instantiate_not_contains( const namespacet &ns, const string_not_contains_constraintt &axiom, const std::map> &index_set, + const std::map> ¤t_index_set, const string_constraint_generatort &generator) { - const string_exprt s0=to_string_expr(axiom.s0()); - const string_exprt s1=to_string_expr(axiom.s1()); + const string_exprt &s0=axiom.s0(); + const string_exprt &s1=axiom.s1(); stream << "instantiate not contains " << from_expr(ns, "", s0) << " : " << from_expr(ns, "", s1) << messaget::eom; - const auto &i0=index_set.find(s0.content()); - const auto &i1=index_set.find(s1.content()); - if(i0!=index_set.end() && i1!=index_set.end()) + + const auto &index_set0=index_set.find(s0.content()); + const auto &index_set1=index_set.find(s1.content()); + const auto ¤t_index_set0=current_index_set.find(s0.content()); + const auto ¤t_index_set1=current_index_set.find(s1.content()); + + if(index_set0!=index_set.end() && + index_set1!=index_set.end() && + current_index_set0!=index_set.end() && + current_index_set1!=index_set.end()) { - return ::instantiate_not_contains( - axiom, i0->second, i1->second, generator); + typedef std::pair expr_pairt; + std::set index_pairs; + + for(const auto &ic0 : current_index_set0->second) + for(const auto &i1 : index_set1->second) + index_pairs.insert(expr_pairt(ic0, i1)); + for(const auto &ic1 : current_index_set1->second) + for(const auto &i0 : index_set0->second) + index_pairs.insert(expr_pairt(i0, ic1)); + + return ::instantiate_not_contains(axiom, index_pairs, generator); } return { }; } diff --git a/src/solvers/refinement/string_refinement.h b/src/solvers/refinement/string_refinement.h index b070047c582..c584b953744 100644 --- a/src/solvers/refinement/string_refinement.h +++ b/src/solvers/refinement/string_refinement.h @@ -39,7 +39,7 @@ class string_refinementt final: public bv_refinementt bool string_non_empty=false; /// Concretize strings after solver is finished bool trace=false; - bool use_counter_example=false; + bool use_counter_example=true; }; public: /// string_refinementt constructor arguments 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 a0ecd2e3f5c..2cd07e9f082 100644 --- a/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp +++ b/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp @@ -11,12 +11,9 @@ #include #include -#include #include #include #include -#include -#include #include /// \class Types used throughout the test. Currently it is impossible to @@ -48,7 +45,7 @@ const tt t; /// Creates a `constant_exprt` of the proper length type. /// \param [in] i: integer to convert /// \return corresponding `constant_exprt` -constant_exprt from_integer(const mp_integer i) +constant_exprt from_integer(const mp_integer &i) { return from_integer(i, t.length_type()); } @@ -81,6 +78,17 @@ std::set full_index_set(const string_exprt &s) return ret; } +/// Create the cartesian product of two sets. +template +std::set> product(const std::set ts, const std::set us) +{ + std::set> s; + for(const auto &t : ts) + for(const auto &u : us) + s.insert(std::pair(t, u)); + return s; +} + /// Simplifies, and returns the conjunction of the lemmas. /// \param [in] lemmas: lemmas to process /// \param [in] ns: namespace for simplifying @@ -152,7 +160,7 @@ SCENARIO("instantiate_not_contains", // Generating the corresponding axioms and simplifying, recording info symbol_tablet symtab; - namespacet empty_ns(symtab); + const namespacet empty_ns(symtab); string_constraint_generatort::infot info; string_constraint_generatort generator(info, ns); exprt res=generator.add_axioms_for_function_application(func); @@ -196,7 +204,7 @@ SCENARIO("instantiate_not_contains", for(const auto &axiom : nc_axioms) { const std::vector l=instantiate_not_contains( - axiom, index_set_ab, index_set_b, generator); + axiom, product(index_set_ab, index_set_b), generator); lemmas.insert(lemmas.end(), l.begin(), l.end()); } @@ -239,7 +247,7 @@ SCENARIO("instantiate_not_contains", // Create witness for axiom symbol_tablet symtab; - namespacet empty_ns(symtab); + const namespacet empty_ns(symtab); string_constraint_generatort::infot info; string_constraint_generatort generator(info, ns); generator.witness[vacuous]= @@ -255,7 +263,7 @@ SCENARIO("instantiate_not_contains", // Instantiate the lemmas std::vector lemmas=instantiate_not_contains( - vacuous, index_set_a, index_set_a, generator); + vacuous, product(index_set_a, index_set_a), generator); const exprt conj=combine_lemmas(lemmas, ns); const std::string info=create_info(lemmas, ns); @@ -297,7 +305,7 @@ SCENARIO("instantiate_not_contains", // Create witness for axiom symbol_tablet symtab; - namespacet ns(symtab); + const namespacet ns(symtab); string_constraint_generatort::infot info; string_constraint_generatort generator(info, ns); generator.witness[trivial]= @@ -314,7 +322,7 @@ SCENARIO("instantiate_not_contains", // Instantiate the lemmas std::vector lemmas=instantiate_not_contains( - trivial, index_set_a, index_set_b, generator); + trivial, product(index_set_a, index_set_b), generator); const exprt conj=combine_lemmas(lemmas, ns); const std::string info=create_info(lemmas, ns); @@ -356,7 +364,7 @@ SCENARIO("instantiate_not_contains", // Create witness for axiom symbol_tablet symtab; - namespacet empty_ns(symtab); + const namespacet empty_ns(symtab); string_constraint_generatort::infot info; string_constraint_generatort generator(info, ns); generator.witness[trivial]= @@ -374,7 +382,7 @@ SCENARIO("instantiate_not_contains", // Instantiate the lemmas std::vector lemmas=instantiate_not_contains( - trivial, index_set_a, index_set_empty, generator); + trivial, product(index_set_a, index_set_empty), generator); const exprt conj=combine_lemmas(lemmas, ns); const std::string info=create_info(lemmas, ns); @@ -416,7 +424,7 @@ SCENARIO("instantiate_not_contains", // Create witness for axiom symbol_tablet symtab; - namespacet empty_ns(symtab); + const namespacet empty_ns(symtab); string_constraint_generatort::infot info; string_constraint_generatort generator(info, ns); @@ -433,7 +441,7 @@ SCENARIO("instantiate_not_contains", // Instantiate the lemmas std::vector lemmas=instantiate_not_contains( - trivial, index_set_ab, index_set_ab, generator); + trivial, product(index_set_ab, index_set_ab), generator); const exprt conj=combine_lemmas(lemmas, ns); const std::string info=create_info(lemmas, ns); @@ -476,7 +484,7 @@ SCENARIO("instantiate_not_contains", // Create witness for axiom symbol_tablet symtab; - namespacet empty_ns(symtab); + const namespacet empty_ns(symtab); string_constraint_generatort::infot info; string_constraint_generatort generator(info, ns); generator.witness[trivial]= @@ -493,7 +501,7 @@ SCENARIO("instantiate_not_contains", // Instantiate the lemmas std::vector lemmas=instantiate_not_contains( - trivial, index_set_ab, index_set_cd, generator); + trivial, product(index_set_ab, index_set_cd), generator); const exprt conj=combine_lemmas(lemmas, ns); const std::string info=create_info(lemmas, ns);