Skip to content

Commit 15131da

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 names 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 64ec195 commit 15131da

File tree

8 files changed

+178
-198
lines changed

8 files changed

+178
-198
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: 37 additions & 85 deletions
Original file line numberDiff line numberDiff line change
@@ -104,7 +104,7 @@ class string_constraintt final
104104
};
105105

106106
/// Used for debug printing.
107-
/// \param [in] expr: constraint to render
107+
/// \param expr: constraint to render
108108
/// \return rendered string
109109
inline std::string to_string(const string_constraintt &expr)
110110
{
@@ -116,98 +116,50 @@ 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 formulas of the form:
120+
/// ```
121+
/// forall x in [univ_lower_bound, univ_upper_bound[.
122+
/// premise(x) =>
123+
/// exists y in [exists_lower_bound, exists_upper_bound[. s0[x+y] != s1[y]
124+
/// ```
125+
struct string_not_contains_constraintt
120126
{
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-
};
139-
140-
const exprt &univ_lower_bound() const
141-
{
142-
return op0();
143-
}
144-
145-
const exprt &univ_upper_bound() const
146-
{
147-
return op1();
148-
}
149-
150-
const exprt &premise() const
151-
{
152-
return op2();
153-
}
127+
exprt univ_lower_bound;
128+
exprt univ_upper_bound;
129+
exprt premise;
130+
exprt exists_lower_bound;
131+
exprt exists_upper_bound;
132+
array_string_exprt s0;
133+
array_string_exprt s1;
134+
};
154135

155-
const exprt &exists_lower_bound() const
156-
{
157-
return op3();
158-
}
136+
std::string to_string(const string_not_contains_constraintt &expr);
159137

160-
const exprt &exists_upper_bound() const
161-
{
162-
return operands()[4];
163-
}
138+
void replace(
139+
const union_find_replacet &replace_map,
140+
string_not_contains_constraintt &constraint);
164141

165-
const array_string_exprt &s0() const
166-
{
167-
return to_array_string_expr(operands()[5]);
168-
}
142+
bool operator==(
143+
const string_not_contains_constraintt &left,
144+
const string_not_contains_constraintt &right);
169145

170-
const array_string_exprt &s1() const
146+
// NOLINTNEXTLINE [allow specialization within 'std']
147+
namespace std
148+
{
149+
template <>
150+
// NOLINTNEXTLINE [struct identifier 'hash' does not end in t]
151+
struct hash<string_not_contains_constraintt>
152+
{
153+
size_t operator()(const string_not_contains_constraintt &constraint) const
171154
{
172-
return to_array_string_expr(operands()[6]);
155+
return irep_hash()(constraint.univ_lower_bound) ^
156+
irep_hash()(constraint.univ_upper_bound) ^
157+
irep_hash()(constraint.exists_lower_bound) ^
158+
irep_hash()(constraint.exists_upper_bound) ^
159+
irep_hash()(constraint.premise) ^ irep_hash()(constraint.s0) ^
160+
irep_hash()(constraint.s1);
173161
}
174162
};
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);
211163
}
212164

213165
#endif

0 commit comments

Comments
 (0)