Skip to content

Commit ceb97c9

Browse files
Define function template for output_dot
This makes output_dot more reusable as we don't have to inherit from grapht to use it.
1 parent 27d9bc1 commit ceb97c9

File tree

1 file changed

+48
-12
lines changed

1 file changed

+48
-12
lines changed

src/util/graph.h

Lines changed: 48 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -20,6 +20,7 @@ Author: Daniel Kroening, [email protected]
2020
#include <cassert>
2121
#include <algorithm>
2222
#include <queue>
23+
#include <functional>
2324

2425
#include "invariant.h"
2526

@@ -264,8 +265,12 @@ class grapht
264265

265266
std::list<node_indext> topsort() const;
266267

268+
std::vector<node_indext> get_successors(const node_indext &n) const;
267269
void output_dot(std::ostream &out) const;
268270
void output_dot_node(std::ostream &out, node_indext n) const;
271+
void for_each_successor(
272+
const node_indext &n,
273+
std::function<void(const node_indext &)> f) const;
269274

270275
protected:
271276
class tarjant
@@ -668,23 +673,54 @@ std::list<typename grapht<N>::node_indext> grapht<N>::topsort() const
668673
return nodelist;
669674
}
670675

671-
template<class N>
672-
void grapht<N>::output_dot(std::ostream &out) const
676+
template <typename node_index_type>
677+
void output_dot_generic(
678+
std::ostream &out,
679+
node_index_type size,
680+
const std::function<
681+
void(const node_index_type &, std::function<void(const node_index_type &)>)>
682+
&for_each_succ)
673683
{
674-
for(node_indext n=0; n<nodes.size(); n++)
675-
output_dot_node(out, n);
684+
for(node_index_type i = 0; i < size; ++i)
685+
for_each_succ(
686+
i, [&](const node_index_type &n) { out << i << " -> " << n << '\n'; });
676687
}
677688

678-
template<class N>
679-
void grapht<N>::output_dot_node(std::ostream &out, node_indext n) const
689+
template <class N>
690+
std::vector<typename grapht<N>::node_indext>
691+
grapht<N>::get_successors(const node_indext &n) const
680692
{
681-
const nodet &node=nodes[n];
693+
std::vector<node_indext> result;
694+
std::transform(
695+
nodes[n].out.begin(),
696+
nodes[n].out.end(),
697+
std::back_inserter(result),
698+
[&](const std::pair<node_indext, edget> &edge) { return edge.first; });
699+
return result;
700+
}
682701

683-
for(typename edgest::const_iterator
684-
it=node.out.begin();
685-
it!=node.out.end();
686-
it++)
687-
out << n << " -> " << it->first << '\n';
702+
template <class N>
703+
void grapht<N>::for_each_successor(
704+
const node_indext &n,
705+
std::function<void(const node_indext &)> f) const
706+
{
707+
std::for_each(
708+
nodes[n].out.begin(),
709+
nodes[n].out.end(),
710+
[&](const std::pair<node_indext, edget> &edge) { f(edge.first); });
711+
}
712+
713+
template <class N>
714+
void grapht<N>::output_dot(std::ostream &out) const
715+
{
716+
output_dot_generic<node_indext>(
717+
out,
718+
(node_indext)nodes.size(),
719+
[&](
720+
const node_indext &i,
721+
const std::function<void(const node_indext &)> &f) { // NOLINT
722+
for_each_successor(i, f);
723+
});
688724
}
689725

690726
#endif // CPROVER_UTIL_GRAPH_H

0 commit comments

Comments
 (0)