/*
 *  Main authors:
 *     Patrick Pekczynski <pekczynski@ps.uni-sb.de>
 *
 *  Copyright:
 *     Patrick Pekczynski, 2006
 *
 *  Last modified:
 *     $Date: 2007-12-06 14:09:40 +0100 (Thu, 06 Dec 2007) $ by $Author: tack $
 *     $Revision: 5608 $
 *
 *  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 "gecode/support/buddy/bdd.h"

namespace Gecode {
  
  /// %Exception: Error in the Buddy ROBDD manager
  class GECODE_VTABLE_EXPORT BddMgrException : public Exception {
  public:
    /// Initialize with location \a l
    BddMgrException(const char* l);
  };

  inline
  BddMgrException::BddMgrException(const char* l)
    : Exception(l,"Error in ROBDD Manager") {}
  
  namespace CpltSet {

  /**
   * \brief Manager for CpltSetVars. 
   *
   * Used for initialization and destruction of the global lookup table for
   * Bdd nodes and for keeping track between CpltSetVars and their 
   * corresponding indices in the lookup table. 
   */
  class BddMgr {
  private:
    bddStat info;
    /// Number of registered variables
    int _size;
    /// Number of used nodes
    int _offset;
    int dummy_offset;
    int dummy_range;
  public:
    /// Default constructor
    BddMgr(void);
    /// Destructor
    GECODE_CPLTSET_EXPORT ~BddMgr(void);
    
    /// Initialize manager with initial nodesize \a n and cachesize \a c.
    void init(int n, int c);

    /// Test whether bdd \a b is either constant true or constant false
    bool leaf(const bdd& b) const;
    /// Tests whether bdd \a b is constant false
    bool cfalse(const bdd& b) const;
    /// Tests whether bdd \a b is constant true
    bool ctrue(const bdd& b) const;
    /// Sets the variable ordering in the bdd according to \a hls.
    void setorder(int* hls);
    /// Return the size of bdd \a b
    unsigned int bddsize(const bdd& b) const;
    /// Return the number of paths of bdd leading to a true node\a b
    unsigned int bddpath(const bdd& b) const;
    /// Return the total number of paths of bdd \a b
    GECODE_CPLTSET_EXPORT unsigned int numberOfPaths(bdd& b);
    /// Return bdd at position \a i in bdd lookup table
    bdd bddpos(int i) const;
    /// Return negated bdd at position \a i in bdd lookup table
    bdd negbddpos(int i) const;

    /// Get lower cardinality bound for breadth-first iteration
    int lbCard(const bdd& b);
    /// Get upper cardinality bound for breadth-first iteration
    int ubCard(const bdd& b);

    /// Set lower cardinality bound for breadth-first iteration
    void lbCard(const bdd& b, int l);
    /// Set upper cardinality bound for breadth-first iteration
    void ubCard(const bdd& b, int r);

    /// Construct the Bdd for \f$ \mbox{if} v \mbox{then} t \mbox{else} f\f$
    bdd ite(const bdd& v, const bdd& t, const bdd& f);
    /// Marks the bdd \a b
    void mark(const bdd& b);
    /// Unmarks the bdd \a b
    void unmark(const bdd& b);
    /// Check whether \a b is marked
    bool marked(const bdd& b) const;

    int node_level(const bdd& b) const;
    /// Returns the position of variable \a i in the current variable order
    int bdd2var(int i);
    /// Returns the variable at position \a i in the current variable order
    int var2bdd(int i);
    /// Returns the offset of the first dummy var if there is any
    int dummy(void);
    /// Return the true branch of a bdd \a b.
    bdd iftrue(bdd& b);
    /// Return the false branch of a bdd \a b.
    bdd iffalse(bdd& b);
    /// Returns the index of the variable labeling the bdd \a b
    const unsigned int bddidx(const bdd& b);
    
    /// Set the bdd \a dom to \f$ \exists_{V(var)} \left(dom \wedge d\right)\f$
    void existquant(bdd& dom, bdd& d, int* var, int s);
    /// Set the bdd \a dom to \f$ \exists_{V([x_a,\dots,x_b])} \left(dom \wedge d\right)\f$
    void existquant(bdd& dom, bdd& d, int a, int b);
    /// Set the bdd \a dom to \f$ \exists_{V(pr)} \left(dom \wedge d\right)\f$
    void existquant(bdd& dom, bdd& d, bdd& pr);
    /// Set the bdd \a d to \f$ \exists_{V([x_a,\dots,x_b])} d\f$
    bdd eliminate(bdd& d, int a, int b);
    /// Set the bdd \a d to \f$ \exists_{V(e)} d\f$
    bdd eliminate(bdd& d, bdd& e);
    /// Set the bdd \a d to \f$ \exists_{V(var)} d\f$
    bdd eliminate(bdd& d, int* var, int s);
    /// Marks in the table, whether dummy nodes have been allocated so far.
    void markdummy(int a, int b);

    /// Free the node table
    void dispose(void);
    /// Free variable in the node table
    void dispose(int offset, int range, int freenodes = 0);
    /// Free nodes for bdd \a d in the table
    void dispose(bdd& d);
    /** 
     * \brief Subscribe a variable to the lookup table
     *  Returns the offset where the first node starts.
     */
    int allocate(int r);
    /// return the number of used bdd variables
    int varnum(void);
    /// Prints a bdd node \a b with its true edge and its false edge.
    void bddntf(std::ostream&, bdd& b);
    /// Prints dot-output of a bdd \a b.
    void bdd2dot(const bdd& b) const;
    /// Return the number of allocated bdd variables for the set elements in the table
    unsigned int allocated(void);
    /// Set print of a bdd
    void print_set(const bdd& b);
    /// Return the current offset of the manager
    int offset(void) const;
    /// Memory Management
    void setmaxinc(int max);
    /// Check whether the buddy library has already been initialized 
    bool available(void);
  };

  forceinline bool
  BddMgr::available(void) { return bdd_isrunning(); }

  forceinline bool 
  BddMgr::leaf(const bdd& b) const{ return b == bdd_true() || b == bdd_false(); }

  forceinline bool 
  BddMgr::cfalse(const bdd& b) const{ return b == bdd_false(); }

  forceinline bool 
  BddMgr::ctrue(const bdd& b) const{ return b == bdd_true(); }

  forceinline
  BddMgr::BddMgr(void)
  : _size(0), _offset(0), dummy_offset( -1), dummy_range(-1) {}

  forceinline void
  BddMgr::dispose(void) {
    if (available()) { 
      bdd_done(); 
    }
    _size = 0;
    _offset = 0;
    dummy_offset = -1; 
    dummy_range = -1;
  }
   
  forceinline void
  BddMgr::init(int n, int c) {  
    _size = 0;
    _offset = 0;
    dummy_offset = -1; 
    dummy_range = -1;
    bdd_init(n, c);
    
    info.produced = -1;
    info.nodenum = -1;
    info.maxnodenum = -1;
    info.freenodes= -1;
    info.minfreenodes= -1;
    info.varnum= -1;
    info.cachesize= -1;
    info.gbcnum= -1;
  }

  forceinline void
  BddMgr::print_set(const bdd& b) {
    bdd_printset(b);
  }

  forceinline bdd
  BddMgr::bddpos(int i) const{ return bdd_ithvarpp(i); }

  forceinline int 
  BddMgr::allocate(int r) {
    assert(available());
    _size++;
    bdd_stats(&info);
    if (dummy_offset > - 1) {
      if (dummy_range < r) {
        for (int i = dummy_range; i < r; i++) { bdd v = bddpos(i); }
      } else {
        int initoffset = dummy_offset;
        if (dummy_range > r) {
          _offset = dummy_offset;
          _offset += r;
        } else {
          dummy_offset = -1;
        }
        return initoffset;
      }
    }

    // increase on number of allocated bdd variables
    bdd_extvarnum(r);

    for (int i = _offset; i < _offset + r; i++) { bdd v = bddpos(i); }

    int initoffset = _offset;
    _offset += r;
    return initoffset;
  }

  forceinline unsigned int
  BddMgr::allocated(void) {
    bdd_stats(&info);
    return info.varnum;
  }


  forceinline bdd
  BddMgr::negbddpos(int i) const{ return bdd_nithvarpp(i); }

  forceinline void 
  BddMgr::mark(const bdd& b) { bdd_mark_node(b); }

  forceinline void
  BddMgr::unmark(const bdd& b) { bdd_unmark_node(b); }

  forceinline bool
  BddMgr::marked(const bdd& b) const { return bdd_marked_node(b); }

  forceinline int
  BddMgr::node_level(const bdd& b) const{ return bdd_level_node(b); }

  forceinline int
  BddMgr::lbCard(const bdd& b) { return bdd_card_lo(b); }

  forceinline int
  BddMgr::ubCard(const bdd& b) { return bdd_card_hi(b); }

  forceinline void
  BddMgr::lbCard(const bdd& b, int l) {  bdd_set_card_lo(b, l); }

  forceinline void
  BddMgr::ubCard(const bdd& b, int r) {  bdd_set_card_hi(b, r); }
  
  forceinline bdd
  BddMgr::ite(const bdd& v, const bdd& t, const bdd& f) {
    return bdd_ite(v, t, f);
  }

  forceinline int
  BddMgr::bdd2var(int i){ return bdd_level2var(i); }

  forceinline int
  BddMgr::var2bdd(int i){ return bdd_var2level(i); }

  forceinline int
  BddMgr::dummy(void){ return dummy_offset; }

  forceinline void
  BddMgr::setorder(int* hls) {
    bdd_setvarorder(hls);
    bdd_disable_reorder();
  }

  forceinline unsigned int
  BddMgr::bddsize(const bdd& b) const{ return bdd_nodecount(b); }

  forceinline unsigned int
  BddMgr::bddpath(const bdd& b) const{
    return static_cast<unsigned int> (bdd_pathcount(b));
  }

  forceinline bdd 
  BddMgr::iftrue(bdd& b) { return bdd_high(b); }

  forceinline bdd 
  BddMgr::iffalse(bdd& b) { return bdd_low(b); }

  forceinline const unsigned int
  BddMgr::bddidx(const bdd& b) {
    if (marked(b)) {
      unmark(b);
      int i = bdd_var(b);
      mark(b);
      return i;
    } else {
      return bdd_var(b);
    }
  }

  forceinline void
  BddMgr::bdd2dot(const bdd& b) const{ bdd_printdot(b); }

  forceinline void
  BddMgr::existquant(bdd& dom, bdd& d, int* var, int s) {
    bdd outvar = bdd_makeset(var, s);
    bdd newdom = bdd_appex(dom, d, bddop_and, outvar);
    dom        = newdom;
  }

  forceinline void
  BddMgr::existquant(bdd& dom, bdd& d, int a, int b) {
    bdd outvar = bdd_true();
    for (int i = a; i <= b; i++) {
      bdd cur = bddpos(i);
      assert(!marked(cur));
      assert(!leaf(cur));
      outvar &= cur;
    }
    bdd newdom = bdd_appex(dom, d, bddop_and, outvar);
    dom = newdom;
  }

  forceinline void 
  BddMgr::existquant(bdd& dom, bdd& d, bdd& pr) {
    dom = bdd_appex(dom, d, bddop_and, pr);
  }

  forceinline bdd
  BddMgr::eliminate(bdd& d, int a, int b) {
    bdd outvar = bdd_true();
    for (int i = a; i <= b; i++) {
      bdd cur = bddpos(i);
      assert(!marked(cur));
      outvar &= cur;
    }
    return bdd_exist(d, outvar);
  }

  forceinline bdd
  BddMgr::eliminate(bdd& d, bdd& e) {
    return bdd_exist(d, e);
  }

  forceinline bdd
  BddMgr::eliminate(bdd& d, int* var, int s) {
    bdd outvar = bdd_makeset(var, s);
    return bdd_exist(d, outvar);
  }

  forceinline void
  BddMgr::markdummy(int a, int b) {
    dummy_offset = a;
    dummy_range  = b;
    _size--;
  }

  forceinline void
  BddMgr::dispose(int offset, int range, int freenodes) {
    if (available()) {
      for (int i = 0; i < range; i++) {  bddpos(offset + i).dispose(); }
      if (_offset == offset + range) { _offset -= range; }
      // this is done in dipose(bdd d)
      info.freenodes += freenodes;
      if (offset == dummy_offset && dummy_offset > -1) {
        dummy_offset = -1;
        dummy_range  = -1;
      }
    }
  }

  forceinline void
  BddMgr::dispose(bdd& d) {
    if (available()) {
      int freenodes = bddsize(d);
      d = bdd_false();
      info.freenodes += freenodes;
    }
  }

  forceinline void
  BddMgr::bddntf(std::ostream& os, bdd& b) {
    os << "(N" << b;
    os <<", T"<< iftrue(b);
    os << ", F" << iffalse(b) << ")";
    os << "[" << bddidx(b) << "]\n";
  }

  forceinline int
  BddMgr::varnum(void) {
    bdd_stats(&info);
    return info.varnum;
  }
  
  forceinline int
  BddMgr::offset(void) const{
    assert(_offset <= bdd_varnum());
    return _offset;
  }

  forceinline void
  BddMgr::setmaxinc(int max) {
    int o = -1;
    o = bdd_setmaxincrease(max);
  }

  GECODE_CPLTSET_EXPORT extern BddMgr manager;

}}

// STATISTICS: cpltset-var