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()));
124 while(it_a!=a.end() && it_b!=b.end())
165 template<
class N=graph_nodet<empty_edget> >
179 template <
typename... arguments>
183 nodes.emplace_back(std::forward<arguments>(values)...);
194 return nodes[i].out.find(j)!=
nodes[i].out.end();
219 return nodes.empty();
240 nodes[a].erase_out(b);
241 nodes[b].erase_in(a);
246 return nodes[a].out[b];
265 typedef std::list<node_indext>
patht;
286 std::vector<node_indext>
292 std::vector<typename N::node_indext>
296 std::vector<typename N::node_indext> &src,
297 std::size_t limit)
const;
303 std::vector<node_indext> &subgraph_nr);
306 std::size_t
SCCs(std::vector<node_indext> &subgraph_nr)
const;
323 std::vector<typename N::node_indext> &src,
325 std::vector<bool> &visited)
const;
339 tarjant(std::size_t n, std::vector<node_indext> &_subgraph_nr):
357 bool non_trivial)
const;
387 nodet &node=nodes[n];
390 for(
typename edgest::const_iterator
394 nodes[it->first].erase_out(n);
402 nodet &node=nodes[n];
405 for(
typename edgest::const_iterator
409 nodes[it->first].erase_in(n);
419 bool non_trivial)
const
421 std::vector<bool> visited;
422 std::vector<unsigned> distance;
423 std::vector<unsigned> previous;
426 visited.resize(nodes.size(),
false);
427 distance.resize(nodes.size(), (
unsigned)(-1));
428 previous.resize(nodes.size(), 0);
438 std::vector<node_indext> frontier_set, new_frontier_set;
440 frontier_set.reserve(nodes.size());
442 frontier_set.push_back(src);
447 while(!frontier_set.empty() && !found)
451 new_frontier_set.clear();
452 new_frontier_set.reserve(nodes.size());
454 for(
typename std::vector<node_indext>::const_iterator
455 f_it=frontier_set.begin();
456 f_it!=frontier_set.end() && !found;
460 const nodet &n=nodes[i];
463 for(
typename edgest::const_iterator
465 o_it!=n.out.end() && !found;
479 new_frontier_set.push_back(o);
484 frontier_set.swap(new_frontier_set);
492 if(distance[dest]==(
unsigned)(-1))
497 path.push_front(dest);
498 if(distance[dest]==0 ||
499 previous[dest]==src)
break;
501 dest != previous[dest],
"loops cannot be part of the shortest path");
509 std::vector<node_indext> reachable =
get_reachable(src,
true);
510 for(
const auto index : reachable)
511 nodes[index].visited =
true;
525 const std::vector<node_indext> source_nodes(1, src);
526 disconnect_unreachable(source_nodes);
535 std::vector<node_indext> reachable =
get_reachable(src,
true);
536 std::sort(reachable.begin(), reachable.end());
537 std::size_t reachable_idx = 0;
538 for(std::size_t i = 0; i < nodes.size(); i++)
546 reachable_idx >= reachable.size() || i <= reachable[reachable_idx],
547 "node index i is smaller or equal to the node index at "
548 "reachable[reachable_idx], when reachable_idx is within bounds");
550 if(reachable_idx >= reachable.size())
552 else if(i == reachable[reachable_idx])
568 template <
class Container,
typename nodet =
typename Container::value_type>
571 const std::function<
void(
572 const typename Container::value_type &,
573 const std::function<
void(
const typename Container::value_type &)> &)>
576 std::vector<nodet> stack;
577 for(
const auto &elt : set)
578 stack.push_back(elt);
580 while(!stack.empty())
582 auto n = stack.back();
584 for_each_successor(n, [&](
const nodet &node) {
585 if(set.insert(node).second)
586 stack.push_back(node);
597 std::vector<typename N::node_indext>
600 std::vector<node_indext> src_vector;
601 src_vector.push_back(src);
613 const std::vector<node_indext> &src,
616 std::vector<node_indext> result;
617 std::vector<bool> visited(size(),
false);
619 std::stack<node_indext, std::vector<node_indext>> s(src);
632 const auto &node = nodes[n];
633 const auto &succs = forwards ? node.out : node.in;
634 for(
const auto &succ : succs)
635 if(!visited[succ.first])
651 std::size_t limit)
const
653 std::vector<node_indext> start_vector(1, src);
654 return depth_limited_search(start_vector, limit);
665 std::vector<typename N::node_indext> &src,
666 std::size_t limit)
const
668 std::vector<bool> visited(nodes.size(),
false);
670 for(
const auto &node : src)
673 visited[node] =
true;
676 return depth_limited_search(src, limit, visited);
688 std::vector<typename N::node_indext> &src,
690 std::vector<bool> &visited)
const
695 std::vector<node_indext> next_ring;
697 for(
const auto &n : src)
699 for(
const auto &o : nodes[n].out)
701 if(!visited[o.first])
703 next_ring.push_back(o.first);
704 visited[o.first] =
true;
709 if(next_ring.empty())
714 for(
const auto &succ : depth_limited_search(next_ring, limit, visited))
727 std::vector<node_indext> &subgraph_nr)
729 std::vector<bool> visited;
731 visited.resize(nodes.size(),
false);
732 subgraph_nr.resize(nodes.size(), 0);
743 std::stack<node_indext> s;
754 const nodet &node=nodes[n];
756 for(
const auto &o : node.out)
758 if(!visited[o.first])
779 const nodet &node=nodes[v];
780 for(
typename edgest::const_iterator
802 "stack of strongly connected components should have another component");
830 tarjant t(nodes.size(), subgraph_nr);
854 const nodet &n=tmp[i];
857 for(
const auto &o1 : n.out)
858 for(
const auto &o2 : n.out)
860 if(o1.first!=o2.first)
863 this->add_undirected_edge(o1.first, o2.first);
878 std::list<node_indext> nodelist;
880 std::queue<node_indext> indeg0_nodes;
882 std::vector<size_t> in_deg(nodes.size(), 0);
887 in_deg[idx]=in(idx).size();
889 indeg0_nodes.push(idx);
892 while(!indeg0_nodes.empty())
896 nodelist.push_back(source);
898 for(
const auto &edge : out(source))
901 INVARIANT(in_deg[target]!=0,
"in-degree of node cannot be zero here");
906 if(in_deg[target]==0)
907 indeg0_nodes.push(target);
913 if(nodelist.size()!=nodes.size())
918 template <
typename node_index_type>
921 const std::function<
void(std::function<
void(
const node_index_type &)>)>
924 void(
const node_index_type &, std::function<
void(
const node_index_type &)>)>
926 const std::function<std::string(
const node_index_type &)> node_to_string,
927 const std::function<std::string(
const node_index_type &)> node_to_pretty)
929 for_each_node([&](
const node_index_type &i) {
930 out << node_to_pretty(i) <<
";\n";
931 for_each_succ(i, [&](
const node_index_type &n) {
932 out << node_to_string(i) <<
" -> " << node_to_string(n) <<
'\n';
941 std::vector<node_indext> result;
943 nodes[n].out.begin(),
945 std::back_inserter(result),
946 [&](
const std::pair<node_indext, edget> &edge) { return edge.first; });
956 nodes[n].out.begin(),
958 [&](
const std::pair<node_indext, edget> &edge) { f(edge.first); });
964 const auto for_each_node =
965 [
this](
const std::function<void(
const node_indext &)> &f) {
970 const auto for_each_succ = [&](
972 for_each_successor(i, f);
976 const auto to_pretty_string = [
this](
const node_indext &i) {
977 return nodes[i].pretty(i);
979 output_dot_generic<node_indext>(
980 out, for_each_node, for_each_succ,
to_string, to_pretty_string);
983 #endif // CPROVER_UTIL_GRAPH_H