Skip to content

Commit cd5daab

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 cd5daab

File tree

2 files changed

+72
-1
lines changed

2 files changed

+72
-1
lines changed

src/goto-programs/class_hierarchy.cpp

Lines changed: 60 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -88,6 +88,65 @@ 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
94+
class_hierarchy_grapht::ids_from_indices(const std::vector<node_indext>
95+
&nodes) const
96+
{
97+
idst result;
98+
std::transform(
99+
nodes.begin(),
100+
nodes.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
121+
class_hierarchy_grapht::get_reachable_ids(const irep_idt &c, bool forwards)
122+
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+
return ids_from_indices(reachable_indices);
128+
}
129+
130+
/// Get all the classes that inherit (directly or indirectly) from class c.
131+
/// \param c: The class to consider
132+
/// \param [out] dest: A list containing ids of all classes that eventually
133+
/// inherit from c.
134+
class_hierarchy_grapht::idst
135+
class_hierarchy_grapht::get_children_trans(const irep_idt &c) const
136+
{
137+
return get_reachable_ids(c, true);
138+
}
139+
140+
141+
/// Get all the classes that class c inherits from (directly or indirectly).
142+
/// \param c: The class to consider
143+
/// \param [out] dest: A list of class ids that c eventually inherits from.
144+
class_hierarchy_grapht::idst
145+
class_hierarchy_grapht::get_parents_trans(const irep_idt &c) const
146+
{
147+
return get_reachable_ids(c, false);
148+
}
149+
91150
void class_hierarchyt::get_children_trans_rec(
92151
const irep_idt &c,
93152
idst &dest) const
@@ -105,7 +164,7 @@ void class_hierarchyt::get_children_trans_rec(
105164
get_children_trans_rec(child, dest);
106165
}
107166

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

src/goto-programs/class_hierarchy.h

Lines changed: 12 additions & 0 deletions
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)