Skip to content

Commit 78ae508

Browse files
romainbrenguierromainbrenguier
committed
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 named 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.
1 parent 75bec44 commit 78ae508

8 files changed

+173
-197
lines changed

‎jbmc/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp

Lines changed: 50 additions & 65 deletions
Original file line numberDiff line numberDiff line change
@@ -202,7 +202,7 @@ SCENARIO("instantiate_not_contains",
202202

203203
std::string axioms;
204204
std::vector<string_not_contains_constraintt> nc_axioms;
205-
std::map<string_not_contains_constraintt, symbol_exprt> witnesses;
205+
std::unordered_map<string_not_contains_constraintt, symbol_exprt> witnesses;
206206

207207
std::accumulate(
208208
constraints.universal.begin(),
@@ -218,12 +218,12 @@ SCENARIO("instantiate_not_contains",
218218
constraints.not_contains.end(),
219219
axioms,
220220
[&](const std::string &accu, string_not_contains_constraintt sc) {
221-
simplify(sc, ns);
221+
simplify(sc.premise, ns);
222+
simplify(sc.s0, ns);
223+
simplify(sc.s1, ns);
222224
witnesses[sc] = generator.fresh_symbol("w", t.witness_type());
223225
nc_axioms.push_back(sc);
224-
std::string s;
225-
java_lang->from_expr(sc, s, ns);
226-
return accu + s + "\n\n";
226+
return accu + to_string(sc) + "\n\n";
227227
});
228228

229229
axioms = std::accumulate(
@@ -282,26 +282,23 @@ SCENARIO("instantiate_not_contains",
282282
// { .=1, .={ (char)'a' } }[x+y] != { .=1, .={ (char)'b' } }[y]
283283
// )
284284
// which is vacuously true.
285-
string_not_contains_constraintt vacuous(
286-
from_integer(0),
287-
from_integer(0),
288-
true_exprt(),
289-
from_integer(0),
290-
from_integer(1),
291-
a_array,
292-
a_array);
285+
const string_not_contains_constraintt vacuous = {from_integer(0),
286+
from_integer(0),
287+
true_exprt(),
288+
from_integer(0),
289+
from_integer(1),
290+
a_array,
291+
a_array};
293292

294293
// Create witness for axiom
295294
symbol_tablet symtab;
296295
const namespacet empty_ns(symtab);
297296
string_constraint_generatort generator(ns);
298-
std::map<string_not_contains_constraintt, symbol_exprt> witnesses;
297+
std::unordered_map<string_not_contains_constraintt, symbol_exprt> witnesses;
299298
witnesses[vacuous] = generator.fresh_symbol("w", t.witness_type());
300299

301300
INFO("Original axiom:\n");
302-
std::string s;
303-
java_lang->from_expr(vacuous, s, ns);
304-
INFO(s + "\n\n");
301+
INFO(to_string(vacuous) + "\n\n");
305302

306303
WHEN("we instantiate and simplify")
307304
{
@@ -337,26 +334,23 @@ SCENARIO("instantiate_not_contains",
337334
// { .=1, .={ (char)'a' } }[x+y] != { .=1, .={ (char)'b' } }[y]
338335
// )
339336
// which is false.
340-
string_not_contains_constraintt trivial(
341-
from_integer(0),
342-
from_integer(1),
343-
true_exprt(),
344-
from_integer(0),
345-
from_integer(0),
346-
a_array,
347-
b_array);
337+
const string_not_contains_constraintt trivial = {from_integer(0),
338+
from_integer(1),
339+
true_exprt(),
340+
from_integer(0),
341+
from_integer(0),
342+
a_array,
343+
b_array};
348344

349345
// Create witness for axiom
350346
symbol_tablet symtab;
351347
const namespacet ns(symtab);
352348
string_constraint_generatort generator(ns);
353-
std::map<string_not_contains_constraintt, symbol_exprt> witnesses;
349+
std::unordered_map<string_not_contains_constraintt, symbol_exprt> witnesses;
354350
witnesses[trivial] = generator.fresh_symbol("w", t.witness_type());
355351

356352
INFO("Original axiom:\n");
357-
std::string s;
358-
java_lang->from_expr(trivial, s, ns);
359-
INFO(s + "\n\n");
353+
INFO(to_string(trivial) + "\n\n");
360354

361355
WHEN("we instantiate and simplify")
362356
{
@@ -393,26 +387,23 @@ SCENARIO("instantiate_not_contains",
393387
// { .=1, .={ (char)'a' } }[x+y] != { .=0, .={ } }[y]
394388
// )
395389
// which is false.
396-
string_not_contains_constraintt trivial(
397-
from_integer(0),
398-
from_integer(1),
399-
true_exprt(),
400-
from_integer(0),
401-
from_integer(0),
402-
a_array,
403-
empty_array);
390+
const string_not_contains_constraintt trivial = {from_integer(0),
391+
from_integer(1),
392+
true_exprt(),
393+
from_integer(0),
394+
from_integer(0),
395+
a_array,
396+
empty_array};
404397

405398
// Create witness for axiom
406399
symbol_tablet symtab;
407400
const namespacet empty_ns(symtab);
408401
string_constraint_generatort generator(ns);
409-
std::map<string_not_contains_constraintt, symbol_exprt> witnesses;
402+
std::unordered_map<string_not_contains_constraintt, symbol_exprt> witnesses;
410403
witnesses[trivial] = generator.fresh_symbol("w", t.witness_type());
411404

412405
INFO("Original axiom:\n");
413-
std::string s;
414-
java_lang->from_expr(trivial, s, ns);
415-
INFO(s + "\n\n");
406+
INFO(to_string(trivial) + "\n\n");
416407

417408
WHEN("we instantiate and simplify")
418409
{
@@ -451,27 +442,24 @@ SCENARIO("instantiate_not_contains",
451442
// { .=2, .={ (char)'a', (char)'b'}[y]
452443
// )
453444
// which is false (for x = 0).
454-
string_not_contains_constraintt trivial(
455-
from_integer(0),
456-
from_integer(2),
457-
true_exprt(),
458-
from_integer(0),
459-
from_integer(2),
460-
ab_array,
461-
ab_array);
445+
const string_not_contains_constraintt trivial = {from_integer(0),
446+
from_integer(2),
447+
true_exprt(),
448+
from_integer(0),
449+
from_integer(2),
450+
ab_array,
451+
ab_array};
462452

463453
// Create witness for axiom
464454
symbol_tablet symtab;
465455
const namespacet empty_ns(symtab);
466456

467457
string_constraint_generatort generator(ns);
468-
std::map<string_not_contains_constraintt, symbol_exprt> witnesses;
458+
std::unordered_map<string_not_contains_constraintt, symbol_exprt> witnesses;
469459
witnesses[trivial] = generator.fresh_symbol("w", t.witness_type());
470460

471461
INFO("Original axiom:\n");
472-
std::string s;
473-
java_lang->from_expr(trivial, s, ns);
474-
INFO(s + "\n\n");
462+
INFO(to_string(trivial) + "\n\n");
475463

476464
WHEN("we instantiate and simplify")
477465
{
@@ -508,26 +496,23 @@ SCENARIO("instantiate_not_contains",
508496
// { .=2, .={ (char)'a', (char)'b'}[y]
509497
// )
510498
// which is true.
511-
string_not_contains_constraintt trivial(
512-
from_integer(0),
513-
from_integer(2),
514-
true_exprt(),
515-
from_integer(0),
516-
from_integer(2),
517-
ab_array,
518-
cd_array);
499+
const string_not_contains_constraintt trivial = {from_integer(0),
500+
from_integer(2),
501+
true_exprt(),
502+
from_integer(0),
503+
from_integer(2),
504+
ab_array,
505+
cd_array};
519506

520507
// Create witness for axiom
521508
symbol_tablet symtab;
522509
const namespacet empty_ns(symtab);
523510
string_constraint_generatort generator(ns);
524-
std::map<string_not_contains_constraintt, symbol_exprt> witnesses;
511+
std::unordered_map<string_not_contains_constraintt, symbol_exprt> witnesses;
525512
witnesses[trivial] = generator.fresh_symbol("w", t.witness_type());
526513

527514
INFO("Original axiom:\n");
528-
std::string s;
529-
java_lang->from_expr(trivial, s, ns);
530-
INFO(s + "\n\n");
515+
INFO(to_string(trivial) + "\n\n");
531516

532517
WHEN("we instantiate and simplify")
533518
{

‎src/solvers/refinement/string_constraint.cpp

Lines changed: 40 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -46,3 +46,43 @@ string_constraintt::string_constraintt(
4646
"String constraints must have non-negative upper bound.\n" +
4747
upper_bound.pretty());
4848
}
49+
50+
/// Used for debug printing.
51+
/// \param [in] expr: constraint to render
52+
/// \return rendered string
53+
std::string to_string(const string_not_contains_constraintt &expr)
54+
{
55+
std::ostringstream out;
56+
out << "forall x in [" << format(expr.univ_lower_bound) << ", "
57+
<< format(expr.univ_upper_bound) << "). " << format(expr.premise)
58+
<< " => ("
59+
<< "exists y in [" << format(expr.exists_lower_bound) << ", "
60+
<< format(expr.exists_upper_bound) << "). " << format(expr.s0)
61+
<< "[x+y] != " << format(expr.s1) << "[y])";
62+
return out.str();
63+
}
64+
65+
void replace(
66+
const union_find_replacet &replace_map,
67+
string_not_contains_constraintt &constraint)
68+
{
69+
replace_map.replace_expr(constraint.univ_lower_bound);
70+
replace_map.replace_expr(constraint.univ_upper_bound);
71+
replace_map.replace_expr(constraint.premise);
72+
replace_map.replace_expr(constraint.exists_lower_bound);
73+
replace_map.replace_expr(constraint.exists_upper_bound);
74+
replace_map.replace_expr(constraint.s0);
75+
replace_map.replace_expr(constraint.s1);
76+
}
77+
78+
bool operator==(
79+
const string_not_contains_constraintt &left,
80+
const string_not_contains_constraintt &right)
81+
{
82+
return left.univ_upper_bound == right.univ_upper_bound &&
83+
left.univ_lower_bound == right.univ_lower_bound &&
84+
left.exists_lower_bound == right.exists_lower_bound &&
85+
left.exists_upper_bound == right.exists_upper_bound &&
86+
left.premise == right.premise && left.s0 == right.s0 &&
87+
left.s1 == right.s1;
88+
}

‎src/solvers/refinement/string_constraint.h

Lines changed: 32 additions & 84 deletions
Original file line numberDiff line numberDiff line change
@@ -116,98 +116,46 @@ inline std::string to_string(const string_constraintt &expr)
116116
}
117117

118118
/// Constraints to encode non containement of strings.
119-
class string_not_contains_constraintt : public exprt
119+
/// string_not contains_constraintt are formula of the form:
120+
/// forall x in [lb,ub[. p(x) => exists y in [lb,ub[. s0[x+y] != s1[y]
121+
struct string_not_contains_constraintt
120122
{
121-
public:
122-
// string_not contains_constraintt are formula of the form:
123-
// forall x in [lb,ub[. p(x) => exists y in [lb,ub[. s0[x+y] != s1[y]
124-
125-
string_not_contains_constraintt(
126-
exprt univ_lower_bound,
127-
exprt univ_bound_sup,
128-
exprt premise,
129-
exprt exists_bound_inf,
130-
exprt exists_bound_sup,
131-
const array_string_exprt &s0,
132-
const array_string_exprt &s1)
133-
: exprt(ID_string_not_contains_constraint)
134-
{
135-
copy_to_operands(univ_lower_bound, univ_bound_sup, premise);
136-
copy_to_operands(exists_bound_inf, exists_bound_sup, s0);
137-
copy_to_operands(s1);
138-
};
123+
exprt univ_lower_bound;
124+
exprt univ_upper_bound;
125+
exprt premise;
126+
exprt exists_lower_bound;
127+
exprt exists_upper_bound;
128+
array_string_exprt s0;
129+
array_string_exprt s1;
130+
};
139131

140-
const exprt &univ_lower_bound() const
141-
{
142-
return op0();
143-
}
132+
std::string to_string(const string_not_contains_constraintt &expr);
144133

145-
const exprt &univ_upper_bound() const
146-
{
147-
return op1();
148-
}
134+
void replace(
135+
const union_find_replacet &replace_map,
136+
string_not_contains_constraintt &constraint);
149137

150-
const exprt &premise() const
151-
{
152-
return op2();
153-
}
138+
bool operator==(
139+
const string_not_contains_constraintt &left,
140+
const string_not_contains_constraintt &right);
154141

155-
const exprt &exists_lower_bound() const
156-
{
157-
return op3();
158-
}
159-
160-
const exprt &exists_upper_bound() const
161-
{
162-
return operands()[4];
163-
}
164-
165-
const array_string_exprt &s0() const
166-
{
167-
return to_array_string_expr(operands()[5]);
168-
}
169-
170-
const array_string_exprt &s1() const
142+
// NOLINTNEXTLINE [allow specialization within 'std']
143+
namespace std
144+
{
145+
template <>
146+
// NOLINTNEXTLINE [struct identifier 'hash' does not end in t]
147+
struct hash<string_not_contains_constraintt>
148+
{
149+
size_t operator()(const string_not_contains_constraintt &constraint) const
171150
{
172-
return to_array_string_expr(operands()[6]);
151+
return irep_hash()(constraint.univ_lower_bound) ^
152+
irep_hash()(constraint.univ_upper_bound) ^
153+
irep_hash()(constraint.exists_lower_bound) ^
154+
irep_hash()(constraint.exists_upper_bound) ^
155+
irep_hash()(constraint.premise) ^ irep_hash()(constraint.s0) ^
156+
irep_hash()(constraint.s1);
173157
}
174158
};
175-
176-
/// Used for debug printing.
177-
/// \param [in] expr: constraint to render
178-
/// \return rendered string
179-
inline std::string to_string(const string_not_contains_constraintt &expr)
180-
{
181-
std::ostringstream out;
182-
out << "forall x in [" << format(expr.univ_lower_bound()) << ", "
183-
<< format(expr.univ_upper_bound()) << "). " << format(expr.premise())
184-
<< " => ("
185-
<< "exists y in [" << format(expr.exists_lower_bound()) << ", "
186-
<< format(expr.exists_upper_bound()) << "). " << format(expr.s0())
187-
<< "[x+y] != " << format(expr.s1()) << "[y])";
188-
return out.str();
189-
}
190-
191-
inline const string_not_contains_constraintt
192-
&to_string_not_contains_constraint(const exprt &expr)
193-
{
194-
PRECONDITION(expr.id()==ID_string_not_contains_constraint);
195-
DATA_INVARIANT(
196-
expr.operands().size()==7,
197-
string_refinement_invariantt("string_not_contains_constraintt must have 7 "
198-
"operands"));
199-
return static_cast<const string_not_contains_constraintt &>(expr);
200-
}
201-
202-
inline string_not_contains_constraintt
203-
&to_string_not_contains_constraint(exprt &expr)
204-
{
205-
PRECONDITION(expr.id()==ID_string_not_contains_constraint);
206-
DATA_INVARIANT(
207-
expr.operands().size()==7,
208-
string_refinement_invariantt("string_not_contains_constraintt must have 7 "
209-
"operands"));
210-
return static_cast<string_not_contains_constraintt &>(expr);
211159
}
212160

213161
#endif

0 commit comments

Comments
 (0)