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> >
172 typedef typename nodet::edget
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;
327 std::vector<typename N::node_indext> &src,
329 std::vector<bool> &visited)
const;
343 tarjant(std::size_t n, std::vector<node_indext> &_subgraph_nr):
361 bool non_trivial)
const;
391 nodet &node=nodes[n];
394 for(
typename edgest::const_iterator
398 nodes[it->first].erase_out(n);
406 nodet &node=nodes[n];
409 for(
typename edgest::const_iterator
413 nodes[it->first].erase_in(n);
423 bool non_trivial)
const
425 std::vector<bool> visited;
426 std::vector<unsigned> distance;
427 std::vector<unsigned> previous;
430 visited.resize(nodes.size(),
false);
431 distance.resize(nodes.size(), (
unsigned)(-1));
432 previous.resize(nodes.size(), 0);
442 std::vector<node_indext> frontier_set, new_frontier_set;
444 frontier_set.reserve(nodes.size());
446 frontier_set.push_back(src);
451 while(!frontier_set.empty() && !found)
455 new_frontier_set.clear();
456 new_frontier_set.reserve(nodes.size());
458 for(
typename std::vector<node_indext>::const_iterator
459 f_it=frontier_set.begin();
460 f_it!=frontier_set.end() && !found;
464 const nodet &n=nodes[i];
467 for(
typename edgest::const_iterator
469 o_it!=n.out.end() && !found;
483 new_frontier_set.push_back(o);
488 frontier_set.swap(new_frontier_set);
496 if(distance[dest]==(
unsigned)(-1))
501 path.push_front(dest);
502 if(distance[dest]==0 ||
503 previous[dest]==src)
break;
505 dest != previous[dest],
"loops cannot be part of the shortest path");
513 std::vector<node_indext> reachable =
get_reachable(src,
true);
514 for(
const auto index : reachable)
515 nodes[index].visited =
true;
529 const std::vector<node_indext> source_nodes(1, src);
530 disconnect_unreachable(source_nodes);
539 std::vector<node_indext> reachable =
get_reachable(src,
true);
540 std::sort(reachable.begin(), reachable.end());
541 std::size_t reachable_idx = 0;
542 for(std::size_t i = 0; i < nodes.size(); i++)
550 reachable_idx >= reachable.size() || i <= reachable[reachable_idx],
551 "node index i is smaller or equal to the node index at "
552 "reachable[reachable_idx], when reachable_idx is within bounds");
554 if(reachable_idx >= reachable.size())
556 else if(i == reachable[reachable_idx])
572 template <
class Container,
typename nodet =
typename Container::value_type>
575 const std::function<
void(
576 const typename Container::value_type &,
577 const std::function<
void(
const typename Container::value_type &)> &)>
580 std::vector<nodet> stack;
581 for(
const auto &elt : set)
582 stack.push_back(elt);
584 while(!stack.empty())
586 auto n = stack.back();
588 for_each_successor(n, [&](
const nodet &node) {
589 if(set.insert(node).second)
590 stack.push_back(node);
601 std::vector<typename N::node_indext>
604 std::vector<node_indext> src_vector;
605 src_vector.push_back(src);
617 const std::vector<node_indext> &src,
620 std::vector<node_indext> result;
621 std::vector<bool> visited(size(),
false);
623 std::stack<node_indext, std::vector<node_indext>> s(src);
636 const auto &node = nodes[n];
637 const auto &succs = forwards ? node.out : node.in;
638 for(
const auto &succ : succs)
639 if(!visited[succ.first])
655 std::size_t limit)
const
657 std::vector<node_indext> start_vector(1, src);
658 return depth_limited_search(start_vector, limit);
669 std::vector<typename N::node_indext> &src,
670 std::size_t limit)
const
672 std::vector<bool> visited(nodes.size(),
false);
674 for(
const auto &node : src)
677 visited[node] =
true;
680 return depth_limited_search(src, limit, visited);
692 std::vector<typename N::node_indext> &src,
694 std::vector<bool> &visited)
const
699 std::vector<node_indext> next_ring;
701 for(
const auto &n : src)
703 for(
const auto &o : nodes[n].out)
705 if(!visited[o.first])
707 next_ring.push_back(o.first);
708 visited[o.first] =
true;
713 if(next_ring.empty())
718 for(
const auto &succ : depth_limited_search(next_ring, limit, visited))
731 std::vector<node_indext> &subgraph_nr)
733 std::vector<bool> visited;
735 visited.resize(nodes.size(),
false);
736 subgraph_nr.resize(nodes.size(), 0);
747 std::stack<node_indext> s;
758 const nodet &node=nodes[n];
760 for(
const auto &o : node.out)
762 if(!visited[o.first])
783 const nodet &node=nodes[v];
784 for(
typename edgest::const_iterator
806 "stack of strongly connected components should have another component");
834 tarjant t(nodes.size(), subgraph_nr);
858 const nodet &n=tmp[i];
861 for(
const auto &o1 : n.out)
862 for(
const auto &o2 : n.out)
864 if(o1.first!=o2.first)
867 this->add_undirected_edge(o1.first, o2.first);
882 std::list<node_indext> nodelist;
884 std::queue<node_indext> indeg0_nodes;
886 std::vector<size_t> in_deg(nodes.size(), 0);
891 in_deg[idx]=in(idx).size();
893 indeg0_nodes.push(idx);
896 while(!indeg0_nodes.empty())
900 nodelist.push_back(source);
902 for(
const auto &edge : out(source))
905 INVARIANT(in_deg[target]!=0,
"in-degree of node cannot be zero here");
910 if(in_deg[target]==0)
911 indeg0_nodes.push(target);
917 if(nodelist.size()!=nodes.size())
922 template <
typename node_index_type>
925 const std::function<
void(std::function<
void(
const node_index_type &)>)>
928 void(
const node_index_type &, std::function<
void(
const node_index_type &)>)>
930 const std::function<std::string(
const node_index_type &)> node_to_string,
931 const std::function<std::string(
const node_index_type &)> node_to_pretty)
933 for_each_node([&](
const node_index_type &i) {
934 out << node_to_pretty(i) <<
";\n";
935 for_each_succ(i, [&](
const node_index_type &n) {
936 out << node_to_string(i) <<
" -> " << node_to_string(n) <<
'\n';
945 std::vector<node_indext> result;
949 std::back_inserter(result),
950 [&](
const std::pair<node_indext, edget> &edge) { return edge.first; });
958 std::vector<node_indext> result;
960 nodes[n].out.begin(),
962 std::back_inserter(result),
963 [&](
const std::pair<node_indext, edget> &edge) { return edge.first; });
975 [&](
const std::pair<node_indext, edget> &edge) { f(edge.first); });
984 nodes[n].out.begin(),
986 [&](
const std::pair<node_indext, edget> &edge) { f(edge.first); });
992 const auto for_each_node =
993 [
this](
const std::function<void(
const node_indext &)> &f) {
998 const auto for_each_succ = [&](
1000 for_each_successor(i, f);
1004 const auto to_pretty_string = [
this](
const node_indext &i) {
1005 return nodes[i].pretty(i);
1007 output_dot_generic<node_indext>(
1008 out, for_each_node, for_each_succ,
to_string, to_pretty_string);
static abstract_object_pointert transform(const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns)
This class represents a node in a directed graph.
std::string pretty(const node_indext &idx) const
void add_out(node_indext n)
void erase_out(node_indext n)
void erase_in(node_indext n)
virtual std::string dot_attributes(const node_indext &) const
Node with attributes suitable for Graphviz DOT format.
void add_in(node_indext n)
std::map< node_indext, edget > edgest
std::vector< unsigned > lowlink
std::stack< node_indext > scc_stack
tarjant(std::size_t n, std::vector< node_indext > &_subgraph_nr)
std::vector< node_indext > & subgraph_nr
std::vector< unsigned > depth
std::vector< bool > visited
std::vector< bool > in_scc
A generic directed graph with a parametric node type.
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 for_each_successor(const node_indext &n, std::function< void(const node_indext &)> f) const
void add_undirected_edge(node_indext a, node_indext b)
void resize(node_indext s)
std::vector< typename N::node_indext > depth_limited_search(typename N::node_indext src, std::size_t limit) const
Run recursive depth-limited search on the graph, starting from multiple source nodes,...
std::vector< node_indext > get_predecessors(const node_indext &n) const
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...
std::vector< node_indext > get_reachable(const std::vector< node_indext > &src, bool forwards) const
Run depth-first search on the graph, starting from multiple source nodes.
const nodet & operator[](node_indext n) const
void shortest_path(node_indext src, node_indext dest, patht &path, bool non_trivial) const
const edgest & in(node_indext n) const
nodet::node_indext node_indext
void remove_undirected_edge(node_indext a, node_indext b)
std::vector< nodet > nodest
void remove_out_edges(node_indext n)
nodet & operator[](node_indext n)
void disconnect_unreachable(const std::vector< node_indext > &src)
Removes any edges between nodes in a graph that are unreachable from a vector of start nodes.
std::list< node_indext > patht
bool has_edge(node_indext i, node_indext j) const
void visit_reachable(node_indext src)
std::vector< typename N::node_indext > depth_limited_search(std::vector< typename N::node_indext > &src, std::size_t limit, std::vector< bool > &visited) const
Run recursive depth-limited search on the graph, starting from multiple source nodes,...
node_indext add_node(arguments &&... values)
void shortest_path(node_indext src, node_indext dest, patht &path) const
void output_dot(std::ostream &out) const
void add_edge(node_indext a, node_indext b)
void make_chordal()
Ensure a graph is chordal (contains no 4+-cycles without an edge crossing the cycle) by adding extra ...
void disconnect_unreachable(node_indext src)
Removes any edges between nodes in a graph that are unreachable from a given start node.
std::vector< typename N::node_indext > depth_limited_search(std::vector< typename N::node_indext > &src, std::size_t limit) const
Run recursive depth-limited search on the graph, starting from multiple source nodes,...
std::size_t connected_subgraphs(std::vector< node_indext > &subgraph_nr)
Find connected subgraphs in an undirected graph.
void for_each_predecessor(const node_indext &n, std::function< void(const node_indext &)> f) const
std::vector< node_indext > get_successors(const node_indext &n) const
void remove_edge(node_indext a, node_indext b)
edget & edge(node_indext a, node_indext b)
void remove_edges(node_indext n)
const edgest & out(node_indext n) const
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.
void tarjan(class tarjant &t, node_indext v) const
void shortest_loop(node_indext node, patht &path) const
void remove_in_edges(node_indext n)
A node type with an extra bit.
graph_nodet< E >::edgest edgest
graph_nodet< E >::edget edget
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, const std::function< std::string(const node_index_type &)> node_to_pretty)
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.
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.
#define PRECONDITION(CONDITION)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.