Skip to content

TG-592 Implemented the correct instantiation procedure for not contains constraints #1407

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
Sep 24, 2017
Merged

TG-592 Implemented the correct instantiation procedure for not contains constraints #1407

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
71 changes: 28 additions & 43 deletions src/solvers/refinement/string_constraint_instantiation.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,61 +11,46 @@ Author: Jesse Sigal, jesse.sigal@diffblue.com

#include <solvers/refinement/string_constraint_instantiation.h>

#include <solvers/refinement/string_constraint.h>
#include <solvers/refinement/string_constraint_generator.h>
#include <solvers/refinement/string_refinement.h>

/// 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<exprt> instantiate_not_contains(
const string_not_contains_constraintt &axiom,
const std::set<exprt> &index_set0,
const std::set<exprt> &index_set1,
const std::set<std::pair<exprt, exprt>> &index_pairs,
const string_constraint_generatort &generator)
{
std::vector<exprt> 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;
}
3 changes: 1 addition & 2 deletions src/solvers/refinement/string_constraint_instantiation.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -17,8 +17,7 @@ Author: Jesse Sigal, jesse.sigal@diffblue.com

std::vector<exprt> instantiate_not_contains(
const string_not_contains_constraintt &axiom,
const std::set<exprt> &index_set0,
const std::set<exprt> &index_set1,
const std::set<std::pair<exprt, exprt>> &index_pairs,
const string_constraint_generatort &generator);

#endif // CPROVER_SOLVERS_REFINEMENT_STRING_CONSTRAINT_INSTANTIATION_H
68 changes: 47 additions & 21 deletions src/solvers/refinement/string_refinement.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -99,6 +99,7 @@ static std::vector<exprt> instantiate_not_contains(
const namespacet &ns,
const string_not_contains_constraintt &axiom,
const std::map<exprt, std::set<exprt>> &index_set,
const std::map<exprt, std::set<exprt>> &current_index_set,
const string_constraint_generatort &generator);

static exprt get_array(
Expand Down Expand Up @@ -850,7 +851,12 @@ decision_proceduret::resultt string_refinementt::dec_solve()
debug() << "constraint " << i << '\n';
const std::vector<exprt> 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);
}
Expand Down Expand Up @@ -1510,23 +1516,26 @@ static std::pair<bool, std::vector<exprt>> check_axioms(

if(use_counter_example)
Copy link
Contributor

@romainbrenguier romainbrenguier Sep 20, 2017

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Could we put this block into a new function, and call it from dec_solve? Because this is not really checking axioms but adding new things to the solver.

Copy link
Contributor Author

@jasigal jasigal Sep 22, 2017

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

In my refactor ticket, I really rearrange dec_solve, including this. Is that okay?

{
// 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<exprt> 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<std::pair<exprt, exprt>> indices;
indices.insert(std::pair<exprt, exprt>(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 };
}
Expand Down Expand Up @@ -1960,19 +1969,36 @@ static std::vector<exprt> instantiate_not_contains(
const namespacet &ns,
const string_not_contains_constraintt &axiom,
const std::map<exprt, std::set<exprt>> &index_set,
const std::map<exprt, std::set<exprt>> &current_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 &current_index_set0=current_index_set.find(s0.content());
const auto &current_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<exprt, exprt> expr_pairt;
std::set<expr_pairt> 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 { };
}
Expand Down
2 changes: 1 addition & 1 deletion src/solvers/refinement/string_refinement.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Copy link
Contributor

@romainbrenguier romainbrenguier Sep 22, 2017

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

we could remove this variable has it is never modified

Copy link
Contributor Author

@jasigal jasigal Sep 22, 2017

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think it should still be kept, as it was kept before, because it can have a big effect on the solver. If you're not using not contains constraints, I think it's pretty unnecessary based on our tests. However, it will probably add a good number of new lemmas. I think there may a command line argument in test-gen that can set this.

Copy link
Member

@peterschrammel peterschrammel Sep 22, 2017

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

How would you decide when to turn off/on that flag?

Copy link
Contributor Author

@jasigal jasigal Sep 22, 2017

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Would leave it on by default so that more tests are produced by test-gen, but would be turned off it test-gen mem'd or timed out (and could be tracked to strings). Then you could turn it off, which would keep correctness but possibly produce less tests when not contains constraints are involved.

};
public:
/// string_refinementt constructor arguments
Expand Down
40 changes: 24 additions & 16 deletions unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,12 +11,9 @@
#include <solvers/refinement/string_constraint_instantiation.h>

#include <solvers/sat/satcheck.h>
#include <solvers/refinement/bv_refinement.h>
#include <java_bytecode/java_types.h>
#include <langapi/mode.h>
#include <java_bytecode/java_bytecode_language.h>
#include <util/namespace.h>
#include <util/symbol_table.h>
#include <util/simplify_expr.h>

/// \class Types used throughout the test. Currently it is impossible to
Expand Down Expand Up @@ -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());
}
Expand Down Expand Up @@ -81,6 +78,17 @@ std::set<exprt> full_index_set(const string_exprt &s)
return ret;
}

/// Create the cartesian product of two sets.
template<class T, class U>
std::set<std::pair<T, U>> product(const std::set<T> ts, const std::set<U> us)
Copy link
Contributor

@romainbrenguier romainbrenguier Sep 22, 2017

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

depending on the usage, you could replace this set by a vector since all insertions are going to be distinct.

Copy link
Contributor Author

@jasigal jasigal Sep 22, 2017

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The sets are used because sets are used in string_refinementt, where a set is needed because insertions aren't unique. Hence I had to use sets here, and why this utility function uses sets.

{
std::set<std::pair<T, U>> s;
for(const auto &t : ts)
for(const auto &u : us)
s.insert(std::pair<T, U>(t, u));
return s;
}

/// Simplifies, and returns the conjunction of the lemmas.
/// \param [in] lemmas: lemmas to process
/// \param [in] ns: namespace for simplifying
Expand Down Expand Up @@ -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);
Expand Down Expand Up @@ -196,7 +204,7 @@ SCENARIO("instantiate_not_contains",
for(const auto &axiom : nc_axioms)
{
const std::vector<exprt> 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());
}

Expand Down Expand Up @@ -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]=
Expand All @@ -255,7 +263,7 @@ SCENARIO("instantiate_not_contains",

// Instantiate the lemmas
std::vector<exprt> 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);
Expand Down Expand Up @@ -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]=
Expand All @@ -314,7 +322,7 @@ SCENARIO("instantiate_not_contains",

// Instantiate the lemmas
std::vector<exprt> 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);
Expand Down Expand Up @@ -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]=
Expand All @@ -374,7 +382,7 @@ SCENARIO("instantiate_not_contains",

// Instantiate the lemmas
std::vector<exprt> 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);
Expand Down Expand Up @@ -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);
Expand All @@ -433,7 +441,7 @@ SCENARIO("instantiate_not_contains",

// Instantiate the lemmas
std::vector<exprt> 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);
Expand Down Expand Up @@ -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]=
Expand All @@ -493,7 +501,7 @@ SCENARIO("instantiate_not_contains",

// Instantiate the lemmas
std::vector<exprt> 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);
Expand Down