DDD
1.9.0.20240826145154
|
#include <typeinfo>
#include <iostream>
#include <cassert>
#include <map>
#include <algorithm>
#include "ddd/util/set.hh"
#include "ddd/Hom.h"
#include "ddd/DDD.h"
#include "ddd/DED.h"
#include "ddd/UniqueTable.h"
#include "ddd/MLHom.h"
#include "ddd/util/hash_support.hh"
#include "ddd/util/configuration.hh"
#include "ddd/Cache.hh"
#include "ddd/MemoryManager.h"
#include "ddd/FixObserver.hh"
Classes | |
struct | d3::util::equal< _GHom * > |
class | Identity |
class | Constant |
class | Apply2k |
class | DomExtract |
Extractor of variable domains for invert computations. More... | |
class | Mult |
class | Inter |
class | NotCond |
class | Add |
class | Monotonic |
class | Compose |
class | And |
A commutative composition of n homomorphisms. More... | |
class | LeftConcat |
class | RightConcat |
class | Minus |
class | Fixpoint |
class | MLHomAdapter |
Namespaces | |
d3 | |
d3::util | |
Typedefs | |
typedef Cache< GHom, GDDD, GDDD > | HomCache |
typedef Cache< GHom, GDDD, GDDD, char > | ImgHomCache |
Functions | |
bool | testWasInterrupt (bool can_garbage, const GDDD &d1, const GDDD &d2) |
bool | testShouldInterrupt (bool can_garbage, const GDDD &d1, const GDDD &d2) |
GDDD | computeDomain (int var, const GDDD &d) |
Return the domain of the first variable bearing the provided index in the provided DDD Useful for invert computations. More... | |
static bool | notInRange (const GHom::range_t &h1r, const GHom &h2) |
bool | commutative (const GHom &h1, const GHom &h2) |
return true if the provided operations are commutative More... | |
GHom | fixpoint (const GHom &h, bool is_top_level) |
Apply a homomorphism until fixpoint is reached. More... | |
GHom | monotonic (const d3::set< GHom >::type &set) |
static void | printCondError (const GHom &cond) |
GHom | ITE (const GHom &cond, const GHom &iftrue, const GHom &iffalse) |
An IF-THEN-ELSE construct. More... | |
GHom | operator! (const GHom &cond) |
A negation/complement constructor for selector homomophisms. More... | |
static void | addCompositionParameter (const GHom &h, And::parameters_t &args) |
GHom | operator& (const GHom &h1, const GHom &h2) |
Composition by circ (rond) of homomorphisms. More... | |
GHom | operator+ (const GHom &h1, const GHom &h2) |
Composition by union of two homomorphisms. More... | |
GHom | operator* (const GDDD &d, const GHom &h) |
Intersection with a constant DDD. More... | |
GHom | operator* (const GHom &h, const GDDD &d) |
Intersection with a constant SDD. More... | |
GHom | operator* (const GHom &h, const GHom &cond) |
Intersection with a selector Hom. More... | |
GHom | operator^ (const GDDD &d, const GHom &h) |
Left Concatenation of a constant SDD. More... | |
GHom | operator^ (const GHom &h, const GDDD &d) |
Right Concatenation of a constant SDD. More... | |
GHom | operator- (const GHom &h, const GDDD &d) |
Set difference. More... | |
GHom | apply2k (const GDDD &d) |
Apply a 2 level DDD representing a transition relation to current variable. More... | |
std::ostream & | operator<< (std::ostream &os, const GHom &h) |
Variables | |
static UniqueTable< _GHom > | canonical |
static HomCache | cache |
static ImgHomCache | imgcache |
typedef Cache<GHom,GDDD,GDDD,char> ImgHomCache |
|
static |
References commutative(), and _GHom::get_concret().
Apply a 2 level DDD representing a transition relation to current variable.
References GDDD::null, GDDD::one, and GDDD::top.
return true if the provided operations are commutative
References GHom::get_range(), GHom::is_selector(), and notInRange().
Referenced by addCompositionParameter().
Return the domain of the first variable bearing the provided index in the provided DDD Useful for invert computations.
Referenced by _setVarConst::invert(), and _incVar::invert().
Apply a homomorphism until fixpoint is reached.
Application consists in : while ( h(d) != d ) d = h(d); Where d is a DDD and h a homomorphism.
Referenced by Fixpoint::eval(), Fixpoint::has_image(), and Fixpoint::invert().
An IF-THEN-ELSE construct.
The behavior of the condition must be a selection, as indicated by its isSelector() flag. PITFALL : Otherwise an assertion violation will be raised (with an explicit stderr message)
Semantics : ITE ( cond, iftrue, iffalse) (d) = (iftrue & cond(d)) + (iffalse & !cond(d))
References GHom::is_selector(), and printCondError().
Similar to the fixpoint, but we suppose here that the parameters are commutative And that any application order converges to the same result Typically this is the property of a base of monotonic< permutations.
Referenced by Monotonic::skip_variable().
|
static |
References GHom::get_range().
Referenced by commutative().
A negation/complement constructor for selector homomophisms.
Let cond be a selector, !cond(d) = d - cond(d) PITFALL : Raises an assert violation if is_selector() returns false !
Composition by circ (rond) of homomorphisms.
(h & g) (d) = h( g(d) ) ; Where g,h are homomorphisms and d is a DDD.
Intersection with a selector Hom.
Semantics : (d1 * sel) (d) = d1 (d) * sel (d) WARNING : assert failure if 2nd argument is not a selector.
References GHom::is_selector(), and GDDD::null.
Composition by union of two homomorphisms.
By definition, as homomorphism are linear, (h+g) (d) = h(d) + g(d) ; Where g,h are homomorphisms and d is a DDD.
Set difference.
(h - d1) (d2) = h(d2) - d1 Where h is a homomorphism and d1, d2 are DDD.
std::ostream& operator<< | ( | std::ostream & | os, |
const GHom & | h | ||
) |
Referenced by Fixpoint::eval().
References fobs::get_fixobserver(), fobs::FixObserver::should_interrupt(), and fobs::FixObserver::update().
Referenced by Fixpoint::eval().
|
static |
Referenced by GHom::garbage(), GHom::operator()(), DED::pstats(), and GHom::pstats().
|
static |
Referenced by GHom::add(), GHom::ccompose(), GHom::garbage(), GShom::garbage(), GShom::GShom(), GHom::pstats(), GShom::pstats(), GHom::statistics(), and GShom::statistics().
|
static |
Referenced by GHom::garbage(), and GHom::has_image().