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


  /*
   * Summary of the propagation algorithm as implemented in the
   * propagate method below:
   *
   * STEP 1: Normalize the domains of the y variables
   * STEP 2: Sort the domains of the x variables according to their lower
   *         and upper endpoints
   * STEP 3: Compute the matchings phi and phiprime with
   *         Glover's matching algorithm
   * STEP 4: Compute the strongly connected components in
   *         the oriented intersection graph
   * STEP 5: Narrow the domains of the variables
   *
   */

  /**
   * \brief Perform bounds consistent sortedness propagation
   *
   * Implements the propagation algorithm for Sortedness::Sortedness
   * and is provided as seperate function, because a second pass of
   * the propagation algorithm is needed in order to achieve idempotency
   * in case explicit permutation variables are provided.
   *
   * If \a Perm is true, permutation variables form the
   * third argument which implies additional inferences,
   * consistency check on the permutation variables and eventually a
   * second pass of the propagation algorithm.
   * Otherwise, the algorithm does not take care of the permutation
   * variables resulting in a better performance.
   */

  template<class View, class Tuple, bool Perm>
  ExecStatus
  bounds_propagation(Space* home,
		     ViewArray<Tuple>& xz,
		     ViewArray<View>& y,
		     bool& repairpass,
		     bool& nofix,
		     bool& match_fixed){

    int n        = xz.size();

    GECODE_AUTOARRAY(int, tau,      n);
    GECODE_AUTOARRAY(int, phi,      n);
    GECODE_AUTOARRAY(int, phiprime, n);
    GECODE_AUTOARRAY(OfflineMinItem, sequence, n);
    GECODE_AUTOARRAY(int, vertices, n);

    if (match_fixed) {
      // sorting is determined
      // sigma and tau coincide
      for (int i = xz.size(); i--; ) {
	int pi = xz[i][1].val();
	tau[pi] = i;
      }
    } else {
      for (int i = n; i--; ) {
	tau[i] = i;
      }
    }

    bool yval    = true;
    bool ysorted = true;
    for (int i = n; i--; ) {
      yval    &= y[i].assigned();
      if (i) {
	ysorted &= (y[i].min() <= y[i - 1].min() &&
		    y[i].max() <= y[i - 1].max());
      }
    }

    if (Perm) {

      // normalized and sorted
      // collect all bounds

      // minimum bound
      int mib = y[0].min();
      // maximum bound
      int mab = y[n - 1].max();
      // interval size
      int ivs = (mab - mib + 1);
      GECODE_AUTOARRAY(Rank, allbnd, ivs);
      int iter = mib;
      int idx = 0;
      while(iter <= mab && idx < n) {
	if (y[idx].min() > iter) {
	  // idx cannot be zero because consisteny in posting
	  assert(idx > 0);
	  allbnd[iter - mib].min = idx;
	  allbnd[iter - mib].max = idx - 1;
	  iter++;
	} else {
	  if (y[idx].min() <= iter && iter <= y[idx].max() ) {
	    allbnd[iter - mib].min = idx;
	    allbnd[iter - mib].max = idx;
	    iter++;
	  } else {
	    idx++;
	  }
	}
      }

      iter = mab;
      idx = n -1;
      while(iter >= mib && idx >= 0) {
	if (y[idx].min() > iter) {
	  // idx cannot be zero because consisteny in posting
	  assert(idx > 0);
	  allbnd[iter - mib].max = idx - 1;
	  iter--;
	} else {
	  if (y[idx].min() <= iter && iter <= y[idx].max() ) {
	    allbnd[iter - mib].max = idx;
	    iter--;
	  } else {
	    idx--;
	  }
	}
      }

      for (int i = n; i--; ) {
	// minimum reachable y-variable
	int minr = allbnd[xz[i][0].min() - mib].min;
	int maxr = allbnd[xz[i][0].max() - mib].max;

	ModEvent me = xz[i][0].gq(home, y[minr].min());
	if (me_failed(me)) {
	  return ES_FAILED;
	}
	nofix |= (me_modified(me) &&
		  xz[i][0].min() != y[minr].min());

	me = xz[i][0].lq(home, y[maxr].max());
	if (me_failed(me)) {
	  return ES_FAILED;
	}
	nofix |= (me_modified(me) &&
		  xz[i][0].min() != y[maxr].max());

	me = xz[i][1].gq(home, minr);
	if (me_failed(me)) {
	  return ES_FAILED;
	}
	nofix |= (me_modified(me) &&  xz[i][1].min() != minr);

	me = xz[i][1].lq(home, maxr);
	if (me_failed(me)) {
	  return ES_FAILED;
	}
	nofix |= (me_modified(me) &&  xz[i][1].max() != maxr);

      }

      // channel information from x to y through permutation variables in z
      if (!channel<View, Tuple, Perm>(home, xz, y, nofix)) {
	return ES_FAILED;
      }
      if (nofix) {
	return ES_NOFIX;
      }
    }

    /*
     * STEP 1:
     *  normalization is implemented in "sortedness/order.icc"
     *    o  setting the lower bounds of the y_i domains (\lb E_i)
     *       to max(\lb E_{i-1},\lb E_i)
     *    o  setting the upper bounds of the y_i domains (\ub E_i)
     *       to min(\ub E_i,\ub E_{i+1})
     */

    if (!normalize<View, Tuple>(home, y, xz, nofix)) {
      return ES_FAILED;
    }

    if (Perm) {
      // check consistency of channeling after normalization
      if (!channel<View, Tuple, Perm>(home, xz, y, nofix)) {
	return ES_FAILED;
      }
      if (nofix) {
	return ES_NOFIX;
      }
    }


    // if bounds have changed we have to recreate sigma to restore
    // optimized dropping of variables

    sort_sigma<View, Tuple, Perm>(xz, match_fixed);

    bool subsumed   = true;
    bool array_subs = false;
    int  dropfst  = 0;
    bool noperm_bc = false;

    if (!(check_subsumption<View, Tuple, Perm>
	  (home, xz, y, subsumed, dropfst)) ||
	!(array_assigned<View, Tuple, Perm>
	  (home, xz, y, array_subs, match_fixed, nofix, noperm_bc))) {
      return ES_FAILED;
    }

    if (subsumed || array_subs) {
      return ES_SUBSUMED;
    }


    /*
     * STEP 2: creating tau
     * Sort the domains of the x variables according
     * to their lower bounds, where we use an
     * intermediate array of integers for sorting
     */
    sort_tau<View, Tuple, Perm>(xz, tau);

    /*
     * STEP 3:
     *  Compute the matchings \phi and \phi' between
     *  the x and the y variables
     *  with Glover's matching algorithm.
     *        o  phi is computed with the glover function
     *        o  phiprime is computed with the revglover function
     *  glover and revglover are implemented in "sortedness/matching.icc"
     */

    if (!match_fixed) {
      if (!glover<View, Tuple, Perm>
	  (home, xz, y, tau, phi, sequence, vertices)) {
	return ES_FAILED;
      }
    } else {
      for (int i = xz.size(); i--; ) {
	phi[i]      = xz[i][1].val();
	phiprime[i] = phi[i];
      }
    }

    if(!yval) {
      // phiprime is not needed to narrow the domains of the x-variables
      if (!match_fixed) {
	if (!revglover<View, Tuple, Perm>
	    (home, xz, y, tau, phiprime, sequence, vertices)) {
	  return ES_FAILED;
	}
      }

      if (!narrow_domy<View, Tuple, Perm>
	  (home, xz, y, phi, phiprime, nofix)) {
	return ES_FAILED;
      }

      if (nofix && !match_fixed) {
	// data structures (matching) destroyed by domains with holes
	
	for (int i = y.size(); i--; ) {
	  phi[i] = 0;
	  phiprime[i] = 0;
	}
	if (!glover<View, Tuple, Perm>
	    (home, xz, y, tau, phi, sequence, vertices)) {
	  return ES_FAILED;
	}
	
	if (!revglover<View, Tuple, Perm>
	    (home, xz, y, tau, phiprime, sequence, vertices)) {
	  return ES_FAILED;
	}

	if (!narrow_domy<View, Tuple, Perm>
	    (home, xz, y, phi, phiprime, nofix)) {
	  return ES_FAILED;
	}
      }
    }

    /*
     * STEP 4:
     *  Compute the strongly connected components in
     *  the oriented intersection graph
     *  the computation of the sccs is implemented in
     *  "sortedness/narrowing.icc" in the function narrow_domx
     */

    GECODE_AUTOARRAY(int,          scclist, n);
    GECODE_AUTOARRAY(SccComponent, sinfo  , n);

    for(int i = n; i--; ) {
      sinfo[i].left       = i;
      sinfo[i].right      = i;
      sinfo[i].rightmost  = i;
      sinfo[i].leftmost   = i;
    }

    computesccs<View>(home, xz, y, phi, sinfo, scclist);

    /*
     * STEP 5:
     *  Narrow the domains of the variables
     *  Also implemented in "sortedness/narrowing.icc"
     *  in the functions narrow_domx and narrow_domy
     */

    if (!narrow_domx<View, Tuple, Perm>
	(home, xz, y, tau, phi, scclist, sinfo, nofix)) {
      return ES_FAILED;
    }

    if (Perm) {
      if (!noperm_bc) {
	if (!perm_bc<View, Tuple, Perm>
	    (home, tau, sinfo, scclist, xz, repairpass, nofix)) {
	  return ES_FAILED;
	}
      }

      // channeling also needed after normal propagation steps
      // in order to ensure consistency after possible modification in perm_bc
      if (!channel<View, Tuple, Perm>(home, xz, y, nofix)) {
	return ES_FAILED;
      }
      if (nofix) {
	return ES_NOFIX;
      }
    }

    sort_tau<View, Tuple, Perm>(xz, tau);

    if (Perm) {
      // special case of sccs of size 2 denoted by permutation variables
      // used to enforce consistency from x to y
      // case of the upper bound ordering tau
      for (int i = xz.size() - 1; i--; ) {
	// two x variables are in the same scc of size 2
	if (xz[tau[i]][1].min() == xz[tau[i+1]][1].min() &&
	    xz[tau[i]][1].max() == xz[tau[i+1]][1].max() &&
	    xz[tau[i]][1].size() == 2 && xz[tau[i]][1].range()) {
	  // if bounds are strictly smaller
	  if (xz[tau[i]][0].max() < xz[tau[i+1]][0].max()) {
	    ModEvent me = y[xz[tau[i]][1].min()].lq(home, xz[tau[i]][0].max());
	    if (me_failed(me)) {
	      return ES_FAILED;
	    }
	    nofix |= (y[xz[tau[i]][1].min()].modified() &&
		      y[xz[tau[i]][1].min()].max() != xz[tau[i]][0].max());
	
	    me = y[xz[tau[i+1]][1].max()].lq(home, xz[tau[i+1]][0].max());
	    if (me_failed(me)) {
	      return ES_FAILED;
	    }
	    nofix |= (y[xz[tau[i+1]][1].max()].modified() &&
		      y[xz[tau[i+1]][1].max()].max() != xz[tau[i+1]][0].max());
	  }
	}
      }
    }
    return nofix ? ES_NOFIX : ES_FIX;
  }

  template<class View, class Tuple, bool Perm>
  forceinline Sortedness<View, Tuple, Perm>::
  Sortedness(Space* home, bool share, Sortedness<View, Tuple, Perm>& p):
    Propagator(home, share, p),
    reachable(p.reachable) {
    xz.update(home, share, p.xz);
    y.update(home, share, p.y);
    w.update(home, share, p.w);
  }

  template<class View, class Tuple, bool Perm>
  Sortedness<View, Tuple, Perm>::
  Sortedness(Space* home, ViewArray<Tuple>& xz0, ViewArray<View>& y0):
    Propagator(home), xz(xz0), y(y0), w(home, y0), reachable(-1) {
    xz.subscribe(home, this, PC_INT_BND);
    y.subscribe(home, this, PC_INT_BND);

  }

  template<class View, class Tuple, bool Perm>
  size_t
  Sortedness<View, Tuple, Perm>::dispose(Space* home) {
    assert(!home->failed());
    xz.cancel(home,this, PC_INT_BND);
    y.cancel(home,this, PC_INT_BND);
    (void) Propagator::dispose(home);
    return sizeof(*this);
  }

  template<class View, class Tuple, bool Perm>
  Actor* Sortedness<View, Tuple, Perm>::copy(Space* home, bool share) {
    return new (home) Sortedness<View, Tuple, Perm>(home, share, *this);
  }

  template<class View, class Tuple, bool Perm>
  PropCost Sortedness<View, Tuple, Perm>::cost(void) const {
    return cost_hi(xz.size(), PC_LINEAR_HI);
  }

  template<class View, class Tuple, bool Perm>
  ExecStatus
  Sortedness<View, Tuple, Perm>::propagate(Space* home) {

    int  n           = xz.size();
    bool secondpass  = false;
    bool nofix       = false;
    int  dropfst     = 0;

    bool subsumed    = false;
    bool array_subs  = false;
    bool match_fixed = false;

    // normalization of x and y
    if (!normalize<View, Tuple>(home, y, xz, nofix)) {
      return ES_FAILED;
    }

    // create sigma sorting
    sort_sigma<View, Tuple, Perm>(xz, match_fixed);

    bool noperm_bc = false;
    if (!array_assigned<View, Tuple, Perm>
	(home, xz, y, array_subs, match_fixed, nofix, noperm_bc)) {
      return ES_FAILED;
    }

    if (array_subs) {
      return ES_SUBSUMED;
    }

    sort_sigma<View, Tuple, Perm>(xz, match_fixed);

    // in this case check_subsumptions is guaranteed to find
    // the xs ordered by sigma

    if (!check_subsumption<View, Tuple, Perm>
	(home, xz, y, subsumed, dropfst)) {
      return ES_FAILED;
    }

    if (subsumed) {
      return ES_SUBSUMED;
    }	

    if (Perm) {
      // dropping possibly yields inconsistent indices on permutation variables
      if (dropfst) {
	reachable = w[dropfst - 1].max();
	bool unreachable = true;
	for (int i = xz.size(); unreachable && i-- ; ) {
	  unreachable &= (reachable < xz[i][0].min());
	}

	if (unreachable) {
	  xz.drop_fst(dropfst, home, this, PC_INT_BND);
	  y.drop_fst (dropfst, home, this, PC_INT_BND);
	} else {
	  dropfst = 0;
	}
      }

      n = xz.size();

      if (n < 2) {
	if (xz[0][0].max() < y[0].min() || y[0].max() < xz[0][0].min()) {
	  return ES_FAILED;
	} else {
	  if (Perm) {
	    GECODE_ME_CHECK(xz[0][1].eq(home, w.size() - 1));
	  }
	  Rel::EqBnd<View,View>::post(home, xz[0][0], y[0]);
	  return ES_SUBSUMED;

	}
      }

      // check whether shifting the permutation variables
      // is necessary after dropping x and y vars
      // highest reachable index
      int  valid = n - 1;
      int  index = 0;
      int  shift = 0;

      for (int i = n; i--; ){
	if (xz[i][1].max() > index) {
	  index = xz[i][1].max();
	}
	if (index > valid) {
	  shift = index - valid;
	}
      }

      if (shift) {
     	ViewArray<ViewTuple<OffsetView,2> > oxz(home, n);
	ViewArray<OffsetView> oy(home, n);

	for (int i = n; i--; ) {

	  GECODE_ME_CHECK(xz[i][1].gq(home, shift));

	  oxz[i][1] = OffsetView(xz[i][1], -shift);
	  oxz[i][0] = OffsetView(xz[i][0], 0);
	  oy[i] = OffsetView(y[i], 0);
	}

	GECODE_ES_CHECK((bounds_propagation<OffsetView,
			 ViewTuple<OffsetView,2>, Perm>
			 (home, oxz, oy, secondpass, nofix, match_fixed)));

	if (secondpass) {
	  GECODE_ES_CHECK((bounds_propagation<OffsetView,
			   ViewTuple<OffsetView,2>, Perm>
			   (home, oxz, oy, secondpass, nofix, match_fixed)));
	}
      } else {
	GECODE_ES_CHECK((bounds_propagation<View, Tuple, Perm>
			 (home, xz, y, secondpass, nofix, match_fixed)));

	if (secondpass) {
	  GECODE_ES_CHECK((bounds_propagation<View, Tuple, Perm>
			   (home, xz, y, secondpass, nofix, match_fixed)));
	}
      }
    } else {
      // dropping has no consequences
      if (dropfst) {
	xz.drop_fst(dropfst, home, this, PC_INT_BND);
	y.drop_fst (dropfst, home, this, PC_INT_BND);
      }

      n = xz.size();

      if (n < 2) {
	if (xz[0][0].max() < y[0].min() || y[0].max() < xz[0][0].min()) {
	  return ES_FAILED;
	} else {
	  Rel::EqBnd<View,View>::post(home, xz[0][0], y[0]);
	  return ES_SUBSUMED;
	}
      }
      GECODE_ES_CHECK((bounds_propagation<View, Tuple, Perm>
		       (home, xz, y, secondpass, nofix, match_fixed)));
      // no second pass possible if there are no permvars
    }

    if (!normalize<View, Tuple>(home, y, xz, nofix)) {
      return ES_FAILED;
    }

    GECODE_AUTOARRAY(int, tau,      n);
    if (match_fixed) {
      // sorting is determined
      // sigma and tau coincide
      for (int i = xz.size(); i--; ) {
	int pi = xz[i][1].val();
	tau[pi] = i;
      }
    } else {
      for (int i = n; i--; ) {
	tau[i] = i;
      }
    }

    sort_tau<View, Tuple, Perm>(xz, tau);
    // recreate consistency for already assigned subparts
    // in order of the upper bounds starting at the end of the array
    bool xbassigned = true;
    for (int i = xz.size(); i--; ) {
      if (xz[tau[i]][0].assigned() && xbassigned) {
	ModEvent me = y[i].eq(home, xz[tau[i]][0].val());
	if (me_failed(me)) {
	  return ES_FAILED;
	}
      } else {
	xbassigned = false;
      }
    }

    subsumed   = true;
    array_subs = false;
    noperm_bc  = false;

    // creating sorting anew
    sort_sigma<View, Tuple, Perm>(xz, match_fixed);

    if (Perm) {
      for (int i = 0; i < xz.size() - 1; i++) {
	// special case of subsccs of size2 for the lower bounds
	// two x variables are in the same scc of size 2
	if (xz[i][1].min() == xz[i+1][1].min() &&
	    xz[i][1].max() == xz[i+1][1].max() &&
	    xz[i][1].size() == 2 && xz[i][1].range()) {
	  if (xz[i][0].min() < xz[i+1][0].min()) {
	    ModEvent me = y[xz[i][1].min()].gq(home, xz[i][0].min());
	    if (me_failed(me)) {
	      return ES_FAILED;
	    }
	    nofix |= (y[xz[i][1].min()].modified() &&
		      y[xz[i][1].min()].min() != xz[i][0].min());

	    me = y[xz[i+1][1].max()].gq(home, xz[i+1][0].min());
	    if (me_failed(me)) {
	      return ES_FAILED;
	    }
	    nofix |= (y[xz[i+1][1].max()].modified() &&
		      y[xz[i+1][1].max()].min() != xz[i+1][0].min());
	  }
	}
      }
    }

    // check assigned
    // should be sorted
    bool xassigned = true;
    for (int i = 0; i < xz.size(); i++) {
      if (xz[i][0].assigned() && xassigned) {
	ModEvent me = y[i].eq(home, xz[i][0].val());
	if (me_failed(me)) {
	  return ES_FAILED;
	}
      } else {
	xassigned = false;
      }
    }

    // sorted check bounds
    // final check that variables are consitent with least and greatest possible
    // values
    int tlb = std::min(xz[0][0].min(), y[0].min());
    int tub = std::max(xz[xz.size() - 1][0].max(), y[y.size() - 1].max());
    for (int i = xz.size(); i--; ) {
      ModEvent me = y[i].lq(home, tub);
      if (me_failed(me)) {
	return ES_FAILED;
      }
      nofix |= y[i].modified() && y[i].max() != tub;

      me = y[i].gq(home, tlb);
      if (me_failed(me)) {
	return ES_FAILED;
      }
      nofix |= y[i].modified() && y[i].min() != tlb;

      me = xz[i][0].lq(home, tub);
      if (me_failed(me)) {
	return ES_FAILED;
      }
      nofix |= xz[i][0].modified() && xz[i][0].max() != tub;

      me = xz[i][0].gq(home, tlb);
      if (me_failed(me)) {
	return ES_FAILED;
      }
      nofix |= xz[i][0].modified() && xz[i][0].min() != tlb;
    }

    if (!array_assigned<View, Tuple, Perm>
	(home, xz, y, array_subs, match_fixed, nofix, noperm_bc)) {
      return ES_FAILED;
    }

    if (array_subs) {
      return ES_SUBSUMED;
    }

    if (!check_subsumption<View, Tuple, Perm>
	(home, xz, y, subsumed, dropfst)) {
      return ES_FAILED;
    }

    if (subsumed) {
      return ES_SUBSUMED;
    }

    return nofix ? ES_NOFIX : ES_FIX;
  }

  template<class View, class Tuple, bool Perm>
  ExecStatus
  Sortedness<View, Tuple, Perm>::
  post(Space* home, ViewArray<Tuple>& xz0, ViewArray<View>& y0) {
    int n = xz0.size();
    if (n < 2) {
      if ((xz0[0][0].max() < y0[0].min()) || (y0[0].max() < xz0[0][0].min())) {
	return ES_FAILED;
      } else {
	Rel::EqBnd<View,View>::post(home, xz0[0][0], y0[0]);
	if (Perm) {
	  GECODE_ME_CHECK(xz0[0][1].eq(home, 0));
	}
      }
    } else {
      new (home) Sortedness<View, Tuple, Perm>(home, xz0, y0);
    }
    return ES_OK;
  }

}}}

// STATISTICS: int-prop