1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
|
/**CFile****************************************************************
FileName [dsdMan.c]
PackageName [DSD: Disjoint-support decomposition package.]
Synopsis [APIs of the DSD manager.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 8.0. Started - September 22, 2003.]
Revision [$Id: dsdMan.c,v 1.0 2002/22/09 00:00:00 alanmi Exp $]
***********************************************************************/
#include "dsdInt.h"
////////////////////////////////////////////////////////////////////////
/// FUNCTION DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// API OF DSD MANAGER ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Starts the DSD manager.]
Description [Takes the started BDD manager and the maximum support size
of the function to be DSD-decomposed. The manager should have at least as
many variables as there are variables in the support. The functions should
be expressed using the first nSuppSizeMax variables in the manager (these
may be ordered not necessarily on top of the manager).]
SideEffects []
SeeAlso []
***********************************************************************/
Dsd_Manager_t * Dsd_ManagerStart( DdManager * dd, int nSuppMax, int fVerbose )
{
Dsd_Manager_t * dMan;
Dsd_Node_t * pNode;
int i;
assert( nSuppMax <= dd->size );
dMan = ALLOC( Dsd_Manager_t, 1 );
memset( dMan, 0, sizeof(Dsd_Manager_t) );
dMan->dd = dd;
dMan->nInputs = nSuppMax;
dMan->fVerbose = fVerbose;
dMan->nRoots = 0;
dMan->nRootsAlloc = 50;
dMan->pRoots = (Dsd_Node_t **) malloc( dMan->nRootsAlloc * sizeof(Dsd_Node_t *) );
dMan->pInputs = (Dsd_Node_t **) malloc( dMan->nInputs * sizeof(Dsd_Node_t *) );
// create the primary inputs and insert them into the table
dMan->Table = st_init_table(st_ptrcmp, st_ptrhash);
for ( i = 0; i < dMan->nInputs; i++ )
{
pNode = Dsd_TreeNodeCreate( DSD_NODE_BUF, 1, 0 );
pNode->G = dd->vars[i]; Cudd_Ref( pNode->G );
pNode->S = dd->vars[i]; Cudd_Ref( pNode->S );
st_insert( dMan->Table, (char*)dd->vars[i], (char*)pNode );
dMan->pInputs[i] = pNode;
}
pNode = Dsd_TreeNodeCreate( DSD_NODE_CONST1, 0, 0 );
pNode->G = b1; Cudd_Ref( pNode->G );
pNode->S = b1; Cudd_Ref( pNode->S );
st_insert( dMan->Table, (char*)b1, (char*)pNode );
Dsd_CheckCacheAllocate( 5000 );
return dMan;
}
/**Function*************************************************************
Synopsis [Stops the DSD manager.]
Description [Stopping the DSD manager automatically derefereces and
deallocates all the DSD nodes that were created during the life time
of the DSD manager. As a result, the user does not need to deref or
deallocate any DSD nodes or trees that are derived and placed in
the manager while it exists.]
SideEffects []
SeeAlso []
***********************************************************************/
void Dsd_ManagerStop( Dsd_Manager_t * dMan )
{
st_generator * gen;
Dsd_Node_t * pNode;
DdNode * bFunc;
// delete the nodes
st_foreach_item( dMan->Table, gen, (char**)&bFunc, (char**)&pNode )
Dsd_TreeNodeDelete( dMan->dd, Dsd_Regular(pNode) );
st_free_table(dMan->Table);
free( dMan->pInputs );
free( dMan->pRoots );
free( dMan );
Dsd_CheckCacheDeallocate();
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
|
