diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2015-04-10 21:30:53 +0900 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2015-04-10 21:30:53 +0900 |
| commit | dff6e2ab3162b33b309d20a8c8bde07e6a5590ac (patch) | |
| tree | e53eb51d73edb51904eadfba1cf40f2b2b6cef6a /src/misc/extra | |
| parent | b6b9d284c4895f48c61294a8619ab14bf3bc14b3 (diff) | |
| download | abc-dff6e2ab3162b33b309d20a8c8bde07e6a5590ac.tar.gz abc-dff6e2ab3162b33b309d20a8c8bde07e6a5590ac.tar.bz2 abc-dff6e2ab3162b33b309d20a8c8bde07e6a5590ac.zip | |
Procedure to dump ZDD representing a set of cubes into a PLA file.
Diffstat (limited to 'src/misc/extra')
| -rw-r--r-- | src/misc/extra/extraBdd.h | 1 | ||||
| -rw-r--r-- | src/misc/extra/extraBddMisc.c | 39 |
2 files changed, 40 insertions, 0 deletions
diff --git a/src/misc/extra/extraBdd.h b/src/misc/extra/extraBdd.h index 1f86950c..3dbc6264 100644 --- a/src/misc/extra/extraBdd.h +++ b/src/misc/extra/extraBdd.h @@ -196,6 +196,7 @@ extern DdNode * extraBddChangePolarity( DdManager * dd, DdNode * bFunc, DdNo extern int Extra_bddVarIsInCube( DdNode * bCube, int iVar ); extern DdNode * Extra_bddAndPermute( DdManager * ddF, DdNode * bF, DdManager * ddG, DdNode * bG, int * pPermute ); extern int Extra_bddCountCubes( DdManager * dd, DdNode ** pFuncs, int nFuncs, int fMode, int nLimit, int * pGuide ); +extern void Extra_zddDumpPla( DdManager * dd, DdNode * zCover, int nVars, char * pFileName ); #ifndef ABC_PRB #define ABC_PRB(dd,f) printf("%s = ", #f); Extra_bddPrint(dd,f); printf("\n") diff --git a/src/misc/extra/extraBddMisc.c b/src/misc/extra/extraBddMisc.c index be6c03f1..a2ba4036 100644 --- a/src/misc/extra/extraBddMisc.c +++ b/src/misc/extra/extraBddMisc.c @@ -2293,6 +2293,45 @@ printf( "|F| =%6d |G| =%6d |H| =%6d |F|*|G| =%9d ", Cudd_AutodynEnable( ddF, CUDD_REORDER_SYMM_SIFT ); } +/**Function************************************************************* + + Synopsis [Writes ZDD into a PLA file.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Extra_zddDumpPla( DdManager * dd, DdNode * F, int nVars, char * pFileName ) +{ + DdGen *gen; + char * pCube; + int * pPath, i; + FILE * pFile = fopen( pFileName, "wb" ); + if ( pFile == NULL ) + { + printf( "Cannot open file \"%s\" for writing.\n", pFileName ); + return; + } + fprintf( pFile, "# PLA file dumped by Extra_zddDumpPla() in ABC\n" ); + fprintf( pFile, ".i %d\n", nVars ); + fprintf( pFile, ".o 1\n" ); + pCube = ABC_CALLOC( char, dd->sizeZ ); + Cudd_zddForeachPath( dd, F, gen, pPath ) + { + for ( i = 0; i < nVars; i++ ) + pCube[i] = '-'; + for ( i = 0; i < nVars; i++ ) + if ( pPath[2*i] == 1 || pPath[2*i+1] == 1 ) + pCube[i] = '0' + (pPath[2*i] == 1); + fprintf( pFile, "%s 1\n", pCube ); + } + fprintf( pFile, ".e\n\n" ); + fclose( pFile ); + ABC_FREE( pCube ); +} //////////////////////////////////////////////////////////////////////// /// END OF FILE /// |