82 template <
class Value,
class Key,
class HashFcn,
83 class ExtractKey,
class SetKey,
class EqualKey,
class Alloc>
84 friend class google::sparse_hashtable;
195 static void pstats(
bool reinit=
true);
501 virtual void print (std::ostream & os)
const = 0;
525 std::cerr <<
"Cannot invert homomorphism : " ;
527 std::cerr << std::endl ;
568 virtual void print (std::ostream & os)
const ;
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
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
std::set< Key, Compare, Allocator > type
Definition: set.hh:18
bool operator()(const GShom &g1, const GShom &g2) const
Definition: SHom.h:370