abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
dsdMan.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [dsdMan.c]
4 
5  PackageName [DSD: Disjoint-support decomposition package.]
6 
7  Synopsis [APIs of the DSD manager.]
8 
9  Author [Alan Mishchenko]
10 
11  Affiliation [UC Berkeley]
12 
13  Date [Ver. 8.0. Started - September 22, 2003.]
14 
15  Revision [$Id: dsdMan.c,v 1.0 2002/22/09 00:00:00 alanmi Exp $]
16 
17 ***********************************************************************/
18 
19 #include "dsdInt.h"
20 
22 
23 
24 ////////////////////////////////////////////////////////////////////////
25 /// FUNCTION DECLARATIONS ///
26 ////////////////////////////////////////////////////////////////////////
27 
28 ////////////////////////////////////////////////////////////////////////
29 /// API OF DSD MANAGER ///
30 ////////////////////////////////////////////////////////////////////////
31 
32 /**Function*************************************************************
33 
34  Synopsis [Starts the DSD manager.]
35 
36  Description [Takes the started BDD manager and the maximum support size
37  of the function to be DSD-decomposed. The manager should have at least as
38  many variables as there are variables in the support. The functions should
39  be expressed using the first nSuppSizeMax variables in the manager (these
40  may be ordered not necessarily on top of the manager).]
41 
42  SideEffects []
43 
44  SeeAlso []
45 
46 ***********************************************************************/
47 Dsd_Manager_t * Dsd_ManagerStart( DdManager * dd, int nSuppMax, int fVerbose )
48 {
49  Dsd_Manager_t * dMan;
50  Dsd_Node_t * pNode;
51  int i;
52 
53  assert( nSuppMax <= dd->size );
54 
55  dMan = ABC_ALLOC( Dsd_Manager_t, 1 );
56  memset( dMan, 0, sizeof(Dsd_Manager_t) );
57  dMan->dd = dd;
58  dMan->nInputs = nSuppMax;
59  dMan->fVerbose = fVerbose;
60  dMan->nRoots = 0;
61  dMan->nRootsAlloc = 50;
62  dMan->pRoots = (Dsd_Node_t **) ABC_ALLOC( char, dMan->nRootsAlloc * sizeof(Dsd_Node_t *) );
63  dMan->pInputs = (Dsd_Node_t **) ABC_ALLOC( char, dMan->nInputs * sizeof(Dsd_Node_t *) );
64 
65  // create the primary inputs and insert them into the table
67  for ( i = 0; i < dMan->nInputs; i++ )
68  {
69  pNode = Dsd_TreeNodeCreate( DSD_NODE_BUF, 1, 0 );
70  pNode->G = dd->vars[i]; Cudd_Ref( pNode->G );
71  pNode->S = dd->vars[i]; Cudd_Ref( pNode->S );
72  st__insert( dMan->Table, (char*)dd->vars[i], (char*)pNode );
73  dMan->pInputs[i] = pNode;
74  }
75  pNode = Dsd_TreeNodeCreate( DSD_NODE_CONST1, 0, 0 );
76  pNode->G = b1; Cudd_Ref( pNode->G );
77  pNode->S = b1; Cudd_Ref( pNode->S );
78  st__insert( dMan->Table, (char*)b1, (char*)pNode );
79  dMan->pConst1 = pNode;
80 
81  Dsd_CheckCacheAllocate( 5000 );
82  return dMan;
83 }
84 
85 /**Function*************************************************************
86 
87  Synopsis [Stops the DSD manager.]
88 
89  Description [Stopping the DSD manager automatically derefereces and
90  deallocates all the DSD nodes that were created during the life time
91  of the DSD manager. As a result, the user does not need to deref or
92  deallocate any DSD nodes or trees that are derived and placed in
93  the manager while it exists.]
94 
95  SideEffects []
96 
97  SeeAlso []
98 
99 ***********************************************************************/
101 {
102  st__generator * gen;
103  Dsd_Node_t * pNode;
104  DdNode * bFunc;
105  // delete the nodes
106  st__foreach_item( dMan->Table, gen, (const char**)&bFunc, (char**)&pNode )
107  Dsd_TreeNodeDelete( dMan->dd, Dsd_Regular(pNode) );
108  st__free_table(dMan->Table);
109  ABC_FREE( dMan->pInputs );
110  ABC_FREE( dMan->pRoots );
111  ABC_FREE( dMan );
113 }
114 
115 ////////////////////////////////////////////////////////////////////////
116 /// END OF FILE ///
117 ////////////////////////////////////////////////////////////////////////
119 
char * memset()
DdNode * S
Definition: dsdInt.h:58
void st__free_table(st__table *table)
Definition: st.c:81
DdManager * dd
Definition: dsdInt.h:42
Definition: cudd.h:278
DdNode * G
Definition: dsdInt.h:57
int fVerbose
Definition: dsdInt.h:50
st__table * Table
Definition: dsdInt.h:43
int st__insert(st__table *table, const char *key, char *value)
Definition: st.c:171
void Dsd_TreeNodeDelete(DdManager *dd, Dsd_Node_t *pNode)
Definition: dsdTree.c:87
Dsd_Node_t * pConst1
Definition: dsdInt.h:49
#define b1
Definition: extraBdd.h:76
void Dsd_CheckCacheAllocate(int nEntries)
FUNCTION DEFINITIONS ///.
Definition: dsdCheck.c:63
int st__ptrcmp(const char *, const char *)
Definition: st.c:480
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
int nSuppMax
Definition: llb3Image.c:83
st__table * st__init_table(st__compare_func_type compare, st__hash_func_type hash)
Definition: st.c:72
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
static int size
Definition: cuddSign.c:86
STRUCTURE DEFINITIONS ///.
Definition: dsdInt.h:40
#define Dsd_Regular(p)
Definition: dsd.h:69
int nRootsAlloc
Definition: dsdInt.h:46
void Dsd_CheckCacheDeallocate()
Definition: dsdCheck.c:97
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
int nInputs
Definition: dsdInt.h:44
Dsd_Node_t * Dsd_TreeNodeCreate(int Type, int nDecs, int BlockNum)
FUNCTION DEFINITIONS ///.
Definition: dsdTree.c:61
Dsd_Node_t ** pInputs
Definition: dsdInt.h:47
#define ABC_FREE(obj)
Definition: abc_global.h:232
DdNode ** vars
Definition: cuddInt.h:390
void Dsd_ManagerStop(Dsd_Manager_t *dMan)
Definition: dsdMan.c:100
#define st__foreach_item(table, gen, key, value)
Definition: st.h:107
#define assert(ex)
Definition: util_old.h:213
void Cudd_Ref(DdNode *n)
Definition: cuddRef.c:129
ABC_NAMESPACE_IMPL_START Dsd_Manager_t * Dsd_ManagerStart(DdManager *dd, int nSuppMax, int fVerbose)
FUNCTION DECLARATIONS ///.
Definition: dsdMan.c:47
int nRoots
Definition: dsdInt.h:45
int st__ptrhash(const char *, int)
Definition: st.c:468
Dsd_Node_t ** pRoots
Definition: dsdInt.h:48