/* -*- 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-27 17:49:28 +0100 (Wed, 27 Feb 2008) $ by $Author: tack $
 *     $Revision: 6327 $
 *
 *  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.
 *
 */

#include <iostream>

namespace Gecode { namespace CpltSet {

  enum NodeStatus {
    INIT = -1,
    FIX_GLB = 1,
    FIX_NOT_LUB = 0,
    FIX_UNKNOWN = 2,
    UNDET = 5
  };

  /// Iterate the values in the greatest lower bound of a CpltSetvariable
  template <class T> class GlbValues {
  public:
    /// \name Constructors and initialization
    //@{
    /// Default constructor
    GlbValues(void);
    /// Initialize with least upper bound ranges for set variable \a x
    GlbValues(const T& x);
    /// Initialize with least upper bound ranges for set variable \a x
    void init(const T& x);
    //@}
    /// \name Iteration control
    //@{
    /// Test whether iterator is still at a range or done
    bool operator()(void) const;
    /// Move iterator to next range (if possible)
    void operator++(void);
    //@}
    /// \name Value access
    //@{
    /// Return current value
    int val(void) const;
    //@}
  };

  /// Iterate the values in the least upper bound of a bdd set variable
  template <class T> class LubValues {
  public:
    /// \name Constructors and initialization
    //@{
    /// Default constructor
    LubValues(void);
    /// Initialize with least upper bound ranges for set variable \a x
    LubValues(const T& x);
    /// Initialize with least upper bound ranges for set variable \a x
    void init(const T& x);
    //@}
    /// \name Iteration control
    //@{
    /// Test whether iterator is still at a range or done
    bool operator()(void) const;
    /// Move iterator to next range (if possible)
    void operator++(void);
    //@}
    /// \name Value access
    //@{
    /// Return minimum of current range
    int min(void) const;
    /// Return maximum of current range
    int max(void) const;
    //@}
  };

  /// Iterate the values lub-glb of a bdd set variable
  template <class T> class UnknownValues {
  public:
    /// \name Constructors and initialization
    //@{
    /// Default constructor
    UnknownValues(void);
    /// Initialize with least upper bound ranges for set variable \a x
    UnknownValues(const T& x);
    /// Initialize with least upper bound ranges for set variable \a x
    void init(const T& x);
    //@}
    /// \name Iteration control
    //@{
    /// Test whether iterator is still at a range or done
    bool operator()(void) const;
    /// Move iterator to next range (if possible)
    void operator++(void);
    //@}
    /// \name Value access
    //@{
    /// Return current value
    int val(void) const;
    //@}
  };

  /**
   * \brief Finite integer set variable implementation using a complete domain 
   * representation
   *
   * \ingroup Other
   */  
  class CpltSetVarImp : public CpltSetVarImpBase {
    friend class BddIterator;
    friend class DomBddIterator;

    friend class GlbValues<CpltSetVarImp*>;
    friend class LubValues<CpltSetVarImp*>;
    friend class UnknownValues<CpltSetVarImp*>;

  public:
    /// Returned by empty sets when asked for their maximum element
    static const int MAX_OF_EMPTY = Gecode::Set::Limits::min-1;
    /// Returned by empty sets when asked for their minimum element
    static const int MIN_OF_EMPTY = Gecode::Set::Limits::max+1;

    void printdom(void) const;
  private:
    /// Binary decision diagram representing the domain of this variable
    bdd domain;
    /// Initial minimum of the domain, needed for bdd operations
    int min;
    /// Initial maximum of the domain, needed for bdd operations
    int max;
    /** \brief Starting index of the bdd variable vector for this CpltSet 
      * variable in the bdd table
      */
    unsigned int _offset;
    /// Cache whether the variable is assigned
    bool _assigned;
  protected:
    /// Constructor for cloning \a x
    GECODE_CPLTSET_EXPORT
    CpltSetVarImp(Space* home, bool share, CpltSetVarImp& x);
    /// Produce bdd representing \a i for this variable
    template <class I>
    bdd iterToBdd(I& i);

  public:
    /// Construct variable with given domain
    GECODE_CPLTSET_EXPORT
    CpltSetVarImp(Space* home, int glbMin, int glbMax, int lubMin, int lubMax, 
                  unsigned int cardMin, unsigned int cardMax);
    /// Construct variable with given domain
    GECODE_CPLTSET_EXPORT
    CpltSetVarImp(Space* home, const IntSet& glbD, int lubMin, int lubMax, 
                  unsigned int cardMin, unsigned int cardMax);
    /// Construct variable with given domain
    GECODE_CPLTSET_EXPORT
    CpltSetVarImp(Space* home, int glbMin, int glbMax, const IntSet& lubD,
                  unsigned int cardMin, unsigned int cardMax);
    /// Construct variable with given domain
    GECODE_CPLTSET_EXPORT
    CpltSetVarImp(Space* home, const IntSet& glbD,const IntSet& lubD,
                  unsigned int cardMin, unsigned int cardMax);
    // Delete a bdd variable
    GECODE_CPLTSET_EXPORT
    void dispose(Space* home);
  public:
    /// \name Set bounds update by value
    //@{
    /// Exclude value \a v from lub
    ModEvent exclude(Space* home, int v);
    /// Exclude range \f$ [a,\dots, b] \f$ from
    GECODE_CPLTSET_EXPORT ModEvent exclude(Space* home, int a, int b);

    /// Include value \a v in glb
    ModEvent include(Space* home, int v);
    /// Include range \f$ [a,\dots, b] \f$ in glb
    GECODE_CPLTSET_EXPORT ModEvent include(Space* home, int a, int b);

    /// Intersect domain with singleton set \f$ \{i\} \f$
    ModEvent intersect(Space* home, int i);
    /// Intersect domain with range \f$ [a..b] \f$
    GECODE_CPLTSET_EXPORT ModEvent intersect(Space* home, int a, int b);
    //@}

    /// \name Set bounds update by range iterator
    //@{
    /// Intersect domain with range sequence described by \a i
    template <class I> ModEvent intersectI(Space* home, I& i);
    /// Exclude set described by range sequence \a i from lub
    template <class I> ModEvent excludeI(Space* home, I& i);  
    /// Include set described by range list \a i in glb
    template <class I> ModEvent includeI(Space* home, I& i);  
    //@}

    /// \name Set cardinality update 
    //@{
    /// Restrict cardinality to be at least l and at most u
    GECODE_CPLTSET_EXPORT ModEvent cardinality(Space* home, int l, int u);
    /// Restrict cardinality to be at least n
    ModEvent cardMin(Space* home,unsigned int n);
    /// Restrict cardinality to be at most n
    ModEvent cardMax(Space* home,unsigned int n);
    //@}

    /// \name Set domain update by value
    //@{
    /// Restrict domain values to be different from singleton set \f$\{v\}\f$.
    ModEvent nq(Space* home, int v);
    /// Restrict domain values to be different from range \f$[a,b]\f$.
    GECODE_CPLTSET_EXPORT ModEvent nq(Space* home, int a, int b);

    /// Restrict domain to be equal to singleton set \f$\{v\}\f$.
    ModEvent eq(Space* home, int v);
    /// Restrict domain to be equal to range \f$[a,b]\f$.
    GECODE_CPLTSET_EXPORT ModEvent eq(Space* home, int a, int b);
    //@}

    /// \name Set domain update by range iterator
    //@{
    /// Restrict domain values to be different from set described by \a i.
    template <class I> ModEvent nqI(Space* home, I& i);
    /// Restrict domain to be equal to the range sequence \a i
    template <class I> ModEvent eqI(Space* home, I& i);
    //@}

    /// \name Set domain update by bdd
    //@{
    /// Intersect domain with the domain represented by \a d
    GECODE_CPLTSET_EXPORT ModEvent intersect(Space* home, bdd& d);
    //@}
    
    /// \name Value access
    //@{

    /// Return current cardinality minimum
    unsigned int cardMin(void) const;
    /// Return current cardinality maximum
    unsigned int cardMax(void) const;

    /// Return minimum of the greatest lower bound
    GECODE_CPLTSET_EXPORT int glbMin(void) const;
    /// Return maximum of the greatest lower bound
    GECODE_CPLTSET_EXPORT int glbMax(void) const;
    /// Return the size of the greatest lower bound
    GECODE_CPLTSET_EXPORT unsigned int glbSize(void) const;
    /// Return minimum of the least upper bound
    GECODE_CPLTSET_EXPORT int lubMin(void) const;
    /// Return maximum of the least upper bound
    GECODE_CPLTSET_EXPORT int lubMax(void) const;
    /// Return the size of the least upper bound
    GECODE_CPLTSET_EXPORT unsigned int lubSize(void) const;
    /// Return \a n -th smallest element in the least upper bound
    GECODE_CPLTSET_EXPORT int lubMinN(int n) const;
    /// Return \a n -th largest element in the least upper bound
    GECODE_CPLTSET_EXPORT int lubMaxN(int n) const;

    /// Return minimum of the difference between the greatest lower and the least upper bound
    GECODE_CPLTSET_EXPORT int unknownMin(void) const;
    /// Return maximum of the difference between the greatest lower and the least upper bound
    GECODE_CPLTSET_EXPORT int unknownMax(void) const;
    /// Return the size of the difference between the greatest lower and the least upper bound
    GECODE_CPLTSET_EXPORT unsigned int unknownSize(void) const;

    //@}


    /// \name Bdd information 
    //@{
    /// Return the initial minimum of the least upper bound
    int initialLubMin(void) const;
    /// Return the initial maximum of the least upper bound
    int initialLubMax(void) const;
    /** \brief Return the number of bdd variables allocated for this variable 
      * (initialLubMax-initialLubMin) */
    unsigned int tableWidth(void) const;
    /** \brief Return the offset in the global bdd table where the variable's 
      * domain starts */
    unsigned int offset(void) const;
    /** \brief Return bdd for the \a i -th element of this variable (counting 
      * from initialLubMin) */
    bdd element(int i) const;
    /** \brief Return negated bdd for the \a i -th element of this variable 
      * (counting from initialLubMin) */
    bdd elementNeg(int i) const;
    /// Return the bdd representing the current domain
    bdd dom(void) const;
    //@}

    /// \name Domain tests
    //@{
    /// Test whether variable is assigned
    GECODE_CPLTSET_EXPORT bool assigned(void) ;
    /// Test whether \a i is contained in the greatest lower bound
    GECODE_CPLTSET_EXPORT bool knownIn(int i) const;
    /// Test whether \a i is not contained in the least upper bound
    GECODE_CPLTSET_EXPORT bool knownOut(int i) const;
    /// Test whether domain is a range 
    bool range(void) const;
    //@}
    
    /// \name Dependencies
    //@{
    /// Subscribe propagator \a p with propagation condition \a pc to variable
    void subscribe(Space* home, Propagator* p, PropCond pc, bool process=true);
    /// Cancel subscription of propagator \a p with propagation condition \a pc
    void cancel(Space* home, Propagator* p, PropCond pc);
    //@}

  private:
    /// Return copy of not-yet copied variable
    GECODE_CPLTSET_EXPORT 
    CpltSetVarImp* perform_copy(Space* home, bool share);

  public:
    /// \name Cloning
    //@{
    /// Return copy of this variable
    CpltSetVarImp* copy(Space* home, bool share);
    //@}  

    /// \name Reflection
    //@{
    GECODE_CPLTSET_EXPORT Reflection::Arg*
    spec(const Space* home, Reflection::VarMap& m) const;
    //@}

    /// \name Delta information for advisors
    //@{
    /// Return modification event
    static ModEvent modevent(const Delta* d);
    //@}

  };


  /**
   * \brief Iterator for level-wise iteration over a given bdd
   *
   * \note This iterator computes the complete node information in its
   *       constructor and init function in \f$ O(N)\f$, where N is the
   *       number of nodes of the iterated bdd
   */
  class BddIterator {
  private:
    // Stores the bdd to be iterated
    bdd c;
    // Stores the current sub-bdd under exploration
    bdd cur;
    // ensure that there are no marked nodes when we leave the iterator
    int markref;
    // Number of nodes of c
    int n;
    // Range size of the initial variable domain, i.e. \f$ |[min, max]| \f$
    int m;
    // Stores for each node whether it is fixed, nonfixed or undetermined
    NodeStatus flag;
    bool singleton;
    // Explores the iterated bdd
    SharedArray<bdd> nodes;
    // Left end of the nodes array
    int l;
    // Right end of the nodes array
    int r;
    // If bypassed is true the current level cannot be fixed
    bool bypassed;
    // If on the same level an internal node has only leaf childs
    // and on another path has at least some internal child
    // then this child cannot be fixed
    bool onlyleaves;
    // The number of the current level in the bdd
    int _level;
    
    // marks all nodes in the cache 
    GECODE_CPLTSET_EXPORT void cache_mark(void);
    // unmarks all nodes in the cache 
    GECODE_CPLTSET_EXPORT void cache_unmark(void);
  public:
    /// \name Constructors and initialization
    //@{
    BddIterator(void);
    BddIterator(const bdd&);
    GECODE_CPLTSET_EXPORT void init(const bdd&);
    //@}
    /// \name Iteration control
    //@{
    /// Test whether iterator is still valid or done
    bool operator()(void) const;
    /// Move iterator to next level in the bdd
    GECODE_CPLTSET_EXPORT void operator++(void);
    //@}
    /// \name Status information
    //@{
    /// Retrieves the status of the current level
    NodeStatus status(void) const;
    /// Retrieves the current level
    int level(void) const;
    /// Retrieves the current label
    int label(void) const;
    /// Test whether agenda is empty
    bool empty(void) const;
    /// Retrieve number of nodes of iterated bdd
    int size(void) const;
    //@}
  };


  /// Iterator for level-wise iteration of a variable domain
  class DomBddIterator : public BddIterator {
  private:
    /// denotes the index in the boolean vector representing the set variable
    int vector_level;
    int mi;
    int ma;
    int off;
    /// denotes the level in the bdd representing the set variable
    int bdd_level;
  protected:
    /// tests whether vector_level and bdd_level are equal
    bool same(void) const;
  public:
    /// \name Constructors and initialization
    //@{
    DomBddIterator(void);
    DomBddIterator(const CpltSetVarImp* x);
    DomBddIterator(const CpltSetVarImp* x, bdd& remain);
    void init(const CpltSetVarImp* x);
    void init(const CpltSetVarImp* x, bdd& remain);
    //@}
    /// \name Iteration control
    //@{
    /// Test whether iterator is still valid or done
    bool operator()(void) const;
    /// Move iterator to next level in the bdd
    void operator++(void);
    //@}
    /// \name Status information
    //@{
    /// Retrieves the status of the current level
    NodeStatus status(void) const;
    /// Retrieves the current value
    int val(void) const;
    //@}
  };

}}

#include "gecode/cpltset/var-imp/cpltset.icc"

namespace Gecode {

  class CpltSetVar;

  /** \brief Traits class for variable implementations and variables */
  template <>
  class VarImpVarTraits<CpltSet::CpltSetVarImp> {
  public:
    typedef CpltSetVar Var;
  };
}

// STATISTICS: cpltset-var