MLHom.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 */
/*                                                                          */
/****************************************************************************/
 
#ifndef __MLHOM__H__
#define __MLHOM__H__
 
#include "ddd/Hom.h"
#include "ddd/AdditiveMap.hpp"
 
class MLHom;
 
typedef AdditiveMap<GHom,GDDD> HomNodeMap ;
 
typedef  AdditiveMap<GHom,MLHom> HomHomMap; 
 
 
class _MLHom;
class StrongMLHom;
 
class MLHom {
 
  friend MLHom operator+(const MLHom &,const MLHom &);
  const _MLHom* concret;
 
#ifdef HASH_STAT
  // open access to instrumented hashtable
  template <class Value, class Key, class HashFcn,
  class ExtractKey, class SetKey, class EqualKey, class Alloc>
  friend class google::sparse_hashtable;
#endif
  
public :
 
  static const MLHom id;
 
  MLHom():concret(id.concret){};
  
  MLHom(const GHom &h);
  MLHom (const GHom & up, const MLHom & down);
  MLHom (const _MLHom &);
  MLHom (_MLHom *);
  MLHom (const _MLHom *);
  
  
  MLHom(int var, int val, const MLHom &h=MLHom::id);  
 
  virtual ~MLHom();
 
  
  bool operator<(const MLHom &h) const {return concret<h.concret;};
  bool operator==(const MLHom &h) const {return concret==h.concret;};
  size_t hash() const { return ddd::knuth32_hash(reinterpret_cast<size_t>(concret)); };
  
    HomNodeMap eval(const GDDD &d) const ;
  HomNodeMap operator() (const GDDD &) const;
 
  
  static void garbage();
 
};
 
MLHom operator+(const MLHom &,const MLHom &); 
 
class _MLHom {
  mutable int refCounter;
  mutable bool marking;
 
  friend class MLHom;
 
  virtual void mark() const{};
 
  
public:
  _MLHom (int ref=0) : refCounter(ref),marking(false) {}
  virtual bool shouldCache () const { return true ; }
 
  virtual ~_MLHom(){};
  virtual HomNodeMap eval(const GDDD &) const = 0;
 
  virtual size_t hash() const = 0;
  virtual bool operator==(const _MLHom &h) const=0;
  // for use by unique table : return new MyConcreteClassName(*this);
  virtual _MLHom * clone () const =0 ;
  
};
 
class StrongMLHom : public _MLHom {
public :
 
  bool operator==(const _MLHom &h) const;
 
  virtual bool operator==(const StrongMLHom &) const=0;
 
  HomNodeMap eval(const GDDD &) const ;
 
  virtual HomHomMap phi (int var,int val) const=0;   
  virtual HomNodeMap phiOne () const=0;   
 
};
 
#endif