1 /**CFile**************************************************************** 2 3 FileName [extraBdd.h] 4 5 SystemName [ABC: Logic synthesis and verification system.] 6 7 PackageName [extra] 8 9 Synopsis [Various reusable software utilities.] 10 11 Description [This library contains a number of operators and 12 traversal routines developed to extend the functionality of 13 CUDD v.2.3.x, by Fabio Somenzi (http://vlsi.colorado.edu/~fabio/) 14 To compile your code with the library, #include "extra.h" 15 in your source files and link your project to CUDD and this 16 library. Use the library at your own risk and with caution. 17 Note that debugging of some operators still continues.] 18 19 Author [Alan Mishchenko] 20 21 Affiliation [UC Berkeley] 22 23 Date [Ver. 1.0. Started - June 20, 2005.] 24 25 Revision [$Id: extraBdd.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $] 26 27 ***********************************************************************/ 28 29 #ifndef ABC__misc__extra__extra_bdd_h 30 #define ABC__misc__extra__extra_bdd_h 31 32 33 #ifdef _WIN32 34 #define inline __inline // compatible with MS VS 6.0 35 #endif 36 37 /*---------------------------------------------------------------------------*/ 38 /* Nested includes */ 39 /*---------------------------------------------------------------------------*/ 40 41 #include <stdio.h> 42 #include <stdlib.h> 43 #include <string.h> 44 #include <assert.h> 45 46 #include "misc/st/st.h" 47 #include "bdd/cudd/cuddInt.h" 48 #include "misc/extra/extra.h" 49 50 51 ABC_NAMESPACE_HEADER_START 52 53 54 /*---------------------------------------------------------------------------*/ 55 /* Constant declarations */ 56 /*---------------------------------------------------------------------------*/ 57 58 /*---------------------------------------------------------------------------*/ 59 /* Stucture declarations */ 60 /*---------------------------------------------------------------------------*/ 61 62 /*---------------------------------------------------------------------------*/ 63 /* Type declarations */ 64 /*---------------------------------------------------------------------------*/ 65 66 /*---------------------------------------------------------------------------*/ 67 /* Variable declarations */ 68 /*---------------------------------------------------------------------------*/ 69 70 /*---------------------------------------------------------------------------*/ 71 /* Macro declarations */ 72 /*---------------------------------------------------------------------------*/ 73 74 /* constants of the manager */ 75 #define b0 Cudd_Not((dd)->one) 76 #define b1 (dd)->one 77 #define z0 (dd)->zero 78 #define z1 (dd)->one 79 #define a0 (dd)->zero 80 #define a1 (dd)->one 81 82 // hash key macros 83 #define hashKey1(a,TSIZE) \ 84 ((ABC_PTRUINT_T)(a) % TSIZE) 85 86 #define hashKey2(a,b,TSIZE) \ 87 (((ABC_PTRUINT_T)(a) + (ABC_PTRUINT_T)(b) * DD_P1) % TSIZE) 88 89 #define hashKey3(a,b,c,TSIZE) \ 90 (((((ABC_PTRUINT_T)(a) + (ABC_PTRUINT_T)(b)) * DD_P1 + (ABC_PTRUINT_T)(c)) * DD_P2 ) % TSIZE) 91 92 #define hashKey4(a,b,c,d,TSIZE) \ 93 ((((((ABC_PTRUINT_T)(a) + (ABC_PTRUINT_T)(b)) * DD_P1 + (ABC_PTRUINT_T)(c)) * DD_P2 + \ 94 (ABC_PTRUINT_T)(d)) * DD_P3) % TSIZE) 95 96 #define hashKey5(a,b,c,d,e,TSIZE) \ 97 (((((((ABC_PTRUINT_T)(a) + (ABC_PTRUINT_T)(b)) * DD_P1 + (ABC_PTRUINT_T)(c)) * DD_P2 + \ 98 (ABC_PTRUINT_T)(d)) * DD_P3 + (ABC_PTRUINT_T)(e)) * DD_P1) % TSIZE) 99 100 /*===========================================================================*/ 101 /* Various Utilities */ 102 /*===========================================================================*/ 103 104 /*=== extraBddAuto.c ========================================================*/ 105 106 extern DdNode * Extra_bddSpaceFromFunctionFast( DdManager * dd, DdNode * bFunc ); 107 extern DdNode * Extra_bddSpaceFromFunction( DdManager * dd, DdNode * bF, DdNode * bG ); 108 extern DdNode * extraBddSpaceFromFunction( DdManager * dd, DdNode * bF, DdNode * bG ); 109 extern DdNode * Extra_bddSpaceFromFunctionPos( DdManager * dd, DdNode * bFunc ); 110 extern DdNode * extraBddSpaceFromFunctionPos( DdManager * dd, DdNode * bFunc ); 111 extern DdNode * Extra_bddSpaceFromFunctionNeg( DdManager * dd, DdNode * bFunc ); 112 extern DdNode * extraBddSpaceFromFunctionNeg( DdManager * dd, DdNode * bFunc ); 113 114 extern DdNode * Extra_bddSpaceCanonVars( DdManager * dd, DdNode * bSpace ); 115 extern DdNode * extraBddSpaceCanonVars( DdManager * dd, DdNode * bSpace ); 116 117 extern DdNode * Extra_bddSpaceEquations( DdManager * dd, DdNode * bSpace ); 118 extern DdNode * Extra_bddSpaceEquationsNeg( DdManager * dd, DdNode * bSpace ); 119 extern DdNode * extraBddSpaceEquationsNeg( DdManager * dd, DdNode * bSpace ); 120 extern DdNode * Extra_bddSpaceEquationsPos( DdManager * dd, DdNode * bSpace ); 121 extern DdNode * extraBddSpaceEquationsPos( DdManager * dd, DdNode * bSpace ); 122 123 extern DdNode * Extra_bddSpaceFromMatrixPos( DdManager * dd, DdNode * zA ); 124 extern DdNode * extraBddSpaceFromMatrixPos( DdManager * dd, DdNode * zA ); 125 extern DdNode * Extra_bddSpaceFromMatrixNeg( DdManager * dd, DdNode * zA ); 126 extern DdNode * extraBddSpaceFromMatrixNeg( DdManager * dd, DdNode * zA ); 127 128 extern DdNode * Extra_bddSpaceReduce( DdManager * dd, DdNode * bFunc, DdNode * bCanonVars ); 129 extern DdNode ** Extra_bddSpaceExorGates( DdManager * dd, DdNode * bFuncRed, DdNode * zEquations ); 130 131 /*=== extraBddCas.c =============================================================*/ 132 133 /* performs the binary encoding of the set of function using the given vars */ 134 extern DdNode * Extra_bddEncodingBinary( DdManager * dd, DdNode ** pbFuncs, int nFuncs, DdNode ** pbVars, int nVars ); 135 /* solves the column encoding problem using a sophisticated method */ 136 extern DdNode * Extra_bddEncodingNonStrict( DdManager * dd, DdNode ** pbColumns, int nColumns, DdNode * bVarsCol, DdNode ** pCVars, int nMulti, int * pSimple ); 137 /* collects the nodes under the cut and, for each node, computes the sum of paths leading to it from the root */ 138 extern st__table * Extra_bddNodePathsUnderCut( DdManager * dd, DdNode * bFunc, int CutLevel ); 139 /* collects the nodes under the cut starting from the given set of ADD nodes */ 140 extern int Extra_bddNodePathsUnderCutArray( DdManager * dd, DdNode ** paNodes, DdNode ** pbCubes, int nNodes, DdNode ** paNodesRes, DdNode ** pbCubesRes, int CutLevel ); 141 /* find the profile of a DD (the number of edges crossing each level) */ 142 extern int Extra_ProfileWidth( DdManager * dd, DdNode * F, int * Profile, int CutLevel ); 143 144 /*=== extraBddImage.c ================================================================*/ 145 146 typedef struct Extra_ImageTree_t_ Extra_ImageTree_t; 147 extern Extra_ImageTree_t * Extra_bddImageStart( 148 DdManager * dd, DdNode * bCare, 149 int nParts, DdNode ** pbParts, 150 int nVars, DdNode ** pbVars, int fVerbose ); 151 extern DdNode * Extra_bddImageCompute( Extra_ImageTree_t * pTree, DdNode * bCare ); 152 extern void Extra_bddImageTreeDelete( Extra_ImageTree_t * pTree ); 153 extern DdNode * Extra_bddImageRead( Extra_ImageTree_t * pTree ); 154 155 typedef struct Extra_ImageTree2_t_ Extra_ImageTree2_t; 156 extern Extra_ImageTree2_t * Extra_bddImageStart2( 157 DdManager * dd, DdNode * bCare, 158 int nParts, DdNode ** pbParts, 159 int nVars, DdNode ** pbVars, int fVerbose ); 160 extern DdNode * Extra_bddImageCompute2( Extra_ImageTree2_t * pTree, DdNode * bCare ); 161 extern void Extra_bddImageTreeDelete2( Extra_ImageTree2_t * pTree ); 162 extern DdNode * Extra_bddImageRead2( Extra_ImageTree2_t * pTree ); 163 164 /*=== extraBddMisc.c ========================================================*/ 165 166 extern DdNode * Extra_TransferPermute( DdManager * ddSource, DdManager * ddDestination, DdNode * f, int * Permute ); 167 extern DdNode * Extra_TransferLevelByLevel( DdManager * ddSource, DdManager * ddDestination, DdNode * f ); 168 extern DdNode * Extra_bddRemapUp( DdManager * dd, DdNode * bF ); 169 extern DdNode * Extra_bddMove( DdManager * dd, DdNode * bF, int nVars ); 170 extern DdNode * extraBddMove( DdManager * dd, DdNode * bF, DdNode * bFlag ); 171 extern void Extra_StopManager( DdManager * dd ); 172 extern void Extra_bddPrint( DdManager * dd, DdNode * F ); 173 extern void Extra_bddPrintSupport( DdManager * dd, DdNode * F ); 174 extern void extraDecomposeCover( DdManager* dd, DdNode* zC, DdNode** zC0, DdNode** zC1, DdNode** zC2 ); 175 extern int Extra_bddSuppSize( DdManager * dd, DdNode * bSupp ); 176 extern int Extra_bddSuppContainVar( DdManager * dd, DdNode * bS, DdNode * bVar ); 177 extern int Extra_bddSuppOverlapping( DdManager * dd, DdNode * S1, DdNode * S2 ); 178 extern int Extra_bddSuppDifferentVars( DdManager * dd, DdNode * S1, DdNode * S2, int DiffMax ); 179 extern int Extra_bddSuppCheckContainment( DdManager * dd, DdNode * bL, DdNode * bH, DdNode ** bLarge, DdNode ** bSmall ); 180 extern int * Extra_SupportArray( DdManager * dd, DdNode * F, int * support ); 181 extern int * Extra_VectorSupportArray( DdManager * dd, DdNode ** F, int n, int * support ); 182 extern DdNode * Extra_bddFindOneCube( DdManager * dd, DdNode * bF ); 183 extern DdNode * Extra_bddGetOneCube( DdManager * dd, DdNode * bFunc ); 184 extern DdNode * Extra_bddComputeRangeCube( DdManager * dd, int iStart, int iStop ); 185 extern DdNode * Extra_bddBitsToCube( DdManager * dd, int Code, int CodeWidth, DdNode ** pbVars, int fMsbFirst ); 186 extern DdNode * Extra_bddSupportNegativeCube( DdManager * dd, DdNode * f ); 187 extern int Extra_bddIsVar( DdNode * bFunc ); 188 extern DdNode * Extra_bddCreateAnd( DdManager * dd, int nVars ); 189 extern DdNode * Extra_bddCreateOr( DdManager * dd, int nVars ); 190 extern DdNode * Extra_bddCreateExor( DdManager * dd, int nVars ); 191 extern DdNode * Extra_zddPrimes( DdManager * dd, DdNode * F ); 192 extern void Extra_bddPermuteArray( DdManager * dd, DdNode ** bNodesIn, DdNode ** bNodesOut, int nNodes, int *permut ); 193 extern DdNode * Extra_bddComputeCube( DdManager * dd, DdNode ** bXVars, int nVars ); 194 extern DdNode * Extra_bddChangePolarity( DdManager * dd, DdNode * bFunc, DdNode * bVars ); 195 extern DdNode * extraBddChangePolarity( DdManager * dd, DdNode * bFunc, DdNode * bVars ); 196 extern int Extra_bddVarIsInCube( DdNode * bCube, int iVar ); 197 extern DdNode * Extra_bddAndPermute( DdManager * ddF, DdNode * bF, DdManager * ddG, DdNode * bG, int * pPermute ); 198 extern int Extra_bddCountCubes( DdManager * dd, DdNode ** pFuncs, int nFuncs, int fMode, int nLimit, int * pGuide ); 199 extern void Extra_zddDumpPla( DdManager * dd, DdNode * zCover, int nVars, char * pFileName ); 200 201 /* build the set of all tuples of K variables out of N */ 202 extern DdNode * Extra_bddTuples( DdManager * dd, int K, DdNode * bVarsN ); 203 extern DdNode * extraBddTuples( DdManager * dd, DdNode * bVarsK, DdNode * bVarsN ); 204 205 #ifndef ABC_PRB 206 #define ABC_PRB(dd,f) printf("%s = ", #f); Extra_bddPrint(dd,f); printf("\n") 207 #endif 208 209 /*=== extraMaxMin.c ==============================================================*/ 210 211 /* maximal/minimimal */ 212 extern DdNode * Extra_zddMaximal (DdManager *dd, DdNode *S); 213 extern DdNode * extraZddMaximal (DdManager *dd, DdNode *S); 214 extern DdNode * Extra_zddMinimal (DdManager *dd, DdNode *S); 215 extern DdNode * extraZddMinimal (DdManager *dd, DdNode *S); 216 /* maximal/minimal of the union of two sets of subsets */ 217 extern DdNode * Extra_zddMaxUnion (DdManager *dd, DdNode *S, DdNode *T); 218 extern DdNode * extraZddMaxUnion (DdManager *dd, DdNode *S, DdNode *T); 219 extern DdNode * Extra_zddMinUnion (DdManager *dd, DdNode *S, DdNode *T); 220 extern DdNode * extraZddMinUnion (DdManager *dd, DdNode *S, DdNode *T); 221 /* dot/cross products */ 222 extern DdNode * Extra_zddDotProduct (DdManager *dd, DdNode *S, DdNode *T); 223 extern DdNode * extraZddDotProduct (DdManager *dd, DdNode *S, DdNode *T); 224 extern DdNode * Extra_zddCrossProduct (DdManager *dd, DdNode *S, DdNode *T); 225 extern DdNode * extraZddCrossProduct (DdManager *dd, DdNode *S, DdNode *T); 226 extern DdNode * Extra_zddMaxDotProduct (DdManager *dd, DdNode *S, DdNode *T); 227 extern DdNode * extraZddMaxDotProduct (DdManager *dd, DdNode *S, DdNode *T); 228 229 /*=== extraBddSet.c ==============================================================*/ 230 231 /* subset/supset operations */ 232 extern DdNode * Extra_zddSubSet (DdManager *dd, DdNode *X, DdNode *Y); 233 extern DdNode * extraZddSubSet (DdManager *dd, DdNode *X, DdNode *Y); 234 extern DdNode * Extra_zddSupSet (DdManager *dd, DdNode *X, DdNode *Y); 235 extern DdNode * extraZddSupSet (DdManager *dd, DdNode *X, DdNode *Y); 236 extern DdNode * Extra_zddNotSubSet (DdManager *dd, DdNode *X, DdNode *Y); 237 extern DdNode * extraZddNotSubSet (DdManager *dd, DdNode *X, DdNode *Y); 238 extern DdNode * Extra_zddNotSupSet (DdManager *dd, DdNode *X, DdNode *Y); 239 extern DdNode * extraZddNotSupSet (DdManager *dd, DdNode *X, DdNode *Y); 240 extern DdNode * Extra_zddMaxNotSupSet (DdManager *dd, DdNode *X, DdNode *Y); 241 extern DdNode * extraZddMaxNotSupSet (DdManager *dd, DdNode *X, DdNode *Y); 242 /* check whether the empty combination belongs to the set of subsets */ 243 extern int Extra_zddEmptyBelongs (DdManager *dd, DdNode* zS); 244 /* check whether the set consists of one subset only */ 245 extern int Extra_zddIsOneSubset (DdManager *dd, DdNode* zS); 246 247 /*=== extraBddKmap.c ================================================================*/ 248 249 /* displays the Karnaugh Map of a function */ 250 extern void Extra_PrintKMap( FILE * pFile, DdManager * dd, DdNode * OnSet, DdNode * OffSet, int nVars, DdNode ** XVars, int fSuppType, char ** pVarNames ); 251 /* displays the Karnaugh Map of a relation */ 252 extern void Extra_PrintKMapRelation( FILE * pFile, DdManager * dd, DdNode * OnSet, DdNode * OffSet, int nXVars, int nYVars, DdNode ** XVars, DdNode ** YVars ); 253 254 /*=== extraBddSymm.c =================================================================*/ 255 256 typedef struct Extra_SymmInfo_t_ Extra_SymmInfo_t; 257 struct Extra_SymmInfo_t_ { 258 int nVars; // the number of variables in the support 259 int nVarsMax; // the number of variables in the DD manager 260 int nSymms; // the number of pair-wise symmetries 261 int nNodes; // the number of nodes in a ZDD (if applicable) 262 int * pVars; // the list of all variables present in the support 263 char ** pSymms; // the symmetry information 264 }; 265 266 /* computes the classical symmetry information for the function - recursive */ 267 extern Extra_SymmInfo_t * Extra_SymmPairsCompute( DdManager * dd, DdNode * bFunc ); 268 /* computes the classical symmetry information for the function - using naive approach */ 269 extern Extra_SymmInfo_t * Extra_SymmPairsComputeNaive( DdManager * dd, DdNode * bFunc ); 270 extern int Extra_bddCheckVarsSymmetricNaive( DdManager * dd, DdNode * bF, int iVar1, int iVar2 ); 271 272 /* allocates the data structure */ 273 extern Extra_SymmInfo_t * Extra_SymmPairsAllocate( int nVars ); 274 /* deallocates the data structure */ 275 extern void Extra_SymmPairsDissolve( Extra_SymmInfo_t * ); 276 /* print the contents the data structure */ 277 extern void Extra_SymmPairsPrint( Extra_SymmInfo_t * ); 278 /* converts the ZDD into the Extra_SymmInfo_t structure */ 279 extern Extra_SymmInfo_t * Extra_SymmPairsCreateFromZdd( DdManager * dd, DdNode * zPairs, DdNode * bVars ); 280 281 /* computes the classical symmetry information as a ZDD */ 282 extern DdNode * Extra_zddSymmPairsCompute( DdManager * dd, DdNode * bF, DdNode * bVars ); 283 extern DdNode * extraZddSymmPairsCompute( DdManager * dd, DdNode * bF, DdNode * bVars ); 284 /* returns a singleton-set ZDD containing all variables that are symmetric with the given one */ 285 extern DdNode * Extra_zddGetSymmetricVars( DdManager * dd, DdNode * bF, DdNode * bG, DdNode * bVars ); 286 extern DdNode * extraZddGetSymmetricVars( DdManager * dd, DdNode * bF, DdNode * bG, DdNode * bVars ); 287 /* converts a set of variables into a set of singleton subsets */ 288 extern DdNode * Extra_zddGetSingletons( DdManager * dd, DdNode * bVars ); 289 extern DdNode * extraZddGetSingletons( DdManager * dd, DdNode * bVars ); 290 /* filters the set of variables using the support of the function */ 291 extern DdNode * Extra_bddReduceVarSet( DdManager * dd, DdNode * bVars, DdNode * bF ); 292 extern DdNode * extraBddReduceVarSet( DdManager * dd, DdNode * bVars, DdNode * bF ); 293 294 /* checks the possibility that the two vars are symmetric */ 295 extern int Extra_bddCheckVarsSymmetric( DdManager * dd, DdNode * bF, int iVar1, int iVar2 ); 296 extern DdNode * extraBddCheckVarsSymmetric( DdManager * dd, DdNode * bF, DdNode * bVars ); 297 298 /* build the set of all tuples of K variables out of N from the BDD cube */ 299 extern DdNode * Extra_zddTuplesFromBdd( DdManager * dd, int K, DdNode * bVarsN ); 300 extern DdNode * extraZddTuplesFromBdd( DdManager * dd, DdNode * bVarsK, DdNode * bVarsN ); 301 /* selects one subset from a ZDD representing the set of subsets */ 302 extern DdNode * Extra_zddSelectOneSubset( DdManager * dd, DdNode * zS ); 303 extern DdNode * extraZddSelectOneSubset( DdManager * dd, DdNode * zS ); 304 305 /*=== extraBddUnate.c =================================================================*/ 306 307 extern DdNode * Extra_bddAndTime( DdManager * dd, DdNode * f, DdNode * g, int TimeOut ); 308 extern DdNode * Extra_bddAndAbstractTime( DdManager * manager, DdNode * f, DdNode * g, DdNode * cube, int TimeOut ); 309 extern DdNode * Extra_TransferPermuteTime( DdManager * ddSource, DdManager * ddDestination, DdNode * f, int * Permute, int TimeOut ); 310 311 /*=== extraBddUnate.c =================================================================*/ 312 313 typedef struct Extra_UnateVar_t_ Extra_UnateVar_t; 314 struct Extra_UnateVar_t_ { 315 unsigned iVar : 30; // index of the variable 316 unsigned Pos : 1; // 1 if positive unate 317 unsigned Neg : 1; // 1 if negative unate 318 }; 319 320 typedef struct Extra_UnateInfo_t_ Extra_UnateInfo_t; 321 struct Extra_UnateInfo_t_ { 322 int nVars; // the number of variables in the support 323 int nVarsMax; // the number of variables in the DD manager 324 int nUnate; // the number of unate variables 325 Extra_UnateVar_t * pVars; // the array of variables present in the support 326 }; 327 328 /* allocates the data structure */ 329 extern Extra_UnateInfo_t * Extra_UnateInfoAllocate( int nVars ); 330 /* deallocates the data structure */ 331 extern void Extra_UnateInfoDissolve( Extra_UnateInfo_t * ); 332 /* print the contents the data structure */ 333 extern void Extra_UnateInfoPrint( Extra_UnateInfo_t * ); 334 /* converts the ZDD into the Extra_SymmInfo_t structure */ 335 extern Extra_UnateInfo_t * Extra_UnateInfoCreateFromZdd( DdManager * dd, DdNode * zUnate, DdNode * bVars ); 336 /* naive check of unateness of one variable */ 337 extern int Extra_bddCheckUnateNaive( DdManager * dd, DdNode * bF, int iVar ); 338 339 /* computes the unateness information for the function */ 340 extern Extra_UnateInfo_t * Extra_UnateComputeFast( DdManager * dd, DdNode * bFunc ); 341 extern Extra_UnateInfo_t * Extra_UnateComputeSlow( DdManager * dd, DdNode * bFunc ); 342 343 /* computes the classical symmetry information as a ZDD */ 344 extern DdNode * Extra_zddUnateInfoCompute( DdManager * dd, DdNode * bF, DdNode * bVars ); 345 extern DdNode * extraZddUnateInfoCompute( DdManager * dd, DdNode * bF, DdNode * bVars ); 346 347 /* converts a set of variables into a set of singleton subsets */ 348 extern DdNode * Extra_zddGetSingletonsBoth( DdManager * dd, DdNode * bVars ); 349 extern DdNode * extraZddGetSingletonsBoth( DdManager * dd, DdNode * bVars ); 350 351 /**AutomaticEnd***************************************************************/ 352 353 354 355 ABC_NAMESPACE_HEADER_END 356 357 358 359 #endif /* __EXTRA_H__ */ 360