00001
00021 #include "hop.h"
00022 #include "st.h"
00023
00027
00028 typedef struct Aig_CuddMan_t_ Aig_CuddMan_t;
00029 struct Aig_CuddMan_t_
00030 {
00031 Aig_Man_t * pAig;
00032 st_table * pTable;
00033 };
00034
00035
00036 static Aig_CuddMan_t * s_pCuddMan = NULL;
00037
00041
00053 void Cudd2_Init( unsigned int numVars, unsigned int numVarsZ, unsigned int numSlots, unsigned int cacheSize, unsigned long maxMemory, void * pCudd )
00054 {
00055 int v;
00056
00057 if ( s_pCuddMan != NULL )
00058 return;
00059 s_pCuddMan = ALLOC( Aig_CuddMan_t, 1 );
00060 s_pCuddMan->pAig = Aig_ManStart();
00061 s_pCuddMan->pTable = st_init_table( st_ptrcmp, st_ptrhash );
00062 for ( v = 0; v < (int)numVars; v++ )
00063 Aig_ObjCreatePi( s_pCuddMan->pAig );
00064 }
00065
00077 void Cudd2_Quit( void * pCudd )
00078 {
00079 assert( s_pCuddMan != NULL );
00080 Aig_ManDumpBlif( s_pCuddMan->pAig, "aig_temp.blif" );
00081 Aig_ManStop( s_pCuddMan->pAig );
00082 st_free_table( s_pCuddMan->pTable );
00083 free( s_pCuddMan );
00084 s_pCuddMan = NULL;
00085 }
00086
00098 static Aig_Obj_t * Cudd2_GetArg( void * pArg )
00099 {
00100 Aig_Obj_t * pNode;
00101 assert( s_pCuddMan != NULL );
00102 if ( !st_lookup( s_pCuddMan->pTable, (char *)Aig_Regular(pArg), (char **)&pNode ) )
00103 {
00104 printf( "Cudd2_GetArg(): An argument BDD is not in the hash table.\n" );
00105 return NULL;
00106 }
00107 return Aig_NotCond( pNode, Aig_IsComplement(pArg) );
00108 }
00109
00121 static void Cudd2_SetArg( Aig_Obj_t * pNode, void * pResult )
00122 {
00123 assert( s_pCuddMan != NULL );
00124 if ( st_is_member( s_pCuddMan->pTable, (char *)Aig_Regular(pResult) ) )
00125 return;
00126 pNode = Aig_NotCond( pNode, Aig_IsComplement(pResult) );
00127 st_insert( s_pCuddMan->pTable, (char *)Aig_Regular(pResult), (char *)pNode );
00128 }
00129
00141 void Cudd2_bddOne( void * pCudd, void * pResult )
00142 {
00143 Cudd2_SetArg( Aig_ManConst1(s_pCuddMan->pAig), pResult );
00144 }
00145
00157 void Cudd2_bddIthVar( void * pCudd, int iVar, void * pResult )
00158 {
00159 int v;
00160 assert( s_pCuddMan != NULL );
00161 for ( v = Aig_ManPiNum(s_pCuddMan->pAig); v <= iVar; v++ )
00162 Aig_ObjCreatePi( s_pCuddMan->pAig );
00163 Cudd2_SetArg( Aig_ManPi(s_pCuddMan->pAig, iVar), pResult );
00164 }
00165
00177 void Cudd2_bddAnd( void * pCudd, void * pArg0, void * pArg1, void * pResult )
00178 {
00179 Aig_Obj_t * pNode0, * pNode1, * pNode;
00180 pNode0 = Cudd2_GetArg( pArg0 );
00181 pNode1 = Cudd2_GetArg( pArg1 );
00182 pNode = Aig_And( s_pCuddMan->pAig, pNode0, pNode1 );
00183 Cudd2_SetArg( pNode, pResult );
00184 }
00185
00197 void Cudd2_bddOr( void * pCudd, void * pArg0, void * pArg1, void * pResult )
00198 {
00199 Cudd2_bddAnd( pCudd, Aig_Not(pArg0), Aig_Not(pArg1), Aig_Not(pResult) );
00200 }
00201
00213 void Cudd2_bddNand( void * pCudd, void * pArg0, void * pArg1, void * pResult )
00214 {
00215 Cudd2_bddAnd( pCudd, pArg0, pArg1, Aig_Not(pResult) );
00216 }
00217
00229 void Cudd2_bddNor( void * pCudd, void * pArg0, void * pArg1, void * pResult )
00230 {
00231 Cudd2_bddAnd( pCudd, Aig_Not(pArg0), Aig_Not(pArg1), pResult );
00232 }
00233
00245 void Cudd2_bddXor( void * pCudd, void * pArg0, void * pArg1, void * pResult )
00246 {
00247 Aig_Obj_t * pNode0, * pNode1, * pNode;
00248 pNode0 = Cudd2_GetArg( pArg0 );
00249 pNode1 = Cudd2_GetArg( pArg1 );
00250 pNode = Aig_Exor( s_pCuddMan->pAig, pNode0, pNode1 );
00251 Cudd2_SetArg( pNode, pResult );
00252 }
00253
00265 void Cudd2_bddXnor( void * pCudd, void * pArg0, void * pArg1, void * pResult )
00266 {
00267 Cudd2_bddXor( pCudd, pArg0, pArg1, Aig_Not(pResult) );
00268 }
00269
00281 void Cudd2_bddIte( void * pCudd, void * pArg0, void * pArg1, void * pArg2, void * pResult )
00282 {
00283 Aig_Obj_t * pNode0, * pNode1, * pNode2, * pNode;
00284 pNode0 = Cudd2_GetArg( pArg0 );
00285 pNode1 = Cudd2_GetArg( pArg1 );
00286 pNode2 = Cudd2_GetArg( pArg2 );
00287 pNode = Aig_Mux( s_pCuddMan->pAig, pNode0, pNode1, pNode2 );
00288 Cudd2_SetArg( pNode, pResult );
00289 }
00290
00302 void Cudd2_bddCompose( void * pCudd, void * pArg0, void * pArg1, int v, void * pResult )
00303 {
00304 Aig_Obj_t * pNode0, * pNode1, * pNode;
00305 pNode0 = Cudd2_GetArg( pArg0 );
00306 pNode1 = Cudd2_GetArg( pArg1 );
00307 pNode = Aig_Compose( s_pCuddMan->pAig, pNode0, pNode1, v );
00308 Cudd2_SetArg( pNode, pResult );
00309 }
00310
00322 void Cudd2_bddLeq( void * pCudd, void * pArg0, void * pArg1, int Result )
00323 {
00324 Aig_Obj_t * pNode0, * pNode1, * pNode;
00325 pNode0 = Cudd2_GetArg( pArg0 );
00326 pNode1 = Cudd2_GetArg( pArg1 );
00327 pNode = Aig_And( s_pCuddMan->pAig, pNode0, Aig_Not(pNode1) );
00328 Aig_ObjCreatePo( s_pCuddMan->pAig, pNode );
00329 }
00330
00342 void Cudd2_bddEqual( void * pCudd, void * pArg0, void * pArg1, int Result )
00343 {
00344 Aig_Obj_t * pNode0, * pNode1, * pNode;
00345 pNode0 = Cudd2_GetArg( pArg0 );
00346 pNode1 = Cudd2_GetArg( pArg1 );
00347 pNode = Aig_Exor( s_pCuddMan->pAig, pNode0, pNode1 );
00348 Aig_ObjCreatePo( s_pCuddMan->pAig, pNode );
00349 }
00350
00354
00355
