DSDInterface.h File Reference

#include "DSD.h"
#include "DSDManager.h"
#include "DSDDecompose.h"
#include "DSDManipulations.h"
#include "DSDUtilities.h"

Go to the source code of this file.

Defines
#define	RECOMMENDATION_DEFAULT   1000000
Functions
DSDManager *	DSD_Init (DdManager *manager, int_32 recommendation_size)
void	DSD_Quit (DSDManager *manager)
DSDNode *	DSD_Create (DSDManager *manager, DdNode *f)
void	DSD_RecursiveDeref (DSDManager *manger, DSDNode *dsd_node)
void	DSD_Ref (DSDManager *manager, DSDNode *dsd_node)
void	DSD_Deref (DSDManager *manager, DSDNode *dsd_node)
DdNode *	get_symbolic_kernel (DSDNode *dsd_node)
DdNode *	get_bdd (DSDNode *dsd_node)
int_32	Get_Type (DSDNode *dsd_node)
int_32	get_num_actuals (DSDNode *dsd_node)
DSDNode *	Get_X_Input (DSDNode *dsd_node, int index)
void	mark_decomposition (DSDNode *dsd_node)
void	unmark_decomposition (DSDNode *dsd_node)
int	is_marked (DSDNode *dsd_node)
void	Decomposition_Print (DSDNode *dsd_node)
void	Recursive_Decomposition_Print (DSDNode *dsd_node)
void	load_arrays (DSDManager *manager, DSDNode *result)
void	print_stats (DSDManager *manager)
void	count_unique (DSDManager *manager, DSDNode *node)
void	update_blocks (DSDManager *manager, DSDNode *result)
void	validate_deref (DSDManager *manager)
void	check_one (DSDNode *node)

---

Define Documentation

#define RECOMMENDATION_DEFAULT   1000000

A default starting cache value for the DSD unique table. This value should get passed into the DSD_Init function when no prior knowledge is known about future size requirements.

---

Function Documentation

void check_one (  DSDNode *  node  )

void count_unique (  DSDManager *  manager, DSDNode *  node )

void Decomposition_Print (  DSDNode *  dsd_node  )

prints actuals list and decomposition type

DSDNode* DSD_Create (  DSDManager *  manager, DdNode *  f )

Basic DSD creation function. It takes a pointer to the DSD Manager along with a BDD

void DSD_Deref (  DSDManager *  manager, DSDNode *  dsd_node )

This function just derefs the top block in the decomposition. It behaves similarly to the version CUDD uses for BDDs

DSDManager* DSD_Init (  DdManager *  manager, int_32  recommendation_size )

set recommendation_size to some factor of the memory used to produce the initial BDDs

void DSD_Quit (  DSDManager *  manager  )

void DSD_RecursiveDeref (  DSDManager *  manger, DSDNode *  dsd_node )

This function derefs in the same manner as CUDD does for BDDs

void DSD_Ref (  DSDManager *  manager, DSDNode *  dsd_node )

This function is the analogue to CUDD version and must be called after creating or producing a DSD

DdNode* get_bdd (  DSDNode *  dsd_node  )

This function returns the BDD that the DSD represents

int_32 get_num_actuals (  DSDNode *  dsd_node  )

Get the number of actuals in the actuals list

DdNode* get_symbolic_kernel (  DSDNode *  dsd_node  )

This function returns the BDD that points to the symbolic kernel

int_32 Get_Type (  DSDNode *  dsd_node  )

This function returns the type of decomposition, OR, XOR, PRIME, or VAR. OR and XOR decompositions are both associative decompositions. OR, XOR, PRIME, and VAR are #defines in STACCATO

DSDNode* Get_X_Input (  DSDNode *  dsd_node, int  index )

This function returns NULL if the variable, index, is less than 0, is equal to the size of the actuals list, or the dsd_node is actually a variable.

int is_marked (  DSDNode *  dsd_node  )

This function returns 1 when the DSD is marked and 0 when the DSD is not marked

void load_arrays (  DSDManager *  manager, DSDNode *  result )

void mark_decomposition (  DSDNode *  dsd_node  )

Used to mark a decomposition. Make sure to unmark any decompostion before computing another decomposition with DSD_Create.

void print_stats (  DSDManager *  manager  )

void Recursive_Decomposition_Print (  DSDNode *  dsd_node  )

prints complete decomposition tree

void unmark_decomposition (  DSDNode *  dsd_node  )

Used to unmark a decomposition

void update_blocks (  DSDManager *  manager, DSDNode *  result )

void validate_deref (  DSDManager *  manager  )

---