Skip to content

Commit 4badd8f

Browse files
committed
Add useful functions to class_hierarchy_grapht
class_hierarchy_grapht is a more advanced representation of the class hierarchy than class_hierarchyt. So ideally we want to migrate all functions from the old version to the graph-based representation. This commit does this for the functions get_parents_trans, get_children_trans, and introduces a new function get_direct_children.
1 parent 6566d10 commit 4badd8f

File tree

2 files changed

+78
-1
lines changed

2 files changed

+78
-1
lines changed

src/goto-programs/class_hierarchy.cpp

+66-1
Original file line numberDiff line numberDiff line change
@@ -13,6 +13,7 @@ Date: April 2016
1313

1414
#include "class_hierarchy.h"
1515

16+
#include <iterator>
1617
#include <ostream>
1718

1819
#include <util/json_stream.h>
@@ -88,6 +89,70 @@ void class_hierarchy_grapht::populate(const symbol_tablet &symbol_table)
8889
}
8990
}
9091

92+
/// Helper function that converts a vector of node_indext to a vector of ids
93+
/// that are stored in the corresponding nodes in the graph.
94+
class_hierarchy_grapht::idst class_hierarchy_grapht::ids_from_indices(
95+
const std::vector<node_indext> &node_indices) const
96+
{
97+
idst result;
98+
std::transform(
99+
node_indices.begin(),
100+
node_indices.end(),
101+
back_inserter(result),
102+
[&](const node_indext &node_index) {
103+
return (*this)[node_index].class_identifier;
104+
});
105+
return result;
106+
}
107+
108+
/// Get all the classes that directly (i.e. in one step) inherit from class c.
109+
/// \param c: The class to consider
110+
/// \return A list containing ids of all direct children of c.
111+
class_hierarchy_grapht::idst
112+
class_hierarchy_grapht::get_direct_children(const irep_idt &c) const
113+
{
114+
const node_indext &node_index = nodes_by_name.at(c);
115+
const auto &child_indices = get_successors(node_index);
116+
return ids_from_indices(child_indices);
117+
}
118+
119+
/// Helper function for `get_children_trans` and `get_parents_trans`
120+
class_hierarchy_grapht::idst class_hierarchy_grapht::get_other_reachable_ids(
121+
const irep_idt &c,
122+
bool forwards) const
123+
{
124+
idst direct_child_ids;
125+
const node_indext &node_index = nodes_by_name.at(c);
126+
const auto &reachable_indices = get_reachable(node_index, forwards);
127+
auto reachable_ids = ids_from_indices(reachable_indices);
128+
// Remove c itself from the list
129+
// TODO Adding it first and then removing it is not ideal. It would be
130+
// better to define a function grapht::get_other_reachable and directly use
131+
// that here.
132+
reachable_ids.erase(
133+
std::remove(reachable_ids.begin(), reachable_ids.end(), c),
134+
reachable_ids.end());
135+
return reachable_ids;
136+
}
137+
138+
/// Get all the classes that inherit (directly or indirectly) from class c.
139+
/// \param c: The class to consider
140+
/// \return A list containing ids of all classes that eventually inherit from c.
141+
class_hierarchy_grapht::idst
142+
class_hierarchy_grapht::get_children_trans(const irep_idt &c) const
143+
{
144+
return get_other_reachable_ids(c, true);
145+
}
146+
147+
/// Get all the classes that class c inherits from (directly or indirectly).
148+
/// \param c: The class to consider
149+
/// \return A list of class ids that c eventually inherits from.
150+
class_hierarchy_grapht::idst
151+
class_hierarchy_grapht::get_parents_trans(const irep_idt &c) const
152+
{
153+
return get_other_reachable_ids(c, false);
154+
}
155+
91156
void class_hierarchyt::get_children_trans_rec(
92157
const irep_idt &c,
93158
idst &dest) const
@@ -105,7 +170,7 @@ void class_hierarchyt::get_children_trans_rec(
105170
get_children_trans_rec(child, dest);
106171
}
107172

108-
/// Get all the classes that inherit (directly or indirectly) from class c. The
173+
/// Get all the classes that class c inherits from (directly or indirectly). The
109174
/// first element(s) will be the immediate parents of c, though after this
110175
/// the order is all the parents of the first immediate parent
111176
/// \param c: The class to consider

src/goto-programs/class_hierarchy.h

+12
Original file line numberDiff line numberDiff line change
@@ -89,6 +89,8 @@ class class_hierarchy_graph_nodet : public graph_nodet<empty_edget>
8989
class class_hierarchy_grapht : public grapht<class_hierarchy_graph_nodet>
9090
{
9191
public:
92+
typedef std::vector<irep_idt> idst;
93+
9294
/// Maps class identifiers onto node indices
9395
typedef std::unordered_map<irep_idt, node_indext> nodes_by_namet;
9496

@@ -101,9 +103,19 @@ class class_hierarchy_grapht : public grapht<class_hierarchy_graph_nodet>
101103
return nodes_by_name;
102104
}
103105

106+
idst get_direct_children(const irep_idt &c) const;
107+
108+
idst get_children_trans(const irep_idt &c) const;
109+
110+
idst get_parents_trans(const irep_idt &c) const;
111+
104112
private:
105113
/// Maps class identifiers onto node indices
106114
nodes_by_namet nodes_by_name;
115+
116+
idst ids_from_indices(const std::vector<node_indext> &nodes) const;
117+
118+
idst get_other_reachable_ids(const irep_idt &c, bool forwards) const;
107119
};
108120

109121
/// Output the class hierarchy

0 commit comments

Comments
 (0)