/*
 *  Main authors:
 *     Christian Schulte <schulte@gecode.org>
 *
 *  Copyright:
 *     Christian Schulte, 2004
 *
 *  Last modified:
 *     $Date: 2006-09-11 11:34:58 +0200 (Mon, 11 Sep 2006) $ by $Author: schulte $
 *     $Revision: 3646 $
 *
 *  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 Bool {

  /*
   * Boolean disjunction propagator (true)
   *
   */

  template <class BVA, class BVB>
  forceinline
  OrTrue<BVA,BVB>::OrTrue(Space* home, BVA b0, BVB b1)
    : BoolBinary<BVA,BVB>(home,b0,b1) {}

  template <class BVA, class BVB>
  forceinline
  OrTrue<BVA,BVB>::OrTrue(Space* home, bool share, OrTrue<BVA,BVB>& p)
    : BoolBinary<BVA,BVB>(home,share,p) {}

  template <class BVA, class BVB>
  forceinline
  OrTrue<BVA,BVB>::OrTrue(Space* home, bool share, Propagator& p,
			      BVA b0, BVB b1)
    : BoolBinary<BVA,BVB>(home,share,p,b0,b1) {}

  template <class BVA, class BVB>
  inline ExecStatus
  OrTrue<BVA,BVB>::post(Space* home, BVA b0, BVB b1) {
    switch (bool_test(b0,b1)) {
    case BT_SAME:
      GECODE_ME_CHECK(b0.t_one(home));
      break;
    case BT_COMP:
      break;
    case BT_NONE:
      if (b0.zero()) {
	GECODE_ES_CHECK(b1.t_one(home));
      } else if (b1.zero()) {
	GECODE_ES_CHECK(b0.t_one(home));
      } else if (!b0.one() && !b1.one()) {
	(void) new (home) OrTrue<BVA,BVB>(home,b0,b1);
      }
      break;
    default: GECODE_NEVER;
    }
    return ES_OK;
  }

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

  template <class BVA, class BVB>
  ExecStatus
  OrTrue<BVA,BVB>::propagate(Space* home) {
    if (x0.zero()) {
      GECODE_ME_CHECK(x1.t_one(home));
    } else if (x1.zero()) {
      GECODE_ME_CHECK(x0.t_one(home));
    } else {
      assert(x0.one() || x1.one());
    }
    return ES_SUBSUMED;
  }


  /*
   * Boolean disjunction propagator
   *
   */

  template <class BVA, class BVB, class BVC>
  forceinline
  Or<BVA,BVB,BVC>::Or(Space* home, BVA b0, BVB b1, BVC b2)
    : BoolTernary<BVA,BVB,BVC>(home,b0,b1,b2) {}

  template <class BVA, class BVB, class BVC>
  forceinline
  Or<BVA,BVB,BVC>::Or(Space* home, bool share, Or<BVA,BVB,BVC>& p)
    : BoolTernary<BVA,BVB,BVC>(home,share,p) {}

  template <class BVA, class BVB, class BVC>
  forceinline
  Or<BVA,BVB,BVC>::Or(Space* home, bool share, Propagator& p,
			BVA b0, BVB b1, BVC b2)
    : BoolTernary<BVA,BVB,BVC>(home,share,p,b0,b1,b2) {}

  template <class BVA, class BVB, class BVC>
  inline ExecStatus
  Or<BVA,BVB,BVC>::post(Space* home, BVA b0, BVB b1, BVC b2) {
    if (b2.zero()) {
      GECODE_ME_CHECK(b0.t_zero(home));
      GECODE_ME_CHECK(b1.t_zero(home));
    } else if (b2.one()) {
      return OrTrue<BVA,BVB>::post(home,b0,b1);
    } else {
      switch (bool_test(b0,b1)) {
      case BT_SAME:
	return Eq<BVA,BVC>::post(home,b0,b2);
      case BT_COMP:
	GECODE_ME_CHECK(b2.t_one(home));
	break;
      case BT_NONE:
	if (b0.one() || b1.one()) {
	  GECODE_ME_CHECK(b2.t_one(home));
	} else if (b0.zero()) {
	  return Eq<BVB,BVC>::post(home,b1,b2);
	} else if (b1.zero()) {
	  return Eq<BVA,BVC>::post(home,b0,b2);
	} else {
	  (void) new (home) Or<BVA,BVB,BVC>(home,b0,b1,b2);
	}
	break;
      default: GECODE_NEVER;
      }
    }
    return ES_OK;
  }

  template <class BVA, class BVB, class BVC>
  Actor*
  Or<BVA,BVB,BVC>::copy(Space* home, bool share) {
    return new (home) Or<BVA,BVB,BVC>(home,share,*this);
  }

  template <class BVA, class BVB, class BVC>
  ExecStatus
  Or<BVA,BVB,BVC>::propagate(Space* home) {
    if (x0.one() || x1.one()) {
      GECODE_ES_CHECK(x2.t_one(home));
    } else if (x2.zero()) {
      GECODE_ES_CHECK(x0.t_zero(home));
      GECODE_ES_CHECK(x1.t_zero(home));
    } else if (x2.one()) {
      if (x0.zero()) {
	GECODE_ES_CHECK(x1.t_one(home));
      } else if (x1.zero()) {
	GECODE_ES_CHECK(x0.t_one(home));
      } else {
	return ES_FIX;
      }	
    } else if (x0.zero() && x1.zero()) {
      GECODE_ES_CHECK(x2.t_zero(home));
    } else {
      return ES_FIX;
    }
    return ES_SUBSUMED;
  }



  /*
   * N-ary Boolean disjunction propagator (true)
   *
   */

  template<class View>
  forceinline
  NaryOrTrue<View>::NaryOrTrue(Space* home, ViewArray<View>& b)
    : BinaryPropagator<View,PC_INT_VAL>(home,
					b[b.size()-2],
					b[b.size()-1]), x(b) {
    assert(x.size() > 2);
    x.size(x.size()-2);
  }

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

  template<class View>
  forceinline
  NaryOrTrue<View>::NaryOrTrue(Space* home, bool share, NaryOrTrue<View>& p)
    : BinaryPropagator<View,PC_INT_VAL>(home,share,p), x(home,p.x.size()) {
    // Eliminate all zeros and all but one ones in original and update
    int n = p.x.size();
    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()) {
	x[i].update(home,share,p.x[i]);
	// Now eliminate all remaining zeros and ones
	while (i--)
	  if (p.x[i].zero() || p.x[i].one()) {
	    n--; p.x[i]=p.x[n]; x[i]=x[n];
	  } else {
	    x[i].update(home,share,p.x[i]);
	  }
	goto done;
      } else {
	x[i].update(home,share,p.x[i]);
      }
    done:
    x.size(n); p.x.size(n);
  }

  template<class View>
  inline ExecStatus
  NaryOrTrue<View>::post(Space* home, ViewArray<View>& b) {
    for (int i=b.size(); i--; )
      if (b[i].one())
	return ES_OK;
      else if (b[i].zero())
	b.move_lst(i);
    if (b.size() == 0)
      return ES_FAILED;
    b.unique();
    if (b.size() == 1) {
      GECODE_ME_CHECK(b[0].t_one(home));
    } else if (b.size() == 2) {
      return OrTrue<View,View>::post(home,b[0],b[1]);
    } else {
      (void) new (home) NaryOrTrue(home,b);
    }
    return ES_OK;
  }

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

  template<class View>
  forceinline ExecStatus
  NaryOrTrue<View>::resubscribe(Space* home, View& x0, View x1) {
    if (x0.zero()) {
      int n = x.size();
      for (int i=n; i--; )
	if (x[i].one()) {
	  x.size(n);
	  return ES_SUBSUMED;
	} else if (x[i].zero()) {
	  x[i] = x[--n];
	} else {
	  // New unassigned view found
	  assert(!x[i].zero() && !x[i].one());
	  // Rewrite if there is just one view left
	  if (i == 0) {
	    View y = x[0];
	    x.size(0);
	    GECODE_ES_CHECK((OrTrue<View,View>::post(home,x1,y)));
	    return ES_SUBSUMED;
	  }
	  // Move to x0 and subscribe
	  x0=x[i]; x[i]=x[--n]; 
	  x.size(n);
	  x0.subscribe(home,this,PC_INT_VAL,false);
	  return ES_FIX;
	}
      // All views have been assigned!
      x.size(0);
      GECODE_ME_CHECK(x1.t_one(home));
      return ES_SUBSUMED;
    }
    return ES_FIX;
  }

  template<class View>
  ExecStatus
  NaryOrTrue<View>::propagate(Space* home) {
    if (x0.one() || x1.one())
      return ES_SUBSUMED;
    ExecStatus e = resubscribe(home,x0,x1);
    if (e != ES_FIX)
      return e;
    return resubscribe(home,x1,x0);
  }


  /*
   * N-ary Boolean disjunction propagator
   *
   */

  template<class View>
  forceinline
  NaryOr<View>::NaryOr(Space* home, ViewArray<View>& b, View c)
    : NaryOnePropagator<View,PC_INT_VAL>(home,b,c) {}

  template<class View>
  forceinline
  NaryOr<View>::NaryOr(Space* home, bool share, NaryOr<View>& p)
    : NaryOnePropagator<View,PC_INT_VAL>(home,share,p) {}

  template<class View>
  inline ExecStatus
  NaryOr<View>::post(Space* home, ViewArray<View>& b, View c) {
    if (c.one())
      return NaryOrTrue<View>::post(home,b);
    if (c.zero()) {
      for (int i=b.size(); i--; )
	GECODE_ME_CHECK(b[i].t_zero(home));
      return ES_OK;
    }
    for (int i=b.size(); i--; )
      if (b[i].one()) {
	GECODE_ME_CHECK(c.t_one(home));
	return ES_OK;
      } else if (b[i].zero()) {
	b.move_lst(i);
      }
    if (b.size() == 0)
      return ES_FAILED;
    b.unique();
    if (b.size() == 1)
      return Eq<View,View>::post(home,b[0],c);
    if (b.size() == 2)
      return Or<View,View,View>::post(home,b[0],b[1],c);
    (void) new (home) NaryOr(home,b,c);
    return ES_OK;
  }

  template<class View>
  Actor*
  NaryOr<View>::copy(Space* home, bool share) {
    if (x.size() == 1)
      return new (home) Eq<View,View>(home,share,*this,
				      x[0],y);
    if (x.size() == 2)
      return new (home) Or<View,View,View>(home,share,*this,
					   x[0],x[1],y);
    return new (home) NaryOr<View>(home,share,*this);
  }

  template<class View>
  ExecStatus
  NaryOr<View>::propagate(Space* home) {
    if (y.zero()) {
      for (int i = x.size(); i--; )
	GECODE_ME_CHECK(x[i].t_zero(home));
      return ES_SUBSUMED;
    }
    if (y.one()) {
      GECODE_ES_CHECK(NaryOrTrue<View>::post(home,x));
      return ES_SUBSUMED;
    }
    for (int i = x.size(); i--; ) {
      if (x[i].one()) {
	y.t_one_none(home);
	return ES_SUBSUMED;
      }
      if (x[i].zero())
	x.move_lst(i);
    }
    if (x.size() == 0) {
      y.t_zero_none(home);
      return ES_SUBSUMED;
    }
    return ES_FIX;
  }


}}}

// STATISTICS: int-prop