Skip to content

Commit bd8ee51

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 0b58e31 commit bd8ee51

File tree

1 file changed

+58
-13
lines changed

1 file changed

+58
-13
lines changed

src/util/graph.h

Lines changed: 58 additions & 13 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,11 @@ 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;
268-
void output_dot_node(std::ostream &out, node_indext n) const;
270+
void for_each_successor(
271+
const node_indext &n,
272+
std::function<void(const node_indext &)> f) const;
269273

270274
protected:
271275
class tarjant
@@ -668,23 +672,64 @@ std::list<typename grapht<N>::node_indext> grapht<N>::topsort() const
668672
return nodelist;
669673
}
670674

671-
template<class N>
672-
void grapht<N>::output_dot(std::ostream &out) const
675+
template <typename node_index_type>
676+
void output_dot_generic(
677+
std::ostream &out,
678+
const std::function<void(std::function<void(const node_index_type &)>)>
679+
&for_each_node,
680+
const std::function<
681+
void(const node_index_type &, std::function<void(const node_index_type &)>)>
682+
&for_each_succ,
683+
const std::function<std::string(const node_index_type &)> node_to_string)
673684
{
674-
for(node_indext n=0; n<nodes.size(); n++)
675-
output_dot_node(out, n);
685+
for_each_node([&](const node_index_type &i) { // NOLINT
686+
for_each_succ(i, [&](const node_index_type &n) { // NOLINT
687+
out << node_to_string(i) << " -> " << node_to_string(n) << '\n';
688+
});
689+
});
676690
}
677691

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

683-
for(typename edgest::const_iterator
684-
it=node.out.begin();
685-
it!=node.out.end();
686-
it++)
687-
out << n << " -> " << it->first << '\n';
705+
template <class N>
706+
void grapht<N>::for_each_successor(
707+
const node_indext &n,
708+
std::function<void(const node_indext &)> f) const
709+
{
710+
std::for_each(
711+
nodes[n].out.begin(),
712+
nodes[n].out.end(),
713+
[&](const std::pair<node_indext, edget> &edge) { f(edge.first); });
714+
}
715+
716+
template <class N>
717+
void grapht<N>::output_dot(std::ostream &out) const
718+
{
719+
const auto for_each_node =
720+
[&](const std::function<void(const node_indext &)> &f) { // NOLINT
721+
for(node_indext i = 0; i < nodes.size(); ++i)
722+
f(i);
723+
};
724+
725+
const auto for_each_succ = [&](
726+
const node_indext &i,
727+
const std::function<void(const node_indext &)> &f) { // NOLINT
728+
for_each_successor(i, f);
729+
};
730+
731+
const auto to_string = [](const node_indext &i) { return std::to_string(i); };
732+
output_dot_generic<node_indext>(out, for_each_node, for_each_succ, to_string);
688733
}
689734

690735
#endif // CPROVER_UTIL_GRAPH_H

0 commit comments

Comments
 (0)