DDD.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 DDD_H
#define DDD_H
 
#include <iosfwd>
#include <string>
#include <vector>
 
#include "ddd/DataSet.h"
#include "ddd/hashfunc.hh"
 
class _GDDD;
 
class DDD;
 
class GDDD 
{
public:
  typedef unsigned int id_t;
private:
  friend std::ostream& operator<<(std::ostream &os,const GDDD &g);
  friend class DDD;
 
  id_t concret;
  GDDD(const id_t &_g);
  GDDD(_GDDD *_g);
  void print(std::ostream& os,std::string s) const;
  void saveNode(std::ostream&, std::vector<id_t>& )const;
  unsigned long int nodeIndex(const std::vector<id_t> &)const;
 
public:
 
 
  typedef short val_t;
  typedef unsigned short valsz_t;
  typedef std::pair<val_t,GDDD> edge_t;
  typedef std::vector<edge_t > Valuation;
  typedef const edge_t * const_iterator;
  int variable() const;
 
  const_iterator begin() const;
  const_iterator end() const;
 
 
 
  GDDD(int variable,const Valuation & value);
  GDDD():concret(null.concret){};
  GDDD(int var,val_t val,const GDDD &d=one );
  GDDD(int var,val_t val1,val_t val2,const GDDD &d=one); //var-[val1,var2]->d
 
 
 
 
  static const GDDD one;
  static const GDDD null;
  static const GDDD top;
 
 
 
  bool operator==(const GDDD& g) const{return concret==g.concret;};
  bool operator!=(const GDDD& g) const{return concret!=g.concret;};
  bool operator<(const GDDD& g) const;
 
  /* Accessors */ 
  unsigned int refCounter() const;
  unsigned long int size() const;
  size_t nbsons () const;
  long double nbStates() const;
  long double noSharedSize() const;
#ifdef EVDDD
  int getMinDistance () const;
  GDDD normalizeDistance (int n) const;
#endif
 
 
 
 
  static void varName( int var, const std::string& name );
  static const std::string getvarName( int var );
 
 
 
  static  unsigned int statistics();
  void mark() const;
  size_t hash () const { 
    return ddd::int32_hash(concret); 
  }
  static void garbage(); 
  static void pstats(bool reinit=true);
  static size_t peak();
 
 
  friend void saveDDD(std::ostream&, std::vector<DDD>);
  friend void loadDDD(std::istream&, std::vector<DDD>&);
};
 
 
std::ostream& operator<<(std::ostream &,const GDDD &);
/* Binary operators */
GDDD operator^(const GDDD&,const GDDD&); 
GDDD operator+(const GDDD&,const GDDD&);
GDDD operator*(const GDDD&,const GDDD&); 
GDDD operator-(const GDDD&,const GDDD&); 
 
 
 
class DDD : public GDDD, public DataSet 
{
public:
  /* Constructors */
  DDD(const DDD &);
  DDD(const GDDD &g=GDDD::null);
 
  DDD(int var,val_t val,const GDDD &d=one ); 
  DDD(int var,val_t val1,val_t val2,const GDDD &d=one); 
  ~DDD(); 
 
 
 
  DDD &operator=(const GDDD&);
  DDD &operator=(const DDD&);
 
 
  
   DataSet *newcopy () const { return new DDD(*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; }
        void mark() const { GDDD::mark(); }
#ifdef EVDDD
   DataSet *normalizeDistance(int n) const { return new DDD(GDDD::normalizeDistance(n)); }
   int getMinDistance() const { return GDDD::getMinDistance();}
#endif
 
 
 
}; // DDD class
 
 
 
namespace std {
  template<>
  struct less<GDDD> {
    bool operator()(const GDDD &g1,const GDDD &g2) const{
      return g1<g2;
    }
  };
}
 
 
#ifdef EVDDD
// the variable id of distance nodes
#define DISTANCE -3
#endif
 
#endif