DDD 1.9.0.20250409152518
Hom.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 HOM_H_
25#define HOM_H_
26
27#include "ddd/DDD.h"
29#include "ddd/util/set.hh"
30
31#include <map>
32#include <cassert>
33#include <iostream>
34/**********************************************************************/
35
37class _GHom;
39class StrongHom;
41class MyGHom;
43class MLHom;
44
55class GHom {
56private:
58 friend class Hom;
60 friend class _GHom;
64 friend GHom fixpoint(const GHom &, bool);
69 friend GHom monotonic(const d3::set<GHom>::type & set);
73 friend GHom operator+(const GHom &,const GHom &);
77 friend GHom operator&(const GHom &,const GHom &);
81 friend GHom operator*(const GDDD &,const GHom &);
85 friend GHom operator*(const GHom &,const GDDD &);
89 friend GHom operator^(const GDDD &,const GHom &);
93 friend GHom operator^(const GHom &,const GDDD &);
97 friend GHom operator-(const GHom &,const GDDD &);
98
99#ifdef HASH_STAT
100 // open access to instrumented hashtable
101 template <class Value, class Key, class HashFcn,
102 class ExtractKey, class SetKey, class EqualKey, class Alloc>
103 friend class google::sparse_hashtable;
104#endif
105
109public:
110 typedef GDDD NodeType;
114 GHom(const _GHom *_h):concret(_h){};
115
125
128 GHom(const _GHom &_h);
130
131
134
136 GHom(const MLHom &);
137
142 GHom(const GDDD& d);
149 GHom(int var, int val, const GHom &h=GHom::id);
151
154 static const GHom id;
155
157
158
161 bool operator==(const GHom &h) const{return concret==h.concret;};
165 bool operator!=(const GHom &h) const{return concret!=h.concret;};
172 bool operator<(const GHom &h) const;
174 bool is_selector() const;
176
178 typedef range_t::const_iterator range_it;
180 const range_t get_range () const;
182 static const range_t full_range;
183
185 GHom invert (const GDDD & pot) const;
186
188 GDDD has_image (const GDDD & d) const;
189
191 GHom negate () const;
192
197 GDDD operator()(const GDDD &d) const;
202 GDDD eval(const GDDD &d) const;
203
204 bool skip_variable(int var) const ;
205
206 GHom compose (const GHom &r) const ;
207
210 int refCounter() const;
211
218 static GHom add(const d3::set<GHom>::type & set);
219
224 static GHom ccompose(const d3::set<GHom>::type & set);
225
226
227 // pretty print of homomorphisms
228 friend std::ostream & operator << (std::ostream & os, const GHom & h);
229
231
232
233 static unsigned int statistics();
236 static void pstats(bool reinit=true);
238 void mark()const;
240 size_t hash () const {
241 return ddd::knuth32_hash(reinterpret_cast<size_t>(concret));
242 }
250 static void garbage();
252};
253
254
255
256/* Operations */
258
259
268GHom fixpoint(const GHom &, bool is_top_level=false);
272GHom operator! (const GHom & cond);
278GHom ITE (const GHom & cond, const GHom & iftrue, const GHom & iffalse);
279
285GHom operator+(const GHom &,const GHom &);
289GHom operator&(const GHom &,const GHom &); // composition
292GHom operator*(const GDDD &,const GHom &);
295GHom operator*(const GHom &,const GDDD &);
299GHom operator*(const GHom &,const GHom &);
305GHom operator^(const GDDD &,const GHom &);
311GHom operator^(const GHom &,const GDDD &);
319GHom operator-(const GHom &,const GDDD &);
320
322GHom apply2k (const GDDD &);
323
326GDDD computeDomain (int var, const GDDD& );
327
329bool commutative (const GHom & h1, const GHom & h2);
330
331
333
334
335
339class Hom:public GHom /*, public DataSet*/ {
340 public:
341 /* Constructor */
344
345
346 Hom(const GHom &h=GHom::id);
348 Hom(const Hom &h);
350 Hom(const GDDD& d); // constant
358 Hom(int var, int val, const GHom &h=GHom::id); // var -- val -> Id
361 ~Hom();
363
365
366
367 Hom &operator=(const GHom &);
369 Hom &operator=(const Hom &);
371};
372
373/******************************************************************************/
374
375namespace std {
378 template<>
379 struct less<GHom> {
380 bool operator()(const GHom &g1,const GHom &g2) const{
381 return g1<g2;
382 }
383 };
384}
385
386/**********************************************************************/
390class _GHom{
391private:
393 friend class GHom;
395 friend class Hom;
398 mutable int refCounter;
403 mutable bool marking;
407 mutable bool immediat;
411
412 GDDD eval_skip(const GDDD &) const;
413public:
414 // made public ONLY for the cache, not part of normal API, use GHom has_image instead (cache etc...).
415 GDDD has_image_skip(const GDDD &) const;
416
417
421 virtual bool
422 skip_variable(int) const
423 {
424 return false;
425 }
428 virtual bool
430 {
431 return false;
432 }
433
435 virtual const GHom::range_t get_range () const
436 {
437 return GHom::full_range;
438 }
439
441 virtual GHom invert (const GDDD & ) const {
442 // default = raise assert
443 if ( is_selector() ) {
444 // A default implementation is provided for selector homomorphisms, overloadable.
445 return this;
446 }
447 // No default implem if ! is_selector
448 std::cerr << "Cannot invert homomorphism : " ;
449 print (std::cerr);
450 std::cerr << std::endl ;
451 assert(0);
452 return GHom(GDDD::null);
453 }
454
455
458 _GHom(int ref=0,bool im=false):refCounter(ref),marking(false),immediat(im){
459 // creation counter
460 static size_t counter = 0;
461 creation_counter = counter++;
462 }
464 virtual ~_GHom(){};
465
466
470 virtual bool operator==(const _GHom &h) const=0;
472 bool operator< (const _GHom &h) const;
477 virtual size_t hash() const=0;
478
479 // for use by unique table : return new MyConcreteClassName(*this);
480 virtual _GHom * clone () const =0 ;
481
485 virtual GDDD eval(const GDDD &)const=0;
486
488 virtual void mark() const{};
489
490 virtual GDDD has_image(const GDDD &) const;
492 virtual GHom negate () const;
493
494
495 virtual GHom compose (const GHom &r) const ;
496
497 virtual void print (std::ostream & os) const = 0;
498
499 // Enable access to the concrete GHom for _GHom homorphisms
500 static const _GHom*
501 get_concret(const GHom& ghom)
502 {
503 return ghom.concret;
504 }
505
506
507};
508
518 :
519 public _GHom
520{
521public:
527 virtual ~StrongHom(){};
531 virtual GDDD phiOne() const{return GDDD::top;};
536 virtual GHom phi(int var,int val) const=0;
538 virtual bool operator==(const StrongHom &h) const=0;
539
543 bool operator==(const _GHom &h) const;
544
546 virtual void print (std::ostream & os) const ;
547
548
555 GDDD eval(const GDDD &)const;
556
557 virtual GDDD has_image (const GDDD &) const;
558
559};
560
561
564class MyGHom:public _GHom{};
565
566#endif /* HOM_H_ */
GHom operator!(const GHom &cond)
A negation/complement constructor for selector homomophisms.
Definition Hom.cpp:2284
GHom ITE(const GHom &cond, const GHom &iftrue, const GHom &iffalse)
An IF-THEN-ELSE construct.
Definition Hom.cpp:2274
GHom fixpoint(const GHom &, bool is_top_level=false)
Apply a homomorphism until fixpoint is reached.
Definition Hom.cpp:2099
GHom operator^(const GDDD &, const GHom &)
Left Concatenation of a constant SDD.
Definition Hom.cpp:2425
GHom apply2k(const GDDD &)
Apply a 2 level DDD representing a transition relation to current variable.
Definition Hom.cpp:2437
GHom operator&(const GHom &, const GHom &)
Composition by circ (rond) of homomorphisms.
Definition Hom.cpp:2363
GHom operator-(const GHom &, const GDDD &)
Set difference.
Definition Hom.cpp:2433
GHom operator*(const GDDD &, const GHom &)
Intersection with a constant DDD.
Definition Hom.cpp:2402
bool commutative(const GHom &h1, const GHom &h2)
return true if the provided operations are commutative
Definition Hom.cpp:1894
GHom operator+(const GHom &, const GHom &)
Composition by union of two homomorphisms.
Definition Hom.cpp:2394
GDDD computeDomain(int var, const GDDD &)
Return the domain of the first variable bearing the provided index in the provided DDD Useful for inv...
Definition Hom.cpp:316
This class is the base class representing a Data Decision Diagram.
Definition DDD.h:49
static const GDDD top
The approximation terminal.
Definition DDD.h:146
static const GDDD null
The non-accepting terminal.
Definition DDD.h:143
This class is the base class representing a homomorphism over DDD.
Definition Hom.h:55
range_t::const_iterator range_it
Definition Hom.h:178
GHom(_GHom *_h)
THIS VERSION IS DELIBERATELY UNIMPLEMENTED OTHERWISE bad calls like GShom(new myHom()) would promote ...
GDDD eval(const GDDD &d) const
Evaluation function : users should use operator() instead of this.
Definition Hom.cpp:1971
GHom negate() const
returns a negation of a selector homomorphism h, such that h.negate() (d) = d - h(d)
Definition Hom.cpp:1914
static const range_t full_range
The full_range : that targets everyone.
Definition Hom.h:182
bool skip_variable(int var) const
Definition Hom.cpp:1864
friend std::ostream & operator<<(std::ostream &os, const GHom &h)
Definition Hom.cpp:2483
static GHom add(const d3::set< GHom >::type &set)
A constructor for a union of several homomorphisms.
Definition Hom.cpp:1981
static void pstats(bool reinit=true)
Prints some statistics to std::cout.
Definition Hom.cpp:2452
bool operator<(const GHom &h) const
Total ordering function between Hom.
Definition Hom.cpp:1860
static void garbage()
For garbage collection.
Definition Hom.cpp:2023
GHom compose(const GHom &r) const
Definition Hom.cpp:1906
GDDD operator()(const GDDD &d) const
Evaluation operator.
Definition Hom.cpp:1941
static unsigned int statistics()
Returns unicity table current size. Gives the number of different _GHom created and not yet destroyed...
Definition Hom.cpp:2011
friend GHom operator^(const GDDD &, const GHom &)
This is the left concatenantion operator, that adds a constant DDD above the operation.
Definition Hom.cpp:2425
GHom invert(const GDDD &pot) const
returns the predescessor homomorphism, using pot to determine variable domains
Definition Hom.cpp:1910
void mark() const
For garbage collection internals. Marks a GHom as in use in garbage collection phase.
Definition Hom.cpp:2016
GDDD NodeType
Definition Hom.h:110
GHom()
Default public constructor.
Definition Hom.h:133
size_t hash() const
For storage in a hash table.
Definition Hom.h:240
friend GHom operator&(const GHom &, const GHom &)
This operator creates an operation that is the composition of two operations.
Definition Hom.cpp:2363
friend GHom operator-(const GHom &, const GDDD &)
This is a set difference constructor, only available for (hom - ddd), not hom - hom as that might not...
Definition Hom.cpp:2433
bool operator!=(const GHom &h) const
Comparison between Homomorphisms.
Definition Hom.h:165
GDDD has_image(const GDDD &d) const
returns true if and only if h(d) != SDD::null
Definition Hom.cpp:1960
GHom(const _GHom *_h)
A uncontrolled constructor used in internals.
Definition Hom.h:114
friend GHom operator*(const GDDD &, const GHom &)
This operator creates an operation that is the intersection of an operation and a constant DDD.
Definition Hom.cpp:2402
friend GHom fixpoint(const GHom &, bool)
This operator applies its argument to a node until a fixpoint is reached.
Definition Hom.cpp:2099
bool operator==(const GHom &h) const
Comparison between Homomorphisms.
Definition Hom.h:161
friend GHom operator+(const GHom &, const GHom &)
This operator creates an operation that is the union of two operations.
Definition Hom.cpp:2394
friend GHom monotonic(const d3::set< GHom >::type &set)
This operator applies its arguments to a node until a fixpoint is reached.
Definition Hom.cpp:2260
friend class Hom
Open access to Hom derived class.
Definition Hom.h:58
bool is_selector() const
This predicate is true if the homomorphism global behavior is only to prune some paths.
Definition Hom.cpp:2093
const _GHom * concret
The real implementation class.
Definition Hom.h:108
static GHom ccompose(const d3::set< GHom >::type &set)
A constructor for a commutative composition of several homomorphisms.
Definition Hom.cpp:1995
static const GHom id
Elementary homomorphism Identity, defined as a constant.
Definition Hom.h:154
const range_t get_range() const
Returns the range for this homomorphism, i.e. the dual of skip_variable.
Definition Hom.cpp:1868
int refCounter() const
Accessor to visualize the reference count of the concret instance.
Definition Hom.cpp:1977
d3::set< int >::type range_t
Definition Hom.h:177
This is the user interface class to manipulate homomorphisms.
Definition Hom.h:339
~Hom()
Destructor maintains reference counting.
Definition Hom.cpp:2069
Hom & operator=(const GHom &)
Overloaded behavior for assignment operator, maintains reference counting.
Definition Hom.cpp:2084
Definition MLHom.h:39
Unknown function for this class.
Definition Hom.h:564
The abstract base class for user defined operations.
Definition Hom.h:520
virtual void print(std::ostream &os) const
pretty print
Definition Hom.cpp:1841
virtual ~StrongHom()
Default destructor.
Definition Hom.h:527
virtual GDDD phiOne() const
Evaluation over terminal GDDD::one.
Definition Hom.h:531
virtual bool operator==(const StrongHom &h) const =0
Comparator is pure virtual. Define a behavior in user homomorphisms.
GDDD eval(const GDDD &) const
The evaluation mechanism of strong homomorphisms.
Definition Hom.cpp:1811
virtual GHom phi(int var, int val) const =0
Evaluation over an arbitrary arc of a SDD.
StrongHom()
Default constructor.
Definition Hom.h:524
virtual GDDD has_image(const GDDD &) const
Definition Hom.cpp:1780
The concrete data class for Homomorphisms.
Definition Hom.h:390
virtual GHom invert(const GDDD &) const
returns the predescessor homomorphism, using pot to determine variable domains
Definition Hom.h:441
static const _GHom * get_concret(const GHom &ghom)
Definition Hom.h:501
GDDD eval_skip(const GDDD &) const
Definition Hom.cpp:1682
virtual bool operator==(const _GHom &h) const =0
Comparator.
size_t creation_counter
Counter of objects created (see constructors).
Definition Hom.h:410
virtual size_t hash() const =0
Hash key computation.
virtual GHom compose(const GHom &r) const
Definition Hom.cpp:1621
virtual GDDD has_image(const GDDD &) const
Definition Hom.cpp:1647
virtual const GHom::range_t get_range() const
The range returns the dual of skip_variable, default implem considers that all variables are affected...
Definition Hom.h:435
virtual GHom negate() const
returns a negation of a selector homomorphism h, such that h.negate() (d) = d - h(d)
Definition Hom.cpp:1640
bool operator<(const _GHom &h) const
Ordering between _GHom. It is the chronological ordering of creation.
Definition Hom.cpp:2448
int refCounter
For garbage collection.
Definition Hom.h:398
virtual void mark() const
For garbage collection. Used in first phase of garbage collection.
Definition Hom.h:488
GDDD has_image_skip(const GDDD &) const
Definition Hom.cpp:1652
virtual _GHom * clone() const =0
virtual void print(std::ostream &os) const =0
virtual bool is_selector() const
The isSelector predicate indicates a homomorphism that only selects paths in the SDD (no modification...
Definition Hom.h:429
virtual GDDD eval(const GDDD &) const =0
The computation function responsible for evaluation over a node.
_GHom(int ref=0, bool im=false)
Constructor.
Definition Hom.h:458
friend class GHom
open access to container class GHom.
Definition Hom.h:393
bool marking
For garbage collection.
Definition Hom.h:403
virtual ~_GHom()
Virtual Destructor. Default behavior.
Definition Hom.h:464
virtual bool skip_variable(int) const
The skip_variable predicate indicates which variables are "don't care" with respect to this SHom.
Definition Hom.h:422
bool immediat
For operation cache management.
Definition Hom.h:407
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 GHom &g1, const GHom &g2) const
Definition Hom.h:380

Please comment this page and report errors about it on the RefDocComments page.
Generated on Wed Apr 9 2025 15:27:42 for DDD by doxygen 1.9.8