graph.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: A Template Class for Graphs
 
Author: Daniel Kroening, kroening@kroening.com
 
\*******************************************************************/
 
 
#ifndef CPROVER_UTIL_GRAPH_H
#define CPROVER_UTIL_GRAPH_H
 
#include <algorithm>
#include <functional>
#include <iosfwd>
#include <list>
#include <map>
#include <queue>
#include <sstream>
#include <stack>
#include <vector>
 
#include "invariant.h"
 
class empty_edget
{
};
 
template<class E=empty_edget>
class graph_nodet
{
public:
  typedef std::size_t node_indext;
 
  typedef E edget;
  typedef std::map<node_indext, edget> edgest;
 
  edgest in, out;
 
  void add_in(node_indext n)
  {
    in.insert(std::pair<node_indext, edget>(n, edget()));
  }
 
  void add_out(node_indext n)
  {
    out.insert(std::pair<node_indext, edget>(n, edget()));
  }
 
  void erase_in(node_indext n)
  {
    in.erase(n);
  }
 
  void erase_out(node_indext n)
  {
    out.erase(n);
  }
 
private:
  virtual std::string dot_attributes(const node_indext &) const
  {
    return "";
  }
 
public:
  std::string pretty(const node_indext &idx) const
  {
    std::stringstream ss;
    ss << std::to_string(idx) << " " << dot_attributes(idx);
    return ss.str();
  }
 
  virtual ~graph_nodet()
  {
  }
};
 
template<class E>
class visited_nodet:public graph_nodet<E>
{
public:
  typedef typename graph_nodet<E>::edget edget;
  typedef typename graph_nodet<E>::edgest edgest;
 
  bool visited;
 
  visited_nodet():visited(false)
  {
  }
};
 
template<class E>
void intersection(
  const typename graph_nodet<E>::edgest &a,
  const typename graph_nodet<E>::edgest &b,
  typename graph_nodet<E>::edgest &dest)
{
  typename graph_nodet<E>::edgest::const_iterator
    it_a=a.begin(),
    it_b=b.begin();
 
  while(it_a!=a.end() && it_b!=b.end())
  {
    if(*it_a==*it_b)
    {
      dest.insert(*it_a);
      it_a++;
      it_b++;
    }
    else if(*it_a<*it_b)
      it_a++;
    else // *it_a>*it_b
      it_b++;
  }
}
 
template<class N=graph_nodet<empty_edget> >
class grapht
{
public:
  typedef N nodet;
  typedef typename nodet::edgest edgest;
  typedef std::vector<nodet> nodest;
  typedef typename nodet::edget edget;
  typedef typename nodet::node_indext node_indext;
 
protected:
  nodest nodes;
 
public:
  template <typename... arguments>
  node_indext add_node(arguments &&... values)
  {
    node_indext no=nodes.size();
    nodes.emplace_back(std::forward<arguments>(values)...);
    return no;
  }
 
  void swap(grapht &other)
  {
    nodes.swap(other.nodes);
  }
 
  bool has_edge(node_indext i, node_indext j) const
  {
    return nodes[i].out.find(j)!=nodes[i].out.end();
  }
 
  const nodet &operator[](node_indext n) const
  {
    return nodes[n];
  }
 
  nodet &operator[](node_indext n)
  {
    return nodes[n];
  }
 
  void resize(node_indext s)
  {
    nodes.resize(s);
  }
 
  std::size_t size() const
  {
    return nodes.size();
  }
 
  bool empty() const
  {
    return nodes.empty();
  }
 
  const edgest &in(node_indext n) const
  {
    return nodes[n].in;
  }
 
  const edgest &out(node_indext n) const
  {
    return nodes[n].out;
  }
 
  void add_edge(node_indext a, node_indext b)
  {
    nodes[a].add_out(b);
    nodes[b].add_in(a);
  }
 
  void remove_edge(node_indext a, node_indext b)
  {
    nodes[a].erase_out(b);
    nodes[b].erase_in(a);
  }
 
  edget &edge(node_indext a, node_indext b)
  {
    return nodes[a].out[b];
  }
 
  void add_undirected_edge(node_indext a, node_indext b);
  void remove_undirected_edge(node_indext a, node_indext b);
  void remove_in_edges(node_indext n);
  void remove_out_edges(node_indext n);
 
  void remove_edges(node_indext n)
  {
    remove_in_edges(n);
    remove_out_edges(n);
  }
 
  void clear()
  {
    nodes.clear();
  }
 
  typedef std::list<node_indext> patht;
 
  void shortest_path(
    node_indext src,
    node_indext dest,
    patht &path) const
  {
    shortest_path(src, dest, path, false);
  }
 
  void shortest_loop(
    node_indext node,
    patht &path) const
  {
    shortest_path(node, node, path, true);
  }
 
  void visit_reachable(node_indext src);
 
  std::vector<node_indext> get_reachable(node_indext src, bool forwards) const;
 
  std::vector<node_indext>
  get_reachable(const std::vector<node_indext> &src, bool forwards) const;
 
  void disconnect_unreachable(node_indext src);
  void disconnect_unreachable(const std::vector<node_indext> &src);
 
  std::vector<typename N::node_indext>
  depth_limited_search(typename N::node_indext src, std::size_t limit) const;
 
  std::vector<typename N::node_indext> depth_limited_search(
    std::vector<typename N::node_indext> &src,
    std::size_t limit) const;
 
  void make_chordal();
 
  // return value: number of connected subgraphs
  std::size_t connected_subgraphs(
    std::vector<node_indext> &subgraph_nr);
 
  // return value: number of SCCs
  std::size_t SCCs(std::vector<node_indext> &subgraph_nr) const;
 
  bool is_dag() const
  {
    return empty() || !topsort().empty();
  }
 
  std::list<node_indext> topsort() const;
 
  std::vector<node_indext> get_predecessors(const node_indext &n) const;
  std::vector<node_indext> get_successors(const node_indext &n) const;
  void output_dot(std::ostream &out) const;
  void for_each_predecessor(
    const node_indext &n,
    std::function<void(const node_indext &)> f) const;
  void for_each_successor(
    const node_indext &n,
    std::function<void(const node_indext &)> f) const;
 
protected:
  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;
 
  class tarjant
  {
  public:
    std::vector<bool> visited;
    std::vector<unsigned> depth;
    std::vector<unsigned> lowlink;
    std::vector<bool> in_scc;
    std::stack<node_indext> scc_stack;
    std::vector<node_indext> &subgraph_nr;
 
    std::size_t scc_count, max_dfs;
 
    tarjant(std::size_t n, std::vector<node_indext> &_subgraph_nr):
      subgraph_nr(_subgraph_nr)
    {
      visited.resize(n, false);
      depth.resize(n, 0);
      lowlink.resize(n, 0);
      in_scc.resize(n, false);
      max_dfs=scc_count=0;
      subgraph_nr.resize(n, 0);
    }
  };
 
  void tarjan(class tarjant &t, node_indext v) const;
 
  void shortest_path(
    node_indext src,
    node_indext dest,
    patht &path,
    bool non_trivial) const;
};
 
template<class N>
void grapht<N>::add_undirected_edge(node_indext a, node_indext b)
{
  PRECONDITION(a < nodes.size());
  PRECONDITION(b < nodes.size());
  nodet &na=nodes[a];
  nodet &nb=nodes[b];
  na.add_out(b);
  nb.add_out(a);
  na.add_in(b);
  nb.add_in(a);
}
 
template<class N>
void grapht<N>::remove_undirected_edge(node_indext a, node_indext b)
{
  nodet &na=nodes[a];
  nodet &nb=nodes[b];
  na.out.erase(b);
  nb.out.erase(a);
  na.in.erase(b);
  nb.in.erase(a);
}
 
template<class N>
void grapht<N>::remove_in_edges(node_indext n)
{
  nodet &node=nodes[n];
 
  // delete all incoming edges
  for(typename edgest::const_iterator
      it=node.in.begin();
      it!=node.in.end();
      it++)
    nodes[it->first].erase_out(n);
 
  node.in.clear();
}
 
template<class N>
void grapht<N>::remove_out_edges(node_indext n)
{
  nodet &node=nodes[n];
 
  // delete all outgoing edges
  for(typename edgest::const_iterator
      it=node.out.begin();
      it!=node.out.end();
      it++)
    nodes[it->first].erase_in(n);
 
  node.out.clear();
}
 
template<class N>
void grapht<N>::shortest_path(
  node_indext src,
  node_indext dest,
  patht &path,
  bool non_trivial) const
{
  std::vector<bool> visited;
  std::vector<unsigned> distance;
  std::vector<unsigned> previous;
 
  // initialization
  visited.resize(nodes.size(), false);
  distance.resize(nodes.size(), (unsigned)(-1));
  previous.resize(nodes.size(), 0);
 
  if(!non_trivial)
  {
    distance[src]=0;
    visited[src]=true;
  }
 
  // does BFS, not Dijkstra
  // we hope the graph is sparse
  std::vector<node_indext> frontier_set, new_frontier_set;
 
  frontier_set.reserve(nodes.size());
 
  frontier_set.push_back(src);
 
  unsigned d=0;
  bool found=false;
 
  while(!frontier_set.empty() && !found)
  {
    d++;
 
    new_frontier_set.clear();
    new_frontier_set.reserve(nodes.size());
 
    for(typename std::vector<node_indext>::const_iterator
        f_it=frontier_set.begin();
        f_it!=frontier_set.end() && !found;
        f_it++)
    {
      node_indext i=*f_it;
      const nodet &n=nodes[i];
 
      // do all neighbors
      for(typename edgest::const_iterator
          o_it=n.out.begin();
          o_it!=n.out.end() && !found;
          o_it++)
      {
        node_indext o=o_it->first;
 
        if(!visited[o])
        {
          distance[o]=d;
          previous[o]=i;
          visited[o]=true;
 
          if(o==dest)
            found=true;
          else
            new_frontier_set.push_back(o);
        }
      }
    }
 
    frontier_set.swap(new_frontier_set);
  }
 
  // compute path
  // walk towards 0-distance node
  path.clear();
 
  // reachable at all?
  if(distance[dest]==(unsigned)(-1))
    return; // nah
 
  while(true)
  {
    path.push_front(dest);
    if(distance[dest]==0 ||
       previous[dest]==src) break; // we are there
    INVARIANT(
      dest != previous[dest], "loops cannot be part of the shortest path");
    dest=previous[dest];
  }
}
 
template<class N>
void grapht<N>::visit_reachable(node_indext src)
{
  std::vector<node_indext> reachable = get_reachable(src, true);
  for(const auto index : reachable)
    nodes[index].visited = true;
}
 
template <class N>
void grapht<N>::disconnect_unreachable(node_indext src)
{
  const std::vector<node_indext> source_nodes(1, src);
  disconnect_unreachable(source_nodes);
}
 
template <class N>
void grapht<N>::disconnect_unreachable(const std::vector<node_indext> &src)
{
  std::vector<node_indext> reachable = get_reachable(src, true);
  std::sort(reachable.begin(), reachable.end());
  std::size_t reachable_idx = 0;
  for(std::size_t i = 0; i < nodes.size(); i++)
  {
    // Holds since `reachable` contains node indices (i.e., all elements are
    // smaller than `nodes.size()`), `reachable` is sorted, indices from `0` to
    // `nodes.size()-1` are iterated over by variable i in order, and
    // `reachable_idx` is only incremented when `i == reachable[reachable_idx]`
    // holds.
    INVARIANT(
      reachable_idx >= reachable.size() || i <= reachable[reachable_idx],
      "node index i is smaller or equal to the node index at "
      "reachable[reachable_idx], when reachable_idx is within bounds");
 
    if(reachable_idx >= reachable.size())
      remove_edges(i);
    else if(i == reachable[reachable_idx])
      reachable_idx++;
    else
      remove_edges(i);
  }
}
 
template <class Container, typename nodet = typename Container::value_type>
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)
{
  std::vector<nodet> stack;
  for(const auto &elt : set)
    stack.push_back(elt);
 
  while(!stack.empty())
  {
    auto n = stack.back();
    stack.pop_back();
    for_each_successor(n, [&](const nodet &node) {
      if(set.insert(node).second)
        stack.push_back(node);
    });
  }
}
 
template<class N>
std::vector<typename N::node_indext>
grapht<N>::get_reachable(node_indext src, bool forwards) const
{
  std::vector<node_indext> src_vector;
  src_vector.push_back(src);
 
  return get_reachable(src_vector, forwards);
}
 
template <class N>
std::vector<typename N::node_indext> grapht<N>::get_reachable(
  const std::vector<node_indext> &src,
  bool forwards) const
{
  std::vector<node_indext> result;
  std::vector<bool> visited(size(), false);
 
  std::stack<node_indext, std::vector<node_indext>> s(src);
 
  while(!s.empty())
  {
    node_indext n = s.top();
    s.pop();
 
    if(visited[n])
      continue;
 
    result.push_back(n);
    visited[n] = true;
 
    const auto &node = nodes[n];
    const auto &succs = forwards ? node.out : node.in;
    for(const auto &succ : succs)
      if(!visited[succ.first])
        s.push(succ.first);
  }
 
  return result;
}
 
template <class N>
std::vector<typename N::node_indext> grapht<N>::depth_limited_search(
  const typename N::node_indext src,
  std::size_t limit) const
{
  std::vector<node_indext> start_vector(1, src);
  return depth_limited_search(start_vector, limit);
}
 
template <class N>
std::vector<typename N::node_indext> grapht<N>::depth_limited_search(
  std::vector<typename N::node_indext> &src,
  std::size_t limit) const
{
  std::vector<bool> visited(nodes.size(), false);
 
  for(const auto &node : src)
  {
    PRECONDITION(node < nodes.size());
    visited[node] = true;
  }
 
  return depth_limited_search(src, limit, visited);
}
 
template <class N>
std::vector<typename N::node_indext> grapht<N>::depth_limited_search(
  std::vector<typename N::node_indext> &src,
  std::size_t limit,
  std::vector<bool> &visited) const
{
  if(limit == 0)
    return src;
 
  std::vector<node_indext> next_ring;
 
  for(const auto &n : src)
  {
    for(const auto &o : nodes[n].out)
    {
      if(!visited[o.first])
      {
        next_ring.push_back(o.first);
        visited[o.first] = true;
      }
    }
  }
 
  if(next_ring.empty())
    return src;
 
  limit--;
 
  for(const auto &succ : depth_limited_search(next_ring, limit, visited))
    src.push_back(succ);
 
  return src;
}
 
template<class N>
std::size_t grapht<N>::connected_subgraphs(
  std::vector<node_indext> &subgraph_nr)
{
  std::vector<bool> visited;
 
  visited.resize(nodes.size(), false);
  subgraph_nr.resize(nodes.size(), 0);
 
  std::size_t nr=0;
 
  for(node_indext src=0; src<size(); src++)
  {
    if(visited[src])
      continue;
 
    // DFS
 
    std::stack<node_indext> s;
    s.push(src);
 
    while(!s.empty())
    {
      node_indext n=s.top();
      s.pop();
 
      visited[n]=true;
      subgraph_nr[n]=nr;
 
      const nodet &node=nodes[n];
 
      for(const auto &o : node.out)
      {
        if(!visited[o.first])
          s.push(o.first);
      }
    }
 
    nr++;
  }
 
  return nr;
}
 
template<class N>
void grapht<N>::tarjan(tarjant &t, node_indext v) const
{
  t.scc_stack.push(v);
  t.in_scc[v]=true;
  t.depth[v]=t.max_dfs;
  t.lowlink[v]=t.max_dfs;
  t.visited[v]=true;
  t.max_dfs++;
 
  const nodet &node=nodes[v];
  for(typename edgest::const_iterator
      it=node.out.begin();
      it!=node.out.end();
      it++)
  {
    node_indext vp=it->first;
    if(!t.visited[vp])
    {
      tarjan(t, vp);
      t.lowlink[v]=std::min(t.lowlink[v], t.lowlink[vp]);
    }
    else if(t.in_scc[vp])
      t.lowlink[v]=std::min(t.lowlink[v], t.depth[vp]);
  }
 
  // check if root of SCC
  if(t.lowlink[v]==t.depth[v])
  {
    while(true)
    {
      INVARIANT(
        !t.scc_stack.empty(),
        "stack of strongly connected components should have another component");
      node_indext vp=t.scc_stack.top();
      t.scc_stack.pop();
      t.in_scc[vp]=false;
      t.subgraph_nr[vp]=t.scc_count;
      if(vp==v)
        break;
    }
 
    t.scc_count++;
  }
}
 
template<class N>
std::size_t grapht<N>::SCCs(std::vector<node_indext> &subgraph_nr) const
{
  tarjant t(nodes.size(), subgraph_nr);
 
  for(node_indext v0=0; v0<size(); v0++)
    if(!t.visited[v0])
      tarjan(t, v0);
 
  return t.scc_count;
}
 
template<class N>
void grapht<N>::make_chordal()
{
  grapht tmp(*this);
 
  // This assumes an undirected graph.
  // 1. remove all nodes in tmp, reconnecting the remaining ones
  // 2. the chordal graph is the old one plus the new edges
 
  for(node_indext i=0; i<tmp.size(); i++)
  {
    const nodet &n=tmp[i];
 
    // connect all the nodes in n.out with each other
    for(const auto &o1 : n.out)
      for(const auto &o2 : n.out)
      {
        if(o1.first!=o2.first)
        {
          tmp.add_undirected_edge(o1.first, o2.first);
          this->add_undirected_edge(o1.first, o2.first);
        }
      }
 
    // remove node from tmp graph
    tmp.remove_edges(i);
  }
}
 
template<class N>
std::list<typename grapht<N>::node_indext> grapht<N>::topsort() const
{
  // list of topologically sorted nodes
  std::list<node_indext> nodelist;
  // queue of working set nodes with in-degree zero
  std::queue<node_indext> indeg0_nodes;
  // in-degree for each node
  std::vector<size_t> in_deg(nodes.size(), 0);
 
  // abstract graph as in-degree of each node
  for(node_indext idx=0; idx<nodes.size(); idx++)
  {
    in_deg[idx]=in(idx).size();
    if(in_deg[idx]==0)
      indeg0_nodes.push(idx);
  }
 
  while(!indeg0_nodes.empty())
  {
    node_indext source=indeg0_nodes.front();
    indeg0_nodes.pop();
    nodelist.push_back(source);
 
    for(const auto &edge : out(source))
    {
      const node_indext target=edge.first;
      INVARIANT(in_deg[target]!=0, "in-degree of node cannot be zero here");
 
      // remove edge from graph, by decrementing the in-degree of target
      // outgoing edges from source will not be traversed again
      in_deg[target]--;
      if(in_deg[target]==0)
        indeg0_nodes.push(target);
    }
  }
 
  // if all nodes are sorted, the graph is acyclic
  // return empty list in case of cyclic graph
  if(nodelist.size()!=nodes.size())
    nodelist.clear();
  return nodelist;
}
 
template <typename node_index_type>
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)
{
  for_each_node([&](const node_index_type &i) {
    out << node_to_pretty(i) << ";\n";
    for_each_succ(i, [&](const node_index_type &n) {
      out << node_to_string(i) << " -> " << node_to_string(n) << '\n';
    });
  });
}
 
template <class N>
std::vector<typename grapht<N>::node_indext>
grapht<N>::get_predecessors(const node_indext &n) const
{
  std::vector<node_indext> result;
  std::transform(
    nodes[n].in.begin(),
    nodes[n].in.end(),
    std::back_inserter(result),
    [&](const std::pair<node_indext, edget> &edge) { return edge.first; });
  return result;
}
 
template <class N>
std::vector<typename grapht<N>::node_indext>
grapht<N>::get_successors(const node_indext &n) const
{
  std::vector<node_indext> result;
  std::transform(
    nodes[n].out.begin(),
    nodes[n].out.end(),
    std::back_inserter(result),
    [&](const std::pair<node_indext, edget> &edge) { return edge.first; });
  return result;
}
 
template <class N>
void grapht<N>::for_each_predecessor(
  const node_indext &n,
  std::function<void(const node_indext &)> f) const
{
  std::for_each(
    nodes[n].in.begin(),
    nodes[n].in.end(),
    [&](const std::pair<node_indext, edget> &edge) { f(edge.first); });
}
 
template <class N>
void grapht<N>::for_each_successor(
  const node_indext &n,
  std::function<void(const node_indext &)> f) const
{
  std::for_each(
    nodes[n].out.begin(),
    nodes[n].out.end(),
    [&](const std::pair<node_indext, edget> &edge) { f(edge.first); });
}
 
template <class N>
void grapht<N>::output_dot(std::ostream &out) const
{
  const auto for_each_node =
    [this](const std::function<void(const node_indext &)> &f) {
      for(node_indext i = 0; i < nodes.size(); ++i)
        f(i);
    };
 
  const auto for_each_succ = [&](
    const node_indext &i, const std::function<void(const node_indext &)> &f) {
    for_each_successor(i, f);
  };
 
  const auto to_string = [](const node_indext &i) { return std::to_string(i); };
  const auto to_pretty_string = [this](const node_indext &i) {
    return nodes[i].pretty(i);
  };
  output_dot_generic<node_indext>(
    out, for_each_node, for_each_succ, to_string, to_pretty_string);
}
 
#endif // CPROVER_UTIL_GRAPH_H