/*
 *  Main authors:
 *     Patrick Pekczynski <pekczynski@ps.uni-sb.de>
 *
 *  Copyright:
 *     Patrick Pekczynski, 2004
 *
 *  Last modified:
 *     $Date: 2006-08-04 16:03:26 +0200 (Fri, 04 Aug 2006) $ by $Author: schulte $
 *     $Revision: 3512 $
 *
 *  This file is part of Gecode, the generic constraint
 *  development environment:
 *     http://www.gecode.org
 *
 *  See the file "LICENSE" for information on usage and
 *  redistribution of this file, and for a
 *     DISCLAIMER OF ALL WARRANTIES.
 *
 */	

namespace Gecode { namespace Int { namespace Sortedness {

  /// Debugging: Print a View
  template<class View>
  void pview(View& v){
    if (v.min() == v.max()) {
      std::cout << v.min() <<" ";
    } else {
      if (v.range()){
	std::cout << "["<<v.min() <<".."<<v.max()<<"] ";
      } else {
	std::cout << "{";
	ViewValues<View> iter(v);
	while(iter()){
	  std::cout << iter.val() <<",";
	  ++iter;
	}
	std::cout << "} ";
      }
    }
  }

  /// Debugging: Print a ViewTuple
  template <class T, unsigned int n>
  inline std::ostream&
  operator<<(std::ostream& os, ViewTuple<T,n>& xs) {
    if (n > 1) { os << "<";}
    if (xs[0].min() == xs[0].max()) {
      os << xs[0].min();
      if (n > 1) {
	std::cout << ",";
	if (xs[1].min() == xs[1].max()) {
	  os << xs[1].min() <<" ";
	} else {
	  os << "["<<xs[1].min() <<".."<<xs[1].max()<<"]("<<xs[1].range()<<") ";
	}
      }
    } else {
      os << "["<<xs[0].min() <<".."<<xs[0].max()<<"]("<<xs[0].range()<<")";
      if (n > 1) {
	std::cout << ", ";
	if (xs[1].min() == xs[1].max()) {
	  os << xs[1].min() <<" ";
	} else {
	  os << "["<<xs[1].min() <<".."<<xs[1].max()<<"]("<<xs[1].range()<<") ";
	}
      }
    }
//  else {
// 	os << "{";
// 	ViewValues<View> iter(xs[0]);
// 	while(iter()){
// 	  os << iter.val() <<",";
// 	  ++iter;
// 	}
// 	os << "} ";
//       }
    if (n > 1) { os << ">";}
    return os;
  }

  /**
   * \brief Storage class for mininmum and maximum of a variable.
   */
  class Rank {
  public:
    // stores the mininmum of a variable
    int min;
    // stores the mininmum of a variable
    int max;
  };

  /**
   *  \brief Representation of a strongly connected component
   *
   *  Used with the implicit array representation of the
   *  bipartite oriented intersection graph.
   */
  class SccComponent {
  public:
    /// Leftmost y-node in a scc
    int leftmost;
    /// Direct left neighbour of an y-node in a scc
    int left;
    /// Direct right neighbour of an y-node in a scc
    int right;
    /// Rightmost reachable y-node in a scc
    int rightmost;
  };

  /**
   * \brief Subsumption test
   *
   * The propagator for Sortedness is subsumed if all
   * variables of the ViewArrays
   * \a x, \a y and \a z are determined and
   * \ref SortednessSemantics "the Semantics of Sortedness"
   * are respected. \n
   * In addition to the subsumption test check_subsumption
   * determines, whether we can reduce the orginial problem
   * to a smaller one, by dropping already matched variables.
   */

  template<class View, class Tuple, bool Perm>
  forceinline bool
  check_subsumption(Space* home,
		    ViewArray<Tuple>& xz,
		    ViewArray<View>& y,
		    bool& subsumed,
		    int& dropfst) {

    dropfst  = 0;
    subsumed = true;
    int  xs  = xz.size();
    for (int i = 0; i < xs ; i++) {
      if (Perm) {
	subsumed &= (xz[i][0].assigned() &&
		     xz[i][1].assigned() &&
		     y[xz[i][1].val()].assigned());
	if (subsumed) {
	  if (xz[i][0].val() != y[xz[i][1].val()].val()) {
	    return false;
	  } else {
	    if (xz[i][1].val() == i) {
	      dropfst++;
	    }
	  }
	}
      } else {
	subsumed &= (xz[i][0].assigned() && y[i].assigned());
	if (subsumed) {
	  if (xz[i][0].val() != y[i].val()) {
	    return false;
	  } else {
	    dropfst++;
	  }
	}
      }
    }
    return true;
  }

  /**
   *   \brief Item used to construct the OfflineMin sequence
   *
   */

  class OfflineMinItem{
  public:
    /// Root node representing the set the vertex belongs to
    int root;
    /// Predecessor in the tree representation of the set
    int parent;
    /// Ranking of the set given by its cardinality
    int rank;
    /// Name or label of a set
    int name;
    /**
     *  \brief Initial set label
     *
     *   This label represents the iteration index \f$i\f$
     *   and hence the index of an insert instruction
     *   in the complete Offline-Min sequence
     */
    int iset;
    /// Successor in the Offline-Min sequence
    int succ;
    /// Predecessor in the Offline-Min sequence
    int pred;
  };

  /**
   *  \brief Offline-Min datastructure
   *  Used to compute the perfect matching between the unsorted views
   *  \a x and the sorted views \a y.
   */
  class OfflineMin {
  private:
    OfflineMinItem* sequence;
    int* vertices;
    int  n;
  public:
    OfflineMin(void);
    OfflineMin(OfflineMinItem[], int[], int);
    /**
     *  Find the set x belongs to
     *  (wihtout path compression)
     */
    int  find(int x);
    /**
     *  Find the set x belongs to
     *  (using path compression)
     */
    int  find_pc(int x);
    /// Unite two sets \a a and \a b and label the union with \a c
    void unite(int a, int b, int c);
    /// Initialization of the datastructure
    void makeset(void);
    /// Return the size of the Offline-Min item
    int  size(void);
    OfflineMinItem& operator[](int);
  };

  OfflineMin::OfflineMin(void){
    n = 0;
    sequence = NULL;
    vertices = NULL;
  }

  OfflineMin::OfflineMin(OfflineMinItem s[], int v[], int size){
    n = size;
    sequence = &s[0];
    vertices = &v[0];
  }

  forceinline int
  OfflineMin::find(int x) {
    while (sequence[x].parent != x) {
      x = sequence[x].parent;
    }
    // x is now the root of the tree
    // return the set, x belongs to
    return sequence[x].name;
  }

  forceinline int
  OfflineMin::find_pc(int x){
    int vsize = 0;
    while (sequence[x].parent != x) {
      vertices[x] = x;
      x = sequence[x].parent;
    }
    // x is now the root of the tree
    for (int i = vsize; i--; ) {
      sequence[vertices[i]].parent = x;
    }
    // return the set, x belongs to
    return sequence[x].name;
  }

  forceinline void
  OfflineMin::unite(int a, int b, int c){
    // c is the union of a and b
    int ra = sequence[a].root;
    int rb = sequence[b].root;
    int large = rb;
    int small = ra;
    if (sequence[ra].rank > sequence[rb].rank) {
      large = ra;
      small = rb;
    }
    sequence[small].parent =  large;
    sequence[large].rank   += sequence[small].rank;
    sequence[large].name   =  c;
    sequence[c].root       =  large;
  }

  forceinline void
  OfflineMin::makeset(void){
    for(int i = n; i--; ){
      OfflineMinItem& cur = sequence[i];
      cur.rank   = 0;     // initially each set is empty
      cur.name   = i;     // it has its own name
      cur.root   = i;     // it is the root node
      cur.parent = i;     // it is its own parent
      cur.pred   = i - 1;
      cur.succ   = i + 1;
      cur.iset   = -5;
    }
  }

  forceinline int
  OfflineMin::size(void){
    return n;
  }

  forceinline OfflineMinItem&
  OfflineMin::operator [](int i){
    return sequence[i];
  }

  /// Print an OfflineMin sequence
  forceinline std::ostream&
  operator<<(std::ostream& os,  OfflineMin seq){
    for (int i = 0; i < seq.size();i++) {
      os << "Succ(" <<seq[i].succ   << ") "
	 << "Pred(" <<seq[i].pred   << ") "
	 << "Root(" <<seq[i].root   << ") "
	 << "Par (" <<seq[i].parent << ") "
	 << "Rank(" <<seq[i].rank   << ") "
	 << "Name(" <<seq[i].name   << ") "
	 << "Set (" <<seq[i].iset   << ") \n";
    }
    return os;
  }

  /**
   *  \brief Index comparison for %ViewArray<Tuple>
   *
   *  Checks whether for two indices \a i and \a j
   *  the first component of the corresponding viewtuples
   *  \f$x_i\f$ and \f$x_j\f$ the upper domain bound of \f$x_j\f$
   *  is larger than the upper domain bound of \f$x_i\f$
   *
   */
  template <class Tuple>
  class TupleMaxInc {
  protected:
    ViewArray<Tuple> x;
  public:
    TupleMaxInc(const ViewArray<Tuple>& x0) : x(x0) {}
    bool operator()(const int i, const int j) {
      if (x[i][0].max() == x[j][0].max()) {
	return x[i][0].min() < x[j][0].min();
      } else {
	return x[i][0].max() < x[j][0].max();
      }
    }
  };


  /**
   *  \brief Extended Index comparison for %ViewArray<Tuple>
   *
   *  Checks whether for two indices \a i and \a j
   *  the first component of the corresponding viewtuples
   *  \f$x_i\f$ and \f$x_j\f$ the upper domain bound of \f$x_j\f$
   *  is larger than the upper domain bound of \f$x_i\f$
   *
   */
  template <class Tuple>
  class TupleMaxIncExt {
  protected:
    ViewArray<Tuple> x;
  public:
    TupleMaxIncExt(const ViewArray<Tuple>& x0) : x(x0) {}
    bool operator()(const int i, const int j) {
      if (x[i][0].max() == x[j][0].max()) {
	if (x[i][0].min() == x[j][0].min()) {
	  if (x[i][1].max() == x[j][1].max()) {
	    return x[i][1].min() < x[j][1].min();
	  } else {
	    return x[i][1].max() < x[j][1].max();
	  }
	} else {
	  return x[i][0].min() < x[j][0].min();
	}
      } else {
	return x[i][0].max() < x[j][0].max();
      }
    }
  };

  /**
   * \brief View comparison on ViewTuples
   *
   * Checks whether the lower domain bound of the
   * first component of \a x (the variable itself)
   * is smaller than the lower domain bound of the
   * first component of \a y
   */

  template <class View>
  class TupleMinInc {
  public:
    bool operator()(const View& x, const View& y) {
      if (x[0].min() == y[0].min()) {
	return x[0].max() < y[0].max();
      } else {
	return x[0].min() < y[0].min();
      }
    }
  };

  /**
   * \brief Extended View comparison on ViewTuples
   *
   * Checks whether the lower domain bound of the
   * first component of \a x (the variable itself)
   * is smaller than the lower domain bound of the
   * first component of \a y. If they are equal
   * it checks their upper bounds. If they are also
   * equal we sort the views by the permutation variables.
   */

  template <class View>
  class TupleMinIncExt {
  public:
    bool operator()(const View& x, const View& y) {
      if (x[0].min() == y[0].min()) {
	if (x[0].max() == y[0].max()) {
	  if (x[1].min() == y[1].min()) {
	    return x[1].max() < y[1].max();
	  } else {
	    return x[1].min() < y[1].min();
	  }
	} else {
	  return x[0].max() < y[0].max();
	}
      } else {
	return x[0].min() < y[0].min();
      }
    }
  };

  /**
   * \brief View comparison on ViewTuples
   *
   * Checks whether the lower domain bound of the second component
   * of \a x (the lower bound on the permutation variable) is smaller
   * than the lower domain bound of the second component of \a y.
   */

  template <class View>
  class TupleMinIncPerm {
  public:
    bool operator()(const View& x, const View& y) {
      if (x[1].min() == y[1].min()) {
	return x[1].max() < y[1].max();
      } else {
	return x[1].min() < y[1].min();
      }
    }
  };

  /**
   * \brief View comparison on ViewTuples
   *
   * Checks whether the upper domain bound of the second component
   * of \a x (the upper bound on the permutation variable) is smaller
   * than the upper domain bound of the second component of \a y.
   */

  template <class View>
  class TupleMaxIncPerm {
  public:
    bool operator()(const View& x, const View& y) {
      if (x[1].max() == y[1].max()) {
	return x[1].min() < y[1].min();
      } else {
	return x[1].max() < y[1].max();
      }
    }
  };

  /**
   * \brief Check for assignment of a variable array
   *
   * Check whether one of the argument arrays is completely assigned
   * and udpates the other array respectively.
   */

  template<class View, class Tuple, bool Perm>
  forceinline bool
  array_assigned(Space* home,
		 ViewArray<Tuple>& xz,
		 ViewArray<View>& y,
		 bool& subsumed,
		 bool& match_fixed,
		 bool& nofix,
		 bool& noperm_bc) {

    bool x_complete = true;
    bool y_complete = true;
    bool z_complete = true;

    for (int i = y.size(); i--; ) {
      x_complete &= xz[i][0].assigned();
      y_complete &= y[i].assigned();
      if (Perm) {
	z_complete &= xz[i][1].assigned();
      }
    }

    if (x_complete) {
      for (int i = xz.size(); i--; ) {
	ModEvent me = y[i].eq(home, xz[i][0].val());
	if (me_failed(me)) {
	  return false;
	}
      }
      if (Perm) {
	subsumed = false;
      } else {
	subsumed = true;
      }
    }

    if (y_complete) {
      bool y_equality = true;
      for (int i = y.size() - 1; i--; ) {
	y_equality &= (y[i].val() == y[i + 1].val());
      }
      if (y_equality) {
	for (int i = xz.size(); i--; ) {
	  ModEvent me = xz[i][0].eq(home, y[i].val());
	  if (me_failed(me)) {
	    return false;
	  }
	}
	if (Perm) {
	  subsumed = false;
	} else {
	  subsumed = true;
	}
	noperm_bc = true;
      }
    }

    if (Perm) {
      if (z_complete) {
	if (x_complete) {
	  for (int i = xz.size(); i--; ) {
	    ModEvent me = y[xz[i][1].val()].eq(home, xz[i][0].val());
	    if (me_failed(me)) {
	      return false;
	    }
	  }
	  subsumed = true;
	  return subsumed;
	}
	if (y_complete) {
	  for (int i = xz.size(); i--; ) {
	    ModEvent me = xz[i][0].eq(home, y[xz[i][1].val()].val());
	    if (me_failed(me)) {
	      return false;
	    }
	  }
	  subsumed = true;
	  return subsumed;
	}

	// validate the permutation
	int sum = 0;
	for (int i = xz.size(); i--; ) {
	  int pi = xz[i][1].val();
	  if (xz[i][0].max() < y[pi].min() ||
	      xz[i][0].min() > y[pi].max()) {
	    return false;
	  }
	  sum += pi;
	}
	int n = xz.size();
	int gauss = ( (n * (n + 1)) / 2);
	// if the sum over all assigned permutation variables is not
	// equal to the gaussian sum - n they are not distinct, hence invalid
	if (sum != gauss - n) {
	  return false;
	}
	match_fixed = true;
      }
    }
    return true;
  }

  /**
   * \brief Channel between \a x, \a y and \a z
   *
   * Keep variables consisting by channeling information
   *
   */

  template<class View, class Tuple, bool Perm>
  forceinline bool
  channel(Space* home, ViewArray<Tuple>& xz, ViewArray<View>& y, bool& nofix) {
    int n = xz.size();
    for (int i = n; i--; ) {
      if (xz[i][1].assigned()) {

	// if the permutation variable is determined
	
	int v = xz[i][1].val();
	if (xz[i][0].assigned()) {
	  // channel equality from x to y
	  ModEvent me = y[v].eq(home, xz[i][0].val());
	  if (me_failed(me)) {
	    return false;
	  }
	} else {
	  if (y[v].assigned()) {
	    // channel equality from y to x
	    ModEvent me = xz[i][0].eq(home, y[v].val());
	    if (me_failed(me)) {
	      return false;
	    }
	  } else {
	    // constrain upper bound
	    ModEvent me = xz[i][0].lq(home, y[v].max());
	    if (me_failed(me)) {
	      return false;
	    }
	    nofix |= (me_modified(me) && xz[i][0].max() != y[v].max());

	    // constrain lower bound
	    me = xz[i][0].gq(home, y[v].min());
	    if (me_failed(me)) {
	      return false;
	    }
	    nofix |= (me_modified(me) && xz[i][0].min() != y[v].min());

	    // constrain the sorted variable
	    // constrain upper bound
	    me = y[v].lq(home, xz[i][0].max());
	    if (me_failed(me)) {
	      return false;
	    }
	    nofix |= (me_modified(me) && y[v].max() != xz[i][0].max());

	    // constrain lower bound
	    me = y[v].gq(home, xz[i][0].min());
	    if (me_failed(me)) {
	      return false;
	    }
	    nofix |= (me_modified(me) && y[v].min() != xz[i][0].min());
	  }
	}
      } else {
	
	// if the permutation variable is undetermined
	int l = xz[i][1].min();
	int r = xz[i][1].max();
	
	// upper bound
	ModEvent me = xz[i][0].lq(home, y[r].max());
	if (me_failed(me)) {
	  return false;
	}
	nofix |= (me_modified(me) && xz[i][0].max() != y[r].max());

	// lower bound
	me = xz[i][0].gq(home, y[l].min());
	if (me_failed(me)) {
	  return false;
	}
	nofix |= (me_modified(me) && xz[i][0].min() != y[l].min());
      }
    }
    return true;
  }


}}}


// STATISTICS: int-prop