bddmanager.icc

Go to the documentation of this file.

/*
 *  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 {
  
  class GECODE_VTABLE_EXPORT BddMgrException : public Exception {
  public:
    BddMgrException(const char* l);
  };

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

  class BddMgr {
  private:
    bddStat info;
    int _size;
    int _offset;
    int dummy_offset;
    int dummy_range;
  public:
    BddMgr(void);
    GECODE_CPLTSET_EXPORT ~BddMgr(void);
    
    void init(int n, int c);

    bool leaf(const bdd& b) const;
    bool cfalse(const bdd& b) const;
    bool ctrue(const bdd& b) const;
    void setorder(int* hls);
    unsigned int bddsize(const bdd& b) const;
    unsigned int bddpath(const bdd& b) const;
    GECODE_CPLTSET_EXPORT unsigned int numberOfPaths(bdd& b);
    bdd bddpos(int i) const;
    bdd negbddpos(int i) const;

    int lbCard(const bdd& b);
    int ubCard(const bdd& b);

    void lbCard(const bdd& b, int l);
    void ubCard(const bdd& b, int r);

    bdd ite(const bdd& v, const bdd& t, const bdd& f);
    void mark(const bdd& b);
    void unmark(const bdd& b);
    bool marked(const bdd& b) const;

    int node_level(const bdd& b) const;
    int bdd2var(int i);
    int var2bdd(int i);
    int dummy(void);
    bdd iftrue(bdd& b);
    bdd iffalse(bdd& b);
    const unsigned int bddidx(const bdd& b);
    
    void existquant(bdd& dom, bdd& d, int* var, int s);
    void existquant(bdd& dom, bdd& d, int a, int b);
    void existquant(bdd& dom, bdd& d, bdd& pr);
    bdd eliminate(bdd& d, int a, int b);
    bdd eliminate(bdd& d, bdd& e);
    bdd eliminate(bdd& d, int* var, int s);
    void markdummy(int a, int b);

    void dispose(void);
    void dispose(int offset, int range, int freenodes = 0);
    void dispose(bdd& d);
    int allocate(int r);
    int varnum(void);
    void bddntf(std::ostream&, bdd& b);
    void bdd2dot(const bdd& b) const;
    unsigned int allocated(void);
    void print_set(const bdd& b);
    int offset(void) const;
    void setmaxinc(int max);
    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