SHom.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 SHOM_H_
#define SHOM_H_
 
#include "ddd/SDD.h"
#include "ddd/Hom.h"
#include "ddd/Cache.hh"
 
#include "ddd/util/set.hh"
 
/**********************************************************************/
 
class _GShom;
class StrongShom;
class MyGShom;
class MLShom;
 
 
 
class GShom 
{
private:
  friend class Shom;
  friend class _GShom;
 
 
  friend GShom fixpoint(const GShom &, bool is_top_level);
  friend GShom localApply(const GHom &,int target);
  friend GShom localApply(const GShom &,int target);
  friend GShom add(const d3::set<GShom>::type &);
  friend GShom operator+(const GShom &,const GShom &); 
  friend GShom operator&(const GShom &,const GShom &); 
  friend GShom operator*(const GSDD &,const GShom &); 
  friend GShom operator*(const GShom &,const GSDD &); 
  friend GShom operator^(const GSDD &,const GShom &); 
  friend GShom operator^(const GShom &,const GSDD &); 
  friend GShom operator-(const GShom &,const GSDD &);
  
#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 _GShom* concret;
public:
  typedef GSDD NodeType;
 
 
  GShom():concret(id.concret){};
 
  GShom(const _GShom *_h);
 
  GShom(_GShom *_h);
 
   GShom(const _GShom &_h);
 
  GShom(const MLShom &);
 
  GShom(const GSDD& d);   
  GShom(int var,const DataSet& val, const GShom &h=GShom::id);  // var -- val -> Id
 
  static const GShom id;
 
  GShom invert (const GSDD & pot) const;
 
  GSDD has_image (const GSDD & d) const;
  
  GShom compose(const GShom &) const;
 
 
  bool operator==(const GShom &h) const{return concret==h.concret;};
  bool operator!=(const GShom &h) const{return concret!=h.concret;};
  bool operator<(const GShom &h) const{return concret<h.concret;};
  bool is_selector() const;
  bool skip_variable(int) 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;
 
 
 
  GSDD operator()(const GSDD &d) const; 
  GSDD eval(const GSDD &d) const;
  
  int refCounter() const;
 
    static GShom add(const d3::set<GShom>::type & s);
 
  // pretty print of homomorphisms
  friend std::ostream & operator << (std::ostream & os, const GShom & h);
 
 
 
  static  unsigned int statistics();
  static size_t cache_size();
  static size_t cache_peak();
  
  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();
 
  // strategies for fixpoint evaluation insaturation context
  // BFS = do each g_i once then go to g_i+1
  // DFS = do each g_i to saturation then go to g_i+1
  enum fixpointStrategy {BFS, DFS};
  enum saturationStrategy {ORDINARY, RECFIREANDSAT};
 
 private : 
  static fixpointStrategy fixpointStrategy_;
  static saturationStrategy saturationStrategy_;
 
 public :
  static fixpointStrategy getFixpointStrategy() { return fixpointStrategy_; }
  static void setFixpointStrategy(fixpointStrategy strat) { fixpointStrategy_ = strat; }
 
  static saturationStrategy getSaturationStrategy() { return saturationStrategy_; }
  static void setSaturationStrategy(saturationStrategy strat) { saturationStrategy_ = strat; }
 
 
};
 
 
 
 
 
GShom fixpoint(const GShom &, bool is_top_level=false);
 GShom localApply(const GHom &,int target);
 GShom localApply(const GShom &,int target);
 
 GShom extractPotential (int var);
 
GShom ITE (const GShom & cond, const GShom & iftrue, const GShom & iffalse);
 
GShom operator! (const GShom & cond);
 
GShom operator+(const GShom &,const GShom &); 
GShom operator&(const GShom &,const GShom &);
GShom operator*(const GSDD &,const GShom &);
GShom operator*(const GShom &,const GSDD &); 
GShom operator*(const GShom &,const GShom &); 
GShom operator^(const GSDD &,const GShom &); 
GShom operator^(const GShom &,const GSDD &);
GShom operator-(const GShom &,const GSDD &); 
GShom operator-(const GShom &,const GShom &); 
 
GShom apply2k (const GSDD &);
 
 
 
 
class Shom : public GShom 
{
public:
 
 
  Shom(const GShom &h=GShom::id);
  Shom(const Shom &h);
  Shom(const GSDD& d);  
  Shom(int var,const DataSet& val, const GShom &h=GShom::id); 
  ~Shom();
 
  // Elementary emptyset homomorphism
  static const Shom null;
 
 
 
  Shom &operator=(const GShom &);
  Shom &operator=(const Shom &);
};
 
 
 
/******************************************************************************/
 
 
 
namespace std {
  template<>  struct less<GShom> {
    bool operator()(const GShom &g1,const GShom &g2) const{
      return g1<g2;
    }
  };
}
 
/**********************************************************************/
class _GShom 
{
private:
  friend class GShom;
  friend class Shom;
  mutable int _refCounter;
 
 
    GSDD eval_skip(const GSDD &) const;
 
 
  virtual bool immediat () const {return false;}
        
public:
  // made public ONLY for the cache, not part of normal API, use GShom has_image instead (cache etc...).
    GSDD has_image_skip(const GSDD &) const;
 
    virtual bool
    skip_variable(int) const
    {
        return false;
    }
 
    virtual bool
    is_selector() const
    {
        return false;
    }
 
      virtual const GShom::range_t get_range () const 
    {
      return GShom::full_range;
    }
 
  _GShom(int ref=0):_refCounter(2*ref){};
  virtual ~_GShom(){};
 
  virtual bool operator==(const _GShom &h) const=0;
  virtual size_t hash() const=0;
 
  // for use by unique table : return new MyConcreteClassName(*this);
  virtual _GShom * clone () const =0 ;
 
  virtual GSDD has_image (const GSDD & d) const ;
 
  virtual GShom compose(const GShom &) const;
  
  virtual GSDD eval(const GSDD &) const=0;
 
  virtual void mark() const{};
 
  void mark_if_refd () const {
        if ( refCounter() ) {           
                set_mark(true);         
        }  
  }
  
  void ref () const {
        _refCounter += 2;
  }
  
  void deref () const {
        _refCounter -= 2;
  }
  
  unsigned long int refCounter() const {
        return _refCounter >> 1;
  }
  
  bool is_marked() const {
        return _refCounter & 1;
  }
  
  void set_mark (bool val) const {
        if (val) {
                if (! is_marked() ) {
                        _refCounter |= 1;
                        mark();
                }
        } else {
                _refCounter >>= 1;
                _refCounter <<= 1;              
        }
  }
  
  
  virtual void print (std::ostream & os) const = 0;
public:
    
    // Enable access to the concrete GSHom for _GSHom homorphisms
    static
        const _GShom*
    get_concret(const GShom& gshom)
    {
        return gshom.concret;
    }
 
    // produce the predescessor homomorphism, using pot to compute variable domains
    virtual GShom invert (const GSDD & ) const { 
      // default = raise assert
      if ( is_selector() ) {
        // A default implmentation is provided for selector homomorphisms, overloadable.
        // sel^-1 (s) = pot - sel(pot) + s = ((pot-sel(pot)) + id)
        // return  ( (pot - GShom(this)(pot))+ GShom::id ); 
        // NEW VERSION : the invert of a selection is itself...
        return this;
      }
      // No default implem if ! is_selector 
      std::cerr << "Cannot invert homomorphism : " ;
      print (std::cerr);
      std::cerr << std::endl ;
      assert(0); 
      return Shom::null;
    }
 
};
 
class StrongShom : public _GShom 
{
public:
  StrongShom(): _GShom(0) {};
  virtual ~StrongShom(){};
  virtual GSDD phiOne() const{return GSDD::top;}; 
  virtual GShom phi(int var,const DataSet& val) const=0;
  virtual bool operator==(const StrongShom &h) const=0;
  bool operator==(const _GShom &h) const;
 
  virtual void print (std::ostream & os) const ;
 
  GSDD eval(const GSDD &)const;  
 
  virtual GSDD has_image (const GSDD & d) const ;
 
};
 
class MyGShom : public _GShom{};
 
#endif /* SHOM_H_ */