12 #ifndef CPROVER_UTIL_GRAPH_H
13 #define CPROVER_UTIL_GRAPH_H
34 template<
class E=empty_edget>
41 typedef std::map<node_indext, edget>
edgest;
47 in.insert(std::pair<node_indext, edget>(n,
edget()));
52 out.insert(std::pair<node_indext, edget>(n,
edget()));
125 while(it_a!=a.end() && it_b!=b.end())
166 template<
class N=graph_nodet<empty_edget> >
180 template <
typename... arguments>
184 nodes.emplace_back(std::forward<arguments>(values)...);
195 return nodes[i].out.find(j)!=
nodes[i].out.end();
220 return nodes.empty();
241 nodes[a].erase_out(b);
242 nodes[b].erase_in(a);
247 return nodes[a].out[b];
266 typedef std::list<node_indext>
patht;
287 std::vector<node_indext>
293 std::vector<typename N::node_indext>
297 std::vector<typename N::node_indext> &src,
298 std::size_t limit)
const;
304 std::vector<node_indext> &subgraph_nr);
307 std::size_t
SCCs(std::vector<node_indext> &subgraph_nr)
const;
324 std::vector<typename N::node_indext> &src,
326 std::vector<bool> &visited)
const;
340 tarjant(std::size_t n, std::vector<node_indext> &_subgraph_nr):
358 bool non_trivial)
const;
388 nodet &node=nodes[n];
391 for(
typename edgest::const_iterator
395 nodes[it->first].erase_out(n);
403 nodet &node=nodes[n];
406 for(
typename edgest::const_iterator
410 nodes[it->first].erase_in(n);
420 bool non_trivial)
const
422 std::vector<bool> visited;
423 std::vector<unsigned> distance;
424 std::vector<unsigned> previous;
427 visited.resize(nodes.size(),
false);
428 distance.resize(nodes.size(), (
unsigned)(-1));
429 previous.resize(nodes.size(), 0);
439 std::vector<node_indext> frontier_set, new_frontier_set;
441 frontier_set.reserve(nodes.size());
443 frontier_set.push_back(src);
448 while(!frontier_set.empty() && !found)
452 new_frontier_set.clear();
453 new_frontier_set.reserve(nodes.size());
455 for(
typename std::vector<node_indext>::const_iterator
456 f_it=frontier_set.begin();
457 f_it!=frontier_set.end() && !found;
461 const nodet &n=nodes[i];
464 for(
typename edgest::const_iterator
466 o_it!=n.out.end() && !found;
480 new_frontier_set.push_back(o);
485 frontier_set.swap(new_frontier_set);
493 if(distance[dest]==(
unsigned)(-1))
498 path.push_front(dest);
499 if(distance[dest]==0 ||
500 previous[dest]==src)
break;
502 dest != previous[dest],
"loops cannot be part of the shortest path");
510 std::vector<node_indext> reachable =
get_reachable(src,
true);
511 for(
const auto index : reachable)
512 nodes[index].visited =
true;
526 const std::vector<node_indext> source_nodes(1, src);
527 disconnect_unreachable(source_nodes);
536 std::vector<node_indext> reachable =
get_reachable(src,
true);
537 std::sort(reachable.begin(), reachable.end());
538 std::size_t reachable_idx = 0;
539 for(std::size_t i = 0; i < nodes.size(); i++)
547 reachable_idx >= reachable.size() || i <= reachable[reachable_idx],
548 "node index i is smaller or equal to the node index at "
549 "reachable[reachable_idx], when reachable_idx is within bounds");
551 if(reachable_idx >= reachable.size())
553 else if(i == reachable[reachable_idx])
569 template <
class Container,
typename nodet =
typename Container::value_type>
572 const std::function<
void(
573 const typename Container::value_type &,
574 const std::function<
void(
const typename Container::value_type &)> &)>
577 std::vector<nodet> stack;
578 for(
const auto &elt : set)
579 stack.push_back(elt);
581 while(!stack.empty())
583 auto n = stack.back();
585 for_each_successor(n, [&](
const nodet &node) {
586 if(set.insert(node).second)
587 stack.push_back(node);
598 std::vector<typename N::node_indext>
601 std::vector<node_indext> src_vector;
602 src_vector.push_back(src);
614 const std::vector<node_indext> &src,
617 std::vector<node_indext> result;
618 std::vector<bool> visited(size(),
false);
620 std::stack<node_indext, std::vector<node_indext>> s(src);
633 const auto &node = nodes[n];
634 const auto &succs = forwards ? node.out : node.in;
635 for(
const auto &succ : succs)
636 if(!visited[succ.first])
652 std::size_t limit)
const
654 std::vector<node_indext> start_vector(1, src);
655 return depth_limited_search(start_vector, limit);
666 std::vector<typename N::node_indext> &src,
667 std::size_t limit)
const
669 std::vector<bool> visited(nodes.size(),
false);
671 for(
const auto &node : src)
674 visited[node] =
true;
677 return depth_limited_search(src, limit, visited);
689 std::vector<typename N::node_indext> &src,
691 std::vector<bool> &visited)
const
696 std::vector<node_indext> next_ring;
698 for(
const auto &n : src)
700 for(
const auto &o : nodes[n].out)
702 if(!visited[o.first])
704 next_ring.push_back(o.first);
705 visited[o.first] =
true;
710 if(next_ring.empty())
715 for(
const auto &succ : depth_limited_search(next_ring, limit, visited))
728 std::vector<node_indext> &subgraph_nr)
730 std::vector<bool> visited;
732 visited.resize(nodes.size(),
false);
733 subgraph_nr.resize(nodes.size(), 0);
744 std::stack<node_indext> s;
755 const nodet &node=nodes[n];
757 for(
const auto &o : node.out)
759 if(!visited[o.first])
780 const nodet &node=nodes[v];
781 for(
typename edgest::const_iterator
803 "stack of strongly connected components should have another component");
831 tarjant t(nodes.size(), subgraph_nr);
855 const nodet &n=tmp[i];
858 for(
const auto &o1 : n.out)
859 for(
const auto &o2 : n.out)
861 if(o1.first!=o2.first)
864 this->add_undirected_edge(o1.first, o2.first);
879 std::list<node_indext> nodelist;
881 std::queue<node_indext> indeg0_nodes;
883 std::vector<size_t> in_deg(nodes.size(), 0);
888 in_deg[idx]=in(idx).size();
890 indeg0_nodes.push(idx);
893 while(!indeg0_nodes.empty())
897 nodelist.push_back(source);
899 for(
const auto &edge : out(source))
902 INVARIANT(in_deg[target]!=0,
"in-degree of node cannot be zero here");
907 if(in_deg[target]==0)
908 indeg0_nodes.push(target);
914 if(nodelist.size()!=nodes.size())
919 template <
typename node_index_type>
922 const std::function<
void(std::function<
void(
const node_index_type &)>)>
925 void(
const node_index_type &, std::function<
void(
const node_index_type &)>)>
927 const std::function<std::string(
const node_index_type &)> node_to_string,
928 const std::function<std::string(
const node_index_type &)> node_to_pretty)
930 for_each_node([&](
const node_index_type &i) {
931 out << node_to_pretty(i) <<
";\n";
932 for_each_succ(i, [&](
const node_index_type &n) {
933 out << node_to_string(i) <<
" -> " << node_to_string(n) <<
'\n';
942 std::vector<node_indext> result;
944 nodes[n].out.begin(),
946 std::back_inserter(result),
947 [&](
const std::pair<node_indext, edget> &edge) { return edge.first; });
957 nodes[n].out.begin(),
959 [&](
const std::pair<node_indext, edget> &edge) { f(edge.first); });
965 const auto for_each_node =
966 [
this](
const std::function<void(
const node_indext &)> &f) {
971 const auto for_each_succ = [&](
973 for_each_successor(i, f);
977 const auto to_pretty_string = [
this](
const node_indext &i) {
978 return nodes[i].pretty(i);
980 output_dot_generic<node_indext>(
981 out, for_each_node, for_each_succ,
to_string, to_pretty_string);
984 #endif // CPROVER_UTIL_GRAPH_H