/* -*- mode: C++; c-basic-offset: 2; indent-tabs-mode: nil -*- */
/*
 *  Main authors:
 *     Christian Schulte <schulte@gecode.org>
 *
 *  Copyright:
 *     Christian Schulte, 2006
 *
 *  Last modified:
 *     $Date: 2008-02-18 15:29:18 +0100 (Mon, 18 Feb 2008) $ by $Author: tack $
 *     $Revision: 6215 $
 *
 *  This file is part of Gecode, the generic constraint
 *  development environment:
 *     http://www.gecode.org
 *
 *  Permission is hereby granted, free of charge, to any person obtaining
 *  a copy of this software and associated documentation files (the
 *  "Software"), to deal in the Software without restriction, including
 *  without limitation the rights to use, copy, modify, merge, publish,
 *  distribute, sublicense, and/or sell copies of the Software, and to
 *  permit persons to whom the Software is furnished to do so, subject to
 *  the following conditions:
 *
 *  The above copyright notice and this permission notice shall be
 *  included in all copies or substantial portions of the Software.
 *
 *  THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
 *  EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
 *  MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
 *  NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
 *  LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
 *  OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
 *  WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
 *
 */

namespace Gecode { namespace Int { namespace Linear {

  /*
   * Array of scale Boolean views
   *
   */
  forceinline
  ScaleBoolArray::ScaleBoolArray(void) {}
  forceinline
  ScaleBoolArray::ScaleBoolArray(Space* home, int n) {
    if (n > 0) {
      _fst = static_cast<ScaleBool*>(home->alloc(n*sizeof(ScaleBool)));
      _lst = _fst+n;
    } else {
      _fst = _lst = NULL;
    }
  }
  forceinline void 
  ScaleBoolArray::subscribe(Space* home, Propagator* p) {
    for (ScaleBool* f = _fst; f < _lst; f++)
      f->x.subscribe(home,p,PC_BOOL_VAL);
  }
  forceinline void 
  ScaleBoolArray::cancel(Space* home, Propagator* p) {
    for (ScaleBool* f = _fst; f < _lst; f++)
      f->x.cancel(home,p,PC_BOOL_VAL);
  }
  forceinline void 
  ScaleBoolArray::update(Space* home, bool share, ScaleBoolArray& sba) {
    int n = sba._lst - sba._fst;
    if (n > 0) {
      _fst = static_cast<ScaleBool*>(home->alloc(n*sizeof(ScaleBool)));
      _lst = _fst+n;
      for (int i=n; i--; ) {
        _fst[i].a = sba._fst[i].a;
        _fst[i].x.update(home,share,sba._fst[i].x);
      }
    } else {
      _fst = _lst = NULL;
    }
  }
  forceinline ScaleBool* 
  ScaleBoolArray::fst(void) const {
    return _fst;
  }
  forceinline ScaleBool* 
  ScaleBoolArray::lst(void) const {
    return _lst;
  }
  forceinline void 
  ScaleBoolArray::fst(ScaleBool* f) {
    _fst = f;
  }
  forceinline void 
  ScaleBoolArray::lst(ScaleBool* l) {
    _lst = l;
  }
  forceinline bool 
  ScaleBoolArray::empty(void) const {
    return _fst == _lst;
  }
  forceinline int 
  ScaleBoolArray::size(void) const {
    return static_cast<int>(_lst - _fst);
  }
  forceinline bool
  ScaleBoolArray::ScaleDec::operator()(const ScaleBool& x, 
                                       const ScaleBool& y) {
    return x.a > y.a;
  }

  inline void 
  ScaleBoolArray::sort(void) {
    ScaleDec scale_dec;
    Support::quicksort<ScaleBool,ScaleDec>(fst(), size(), scale_dec);
  }

  inline Support::Symbol
  ScaleBoolArray::type(void) {
    return Support::Symbol("Gecode::Int::Linear::ScaleBoolArray");
  }

  /*
   * Empty array of scale Boolean views
   *
   */
  forceinline
  EmptyScaleBoolArray::EmptyScaleBoolArray(void) {}
  forceinline
  EmptyScaleBoolArray::EmptyScaleBoolArray(Space*, int) {}
  forceinline void 
  EmptyScaleBoolArray::subscribe(Space*, Propagator*) {}
  forceinline void 
  EmptyScaleBoolArray::cancel(Space*, Propagator*) {}
  forceinline void 
  EmptyScaleBoolArray::update(Space*, bool, EmptyScaleBoolArray&) {}
  forceinline ScaleBool* 
  EmptyScaleBoolArray::fst(void) const { return NULL; }
  forceinline ScaleBool* 
  EmptyScaleBoolArray::lst(void) const { return NULL; }
  forceinline void 
  EmptyScaleBoolArray::fst(ScaleBool*) {}
  forceinline void 
  EmptyScaleBoolArray::lst(ScaleBool*) {}
  forceinline bool 
  EmptyScaleBoolArray::empty(void) const { return true; }
  forceinline int 
  EmptyScaleBoolArray::size(void) const { return 0; }
  forceinline void 
  EmptyScaleBoolArray::sort(void) {}
  inline Support::Symbol
  EmptyScaleBoolArray::type(void) {
    return Support::Symbol("Gecode::Int::Linear::EmptyScaleBoolArray");
  }


  /*
   * Base-class for Boolean constraints with coefficients
   *
   */

  template<class SBAP, class SBAN, class VX, PropCond pcx>
  forceinline
  LinBoolScale<SBAP,SBAN,VX,pcx>::LinBoolScale(Space* home, 
                                               SBAP& p0, SBAN& n0,
                                               VX x0, int c0)
    : Propagator(home), p(p0), n(n0), x(x0), c(c0) {
    x.subscribe(home,this,pcx);
    p.subscribe(home,this);
    n.subscribe(home,this);
  }

  template<class SBAP, class SBAN, class VX, PropCond pcx>
  PropCost
  LinBoolScale<SBAP,SBAN,VX,pcx>::cost(ModEventDelta) const {
    return cost_lo(p.size() + n.size(), PC_LINEAR_LO);
  }

  template<class SBAP, class SBAN, class VX, PropCond pcx>
  forceinline size_t
  LinBoolScale<SBAP,SBAN,VX,pcx>::dispose(Space* home) {
    x.cancel(home,this,pcx);
    p.cancel(home,this);
    n.cancel(home,this);
    (void) Propagator::dispose(home);
    return sizeof(*this);
  }

  template<class SBAP, class SBAN, class VX, PropCond pcx>
  forceinline
  LinBoolScale<SBAP,SBAN,VX,pcx>::LinBoolScale(Space* home, bool share, 
                                               Propagator& pr,
                                               SBAP& p0, SBAN& n0,
                                               VX x0, int c0)
    : Propagator(home,share,pr), c(c0) {
    x.update(home,share,x0);
    p.update(home,share,p0);
    n.update(home,share,n0);
  }

  template<class SBAP, class SBAN, class VX, PropCond pcx>
  Reflection::ActorSpec
  LinBoolScale<SBAP,SBAN,VX,pcx>::spec(const Space* home,
                                       Reflection::VarMap& m,
                                       const Support::Symbol& ati) const {
    Reflection::ActorSpec s(ati);

    Reflection::IntArrayArg* c_p = Reflection::Arg::newIntArray(p.size());
    Reflection::ArrayArg* b_p = Reflection::Arg::newArray(p.size());
      
    int count = 0;
    for (ScaleBool* f = p.fst(); f != p.lst(); f++) {
      (*c_p)[count] = f->a;
      (*b_p)[count++]  = f->x.spec(home, m);
    }

    Reflection::IntArrayArg* c_n = Reflection::Arg::newIntArray(n.size());
    Reflection::ArrayArg* b_n = Reflection::Arg::newArray(n.size());
    count = 0;
    for (ScaleBool* f = n.fst(); f != n.lst(); f++) {
      (*c_n)[count] = f->a;
      (*b_n)[count++]  = f->x.spec(home, m);
    }

    return s << c_p << b_p
             << c_n << b_n << x.spec(home, m)
             << c;
  }

  /*
   * Boolean equality with coefficients
   *
   */

  template<class SBAP, class SBAN, class VX>
  forceinline
  EqBoolScale<SBAP,SBAN,VX>::EqBoolScale(Space* home, 
                                         SBAP& p, SBAN& n,
                                         VX x, int c)
    : LinBoolScale<SBAP,SBAN,VX,PC_INT_BND>(home,p,n,x,c) {}

  template<class SBAP, class SBAN, class VX>
  forceinline
  EqBoolScale<SBAP,SBAN,VX>::EqBoolScale(Space* home, bool share, 
                                         Propagator& pr,
                                         SBAP& p, SBAN& n,
                                         VX x, int c)
    : LinBoolScale<SBAP,SBAN,VX,PC_INT_BND>(home,share,pr,p,n,x,c) {}

  template<class SBAP, class SBAN, class VX>
  Actor*
  EqBoolScale<SBAP,SBAN,VX>::copy(Space* home, bool share) {
    if (p.empty()) {
      EmptyScaleBoolArray ep;
      if (x.assigned()) {
        ZeroIntView z;
        return new (home) EqBoolScale<EmptyScaleBoolArray,SBAN,ZeroIntView>
          (home,share,*this,ep,n,z,c+x.val());
      } else {
        return new (home) EqBoolScale<EmptyScaleBoolArray,SBAN,VX>
          (home,share,*this,ep,n,x,c);
      }
    } else if (n.empty()) {
      EmptyScaleBoolArray en;
      if (x.assigned()) {
        ZeroIntView z;
        return new (home) EqBoolScale<SBAP,EmptyScaleBoolArray,ZeroIntView>
          (home,share,*this,p,en,z,c+x.val());
      } else {
        return new (home) EqBoolScale<SBAP,EmptyScaleBoolArray,VX>
          (home,share,*this,p,en,x,c);
      }
    } else {
      return new (home) EqBoolScale<SBAP,SBAN,VX>(home,share,*this,p,n,x,c);
    }
  }

  template<class SBAP, class SBAN, class VX>
  inline Support::Symbol
  EqBoolScale<SBAP,SBAN,VX>::ati(void) {
    return Reflection::mangle<SBAP,SBAN,VX>("Gecode::Int::Linear::EqBoolScale");
  }

  template<class SBAP, class SBAN, class VX>
  Reflection::ActorSpec
  EqBoolScale<SBAP,SBAN,VX>::spec(const Space* home,
                                  Reflection::VarMap& m) const {
    return LinBoolScale<SBAP,SBAN,VX,PC_INT_BND>::spec(home, m, ati());
  }

  template<class SBAP, class SBAN, class VX>
  void
  EqBoolScale<SBAP,SBAN,VX>::post(Space* home, Reflection::VarMap& vars,
                                  const Reflection::ActorSpec& spec) {
    spec.checkArity(6);
    Reflection::IntArrayArg* c_p = spec[0]->toIntArray();
    ViewArray<BoolView> b_pv(home, vars, spec[1]);
    Reflection::IntArrayArg* c_n = spec[2]->toIntArray();
    ViewArray<BoolView> b_nv(home, vars, spec[3]);
    VX x(home, vars, spec[4]);
    int c = spec[5]->toInt();
    SBAP b_p(home,b_pv.size());
    {
      ScaleBool* f=b_p.fst();
      for (int i=b_pv.size(); i--; ) {
        f[i].x=b_pv[i]; f[i].a=(*c_p)[i];
      }
    }
    SBAN b_n(home,b_nv.size());
    {
      ScaleBool* f=b_n.fst();
      for (int i=b_nv.size(); i--; ) {
        f[i].x=b_nv[i]; f[i].a=(*c_n)[i];
      }
    }
    (void) new (home) EqBoolScale<SBAP,SBAN,VX>(home,b_p,b_n,x,c);
  }
  
  template<class SBAP, class SBAN, class VX>
  ExecStatus
  EqBoolScale<SBAP,SBAN,VX>::propagate(Space* home, ModEventDelta med) {
    int sl_p = 0; // Lower bound, computed positive
    int su_n = 0; // Upper bound, computed negative
    if (BoolView::me(med) == ME_BOOL_VAL) {
      // Eliminate assigned positive views while keeping order
      {
        // Skip not assigned views
        ScaleBool* f = p.fst();
        ScaleBool* l = p.lst();
        while ((f < l) && f->x.none()) {
          su_n += f->a; f++;
        }
        // Copy unassigned views to t
        ScaleBool* t = f;
        while (f < l) {
          if (f->x.one()) {
            c -= f->a;
          } else if (f->x.none()) {
            su_n += f->a; *t = *f; t++;
          }
          f++;
        }
        p.lst(t);
      }
      // Eliminate assigned negative views while keeping order
      {
        // Skip not assigned views
        ScaleBool* f = n.fst();
        ScaleBool* l = n.lst();
        while ((f < l) && f->x.none()) {
          sl_p += f->a; f++;
        }
        // Copy unassigned views to t
        ScaleBool* t = f;
        while (f < l) {
          if (f->x.one()) {
            c += f->a;
          } else if (f->x.none()) {
            sl_p += f->a; *t = *f; t++;
          }
          f++;
        }
        n.lst(t);
      }
    } else {
      for (ScaleBool* f=p.fst(); f<p.lst(); f++)
        su_n += f->a;
      for (ScaleBool* f=n.fst(); f<n.lst(); f++)
        sl_p += f->a;
    }
    
    if (p.empty() && n.empty()) {
      GECODE_ME_CHECK(x.eq(home,-c)); 
      return ES_SUBSUMED(this,sizeof(*this));
    }

    sl_p += x.max() + c;
    su_n -= x.min() + c;

    const int MOD_SL = 1 << 0;
    const int MOD_SU = 1 << 1;

    int mod = MOD_SL | MOD_SU;

    do {
      if ((mod & MOD_SL) != 0) {
        mod -= MOD_SL;
        // Propagate lower bound for positive Boolean views
        {
          ScaleBool* f=p.fst();
          for (ScaleBool* l=p.lst(); (f < l) && (f->a > sl_p); f++) {
            GECODE_ME_CHECK(f->x.zero_none(home));
            su_n -= f->a;
          }
          if (f > p.fst()) {
            p.fst(f); mod |= MOD_SU;
          }
        }
        // Propagate lower bound for negative Boolean views
        {
          ScaleBool* f=n.fst();
          for (ScaleBool* l=n.lst(); (f < l) && (f->a > sl_p); f++) {
            GECODE_ME_CHECK(f->x.one_none(home)); c += f->a;
            su_n -= f->a;
          }
          if (f > n.fst()) {
            n.fst(f); mod |= MOD_SU;
          }
        }
        // Propagate lower bound for integer view
        {
          const int x_min = x.min();
          ModEvent me = x.gq(home,x.max() - sl_p);
          if (me_failed(me))
            return ES_FAILED;
          if (me_modified(me)) {
            su_n -= x.min() - x_min;
            mod |= MOD_SU;
          }
        }
      }
      if ((mod & MOD_SU) != 0) {
        mod -= MOD_SU;
        // Propagate upper bound for positive Boolean views
        {
          ScaleBool* f=p.fst();
          for (ScaleBool* l=p.lst(); (f < l) && (f->a > su_n); f++) {
            GECODE_ME_CHECK(f->x.one_none(home)); c -= f->a;
            sl_p -= f->a;
          }
          if (f > p.fst()) {
            p.fst(f); mod |= MOD_SL;;
          }
        }
        // Propagate upper bound for negative Boolean views
        {
          ScaleBool* f=n.fst();
          for (ScaleBool* l=n.lst(); (f < l) && (f->a > su_n); f++) {
            GECODE_ME_CHECK(f->x.zero_none(home));
            sl_p -= f->a;
          }
          if (f > n.fst()) {
            n.fst(f); mod |= MOD_SL;;
          }
        }
        // Propagate upper bound for integer view
        {
          const int x_max = x.max();
          ModEvent me = x.lq(home,x.min() + su_n);
          if (me_failed(me))
            return ES_FAILED;
          if (me_modified(me)) {
            sl_p += x.max() - x_max;
            mod |= MOD_SL;;
          }
        }
      }
    } while (mod != 0);
    
    return (sl_p == -su_n) ? ES_SUBSUMED(this,sizeof(*this)) : ES_FIX;
  }



  template<class SBAP, class SBAN, class VX>
  ExecStatus
  EqBoolScale<SBAP,SBAN,VX>::post(Space* home,
                                  SBAP& p, SBAN& n, VX x, int c) {
    p.sort(); n.sort();
    if (p.empty()) {
      EmptyScaleBoolArray ep;
      (void) new (home) EqBoolScale<EmptyScaleBoolArray,SBAN,VX>
        (home,ep,n,x,c);
    } else if (n.empty()) {
      EmptyScaleBoolArray en;
      (void) new (home) EqBoolScale<SBAP,EmptyScaleBoolArray,VX>
        (home,p,en,x,c);
    } else {
      (void) new (home) EqBoolScale<ScaleBoolArray,ScaleBoolArray,VX>
        (home,p,n,x,c);
    }
    return ES_OK;
  }


  /*
   * Boolean inequality with coefficients
   *
   */

  template<class SBAP, class SBAN, class VX>
  forceinline
  LqBoolScale<SBAP,SBAN,VX>::LqBoolScale(Space* home, 
                                         SBAP& p, SBAN& n,
                                         VX x, int c)
    : LinBoolScale<SBAP,SBAN,VX,PC_INT_BND>(home,p,n,x,c) {}

  template<class SBAP, class SBAN, class VX>
  forceinline
  LqBoolScale<SBAP,SBAN,VX>::LqBoolScale(Space* home, bool share, 
                                         Propagator& pr,
                                         SBAP& p, SBAN& n,
                                         VX x, int c)
    : LinBoolScale<SBAP,SBAN,VX,PC_INT_BND>(home,share,pr,p,n,x,c) {}

  template<class SBAP, class SBAN, class VX>
  Actor*
  LqBoolScale<SBAP,SBAN,VX>::copy(Space* home, bool share) {
    if (p.empty()) {
      EmptyScaleBoolArray ep;
      if (x.assigned()) {
        ZeroIntView z;
        return new (home) LqBoolScale<EmptyScaleBoolArray,SBAN,ZeroIntView>
          (home,share,*this,ep,n,z,c+x.val());
      } else {
        return new (home) LqBoolScale<EmptyScaleBoolArray,SBAN,VX>
          (home,share,*this,ep,n,x,c);
      }
    } else if (n.empty()) {
      EmptyScaleBoolArray en;
      if (x.assigned()) {
        ZeroIntView z;
        return new (home) LqBoolScale<SBAP,EmptyScaleBoolArray,ZeroIntView>
          (home,share,*this,p,en,z,c+x.val());
      } else {
        return new (home) LqBoolScale<SBAP,EmptyScaleBoolArray,VX>
          (home,share,*this,p,en,x,c);
      }
    } else {
      return new (home) LqBoolScale<SBAP,SBAN,VX>(home,share,*this,p,n,x,c);
    }
  }

  template<class SBAP, class SBAN, class VX>
  inline Support::Symbol
  LqBoolScale<SBAP,SBAN,VX>::ati(void) {
    return Reflection::mangle<SBAP,SBAN,VX>("Gecode::Int::Linear::LqBoolScale");
  }

  template<class SBAP, class SBAN, class VX>
  Reflection::ActorSpec
  LqBoolScale<SBAP,SBAN,VX>::spec(const Space* home,
                                  Reflection::VarMap& m) const {
    return LinBoolScale<SBAP,SBAN,VX,PC_INT_BND>::spec(home, m, ati());
  }

  template<class SBAP, class SBAN, class VX>
  void
  LqBoolScale<SBAP,SBAN,VX>::post(Space* home, Reflection::VarMap& vars,
                                  const Reflection::ActorSpec& spec) {
    spec.checkArity(6);
    Reflection::IntArrayArg* c_p = spec[0]->toIntArray();
    ViewArray<BoolView> b_pv(home, vars, spec[1]);
    Reflection::IntArrayArg* c_n = spec[2]->toIntArray();
    ViewArray<BoolView> b_nv(home, vars, spec[3]);
    VX x(home, vars, spec[4]);
    int c = spec[5]->toInt();
    SBAP b_p(home,b_pv.size());
    {
      ScaleBool* f=b_p.fst();
      for (int i=b_pv.size(); i--; ) {
        f[i].x=b_pv[i]; f[i].a=(*c_p)[i];
      }
    }
    SBAN b_n(home,b_nv.size());
    {
      ScaleBool* f=b_n.fst();
      for (int i=b_nv.size(); i--; ) {
        f[i].x=b_nv[i]; f[i].a=(*c_n)[i];
      }
    }
    (void) new (home) LqBoolScale<SBAP,SBAN,VX>(home,b_p,b_n,x,c);
  }

  template<class SBAP, class SBAN, class VX>
  ExecStatus
  LqBoolScale<SBAP,SBAN,VX>::propagate(Space* home, ModEventDelta med) {
    int sl = 0;
    if (BoolView::me(med) == ME_BOOL_VAL) {
      // Eliminate assigned positive views while keeping order
      {
        // Skip not assigned views
        ScaleBool* f = p.fst();
        ScaleBool* l = p.lst();
        while ((f < l) && f->x.none())
          f++;
        // Copy unassigned views to t
        ScaleBool* t = f;
        while (f < l) {
          if (f->x.one()) {
            c -= f->a;
          } else if (f->x.none()) {
            *t = *f; t++;
          }
          f++;
        }
        p.lst(t);
      }
      // Eliminate assigned negative views while keeping order
      {
        // Skip not assigned views
        ScaleBool* f = n.fst();
        ScaleBool* l = n.lst();
        while ((f < l) && f->x.none()) {
          sl += f->a; f++;
        }
        // Copy unassigned views to t
        ScaleBool* t = f;
        while (f < l) {
          if (f->x.one()) {
            c += f->a;
          } else if (f->x.none()) {
            sl += f->a; *t = *f; t++;
          }
          f++;
        }
        n.lst(t);
      }
    } else {
      for (ScaleBool* f=n.fst(); f<n.lst(); f++)
        sl += f->a;
    }
    
    sl += x.max() + c;

    // Propagate upper bound for positive Boolean views
    {
      ScaleBool* f=p.fst();
      for (ScaleBool* l=p.lst(); (f < l) && (f->a > sl); f++)
        GECODE_ME_CHECK(f->x.zero_none(home));
      p.fst(f);
    }
    // Propagate lower bound for negative Boolean views
    {
      ScaleBool* f=n.fst();
      for (ScaleBool* l=n.lst(); (f < l) && (f->a > sl); f++) {
        c += f->a; 
        GECODE_ME_CHECK(f->x.one_none(home));
      }
      n.fst(f);
    }
    ExecStatus es = ES_FIX;
    // Propagate lower bound for integer view
    {
      const int slx = x.max() - sl;
      ModEvent me = x.gq(home,slx);
      if (me_failed(me))
        return ES_FAILED;
      if (me_modified(me) && (slx != x.min()))
        es = ES_NOFIX;
    }

    if (p.empty() && n.empty())
      return ES_SUBSUMED(this,home);

    return es;
  }



  template<class SBAP, class SBAN, class VX>
  ExecStatus
  LqBoolScale<SBAP,SBAN,VX>::post(Space* home,
                                  SBAP& p, SBAN& n, VX x, int c) {
    p.sort(); n.sort();
    if (p.empty()) {
      EmptyScaleBoolArray ep;
      (void) new (home) LqBoolScale<EmptyScaleBoolArray,SBAN,VX>
        (home,ep,n,x,c);
    } else if (n.empty()) {
      EmptyScaleBoolArray en;
      (void) new (home) LqBoolScale<SBAP,EmptyScaleBoolArray,VX>
        (home,p,en,x,c);
    } else {
      (void) new (home) LqBoolScale<ScaleBoolArray,ScaleBoolArray,VX>
        (home,p,n,x,c);
    }
    return ES_OK;
  }

  /*
   * Boolean disequality with coefficients
   *
   */

  template<class SBAP, class SBAN, class VX>
  forceinline
  NqBoolScale<SBAP,SBAN,VX>::NqBoolScale(Space* home, 
                                         SBAP& p, SBAN& n,
                                         VX x, int c)
    : LinBoolScale<SBAP,SBAN,VX,PC_INT_VAL>(home,p,n,x,c) {}

  template<class SBAP, class SBAN, class VX>
  forceinline
  NqBoolScale<SBAP,SBAN,VX>::NqBoolScale(Space* home, bool share, 
                                         Propagator& pr,
                                         SBAP& p, SBAN& n,
                                         VX x, int c)
    : LinBoolScale<SBAP,SBAN,VX,PC_INT_VAL>(home,share,pr,p,n,x,c) {}

  template<class SBAP, class SBAN, class VX>
  Actor*
  NqBoolScale<SBAP,SBAN,VX>::copy(Space* home, bool share) {
    if (p.empty()) {
      EmptyScaleBoolArray ep;
      if (x.assigned()) {
        ZeroIntView z;
        return new (home) NqBoolScale<EmptyScaleBoolArray,SBAN,ZeroIntView>
          (home,share,*this,ep,n,z,c+x.val());
      } else {
        return new (home) NqBoolScale<EmptyScaleBoolArray,SBAN,VX>
          (home,share,*this,ep,n,x,c);
      }
    } else if (n.empty()) {
      EmptyScaleBoolArray en;
      if (x.assigned()) {
        ZeroIntView z;
        return new (home) NqBoolScale<SBAP,EmptyScaleBoolArray,ZeroIntView>
          (home,share,*this,p,en,z,c+x.val());
      } else {
        return new (home) NqBoolScale<SBAP,EmptyScaleBoolArray,VX>
          (home,share,*this,p,en,x,c);
      }
    } else {
      return new (home) NqBoolScale<SBAP,SBAN,VX>(home,share,*this,p,n,x,c);
    }
  }

  template<class SBAP, class SBAN, class VX>
  inline Support::Symbol
  NqBoolScale<SBAP,SBAN,VX>::ati(void) {
    return Reflection::mangle<SBAP,SBAN,VX>("Gecode::Int::Linear::NqBoolScale");
  }

  template<class SBAP, class SBAN, class VX>
  Reflection::ActorSpec
  NqBoolScale<SBAP,SBAN,VX>::spec(const Space* home,
                                  Reflection::VarMap& m) const {
    return LinBoolScale<SBAP,SBAN,VX,PC_INT_VAL>::spec(home, m, ati());
  }

  template<class SBAP, class SBAN, class VX>
  void
  NqBoolScale<SBAP,SBAN,VX>::post(Space* home, Reflection::VarMap& vars,
                                  const Reflection::ActorSpec& spec) {
    spec.checkArity(6);
    Reflection::IntArrayArg* c_p = spec[0]->toIntArray();
    ViewArray<BoolView> b_pv(home, vars, spec[1]);
    Reflection::IntArrayArg* c_n = spec[2]->toIntArray();
    ViewArray<BoolView> b_nv(home, vars, spec[3]);
    VX x(home, vars, spec[4]);
    int c = spec[5]->toInt();
    SBAP b_p(home,b_pv.size());
    {
      ScaleBool* f=b_p.fst();
      for (int i=b_pv.size(); i--; ) {
        f[i].x=b_pv[i]; f[i].a=(*c_p)[i];
      }
    }
    SBAN b_n(home,b_nv.size());
    {
      ScaleBool* f=b_n.fst();
      for (int i=b_nv.size(); i--; ) {
        f[i].x=b_nv[i]; f[i].a=(*c_n)[i];
      }
    }
    (void) new (home) NqBoolScale<SBAP,SBAN,VX>(home,b_p,b_n,x,c);
  }

  template<class SBAP, class SBAN, class VX>
  ExecStatus
  NqBoolScale<SBAP,SBAN,VX>::propagate(Space* home, ModEventDelta med) {
    if (BoolView::me(med) == ME_BOOL_VAL) {
      // Eliminate assigned positive views
      {
        ScaleBool* f = p.fst();
        ScaleBool* t = f;
        ScaleBool* l = p.lst();
        while (f < l) {
          if (f->x.one()) {
            c -= f->a; *f = *(t++);
          } else if (f->x.zero()) {
            *f = *(t++);
          } 
          f++;
        }
        p.fst(t);
      }
      // Eliminate assigned negative views
      {
        ScaleBool* f = n.fst();
        ScaleBool* t = f;
        ScaleBool* l = n.lst();
        while (f < l) {
          if (f->x.one()) {
            c += f->a; *f = *(t++);
          } else if (f->x.zero()) {
            *f = *(t++);
          } 
          f++;
        }
        n.fst(t);
      }
    }
    
    if (p.empty() && n.empty()) {
      GECODE_ME_CHECK(x.nq(home,-c)); 
      return ES_SUBSUMED(this,home);
    }

    if (x.assigned()) {
      int r = x.val()+c;
      if (p.empty() && (n.size() == 1)) {
        if (r == -n.fst()->a) {
          GECODE_ME_CHECK(n.fst()->x.zero_none(home));
        } else if (r == 0) {
          GECODE_ME_CHECK(n.fst()->x.one_none(home));
        }
        return ES_SUBSUMED(this,home);
      }
      if ((p.size() == 1) && n.empty()) {
        if (r == p.fst()->a) {
          GECODE_ME_CHECK(p.fst()->x.zero_none(home));
        } else if (r == 0) {
          GECODE_ME_CHECK(p.fst()->x.one_none(home));
        }
        return ES_SUBSUMED(this,home);
      }
    }
    return ES_FIX;
  }



  template<class SBAP, class SBAN, class VX>
  ExecStatus
  NqBoolScale<SBAP,SBAN,VX>::post(Space* home,
                                  SBAP& p, SBAN& n, VX x, int c) {
    if (p.empty()) {
      EmptyScaleBoolArray ep;
      (void) new (home) NqBoolScale<EmptyScaleBoolArray,SBAN,VX>
        (home,ep,n,x,c);
    } else if (n.empty()) {
      EmptyScaleBoolArray en;
      (void) new (home) NqBoolScale<SBAP,EmptyScaleBoolArray,VX>
        (home,p,en,x,c);
    } else {
      (void) new (home) NqBoolScale<ScaleBoolArray,ScaleBoolArray,VX>
        (home,p,n,x,c);
    }
    return ES_OK;
  }

}}}

// STATISTICS: int-prop