DDD
1.9.0.20240826145154
|
Extractor of variable domains for invert computations. More...
Public Member Functions | |
SDomExtract () | |
SDomExtract (int t) | |
bool | skip_variable (int) const |
The skip_variable predicate indicates which variables are "don't care" with respect to this SHom. More... | |
bool | is_selector () const |
The isSelector predicate indicates a homomorphism that only selects paths in the SDD (no modifications, no additions) Tagging with isSelector() allows to enable optimizations and makes the homomorphism eligible as "condition" in ITE construct. More... | |
GSDD | eval (const GSDD &d) const |
The computation function responsible for evaluation over a node. More... | |
size_t | hash () const |
Hash key computation. More... | |
bool | operator== (const _GShom &s) const |
Comparator. More... | |
_GShom * | clone () const |
void | print (std::ostream &os) const |
GSDD | has_image_skip (const GSDD &) const |
virtual const GShom::range_t | get_range () const |
The range returns the dual of skip_variable, default implem considers that all variables are affected by this homomorphism. More... | |
virtual GSDD | has_image (const GSDD &d) const |
virtual GShom | compose (const GShom &) const |
virtual void | mark () const |
For garbage collection. Used in first phase of garbage collection. More... | |
void | mark_if_refd () const |
void | ref () const |
void | deref () const |
unsigned long int | refCounter () const |
bool | is_marked () const |
void | set_mark (bool val) const |
virtual GShom | invert (const GSDD &) const |
Static Public Member Functions | |
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... More... | |
Public Attributes | |
int | target |
Private Member Functions | |
GSDD | eval_skip (const GSDD &) const |
The procedure responsible for propagating efficiently across "skipped" variable nodes. More... | |
virtual bool | immediat () const |
For operation cache management. More... | |
Private Attributes | |
int | _refCounter |
For garbage collection. More... | |
Extractor of variable domains for invert computations.
|
inline |
Referenced by clone().
|
inline |
|
inlinevirtual |
Implements _GShom.
References SDomExtract().
References GShom::id, and GSDD::null.
Referenced by GShom::compose().
|
inlineinherited |
References _GShom::_refCounter.
Referenced by Shom::operator=(), and Shom::~Shom().
The computation function responsible for evaluation over a node.
Users should not directly use this. Normal behavior is to use GShom::operator() that encapsulates this call with operation caching.
Implements _GShom.
References SDED::add(), GSDD::begin(), GSDD::end(), _GShom::GShom, GSDD::null, GSDD::one, target, GSDD::top, and GSDD::variable().
The procedure responsible for propagating efficiently across "skipped" variable nodes.
References GSDD::begin(), GSDD::end(), _GShom::eval(), GShom::id, _GShom::immediat(), GSDD::nbsons(), GSDD::null, GSDD::one, _GShom::skip_variable(), square_union(), GSDD::top, and GSDD::variable().
Referenced by GShom::eval().
TODO : this is a dirty trick to allow us to do terms rewriting in Add, Fixpoint etc...
A more elegant architecture would be nice.
References GShom::concret.
Referenced by addCompositionParameter(), addParameter(), buildUnionParameters(), sns::RecFireSat::eval(), sns::Fixpoint::eval(), sns::Add::factorizeByLevel(), GShom::GShom(), sns::Fixpoint::has_image(), operator!(), operator*(), sns::recFireSat(), sns::Inter::skip_variable(), sns::Add::skip_variable(), and sns::RightConcat::skip_variable().
|
inlinevirtualinherited |
The range returns the dual of skip_variable, default implem considers that all variables are affected by this homomorphism.
Reimplemented in sns::Fixpoint, sns::Compose, sns::RecFireSat, sns::Add, sns::And, sns::SNotCond, sns::SLocalApply, and sns::LocalApply.
References GShom::full_range.
Referenced by GShom::get_range().
Reimplemented in StrongShom, sns::Fixpoint, sns::RightConcat, sns::LeftConcat, sns::Compose, sns::Add, sns::And, sns::SNotCond, sns::SLocalApply, sns::LocalApply, sns::Inter, and sns::Identity.
References _GShom::GShom.
Referenced by sns::Inter::has_image(), sns::SNotCond::has_image(), sns::Compose::has_image(), sns::Fixpoint::has_image(), and _GShom::has_image_skip().
|
inlinevirtual |
Hash key computation.
It is essential for good hash table operation that the spread of the keys be as good as possible. Also, fast hash key computation is a good design goal. Note that bad hash functions will yield more collisions, thus equality comparisons which may be quite costly.
Implements _GShom.
References target.
|
inlineprivatevirtualinherited |
For operation cache management.
If immediat==true, eval is called without attempting a cache hit. Currently only the constant homomorphism has this attribute set to true. Overload and return true for immediate computations.
Reimplemented in sns::Constant, and sns::Identity.
Referenced by _GShom::eval_skip(), and GShom::operator()().
Reimplemented in sns::Fixpoint, sns::HomMinus, sns::Minus, sns::Compose, sns::RecFireSat, sns::Add, sns::And, sns::SLocalApply, sns::LocalApply, sns::Inter, sns::Mult, sns::SApply2k, sns::Constant, and sns::Identity.
References _GShom::is_selector(), Shom::null, and _GShom::print().
Referenced by GShom::invert().
|
inlineinherited |
References _GShom::_refCounter.
Referenced by _GShom::set_mark().
|
inlinevirtual |
|
inlinevirtualinherited |
For garbage collection. Used in first phase of garbage collection.
Reimplemented in sns::MLShomAdapter, sns::Fixpoint, sns::HomMinus, sns::Minus, sns::RightConcat, sns::LeftConcat, sns::Compose, sns::RecFireSat, sns::Add, sns::And, sns::SNotCond, sns::SLocalApply, sns::LocalApply, sns::Inter, sns::Mult, sns::SApply2k, and sns::Constant.
Referenced by _GShom::set_mark().
|
inlineinherited |
References _GShom::refCounter(), and _GShom::set_mark().
|
inlinevirtual |
|
inlinevirtual |
|
inlineinherited |
References _GShom::_refCounter.
Referenced by Shom::operator=(), and Shom::Shom().
|
inlineinherited |
References _GShom::_refCounter.
Referenced by _GShom::mark_if_refd(), Shom::operator=(), GShom::refCounter(), and Shom::~Shom().
|
inlineinherited |
References _GShom::_refCounter, _GShom::is_marked(), and _GShom::mark().
Referenced by GShom::garbage(), GShom::mark(), and _GShom::mark_if_refd().
|
inlinevirtual |
The skip_variable predicate indicates which variables are "don't care" with respect to this SHom.
This is defined as a StrongHom with : phi(var,val) { if ( skip_variable(var) ) return GShom( var, val, this ); else { real behavior } }
Reimplemented from _GShom.
|
mutableprivateinherited |
For garbage collection.
Counts the number of times a _GShom is referenced from the context of an Shom. For garbage collection: lowest bit of refCounter gives marking value for mark&sweep. Used in the two phase garbage collection process. A Shom that is not marked after the first pass over the unicity table, will be sweeped in the second phase. Outside of garbage collection routine, marking should always bear the value false.
Referenced by _GShom::deref(), _GShom::is_marked(), _GShom::ref(), _GShom::refCounter(), and _GShom::set_mark().
int sns::SDomExtract::target |
Referenced by eval(), hash(), operator==(), and print().