/*
 *  Main authors:
 *     Christian Schulte <schulte@gecode.org>
 *
 *  Copyright:
 *     Christian Schulte, 2006
 *
 *  Last modified:
 *     $Date: 2006-09-06 15:51:28 +0200 (Wed, 06 Sep 2006) $ by $Author: schulte $
 *     $Revision: 3604 $
 *
 *  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 <algorithm>

#include "gecode/int/bool.hh"

namespace Gecode { namespace Int { namespace Linear {

  /*
   * Baseclass for integer Boolean sum
   *
   */
  template <class VX>
  forceinline
  LinBoolInt<VX>::LinBoolInt(Space* home, ViewArray<VX>& x0,
			     int n_s0, int c0)
    : Propagator(home), x(x0), n_s(n_s0), c(c0) {
    for (int i=n_s; i--; )
      x[i].subscribe(home,this,PC_INT_VAL);
  }

  template <class VX>
  size_t
  LinBoolInt<VX>::dispose(Space* home) {
    assert(!home->failed());
    for (int i=n_s; i--; )
      x[i].cancel(home,this,PC_INT_VAL);
    (void) Propagator::dispose(home);
    return sizeof(*this);
  }

  template <class VX>
  forceinline
  LinBoolInt<VX>::LinBoolInt(Space* home, bool share, LinBoolInt<VX>& p)
    : Propagator(home,share,p), x(home,p.x.size()), n_s(p.n_s) {
    // Update views not assigned and subscribed to
    for (int i=n_s; i--; )
      x[i].update(home,share,p.x[i]);
    // Eliminate assigned but not subscribed views in original
    // and update remaining ones
    int n_x = p.x.size();
    int p_c = p.c;
    for (int i=n_x; i-- > n_s; )
      if (p.x[i].zero()) {
	n_x--;
	p.x[i]=p.x[n_x]; x[i]=x[n_x];
      } else if (p.x[i].one()) {
	n_x--; p_c--;
	p.x[i]=p.x[n_x]; x[i]=x[n_x];
      } else {
	x[i].update(home,share,p.x[i]);
      }
    p.c = p_c; c = p_c;
    p.x.size(n_x); x.size(n_x);
  }

  template <class VX>
  PropCost
  LinBoolInt<VX>::cost(void) const {
    return cost_lo(x.size(),PC_LINEAR_LO);
  }


  /*
   * Less or equal propagator (integer rhs)
   *
   */

  template <class VX>
  forceinline
  GqBoolInt<VX>::GqBoolInt(Space* home, ViewArray<VX>& x,
			   int n_s, int c)
    : LinBoolInt<VX>(home,x,n_s,c) {}

  template <class VX>
  ExecStatus
  GqBoolInt<VX>::post(Space* home, ViewArray<VX>& x, int c) {
    if (c == 1)
      return Bool::NaryOrTrue<VX>::post(home,x);
    // Eliminate assigned views
    int n_x = x.size();
    for (int i=n_x; i--; )
      if (x[i].zero()) {
	x[i] = x[--n_x];
      } else if (x[i].one()) {
	x[i] = x[--n_x]; c--;
      }
    // RHS too large
    if (n_x < c)
      return ES_FAILED;
    // Whatever the x[i] take for values, the inequality is subsumed
    if (c <= 0)
      return ES_OK;
    // All views must be one to satisfy inequality
    if (c == n_x) {
      for (int i=n_x; i--; )
	x[i].t_one_none(home);
      return ES_OK;
    }
    // This is the needed invariant as c+1 subscriptions must be created
    assert(n_x > c);
    x.size(n_x);
    (void) new (home) GqBoolInt<VX>(home,x,c+1,c);
    return ES_OK;
  }

  template <class VX>
  forceinline
  GqBoolInt<VX>::GqBoolInt(Space* home, bool share, GqBoolInt<VX>& p)
    : LinBoolInt<VX>(home,share,p) {}

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

  template <class VX>
  ExecStatus
  GqBoolInt<VX>::propagate(Space* home) {
    // Eliminate assigned views from subscribed views
    int n_x = x.size();
    for (int i=n_s; i--; )
      if (x[i].zero()) {
	x[i]=x[--n_s]; x[n_s]=x[--n_x];
      } else if (x[i].one()) {
	x[i]=x[--n_s]; x[n_s]=x[--n_x]; c--;
      }
    x.size(n_x);
    if (n_x < c)
      return ES_FAILED;
    if (c <= 0)
      return ES_SUBSUMED;
    // Find unassigned variables to subscribe to
    while ((n_s < n_x) && (n_s <= c)) 
      if (x[n_s].zero()) {
	x[n_s]=x[--n_x];
      } else if (x[n_s].one()) {
	x[n_s]=x[--n_x]; c--;
      } else {
	x[n_s++].subscribe(home,this,PC_INT_VAL,false);
      }
    x.size(n_x);
    if (n_x < c)
      return ES_FAILED;
    if (c <= 0)
      return ES_SUBSUMED;
    if (c == n_x) {
      // These are known to be not assigned
      for (int i=n_s; i--; )
	x[i].t_one_none(home);
      // These are not known to be assigned
      for (int i=n_s+1; i<n_x; i++)
	x[i].t_one(home);
      // Fix number of subscriptions such that cancelling subscriptions work
      n_s = 0;
      return ES_SUBSUMED;
    }
    return ES_FIX;
  }


  /*
   * Equal propagator (integer rhs)
   *
   */
  template <class VX>
  forceinline
  EqBoolInt<VX>::EqBoolInt(Space* home, ViewArray<VX>& x,
			   int n_s, int c)
    : LinBoolInt<VX>(home,x,n_s,c) {}

  template <class VX>
  ExecStatus
  EqBoolInt<VX>::post(Space* home, ViewArray<VX>& x, int c) {
    // Eliminate assigned views
    int n_x = x.size();
    for (int i=n_x; i--; )
      if (x[i].zero()) {
	x[i] = x[--n_x];
      } else if (x[i].one()) {
	x[i] = x[--n_x]; c--;
      }
    // RHS too small or too large
    if ((c < 0) || (c > n_x))
      return ES_FAILED;
    // All views must be zero to satisfy equality
    if (c == 0) {
      for (int i=n_x; i--; )
	x[i].t_zero_none(home);
      return ES_OK;
    }
    // All views must be one to satisfy equality
    if (c == n_x) {
      for (int i=n_x; i--; )
	x[i].t_one_none(home);
      return ES_OK;
    }
    x.size(n_x);
    // Compute how many subscriptions must be created
    int n_s = std::max(c,n_x-c)+1;
    assert(n_s <= n_x);
    (void) new (home) EqBoolInt<VX>(home,x,n_s,c);
    return ES_OK;
  }

  template <class VX>
  forceinline
  EqBoolInt<VX>::EqBoolInt(Space* home, bool share, EqBoolInt<VX>& p)
    : LinBoolInt<VX>(home,share,p) {}

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

  template <class VX>
  ExecStatus
  EqBoolInt<VX>::propagate(Space* home) {
    // Eliminate assigned views from subscribed views
    int n_x = x.size();
    for (int i=n_s; i--; )
      if (x[i].zero()) {
	x[i]=x[--n_s]; x[n_s]=x[--n_x];
      } else if (x[i].one()) {
	x[i]=x[--n_s]; x[n_s]=x[--n_x]; c--;
      }
    x.size(n_x);
    if ((c < 0) || (c > n_x))
      return ES_FAILED;
    // Find unassigned variables to subscribe to
    while ((n_s < n_x) && ((n_s <= c) || (n_s <= n_x-c))) 
      if (x[n_s].zero()) {
	x[n_s]=x[--n_x];
      } else if (x[n_s].one()) {
	x[n_s]=x[--n_x]; c--;
      } else {
	x[n_s++].subscribe(home,this,PC_INT_VAL,false);
      }
    x.size(n_x);
    if ((c < 0) || (c > n_x))
      return ES_FAILED;
    if (c == 0) {
      // These are known to be not assigned
      for (int i=n_s; i--; )
	x[i].t_zero_none(home);
      // These are not known to be assigned
      for (int i=n_s+1; i<n_x; i++)
	x[i].t_zero(home);
      // Fix number of subscriptions such that cancelling subscriptions work
      n_s = 0;
      return ES_SUBSUMED;
    }
    if (c == n_x) {
      // These are known to be not assigned
      for (int i=n_s; i--; )
	x[i].t_one_none(home);
      // These are not known to be assigned
      for (int i=n_s+1; i<n_x; i++)
	x[i].t_one(home);
      // Fix number of subscriptions such that cancelling subscriptions work
      n_s = 0;
      return ES_SUBSUMED;
    }
    return ES_FIX;
  }


  /*
   * Integer disequal to Boolean sum
   *
   */

  template<class VX>
  forceinline
  NqBoolInt<VX>::NqBoolInt(Space* home, ViewArray<VX>& b, int c0)
    : BinaryPropagator<VX,PC_INT_VAL>(home,
				      b[b.size()-2],
				      b[b.size()-1]), x(b), c(c0) {
    assert(x.size() >= 2);
    x.size(x.size()-2);
  }

  template<class VX>
  forceinline
  NqBoolInt<VX>::NqBoolInt(Space* home, bool share, NqBoolInt<VX>& p)
    : BinaryPropagator<VX,PC_INT_VAL>(home,share,p), x(home,p.x.size()) {
    // Eliminate all zeros and ones in original and update
    int n = p.x.size();
    int p_c = p.c;
    for (int i=n; i--; )
      if (p.x[i].zero()) {
	n--; p.x[i]=p.x[n]; x[i]=x[n];
      } else if (p.x[i].one()) {
	n--; p_c--; p.x[i]=p.x[n]; x[i]=x[n];
      } else {
	x[i].update(home,share,p.x[i]);
      }
    c = p_c; p.c = p_c;
    x.size(n); p.x.size(n);
  }

  template<class VX>
  forceinline ExecStatus
  NqBoolInt<VX>::post(Space* home, ViewArray<VX>& x, int c) {
    int n = x.size();
    for (int i=n; i--; )
      if (x[i].one()) {
	x[i]=x[--n]; c--;
      } else if (x[i].zero()) {
	x[i]=x[--n];
      }
    x.size(n);
    if ((n < c) || (c < 0))
      return ES_OK;
    if (n == 0)
      return (c == 0) ? ES_FAILED : ES_OK;
    if (n == 1) {
      if (c == 1)
	x[0].t_zero_none(home);
      else
	x[0].t_one_none(home);
      return ES_OK;
    }
    (void) new (home) NqBoolInt(home,x,c);
    return ES_OK;
  }

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

  template<class VX>
  PropCost
  NqBoolInt<VX>::cost(void) const {
    return PC_LINEAR_LO;
  }

  template<class VX>
  forceinline bool
  NqBoolInt<VX>::resubscribe(Space* home, VX& y) {
    if (y.one())
      c--;
    int n = x.size();
    for (int i=n; i--; )
      if (x[i].one()) {
	c--; x[i]=x[--n];
      } else if (x[i].zero()) {
	x[i] = x[--n];
      } else {
	// New unassigned view found
	assert(!x[i].zero() && !x[i].one());
	// Move to y and subscribe
	y=x[i]; x[i]=x[--n]; 
	x.size(n);
	y.subscribe(home,this,PC_INT_VAL,false);
	return true;
      }
    // All views have been assigned!
    x.size(0);
    return false;
  }

  template<class VX>
  ExecStatus
  NqBoolInt<VX>::propagate(Space* home) {
    bool s0 = true; 
    if (x0.zero() || x0.one())
      s0 = resubscribe(home,x0);
    bool s1 = true;
    if (x1.zero() || x1.one())
      s1 = resubscribe(home,x1);
    int n = x.size() + s0 + s1;
    if ((n < c) || (c < 0))
      return ES_SUBSUMED;
    if (n == 0)
      return (c == 0) ? ES_FAILED : ES_SUBSUMED;
    if (n == 1) {
      if (s0) {
	if (c == 1)
	  x0.t_zero_none(home);
	else
	  x0.t_one_none(home);
      } else {
	assert(s1);
	if (c == 1)
	  x1.t_zero_none(home);
	else
	  x1.t_one_none(home);
      }
      return ES_SUBSUMED;
    }
    return ES_FIX;
  }


}}}

// STATISTICS: int-prop