/*******************************************************************\

Module: data dependencies

Author: Vincent Nimal

Date: 2012

\*******************************************************************/

/// \file
/// data dependencies

#ifndef CPROVER_GOTO_INSTRUMENT_WMM_DATA_DP_H
#define CPROVER_GOTO_INSTRUMENT_WMM_DATA_DP_H

#include <set>

#include <util/source_location.h>

class abstract_eventt;
class messaget;

struct datat
{
  irep_idt id;
  source_locationt loc;
  mutable unsigned eq_class;

  datat(irep_idt _id, source_locationt _loc, unsigned _eq_class)
  : id(_id), loc(_loc), eq_class(_eq_class)
  {
  }

  datat(irep_idt _id, source_locationt _loc)
  : id(_id), loc(_loc), eq_class(0)
  {
  }

  bool operator==(const datat &d) const
  {
    return id==d.id && loc==d.loc;
  }

  bool operator<(const datat &d2) const
  {
    return id<d2.id || (id==d2.id && loc<d2.loc);
  }
};

class data_dpt final
{
  typedef std::set<datat> data_typet;
  data_typet data;
  unsigned class_nb;

public:
  /* add this dependency in the structure */
  void dp_analysis(const abstract_eventt &read, const abstract_eventt &write);
  void dp_analysis(
    const datat &read,
    bool local_read,
    const datat &write,
    bool local_write);

  /* are these two events with a data dependency ? */
  bool dp(const abstract_eventt &e1, const abstract_eventt &e2) const;

  /* routine to maintain partitioning */
  void dp_merge();

  /* printing */
  void print(messaget &message);
};

#endif // CPROVER_GOTO_INSTRUMENT_WMM_DATA_DP_H
