From e4e2b10260395bbe81ac5bc44887f8c0d49c3834 Mon Sep 17 00:00:00 2001 From: Jesse Sigal Date: Wed, 20 Sep 2017 13:21:29 +0100 Subject: [PATCH] TG-592 Implemented the correct instantiation procedure for not contains constraints The method of insantiating not contains constraints is correct, see TG-591. This involved a localized change to `string_constraint_instantiation.cpp:instantiate_not_contains`, but also involved the activation of counter-examples in `string_refinementt`. The reason for this is that the new (correct) instances are relatively weak, and the solver will end up with an empty index set. The current behavior of returning SAT in this case is incorrect, and will be fixed shortly by TG-672. Additionally, the choice of indices at which to instantiate not contains constraints has been changed to be more sensible. Finally, the relevant unit tests have been updated. --- .../string_constraint_instantiation.cpp | 71 ++++++++----------- .../string_constraint_instantiation.h | 3 +- src/solvers/refinement/string_refinement.cpp | 68 ++++++++++++------ src/solvers/refinement/string_refinement.h | 2 +- .../instantiate_not_contains.cpp | 40 ++++++----- 5 files changed, 101 insertions(+), 83 deletions(-) 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);