Skip to content

Commit 5b47a4d

Browse files
romainbrenguierromainbrenguier
authored
Merge pull request #3256 from romainbrenguier/refactor/string-not-constains-struct
Make string_not_contains_constraintt a struct
2 parents 8ba1734 + 14057f5 commit 5b47a4d

9 files changed

+178
-199
lines changed

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

+50-65
Original file line numberDiff line numberDiff line change
@@ -200,7 +200,7 @@ SCENARIO("instantiate_not_contains",
200200

201201
std::string axioms;
202202
std::vector<string_not_contains_constraintt> nc_axioms;
203-
std::map<string_not_contains_constraintt, symbol_exprt> witnesses;
203+
std::unordered_map<string_not_contains_constraintt, symbol_exprt> witnesses;
204204

205205
std::accumulate(
206206
constraints.universal.begin(),
@@ -216,12 +216,12 @@ SCENARIO("instantiate_not_contains",
216216
constraints.not_contains.end(),
217217
axioms,
218218
[&](const std::string &accu, string_not_contains_constraintt sc) {
219-
simplify(sc, ns);
219+
simplify(sc.premise, ns);
220+
simplify(sc.s0, ns);
221+
simplify(sc.s1, ns);
220222
witnesses[sc] = generator.fresh_symbol("w", t.witness_type());
221223
nc_axioms.push_back(sc);
222-
std::string s;
223-
java_lang->from_expr(sc, s, ns);
224-
return accu + s + "\n\n";
224+
return accu + to_string(sc) + "\n\n";
225225
});
226226

227227
axioms = std::accumulate(
@@ -280,26 +280,23 @@ SCENARIO("instantiate_not_contains",
280280
// { .=1, .={ (char)'a' } }[x+y] != { .=1, .={ (char)'b' } }[y]
281281
// )
282282
// which is vacuously true.
283-
string_not_contains_constraintt vacuous(
284-
from_integer(0),
285-
from_integer(0),
286-
true_exprt(),
287-
from_integer(0),
288-
from_integer(1),
289-
a_array,
290-
a_array);
283+
const string_not_contains_constraintt vacuous = {from_integer(0),
284+
from_integer(0),
285+
true_exprt(),
286+
from_integer(0),
287+
from_integer(1),
288+
a_array,
289+
a_array};
291290

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

299298
INFO("Original axiom:\n");
300-
std::string s;
301-
java_lang->from_expr(vacuous, s, ns);
302-
INFO(s + "\n\n");
299+
INFO(to_string(vacuous) + "\n\n");
303300

304301
WHEN("we instantiate and simplify")
305302
{
@@ -335,26 +332,23 @@ SCENARIO("instantiate_not_contains",
335332
// { .=1, .={ (char)'a' } }[x+y] != { .=1, .={ (char)'b' } }[y]
336333
// )
337334
// which is false.
338-
string_not_contains_constraintt trivial(
339-
from_integer(0),
340-
from_integer(1),
341-
true_exprt(),
342-
from_integer(0),
343-
from_integer(0),
344-
a_array,
345-
b_array);
335+
const string_not_contains_constraintt trivial = {from_integer(0),
336+
from_integer(1),
337+
true_exprt(),
338+
from_integer(0),
339+
from_integer(0),
340+
a_array,
341+
b_array};
346342

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

354350
INFO("Original axiom:\n");
355-
std::string s;
356-
java_lang->from_expr(trivial, s, ns);
357-
INFO(s + "\n\n");
351+
INFO(to_string(trivial) + "\n\n");
358352

359353
WHEN("we instantiate and simplify")
360354
{
@@ -391,26 +385,23 @@ SCENARIO("instantiate_not_contains",
391385
// { .=1, .={ (char)'a' } }[x+y] != { .=0, .={ } }[y]
392386
// )
393387
// which is false.
394-
string_not_contains_constraintt trivial(
395-
from_integer(0),
396-
from_integer(1),
397-
true_exprt(),
398-
from_integer(0),
399-
from_integer(0),
400-
a_array,
401-
empty_array);
388+
const string_not_contains_constraintt trivial = {from_integer(0),
389+
from_integer(1),
390+
true_exprt(),
391+
from_integer(0),
392+
from_integer(0),
393+
a_array,
394+
empty_array};
402395

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

410403
INFO("Original axiom:\n");
411-
std::string s;
412-
java_lang->from_expr(trivial, s, ns);
413-
INFO(s + "\n\n");
404+
INFO(to_string(trivial) + "\n\n");
414405

415406
WHEN("we instantiate and simplify")
416407
{
@@ -449,27 +440,24 @@ SCENARIO("instantiate_not_contains",
449440
// { .=2, .={ (char)'a', (char)'b'}[y]
450441
// )
451442
// which is false (for x = 0).
452-
string_not_contains_constraintt trivial(
453-
from_integer(0),
454-
from_integer(2),
455-
true_exprt(),
456-
from_integer(0),
457-
from_integer(2),
458-
ab_array,
459-
ab_array);
443+
const string_not_contains_constraintt trivial = {from_integer(0),
444+
from_integer(2),
445+
true_exprt(),
446+
from_integer(0),
447+
from_integer(2),
448+
ab_array,
449+
ab_array};
460450

461451
// Create witness for axiom
462452
symbol_tablet symtab;
463453
const namespacet empty_ns(symtab);
464454

465455
string_constraint_generatort generator(ns);
466-
std::map<string_not_contains_constraintt, symbol_exprt> witnesses;
456+
std::unordered_map<string_not_contains_constraintt, symbol_exprt> witnesses;
467457
witnesses[trivial] = generator.fresh_symbol("w", t.witness_type());
468458

469459
INFO("Original axiom:\n");
470-
std::string s;
471-
java_lang->from_expr(trivial, s, ns);
472-
INFO(s + "\n\n");
460+
INFO(to_string(trivial) + "\n\n");
473461

474462
WHEN("we instantiate and simplify")
475463
{
@@ -506,26 +494,23 @@ SCENARIO("instantiate_not_contains",
506494
// { .=2, .={ (char)'a', (char)'b'}[y]
507495
// )
508496
// which is true.
509-
string_not_contains_constraintt trivial(
510-
from_integer(0),
511-
from_integer(2),
512-
true_exprt(),
513-
from_integer(0),
514-
from_integer(2),
515-
ab_array,
516-
cd_array);
497+
const string_not_contains_constraintt trivial = {from_integer(0),
498+
from_integer(2),
499+
true_exprt(),
500+
from_integer(0),
501+
from_integer(2),
502+
ab_array,
503+
cd_array};
517504

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

525512
INFO("Original axiom:\n");
526-
std::string s;
527-
java_lang->from_expr(trivial, s, ns);
528-
INFO(s + "\n\n");
513+
INFO(to_string(trivial) + "\n\n");
529514

530515
WHEN("we instantiate and simplify")
531516
{

‎src/solvers/refinement/string_constraint.cpp

+40
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

+37-85
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)