Skip to content

Make string_not_contains_constraintt a struct #3256

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 2 commits into from
Nov 8, 2018
Merged

Make string_not_contains_constraintt a struct #3256

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
15131da
Make string_not_contains_constraintt a struct
romainbrenguier Oct 31, 2018
14057f5
Remove unused ID_string_not_contains_constraint
romainbrenguier Nov 2, 2018
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
115 changes: 50 additions & 65 deletions jbmc/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 @@ -202,7 +202,7 @@ SCENARIO("instantiate_not_contains",

std::string axioms;
std::vector<string_not_contains_constraintt> nc_axioms;
std::map<string_not_contains_constraintt, symbol_exprt> witnesses;
std::unordered_map<string_not_contains_constraintt, symbol_exprt> witnesses;

std::accumulate(
constraints.universal.begin(),
Expand All @@ -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(
Expand Down Expand Up @@ -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<string_not_contains_constraintt, symbol_exprt> witnesses;
std::unordered_map<string_not_contains_constraintt, symbol_exprt> witnesses;
witnesses[vacuous] = generator.fresh_symbol("w", t.witness_type());

INFO("Original axiom:\n");
Copy link
Member

Choose a reason for hiding this comment

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

Side remark (not for this PR): Calling debug output INFO is a bit confusing.

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")
{
Expand Down Expand Up @@ -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<string_not_contains_constraintt, symbol_exprt> witnesses;
std::unordered_map<string_not_contains_constraintt, symbol_exprt> 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")
{
Expand Down Expand Up @@ -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<string_not_contains_constraintt, symbol_exprt> witnesses;
std::unordered_map<string_not_contains_constraintt, symbol_exprt> 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")
{
Expand Down Expand Up @@ -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<string_not_contains_constraintt, symbol_exprt> witnesses;
std::unordered_map<string_not_contains_constraintt, symbol_exprt> 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")
{
Expand Down Expand Up @@ -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<string_not_contains_constraintt, symbol_exprt> witnesses;
std::unordered_map<string_not_contains_constraintt, symbol_exprt> 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")
{
Expand Down
40 changes: 40 additions & 0 deletions src/solvers/refinement/string_constraint.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Copy link

Choose a reason for hiding this comment

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

Is the [in] needed?

/// \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;
}
122 changes: 37 additions & 85 deletions src/solvers/refinement/string_constraint.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
{
Expand All @@ -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<string_not_contains_constraintt>
{
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<const string_not_contains_constraintt &>(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<string_not_contains_constraintt &>(expr);
}

#endif
Loading