/*
 *  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 GCC {

  /**
   * \brief Upper Bounds constraint (UBC) stating
   * \f$ \forall j \in \{0, \dots, |k|-1\}:
   * \#\{i\in\{0, \dots, |x| - 1\} | x_i = card(k_j)\} \leq max(k_j)\f$
   * Hence the ubc constraints the variables such that no value occurs
   * more often than specified by its upper cardinality bound.
   * \param home current space
   * \param x  the problem variables
   * \param nb denotes number of unique bounds
   * \param hall contains information about the hall structure of the problem
   *        (cf. HallInfo)
   * \param rank ranking information about the variable bounds (cf. Rank)
   * \param ups partial sum structure for the upper cardinality bounds (cf. PartialSum)
   * \param mu permutation \f$ \mu \f$ such that
   *        \f$ \forall i\in \{0, \dots, |x|-2\}:
   *        max(x_{\mu(i)}) \leq max(x_{\mu(i+1)})\f$
   * \param nu permutation \f$ \nu \f$ such that
   *        \f$ \forall i\in \{0, \dots, |x|-2\}:
   *        min(x_{\mu(i)}) \leq min(x_{\mu(i+1)})\f$
   */

  template <class View, class Card, bool shared>
  inline ExecStatus
  ubc(Space* home, ViewArray<View>& x, int& nb,
      HallInfo hall[], Rank rank[],
      PartialSum<Card>* ups,
      int mu[], int nu[]){
    ExecStatus es = ES_FIX;

    int rightmost = nb + 1; // rightmost accesible value in bounds
    int bsize     = nb + 2; // number of unique bounds including sentinels

    //Narrow lower bounds (UBC)

    /*
     * Initializing tree structure with the values from bounds
     * and the interval capacities of neighboured values
     * from left to right
     */


    hall[0].h = 0;
    hall[0].t = 0;
    hall[0].d = 0;

    for (int i = 1; i < bsize; i++) {
      int pred  = i - 1;
      hall[i].h = pred;
      hall[i].t = pred;
      hall[i].d = ups->sumup(hall[pred].bounds, hall[i].bounds - 1);
    }

    int n          = x.size();

    for (int i = 0; i < n; i++) {

      // visit intervals in increasing max order
      int x0   = rank[mu[i]].min;
      int succ = x0 + 1;
      int y    = rank[mu[i]].max;
      int z    = pathmax_t(hall, succ);
      int j    = hall[z].t;

      /* DOMINATION:
       *     v^i_j denotes
       *     unused values in the current interval. If the difference d
       *     between to critical capacities v^i_j and v^i_z
       *     is equal to zero, j dominates z
       *
       *     i.e. [hall[l].bounds, hall[nb+1].bounds] is not left-maximal and
       *     [hall[j].bounds, hall[l].bounds] is a Hall set iff
       *     [hall[j].bounds, hall[l].bounds] processing a variable x_i uses up a value in the interval
       *     [hall[z].bounds,hall[z+1].bounds] according to the intervals
       *     capacity. Therefore, if d = 0
       *     the considered value has already been used by processed variables
       *     m-times, where m = u[i] for value v_i. Since this value must not
       *     be reconsidered the path can be compressed
       */
      if (--hall[z].d == 0){
	hall[z].t = z + 1;
	z         = pathmax_t(hall, hall[z].t);
	if (z >= bsize) {
	  z--;
	}
	hall[z].t = j;
      }
      pathset_t(hall, succ, z, z); // path compression
      /* NEGATIVE CAPACITY:
       *     A negative capacity results in a failure.Since a
       *     negative capacity signals that the number of variables
       *     whose domain is contained in the set S is larger than
       *     the maximum capacity of S => UBC is not satisfiable,
       *     i.e. there are more variables than values to instantiate them
       */

      if (hall[z].d < ups->sumup(hall[y].bounds, hall[z].bounds - 1)){
	return ES_FAILED;
      }

      /* UPDATING LOWER BOUND:
       *   If the lower bound min_i lies inside a Hall interval [a,b]
       *   i.e. a <= min_i <=b <= max_i
       *   min_i is set to  min_i := b+1
       */
      if (hall[x0].h > x0) {
	int w       = pathmax_h(hall, hall[x0].h);
	int m       = hall[w].bounds;

	ModEvent me = x[mu[i]].gq(home, m);
	if (me_failed(me)) {
	  return ES_FAILED;
	}
	if (me_modified(me) && (m != x[mu[i]].min())) {
	  es = ES_NOFIX;
	}
	if (shared && me_modified(me)) {
	  es = ES_NOFIX;
	}
	pathset_h(hall, x0, w, w); // path compression
      }

      /* ZEROTEST:
       *     (using the difference between capacity pointers)
       *     zero capacity => the difference between critical capacity
       *     pointers is equal to the maximum capacity of the interval,i.e.
       *     the number of variables whose domain is contained in the
       *     interval is equal to the sum over all u[i] for a value v_i that
       *     lies in the Hall-Intervall which can also be thought of as a
       *     Hall-Set
       *
       *    ZeroTestLemma: Let k and l be succesive critical indices.
       *          v^i_k=0  =>  v^i_k = max_i+1-l+d
       *                   <=> v^i_k = y + 1 - z + d
       *                   <=> d = z-1-y
       *    if this equation holds the interval [j,z-1] is a hall intervall
       */

      if (hall[z].d == ups->sumup(hall[y].bounds, hall[z].bounds - 1)) {
	/*
	 *mark hall interval [j,z-1]
	 * hall pointers form a path to the upper bound of the interval
	 */
	int predj = j - 1;
	pathset_h(hall, hall[y].h, predj, y);
	hall[y].h = predj;
      }
    }

    /* Narrow upper bounds (UBC)
     * symmetric to the narrowing of the lower bounds
     */
    for (int i = 0; i < rightmost; i++) {
      int succ  = i + 1;
      hall[i].h = succ;
      hall[i].t = succ;
      hall[i].d = ups->sumup(hall[i].bounds, hall[succ].bounds - 1);
    }

    for (int i = n; i--; ) {
      // visit intervals in decreasing min order
      int x0   = rank[nu[i]].max;
      int pred = x0 - 1;
      int y    = rank[nu[i]].min;
      int z    = pathmin_t(hall, pred);
      int j    = hall[z].t;

      // DOMINATION:
      if (--hall[z].d == 0){
	hall[z].t = z - 1;
	z         = pathmin_t(hall, hall[z].t);
	hall[z].t = j;
      }
      pathset_t(hall, pred, z, z);

      // NEGATIVE CAPACITY:
      if (hall[z].d < ups->sumup(hall[z].bounds,hall[y].bounds-1)){
	return ES_FAILED;
      }

      /* UPDATING UPPER BOUND:
       *   If the upper bound max_i lies inside a Hall interval [a,b]
       *   i.e. min_i <= a <= max_i < b
       *   max_i is set to  max_i := a-1
       */
      if (hall[x0].h < x0) {
	int w       = pathmin_h(hall, hall[x0].h);
	int m       = hall[w].bounds - 1;
	ModEvent me = x[nu[i]].lq(home, m);
	if (me_failed(me)) {
	  return ES_FAILED;
	}
	if (me_modified(me) && (m != x[nu[i]].max())) {
	  es = ES_NOFIX;
	}
	if (me_modified(me) && shared) {
	  es = ES_NOFIX;
	}
	pathset_h(hall, x0, w, w);
      }
      // ZEROTEST
      if (hall[z].d == ups->sumup(hall[z].bounds, hall[y].bounds - 1)) {
	//mark hall interval [y,j]
	int succj = j + 1;
	pathset_h(hall, hall[y].h, succj, y);
	hall[y].h = succj;
      }
    }
    return es;
  }

}}}

// STATISTICS: int-prop