DSDPrimeDecompose.h File Reference

#include "DSDDecompose.h"

Go to the source code of this file.

Functions
DSDNode *	Prime_Decomp (DSDManager *manager, DdNode *f, DdNode *top_func, DSDNode *T, DSDNode *E)
DSDNode *	BDN_MUX_VAR_DEC_DEC (DSDManager *manager, DdNode *f, DdNode *top_func, DSDNode *E, DSDNode *T)
DSDNode *	BDN_BDD_MUX_VAR_DEC_DEC (DSDManager *manager, DdNode *top_func, DSDNode *E, DSDNode *T)
DSDNode *	BDN_BDD_PRIME_SUB (DSDManager *manager, DdNode *f, DdNode *top_func, ActualNode *conflict_residue, DSDNode *node)
DSDNode *	BDN_BDD_PRIME_XOR_SUB (DSDManager *manager, DdNode *f, DdNode *top_func, ActualNode *conflict_residue, DSDNode *node)
DSDNode *	BDN_BDD_PRIME_MUX_SUB (DSDManager *manager, DdNode *f, DdNode *top_func, ActualNode *conflict_residue, DSDNode *node)
ActualNode *	cofactor_container_node_equivalence (DSDManager *manager, DSDNode *container, DSDNode *child)
ActualNode *	cofactor_cofactor_equivalence (DSDManager *manager, DSDNode *container, DSDNode *child, int *switch_them)
ActualNode *	cofactor_equivalence (DSDManager *manager, DSDNode *container, DSDNode *child)
DSDNode *	cofactor_elem_BDN_BDD_PRIME_SUB_ELEM (DSDManager *manager, DdNode *f, DdNode *top_func, DSDNode *node1, DSDNode *node2)
int	symbolic_finder_builder (DSDManager *manager, DSDNode *node1, DSDNode *node2)
int	symbolic_finder_builder_incomplete (DSDManager *manager, DSDNode *node1, DSDNode *node2)

---

Function Documentation

DSDNode* BDN_BDD_MUX_VAR_DEC_DEC (  DSDManager *  manager, DdNode *  top_func, DSDNode *  E, DSDNode *  T )

Internal function that creates a BDD that is a mux between the variable top_func and the functions rooted at the DSDs E and T and produces the corresponding DSD

DSDNode* BDN_BDD_PRIME_MUX_SUB (  DSDManager *  manager, DdNode *  f, DdNode *  top_func, ActualNode *  conflict_residue, DSDNode *  node )

Internal function that creates a BDD whose resulting DSD is an inherited prime decomposition

DSDNode* BDN_BDD_PRIME_SUB (  DSDManager *  manager, DdNode *  f, DdNode *  top_func, ActualNode *  conflict_residue, DSDNode *  node )

Internal function that creates a BDD whose resulting DSD is an inherited prime decomposition

DSDNode* BDN_BDD_PRIME_XOR_SUB (  DSDManager *  manager, DdNode *  f, DdNode *  top_func, ActualNode *  conflict_residue, DSDNode *  node )

Internal function that creates a BDD whose resulting DSD is an inherited prime decomposition

DSDNode* BDN_MUX_VAR_DEC_DEC (  DSDManager *  manager, DdNode *  f, DdNode *  top_func, DSDNode *  E, DSDNode *  T )

Internal function that creates a DSD that is a mux between the variable top_func and the functions rooted at the DSDs E and T

ActualNode* cofactor_cofactor_equivalence (  DSDManager *  manager, DSDNode *  container, DSDNode *  child, int *  switch_them )

Internal function used by the Prime Decomp to identify a potential inherited decomposition

ActualNode* cofactor_container_node_equivalence (  DSDManager *  manager, DSDNode *  container, DSDNode *  child )

Internal function used by the Prime Decomp to identify a potential inherited decomposition

DSDNode* cofactor_elem_BDN_BDD_PRIME_SUB_ELEM (  DSDManager *  manager, DdNode *  f, DdNode *  top_func, DSDNode *  node1, DSDNode *  node2 )

Internal function that creates a prime DSD for a complicated special case

ActualNode* cofactor_equivalence (  DSDManager *  manager, DSDNode *  container, DSDNode *  child )

Internal function used by the Prime Decomp to identify a potential inherited decomposition

DSDNode* Prime_Decomp (  DSDManager *  manager, DdNode *  f, DdNode *  top_func, DSDNode *  T, DSDNode *  E )

Internal function tries different algorithms to see whether the resulting DSD will be an inherited prime decomposition

int symbolic_finder_builder (  DSDManager *  manager, DSDNode *  node1, DSDNode *  node2 )

Internal function that supports the function cofactor_elem_BDN_BDD_PRIME_SUB_ELEM

int symbolic_finder_builder_incomplete (  DSDManager *  manager, DSDNode *  node1, DSDNode *  node2 )

!!if(DSD_IsComplement(node2)) { return Cudd_Not(result); } else {

---