diff options
Diffstat (limited to 'src')
| -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 /// |