/*
 *  Main authors:
 *     Christian Schulte <schulte@gecode.org>
 *
 *  Contributing authors:
 *     Mikael Lagerkvist <lagerkvist@gecode.org>
 *
 *  Copyright:
 *     Christian Schulte, 2006
 *     Mikael Lagerkvist, 2006
 *
 *  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.
 *
 */

#include "gecode/iter.hh"

namespace Gecode { namespace Int { namespace Channel {

  /**
   * \brief Combine view with information for domain propagation
   *
   */
  template <class View>
  class DomInfo {
  public:
    View         view;
    unsigned int card;
    int          min;
    int          max;
    /// Allocate memory from space \a home for \a n elements
    static DomInfo<View>* allocate(Space* home, int n);
    /// Initialize
    void init(View x, int n);
    /// Update during cloning
    void update(Space* home, bool share, DomInfo<View>& vcb);
    /// Check whether propagation for assignment is to be done
    bool doval(void) const;
    /// Check whether propagation for domain is to be done
    bool dodom(void) const;
    /// Record that view got assigned
    void assigned(void);
    /// Record that one value got removed
    void removed(int i);
    /// Update the cardinality and bounds information after pruning
    void done(void);
  };

  template <class View>
  forceinline DomInfo<View>*
  DomInfo<View>::allocate(Space* home, int n) {
    return reinterpret_cast<DomInfo<View>*>
      (home->alloc(n*sizeof(DomInfo<View>)));
  }

  template <class View>
  forceinline void
  DomInfo<View>::init(View x, int n) {
    view = x;
    card = static_cast<unsigned int>(n);
    min  = 0;
    max  = n-1;
  }

  template <class View>
  forceinline void
  DomInfo<View>::update(Space* home, bool share, DomInfo<View>& di) {
    view.update(home,share,di.view);
    card = di.card;
    min  = di.min;
    max  = di.max;
  }

  template <class View>
  forceinline bool
  DomInfo<View>::doval(void) const {
    return (card != 1) && view.assigned();
  }

  template <class View>
  forceinline bool
  DomInfo<View>::dodom(void) const {
    return card != view.size();
  }

  template <class View>
  forceinline void
  DomInfo<View>::assigned(void) {
    card = 1;
  }

  template <class View>
  forceinline void
  DomInfo<View>::removed(int i) {
    card--;
    if (i == min)
      min++;
    else if (i == max)
      max--;
  }

  template <class View>
  forceinline void
  DomInfo<View>::done(void) {
    card = view.size();
    min  = view.min();
    max  = view.max();
  }

  // Propagate domain information from x to y
  template <class View>
  ExecStatus
  prop_dom(Space* home, int n, DomInfo<View>* x, DomInfo<View>* y,
	   ProcessStack& ya) {
    for (int i = n; i--; )
      // Only views with not yet propagated missing values
      if (x[i].dodom()) {
	// Iterate the values in the complement of x[i]
	ViewRanges<IntView>
	  xir(x[i].view);
	Iter::Ranges::ComplVal<ViewRanges<IntView> >
	  xirc(x[i].min,x[i].max,xir);
	Iter::Ranges::ToValues<Iter::Ranges::ComplVal<ViewRanges<IntView> > >
	  jv(xirc);
	while (jv()) {
	  // j is not in the domain of x[i], so prune i from y[j]
	  int j = jv.val();
	  ModEvent me = y[j].view.nq(home,i);
	  if (me_failed(me))
	    return ES_FAILED;
	  if (me_modified(me))
	    if (me == ME_INT_VAL) {
	      // Record that y[j] has been assigned and must be propagated
	      ya.push(j);
	    } else {
	      // Obvious as x[i] is different from j
	      y[j].removed(i);
	    }
	  ++jv;
	}
	// Update which values have been propagated and what are the new bounds
	x[i].done();
      }
    return ES_OK;
  }

  /*
   * The actual propagator
   *
   */
  template <class View>
  forceinline
  Dom<View>::Dom(Space* home, int n, DomInfo<View>* xy)
    : Base<DomInfo<View>,PC_INT_DOM>(home,n,xy,true) {}

  template <class View>
  forceinline
  Dom<View>::Dom(Space* home, bool share, Dom<View>& p)
    : Base<DomInfo<View>,PC_INT_DOM>(home,share,p) {}

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

  template <class View>
  PropCost
  Dom<View>::cost(void) const {
    return (View::pme(this) == ME_INT_VAL) ? PC_QUADRATIC_LO : PC_CUBIC_HI;
  }

  template <class View>
  ExecStatus
  Dom<View>::propagate(Space* home) {
    GECODE_AUTOARRAY(int, __xa, n+1);
    GECODE_AUTOARRAY(int, __ya, n+1);
    ProcessStack xa(__xa);
    ProcessStack ya(__ya);

    DomInfo<View>* x = xy;
    DomInfo<View>* y = xy+n;

    if (View::pme(this) == ME_INT_VAL) {
      // Scan x and y for assigned but not yet propagated views
      for (int i = n; i--; ) {
	if (x[i].doval()) xa.push(i);
	if (y[i].doval()) ya.push(i);
      }

      do {
	// Propagate assigned views for x
	if (prop_val<View,DomInfo<View> >(home,n,x,y,n_na,xa,ya) == ES_FAILED)
	  return ES_FAILED;
	// Propagate assigned views for y
	if (prop_val<View,DomInfo<View> >(home,n,y,x,n_na,ya,xa) == ES_FAILED)
	  return ES_FAILED;
	assert(ya.empty());
      } while (!xa.empty());
      this->ES_FIX_PARTIAL(View::pme(ME_INT_DOM));
    }

    // Process changed views for y
    // This propagates from y to x and possibly records xs that
    // got assigned
    if (prop_dom(home,n,y,x,xa) == ES_FAILED)
      return ES_FAILED;

    // Process assigned views for x
    if (prop_val<View,DomInfo<View> >(home,n,x,y,n_na,xa,ya) == ES_FAILED)
      return ES_FAILED;

    // Perform domain consistent propagation for distinct on the x views
    if (dc.available()) {
      GECODE_ES_CHECK(dc.sync());
    } else {
      GECODE_AUTOARRAY(View,xv,n);
      for (int i=n; i--; )
	xv[i] = x[i].view;
      GECODE_ES_CHECK(dc.init(n,&xv[0]));
    }
    dc.propagate(home);
    // This might assign some more views in x which goes unnoticed
    // (that is, not recorded in xa). This must be checked and propagated
    // to the y views, however the distinctness on x is already
    // propagated.
    for (int i=n; i--; )
      if (x[i].doval()) {
	int j = x[i].view.val();
	// Assign the y variable to i (or test if already assigned!)
	ModEvent me = y[j].view.eq(home,i);
	if (me_failed(me))
	  return ES_FAILED;
	if (me_modified(me)) {
	  // Record that y[j] has been assigned and must be propagated
	  assert(me == ME_INT_VAL);
	  // Otherwise the modification event would not be ME_INT_VAL
	  ya.push(j);
	}
	x[i].assigned(); n_na--;
      }

    // Process changed views for x
    // This propagates from x to y and possibly records ys that
    // got assigned
    if (prop_dom(home,n,x,y,ya) == ES_FAILED)
      return ES_FAILED;

    // Process assigned view again (some might have been found above)
    while (!xa.empty() || !ya.empty()) {
      // Process assigned views for x
      if (prop_val<View,DomInfo<View> >(home,n,x,y,n_na,xa,ya) == ES_FAILED)
	return ES_FAILED;
      // Process assigned views for y
      if (prop_val<View,DomInfo<View> >(home,n,y,x,n_na,ya,xa) == ES_FAILED)
	return ES_FAILED;
    };

    return (n_na == 0) ? ES_SUBSUMED : ES_FIX;
  }

  template <class View>
  ExecStatus
  Dom<View>::post(Space* home, int n, DomInfo<View>* xy) {
    assert(n > 0);
    if (n == 1) {
      GECODE_ME_CHECK(xy[0].view.eq(home,0));
      GECODE_ME_CHECK(xy[1].view.eq(home,0));
      return ES_OK;
    }
    for (int i=2*n; i--; ) {
      GECODE_ME_CHECK(xy[i].view.gq(home,0));
      GECODE_ME_CHECK(xy[i].view.le(home,n));
    }
    (void) new (home) Dom<View>(home,n,xy);
    return ES_OK;
  }

  template <class View>
  void
  Dom<View>::flush(void) {
    dc.flush();
  }

  template <class View>
  size_t
  Dom<View>::size(void) const {
    return dc.size();
  }

  template <class View>
  size_t
  Dom<View>::dispose(Space* home) {
    dc.dispose();
    (void) Base<DomInfo<View>,PC_INT_DOM>::dispose(home);
    return sizeof(*this);
  }


}}}

// STATISTICS: int-prop