Deriving AIG after cell mapping.

5 files changed, 69 insertions, 2 deletions

diff --git a/src/aig/gia/giaIf.c b/src/aig/gia/giaIf.c
index d3239299..1c4ae9c0 100644
--- a/src/aig/gia/giaIf.c
+++ b/src/aig/gia/giaIf.c
@@ -1425,6 +1425,22 @@ int Gia_ManFromIfLogicFindLut( If_Man_t * pIfMan, Gia_Man_t * pNew, If_Cut_t * p
   SeeAlso     []
 
 ***********************************************************************/
+int Gia_ManFromIfLogicFindCell( If_Man_t * pIfMan, Gia_Man_t * pNew, If_Cut_t * pCutBest, sat_solver * pSat, Vec_Int_t * vPiVars, Vec_Int_t * vPoVars, void * pNtkCell, Vec_Int_t * vLeaves, Vec_Int_t * vLits, Vec_Int_t * vCover, Vec_Int_t * vMapping, Vec_Int_t * vMapping2, Vec_Int_t * vPacking )
+{
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Converts IF into GIA manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 Gia_Man_t * Gia_ManFromIfLogic( If_Man_t * pIfMan )
 {
     Gia_Man_t * pNew;
@@ -1432,7 +1448,9 @@ Gia_Man_t * Gia_ManFromIfLogic( If_Man_t * pIfMan )
     If_Obj_t * pIfObj, * pIfLeaf;
     Vec_Int_t * vMapping, * vMapping2, * vPacking = NULL;
     Vec_Int_t * vLeaves, * vLeaves2, * vCover, * vLits;
+    Vec_Int_t * vPiVars = NULL, * vPoVars = NULL;
     sat_solver * pSat = NULL;
+    void * pNtkCell = NULL;
     int i, k, Entry;
     assert( !pIfMan->pPars->fDeriveLuts || pIfMan->pPars->fTruth );
 //    if ( pIfMan->pPars->fEnableCheck07 )
@@ -1478,6 +1496,13 @@ Gia_Man_t * Gia_ManFromIfLogic( If_Man_t * pIfMan )
                     pIfObj->iCopy = Gia_ManFromIfLogicCreateLut( pNew, If_CutTruthW(pIfMan, pCutBest), vLeaves, vCover, vMapping, vMapping2 );
                 pIfObj->iCopy = Abc_LitNotCond( pIfObj->iCopy, pCutBest->fCompl );
             }
+            else if ( pIfMan->pPars->fUseDsd && pIfMan->pPars->fUseDsdTune && pIfMan->pPars->fDeriveLuts )
+            {
+                if ( pSat == NULL )
+                    pSat = (sat_solver *)If_ManSatBuildFromCell( NULL, &vPiVars, &vPoVars, (void **)&pNtkCell );
+                pIfObj->iCopy = Gia_ManFromIfLogicFindCell( pIfMan, pNew, pCutBest, pSat, vPiVars, vPoVars, pNtkCell, vLeaves, vLits, vCover, vMapping, vMapping2, vPacking );
+                pIfObj->iCopy = Abc_LitNotCond( pIfObj->iCopy, pCutBest->fCompl );
+            }
             else if ( (pIfMan->pPars->fDeriveLuts && pIfMan->pPars->fTruth) || pIfMan->pPars->fUseDsd || pIfMan->pPars->fUseTtPerm )
             {
                 word * pTruth = If_CutTruthW(pIfMan, pCutBest);
@@ -1520,6 +1545,10 @@ Gia_Man_t * Gia_ManFromIfLogic( If_Man_t * pIfMan )
     Vec_IntFree( vCover );
     Vec_IntFree( vLeaves );
     Vec_IntFree( vLeaves2 );
+    Vec_IntFreeP( &vPiVars );
+    Vec_IntFreeP( &vPoVars );
+    if ( pNtkCell )
+        ABC_FREE( pNtkCell );
     if ( pSat != NULL )
         sat_solver_delete(pSat);
 //    printf( "Mapping array size:  IfMan = %d. Gia = %d. Increase = %.2f\n", 
diff --git a/src/base/cmd/cmd.c b/src/base/cmd/cmd.c
index 511cee68..42274433 100644
--- a/src/base/cmd/cmd.c
+++ b/src/base/cmd/cmd.c
@@ -1319,6 +1319,32 @@ int CmfFindNumber( char * pName )
 
 /**Function*************************************************************
 
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void CnfDupFileUnzip( char * pOldName )
+{
+    extern char * Io_MvLoadFileBz2( char * pFileName, int * pnFileSize );
+    char pNewName[1000];
+    FILE * pFile;
+    int nFileSize;
+    char * pBuffer = Io_MvLoadFileBz2( pOldName, &nFileSize );
+    assert( strlen(pOldName) < 1000 );
+    sprintf( pNewName, "%s.v", pOldName );
+    pFile = fopen( pNewName, "wb" );
+    fwrite( pBuffer, nFileSize, 1, pFile );
+    fclose( pFile );
+    ABC_FREE( pBuffer );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Command to print the contents of the current directory (Windows).]
 
   Description []
@@ -1446,8 +1472,9 @@ int CmdCommandRenameFiles( Abc_Frame_t * pAbc, int argc, char **argv )
         {
             pOldName = (char *)Vec_PtrEntry( vNames, pOrder[i] );
             sprintf( pNewName, "%s%0*d.%s", pNameNew ? pNameNew : "", nDigits, nBase+Vec_IntEntry(vNums, pOrder[i]), pNameExt );
-            printf( "%s -> %s\n", pOldName, pNewName );
             rename( pOldName, pNewName );
+            printf( "%s -> %s\n", pOldName, pNewName );
+//            CnfDupFileUnzip( pOldName );
         }
         // cleanup
         Vec_PtrFreeFree( vNames );
diff --git a/src/base/io/ioReadBlifMv.c b/src/base/io/ioReadBlifMv.c
index bd7aa78a..d78f567a 100644
--- a/src/base/io/ioReadBlifMv.c
+++ b/src/base/io/ioReadBlifMv.c
@@ -548,7 +548,7 @@ typedef struct buflist {
   struct buflist * next;
 } buflist;
 
-static char * Io_MvLoadFileBz2( char * pFileName, int * pnFileSize )
+char * Io_MvLoadFileBz2( char * pFileName, int * pnFileSize )
 {
     FILE    * pFile;
     int       nFileSize = 0;
diff --git a/src/map/if/if.h b/src/map/if/if.h
index 8114e5c3..a94a5fe8 100644
--- a/src/map/if/if.h
+++ b/src/map/if/if.h
@@ -623,6 +623,8 @@ extern void            If_ManComputeRequired( If_Man_t * p );
 extern void            If_CutRotatePins( If_Man_t * p, If_Cut_t * pCut );
 extern int             If_CutComputeTruth( If_Man_t * p, If_Cut_t * pCut, If_Cut_t * pCut0, If_Cut_t * pCut1, int fCompl0, int fCompl1 );
 extern int             If_CutComputeTruthPerm( If_Man_t * p, If_Cut_t * pCut, If_Cut_t * pCut0, If_Cut_t * pCut1, int fCompl0, int fCompl1 );
+/*=== ifTune.c ===========================================================*/
+extern void *          If_ManSatBuildFromCell( char * pStr, Vec_Int_t ** pvPiVars, Vec_Int_t ** pvPoVars, void ** ppNtk );
 /*=== ifUtil.c ============================================================*/
 extern void            If_ManCleanNodeCopy( If_Man_t * p );
 extern void            If_ManCleanCutData( If_Man_t * p );
diff --git a/src/map/if/ifTune.c b/src/map/if/ifTune.c
index f75192b6..6e48448b 100644
--- a/src/map/if/ifTune.c
+++ b/src/map/if/ifTune.c
@@ -621,6 +621,15 @@ sat_solver * Ifn_ManSatBuild( Ifn_Ntk_t * p, Vec_Int_t ** pvPiVars, Vec_Int_t **
     Gia_ManStop( p2 );
     return pSat;
 }
+void * If_ManSatBuildFromCell( char * pStr, Vec_Int_t ** pvPiVars, Vec_Int_t ** pvPoVars, void ** ppNtk )
+{
+    Ifn_Ntk_t * p = Ifn_NtkParse( pStr );
+    *ppNtk = p;
+    if ( p == NULL )
+        return NULL;
+//    Ifn_NtkPrint( p );
+    return Ifn_ManSatBuild( p, pvPiVars, pvPoVars );
+}
 
 /**Function*************************************************************