Skip to content

Commit 49429eb

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 49429eb

File tree

2 files changed

+69
-1
lines changed

2 files changed

+69
-1
lines changed

src/goto-programs/class_hierarchy.cpp

+57-1
Original file line numberDiff line numberDiff line change
@@ -88,6 +88,62 @@ void class_hierarchy_grapht::populate(const symbol_tablet &symbol_table)
8888
}
8989
}
9090

91+
/// Helper function that converts a vector of node_indext to a vector of ids
92+
/// that are stored in the corresponding nodes in the graph.
93+
class_hierarchy_grapht::idst class_hierarchy_grapht::ids_from_indices(
94+
const std::vector<node_indext> &nodes) const
95+
{
96+
idst result;
97+
std::transform(
98+
nodes.begin(),
99+
nodes.end(),
100+
std::back_inserter(result),
101+
[&](const node_indext &node_index) {
102+
return (*this)[node_index].class_identifier;
103+
});
104+
return result;
105+
}
106+
107+
/// Get all the classes that directly (i.e. in one step) inherit from class c.
108+
/// \param c: The class to consider
109+
/// \return A list containing ids of all direct children of c.
110+
class_hierarchy_grapht::idst
111+
class_hierarchy_grapht::get_direct_children(const irep_idt &c) const
112+
{
113+
const node_indext &node_index = nodes_by_name.at(c);
114+
const auto &child_indices = get_successors(node_index);
115+
return ids_from_indices(child_indices);
116+
}
117+
118+
/// Helper function for `get_children_trans` and `get_parents_trans`
119+
class_hierarchy_grapht::idst class_hierarchy_grapht::get_reachable_ids(
120+
const irep_idt &c,
121+
bool forwards) const
122+
{
123+
idst direct_child_ids;
124+
const node_indext &node_index = nodes_by_name.at(c);
125+
const auto &reachable_indices = get_reachable(node_index, forwards);
126+
return ids_from_indices(reachable_indices);
127+
}
128+
129+
/// Get all the classes that inherit (directly or indirectly) from class c.
130+
/// \param c: The class to consider
131+
/// \return A list containing ids of all classes that eventually inherit from c.
132+
class_hierarchy_grapht::idst
133+
class_hierarchy_grapht::get_children_trans(const irep_idt &c) const
134+
{
135+
return get_reachable_ids(c, true);
136+
}
137+
138+
/// Get all the classes that class c inherits from (directly or indirectly).
139+
/// \param c: The class to consider
140+
/// \return A list of class ids that c eventually inherits from.
141+
class_hierarchy_grapht::idst
142+
class_hierarchy_grapht::get_parents_trans(const irep_idt &c) const
143+
{
144+
return get_reachable_ids(c, false);
145+
}
146+
91147
void class_hierarchyt::get_children_trans_rec(
92148
const irep_idt &c,
93149
idst &dest) const
@@ -105,7 +161,7 @@ void class_hierarchyt::get_children_trans_rec(
105161
get_children_trans_rec(child, dest);
106162
}
107163

108-
/// Get all the classes that inherit (directly or indirectly) from class c. The
164+
/// Get all the classes that class c inherits from (directly or indirectly). The
109165
/// first element(s) will be the immediate parents of c, though after this
110166
/// the order is all the parents of the first immediate parent
111167
/// \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_reachable_ids(const irep_idt &c, bool forwards) const;
107119
};
108120

109121
/// Output the class hierarchy

0 commit comments

Comments
 (0)