Skip to content

Commit e308bad

Browse files
romainbrenguierromainbrenguier
committed
Rename class to string_dependenciest
1 parent 06dc6b2 commit e308bad

File tree

4 files changed

+35
-35
lines changed

4 files changed

+35
-35
lines changed

‎src/solvers/refinement/string_refinement.cpp

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -680,12 +680,12 @@ decision_proceduret::resultt string_refinementt::dec_solve()
680680
#ifdef DEBUG
681681
output_equations(debug(), equations, ns);
682682

683-
string_dependencest dependences;
683+
string_dependenciest dependencies;
684684
for(const equal_exprt &eq : equations)
685-
add_node(dependences, eq, generator.array_pool);
685+
add_node(dependencies, eq, generator.array_pool);
686686

687687
debug() << "dec_solve: dependence graph:" << eom;
688-
dependences.output_dot(debug());
688+
dependencies.output_dot(debug());
689689
#endif
690690

691691
debug() << "dec_solve: Replace function applications" << eom;

‎src/solvers/refinement/string_refinement_util.cpp

Lines changed: 24 additions & 24 deletions
Original file line numberDiff line numberDiff line change
@@ -322,8 +322,8 @@ static std::unique_ptr<string_builtin_functiont> to_string_builtin_function(
322322
return {};
323323
}
324324

325-
string_dependencest::string_nodet &
326-
string_dependencest::get_node(const array_string_exprt &e)
325+
string_dependenciest::string_nodet &
326+
string_dependenciest::get_node(const array_string_exprt &e)
327327
{
328328
auto entry_inserted = node_index_pool.emplace(e, string_nodes.size());
329329
if(!entry_inserted.second)
@@ -333,7 +333,7 @@ string_dependencest::get_node(const array_string_exprt &e)
333333
return string_nodes.back();
334334
}
335335

336-
string_dependencest::builtin_function_nodet string_dependencest::make_node(
336+
string_dependenciest::builtin_function_nodet string_dependenciest::make_node(
337337
std::unique_ptr<string_builtin_functiont> &builtin_function)
338338
{
339339
const builtin_function_nodet builtin_function_node(
@@ -343,36 +343,36 @@ string_dependencest::builtin_function_nodet string_dependencest::make_node(
343343
return builtin_function_node;
344344
}
345345

346-
const string_builtin_functiont &string_dependencest::get_builtin_function(
346+
const string_builtin_functiont &string_dependenciest::get_builtin_function(
347347
const builtin_function_nodet &node) const
348348
{
349349
PRECONDITION(node.index < builtin_function_nodes.size());
350350
return *(builtin_function_nodes[node.index]);
351351
}
352352

353-
const std::vector<string_dependencest::builtin_function_nodet> &
354-
string_dependencest::dependencies(
355-
const string_dependencest::string_nodet &node) const
353+
const std::vector<string_dependenciest::builtin_function_nodet> &
354+
string_dependenciest::dependencies(
355+
const string_dependenciest::string_nodet &node) const
356356
{
357357
return node.dependencies;
358358
}
359359

360-
void string_dependencest::add_dependency(
360+
void string_dependenciest::add_dependency(
361361
const array_string_exprt &e,
362362
const builtin_function_nodet &builtin_function_node)
363363
{
364364
string_nodet &string_node = get_node(e);
365365
string_node.dependencies.push_back(builtin_function_node);
366366
}
367367

368-
void string_dependencest::add_unknown_dependency(const array_string_exprt &e)
368+
void string_dependenciest::add_unknown_dependency(const array_string_exprt &e)
369369
{
370370
string_nodet &string_node = get_node(e);
371371
string_node.depends_on_unknown_builtin_function = true;
372372
}
373373

374374
static void add_unknown_dependency_to_string_subexprs(
375-
string_dependencest &dependencies,
375+
string_dependenciest &dependencies,
376376
const function_application_exprt &fun_app,
377377
array_poolt &array_pool)
378378
{
@@ -392,9 +392,9 @@ static void add_unknown_dependency_to_string_subexprs(
392392
}
393393

394394
static void add_dependency_to_string_subexprs(
395-
string_dependencest &dependencies,
395+
string_dependenciest &dependencies,
396396
const function_application_exprt &fun_app,
397-
const string_dependencest::builtin_function_nodet &builtin_function_node,
397+
const string_dependenciest::builtin_function_nodet &builtin_function_node,
398398
array_poolt &array_pool)
399399
{
400400
PRECONDITION(fun_app.arguments()[0].type().id() != ID_pointer);
@@ -424,7 +424,7 @@ static void add_dependency_to_string_subexprs(
424424
}
425425
}
426426

427-
string_dependencest::node_indext string_dependencest::size() const
427+
string_dependenciest::node_indext string_dependenciest::size() const
428428
{
429429
return builtin_function_nodes.size() + string_nodes.size();
430430
}
@@ -444,36 +444,36 @@ builtin_function_index_to_node_index(const std::size_t builtin_index)
444444
return 2 * builtin_index;
445445
}
446446

447-
string_dependencest::node_indext
448-
string_dependencest::node_index(const builtin_function_nodet &n) const
447+
string_dependenciest::node_indext
448+
string_dependenciest::node_index(const builtin_function_nodet &n) const
449449
{
450450
return builtin_function_index_to_node_index(n.index);
451451
}
452452

453-
string_dependencest::node_indext
454-
string_dependencest::node_index(const array_string_exprt &s) const
453+
string_dependenciest::node_indext
454+
string_dependenciest::node_index(const array_string_exprt &s) const
455455
{
456456
return string_index_to_node_index(node_index_pool.at(s));
457457
}
458458

459-
optionalt<string_dependencest::builtin_function_nodet>
460-
string_dependencest::get_builtin_function_node(node_indext i) const
459+
optionalt<string_dependenciest::builtin_function_nodet>
460+
string_dependenciest::get_builtin_function_node(node_indext i) const
461461
{
462462
if(i % 2 == 0)
463463
return builtin_function_nodet(i / 2);
464464
return {};
465465
}
466466

467-
optionalt<string_dependencest::string_nodet>
468-
string_dependencest::get_string_node(node_indext i) const
467+
optionalt<string_dependenciest::string_nodet>
468+
string_dependenciest::get_string_node(node_indext i) const
469469
{
470470
if(i % 2 == 1 && i / 2 < string_nodes.size())
471471
return string_nodes[i / 2];
472472
return {};
473473
}
474474

475475
bool add_node(
476-
string_dependencest &dependencies,
476+
string_dependenciest &dependencies,
477477
const equal_exprt &equation,
478478
array_poolt &array_pool)
479479
{
@@ -505,7 +505,7 @@ bool add_node(
505505
return true;
506506
}
507507

508-
void string_dependencest::for_each_successor(
508+
void string_dependenciest::for_each_successor(
509509
const std::size_t &i,
510510
const std::function<void(const std::size_t &)> &f) const
511511
{
@@ -529,7 +529,7 @@ void string_dependencest::for_each_successor(
529529
UNREACHABLE;
530530
}
531531

532-
void string_dependencest::output_dot(std::ostream &stream) const
532+
void string_dependenciest::output_dot(std::ostream &stream) const
533533
{
534534
const auto for_each_node =
535535
[&](const std::function<void(const std::size_t &)> &f) { // NOLINT

‎src/solvers/refinement/string_refinement_util.h

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -259,9 +259,9 @@ class string_test_builtin_functiont : public string_builtin_functiont
259259
};
260260

261261
/// Keep track of dependencies between strings.
262-
/// Each string points to builtin_function calls on which it depends,
263-
/// each builtin_function points to the strings on which the result depend.
264-
class string_dependencest
262+
/// Each string points to the builtin_function calls on which it depends.
263+
/// Each builtin_function points to the strings on which the result depends.
264+
class string_dependenciest
265265
{
266266
public:
267267
/// A builtin_function node is just an index in the `builtin_function_nodes`
@@ -365,7 +365,7 @@ class string_dependencest
365365
/// the right hand side is not a function application
366366
/// \todo there should be a class with just the three functions we require here
367367
bool add_node(
368-
string_dependencest &dependencies,
368+
string_dependenciest &dependencies,
369369
const equal_exprt &equation,
370370
array_poolt &array_pool);
371371

‎unit/solvers/refinement/string_refinement/dependency_graph.cpp

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -47,7 +47,7 @@ SCENARIO("dependency_graph", "[core][solvers][refinement][string_refinement]")
4747
{
4848
GIVEN("dependency graph")
4949
{
50-
string_dependencest dependences;
50+
string_dependenciest dependences;
5151
refined_string_typet string_type(java_char_type(), java_int_type());
5252
const exprt string1 = make_string_argument("string1");
5353
const exprt string2 = make_string_argument("string2");
@@ -142,7 +142,7 @@ SCENARIO("dependency_graph", "[core][solvers][refinement][string_refinement]")
142142
THEN("string3 depends on primitive0")
143143
{
144144
const auto &node = dependences.get_node(char_array3);
145-
const std::vector<string_dependencest::builtin_function_nodet>
145+
const std::vector<string_dependenciest::builtin_function_nodet>
146146
&depends = dependences.dependencies(node);
147147
REQUIRE(depends.size() == 1);
148148
const auto &primitive0 = dependences.get_builtin_function(depends[0]);
@@ -159,7 +159,7 @@ SCENARIO("dependency_graph", "[core][solvers][refinement][string_refinement]")
159159
THEN("string5 depends on primitive1")
160160
{
161161
const auto &node = dependences.get_node(char_array5);
162-
const std::vector<string_dependencest::builtin_function_nodet>
162+
const std::vector<string_dependenciest::builtin_function_nodet>
163163
&depends = dependences.dependencies(node);
164164
REQUIRE(depends.size() == 1);
165165
const auto &primitive1 = dependences.get_builtin_function(depends[0]);
@@ -176,7 +176,7 @@ SCENARIO("dependency_graph", "[core][solvers][refinement][string_refinement]")
176176
THEN("string6 depends on primitive2")
177177
{
178178
const auto &node = dependences.get_node(char_array6);
179-
const std::vector<string_dependencest::builtin_function_nodet>
179+
const std::vector<string_dependenciest::builtin_function_nodet>
180180
&depends = dependences.dependencies(node);
181181
REQUIRE(depends.size() == 1);
182182
const auto &primitive2 = dependences.get_builtin_function(depends[0]);

0 commit comments

Comments
 (0)