SDD.h

Go to the documentation of this file.

/****************************************************************************/
/*                                                                          */
/* This file is part of libDDD, a library for manipulation of DDD and SDD.  */
/*                                                                          */
/*     Copyright (C) 2001-2008 Yann Thierry-Mieg, Jean-Michel Couvreur      */
/*                             and Denis Poitrenaud                         */
/*                                                                          */
/*     This program is free software; you can redistribute it and/or modify */
/*     it under the terms of the GNU Lesser General Public License as       */
/*     published by the Free Software Foundation; either version 3 of the   */
/*     License, or (at your option) any later version.                      */
/*     This program is distributed in the hope that it will be useful,      */
/*     but WITHOUT ANY WARRANTY; without even the implied warranty of       */
/*     MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the        */
/*     GNU LEsserGeneral Public License for more details.                   */
/*                                                                          */
/* You should have received a copy of the GNU Lesser General Public License */
/*     along with this program; if not, write to the Free Software          */
/*Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA */
/*                                                                          */
/****************************************************************************/
 
/* -*- C++ -*- */
#ifndef SDD_H
#define SDD_H
 
 
#include <string>
 
#include "ddd/UniqueTable.h"
#include "ddd/DataSet.h"
 
 
// #define HEIGHTSDD
 
class _GSDD;
 
/******************************************************************************/
class GSDD :public DataSet {
private:
  friend std::ostream& operator<<(std::ostream &os,const GSDD &g);
  friend class SDD;
  friend class _GSDD;
  const _GSDD *concret;
  void print(std::ostream& os,std::string s) const;
public:
 
  typedef std::vector<std::pair<DataSet *,GSDD> > Valuation;
  typedef Valuation::const_iterator const_iterator;
  int variable() const;
  const_iterator begin() const;
  const_iterator end() const;
 
 
 
 
  
  /* Constructeurs */
 
  GSDD(int variable,Valuation value);
  GSDD():concret(null.concret){};
  GSDD(int var,const DataSet & val,const GSDD &d=one ); //var-val->d
  GSDD(int var,const GSDD & val,const GSDD &d=one ); //var-val->d
  GSDD(int var,const class SDD & val,const GSDD &d=one ); //var-val->d
  GSDD(const _GSDD &_g); 
  GSDD(_GSDD *_g); 
  GSDD(const _GSDD *_g); 
 
  /* Constants */
 
  static const GSDD one;
  static const GSDD null;
  static const GSDD top;
 
 
  /* Compare */
 
  bool operator==(const GSDD& g) const{return concret==g.concret;};
  bool operator!=(const GSDD& g) const{return concret!=g.concret;};
    bool operator<(const GSDD& g) const ;
  
 
  /* Visualisation */ 
  /* Accessors */ 
  unsigned int refCounter() const;
  unsigned long int size() const;
  // Returns the size in number of nodes of a SDD + DDD mixed structure. 
  // \return a pair <number of SDD nodes,number of DDD nodes>
  std::pair<unsigned long int,unsigned long int> node_size() const;
  size_t nbsons () const;
  long double nbStates() const;
#ifdef HEIGHTSDD
  short int getHeight () const;
#endif
 
#ifdef EVDDD
  int getMinDistance () const;
  GSDD normalizeDistance (int n) const;
#endif
 
  //  long double GSDD::noSharedSize() const;
 
 
  /* Memory Manager */
 
  static  unsigned int statistics();
  void mark()const;
  size_t hash () const { 
    return ddd::knuth32_hash(reinterpret_cast<size_t>(concret));
  }
  static void garbage();
  static void pstats(bool reinit=true);
  static size_t peak();
 
 
 
  // DataSet interface
  DataSet *newcopy () const { return new GSDD(*this); }
  DataSet *set_intersect (const DataSet & b) const ;
  DataSet *set_union (const DataSet & b)  const;
  DataSet *set_minus (const DataSet & b) const;
  bool empty() const;
  DataSet *empty_set() const;
  bool set_equal(const DataSet & b) const;
  bool set_less_than (const DataSet & b) const ;
  long double set_size() const;
  size_t set_hash() const;
  void set_print (std::ostream &os) const { os << *this; }
 
 
};
 
 
std::ostream& operator<<(std::ostream &,const GSDD &);
/* Binary operators */
GSDD operator^(const GSDD&,const GSDD&); // concatenation
GSDD operator+(const GSDD&,const GSDD&); // union
GSDD operator*(const GSDD&,const GSDD&); // intersection
GSDD operator-(const GSDD&,const GSDD&); // difference
 
 
/******************************************************************************/
class SDD:public GSDD {
public:
  /* Constructeur */
  SDD(const SDD &);
  SDD(const GSDD &g=GSDD::null);
  SDD(int var,const DataSet& val,const GSDD &d=one ); //var-val->d
  SDD(int var,const GSDD& val,const GSDD &d=one ); //var-val->d
  // to disambiguate when using SDD as referenced type
  SDD(int var,const SDD& val,const GSDD &d=one ); //var-val->d
  virtual ~SDD(); 
 
  /* Set */
 
  SDD &operator=(const GSDD&);
  SDD &operator=(const SDD&);
 
#ifdef EVDDD
  virtual DataSet *normalizeDistance(int n) const { return new SDD(GSDD::normalizeDistance(n)); }
  virtual int getMinDistance() const { return GSDD::getMinDistance();}
#endif
 
 
};
 
namespace SDDutil {
  UniqueTable<_GSDD> * getTable ();
  void foreachTable (void (*foo) (const GSDD & g)); 
}
 
 
namespace std {
  template<>
  struct less<GSDD> {
    bool operator()(const GSDD &g1,const GSDD &g2) const{
      return g1<g2;
    }
  };
}
 
 
 
 
#endif