12 #ifndef CPROVER_UTIL_GRAPH_H 13 #define CPROVER_UTIL_GRAPH_H 33 template<
class E=empty_edget>
40 typedef std::map<node_indext, edget>
edgest;
46 in.insert(std::pair<node_indext, edget>(n,
edget()));
51 out.insert(std::pair<node_indext, edget>(n,
edget()));
91 while(it_a!=a.end() && it_b!=b.end())
132 template<
class N=graph_nodet<empty_edget> >
160 return nodes[i].out.find(j)!=
nodes[i].out.end();
185 return nodes.empty();
206 nodes[a].erase_out(b);
207 nodes[b].erase_in(a);
212 return nodes[a].out[b];
231 typedef std::list<node_indext>
patht;
252 std::vector<node_indext>
253 get_reachable(
const std::vector<node_indext> &src,
bool forwards)
const;
259 std::vector<node_indext> &subgraph_nr);
262 std::size_t
SCCs(std::vector<node_indext> &subgraph_nr)
const;
269 std::list<node_indext>
topsort()
const;
290 tarjant(std::size_t n, std::vector<node_indext> &_subgraph_nr):
308 bool non_trivial)
const;
314 assert(a<nodes.size());
315 assert(b<nodes.size());
338 nodet &node=nodes[n];
341 for(
typename edgest::const_iterator
353 nodet &node=nodes[n];
356 for(
typename edgest::const_iterator
370 bool non_trivial)
const 372 std::vector<bool> visited;
373 std::vector<unsigned> distance;
374 std::vector<unsigned> previous;
377 visited.resize(nodes.size(),
false);
378 distance.resize(nodes.size(), (unsigned)(-1));
379 previous.resize(nodes.size(), 0);
389 std::vector<node_indext> frontier_set, new_frontier_set;
391 frontier_set.reserve(nodes.size());
393 frontier_set.push_back(src);
398 while(!frontier_set.empty() && !found)
402 new_frontier_set.clear();
403 new_frontier_set.reserve(nodes.size());
405 for(
typename std::vector<node_indext>::const_iterator
406 f_it=frontier_set.begin();
407 f_it!=frontier_set.end() && !found;
411 const nodet &n=nodes[i];
414 for(
typename edgest::const_iterator
416 o_it!=n.
out.end() && !found;
430 new_frontier_set.push_back(o);
435 frontier_set.swap(new_frontier_set);
443 if(distance[dest]==(
unsigned)(-1))
448 path.push_front(dest);
449 if(distance[dest]==0 ||
450 previous[dest]==src)
break;
451 assert(dest!=previous[dest]);
459 std::vector<node_indext> reachable =
get_reachable(src,
true);
460 for(
const auto index : reachable)
461 nodes[index].visited =
true;
473 template <
class Container,
typename nodet =
typename Container::value_type>
476 const std::function<
void(
477 const typename Container::value_type &,
478 const std::function<
void(
const typename Container::value_type &)> &)>
481 std::vector<nodet>
stack;
482 for(
const auto &elt :
set)
483 stack.push_back(elt);
485 while(!
stack.empty())
487 auto n =
stack.back();
489 for_each_successor(n, [&](
const nodet &node) {
490 if(
set.insert(node).second)
491 stack.push_back(node);
502 std::vector<typename N::node_indext>
505 std::vector<node_indext> src_vector;
506 src_vector.push_back(src);
518 const std::vector<node_indext> &src,
521 std::vector<node_indext> result;
522 std::vector<bool> visited(size(),
false);
524 std::stack<node_indext, std::vector<node_indext>> s(src);
537 const auto &node = nodes[n];
538 const auto &succs = forwards ? node.out : node.in;
539 for(
const auto succ : succs)
540 if(!visited[succ.first])
549 std::vector<node_indext> &subgraph_nr)
551 std::vector<bool> visited;
553 visited.resize(nodes.size(),
false);
554 subgraph_nr.resize(nodes.size(), 0);
565 std::stack<node_indext> s;
576 const nodet &node=nodes[n];
578 for(
typename edgest::const_iterator
597 t.depth[v]=t.max_dfs;
598 t.lowlink[v]=t.max_dfs;
602 const nodet &node=nodes[v];
603 for(
typename edgest::const_iterator
612 t.lowlink[v]=std::min(t.lowlink[v], t.lowlink[vp]);
614 else if(t.in_scc[vp])
615 t.lowlink[v]=std::min(t.lowlink[v], t.depth[vp]);
619 if(t.lowlink[v]==t.depth[v])
623 assert(!t.scc_stack.empty());
627 t.subgraph_nr[vp]=t.scc_count;
651 tarjant t(nodes.size(), subgraph_nr);
671 const nodet &n=tmp[i];
675 for(
typename edgest::const_iterator
679 for(
typename edgest::const_iterator
687 this->add_undirected_edge(*it1, *it2);
702 std::list<node_indext> nodelist;
704 std::queue<node_indext> indeg0_nodes;
706 std::vector<size_t> in_deg(nodes.size(), 0);
711 in_deg[idx]=in(idx).size();
713 indeg0_nodes.push(idx);
716 while(!indeg0_nodes.empty())
720 nodelist.push_back(source);
722 for(
const auto &edge : out(source))
725 INVARIANT(in_deg[target]!=0,
"in-degree of node cannot be zero here");
730 if(in_deg[target]==0)
731 indeg0_nodes.push(target);
737 if(nodelist.size()!=nodes.size())
742 template <
typename node_index_type>
745 const std::function<
void(std::function<
void(
const node_index_type &)>)>
748 void(
const node_index_type &, std::function<
void(
const node_index_type &)>)>
750 const std::function<std::string(
const node_index_type &)> node_to_string)
752 for_each_node([&](
const node_index_type &i) {
753 for_each_succ(i, [&](
const node_index_type &n) {
754 out << node_to_string(i) <<
" -> " << node_to_string(n) <<
'\n';
760 std::vector<typename grapht<N>::node_indext>
763 std::vector<node_indext> result;
765 nodes[n].out.begin(),
767 std::back_inserter(result),
768 [&](
const std::pair<node_indext, edget> &edge) {
return edge.first; });
778 nodes[n].out.begin(),
780 [&](
const std::pair<node_indext, edget> &edge) { f(edge.first); });
786 const auto for_each_node =
787 [&](
const std::function<void(const node_indext &)> &f) {
792 const auto for_each_succ = [&](
793 const node_indext &i,
const std::function<void(const node_indext &)> &f) {
794 for_each_successor(i, f);
798 output_dot_generic<node_indext>(out, for_each_node, for_each_succ,
to_string);
801 #endif // CPROVER_UTIL_GRAPH_H void output_dot_generic(std::ostream &out, const std::function< void(std::function< void(const node_index_type &)>)> &for_each_node, const std::function< void(const node_index_type &, std::function< void(const node_index_type &)>)> &for_each_succ, const std::function< std::string(const node_index_type &)> node_to_string)
void remove_in_edges(node_indext n)
A generic directed graph with a parametric node type.
std::vector< unsigned > lowlink
std::size_t SCCs(std::vector< node_indext > &subgraph_nr) const
Computes strongly-connected components of a graph and yields a vector expressing a mapping from nodes...
void add_undirected_edge(node_indext a, node_indext b)
A node type with an extra bit.
std::size_t connected_subgraphs(std::vector< node_indext > &subgraph_nr)
void visit_reachable(node_indext src)
#define INVARIANT(CONDITION, REASON)
void shortest_path(node_indext src, node_indext dest, patht &path) const
bool has_edge(node_indext i, node_indext j) const
void remove_edges(node_indext n)
void erase_in(node_indext n)
std::vector< bool > visited
const edgest & out(node_indext n) const
std::list< path_nodet > patht
std::vector< bool > in_scc
std::list< node_indext > patht
std::list< node_indext > topsort() const
Find a topological order of the nodes if graph is DAG, return empty list for non-DAG or empty graph...
nodet::node_indext node_indext
void remove_undirected_edge(node_indext a, node_indext b)
std::vector< node_indext > get_successors(const node_indext &n) const
void add_in(node_indext n)
edget & edge(node_indext a, node_indext b)
void output_dot(std::ostream &out) const
std::map< node_indext, edget > edgest
void tarjan(class tarjant &t, node_indext v) const
void erase_out(node_indext n)
void remove_edge(node_indext a, node_indext b)
const nodet & operator[](node_indext n) const
std::vector< node_indext > & subgraph_nr
void for_each_successor(const node_indext &n, std::function< void(const node_indext &)> f) const
void remove_out_edges(node_indext n)
std::stack< node_indext > scc_stack
void shortest_loop(node_indext node, patht &path) const
std::string to_string(const string_constraintt &expr)
Used for debug printing.
void add_edge(node_indext a, node_indext b)
std::vector< unsigned > depth
void add_out(node_indext n)
const edgest & in(node_indext n) const
void intersection(const typename graph_nodet< E >::edgest &a, const typename graph_nodet< E >::edgest &b, typename graph_nodet< E >::edgest &dest)
Compute intersection of two edge sets, in linear time.
std::vector< nodet > nodest
tarjant(std::size_t n, std::vector< node_indext > &_subgraph_nr)
void resize(node_indext s)
nodet & operator[](node_indext n)
graph_nodet< E >::edgest edgest
This class represents a node in a directed graph.
graph_nodet< E >::edget edget
std::vector< node_indext > get_reachable(node_indext src, bool forwards) const
Run depth-first search on the graph, starting from a single source node.
void get_reachable(Container &set, const std::function< void(const typename Container::value_type &, const std::function< void(const typename Container::value_type &)> &)> &for_each_successor)
Add to set, nodes that are reachable from set.