DDD  1.9.0.20240826145154
Classes | Namespaces | Typedefs | Functions | Variables
Hom.cpp File Reference
#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"
Include dependency graph for Hom.cpp:

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, GDDDHomCache
 
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< _GHomcanonical
 
static HomCache cache
 
static ImgHomCache imgcache
 

Typedef Documentation

◆ HomCache

◆ ImgHomCache

typedef Cache<GHom,GDDD,GDDD,char> ImgHomCache

Function Documentation

◆ addCompositionParameter()

static void addCompositionParameter ( const GHom h,
And::parameters_t args 
)
static

◆ apply2k()

GHom apply2k ( const GDDD d)

Apply a 2 level DDD representing a transition relation to current variable.

References GDDD::null, GDDD::one, and GDDD::top.

◆ commutative()

bool commutative ( const GHom h1,
const GHom h2 
)

return true if the provided operations are commutative

References GHom::get_range(), GHom::is_selector(), and notInRange().

Referenced by addCompositionParameter().

◆ computeDomain()

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.

Referenced by _setVarConst::invert(), and _incVar::invert().

◆ fixpoint()

GHom fixpoint ( const GHom h,
bool  is_top_level 
)

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().

◆ ITE()

GHom ITE ( const GHom cond,
const GHom iftrue,
const GHom iffalse 
)

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().

◆ monotonic()

GHom monotonic ( const d3::set< GHom >::type &  set)

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().

◆ notInRange()

static bool notInRange ( const GHom::range_t h1r,
const GHom h2 
)
static

References GHom::get_range().

Referenced by commutative().

◆ operator!()

GHom operator! ( const GHom cond)

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 !

◆ operator&()

GHom operator& ( const GHom h1,
const GHom h2 
)

Composition by circ (rond) of homomorphisms.

(h & g) (d) = h( g(d) ) ; Where g,h are homomorphisms and d is a DDD.

◆ operator*() [1/3]

GHom operator* ( const GDDD d,
const GHom h 
)

Intersection with a constant DDD.

(d1 * h) (d2) = d1 * h(d2) ; Where h is a homomorphism and d1, d2 are DDD.

◆ operator*() [2/3]

GHom operator* ( const GHom h,
const GDDD d 
)

Intersection with a constant SDD.

(h * d1) (d2) = h(d2) * d1 ; Where h is a homomorphism and d1, d2 are DDD.

◆ operator*() [3/3]

GHom operator* ( const GHom h,
const GHom cond 
)

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.

◆ operator+()

GHom operator+ ( const GHom h1,
const GHom h2 
)

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.

◆ operator-()

GHom operator- ( const GHom h,
const GDDD d 
)

Set difference.

(h - d1) (d2) = h(d2) - d1 Where h is a homomorphism and d1, d2 are DDD.

◆ operator<<()

std::ostream& operator<< ( std::ostream &  os,
const GHom h 
)

◆ operator^() [1/2]

GHom operator^ ( const GDDD d,
const GHom h 
)

Left Concatenation of a constant SDD.

(d1 ^ h) (d2) = d1 ^ h(d2) Where h is a homomorphism and d1, d2 are DDD.

◆ operator^() [2/2]

GHom operator^ ( const GHom h,
const GDDD d 
)

Right Concatenation of a constant SDD.

(h ^ d1) (d2) = h(d1) ^ d2 Where h is a homomorphism and d1, d2 are DDD.

◆ printCondError()

static void printCondError ( const GHom cond)
static

Referenced by ITE().

◆ testShouldInterrupt()

bool testShouldInterrupt ( bool  can_garbage,
const GDDD d1,
const GDDD d2 
)

Referenced by Fixpoint::eval().

◆ testWasInterrupt()

bool testWasInterrupt ( bool  can_garbage,
const GDDD d1,
const GDDD d2 
)

Variable Documentation

◆ cache

HomCache cache
static

◆ canonical

UniqueTable<_GHom> canonical
static

◆ imgcache

ImgHomCache imgcache
static

Referenced by GHom::garbage(), and GHom::has_image().


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