From dff6e2ab3162b33b309d20a8c8bde07e6a5590ac Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Fri, 10 Apr 2015 21:30:53 +0900
Subject: Procedure to dump ZDD representing a set of cubes into a PLA file.

---
 src/misc/extra/extraBdd.h     |  1 +
 src/misc/extra/extraBddMisc.c | 39 +++++++++++++++++++++++++++++++++++++++
 2 files changed, 40 insertions(+)

(limited to 'src/misc/extra')

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                                ///
-- 
cgit v1.2.3