Hom.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 HOM_H_
#define HOM_H_
 
#include "ddd/DDD.h"
#include "ddd/util/hash_support.hh"
#include "ddd/util/set.hh"
 
#include <map>
#include <cassert>
#include <iostream>
/**********************************************************************/
 
class _GHom;
class StrongHom;
class MyGHom;
class MLHom;
 
class GHom {
private:
  friend class Hom;
  friend class _GHom;
  friend GHom fixpoint(const GHom &, bool);
  friend GHom monotonic(const d3::set<GHom>::type & set);
  friend GHom operator+(const GHom &,const GHom &);
  friend GHom operator&(const GHom &,const GHom &); 
  friend GHom operator*(const GDDD &,const GHom &); 
  friend GHom operator*(const GHom &,const GDDD &); 
  friend GHom operator^(const GDDD &,const GHom &);
  friend GHom operator^(const GHom &,const GDDD &); 
  friend GHom operator-(const GHom &,const GDDD &); 
  
#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
  
  const _GHom* concret;
public:
  typedef GDDD NodeType;
  GHom(const _GHom *_h):concret(_h){};
 
  GHom(_GHom *_h);
 
  GHom(const _GHom &_h);
 
  GHom():concret(id.concret){};
 
  GHom(const MLHom &);
  
  GHom(const GDDD& d);   
  GHom(int var, int val, const GHom &h=GHom::id);  
 
  static const GHom id;
 
 
  bool operator==(const GHom &h) const{return concret==h.concret;};
  bool operator!=(const GHom &h) const{return concret!=h.concret;};
  bool operator<(const GHom &h) const;
  bool is_selector() const;
 
        typedef d3::set<int>::type range_t;
        typedef range_t::const_iterator range_it;
        const range_t  get_range () const;  
        static const range_t full_range;
        
  GHom invert (const GDDD & pot) const;
 
  GDDD has_image (const GDDD & d) const;
 
  GHom negate () const;  
 
  GDDD operator()(const GDDD &d) const; 
  GDDD eval(const GDDD &d) const;
  
  bool skip_variable(int var) const ;
 
  GHom compose (const GHom &r) const ;
 
  int refCounter() const;
 
    static GHom add(const d3::set<GHom>::type & set);
 
    static GHom ccompose(const d3::set<GHom>::type & set);
 
 
  // pretty print of homomorphisms
  friend std::ostream & operator << (std::ostream & os, const GHom & h);
 
 
  static  unsigned int statistics();
  static void pstats(bool reinit=true);
  void mark()const;
  size_t hash () const { 
    return ddd::knuth32_hash(reinterpret_cast<size_t>(concret));
  }
  static void garbage(); 
};
 
 
 
/* Operations */
 
GHom fixpoint(const GHom &, bool is_top_level=false);
GHom operator! (const GHom & cond);
GHom ITE (const GHom & cond, const GHom & iftrue, const GHom & iffalse);
 
GHom operator+(const GHom &,const GHom &); 
GHom operator&(const GHom &,const GHom &); // composition
GHom operator*(const GDDD &,const GHom &); 
GHom operator*(const GHom &,const GDDD &); 
GHom operator*(const GHom &,const GHom &);
GHom operator^(const GDDD &,const GHom &); 
GHom operator^(const GHom &,const GDDD &); 
GHom operator-(const GHom &,const GDDD &); 
 
GHom apply2k (const GDDD &);
 
GDDD computeDomain (int var, const GDDD& );
 
bool commutative (const GHom & h1, const GHom & h2);
 
 
 
 
 
class Hom:public GHom /*, public DataSet*/ {
 public:
  /* Constructor */
 
  Hom(const GHom &h=GHom::id);
  Hom(const Hom &h);
  Hom(const GDDD& d);   // constant
  Hom(int var, int val, const GHom &h=GHom::id);  // var -- val -> Id
  ~Hom();
 
 
  Hom &operator=(const GHom &);
  Hom &operator=(const Hom &);
};
 
/******************************************************************************/
 
namespace std {
  template<>
  struct less<GHom> {
    bool operator()(const GHom &g1,const GHom &g2) const{
      return g1<g2;
    }
  };
}
 
/**********************************************************************/
class _GHom{
private:
  friend class GHom;
  friend class Hom;
  mutable int refCounter;
  mutable bool marking;
  mutable bool immediat;
  size_t creation_counter;
 
  GDDD eval_skip(const GDDD &) const;
public:
  // made public ONLY for the cache, not part of normal API, use GHom has_image instead (cache etc...).
  GDDD has_image_skip(const GDDD &) const;
 
 
     virtual bool
    skip_variable(int) const
    {
        return false;
    }
    virtual bool
    is_selector() const
    {
        return false;
    }
 
        virtual const GHom::range_t get_range () const 
    {
                return GHom::full_range;
    }
        
      virtual GHom invert (const GDDD & ) const {
        // default = raise assert
        if ( is_selector() ) {
          // A default implementation is provided for selector homomorphisms, overloadable.
          return this;
        }
        // No default implem if ! is_selector 
        std::cerr << "Cannot invert homomorphism : " ;
        print (std::cerr);
        std::cerr << std::endl ;        
        assert(0); 
        return GHom(GDDD::null);
      }
 
 
  _GHom(int ref=0,bool im=false):refCounter(ref),marking(false),immediat(im){
    // creation counter
    static size_t counter = 0;
    creation_counter = counter++;
  }
  virtual ~_GHom(){};
 
 
  virtual bool operator==(const _GHom &h) const=0;
  bool operator< (const _GHom &h) const;
  virtual size_t hash() const=0;
 
  // for use by unique table : return new MyConcreteClassName(*this);
  virtual _GHom * clone () const =0 ;
 
  virtual GDDD eval(const GDDD &)const=0;
 
  virtual void mark() const{};
 
  virtual GDDD has_image(const GDDD &) const;
  virtual GHom negate () const;  
 
 
  virtual GHom compose (const GHom &r) const ;
 
  virtual void print (std::ostream & os) const = 0;
  
  // Enable access to the concrete GHom for _GHom homorphisms
  static const _GHom*
  get_concret(const GHom& ghom)
  {
    return ghom.concret;
  }
  
  
};
 
class StrongHom
        :
    public _GHom
{
public:
  StrongHom(){};
  virtual ~StrongHom(){};
  virtual GDDD phiOne() const{return GDDD::top;}; 
  virtual GHom phi(int var,int val) const=0; 
  virtual bool operator==(const StrongHom &h) const=0;
  
  bool operator==(const _GHom &h) const;
 
  virtual void print (std::ostream & os) const ;
 
 
  GDDD eval(const GDDD &)const; 
 
  virtual GDDD has_image (const GDDD &) const;
 
};
 
 
class MyGHom:public _GHom{};
 
#endif /* HOM_H_ */