/* -*- mode: C++; c-basic-offset: 2; indent-tabs-mode: nil -*- */
/*
 *  Main authors:
 *     Patrick Pekczynski <pekczynski@ps.uni-sb.de>
 *
 *  Copyright:
 *     Patrick Pekczynski, 2006
 *
 *  Last modified:
 *     $Date: 2008-02-06 18:48:22 +0100 (Wed, 06 Feb 2008) $ by $Author: schulte $
 *     $Revision: 6102 $
 *
 *  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 CpltSet {

  inline void 
  CpltSetVarImp::printdom(void) const {
    manager.print_set(domain);
  }

  forceinline unsigned int 
  CpltSetVarImp::tableWidth(void) const { return max - min + 1; }

  inline bdd
  CpltSetVarImp::element(int i) const { 
    return manager.bddpos(_offset + i); 
  }

  inline bdd
  CpltSetVarImp::elementNeg(int i) const {
    return manager.negbddpos(_offset + i);
  }


  inline bdd 
  CpltSetVarImp::dom(void) const {
    return domain;
  }

  forceinline unsigned int
  CpltSetVarImp::offset(void) const { return _offset; }

  forceinline int
  CpltSetVarImp::initialLubMin(void) const { return min; }

  forceinline int
  CpltSetVarImp::initialLubMax(void) const { return max; }

  inline unsigned int 
  CpltSetVarImp::cardMin(void) const {
    if (manager.ctrue(domain)) { return 0; }
    bdd d = domain;
    int l = 0;
    int u = 0;
    getcardbounds(d, l, u);
    return l;
  }

  inline unsigned int 
  CpltSetVarImp::cardMax(void) const {
    if (manager.ctrue(domain)) { return tableWidth(); }
    bdd d = domain;
    int l = 0;
    int u = 0;
    getcardbounds(d, l, u);
    return u;
  }

  template <class I> 
  ModEvent 
  CpltSetVarImp::excludeI(Space* home, I& i) {
    // we can only exclude what intersects the min and max element of the variable
    Iter::Ranges::Singleton s(min, max);
    Iter::Ranges::Inter<Iter::Ranges::Singleton, I> inter(s, i);
  
    if (!inter()) 
      return ME_CPLTSET_NONE;
  
    bdd not_lub = bdd_true();
    Iter::Ranges::ToValues<
      Iter::Ranges::Inter<Iter::Ranges::Singleton, I>
      > val(inter);

    Iter::Ranges::ValCache<
      Iter::Ranges::ToValues<
      Iter::Ranges::Inter<Iter::Ranges::Singleton, I> >
      > cache(val);
  
    for (cache.last(); cache(); --cache) {
      int v = cache.min();
      not_lub &= elementNeg(v - min);
    }
    return intersect(home, not_lub);
  }

  inline ModEvent 
  CpltSetVarImp::include(Space* home, int v) {
    return include(home, v, v);
  }

  inline ModEvent 
  CpltSetVarImp::exclude(Space* home, int v) {
    return exclude(home, v, v);
  }

  template <class I> 
  ModEvent 
  CpltSetVarImp::includeI(Space* home, I& i) {
    if (!i()) 
      return ME_CPLTSET_NONE;

    bdd in_glb  = bdd_true();
    Iter::Ranges::ToValues<I> val(i);
    Iter::Ranges::ValCache<Iter::Ranges::ToValues<I> > cache(val);

    for (cache.last(); cache(); --cache) {
      int v = cache.min();
      if (v < min || max < v) 
        return ME_CPLTSET_FAILED;
      in_glb &= element(v - min);
    }
    return intersect(home, in_glb);  
  }

  inline ModEvent
  CpltSetVarImp::nq(Space* home, int v) { return nq(home, v, v); }

  template <class I>
  ModEvent
  CpltSetVarImp::nqI(Space* home, I& i) {
    bdd ass = !(iterToBdd(i));
    return intersect(home, ass);
  }

  inline ModEvent
  CpltSetVarImp::eq(Space* home, int v) { return eq(home, v, v); }

  // gen _assigned needs a test in case
  // we try to build an _assigned
  // that is not allowed by the variable domain
  template <class I>
  ModEvent
  CpltSetVarImp::eqI(Space* home, I& i) {
    if (i()) {
      if (i.min() < min || i.min() > max) 
        return ME_CPLTSET_FAILED;
    }
    bdd ass = iterToBdd(i);
    return intersect(home, ass);
  }

  inline ModEvent 
  CpltSetVarImp::intersect(Space* home, int i) {
    return intersect(home, i, i);
  }

  template <class I> 
  ModEvent 
  CpltSetVarImp::intersectI(Space* home, I& i) {
    Iter::Ranges::Compl<Set::Limits::min, Set::Limits::max, I> 
      compI(i);
    return excludeI(home, compI); 
  }

  inline ModEvent 
  CpltSetVarImp::cardMin(Space* home, unsigned int newMin) {
    return cardinality(home, newMin, tableWidth());
  }

  inline ModEvent 
  CpltSetVarImp::cardMax(Space* home, unsigned int newMax) {
    return cardinality(home, 0, newMax);
  }

  // given the empty iterator we should produce an 
  // _assigned for the empty set.
  template <class I>
  bdd
  CpltSetVarImp::iterToBdd(I& i) {

    Iter::Ranges::ToValues<I> vali(i);
    Iter::Ranges::ValCache<Iter::Ranges::ToValues<I> > vc(vali);

    bdd ass = bdd_true();
    // start at the end for backwards iteration
    vc.last();
    for (int v = max; v >= min; v--) {
      if (vc()) {
        if (vc.val() == v) {
          ass &= element(v - min);
          --vc;
        } else {
          ass &= elementNeg(v - min);
        }
      } else {
        ass &= elementNeg(v - min);
      }
    }

    return ass;
  }

  inline bool
  CpltSetVarImp::range(void) const { return manager.ctrue(domain); }

  /*
   * Copying a variable
   *
   */

  forceinline CpltSetVarImp*
  CpltSetVarImp::copy(Space* home, bool share) {
    return copied() ? static_cast<CpltSetVarImp*>(forward())
      : perform_copy(home,share);
  }

  /*
   * Subscribing to variables
   *
   */
  forceinline void
  CpltSetVarImp::subscribe(Space* home, Propagator* p, PropCond pc,
                           bool process) {
    CpltSetVarImpBase::subscribe(home,p,pc,assigned(), process);
  }

  forceinline void
  CpltSetVarImp::cancel(Space* home, Propagator* p, PropCond pc) {
    CpltSetVarImpBase::cancel(home,p,pc,assigned());
  }

  /*
   * Support for delta information
   *
   */
  forceinline ModEvent
  CpltSetVarImp::modevent(const Delta* d) {
    return d->modevent();
  }

  /// Iterator for the values in the greatest lower bound of a bdd variable implementation
  template <> 
  class GlbValues<CpltSetVarImp*> : public DomBddIterator {
  private:
    int mi;
    int ma;
  public:
    /// \name Constructors and initialization
    //@{
    /// Default constructor
    GlbValues(void);
    /// Initialize with ranges for variable implementation \a x
    GlbValues(const CpltSetVarImp* x);
    /// Initialize with ranges for variable implementation \a x
    void init(const CpltSetVarImp* x);
    //@}
    /// \name Iteration control
    //@{
    /// Iterate to the next glb value
    void operator++(void);
    //@}    
    int val(void) const;
  };

  /// Iterator for the values in the least upper bound of a bdd variable implementation
  template <> 
  class LubValues<CpltSetVarImp*> : public DomBddIterator {
  private:
    int mi;
    int ma;
  public:
    /// \name Constructors and initialization
    //@{
    /// Default constructor
    LubValues(void);
    /// Initialize with ranges for variable implementation \a x
    LubValues(const CpltSetVarImp* x);
    /// Initialize with ranges for variable implementation \a x
    void init(const CpltSetVarImp* x);
    //@}
    /// \name Iteration control
    //@{
    /// Iterate to the next glb value
    void operator++(void);
    /// Check validity
    bool operator()(void) const;
    //@}    
    int val(void) const;
  };

  /// Iterator for the unknown values of a bdd variable implementation
  template <> 
  class UnknownValues<CpltSetVarImp*> : public DomBddIterator {
  private:
    int mi;
    int ma;
  public:
    /// \name Constructors and initialization
    //@{
    /// Default constructor
    UnknownValues(void);
    /// Initialize with ranges for variable implementation \a x
    UnknownValues(const CpltSetVarImp* x);
    /// Initialize with ranges for variable implementation \a x 
    UnknownValues(const CpltSetVarImp* x, bdd& remain);
    /// Initialize with ranges for variable implementation \a x
    void init(const CpltSetVarImp* x);
    /// Initialize with ranges for variable implementation \a x
    void init(const CpltSetVarImp* x, bdd& remain);
    //@}
    /// \name Iteration control
    //@{
    /// Iterate to the next glb value
    void operator++(void);
    //@}    
    int val(void) const;
  };

  /*
   * BddIterator
   *
   */

  forceinline
  BddIterator::BddIterator(void) {}

  forceinline
  BddIterator::BddIterator(const bdd& b) {
    init(b);
  }

  forceinline NodeStatus 
  BddIterator::status(void) const { return flag; }

  forceinline int 
  BddIterator::level(void) const { return _level; }

  forceinline bool
  BddIterator::empty(void) const { return (l == 0) && (r == n - 1); }

  inline bool
  BddIterator::operator()(void) const {
    bool valid = (!empty() || singleton );
    return valid;
  }

  inline int 
  BddIterator::label(void) const { 
    if (!operator()()) { 
      return -1; 
    } else {
      return manager.bddidx(cur); 
    }
  }

  forceinline int
  BddIterator::size(void) const { return n; }
  
  /*
   * DomBddIterator
   *
   */

  inline void
  DomBddIterator::init(const CpltSetVarImp* x, bdd& remain) {
    vector_level = 0;
    mi    = x->min;
    ma    = x->max;
    off   = x->_offset;

    bdd dom = x->dom();
    if (dom != remain)
      dom &= remain;
    
    BddIterator::init(dom);
    bdd_level   = BddIterator::label() - off;
  }

  inline void
  DomBddIterator::init(const CpltSetVarImp* x) {
    bdd dom = x->dom();
    init(x, dom);
  }

  forceinline   
  DomBddIterator::DomBddIterator(void) {}

  forceinline
  DomBddIterator::DomBddIterator(const CpltSetVarImp* x) {
    bdd dom = x->dom();
    DomBddIterator::init(x, dom);
  }

  inline
  DomBddIterator::DomBddIterator(const CpltSetVarImp* x, bdd& remain) {
    vector_level = 0;
    mi    = x->min;
    ma    = x->max;
    off   = x->_offset;
    bdd dom = x->dom();
    if (dom != remain) {
      dom &= remain;
    }
    BddIterator::init(dom);
    bdd_level = BddIterator::label() - off;
  }

  forceinline bool
  DomBddIterator::same(void) const { return bdd_level == vector_level; }

  forceinline bool
  DomBddIterator::operator()(void) const {
    return vector_level < (ma-mi+1);
  }

  inline void
  DomBddIterator::operator++(void) {
    if (same()) {
      BddIterator::operator++();
      bdd_level   = BddIterator::label() - off;
    } 
    vector_level++;
  }

  inline NodeStatus
  DomBddIterator::status(void) const{
    return same() ? BddIterator::status() : FIX_UNKNOWN;
  }

  inline int
  DomBddIterator::val(void) const {
    return same() ? mi + BddIterator::label() - off : mi + vector_level;
  }

  forceinline
  GlbValues<CpltSetVarImp*>::GlbValues(void) {}

  inline
  GlbValues<CpltSetVarImp*>::GlbValues(const CpltSetVarImp* x) 
    : mi(x->min), ma(x->max) {
    DomBddIterator::init(x);
    while (operator()() && status() != FIX_GLB) {
      DomBddIterator::operator++();
    }

  }

  inline void 
  GlbValues<CpltSetVarImp*>::init(const CpltSetVarImp* x) {
    mi = x->min;  
    ma = x->max;
    DomBddIterator::init(x);
    while (operator()() && status() != FIX_GLB) {
      DomBddIterator::operator++();
    }
  }

  inline void 
  GlbValues<CpltSetVarImp*>::operator++(void) {
    DomBddIterator::operator++();
    while (operator()() && status() != FIX_GLB) {
      DomBddIterator::operator++();
    }
  }

  forceinline int
  GlbValues<CpltSetVarImp*>::val(void) const {
    return DomBddIterator::val();
  }
  
  forceinline
  LubValues<CpltSetVarImp*>::LubValues(void) {}

  inline
  LubValues<CpltSetVarImp*>::LubValues(const CpltSetVarImp* x) 
    : mi(x->min), ma(x->max) {
    DomBddIterator::init(x);
    while (DomBddIterator::operator()() && status() == FIX_NOT_LUB) {
      DomBddIterator::operator++();
    }
  }

  inline void 
  LubValues<CpltSetVarImp*>::init(const CpltSetVarImp* x) {
    mi = x->min;  
    ma = x->max;

    DomBddIterator::init(x);
    while (DomBddIterator::operator()() && status() == FIX_NOT_LUB) {
      DomBddIterator::operator++();
    }
  }

  inline void 
  LubValues<CpltSetVarImp*>::operator++(void) {
    DomBddIterator::operator++();
    while (DomBddIterator::operator()() && status() == FIX_NOT_LUB) {
      DomBddIterator::operator++();
    }
  }

  inline bool
  LubValues<CpltSetVarImp*>::operator()(void) const {
    return DomBddIterator::operator()() && status() != FIX_NOT_LUB;
  }

  inline int
  LubValues<CpltSetVarImp*>::val(void) const {
    return DomBddIterator::val();
  }

  forceinline
  UnknownValues<CpltSetVarImp*>::UnknownValues(void) {}

  inline
  UnknownValues<CpltSetVarImp*>::UnknownValues(const CpltSetVarImp* x) 
    : mi(x->min), ma(x->max) {
    DomBddIterator::init(x);
    while (operator()() && 
           !(status() == FIX_UNKNOWN || status() == UNDET)) {
      DomBddIterator::operator++();
    }
  }

  inline void 
  UnknownValues<CpltSetVarImp*>::init(const CpltSetVarImp* x) {
    mi = x->min;  
    ma = x->max;

    DomBddIterator::init(x);
    while (operator()() && 
           !(status() == FIX_UNKNOWN || status() == UNDET)) {
      DomBddIterator::operator++();
    }
  }

  inline void 
  UnknownValues<CpltSetVarImp*>::operator++(void) {
    DomBddIterator::operator++();
    while (operator()() && 
           !(status() == FIX_UNKNOWN || status() == UNDET)) {
      DomBddIterator::operator++();
    }
  }

  inline int
  UnknownValues<CpltSetVarImp*>::val(void) const {
    return DomBddIterator::val();
  }
  
}

namespace Set {

  /** \brief Range iterator for greatest lower bound of CpltSet variable 
    * implementation */
  template <> 
  class GlbRanges<CpltSet::CpltSetVarImp*> 
    : public Iter::Values::ToRanges<CpltSet::GlbValues<CpltSet::CpltSetVarImp*> > {
  public:
    /// \name Constructors and initialization
    //@{
    /// Default constructor
    GlbRanges(void);
    /// Initialize with ranges for variable implementation \a x
    GlbRanges(const CpltSet::CpltSetVarImp* x);
    /// Initialize with ranges for variable implementation \a x
    void init(const CpltSet::CpltSetVarImp* x);
    //@}
  };

  forceinline
  GlbRanges<CpltSet::CpltSetVarImp*>::GlbRanges(void) {}

  inline
  GlbRanges<CpltSet::CpltSetVarImp*>
  ::GlbRanges(const CpltSet::CpltSetVarImp* x) {
    CpltSet::GlbValues<CpltSet::CpltSetVarImp*> v(x);
    Iter::Values::ToRanges<CpltSet::GlbValues<CpltSet::CpltSetVarImp*> >::init(v);
  }

  inline void 
  GlbRanges<CpltSet::CpltSetVarImp*>
  ::init(const CpltSet::CpltSetVarImp* x) {
    CpltSet::GlbValues<CpltSet::CpltSetVarImp*> v(x);
    Iter::Values::ToRanges<
      CpltSet::GlbValues<CpltSet::CpltSetVarImp*> >::init(v);
  }

  /** \brief Range iterator for least upper bound of CpltSet variable 
    * implementation */
  template <> 
  class LubRanges<CpltSet::CpltSetVarImp*> 
  : public 
    Iter::Values::ToRanges<CpltSet::LubValues<CpltSet::CpltSetVarImp*> > {
  public:
    /// \name Constructors and initialization
    //@{
    /// Default constructor
    LubRanges(void);
    /// Initialize with ranges for variable implementation \a x
    LubRanges(const CpltSet::CpltSetVarImp* x);
    /// Initialize with ranges for variable implementation \a x
    void init(const CpltSet::CpltSetVarImp* x);
    //@}
  };

  forceinline
  LubRanges<CpltSet::CpltSetVarImp*>::LubRanges(void) {}

  inline
  LubRanges<CpltSet::CpltSetVarImp*>
  ::LubRanges(const CpltSet::CpltSetVarImp* x) {
    CpltSet::LubValues<CpltSet::CpltSetVarImp*> v(x);
    Iter::Values::ToRanges<
      CpltSet::LubValues<CpltSet::CpltSetVarImp*> >::init(v);
  }

  inline void 
  LubRanges<CpltSet::CpltSetVarImp*>::init(const CpltSet::CpltSetVarImp* x) {
    CpltSet::LubValues<CpltSet::CpltSetVarImp*> v(x);
    Iter::Values::ToRanges<
      CpltSet::LubValues<CpltSet::CpltSetVarImp*> >::init(v);
  }
  
  /// Range iterator for the unknown set of CpltSet variable implementation
  template <> 
  class UnknownRanges<CpltSet::CpltSetVarImp*> 
    : public Iter::Values::ToRanges<CpltSet::UnknownValues<CpltSet::CpltSetVarImp*> > {
  public:
    /// \name Constructors and initialization
    //@{
    /// Default constructor
    UnknownRanges(void);
    /// Initialize with ranges for variable implementation \a x
    UnknownRanges(const CpltSet::CpltSetVarImp* x);
    /// Initialize with ranges for variable implementation \a x
    void init(const CpltSet::CpltSetVarImp* x);
    //@}
  };

  forceinline
  UnknownRanges<CpltSet::CpltSetVarImp*>::UnknownRanges(void) {}

  inline
  UnknownRanges<CpltSet::CpltSetVarImp*>
  ::UnknownRanges(const CpltSet::CpltSetVarImp* x) {
    CpltSet::UnknownValues<CpltSet::CpltSetVarImp*> v(x);
    Iter::Values::ToRanges<CpltSet::UnknownValues<
      CpltSet::CpltSetVarImp*> >::init(v);
  }

  inline void 
  UnknownRanges<CpltSet::CpltSetVarImp*>
  ::init(const CpltSet::CpltSetVarImp* x) {
    CpltSet::UnknownValues<CpltSet::CpltSetVarImp*> v(x);
    Iter::Values::ToRanges<CpltSet::UnknownValues<
      CpltSet::CpltSetVarImp*> >::init(v);
  }

}}

// STATISTICS: cpltset-var