STACCATO is stylistically similar to CUDD. The basic idea is that one must first create a BDD of a function using CUDD. Then STACCATO is invoked to decompose that BDD. The following code example creates a simple BDD and finds its DSD using STACCATO. The resulting DSD is examined using various functions in STACCATO. Please refer to the file DSDInterface.h for a description of the most relevant functions for the user. To run this code simply type the following:
Make sure to put the DSD library along with the CUDD libraries into your library path. Also, the CUDD and STACCATO interface header files should be included in the path.
Important: STACCATO currently does not support dynamic reordering. After constructing BDDs with CUDD, disable dynamic reordering as shown in the example below. Also, the package currently can handle no more than a BDD variable index higher than 16384. This limitation will be resolved shortly. Finally, unlike CUDD, when a referencing error occurs, STACCATO often throws out some cryptic assert error message. I will try to make this more intuitive in the future so that debugging big programs can be done more easily.
int main()
{
DSDNode *dsd, *dsd_temp;
DdManager *manager;
DSDManager *dmanager;
DdNode *bdd, *temp, *temp2, *symbolic_kernel;
int num_actuals, type, i, *size;
/*initialize CUDD manager*/
manager = Cudd_Init(0,4,CUDD_UNIQUE_SLOTS,
CUDD_CACHE_SLOTS, 0);
/*Creating a BDD, a((b XOR c) + d)*/
temp = Cudd_bddIthVar(manager, 1);
temp2 = Cudd_bddIthVar(manager, 2);
temp = Cudd_bddXor(manager, temp, temp2);
Cudd_Ref(temp);
temp2 = Cudd_bddIthVar(manager, 3);
temp2 = Cudd_bddOr(manager, temp, temp2);
Cudd_Ref(temp2);
Cudd_RecursiveDeref(manager, temp);
temp = Cudd_bddIthVar(manager, 0);
bdd = Cudd_bddAnd(manager, temp, temp2);
Cudd_Ref(bdd);
Cudd_RecursiveDeref(manager, temp2);
/*Initialize DSD manager by choosing a starting cache size*/
dmanager = DSD_Init(manager,
Cudd_ReadMemoryInUse(manager)/2);
/*Create a DSD from a BDD*/
dsd = DSD_Create(dmanager, bdd);
/*Always reference after creation!!!*/
DSD_Ref(dmanager, dsd);
/*gathering simple decomposition information*/
symbolic_kernel = get_symbolic_kernel(dsd);
num_actuals = get_num_actuals(dsd);
type = Get_Type(dsd);
Recursive_Decomposition_Print(dsd);
/*iterating through actuals list--
make sure to unmark before calling DSD_Create again*/
for(i = 0; i < num_actuals; i++)
{
dsd_temp = Get_X_Input(dsd, i);
mark_decomposition(dsd_temp);
}
for(i = 0; i < num_actuals; i++)
{
dsd_temp = Get_X_Input(dsd, i);
if(is_marked(dsd_temp))
{
unmark_decomposition(dsd_temp);
}
}
/*Reclaim DSD and CUDD memory*/
DSD_Quit(dmanager);
Cudd_Quit(manager);
}
The above code should provide the reader with some of the basic manipulations possible with STACCATO. The Recursive_Decomposition_Print function outputs the DSD with symbolic kernel information to stdout. The two while loops in this code are just to illustrate that traversing the actuals list is a simple task. Also, it is possible to traverse the actuals list of decompositions returned by Get_X_Input.