DDD  1.9.0.20240826145154
SHom.h
Go to the documentation of this file.
1 /****************************************************************************/
2 /* */
3 /* This file is part of libDDD, a library for manipulation of DDD and SDD. */
4 /* */
5 /* Copyright (C) 2001-2008 Yann Thierry-Mieg, Jean-Michel Couvreur */
6 /* and Denis Poitrenaud */
7 /* */
8 /* This program is free software; you can redistribute it and/or modify */
9 /* it under the terms of the GNU Lesser General Public License as */
10 /* published by the Free Software Foundation; either version 3 of the */
11 /* License, or (at your option) any later version. */
12 /* This program is distributed in the hope that it will be useful, */
13 /* but WITHOUT ANY WARRANTY; without even the implied warranty of */
14 /* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the */
15 /* GNU LEsserGeneral Public License for more details. */
16 /* */
17 /* You should have received a copy of the GNU Lesser General Public License */
18 /* along with this program; if not, write to the Free Software */
19 /*Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA */
20 /* */
21 /****************************************************************************/
22 
23 /* -*- C++ -*- */
24 #ifndef SHOM_H_
25 #define SHOM_H_
26 
27 #include "ddd/SDD.h"
28 #include "ddd/Hom.h"
29 #include "ddd/Cache.hh"
30 
31 #include "ddd/util/set.hh"
32 
33 /**********************************************************************/
34 
36 class _GShom;
38 class StrongShom;
39 class MyGShom;
40 class MLShom;
41 
42 
43 
56 class GShom
57 {
58 private:
60  friend class Shom;
62  friend class _GShom;
63 
66 
67  friend GShom fixpoint(const GShom &, bool is_top_level);
68  friend GShom localApply(const GHom &,int target);
69  friend GShom localApply(const GShom &,int target);
70  friend GShom add(const d3::set<GShom>::type &);
71  friend GShom operator+(const GShom &,const GShom &);
72  friend GShom operator&(const GShom &,const GShom &);
73  friend GShom operator*(const GSDD &,const GShom &);
74  friend GShom operator*(const GShom &,const GSDD &);
75  friend GShom operator^(const GSDD &,const GShom &);
76  friend GShom operator^(const GShom &,const GSDD &);
77  friend GShom operator-(const GShom &,const GSDD &);
79 
80 #ifdef HASH_STAT
81  // open access to instrumented hashtable
82  template <class Value, class Key, class HashFcn,
83  class ExtractKey, class SetKey, class EqualKey, class Alloc>
84  friend class google::sparse_hashtable;
85 #endif
86 
88  const _GShom* concret;
89 public:
90  typedef GSDD NodeType;
92 
93  GShom():concret(id.concret){};
95 
99  GShom(const _GShom *_h);
100 
109  GShom(_GShom *_h);
110 
113  GShom(const _GShom &_h);
114 
116  GShom(const MLShom &);
117 
120  GShom(const GSDD& d);
128  GShom(int var,const DataSet& val, const GShom &h=GShom::id); // var -- val -> Id
130 
132  static const GShom id;
133 
135  GShom invert (const GSDD & pot) const;
136 
138  GSDD has_image (const GSDD & d) const;
139 
140  GShom compose(const GShom &) const;
141 
145 
146  bool operator==(const GShom &h) const{return concret==h.concret;};
147  bool operator!=(const GShom &h) const{return concret!=h.concret;};
148  bool operator<(const GShom &h) const{return concret<h.concret;};
150  bool is_selector() const;
152  bool skip_variable(int) const;
153 
155  typedef range_t::const_iterator range_it;
157  const range_t get_range () const;
159  static const range_t full_range;
161 
163 
164  GSDD operator()(const GSDD &d) const;
170  GSDD eval(const GSDD &d) const;
172 
174  int refCounter() const;
175 
179  static GShom add(const d3::set<GShom>::type & s);
180 
181  // pretty print of homomorphisms
182  friend std::ostream & operator << (std::ostream & os, const GShom & h);
183 
185 
186  static unsigned int statistics();
189  static size_t cache_size();
191  static size_t cache_peak();
192 
195  static void pstats(bool reinit=true);
197  void mark() const;
199  size_t hash () const {
200  return ddd::knuth32_hash(reinterpret_cast<size_t>(concret));
201  }
205  static void garbage();
207 
208  // strategies for fixpoint evaluation insaturation context
209  // BFS = do each g_i once then go to g_i+1
210  // DFS = do each g_i to saturation then go to g_i+1
213 
214  private :
217 
218  public :
221 
224 
225 
226 };
227 
228 
229 
231 
232 GShom fixpoint(const GShom &, bool is_top_level=false);
244  GShom localApply(const GHom &,int target);
245  GShom localApply(const GShom &,int target);
246 
250  GShom extractPotential (int var);
251 
257 GShom ITE (const GShom & cond, const GShom & iftrue, const GShom & iffalse);
258 
262 GShom operator! (const GShom & cond);
263 
269 GShom operator+(const GShom &,const GShom &);
273 GShom operator&(const GShom &,const GShom &);
276 GShom operator*(const GSDD &,const GShom &);
279 GShom operator*(const GShom &,const GSDD &);
283 GShom operator*(const GShom &,const GShom &);
289 GShom operator^(const GSDD &,const GShom &);
295 GShom operator^(const GShom &,const GSDD &);
303 GShom operator-(const GShom &,const GSDD &);
311 GShom operator-(const GShom &,const GShom &);
312 
314 GShom apply2k (const GSDD &);
315 
316 
318 
319 
323 class Shom : public GShom
324 {
325 public:
328 
329  Shom(const GShom &h=GShom::id);
332  Shom(const Shom &h);
334  Shom(const GSDD& d);
342  Shom(int var,const DataSet& val, const GShom &h=GShom::id);
345  ~Shom();
347 
348  // Elementary emptyset homomorphism
349  static const Shom null;
350 
352 
353  Shom &operator=(const GShom &);
356  Shom &operator=(const Shom &);
358 };
359 
360 
361 
362 /******************************************************************************/
363 
364 
365 
366 namespace std {
369  template<> struct less<GShom> {
370  bool operator()(const GShom &g1,const GShom &g2) const{
371  return g1<g2;
372  }
373  };
374 }
375 
376 /**********************************************************************/
380 class _GShom
381 {
382 private:
384  friend class GShom;
386  friend class Shom;
394  mutable int _refCounter;
395 
396 
398  GSDD eval_skip(const GSDD &) const;
399 
400 
405  virtual bool immediat () const {return false;}
406 
407 public:
408  // made public ONLY for the cache, not part of normal API, use GShom has_image instead (cache etc...).
409  GSDD has_image_skip(const GSDD &) const;
410 
414  virtual bool
415  skip_variable(int) const
416  {
417  return false;
418  }
419 
422  virtual bool
423  is_selector() const
424  {
425  return false;
426  }
427 
429  virtual const GShom::range_t get_range () const
430  {
431  return GShom::full_range;
432  }
433 
436  _GShom(int ref=0):_refCounter(2*ref){};
439  virtual ~_GShom(){};
440 
444  virtual bool operator==(const _GShom &h) const=0;
449  virtual size_t hash() const=0;
450 
451  // for use by unique table : return new MyConcreteClassName(*this);
452  virtual _GShom * clone () const =0 ;
453 
454  virtual GSDD has_image (const GSDD & d) const ;
455 
456  virtual GShom compose(const GShom &) const;
457 
461  virtual GSDD eval(const GSDD &) const=0;
462 
464  virtual void mark() const{};
465 
466  void mark_if_refd () const {
467  if ( refCounter() ) {
468  set_mark(true);
469  }
470  }
471 
472  void ref () const {
473  _refCounter += 2;
474  }
475 
476  void deref () const {
477  _refCounter -= 2;
478  }
479 
480  unsigned long int refCounter() const {
481  return _refCounter >> 1;
482  }
483 
484  bool is_marked() const {
485  return _refCounter & 1;
486  }
487 
488  void set_mark (bool val) const {
489  if (val) {
490  if (! is_marked() ) {
491  _refCounter |= 1;
492  mark();
493  }
494  } else {
495  _refCounter >>= 1;
496  _refCounter <<= 1;
497  }
498  }
499 
500 
501  virtual void print (std::ostream & os) const = 0;
502 public:
503 
504  // Enable access to the concrete GSHom for _GSHom homorphisms
507  static
508  const _GShom*
509  get_concret(const GShom& gshom)
510  {
511  return gshom.concret;
512  }
513 
514  // produce the predescessor homomorphism, using pot to compute variable domains
515  virtual GShom invert (const GSDD & ) const {
516  // default = raise assert
517  if ( is_selector() ) {
518  // A default implmentation is provided for selector homomorphisms, overloadable.
519  // sel^-1 (s) = pot - sel(pot) + s = ((pot-sel(pot)) + id)
520  // return ( (pot - GShom(this)(pot))+ GShom::id );
521  // NEW VERSION : the invert of a selection is itself...
522  return this;
523  }
524  // No default implem if ! is_selector
525  std::cerr << "Cannot invert homomorphism : " ;
526  print (std::cerr);
527  std::cerr << std::endl ;
528  assert(0);
529  return Shom::null;
530  }
531 
532 };
533 
542 class StrongShom : public _GShom
543 {
544 public:
547  StrongShom(): _GShom(0) {};
550  virtual ~StrongShom(){};
554  virtual GSDD phiOne() const{return GSDD::top;};
559  virtual GShom phi(int var,const DataSet& val) const=0;
561  virtual bool operator==(const StrongShom &h) const=0;
565  bool operator==(const _GShom &h) const;
566 
568  virtual void print (std::ostream & os) const ;
569 
576  GSDD eval(const GSDD &)const;
577 
578  virtual GSDD has_image (const GSDD & d) const ;
579 
580 };
581 
582 class MyGShom : public _GShom{};
583 
584 #endif /* SHOM_H_ */
GShom extractPotential(int var)
Extract the domain of a given variable.
Definition: SHom.cpp:3304
GShom apply2k(const GSDD &)
Apply a 2 level DDD representing a transition relation to current variable.
Definition: SHom.cpp:3292
GShom operator^(const GSDD &, const GShom &)
Left Concatenation of a constant SDD.
Definition: SHom.cpp:3225
GShom operator&(const GShom &, const GShom &)
Composition by circ (rond) of homomorphisms.
Definition: SHom.cpp:3170
GShom operator-(const GShom &, const GSDD &)
Set difference.
Definition: SHom.cpp:3233
GShom localApply(const GHom &, int target)
Apply a homomorphism on a target variable.
Definition: SHom.cpp:2945
GShom fixpoint(const GShom &, bool is_top_level=false)
Apply a homomorphism until fixpoint is reached.
Definition: SHom.cpp:2828
GShom ITE(const GShom &cond, const GShom &iftrue, const GShom &iffalse)
An IF-THEN-ELSE construct.
Definition: SHom.cpp:3256
GShom operator+(const GShom &, const GShom &)
Composition by union of two homomorphisms.
Definition: SHom.cpp:3203
GShom operator!(const GShom &cond)
A negation/complement constructor for selector homomophisms.
Definition: SHom.cpp:3267
GShom operator*(const GSDD &, const GShom &)
Intersection with a constant SDD.
Definition: SHom.cpp:3217
This class is an abstraction of a set of data.
Definition: DataSet.h:44
This class is the base class representing a homomorphism over DDD.
Definition: Hom.h:55
This class is the base class representing a hierarchical Set Decision Diagram.
Definition: SDD.h:49
static const GSDD top
The approximation terminal.
Definition: SDD.h:140
This class is the base class for Homomorphisms over SDD.
Definition: SHom.h:57
GShom(_GShom *_h)
THIS VERSION IS DELIBERATELY UNIMPLEMENTED OTHERWISE bad calls like GShom(new myHom()) would promote ...
bool operator!=(const GShom &h) const
Definition: SHom.h:147
bool operator<(const GShom &h) const
Definition: SHom.h:148
friend GShom fixpoint(const GShom &, bool is_top_level)
Apply a homomorphism until fixpoint is reached.
Definition: SHom.cpp:2828
static fixpointStrategy fixpointStrategy_
Definition: SHom.h:215
const _GShom * concret
Pointer to the data instance in the unicity table.
Definition: SHom.h:88
bool operator==(const GShom &h) const
Definition: SHom.h:146
bool is_selector() const
This predicate is true if the homomorphism global behavior is only to prune some paths.
Definition: SHom.cpp:2790
friend class Shom
Open access to concret for Shom class.
Definition: SHom.h:60
GSDD NodeType
Definition: SHom.h:90
GShom compose(const GShom &) const
Definition: SHom.cpp:2681
saturationStrategy
Definition: SHom.h:212
@ RECFIREANDSAT
Definition: SHom.h:212
@ ORDINARY
Definition: SHom.h:212
friend GShom operator^(const GSDD &, const GShom &)
Left Concatenation of a constant SDD.
Definition: SHom.cpp:3225
friend GShom operator&(const GShom &, const GShom &)
Composition by circ (rond) of homomorphisms.
Definition: SHom.cpp:3170
friend GShom operator-(const GShom &, const GSDD &)
Set difference.
Definition: SHom.cpp:3233
GShom()
Default constructor builds identity homomorphism.
Definition: SHom.h:94
friend GShom localApply(const GHom &, int target)
Apply a homomorphism on a target variable.
Definition: SHom.cpp:2945
static void setFixpointStrategy(fixpointStrategy strat)
Definition: SHom.h:220
static GShom add(const d3::set< GShom >::type &s)
Compute an n-ary sum between homomorphisms.
static size_t cache_size()
Return the current size of the cache for GShom.
Definition: SHom.cpp:2700
fixpointStrategy
Definition: SHom.h:211
@ BFS
Definition: SHom.h:211
@ DFS
Definition: SHom.h:211
static void setSaturationStrategy(saturationStrategy strat)
Definition: SHom.h:223
const range_t get_range() const
Returns the range for this homomorphism, i.e. the dual of skip_variable.
Definition: SHom.cpp:2801
static unsigned int statistics()
Return the current size of the unicity table for GShom.
Definition: SHom.cpp:2696
GSDD has_image(const GSDD &d) const
returns true if and only if h(d) != SDD::null
Definition: SHom.cpp:2664
static void garbage()
Collects and destroys unused homomorphisms.
Definition: SHom.cpp:2716
d3::set< int >::type range_t
Definition: SHom.h:154
int refCounter() const
For debug and development purposes. Gives the reference count of the concrete data.
Definition: SHom.cpp:2685
static saturationStrategy saturationStrategy_
Definition: SHom.h:216
static fixpointStrategy getFixpointStrategy()
Definition: SHom.h:219
bool skip_variable(int) const
This predicate is true if the homomorphism "skips" this variable.
Definition: SHom.cpp:2794
range_t::const_iterator range_it
Definition: SHom.h:155
static void pstats(bool reinit=true)
Print some usage statistics on Shom.
Definition: SHom.cpp:3336
static const GShom id
Elementary SDD homomorphism identity. Applied to any SDD d, it returns d.
Definition: SHom.h:132
GSDD operator()(const GSDD &d) const
Applying a homomorphism to a node returns a node.
Definition: SHom.cpp:2651
static saturationStrategy getSaturationStrategy()
Definition: SHom.h:222
void mark() const
Mark a concrete data as in use (forbids garbage collection of the data).
Definition: SHom.cpp:2709
friend std::ostream & operator<<(std::ostream &os, const GShom &h)
Definition: SHom.cpp:3365
static const range_t full_range
The full_range : that targets everyone.
Definition: SHom.h:159
friend GShom operator+(const GShom &, const GShom &)
Composition by union of two homomorphisms.
Definition: SHom.cpp:3203
friend GShom add(const d3::set< GShom >::type &)
Definition: SHom.cpp:3039
static size_t cache_peak()
Return the peak size of the cache for GShom.
Definition: SHom.cpp:2704
GShom invert(const GSDD &pot) const
returns the predescessor homomorphism, using pot to determine variable domains
Definition: SHom.cpp:2677
size_t hash() const
For storage in a hash table.
Definition: SHom.h:199
GSDD eval(const GSDD &d) const
The full evaluation, this is the computational procedure, that is called when the computation cache y...
Definition: SHom.cpp:2672
friend GShom operator*(const GSDD &, const GShom &)
Intersection with a constant SDD.
Definition: SHom.cpp:3217
Definition: MLSHom.h:14
Definition: SHom.h:582
This is the user interface class to manipulate homomorphisms.
Definition: SHom.h:324
static const Shom null
Definition: SHom.h:349
Shom & operator=(const GShom &)
Overloaded behavior for assignment operator, maintains reference counting.
Definition: SHom.cpp:2781
~Shom()
Destructor maintains reference counting.
Definition: SHom.cpp:2766
The abstract base class for user defined operations.
Definition: SHom.h:543
virtual GSDD has_image(const GSDD &d) const
Definition: SHom.cpp:2548
StrongShom()
Default constructor.
Definition: SHom.h:547
virtual GShom phi(int var, const DataSet &val) const =0
Evaluation over an arbitrary arc of a SDD.
virtual void print(std::ostream &os) const
pretty print
Definition: SHom.cpp:2585
virtual ~StrongShom()
Default destructor.
Definition: SHom.h:550
virtual GSDD phiOne() const
Evaluation over terminal GSDD::one.
Definition: SHom.h:554
GSDD eval(const GSDD &) const
The evaluation mechanism of strong homomorphisms.
Definition: SHom.cpp:2567
virtual bool operator==(const StrongShom &h) const =0
Comparator is pure virtual. Define a behavior in user homomorphisms.
The concrete data class for Homomorphisms.
Definition: SHom.h:381
virtual size_t hash() const =0
Hash key computation.
void set_mark(bool val) const
Definition: SHom.h:488
virtual void mark() const
For garbage collection. Used in first phase of garbage collection.
Definition: SHom.h:464
virtual bool is_selector() const
The isSelector predicate indicates a homomorphism that only selects paths in the SDD (no modification...
Definition: SHom.h:423
void ref() const
Definition: SHom.h:472
virtual GShom compose(const GShom &) const
Definition: SHom.cpp:2521
_GShom(int ref=0)
Constructor.
Definition: SHom.h:436
virtual GSDD eval(const GSDD &) const =0
The computation function responsible for evaluation over a node.
virtual GShom invert(const GSDD &) const
Definition: SHom.h:515
virtual bool immediat() const
For operation cache management.
Definition: SHom.h:405
bool is_marked() const
Definition: SHom.h:484
virtual bool skip_variable(int) const
The skip_variable predicate indicates which variables are "don't care" with respect to this SHom.
Definition: SHom.h:415
virtual bool operator==(const _GShom &h) const =0
Comparator.
virtual void print(std::ostream &os) const =0
virtual _GShom * clone() const =0
static const _GShom * get_concret(const GShom &gshom)
TODO : this is a dirty trick to allow us to do terms rewriting in Add, Fixpoint etc....
Definition: SHom.h:509
virtual const GShom::range_t get_range() const
The range returns the dual of skip_variable, default implem considers that all variables are affected...
Definition: SHom.h:429
GSDD has_image_skip(const GSDD &) const
Definition: SHom.cpp:2356
unsigned long int refCounter() const
Definition: SHom.h:480
virtual GSDD has_image(const GSDD &d) const
Definition: SHom.cpp:2347
int _refCounter
For garbage collection.
Definition: SHom.h:394
void mark_if_refd() const
Definition: SHom.h:466
virtual ~_GShom()
Destructor.
Definition: SHom.h:439
void deref() const
Definition: SHom.h:476
GSDD eval_skip(const GSDD &) const
The procedure responsible for propagating efficiently across "skipped" variable nodes.
Definition: SHom.cpp:2381
size_t knuth32_hash(size_t key)
Knuth's Multiplicative hash function.
Definition: hashfunc.hh:73
Definition: DDD.h:340
std::set< Key, Compare, Allocator > type
Definition: set.hh:18
bool operator()(const GShom &g1, const GShom &g2) const
Definition: SHom.h:370

Please comment this page and report errors about it on the RefDocComments page.
Generated on Mon Aug 26 2024 14:54:00 for DDD by doxygen 1.9.1