Version abc80516

20 files changed, 1922 insertions, 570 deletions

diff --git a/abc.dsp b/abc.dsp
index f856eec0..716ef21e 100644
--- a/abc.dsp
+++ b/abc.dsp
@@ -3266,6 +3266,10 @@ SOURCE=.\src\aig\saig\saigInter.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\aig\saig\saigIoa.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\aig\saig\saigPhase.c
 # End Source File
 # Begin Source File
@@ -3284,6 +3288,10 @@ SOURCE=.\src\aig\saig\saigRetStep.c
 
 SOURCE=.\src\aig\saig\saigScl.c
 # End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\saig\saigTrans.c
+# End Source File
 # End Group
 # Begin Group "bbr"
 
diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h
index bbb5cb6e..6987412d 100644
--- a/src/aig/aig/aig.h
+++ b/src/aig/aig/aig.h
@@ -135,6 +135,7 @@ struct Aig_Man_t_
     Vec_Int_t *      vLevelR;        // the reverse level of the nodes
     int              nLevelMax;      // maximum number of levels
     void *           pData;          // the temporary data
+    void *           pData2;         // the temporary data
     int              nTravIds;       // the current traversal ID
     int              fCatchExor;     // enables EXOR nodes
     int              fAddStrash;     // performs additional strashing
@@ -497,6 +498,7 @@ extern int             Aig_ManCleanup( Aig_Man_t * p );
 extern int             Aig_ManPiCleanup( Aig_Man_t * p );
 extern void            Aig_ManPrintStats( Aig_Man_t * p );
 extern void            Aig_ManReportImprovement( Aig_Man_t * p, Aig_Man_t * pNew );
+extern void            Aig_ManSetRegNum( Aig_Man_t * p, int nRegs );
 /*=== aigMem.c ==========================================================*/
 extern void            Aig_ManStartMemory( Aig_Man_t * p );
 extern void            Aig_ManStopMemory( Aig_Man_t * p );
@@ -625,6 +627,7 @@ extern void            Aig_ManDumpVerilog( Aig_Man_t * p, char * pFileName );
 extern void            Aig_ManSetPioNumbers( Aig_Man_t * p );
 extern void            Aig_ManCleanPioNumbers( Aig_Man_t * p );
 extern int             Aig_ManCountChoices( Aig_Man_t * p );
+extern char *          Aig_FileNameGenericAppend( char * pBase, char * pSuffix );
 extern unsigned        Aig_ManRandom( int fReset );
 
 /*=== aigWin.c =========================================================*/
diff --git a/src/aig/aig/aigMan.c b/src/aig/aig/aigMan.c
index 47ee8d4d..669691f4 100644
--- a/src/aig/aig/aigMan.c
+++ b/src/aig/aig/aigMan.c
@@ -359,6 +359,25 @@ void Aig_ManReportImprovement( Aig_Man_t * p, Aig_Man_t * pNew )
     printf( "\n" );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Sets the number of registers in the AIG manager.]
+
+  Description [This procedure should be called after the manager is 
+  fully constructed.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ManSetRegNum( Aig_Man_t * p, int nRegs )
+{
+    p->nRegs = nRegs;
+    p->nTruePis = Aig_ManPiNum(p) - nRegs;
+    p->nTruePos = Aig_ManPoNum(p) - nRegs;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/aig/aigUtil.c b/src/aig/aig/aigUtil.c
index a01e9582..7b64d562 100644
--- a/src/aig/aig/aigUtil.c
+++ b/src/aig/aig/aigUtil.c
@@ -992,6 +992,28 @@ void Aig_ManPrintControlFanouts( Aig_Man_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Returns the composite name of the file.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Aig_FileNameGenericAppend( char * pBase, char * pSuffix )
+{
+    static char Buffer[1000];
+    char * pDot;
+    strcpy( Buffer, pBase );
+    if ( (pDot = strrchr( Buffer, '.' )) )
+        *pDot = 0;
+    strcat( Buffer, pSuffix );
+    return Buffer;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Creates a sequence or random numbers.]
 
   Description []
diff --git a/src/aig/fra/fraCore.c b/src/aig/fra/fraCore.c
index 11e69b59..92a3f00b 100644
--- a/src/aig/fra/fraCore.c
+++ b/src/aig/fra/fraCore.c
@@ -411,6 +411,7 @@ p->timeTrav += clock() - clk2;
     }
     else
     {
+        Fra_ClassesCopyReprs( p->pCla, p->vTimeouts );
         Aig_ManCleanup( p->pManFraig );
         pManAigNew = p->pManFraig;
         p->pManFraig = NULL;
diff --git a/src/aig/fra/fraInd.c b/src/aig/fra/fraInd.c
index 99b62856..3be0e3f6 100644
--- a/src/aig/fra/fraInd.c
+++ b/src/aig/fra/fraInd.c
@@ -616,6 +616,63 @@ finish:
     return pManAigNew;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Outputs a set of pairs of equivalent nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Fra_FraigInductionTest( char * pFileName, Fra_Ssw_t * pParams )
+{
+    extern Aig_Man_t * Saig_ManReadBlif( char * pFileName );
+    FILE * pFile;
+    char * pFilePairs;
+    Aig_Man_t * pMan, * pNew;
+    Aig_Obj_t * pObj, * pRepr;
+    int * pNum2Id;
+    int i, Counter = 0;
+    pMan = Saig_ManReadBlif( pFileName );
+    if ( pMan == NULL )
+        return 0;
+    // perform seq SAT sweeping
+    pNew = Fra_FraigInduction( pMan, pParams );
+    if ( pNew == NULL )
+    {
+        Aig_ManStop( pMan );
+        return 0;
+    }
+    if ( pParams->fVerbose )
+    {
+        printf( "Original AIG: " );
+        Aig_ManPrintStats( pMan );
+        printf( "Reduced  AIG: " );
+        Aig_ManPrintStats( pNew );
+    }
+    Aig_ManStop( pNew );
+    pNum2Id = pMan->pData;
+    // write the output file
+    pFilePairs = Aig_FileNameGenericAppend( pFileName, ".pairs" );
+    pFile = fopen( pFilePairs, "w" );
+    Aig_ManForEachObj( pMan, pObj, i )
+        if ( (pRepr = pMan->pReprs[pObj->Id]) )
+        {
+            fprintf( pFile, "%d %d %c\n", pNum2Id[pObj->Id], pNum2Id[pRepr->Id], (Aig_ObjPhase(pObj) ^ Aig_ObjPhase(pRepr))? '-' : '+' );
+            Counter++;
+        }
+    fclose( pFile );
+    if ( pParams->fVerbose )
+    {
+        printf( "Result: %d pairs of seq equiv nodes are written into file \"%s\".\n", Counter, pFilePairs );
+    }
+    Aig_ManStop( pMan );
+    return 1;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/ntl/ntl.h b/src/aig/ntl/ntl.h
index c4950650..4179754c 100644
--- a/src/aig/ntl/ntl.h
+++ b/src/aig/ntl/ntl.h
@@ -14,7 +14,7 @@
 
   Date        [Ver. 1.0. Started - June 20, 2005.]
 
-  Revision    [$Id: .h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+  Revision    [$Id: ntl.h,v 1.1 2008/05/14 22:13:09 wudenni Exp $]
 
 ***********************************************************************/
  
@@ -145,8 +145,18 @@ struct Ntl_Lut_t_
 ////////////////////////////////////////////////////////////////////////
 ///                      INLINED FUNCTIONS                           ///
 ////////////////////////////////////////////////////////////////////////
+#ifdef WIN32
+#define DLLEXPORT __declspec(dllexport)
+#define DLLIMPORT __declspec(dllimport)
+#else  /* defined(WIN32) */
+#define DLLIMPORT
+#endif /* defined(WIN32) */
+
+#ifndef ABC_DLL
+#define ABC_DLL DLLIMPORT
+#endif
 
-static inline Ntl_Mod_t * Ntl_ManRootModel( Ntl_Man_t * p )       { return Vec_PtrEntry( p->vModels, 0 );       } 
+static inline Ntl_Mod_t * Ntl_ManRootModel( Ntl_Man_t * p )       { return (Ntl_Mod_t *)Vec_PtrEntry( p->vModels, 0 );       } 
 
 static inline int         Ntl_ModelPiNum( Ntl_Mod_t * p )         { return p->nObjs[NTL_OBJ_PI];                } 
 static inline int         Ntl_ModelPoNum( Ntl_Mod_t * p )         { return p->nObjs[NTL_OBJ_PO];                } 
@@ -157,8 +167,8 @@ static inline int         Ntl_ModelBoxNum( Ntl_Mod_t * p )        { return p->nO
 static inline int         Ntl_ModelCiNum( Ntl_Mod_t * p )         { return p->nObjs[NTL_OBJ_PI] + p->nObjs[NTL_OBJ_LATCH]; } 
 static inline int         Ntl_ModelCoNum( Ntl_Mod_t * p )         { return p->nObjs[NTL_OBJ_PO] + p->nObjs[NTL_OBJ_LATCH]; } 
 
-static inline Ntl_Obj_t * Ntl_ModelPi( Ntl_Mod_t * p, int i )     { return Vec_PtrEntry(p->vPis, i);            } 
-static inline Ntl_Obj_t * Ntl_ModelPo( Ntl_Mod_t * p, int i )     { return Vec_PtrEntry(p->vPos, i);            } 
+static inline Ntl_Obj_t * Ntl_ModelPi( Ntl_Mod_t * p, int i )     { return (Ntl_Obj_t *)Vec_PtrEntry(p->vPis, i);            } 
+static inline Ntl_Obj_t * Ntl_ModelPo( Ntl_Mod_t * p, int i )     { return (Ntl_Obj_t *)Vec_PtrEntry(p->vPos, i);            } 
 
 static inline char *      Ntl_ModelPiName( Ntl_Mod_t * p, int i ) { return Ntl_ModelPi(p, i)->pFanio[0]->pName; } 
 static inline char *      Ntl_ModelPoName( Ntl_Mod_t * p, int i ) { return Ntl_ModelPo(p, i)->pFanio[0]->pName; } 
@@ -188,7 +198,7 @@ static inline void        Ntl_ObjSetFanout( Ntl_Obj_t * p, Ntl_Net_t * pNet, int
 ////////////////////////////////////////////////////////////////////////
 
 #define Ntl_ManForEachModel( p, pMod, i )                                       \
-    Vec_PtrForEachEntry( p->vModels, pMod, i )
+    for ( i = 0; (i < Vec_PtrSize(p->vModels)) && (((pMod) = (Ntl_Mod_t*)Vec_PtrEntry(p->vModels, i)), 1); i++ )
 #define Ntl_ManForEachCiNet( p, pNet, i )                                       \
     Vec_PtrForEachEntry( p->vCis, pNet, i )
 #define Ntl_ManForEachCoNet( p, pNet, i )                                       \
@@ -201,20 +211,20 @@ static inline void        Ntl_ObjSetFanout( Ntl_Obj_t * p, Ntl_Net_t * pNet, int
         if ( (pObj) == NULL || !Ntl_ObjIsBox(pObj) ) {} else
 
 #define Ntl_ModelForEachPi( pNwk, pObj, i )                                     \
-    Vec_PtrForEachEntry( pNwk->vPis, pObj, i )
+    for ( i = 0; (i < Vec_PtrSize(pNwk->vPis)) && (((pObj) = (Ntl_Obj_t*)Vec_PtrEntry(pNwk->vPis, i)), 1); i++ )
 #define Ntl_ModelForEachPo( pNwk, pObj, i )                                     \
-    Vec_PtrForEachEntry( pNwk->vPos, pObj, i )
+    for ( i = 0; (i < Vec_PtrSize(pNwk->vPos)) && (((pObj) = (Ntl_Obj_t*)Vec_PtrEntry(pNwk->vPos, i)), 1); i++ )
 #define Ntl_ModelForEachObj( pNwk, pObj, i )                                    \
-    for ( i = 0; (i < Vec_PtrSize(pNwk->vObjs)) && (((pObj) = Vec_PtrEntry(pNwk->vObjs, i)), 1); i++ ) \
+    for ( i = 0; (i < Vec_PtrSize(pNwk->vObjs)) && (((pObj) = (Ntl_Obj_t*)Vec_PtrEntry(pNwk->vObjs, i)), 1); i++ ) \
         if ( pObj == NULL ) {} else
 #define Ntl_ModelForEachLatch( pNwk, pObj, i )                                  \
-    for ( i = 0; (i < Vec_PtrSize(pNwk->vObjs)) && (((pObj) = Vec_PtrEntry(pNwk->vObjs, i)), 1); i++ ) \
-        if ( (pObj) == NULL || !Ntl_ObjIsLatch(pObj) ) {} else
+    for ( i = 0; (i < Vec_PtrSize(pNwk->vObjs)) && (((pObj) = (Ntl_Obj_t*)Vec_PtrEntry(pNwk->vObjs, i)), 1); i++ ) \
+        if ( (pObj) == NULL || !Ntl_ObjIsLatch((Ntl_Obj_t*)pObj) ) {} else
 #define Ntl_ModelForEachNode( pNwk, pObj, i )                                   \
-    for ( i = 0; (i < Vec_PtrSize(pNwk->vObjs)) && (((pObj) = Vec_PtrEntry(pNwk->vObjs, i)), 1); i++ ) \
+    for ( i = 0; (i < Vec_PtrSize(pNwk->vObjs)) && (((pObj) = (Ntl_Obj_t*)Vec_PtrEntry(pNwk->vObjs, i)), 1); i++ ) \
         if ( (pObj) == NULL || !Ntl_ObjIsNode(pObj) ) {} else
 #define Ntl_ModelForEachBox( pNwk, pObj, i )                                    \
-    for ( i = 0; (i < Vec_PtrSize(pNwk->vObjs)) && (((pObj) = Vec_PtrEntry(pNwk->vObjs, i)), 1); i++ ) \
+    for ( i = 0; (i < Vec_PtrSize(pNwk->vObjs)) && (((pObj) = (Ntl_Obj_t*)Vec_PtrEntry(pNwk->vObjs, i)), 1); i++ ) \
         if ( (pObj) == NULL || !Ntl_ObjIsBox(pObj) ) {} else
 #define Ntl_ModelForEachNet( pNwk, pNet, i )                                    \
     for ( i = 0; i < pNwk->nTableSize; i++ )                                    \
@@ -230,84 +240,84 @@ static inline void        Ntl_ObjSetFanout( Ntl_Obj_t * p, Ntl_Net_t * pNet, int
 ////////////////////////////////////////////////////////////////////////
 
 /*=== ntlCore.c ==========================================================*/
-extern int             Ntl_ManInsertTest( Ntl_Man_t * p, Aig_Man_t * pAig );
-extern int             Ntl_ManInsertTestIf( Ntl_Man_t * p, Aig_Man_t * pAig );
+extern ABC_DLL int             Ntl_ManInsertTest( Ntl_Man_t * p, Aig_Man_t * pAig );
+extern ABC_DLL int             Ntl_ManInsertTestIf( Ntl_Man_t * p, Aig_Man_t * pAig );
 /*=== ntlEc.c ==========================================================*/
-extern void            Ntl_ManPrepareCec( char * pFileName1, char * pFileName2, Aig_Man_t ** ppMan1, Aig_Man_t ** ppMan2 );
-extern Aig_Man_t *     Ntl_ManPrepareSec( char * pFileName1, char * pFileName2 );
+extern ABC_DLL void            Ntl_ManPrepareCec( char * pFileName1, char * pFileName2, Aig_Man_t ** ppMan1, Aig_Man_t ** ppMan2 );
+extern ABC_DLL Aig_Man_t *     Ntl_ManPrepareSec( char * pFileName1, char * pFileName2 );
 /*=== ntlExtract.c ==========================================================*/
-extern Aig_Man_t *     Ntl_ManExtract( Ntl_Man_t * p );
-extern Aig_Man_t *     Ntl_ManCollapse( Ntl_Man_t * p, int fSeq );
-extern Aig_Man_t *     Ntl_ManCollapseForCec( Ntl_Man_t * p );
-extern Aig_Man_t *     Ntl_ManCollapseForSec( Ntl_Man_t * p1, Ntl_Man_t * p2 );
+extern ABC_DLL Aig_Man_t *     Ntl_ManExtract( Ntl_Man_t * p );
+extern ABC_DLL Aig_Man_t *     Ntl_ManCollapse( Ntl_Man_t * p, int fSeq );
+extern ABC_DLL Aig_Man_t *     Ntl_ManCollapseForCec( Ntl_Man_t * p );
+extern ABC_DLL Aig_Man_t *     Ntl_ManCollapseForSec( Ntl_Man_t * p1, Ntl_Man_t * p2 );
 /*=== ntlInsert.c ==========================================================*/
-extern Ntl_Man_t *     Ntl_ManInsertMapping( Ntl_Man_t * p, Vec_Ptr_t * vMapping, Aig_Man_t * pAig );
-extern Ntl_Man_t *     Ntl_ManInsertAig( Ntl_Man_t * p, Aig_Man_t * pAig );
-extern Ntl_Man_t *     Ntl_ManInsertNtk( Ntl_Man_t * p, Nwk_Man_t * pNtk );
+extern ABC_DLL Ntl_Man_t *     Ntl_ManInsertMapping( Ntl_Man_t * p, Vec_Ptr_t * vMapping, Aig_Man_t * pAig );
+extern ABC_DLL Ntl_Man_t *     Ntl_ManInsertAig( Ntl_Man_t * p, Aig_Man_t * pAig );
+extern ABC_DLL Ntl_Man_t *     Ntl_ManInsertNtk( Ntl_Man_t * p, Nwk_Man_t * pNtk );
 /*=== ntlCheck.c ==========================================================*/
-extern int             Ntl_ManCheck( Ntl_Man_t * pMan );
-extern int             Ntl_ModelCheck( Ntl_Mod_t * pModel );
-extern void            Ntl_ModelFixNonDrivenNets( Ntl_Mod_t * pModel );
+extern ABC_DLL int             Ntl_ManCheck( Ntl_Man_t * pMan );
+extern ABC_DLL int             Ntl_ModelCheck( Ntl_Mod_t * pModel );
+extern ABC_DLL void            Ntl_ModelFixNonDrivenNets( Ntl_Mod_t * pModel );
 /*=== ntlMan.c ============================================================*/
-extern Ntl_Man_t *     Ntl_ManAlloc();
-extern void            Ntl_ManCleanup( Ntl_Man_t * p );
-extern Ntl_Man_t *     Ntl_ManStartFrom( Ntl_Man_t * p );
-extern Ntl_Man_t *     Ntl_ManDup( Ntl_Man_t * p );
-extern void            Ntl_ManFree( Ntl_Man_t * p );
-extern int             Ntl_ManIsComb( Ntl_Man_t * p );
-extern int             Ntl_ManLatchNum( Ntl_Man_t * p );
-extern Ntl_Mod_t *     Ntl_ManFindModel( Ntl_Man_t * p, char * pName );
-extern void            Ntl_ManPrintStats( Ntl_Man_t * p );
-extern Tim_Man_t *     Ntl_ManReadTimeMan( Ntl_Man_t * p );
-extern Ntl_Mod_t *     Ntl_ModelAlloc( Ntl_Man_t * pMan, char * pName );
-extern Ntl_Mod_t *     Ntl_ModelStartFrom( Ntl_Man_t * pManNew, Ntl_Mod_t * pModelOld );
-extern Ntl_Mod_t *     Ntl_ModelDup( Ntl_Man_t * pManNew, Ntl_Mod_t * pModelOld );
-extern void            Ntl_ModelFree( Ntl_Mod_t * p );
+extern ABC_DLL Ntl_Man_t *     Ntl_ManAlloc();
+extern ABC_DLL void            Ntl_ManCleanup( Ntl_Man_t * p );
+extern ABC_DLL Ntl_Man_t *     Ntl_ManStartFrom( Ntl_Man_t * p );
+extern ABC_DLL Ntl_Man_t *     Ntl_ManDup( Ntl_Man_t * p );
+extern ABC_DLL void            Ntl_ManFree( Ntl_Man_t * p );
+extern ABC_DLL int             Ntl_ManIsComb( Ntl_Man_t * p );
+extern ABC_DLL int             Ntl_ManLatchNum( Ntl_Man_t * p );
+extern ABC_DLL Ntl_Mod_t *     Ntl_ManFindModel( Ntl_Man_t * p, char * pName );
+extern ABC_DLL void            Ntl_ManPrintStats( Ntl_Man_t * p );
+extern ABC_DLL Tim_Man_t *     Ntl_ManReadTimeMan( Ntl_Man_t * p );
+extern ABC_DLL Ntl_Mod_t *     Ntl_ModelAlloc( Ntl_Man_t * pMan, char * pName );
+extern ABC_DLL Ntl_Mod_t *     Ntl_ModelStartFrom( Ntl_Man_t * pManNew, Ntl_Mod_t * pModelOld );
+extern ABC_DLL Ntl_Mod_t *     Ntl_ModelDup( Ntl_Man_t * pManNew, Ntl_Mod_t * pModelOld );
+extern ABC_DLL void            Ntl_ModelFree( Ntl_Mod_t * p );
 /*=== ntlMap.c ============================================================*/
-extern Vec_Ptr_t *     Ntl_MappingAlloc( int nLuts, int nVars );
-extern Vec_Ptr_t *     Ntl_MappingFromAig( Aig_Man_t * p );
-extern Vec_Ptr_t *     Ntl_MappingFpga( Aig_Man_t * p );
-extern Vec_Ptr_t *     Ntl_MappingIf( Ntl_Man_t * pMan, Aig_Man_t * p );
+extern ABC_DLL Vec_Ptr_t *     Ntl_MappingAlloc( int nLuts, int nVars );
+extern ABC_DLL Vec_Ptr_t *     Ntl_MappingFromAig( Aig_Man_t * p );
+extern ABC_DLL Vec_Ptr_t *     Ntl_MappingFpga( Aig_Man_t * p );
+extern ABC_DLL Vec_Ptr_t *     Ntl_MappingIf( Ntl_Man_t * pMan, Aig_Man_t * p );
 /*=== ntlObj.c ============================================================*/
-extern Ntl_Obj_t *     Ntl_ModelCreatePi( Ntl_Mod_t * pModel );
-extern Ntl_Obj_t *     Ntl_ModelCreatePo( Ntl_Mod_t * pModel, Ntl_Net_t * pNet );
-extern Ntl_Obj_t *     Ntl_ModelCreateLatch( Ntl_Mod_t * pModel );
-extern Ntl_Obj_t *     Ntl_ModelCreateNode( Ntl_Mod_t * pModel, int nFanins );
-extern Ntl_Obj_t *     Ntl_ModelCreateBox( Ntl_Mod_t * pModel, int nFanins, int nFanouts );
-extern Ntl_Obj_t *     Ntl_ModelDupObj( Ntl_Mod_t * pModel, Ntl_Obj_t * pOld );
-extern Ntl_Obj_t *     Ntl_ModelCreatePiWithName( Ntl_Mod_t * pModel, char * pName );
-extern char *          Ntl_ManStoreName( Ntl_Man_t * p, char * pName );
-extern char *          Ntl_ManStoreSop( Aig_MmFlex_t * pMan, char * pSop );
-extern char *          Ntl_ManStoreFileName( Ntl_Man_t * p, char * pFileName );
+extern ABC_DLL Ntl_Obj_t *     Ntl_ModelCreatePi( Ntl_Mod_t * pModel );
+extern ABC_DLL Ntl_Obj_t *     Ntl_ModelCreatePo( Ntl_Mod_t * pModel, Ntl_Net_t * pNet );
+extern ABC_DLL Ntl_Obj_t *     Ntl_ModelCreateLatch( Ntl_Mod_t * pModel );
+extern ABC_DLL Ntl_Obj_t *     Ntl_ModelCreateNode( Ntl_Mod_t * pModel, int nFanins );
+extern ABC_DLL Ntl_Obj_t *     Ntl_ModelCreateBox( Ntl_Mod_t * pModel, int nFanins, int nFanouts );
+extern ABC_DLL Ntl_Obj_t *     Ntl_ModelDupObj( Ntl_Mod_t * pModel, Ntl_Obj_t * pOld );
+extern ABC_DLL Ntl_Obj_t *     Ntl_ModelCreatePiWithName( Ntl_Mod_t * pModel, char * pName );
+extern ABC_DLL char *          Ntl_ManStoreName( Ntl_Man_t * p, char * pName );
+extern ABC_DLL char *          Ntl_ManStoreSop( Aig_MmFlex_t * pMan, char * pSop );
+extern ABC_DLL char *          Ntl_ManStoreFileName( Ntl_Man_t * p, char * pFileName );
 /*=== ntlSweep.c ==========================================================*/
-extern int             Ntl_ManSweep( Ntl_Man_t * p, int fVerbose );
+extern ABC_DLL int             Ntl_ManSweep( Ntl_Man_t * p, int fVerbose );
 /*=== ntlTable.c ==========================================================*/
-extern Ntl_Net_t *     Ntl_ModelFindNet( Ntl_Mod_t * p, char * pName );
-extern Ntl_Net_t *     Ntl_ModelFindOrCreateNet( Ntl_Mod_t * p, char * pName );
-extern int             Ntl_ModelFindPioNumber( Ntl_Mod_t * p, char * pName, int * pNumber );
-extern int             Ntl_ModelSetNetDriver( Ntl_Obj_t * pObj, Ntl_Net_t * pNet );
-extern int             Ntl_ModelClearNetDriver( Ntl_Obj_t * pObj, Ntl_Net_t * pNet );
-extern void            Ntl_ModelDeleteNet( Ntl_Mod_t * p, Ntl_Net_t * pNet );
-extern int             Ntl_ModelCountNets( Ntl_Mod_t * p );
+extern ABC_DLL Ntl_Net_t *     Ntl_ModelFindNet( Ntl_Mod_t * p, char * pName );
+extern ABC_DLL Ntl_Net_t *     Ntl_ModelFindOrCreateNet( Ntl_Mod_t * p, char * pName );
+extern ABC_DLL int             Ntl_ModelFindPioNumber( Ntl_Mod_t * p, char * pName, int * pNumber );
+extern ABC_DLL int             Ntl_ModelSetNetDriver( Ntl_Obj_t * pObj, Ntl_Net_t * pNet );
+extern ABC_DLL int             Ntl_ModelClearNetDriver( Ntl_Obj_t * pObj, Ntl_Net_t * pNet );
+extern ABC_DLL void            Ntl_ModelDeleteNet( Ntl_Mod_t * p, Ntl_Net_t * pNet );
+extern ABC_DLL int             Ntl_ModelCountNets( Ntl_Mod_t * p );
 /*=== ntlTime.c ==========================================================*/
-extern Tim_Man_t *     Ntl_ManCreateTiming( Ntl_Man_t * p );
+extern ABC_DLL Tim_Man_t *     Ntl_ManCreateTiming( Ntl_Man_t * p );
 /*=== ntlReadBlif.c ==========================================================*/
-extern Ntl_Man_t *     Ioa_ReadBlif( char * pFileName, int fCheck );
+extern ABC_DLL Ntl_Man_t *     Ioa_ReadBlif( char * pFileName, int fCheck );
 /*=== ntlWriteBlif.c ==========================================================*/
-extern void            Ioa_WriteBlif( Ntl_Man_t * p, char * pFileName );
-extern void            Ioa_WriteBlifLogic( Nwk_Man_t * pNtk, Ntl_Man_t * p, char * pFileName );
+extern ABC_DLL void            Ioa_WriteBlif( Ntl_Man_t * p, char * pFileName );
+extern ABC_DLL void            Ioa_WriteBlifLogic( Nwk_Man_t * pNtk, Ntl_Man_t * p, char * pFileName );
 /*=== ntlUtil.c ==========================================================*/
-extern int             Ntl_ModelCountLut1( Ntl_Mod_t * pRoot );
-extern int             Ntl_ModelGetFaninMax( Ntl_Mod_t * pRoot );
-extern Ntl_Net_t *     Ntl_ModelFindSimpleNet( Ntl_Net_t * pNetCo );
-extern int             Ntl_ManCountSimpleCoDrivers( Ntl_Man_t * p );
-extern Vec_Ptr_t *     Ntl_ManCollectCiNames( Ntl_Man_t * p );
-extern Vec_Ptr_t *     Ntl_ManCollectCoNames( Ntl_Man_t * p );
-extern void            Ntl_ManMarkCiCoNets( Ntl_Man_t * p );
-extern void            Ntl_ManUnmarkCiCoNets( Ntl_Man_t * p );
-extern int             Ntl_ManCheckNetsAreNotMarked( Ntl_Mod_t * pModel );
-extern void            Ntl_ManSetZeroInitValues( Ntl_Man_t * p );
-extern void            Ntl_ManTransformInitValues( Ntl_Man_t * p );
+extern ABC_DLL int             Ntl_ModelCountLut1( Ntl_Mod_t * pRoot );
+extern ABC_DLL int             Ntl_ModelGetFaninMax( Ntl_Mod_t * pRoot );
+extern ABC_DLL Ntl_Net_t *     Ntl_ModelFindSimpleNet( Ntl_Net_t * pNetCo );
+extern ABC_DLL int             Ntl_ManCountSimpleCoDrivers( Ntl_Man_t * p );
+extern ABC_DLL Vec_Ptr_t *     Ntl_ManCollectCiNames( Ntl_Man_t * p );
+extern ABC_DLL Vec_Ptr_t *     Ntl_ManCollectCoNames( Ntl_Man_t * p );
+extern ABC_DLL void            Ntl_ManMarkCiCoNets( Ntl_Man_t * p );
+extern ABC_DLL void            Ntl_ManUnmarkCiCoNets( Ntl_Man_t * p );
+extern ABC_DLL int             Ntl_ManCheckNetsAreNotMarked( Ntl_Mod_t * pModel );
+extern ABC_DLL void            Ntl_ManSetZeroInitValues( Ntl_Man_t * p );
+extern ABC_DLL void            Ntl_ManTransformInitValues( Ntl_Man_t * p );
 
 #ifdef __cplusplus
 }
diff --git a/src/aig/nwk/nwk.h b/src/aig/nwk/nwk.h
index b0edd243..6c78ca87 100644
--- a/src/aig/nwk/nwk.h
+++ b/src/aig/nwk/nwk.h
@@ -14,7 +14,7 @@
 
   Date        [Ver. 1.0. Started - June 20, 2005.]
 
-  Revision    [$Id: nwk.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+  Revision    [$Id: nwk.h,v 1.1 2008/05/14 22:13:09 wudenni Exp $]
 
 ***********************************************************************/
  
@@ -29,6 +29,8 @@ extern "C" {
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
 
+#pragma warning( disable : 4273 )
+
 #include "aig.h"
 #include "hop.h"
 #include "tim.h"
@@ -117,6 +119,16 @@ struct Nwk_Obj_t_
 ////////////////////////////////////////////////////////////////////////
 ///                      INLINED FUNCTIONS                           ///
 ////////////////////////////////////////////////////////////////////////
+#ifdef WIN32
+#define DLLEXPORT __declspec(dllexport)
+#define DLLIMPORT __declspec(dllimport)
+#else  /* defined(WIN32) */
+#define DLLIMPORT
+#endif /* defined(WIN32) */
+
+#ifndef ABC_DLL
+#define ABC_DLL DLLIMPORT
+#endif
 
 static inline int         Nwk_ManCiNum( Nwk_Man_t * p )           { return p->nObjs[NWK_OBJ_CI];                } 
 static inline int         Nwk_ManCoNum( Nwk_Man_t * p )           { return p->nObjs[NWK_OBJ_CO];                } 
@@ -124,9 +136,9 @@ static inline int         Nwk_ManNodeNum( Nwk_Man_t * p )         { return p->nO
 static inline int         Nwk_ManLatchNum( Nwk_Man_t * p )        { return p->nObjs[NWK_OBJ_LATCH];             } 
 static inline int         Nwk_ManObjNumMax( Nwk_Man_t * p )       { return Vec_PtrSize(p->vObjs);               }
 
-static inline Nwk_Obj_t * Nwk_ManCi( Nwk_Man_t * p, int i )       { return Vec_PtrEntry( p->vCis, i );          } 
-static inline Nwk_Obj_t * Nwk_ManCo( Nwk_Man_t * p, int i )       { return Vec_PtrEntry( p->vCos, i );          } 
-static inline Nwk_Obj_t * Nwk_ManObj( Nwk_Man_t * p, int i )      { return Vec_PtrEntry( p->vObjs, i );         } 
+static inline Nwk_Obj_t * Nwk_ManCi( Nwk_Man_t * p, int i )       { return (Nwk_Obj_t *)Vec_PtrEntry( p->vCis, i );          } 
+static inline Nwk_Obj_t * Nwk_ManCo( Nwk_Man_t * p, int i )       { return (Nwk_Obj_t *)Vec_PtrEntry( p->vCos, i );          } 
+static inline Nwk_Obj_t * Nwk_ManObj( Nwk_Man_t * p, int i )      { return (Nwk_Obj_t *)Vec_PtrEntry( p->vObjs, i );         } 
 
 static inline int         Nwk_ObjId( Nwk_Obj_t * p )              { return p->Id;                               } 
 static inline int         Nwk_ObjPioNum( Nwk_Obj_t * p )          { return p->PioId;                            } 
@@ -216,76 +228,76 @@ static inline int         Nwk_ManTimeMore( float f1, float f2, float Eps )   { r
 ////////////////////////////////////////////////////////////////////////
 
 /*=== nwkAig.c ==========================================================*/
-extern Vec_Ptr_t *     Nwk_ManDeriveRetimingCut( Aig_Man_t * p, int fForward, int fVerbose );
+extern ABC_DLL Vec_Ptr_t *     Nwk_ManDeriveRetimingCut( Aig_Man_t * p, int fForward, int fVerbose );
 /*=== nwkBidec.c ==========================================================*/
-extern void            Nwk_ManBidecResyn( Nwk_Man_t * pNtk, int fVerbose );
-extern Hop_Obj_t *     Nwk_NodeIfNodeResyn( Bdc_Man_t * p, Hop_Man_t * pHop, Hop_Obj_t * pRoot, int nVars, Vec_Int_t * vTruth, unsigned * puCare );
+extern ABC_DLL void            Nwk_ManBidecResyn( Nwk_Man_t * pNtk, int fVerbose );
+extern ABC_DLL Hop_Obj_t *     Nwk_NodeIfNodeResyn( Bdc_Man_t * p, Hop_Man_t * pHop, Hop_Obj_t * pRoot, int nVars, Vec_Int_t * vTruth, unsigned * puCare );
 /*=== nwkCheck.c ==========================================================*/
-extern int             Nwk_ManCheck( Nwk_Man_t * p );
+extern ABC_DLL int             Nwk_ManCheck( Nwk_Man_t * p );
 /*=== nwkDfs.c ==========================================================*/
-extern int             Nwk_ManVerifyTopoOrder( Nwk_Man_t * pNtk );
-extern int             Nwk_ManLevelBackup( Nwk_Man_t * pNtk );
-extern int             Nwk_ManLevel( Nwk_Man_t * pNtk );
-extern int             Nwk_ManLevelMax( Nwk_Man_t * pNtk );
-extern Vec_Vec_t *     Nwk_ManLevelize( Nwk_Man_t * pNtk );
-extern Vec_Ptr_t *     Nwk_ManDfs( Nwk_Man_t * pNtk );
-extern Vec_Ptr_t *     Nwk_ManDfsNodes( Nwk_Man_t * pNtk, Nwk_Obj_t ** ppNodes, int nNodes );
-extern Vec_Ptr_t *     Nwk_ManDfsReverse( Nwk_Man_t * pNtk );
-extern Vec_Ptr_t *     Nwk_ManSupportNodes( Nwk_Man_t * pNtk, Nwk_Obj_t ** ppNodes, int nNodes );
-extern void            Nwk_ManSupportSum( Nwk_Man_t * pNtk );
-extern int             Nwk_ObjMffcLabel( Nwk_Obj_t * pNode );
+extern ABC_DLL int             Nwk_ManVerifyTopoOrder( Nwk_Man_t * pNtk );
+extern ABC_DLL int             Nwk_ManLevelBackup( Nwk_Man_t * pNtk );
+extern ABC_DLL int             Nwk_ManLevel( Nwk_Man_t * pNtk );
+extern ABC_DLL int             Nwk_ManLevelMax( Nwk_Man_t * pNtk );
+extern ABC_DLL Vec_Vec_t *     Nwk_ManLevelize( Nwk_Man_t * pNtk );
+extern ABC_DLL Vec_Ptr_t *     Nwk_ManDfs( Nwk_Man_t * pNtk );
+extern ABC_DLL Vec_Ptr_t *     Nwk_ManDfsNodes( Nwk_Man_t * pNtk, Nwk_Obj_t ** ppNodes, int nNodes );
+extern ABC_DLL Vec_Ptr_t *     Nwk_ManDfsReverse( Nwk_Man_t * pNtk );
+extern ABC_DLL Vec_Ptr_t *     Nwk_ManSupportNodes( Nwk_Man_t * pNtk, Nwk_Obj_t ** ppNodes, int nNodes );
+extern ABC_DLL void            Nwk_ManSupportSum( Nwk_Man_t * pNtk );
+extern ABC_DLL int             Nwk_ObjMffcLabel( Nwk_Obj_t * pNode );
 /*=== nwkFanio.c ==========================================================*/
-extern void            Nwk_ObjCollectFanins( Nwk_Obj_t * pNode, Vec_Ptr_t * vNodes );
-extern void            Nwk_ObjCollectFanouts( Nwk_Obj_t * pNode, Vec_Ptr_t * vNodes );
-extern int             Nwk_ObjFindFanin( Nwk_Obj_t * pObj, Nwk_Obj_t * pFanin );
-extern int             Nwk_ObjFindFanout( Nwk_Obj_t * pObj, Nwk_Obj_t * pFanout );
-extern void            Nwk_ObjAddFanin( Nwk_Obj_t * pObj, Nwk_Obj_t * pFanin );
-extern void            Nwk_ObjDeleteFanin( Nwk_Obj_t * pObj, Nwk_Obj_t * pFanin );
-extern void            Nwk_ObjPatchFanin( Nwk_Obj_t * pObj, Nwk_Obj_t * pFaninOld, Nwk_Obj_t * pFaninNew );
-extern void            Nwk_ObjTransferFanout( Nwk_Obj_t * pNodeFrom, Nwk_Obj_t * pNodeTo );
-extern void            Nwk_ObjReplace( Nwk_Obj_t * pNodeOld, Nwk_Obj_t * pNodeNew );
+extern ABC_DLL void            Nwk_ObjCollectFanins( Nwk_Obj_t * pNode, Vec_Ptr_t * vNodes );
+extern ABC_DLL void            Nwk_ObjCollectFanouts( Nwk_Obj_t * pNode, Vec_Ptr_t * vNodes );
+extern ABC_DLL int             Nwk_ObjFindFanin( Nwk_Obj_t * pObj, Nwk_Obj_t * pFanin );
+extern ABC_DLL int             Nwk_ObjFindFanout( Nwk_Obj_t * pObj, Nwk_Obj_t * pFanout );
+extern ABC_DLL void            Nwk_ObjAddFanin( Nwk_Obj_t * pObj, Nwk_Obj_t * pFanin );
+extern ABC_DLL void            Nwk_ObjDeleteFanin( Nwk_Obj_t * pObj, Nwk_Obj_t * pFanin );
+extern ABC_DLL void            Nwk_ObjPatchFanin( Nwk_Obj_t * pObj, Nwk_Obj_t * pFaninOld, Nwk_Obj_t * pFaninNew );
+extern ABC_DLL void            Nwk_ObjTransferFanout( Nwk_Obj_t * pNodeFrom, Nwk_Obj_t * pNodeTo );
+extern ABC_DLL void            Nwk_ObjReplace( Nwk_Obj_t * pNodeOld, Nwk_Obj_t * pNodeNew );
 /*=== nwkFlow.c ============================================================*/
-extern Vec_Ptr_t *     Nwk_ManRetimeCutForward( Nwk_Man_t * pMan, int nLatches, int fVerbose );
-extern Vec_Ptr_t *     Nwk_ManRetimeCutBackward( Nwk_Man_t * pMan, int nLatches, int fVerbose );
+extern ABC_DLL Vec_Ptr_t *     Nwk_ManRetimeCutForward( Nwk_Man_t * pMan, int nLatches, int fVerbose );
+extern ABC_DLL Vec_Ptr_t *     Nwk_ManRetimeCutBackward( Nwk_Man_t * pMan, int nLatches, int fVerbose );
 /*=== nwkMan.c ============================================================*/
-extern Nwk_Man_t *     Nwk_ManAlloc();
-extern void            Nwk_ManFree( Nwk_Man_t * p );
-extern void            Nwk_ManPrintStats( Nwk_Man_t * p, If_Lib_t * pLutLib, int fSaveBest, int fDumpResult, void * pNtl );
+extern ABC_DLL Nwk_Man_t *     Nwk_ManAlloc();
+extern ABC_DLL void            Nwk_ManFree( Nwk_Man_t * p );
+extern ABC_DLL void            Nwk_ManPrintStats( Nwk_Man_t * p, If_Lib_t * pLutLib, int fSaveBest, int fDumpResult, void * pNtl );
 /*=== nwkMap.c ============================================================*/
-extern Nwk_Man_t *     Nwk_MappingIf( Aig_Man_t * p, Tim_Man_t * pManTime, If_Par_t * pPars );
+extern ABC_DLL Nwk_Man_t *     Nwk_MappingIf( Aig_Man_t * p, Tim_Man_t * pManTime, If_Par_t * pPars );
 /*=== nwkObj.c ============================================================*/
-extern Nwk_Obj_t *     Nwk_ManCreateCi( Nwk_Man_t * pMan, int nFanouts );
-extern Nwk_Obj_t *     Nwk_ManCreateCo( Nwk_Man_t * pMan );
-extern Nwk_Obj_t *     Nwk_ManCreateNode( Nwk_Man_t * pMan, int nFanins, int nFanouts );
-extern Nwk_Obj_t *     Nwk_ManCreateBox( Nwk_Man_t * pMan, int nFanins, int nFanouts );
-extern Nwk_Obj_t *     Nwk_ManCreateLatch( Nwk_Man_t * pMan );
-extern void            Nwk_ManDeleteNode( Nwk_Obj_t * pObj );
-extern void            Nwk_ManDeleteNode_rec( Nwk_Obj_t * pObj );
+extern ABC_DLL Nwk_Obj_t *     Nwk_ManCreateCi( Nwk_Man_t * pMan, int nFanouts );
+extern ABC_DLL Nwk_Obj_t *     Nwk_ManCreateCo( Nwk_Man_t * pMan );
+extern ABC_DLL Nwk_Obj_t *     Nwk_ManCreateNode( Nwk_Man_t * pMan, int nFanins, int nFanouts );
+extern ABC_DLL Nwk_Obj_t *     Nwk_ManCreateBox( Nwk_Man_t * pMan, int nFanins, int nFanouts );
+extern ABC_DLL Nwk_Obj_t *     Nwk_ManCreateLatch( Nwk_Man_t * pMan );
+extern ABC_DLL void            Nwk_ManDeleteNode( Nwk_Obj_t * pObj );
+extern ABC_DLL void            Nwk_ManDeleteNode_rec( Nwk_Obj_t * pObj );
 /*=== nwkSpeedup.c ============================================================*/
-extern Aig_Man_t *     Nwk_ManSpeedup( Nwk_Man_t * pNtk, int fUseLutLib, int Percentage, int Degree, int fVerbose, int fVeryVerbose );
+extern ABC_DLL Aig_Man_t *     Nwk_ManSpeedup( Nwk_Man_t * pNtk, int fUseLutLib, int Percentage, int Degree, int fVerbose, int fVeryVerbose );
 /*=== nwkStrash.c ============================================================*/
-extern Aig_Man_t *     Nwk_ManStrash( Nwk_Man_t * pNtk );
+extern ABC_DLL Aig_Man_t *     Nwk_ManStrash( Nwk_Man_t * pNtk );
 /*=== nwkTiming.c ============================================================*/
-extern int             Nwk_ManVerifyTiming(  Nwk_Man_t * pNtk );
-extern void            Nwk_ManDelayTraceSortPins( Nwk_Obj_t * pNode, int * pPinPerm, float * pPinDelays );
-extern float           Nwk_ManDelayTraceLut( Nwk_Man_t * pNtk );
-extern void            Nwk_ManDelayTracePrint( Nwk_Man_t * pNtk );
-extern void            Nwk_ManUpdate( Nwk_Obj_t * pObj, Nwk_Obj_t * pObjNew, Vec_Vec_t * vLevels );
-extern int             Nwk_ManVerifyLevel( Nwk_Man_t * pNtk );
+extern ABC_DLL int             Nwk_ManVerifyTiming(  Nwk_Man_t * pNtk );
+extern ABC_DLL void            Nwk_ManDelayTraceSortPins( Nwk_Obj_t * pNode, int * pPinPerm, float * pPinDelays );
+extern ABC_DLL float           Nwk_ManDelayTraceLut( Nwk_Man_t * pNtk );
+extern ABC_DLL void            Nwk_ManDelayTracePrint( Nwk_Man_t * pNtk );
+extern ABC_DLL void            Nwk_ManUpdate( Nwk_Obj_t * pObj, Nwk_Obj_t * pObjNew, Vec_Vec_t * vLevels );
+extern ABC_DLL int             Nwk_ManVerifyLevel( Nwk_Man_t * pNtk );
 /*=== nwkUtil.c ============================================================*/
-extern void            Nwk_ManIncrementTravId( Nwk_Man_t * pNtk );
-extern int             Nwk_ManGetFaninMax( Nwk_Man_t * pNtk );
-extern int             Nwk_ManGetTotalFanins( Nwk_Man_t * pNtk );
-extern int             Nwk_ManPiNum( Nwk_Man_t * pNtk );
-extern int             Nwk_ManPoNum( Nwk_Man_t * pNtk );
-extern int             Nwk_ManGetAigNodeNum( Nwk_Man_t * pNtk );
-extern int             Nwk_NodeCompareLevelsIncrease( Nwk_Obj_t ** pp1, Nwk_Obj_t ** pp2 );
-extern int             Nwk_NodeCompareLevelsDecrease( Nwk_Obj_t ** pp1, Nwk_Obj_t ** pp2 );
-extern void            Nwk_ObjPrint( Nwk_Obj_t * pObj );
-extern void            Nwk_ManDumpBlif( Nwk_Man_t * pNtk, char * pFileName, Vec_Ptr_t * vCiNames, Vec_Ptr_t * vCoNames );
-extern void            Nwk_ManPrintFanioNew( Nwk_Man_t * pNtk );
-extern void            Nwk_ManCleanMarks( Nwk_Man_t * pNtk );
-extern void            Nwk_ManMinimumBase( Nwk_Man_t * pNtk, int fVerbose );
+extern ABC_DLL void            Nwk_ManIncrementTravId( Nwk_Man_t * pNtk );
+extern ABC_DLL int             Nwk_ManGetFaninMax( Nwk_Man_t * pNtk );
+extern ABC_DLL int             Nwk_ManGetTotalFanins( Nwk_Man_t * pNtk );
+extern ABC_DLL int             Nwk_ManPiNum( Nwk_Man_t * pNtk );
+extern ABC_DLL int             Nwk_ManPoNum( Nwk_Man_t * pNtk );
+extern ABC_DLL int             Nwk_ManGetAigNodeNum( Nwk_Man_t * pNtk );
+extern ABC_DLL int             Nwk_NodeCompareLevelsIncrease( Nwk_Obj_t ** pp1, Nwk_Obj_t ** pp2 );
+extern ABC_DLL int             Nwk_NodeCompareLevelsDecrease( Nwk_Obj_t ** pp1, Nwk_Obj_t ** pp2 );
+extern ABC_DLL void            Nwk_ObjPrint( Nwk_Obj_t * pObj );
+extern ABC_DLL void            Nwk_ManDumpBlif( Nwk_Man_t * pNtk, char * pFileName, Vec_Ptr_t * vCiNames, Vec_Ptr_t * vCoNames );
+extern ABC_DLL void            Nwk_ManPrintFanioNew( Nwk_Man_t * pNtk );
+extern ABC_DLL void            Nwk_ManCleanMarks( Nwk_Man_t * pNtk );
+extern ABC_DLL void            Nwk_ManMinimumBase( Nwk_Man_t * pNtk, int fVerbose );
 
 #ifdef __cplusplus
 }
diff --git a/src/aig/saig/module.make b/src/aig/saig/module.make
index 68c49133..ea122bbf 100644
--- a/src/aig/saig/module.make
+++ b/src/aig/saig/module.make
@@ -1,8 +1,10 @@
 SRC +=    src/aig/saig/saigBmc.c \
     src/aig/saig/saigCone.c \
     src/aig/saig/saigInter.c \
+    src/aig/saig/saigIoa.c \
     src/aig/saig/saigPhase.c \
     src/aig/saig/saigRetFwd.c \
     src/aig/saig/saigRetMin.c \
     src/aig/saig/saigRetStep.c \
-    src/aig/saig/saigScl.c
+    src/aig/saig/saigScl.c \
+    src/aig/saig/saigTrans.c
diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h
index b9b7de40..c8efab40 100644
--- a/src/aig/saig/saig.h
+++ b/src/aig/saig/saig.h
@@ -79,6 +79,9 @@ static inline int          Saig_ObjIsLi( Aig_Man_t * p, Aig_Obj_t * pObj )    {
 extern int               Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nBTLimit, int fRewrite, int fVerbose, int * piFrame );
 /*=== saigCone.c ==========================================================*/
 extern void              Saig_ManPrintCones( Aig_Man_t * p );
+/*=== saigIoa.c ==========================================================*/
+extern void              Saig_ManDumpBlif( Aig_Man_t * p, char * pFileName );
+extern Aig_Man_t *       Saig_ManReadBlif( char * pFileName );
 /*=== saigInter.c ==========================================================*/
 extern int               Saig_Interpolate( Aig_Man_t * pAig, int nConfLimit, int fRewrite, int fTransLoop, int fVerbose, int * pDepth );
 /*=== saigPhase.c ==========================================================*/
@@ -92,6 +95,8 @@ extern Aig_Man_t *       Saig_ManRetimeMinArea( Aig_Man_t * p, int nMaxIters, in
 extern void              Saig_ManRetimeSteps( Aig_Man_t * p, int nSteps, int fForward );
 /*=== saigScl.c ==========================================================*/
 extern void              Saig_ManReportUselessRegisters( Aig_Man_t * pAig );
+/*=== saigTrans.c ==========================================================*/
+extern Aig_Man_t *       Saig_ManTimeframeSimplify( Aig_Man_t * pAig, int nFrames, int nFramesMax, int fInit, int fVerbose );
 
 #ifdef __cplusplus
 }
diff --git a/src/aig/saig/saigIoa.c b/src/aig/saig/saigIoa.c
new file mode 100644
index 00000000..70870fe9
--- /dev/null
+++ b/src/aig/saig/saigIoa.c
@@ -0,0 +1,399 @@
+/**CFile****************************************************************
+
+  FileName    [saigIoa.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Sequential AIG package.]
+
+  Synopsis    [Input/output for sequential AIGs using BLIF files.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: saigIoa.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "saig.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Saig_ObjName( Aig_Man_t * p, Aig_Obj_t * pObj )
+{
+    static char Buffer[16];
+    if ( Aig_ObjIsNode(pObj) || Aig_ObjIsConst1(pObj) )
+        sprintf( Buffer, "n%0*d", Aig_Base10Log(Aig_ManObjNumMax(p)), Aig_ObjId(pObj) );
+    else if ( Saig_ObjIsPi(p, pObj) )
+        sprintf( Buffer, "pi%0*d", Aig_Base10Log(Saig_ManPiNum(p)), Aig_ObjPioNum(pObj) );
+    else if ( Saig_ObjIsPo(p, pObj) )
+        sprintf( Buffer, "po%0*d", Aig_Base10Log(Saig_ManPoNum(p)), Aig_ObjPioNum(pObj) );
+    else if ( Saig_ObjIsLo(p, pObj) )
+        sprintf( Buffer, "lo%0*d", Aig_Base10Log(Saig_ManRegNum(p)), Aig_ObjPioNum(pObj) - Saig_ManPiNum(p) );
+    else if ( Saig_ObjIsLi(p, pObj) )
+        sprintf( Buffer, "li%0*d", Aig_Base10Log(Saig_ManRegNum(p)), Aig_ObjPioNum(pObj) - Saig_ManPoNum(p) );
+    else 
+        assert( 0 );
+    return Buffer;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Saig_ManDumpBlif( Aig_Man_t * p, char * pFileName )
+{
+    FILE * pFile;
+    Aig_Obj_t * pObj, * pObjLi, * pObjLo;
+    int i;
+    if ( Aig_ManPoNum(p) == 0 )
+    {
+        printf( "Aig_ManDumpBlif(): AIG manager does not have POs.\n" );
+        return;
+    }
+    Aig_ManSetPioNumbers( p );
+    // write input file
+    pFile = fopen( pFileName, "w" );
+    if ( pFile == NULL )
+    {
+        printf( "Saig_ManDumpBlif(): Cannot open file for writing.\n" );
+        return;
+    }
+    fprintf( pFile, "# BLIF file written by procedure Saig_ManDumpBlif()\n" );
+    fprintf( pFile, "# If unedited, this file can be read by Saig_ManReadBlif()\n" );
+    fprintf( pFile, "# AIG stats: pi=%d po=%d reg=%d and=%d obj=%d maxid=%d\n", 
+        Saig_ManPiNum(p), Saig_ManPoNum(p), Saig_ManRegNum(p), 
+        Aig_ManNodeNum(p), Aig_ManObjNum(p), Aig_ManObjNumMax(p) );
+    fprintf( pFile, ".model %s\n", p->pName );
+    // write primary inputs
+    fprintf( pFile, ".inputs" );
+    Aig_ManForEachPiSeq( p, pObj, i )
+        fprintf( pFile, " %s", Saig_ObjName(p, pObj) );
+    fprintf( pFile, "\n" );
+    // write primary outputs
+    fprintf( pFile, ".outputs" );
+    Aig_ManForEachPoSeq( p, pObj, i )
+        fprintf( pFile, " %s", Saig_ObjName(p, pObj) );
+    fprintf( pFile, "\n" );
+    // write registers
+    if ( Aig_ManRegNum(p) )
+    {
+        Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
+        {
+            fprintf( pFile, ".latch" );
+            fprintf( pFile, " %s", Saig_ObjName(p, pObjLi) );
+            fprintf( pFile, " %s", Saig_ObjName(p, pObjLo) );
+            fprintf( pFile, " 0\n" );
+        }
+    } 
+    // check if constant is used
+    if ( Aig_ObjRefs(Aig_ManConst1(p)) )
+        fprintf( pFile, ".names %s\n 1\n", Saig_ObjName(p, Aig_ManConst1(p)) );
+    // write the nodes in the DFS order
+    Aig_ManForEachNode( p, pObj, i )
+    {
+        fprintf( pFile, ".names" );
+        fprintf( pFile, " %s", Saig_ObjName(p, Aig_ObjFanin0(pObj)) );
+        fprintf( pFile, " %s", Saig_ObjName(p, Aig_ObjFanin1(pObj)) );
+        fprintf( pFile, " %s", Saig_ObjName(p, pObj) );
+        fprintf( pFile, "\n%d%d 1\n", !Aig_ObjFaninC0(pObj), !Aig_ObjFaninC1(pObj) );
+    }
+    // write the POs
+    Aig_ManForEachPo( p, pObj, i )
+    {
+        fprintf( pFile, ".names" );
+        fprintf( pFile, " %s", Saig_ObjName(p, Aig_ObjFanin0(pObj)) );
+        fprintf( pFile, " %s", Saig_ObjName(p, pObj) );
+        fprintf( pFile, "\n%d 1\n", !Aig_ObjFaninC0(pObj) );
+    }
+    fprintf( pFile, ".end\n" );
+    fclose( pFile );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Reads one token from file.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Saig_ManReadToken( FILE * pFile )
+{
+    static char Buffer[1000];
+    if ( fscanf( pFile, "%s", Buffer ) == 1 )
+        return Buffer;
+    return NULL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the corresponding number.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Saig_ManReadNumber( Aig_Man_t * p, char * pToken )
+{
+    if ( pToken[0] == 'n' )
+        return atoi( pToken + 1 );
+    if ( pToken[0] == 'p' )
+        return atoi( pToken + 2 );
+    if ( pToken[0] == 'l' )
+        return atoi( pToken + 2 );
+    assert( 0 );
+    return -1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the corresponding node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Obj_t * Saig_ManReadNode( Aig_Man_t * p, int * pNum2Id, char * pToken )
+{
+    int Num;
+    if ( pToken[0] == 'n' )
+    {
+        Num = atoi( pToken + 1 );
+        return Aig_ManObj( p, pNum2Id[Num] );
+    }
+    if ( pToken[0] == 'p' )
+    {
+        pToken++;
+        if ( pToken[0] == 'i' )
+        {
+            Num = atoi( pToken + 1 );
+            return Aig_ManPi( p, Num );
+        }
+        if ( pToken[0] == 'o' )
+            return NULL;
+        assert( 0 );
+        return NULL;
+    }
+    if ( pToken[0] == 'l' )
+    {
+        pToken++;
+        if ( pToken[0] == 'o' )
+        {
+            Num = atoi( pToken + 1 );
+            return Saig_ManLo( p, Num );
+        }
+        if ( pToken[0] == 'i' )
+            return NULL;
+        assert( 0 );
+        return NULL;
+    }
+    assert( 0 );
+    return NULL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Reads BLIF previously dumped by Saig_ManDumpBlif().]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Saig_ManReadBlif( char * pFileName )
+{
+    FILE * pFile;
+    Aig_Man_t * p;
+    Aig_Obj_t * pFanin0, * pFanin1, * pNode;
+    char * pToken;
+    int i, nPis, nPos, nRegs, Number;
+    int * pNum2Id = NULL;  // mapping of node numbers in the file into AIG node IDs
+    // open the file
+    pFile = fopen( pFileName, "r" );
+    if ( pFile == NULL )
+    {
+        printf( "Saig_ManReadBlif(): Cannot open file for reading.\n" );
+        return NULL;
+    }
+    // skip through the comments
+    for ( i = 0; (pToken = Saig_ManReadToken( pFile )) && pToken[0] != '.'; i++ );
+    if ( pToken == NULL ) 
+        { printf( "Saig_ManReadBlif(): Error 1.\n" ); return NULL; }
+    // get he model
+    pToken = Saig_ManReadToken( pFile );
+    if ( pToken == NULL ) 
+        { printf( "Saig_ManReadBlif(): Error 2.\n" ); return NULL; }
+    // start the package
+    p = Aig_ManStart( 10000 );
+    p->pName = Aig_UtilStrsav( pToken );
+    p->pSpec = Aig_UtilStrsav( pFileName );
+    // count PIs
+    pToken = Saig_ManReadToken( pFile );
+    if ( pToken == NULL || strcmp( pToken, ".inputs" ) ) 
+        { printf( "Saig_ManReadBlif(): Error 3.\n" ); Aig_ManStop(p); return NULL; }
+    for ( nPis = 0; (pToken = Saig_ManReadToken( pFile )) && pToken[0] != '.'; nPis++ );
+    // count POs
+    if ( pToken == NULL || strcmp( pToken, ".outputs" ) ) 
+        { printf( "Saig_ManReadBlif(): Error 4.\n" ); Aig_ManStop(p); return NULL; }
+    for ( nPos = 0; (pToken = Saig_ManReadToken( pFile )) && pToken[0] != '.'; nPos++ );
+    // count latches
+    if ( pToken == NULL ) 
+        { printf( "Saig_ManReadBlif(): Error 5.\n" ); Aig_ManStop(p); return NULL; }
+    for ( nRegs = 0; strcmp( pToken, ".latch" ) == 0; nRegs++ )
+    {
+        pToken = Saig_ManReadToken( pFile );
+        if ( pToken == NULL ) 
+            { printf( "Saig_ManReadBlif(): Error 6.\n" ); Aig_ManStop(p); return NULL; }
+        pToken = Saig_ManReadToken( pFile );
+        if ( pToken == NULL ) 
+            { printf( "Saig_ManReadBlif(): Error 7.\n" ); Aig_ManStop(p); return NULL; }
+        pToken = Saig_ManReadToken( pFile );
+        if ( pToken == NULL ) 
+            { printf( "Saig_ManReadBlif(): Error 8.\n" ); Aig_ManStop(p); return NULL; }
+        pToken = Saig_ManReadToken( pFile );
+        if ( pToken == NULL ) 
+            { printf( "Saig_ManReadBlif(): Error 9.\n" ); Aig_ManStop(p); return NULL; }
+    }
+    // create PIs and LOs
+    for ( i = 0; i < nPis + nRegs; i++ )
+        Aig_ObjCreatePi( p );
+    Aig_ManSetRegNum( p, nRegs );
+    // create nodes
+    for ( i = 0; strcmp( pToken, ".names" ) == 0; i++ )
+    {
+        // first token
+        pToken = Saig_ManReadToken( pFile );
+        if ( i == 0 && pToken[0] == 'n' )
+        { // constant node
+            // read 1
+            pToken = Saig_ManReadToken( pFile );
+            if ( pToken == NULL || strcmp( pToken, "1" ) ) 
+                { printf( "Saig_ManReadBlif(): Error 10.\n" ); Aig_ManStop(p); return NULL; }
+            // read next
+            pToken = Saig_ManReadToken( pFile );
+            if ( pToken == NULL ) 
+                { printf( "Saig_ManReadBlif(): Error 11.\n" ); Aig_ManStop(p); return NULL; }
+            continue;
+        }
+        pFanin0 = Saig_ManReadNode( p, pNum2Id, pToken );
+
+        // second token
+        pToken = Saig_ManReadToken( pFile );
+        if ( (pToken[0] == 'p' && pToken[1] == 'o') || (pToken[0] == 'l' && pToken[1] == 'i') )
+        { // buffer
+            // read complemented attribute
+            pToken = Saig_ManReadToken( pFile );
+            if ( pToken == NULL ) 
+                { printf( "Saig_ManReadBlif(): Error 12.\n" ); Aig_ManStop(p); return NULL; }
+            if ( pToken[0] == '0' )
+                pFanin0 = Aig_Not(pFanin0);
+            // read 1
+            pToken = Saig_ManReadToken( pFile );
+            if ( pToken == NULL || strcmp( pToken, "1" ) ) 
+                { printf( "Saig_ManReadBlif(): Error 13.\n" ); Aig_ManStop(p); return NULL; }
+            Aig_ObjCreatePo( p, pFanin0 );
+            // read next
+            pToken = Saig_ManReadToken( pFile );
+            if ( pToken == NULL ) 
+                { printf( "Saig_ManReadBlif(): Error 14.\n" ); Aig_ManStop(p); return NULL; }
+            continue;
+        }
+
+        // third token
+        // regular node
+        pFanin1 = Saig_ManReadNode( p, pNum2Id, pToken );
+        pToken = Saig_ManReadToken( pFile );
+        Number = Saig_ManReadNumber( p, pToken );
+        // allocate mapping
+        if ( pNum2Id == NULL )
+        {
+            extern double pow( double x, double y );
+            int Size = (int)pow(10.0, (double)(strlen(pToken) - 1));
+            pNum2Id = CALLOC( int, Size );
+        }
+
+        // other tokens
+        // get the complemented attributes
+        pToken = Saig_ManReadToken( pFile );
+        if ( pToken == NULL ) 
+            { printf( "Saig_ManReadBlif(): Error 15.\n" ); Aig_ManStop(p); return NULL; }
+        if ( pToken[0] == '0' )
+            pFanin0 = Aig_Not(pFanin0);
+        if ( pToken[1] == '0' )
+            pFanin1 = Aig_Not(pFanin1);
+        // read 1
+        pToken = Saig_ManReadToken( pFile );
+        if ( pToken == NULL || strcmp( pToken, "1" ) ) 
+            { printf( "Saig_ManReadBlif(): Error 16.\n" ); Aig_ManStop(p); return NULL; }
+        // read next
+        pToken = Saig_ManReadToken( pFile );
+        if ( pToken == NULL ) 
+            { printf( "Saig_ManReadBlif(): Error 17.\n" ); Aig_ManStop(p); return NULL; }
+
+        // create new node
+        pNode = Aig_And( p, pFanin0, pFanin1 );
+        if ( Aig_IsComplement(pNode) )
+            { printf( "Saig_ManReadBlif(): Error 18.\n" ); Aig_ManStop(p); return NULL; }
+        // set mapping
+        pNum2Id[ Number ] = pNode->Id;
+    }
+    if ( pToken == NULL || strcmp( pToken, ".end" ) ) 
+        { printf( "Saig_ManReadBlif(): Error 19.\n" ); Aig_ManStop(p); return NULL; }
+    if ( nPos + nRegs != Aig_ManPoNum(p) ) 
+        { printf( "Saig_ManReadBlif(): Error 20.\n" ); Aig_ManStop(p); return NULL; }
+    // add non-node objects to the mapping
+    Aig_ManForEachPi( p, pNode, i )
+        pNum2Id[pNode->Id] = pNode->Id;
+//    FREE( pNum2Id );
+    p->pData = pNum2Id;
+    // check the new manager
+    Aig_ManSetRegNum( p, nRegs );
+    if ( !Aig_ManCheck(p) )
+        printf( "Saig_ManReadBlif(): Check has failed.\n" );
+    return p;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/saig/saigTrans.c b/src/aig/saig/saigTrans.c
new file mode 100644
index 00000000..b0039276
--- /dev/null
+++ b/src/aig/saig/saigTrans.c
@@ -0,0 +1,422 @@
+/**CFile****************************************************************
+
+  FileName    [saigTrans.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Sequential AIG package.]
+
+  Synopsis    [Dynamic simplication of the transition relation.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: saigTrans.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "saig.h"
+
+/* 
+    A similar approach is presented in the his paper:
+    A. Kuehlmann. Dynamic transition relation simplification for 
+    bounded property checking. ICCAD'04, pp. 50-57.
+*/
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Maps a node/frame into a node of a different manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Saig_ManStartMap1( Aig_Man_t * p, int nFrames )
+{
+    Vec_Int_t * vMap;
+    int i;
+    assert( p->pData == NULL );
+    vMap = Vec_IntAlloc( Aig_ManObjNumMax(p) * nFrames );
+    for ( i = 0; i < vMap->nCap; i++ )
+        vMap->pArray[i] = -1;
+    vMap->nSize = vMap->nCap;
+    p->pData = vMap;
+}
+static inline void Saig_ManStopMap1( Aig_Man_t * p )
+{
+    assert( p->pData != NULL );
+    Vec_IntFree( p->pData );
+    p->pData = NULL;
+}
+static inline int Saig_ManHasMap1( Aig_Man_t * p )
+{
+    return (int)(p->pData != NULL);
+}
+static inline void Saig_ManSetMap1( Aig_Man_t * p, Aig_Obj_t * pOld, int f1, Aig_Obj_t * pNew ) 
+{
+    Vec_Int_t * vMap = p->pData;
+    int nOffset = f1 * Aig_ManObjNumMax(p) + pOld->Id;
+    assert( !Aig_IsComplement(pOld) );
+    assert( !Aig_IsComplement(pNew) );
+    Vec_IntWriteEntry( vMap, nOffset, pNew->Id );
+}
+static inline int Saig_ManGetMap1( Aig_Man_t * p, Aig_Obj_t * pOld, int f1 )
+{
+    Vec_Int_t * vMap = p->pData;
+    int nOffset = f1 * Aig_ManObjNumMax(p) + pOld->Id;
+    return Vec_IntEntry( vMap, nOffset );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Maps a node/frame into a node/frame of a different manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Saig_ManStartMap2( Aig_Man_t * p, int nFrames )
+{
+    Vec_Int_t * vMap;
+    int i;
+    assert( p->pData2 == NULL );
+    vMap = Vec_IntAlloc( Aig_ManObjNumMax(p) * nFrames * 2 );
+    for ( i = 0; i < vMap->nCap; i++ )
+        vMap->pArray[i] = -1;
+    vMap->nSize = vMap->nCap;
+    p->pData2 = vMap;
+}
+static inline void Saig_ManStopMap2( Aig_Man_t * p )
+{
+    assert( p->pData2 != NULL );
+    Vec_IntFree( p->pData2 );
+    p->pData2 = NULL;
+}
+static inline int Saig_ManHasMap2( Aig_Man_t * p )
+{
+    return (int)(p->pData2 != NULL);
+}
+static inline void Saig_ManSetMap2( Aig_Man_t * p, Aig_Obj_t * pOld, int f1, Aig_Obj_t * pNew, int f2 ) 
+{
+    Vec_Int_t * vMap = p->pData2;
+    int nOffset = f1 * Aig_ManObjNumMax(p) + pOld->Id;
+    assert( !Aig_IsComplement(pOld) );
+    assert( !Aig_IsComplement(pNew) );
+    Vec_IntWriteEntry( vMap, 2*nOffset + 0, pNew->Id );
+    Vec_IntWriteEntry( vMap, 2*nOffset + 1, f2 );
+}
+static inline int Saig_ManGetMap2( Aig_Man_t * p, Aig_Obj_t * pOld, int f1, int * pf2 )
+{
+    Vec_Int_t * vMap = p->pData2;
+    int nOffset = f1 * Aig_ManObjNumMax(p) + pOld->Id;
+    *pf2 = Vec_IntEntry( vMap, 2*nOffset + 1 );
+    return Vec_IntEntry( vMap, 2*nOffset );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Create mapping for the first nFrames timeframes of pAig.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Saig_ManCreateMapping( Aig_Man_t * pAig, Aig_Man_t * pFrames, int nFrames )
+{
+    Aig_Obj_t * pObj, * pObjFrame, * pObjRepr;
+    int i, f, iNum, iFrame;
+    assert( pFrames->pReprs != NULL ); // mapping from nodes into their representatives
+    // start step mapping for both orignal manager and fraig
+    Saig_ManStartMap2( pAig, nFrames );
+    Saig_ManStartMap2( pFrames, 1 );
+    // for each object in each frame
+    for ( f = 0; f < nFrames; f++ )
+    Aig_ManForEachObj( pAig, pObj, i )
+    {
+        // get the frame object
+        iNum = Saig_ManGetMap1( pAig, pObj, f );
+        pObjFrame = Aig_ManObj( pFrames, iNum );
+        // if the node has no prototype, map it into itself
+        if ( pObjFrame == NULL )
+        {
+            Saig_ManSetMap2( pAig, pObj, f, pObj, f );
+            continue;
+        }
+        // get the representative object
+        pObjRepr = Aig_ObjRepr( pFrames, pObjFrame );
+        if ( pObjRepr == NULL )
+            pObjRepr = pObjFrame;
+        // check if this is the first time this object is reached
+        if ( Saig_ManGetMap2( pFrames, pObjRepr, 0, &iFrame ) == -1 )
+            Saig_ManSetMap2( pFrames, pObjRepr, 0, pObj, f );
+        // set the map for the main object
+        iNum = Saig_ManGetMap2( pFrames, pObjRepr, 0, &iFrame );
+        Saig_ManSetMap2( pAig, pObj, f, Aig_ManObj(pAig, iNum), iFrame );
+    }
+    Saig_ManStopMap2( pFrames );
+    assert( Saig_ManHasMap2(pAig) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Unroll without initialization.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Saig_ManFramesNonInitial( Aig_Man_t * pAig, int nFrames )
+{
+    Aig_Man_t * pFrames;
+    Aig_Obj_t * pObj, * pObjLi, * pObjLo;
+    int i, f;
+    assert( Saig_ManRegNum(pAig) > 0 );
+    // start node map
+    Saig_ManStartMap1( pAig, nFrames ); 
+    // start the new manager
+    pFrames = Aig_ManStart( Aig_ManNodeNum(pAig) * nFrames );
+    // map the constant node
+    Aig_ManConst1(pAig)->pData = Aig_ManConst1( pFrames );
+    // create variables for register outputs
+    Saig_ManForEachLo( pAig, pObj, i )
+        pObj->pData = Aig_ObjCreatePi( pFrames );
+    // add timeframes
+    for ( f = 0; f < nFrames; f++ )
+    {
+        // create PI nodes for this frame
+        Saig_ManForEachPi( pAig, pObj, i )
+            pObj->pData = Aig_ObjCreatePi( pFrames );
+        // add internal nodes of this frame
+        Aig_ManForEachNode( pAig, pObj, i )
+            pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+        // create POs for this frame
+        Saig_ManForEachPo( pAig, pObj, i )
+            pObj->pData = Aig_ObjCreatePo( pFrames, Aig_ObjChild0Copy(pObj) );
+        // save register inputs
+        Saig_ManForEachLi( pAig, pObj, i )
+            pObj->pData = Aig_ObjChild0Copy(pObj);
+        // save the mapping
+        Aig_ManForEachObj( pAig, pObj, i )
+        {
+            assert( pObj->pData != NULL );
+            Saig_ManSetMap1( pAig, pObj, f, Aig_Regular(pObj->pData) );
+        }
+        // quit if the last frame
+        if ( f == nFrames - 1 )
+            break;
+        // transfer to register outputs
+        Saig_ManForEachLiLo(  pAig, pObjLi, pObjLo, i )
+            pObjLo->pData = pObjLi->pData;
+    }
+    // remember register outputs
+    Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i )
+        Aig_ObjCreatePo( pFrames, pObjLi->pData );
+    Aig_ManCleanup( pFrames );
+    return pFrames;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Unroll with initialization and mapping.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Saig_ManFramesInitialMapped( Aig_Man_t * pAig, int nFrames, int nFramesMax, int fInit )
+{
+    Aig_Man_t * pFrames;
+    Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pRepr;
+    int i, f, iNum1, iNum2, iFrame2;
+    assert( nFrames <= nFramesMax );
+    assert( Saig_ManRegNum(pAig) > 0 );
+    // start node map
+    Saig_ManStartMap1( pAig, nFramesMax );
+    // start the new manager
+    pFrames = Aig_ManStart( Aig_ManNodeNum(pAig) * nFramesMax );
+    // create variables for register outputs
+    if ( fInit )
+    {
+        Saig_ManForEachLo( pAig, pObj, i )
+        {
+            pObj->pData = Aig_ManConst0( pFrames );
+            Saig_ManSetMap1( pAig, pObj, 0, Aig_Regular(pObj->pData) );
+        }
+    }
+    else
+    {
+        // create PIs first
+        for ( f = 0; f < nFramesMax; f++ )
+            Saig_ManForEachPi( pAig, pObj, i )
+                Aig_ObjCreatePi( pFrames );
+        // create registers second
+        Saig_ManForEachLo( pAig, pObj, i )
+        {
+            pObj->pData = Aig_ObjCreatePi( pFrames );
+            Saig_ManSetMap1( pAig, pObj, 0, Aig_Regular(pObj->pData) );
+        }
+    }
+    // add timeframes
+    for ( f = 0; f < nFramesMax; f++ )
+    {
+        // map the constant node
+        pObj = Aig_ManConst1(pAig);
+        pObj->pData = Aig_ManConst1( pFrames );
+        Saig_ManSetMap1( pAig, pObj, f, Aig_Regular(pObj->pData) );
+        // create PI nodes for this frame
+        Saig_ManForEachPi( pAig, pObj, i )
+        {
+            if ( fInit )
+                pObj->pData = Aig_ObjCreatePi( pFrames );
+            else
+                pObj->pData = Aig_ManPi( pFrames, f * Saig_ManPiNum(pAig) + i );
+            Saig_ManSetMap1( pAig, pObj, f, Aig_Regular(pObj->pData) );
+        }
+        // add internal nodes of this frame
+        Aig_ManForEachNode( pAig, pObj, i )
+        {
+            pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+            Saig_ManSetMap1( pAig, pObj, f, Aig_Regular(pObj->pData) );
+            if ( !Saig_ManHasMap2(pAig) )
+                continue;
+            if ( f < nFrames )
+            {
+                // get the mapping for this node
+                iNum2 = Saig_ManGetMap2( pAig, pObj, f, &iFrame2 );
+            }
+            else
+            {
+                // get the mapping for this node
+                iNum2 = Saig_ManGetMap2( pAig, pObj, nFrames-1, &iFrame2 );
+                iFrame2 += f - (nFrames-1);
+            }
+            assert( iNum2 != -1 );
+            assert( f >= iFrame2 );
+            // get the corresponding frames node
+            iNum1 = Saig_ManGetMap1( pAig, Aig_ManObj(pAig, iNum2), iFrame2 );
+            pRepr = Aig_ManObj( pFrames, iNum1 );
+            // compare the phases of these nodes
+            pObj->pData = Aig_NotCond( pRepr, pRepr->fPhase ^ Aig_ObjPhaseReal(pObj->pData) );
+        }
+        // create POs for this frame
+        Saig_ManForEachPo( pAig, pObj, i )
+        {
+            pObj->pData = Aig_ObjCreatePo( pFrames, Aig_ObjChild0Copy(pObj) );
+            Saig_ManSetMap1( pAig, pObj, f, Aig_Regular(pObj->pData) );
+        }
+        // save register inputs
+        Saig_ManForEachLi( pAig, pObj, i )
+        {
+            pObj->pData = Aig_ObjChild0Copy(pObj);
+            Saig_ManSetMap1( pAig, pObj, f, Aig_Regular(pObj->pData) );
+        }
+        // quit if the last frame
+        if ( f == nFramesMax - 1 )
+            break;
+        // transfer to register outputs
+        Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i )
+        {
+            pObjLo->pData = pObjLi->pData;
+            if ( !fInit )
+                Saig_ManSetMap1( pAig, pObjLo, f+1, Aig_Regular(pObjLo->pData) );
+        }
+    }
+    if ( !fInit )
+    {
+        // create registers
+        Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i )
+            Aig_ObjCreatePo( pFrames, pObjLi->pData );
+        // set register number
+        Aig_ManSetRegNum( pFrames, pAig->nRegs );
+    }
+    Aig_ManCleanup( pFrames );
+    Saig_ManStopMap1( pAig );
+    return pFrames;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Implements dynamic simplification.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Saig_ManTimeframeSimplify( Aig_Man_t * pAig, int nFrames, int nFramesMax, int fInit, int fVerbose )
+{
+    extern Aig_Man_t * Fra_FraigEquivence( Aig_Man_t * pManAig, int nConfMax, int fProve );
+    Aig_Man_t * pFrames, * pFraig, * pRes1, * pRes2;
+    int clk, clkTotal = clock();
+    // create uninitialized timeframes with map1
+    pFrames = Saig_ManFramesNonInitial( pAig, nFrames );
+    // perform fraiging for the unrolled timeframes
+clk = clock();
+    pFraig = Fra_FraigEquivence( pFrames, 1000, 0 );
+    // report the results
+    if ( fVerbose )
+    {
+        Aig_ManPrintStats( pFrames );
+        Aig_ManPrintStats( pFraig );
+PRT( "Fraiging", clock() - clk );
+    }
+    Aig_ManStop( pFraig );
+    assert( pFrames->pReprs != NULL );
+    // create AIG with map2
+    Saig_ManCreateMapping( pAig, pFrames, nFrames );
+    Aig_ManStop( pFrames );
+    Saig_ManStopMap1( pAig );
+    // create reduced initialized timeframes
+clk = clock();
+    pRes2 = Saig_ManFramesInitialMapped( pAig, nFrames, nFramesMax, fInit );
+PRT( "Mapped", clock() - clk );
+    // free mapping
+    Saig_ManStopMap2( pAig );
+clk = clock();
+    pRes1 = Saig_ManFramesInitialMapped( pAig, nFrames, nFramesMax, fInit );
+PRT( "Normal", clock() - clk );
+    // report the results
+    if ( fVerbose )
+    {
+        Aig_ManPrintStats( pRes1 );
+        Aig_ManPrintStats( pRes2 );
+    }
+    Aig_ManStop( pRes1 );
+    assert( !Saig_ManHasMap1(pAig) );
+    assert( !Saig_ManHasMap2(pAig) );
+    return pRes2;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index 15043266..0cafa314 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -14,7 +14,7 @@
 
   Date        [Ver. 1.0. Started - June 20, 2005.]
 
-  Revision    [$Id: abc.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+  Revision    [$Id: abc.h,v 1.1 2008/05/14 22:13:11 wudenni Exp $]
 
 ***********************************************************************/
 
@@ -29,6 +29,8 @@ extern "C" {
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
 
+#pragma warning( disable : 4273 )
+
 #include <stdio.h>
 #include <stdlib.h>
 #include <string.h>
@@ -224,6 +226,17 @@ struct Abc_Lib_t_
 ///                      MACRO DEFINITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
+#ifdef WIN32
+#define DLLEXPORT __declspec(dllexport)
+#define DLLIMPORT __declspec(dllimport)
+#else  /* defined(WIN32) */
+#define DLLIMPORT
+#endif /* defined(WIN32) */
+
+#ifndef ABC_DLL
+#define ABC_DLL DLLIMPORT
+#endif
+
 // maximum/minimum operators
 #define ABC_MIN(a,b)      (((a) < (b))? (a) : (b))
 #define ABC_MAX(a,b)      (((a) > (b))? (a) : (b))
@@ -307,7 +320,7 @@ static inline bool        Abc_NtkIsComb( Abc_Ntk_t * pNtk )          { return Ab
 static inline bool        Abc_NtkHasOnlyLatchBoxes(Abc_Ntk_t * pNtk ){ return Abc_NtkLatchNum(pNtk) == Abc_NtkBoxNum(pNtk); }
 
 // creating simple objects
-extern        Abc_Obj_t * Abc_NtkCreateObj( Abc_Ntk_t * pNtk, Abc_ObjType_t Type );
+extern ABC_DLL Abc_Obj_t * Abc_NtkCreateObj( Abc_Ntk_t * pNtk, Abc_ObjType_t Type );
 static inline Abc_Obj_t * Abc_NtkCreatePi( Abc_Ntk_t * pNtk )        { return Abc_NtkCreateObj( pNtk, ABC_OBJ_PI );         }
 static inline Abc_Obj_t * Abc_NtkCreatePo( Abc_Ntk_t * pNtk )        { return Abc_NtkCreateObj( pNtk, ABC_OBJ_PO );         }
 static inline Abc_Obj_t * Abc_NtkCreateBi( Abc_Ntk_t * pNtk )        { return Abc_NtkCreateObj( pNtk, ABC_OBJ_BI );         }
@@ -508,410 +521,410 @@ static inline void        Abc_ObjSetMvVar( Abc_Obj_t * pObj, void * pV) { Vec_At
 ////////////////////////////////////////////////////////////////////////
 
 /*=== abcAig.c ==========================================================*/
-extern Abc_Aig_t *        Abc_AigAlloc( Abc_Ntk_t * pNtk );
-extern void               Abc_AigFree( Abc_Aig_t * pMan );
-extern int                Abc_AigCleanup( Abc_Aig_t * pMan );
-extern bool               Abc_AigCheck( Abc_Aig_t * pMan );
-extern int                Abc_AigLevel( Abc_Ntk_t * pNtk );
-extern Abc_Obj_t *        Abc_AigConst1( Abc_Ntk_t * pNtk );
-extern Abc_Obj_t *        Abc_AigAnd( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 );
-extern Abc_Obj_t *        Abc_AigAndLookup( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 );
-extern Abc_Obj_t *        Abc_AigXorLookup( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1, int * pType );
-extern Abc_Obj_t *        Abc_AigMuxLookup( Abc_Aig_t * pMan, Abc_Obj_t * pC, Abc_Obj_t * pT, Abc_Obj_t * pE, int * pType );
-extern Abc_Obj_t *        Abc_AigOr( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 );
-extern Abc_Obj_t *        Abc_AigXor( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 );
-extern Abc_Obj_t *        Abc_AigMux( Abc_Aig_t * pMan, Abc_Obj_t * pC, Abc_Obj_t * p1, Abc_Obj_t * p0 );
-extern Abc_Obj_t *        Abc_AigMiter( Abc_Aig_t * pMan, Vec_Ptr_t * vPairs, int fImplic );
-extern void               Abc_AigReplace( Abc_Aig_t * pMan, Abc_Obj_t * pOld, Abc_Obj_t * pNew, bool fUpdateLevel );
-extern void               Abc_AigDeleteNode( Abc_Aig_t * pMan, Abc_Obj_t * pOld );
-extern void               Abc_AigRehash( Abc_Aig_t * pMan );
-extern bool               Abc_AigNodeHasComplFanoutEdge( Abc_Obj_t * pNode );
-extern bool               Abc_AigNodeHasComplFanoutEdgeTrav( Abc_Obj_t * pNode );
-extern void               Abc_AigPrintNode( Abc_Obj_t * pNode );
-extern bool               Abc_AigNodeIsAcyclic( Abc_Obj_t * pNode, Abc_Obj_t * pRoot );
-extern void               Abc_AigCheckFaninOrder( Abc_Aig_t * pMan );
-extern void               Abc_AigSetNodePhases( Abc_Ntk_t * pNtk );
-extern Vec_Ptr_t *        Abc_AigUpdateStart( Abc_Aig_t * pMan, Vec_Ptr_t ** pvUpdatedNets );
-extern void               Abc_AigUpdateStop( Abc_Aig_t * pMan );
-extern void               Abc_AigUpdateReset( Abc_Aig_t * pMan );
+extern ABC_DLL Abc_Aig_t *        Abc_AigAlloc( Abc_Ntk_t * pNtk );
+extern ABC_DLL void               Abc_AigFree( Abc_Aig_t * pMan );
+extern ABC_DLL int                Abc_AigCleanup( Abc_Aig_t * pMan );
+extern ABC_DLL bool               Abc_AigCheck( Abc_Aig_t * pMan );
+extern ABC_DLL int                Abc_AigLevel( Abc_Ntk_t * pNtk );
+extern ABC_DLL Abc_Obj_t *        Abc_AigConst1( Abc_Ntk_t * pNtk );
+extern ABC_DLL Abc_Obj_t *        Abc_AigAnd( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 );
+extern ABC_DLL Abc_Obj_t *        Abc_AigAndLookup( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 );
+extern ABC_DLL Abc_Obj_t *        Abc_AigXorLookup( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1, int * pType );
+extern ABC_DLL Abc_Obj_t *        Abc_AigMuxLookup( Abc_Aig_t * pMan, Abc_Obj_t * pC, Abc_Obj_t * pT, Abc_Obj_t * pE, int * pType );
+extern ABC_DLL Abc_Obj_t *        Abc_AigOr( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 );
+extern ABC_DLL Abc_Obj_t *        Abc_AigXor( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 );
+extern ABC_DLL Abc_Obj_t *        Abc_AigMux( Abc_Aig_t * pMan, Abc_Obj_t * pC, Abc_Obj_t * p1, Abc_Obj_t * p0 );
+extern ABC_DLL Abc_Obj_t *        Abc_AigMiter( Abc_Aig_t * pMan, Vec_Ptr_t * vPairs, int fImplic );
+extern ABC_DLL void               Abc_AigReplace( Abc_Aig_t * pMan, Abc_Obj_t * pOld, Abc_Obj_t * pNew, bool fUpdateLevel );
+extern ABC_DLL void               Abc_AigDeleteNode( Abc_Aig_t * pMan, Abc_Obj_t * pOld );
+extern ABC_DLL void               Abc_AigRehash( Abc_Aig_t * pMan );
+extern ABC_DLL bool               Abc_AigNodeHasComplFanoutEdge( Abc_Obj_t * pNode );
+extern ABC_DLL bool               Abc_AigNodeHasComplFanoutEdgeTrav( Abc_Obj_t * pNode );
+extern ABC_DLL void               Abc_AigPrintNode( Abc_Obj_t * pNode );
+extern ABC_DLL bool               Abc_AigNodeIsAcyclic( Abc_Obj_t * pNode, Abc_Obj_t * pRoot );
+extern ABC_DLL void               Abc_AigCheckFaninOrder( Abc_Aig_t * pMan );
+extern ABC_DLL void               Abc_AigSetNodePhases( Abc_Ntk_t * pNtk );
+extern ABC_DLL Vec_Ptr_t *        Abc_AigUpdateStart( Abc_Aig_t * pMan, Vec_Ptr_t ** pvUpdatedNets );
+extern ABC_DLL void               Abc_AigUpdateStop( Abc_Aig_t * pMan );
+extern ABC_DLL void               Abc_AigUpdateReset( Abc_Aig_t * pMan );
 /*=== abcAttach.c ==========================================================*/
-extern int                Abc_NtkAttach( Abc_Ntk_t * pNtk );
+extern ABC_DLL int                Abc_NtkAttach( Abc_Ntk_t * pNtk );
 /*=== abcBlifMv.c ==========================================================*/
-extern void               Abc_NtkStartMvVars( Abc_Ntk_t * pNtk );
-extern void               Abc_NtkFreeMvVars( Abc_Ntk_t * pNtk );
-extern void               Abc_NtkSetMvVarValues( Abc_Obj_t * pObj, int nValues );
-extern Abc_Ntk_t *        Abc_NtkStrashBlifMv( Abc_Ntk_t * pNtk );
-extern Abc_Ntk_t *        Abc_NtkInsertBlifMv( Abc_Ntk_t * pNtkBase, Abc_Ntk_t * pNtkLogic );
-extern int                Abc_NtkConvertToBlifMv( Abc_Ntk_t * pNtk );
-extern char *             Abc_NodeConvertSopToMvSop( int nVars, Vec_Int_t * vSop0, Vec_Int_t * vSop1 );
-extern int                Abc_NodeEvalMvCost( int nVars, Vec_Int_t * vSop0, Vec_Int_t * vSop1 );
+extern ABC_DLL void               Abc_NtkStartMvVars( Abc_Ntk_t * pNtk );
+extern ABC_DLL void               Abc_NtkFreeMvVars( Abc_Ntk_t * pNtk );
+extern ABC_DLL void               Abc_NtkSetMvVarValues( Abc_Obj_t * pObj, int nValues );
+extern ABC_DLL Abc_Ntk_t *        Abc_NtkStrashBlifMv( Abc_Ntk_t * pNtk );
+extern ABC_DLL Abc_Ntk_t *        Abc_NtkInsertBlifMv( Abc_Ntk_t * pNtkBase, Abc_Ntk_t * pNtkLogic );
+extern ABC_DLL int                Abc_NtkConvertToBlifMv( Abc_Ntk_t * pNtk );
+extern ABC_DLL char *             Abc_NodeConvertSopToMvSop( int nVars, Vec_Int_t * vSop0, Vec_Int_t * vSop1 );
+extern ABC_DLL int                Abc_NodeEvalMvCost( int nVars, Vec_Int_t * vSop0, Vec_Int_t * vSop1 );
 /*=== abcBalance.c ==========================================================*/
-extern Abc_Ntk_t *        Abc_NtkBalance( Abc_Ntk_t * pNtk, bool fDuplicate, bool fSelective, bool fUpdateLevel );
+extern ABC_DLL Abc_Ntk_t *        Abc_NtkBalance( Abc_Ntk_t * pNtk, bool fDuplicate, bool fSelective, bool fUpdateLevel );
 /*=== abcCheck.c ==========================================================*/
-extern bool               Abc_NtkCheck( Abc_Ntk_t * pNtk );
-extern bool               Abc_NtkCheckRead( Abc_Ntk_t * pNtk );
-extern bool               Abc_NtkDoCheck( Abc_Ntk_t * pNtk );
-extern bool               Abc_NtkCheckObj( Abc_Ntk_t * pNtk, Abc_Obj_t * pObj );
-extern bool               Abc_NtkCompareSignals( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fOnlyPis, int fComb );
-extern int                Abc_NtkIsAcyclicHierarchy( Abc_Ntk_t * pNtk );
-extern int                Abc_NtkCheckUniqueCiNames( Abc_Ntk_t * pNtk );
-extern int                Abc_NtkCheckUniqueCoNames( Abc_Ntk_t * pNtk );
-extern int                Abc_NtkCheckUniqueCioNames( Abc_Ntk_t * pNtk );
+extern ABC_DLL bool               Abc_NtkCheck( Abc_Ntk_t * pNtk );
+extern ABC_DLL bool               Abc_NtkCheckRead( Abc_Ntk_t * pNtk );
+extern ABC_DLL bool               Abc_NtkDoCheck( Abc_Ntk_t * pNtk );
+extern ABC_DLL bool               Abc_NtkCheckObj( Abc_Ntk_t * pNtk, Abc_Obj_t * pObj );
+extern ABC_DLL bool               Abc_NtkCompareSignals( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fOnlyPis, int fComb );
+extern ABC_DLL int                Abc_NtkIsAcyclicHierarchy( Abc_Ntk_t * pNtk );
+extern ABC_DLL int                Abc_NtkCheckUniqueCiNames( Abc_Ntk_t * pNtk );
+extern ABC_DLL int                Abc_NtkCheckUniqueCoNames( Abc_Ntk_t * pNtk );
+extern ABC_DLL int                Abc_NtkCheckUniqueCioNames( Abc_Ntk_t * pNtk );
 /*=== abcCollapse.c ==========================================================*/
-extern Abc_Ntk_t *        Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDualRail, int fReorder, int fVerbose );
+extern ABC_DLL Abc_Ntk_t *        Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDualRail, int fReorder, int fVerbose );
 /*=== abcCut.c ==========================================================*/
-extern void *             Abc_NodeGetCutsRecursive( void * p, Abc_Obj_t * pObj, int fDag, int fTree );
-extern void *             Abc_NodeGetCuts( void * p, Abc_Obj_t * pObj, int fDag, int fTree );
-extern void               Abc_NodeGetCutsSeq( void * p, Abc_Obj_t * pObj, int fFirst );
-extern void *             Abc_NodeReadCuts( void * p, Abc_Obj_t * pObj );
-extern void               Abc_NodeFreeCuts( void * p, Abc_Obj_t * pObj );
+extern ABC_DLL void *             Abc_NodeGetCutsRecursive( void * p, Abc_Obj_t * pObj, int fDag, int fTree );
+extern ABC_DLL void *             Abc_NodeGetCuts( void * p, Abc_Obj_t * pObj, int fDag, int fTree );
+extern ABC_DLL void               Abc_NodeGetCutsSeq( void * p, Abc_Obj_t * pObj, int fFirst );
+extern ABC_DLL void *             Abc_NodeReadCuts( void * p, Abc_Obj_t * pObj );
+extern ABC_DLL void               Abc_NodeFreeCuts( void * p, Abc_Obj_t * pObj );
 /*=== abcDelay.c ==========================================================*/
-extern float              Abc_NtkDelayTraceLut( Abc_Ntk_t * pNtk, int fUseLutLib );
+extern ABC_DLL float              Abc_NtkDelayTraceLut( Abc_Ntk_t * pNtk, int fUseLutLib );
 /*=== abcDfs.c ==========================================================*/
-extern Vec_Ptr_t *        Abc_NtkDfs( Abc_Ntk_t * pNtk, int fCollectAll );
-extern Vec_Ptr_t *        Abc_NtkDfsNodes( Abc_Ntk_t * pNtk, Abc_Obj_t ** ppNodes, int nNodes );
-extern Vec_Ptr_t *        Abc_NtkDfsReverse( Abc_Ntk_t * pNtk );
-extern Vec_Ptr_t *        Abc_NtkDfsReverseNodes( Abc_Ntk_t * pNtk, Abc_Obj_t ** ppNodes, int nNodes );
-extern Vec_Ptr_t *        Abc_NtkDfsReverseNodesContained( Abc_Ntk_t * pNtk, Abc_Obj_t ** ppNodes, int nNodes );
-extern Vec_Ptr_t *        Abc_NtkDfsSeq( Abc_Ntk_t * pNtk );
-extern Vec_Ptr_t *        Abc_NtkDfsSeqReverse( Abc_Ntk_t * pNtk );
-extern Vec_Ptr_t *        Abc_NtkDfsIter( Abc_Ntk_t * pNtk, int fCollectAll );
-extern Vec_Ptr_t *        Abc_NtkDfsHie( Abc_Ntk_t * pNtk, int fCollectAll );
-extern bool               Abc_NtkIsDfsOrdered( Abc_Ntk_t * pNtk );
-extern Vec_Ptr_t *        Abc_NtkSupport( Abc_Ntk_t * pNtk );
-extern Vec_Ptr_t *        Abc_NtkNodeSupport( Abc_Ntk_t * pNtk, Abc_Obj_t ** ppNodes, int nNodes );
-extern Vec_Ptr_t *        Abc_AigDfs( Abc_Ntk_t * pNtk, int fCollectAll, int fCollectCos );
-extern Vec_Vec_t *        Abc_DfsLevelized( Abc_Obj_t * pNode, bool fTfi );
-extern Vec_Vec_t *        Abc_NtkLevelize( Abc_Ntk_t * pNtk );
-extern int                Abc_NtkLevel( Abc_Ntk_t * pNtk );
-extern int                Abc_NtkLevelReverse( Abc_Ntk_t * pNtk );
-extern bool               Abc_NtkIsAcyclic( Abc_Ntk_t * pNtk );
-extern Vec_Ptr_t *        Abc_AigGetLevelizedOrder( Abc_Ntk_t * pNtk, int fCollectCis );
+extern ABC_DLL Vec_Ptr_t *        Abc_NtkDfs( Abc_Ntk_t * pNtk, int fCollectAll );
+extern ABC_DLL Vec_Ptr_t *        Abc_NtkDfsNodes( Abc_Ntk_t * pNtk, Abc_Obj_t ** ppNodes, int nNodes );
+extern ABC_DLL Vec_Ptr_t *        Abc_NtkDfsReverse( Abc_Ntk_t * pNtk );
+extern ABC_DLL Vec_Ptr_t *        Abc_NtkDfsReverseNodes( Abc_Ntk_t * pNtk, Abc_Obj_t ** ppNodes, int nNodes );
+extern ABC_DLL Vec_Ptr_t *        Abc_NtkDfsReverseNodesContained( Abc_Ntk_t * pNtk, Abc_Obj_t ** ppNodes, int nNodes );
+extern ABC_DLL Vec_Ptr_t *        Abc_NtkDfsSeq( Abc_Ntk_t * pNtk );
+extern ABC_DLL Vec_Ptr_t *        Abc_NtkDfsSeqReverse( Abc_Ntk_t * pNtk );
+extern ABC_DLL Vec_Ptr_t *        Abc_NtkDfsIter( Abc_Ntk_t * pNtk, int fCollectAll );
+extern ABC_DLL Vec_Ptr_t *        Abc_NtkDfsHie( Abc_Ntk_t * pNtk, int fCollectAll );
+extern ABC_DLL bool               Abc_NtkIsDfsOrdered( Abc_Ntk_t * pNtk );
+extern ABC_DLL Vec_Ptr_t *        Abc_NtkSupport( Abc_Ntk_t * pNtk );
+extern ABC_DLL Vec_Ptr_t *        Abc_NtkNodeSupport( Abc_Ntk_t * pNtk, Abc_Obj_t ** ppNodes, int nNodes );
+extern ABC_DLL Vec_Ptr_t *        Abc_AigDfs( Abc_Ntk_t * pNtk, int fCollectAll, int fCollectCos );
+extern ABC_DLL Vec_Vec_t *        Abc_DfsLevelized( Abc_Obj_t * pNode, bool fTfi );
+extern ABC_DLL Vec_Vec_t *        Abc_NtkLevelize( Abc_Ntk_t * pNtk );
+extern ABC_DLL int                Abc_NtkLevel( Abc_Ntk_t * pNtk );
+extern ABC_DLL int                Abc_NtkLevelReverse( Abc_Ntk_t * pNtk );
+extern ABC_DLL bool               Abc_NtkIsAcyclic( Abc_Ntk_t * pNtk );
+extern ABC_DLL Vec_Ptr_t *        Abc_AigGetLevelizedOrder( Abc_Ntk_t * pNtk, int fCollectCis );
 /*=== abcFanio.c ==========================================================*/
-extern void               Abc_ObjAddFanin( Abc_Obj_t * pObj, Abc_Obj_t * pFanin );
-extern void               Abc_ObjDeleteFanin( Abc_Obj_t * pObj, Abc_Obj_t * pFanin );
-extern void               Abc_ObjRemoveFanins( Abc_Obj_t * pObj );
-extern void               Abc_ObjPatchFanin( Abc_Obj_t * pObj, Abc_Obj_t * pFaninOld, Abc_Obj_t * pFaninNew );
-extern Abc_Obj_t *        Abc_ObjInsertBetween( Abc_Obj_t * pNodeIn, Abc_Obj_t * pNodeOut, Abc_ObjType_t Type );
-extern void               Abc_ObjTransferFanout( Abc_Obj_t * pObjOld, Abc_Obj_t * pObjNew );
-extern void               Abc_ObjReplace( Abc_Obj_t * pObjOld, Abc_Obj_t * pObjNew );
-extern int                Abc_ObjFanoutFaninNum( Abc_Obj_t * pFanout, Abc_Obj_t * pFanin );
+extern ABC_DLL void               Abc_ObjAddFanin( Abc_Obj_t * pObj, Abc_Obj_t * pFanin );
+extern ABC_DLL void               Abc_ObjDeleteFanin( Abc_Obj_t * pObj, Abc_Obj_t * pFanin );
+extern ABC_DLL void               Abc_ObjRemoveFanins( Abc_Obj_t * pObj );
+extern ABC_DLL void               Abc_ObjPatchFanin( Abc_Obj_t * pObj, Abc_Obj_t * pFaninOld, Abc_Obj_t * pFaninNew );
+extern ABC_DLL Abc_Obj_t *        Abc_ObjInsertBetween( Abc_Obj_t * pNodeIn, Abc_Obj_t * pNodeOut, Abc_ObjType_t Type );
+extern ABC_DLL void               Abc_ObjTransferFanout( Abc_Obj_t * pObjOld, Abc_Obj_t * pObjNew );
+extern ABC_DLL void               Abc_ObjReplace( Abc_Obj_t * pObjOld, Abc_Obj_t * pObjNew );
+extern ABC_DLL int                Abc_ObjFanoutFaninNum( Abc_Obj_t * pFanout, Abc_Obj_t * pFanin );
 /*=== abcFraig.c ==========================================================*/
-extern Abc_Ntk_t *        Abc_NtkFraig( Abc_Ntk_t * pNtk, void * pParams, int fAllNodes, int fExdc );
-extern void *             Abc_NtkToFraig( Abc_Ntk_t * pNtk, void * pParams, int fAllNodes, int fExdc );
-extern Abc_Ntk_t *        Abc_NtkFraigTrust( Abc_Ntk_t * pNtk );
-extern int                Abc_NtkFraigStore( Abc_Ntk_t * pNtk );
-extern Abc_Ntk_t *        Abc_NtkFraigRestore();
-extern void               Abc_NtkFraigStoreClean();
+extern ABC_DLL Abc_Ntk_t *        Abc_NtkFraig( Abc_Ntk_t * pNtk, void * pParams, int fAllNodes, int fExdc );
+extern ABC_DLL void *             Abc_NtkToFraig( Abc_Ntk_t * pNtk, void * pParams, int fAllNodes, int fExdc );
+extern ABC_DLL Abc_Ntk_t *        Abc_NtkFraigTrust( Abc_Ntk_t * pNtk );
+extern ABC_DLL int                Abc_NtkFraigStore( Abc_Ntk_t * pNtk );
+extern ABC_DLL Abc_Ntk_t *        Abc_NtkFraigRestore();
+extern ABC_DLL void               Abc_NtkFraigStoreClean();
 /*=== abcFunc.c ==========================================================*/
-extern int                Abc_NtkSopToBdd( Abc_Ntk_t * pNtk );
-extern DdNode *           Abc_ConvertSopToBdd( DdManager * dd, char * pSop );
-extern char *             Abc_ConvertBddToSop( Extra_MmFlex_t * pMan, DdManager * dd, DdNode * bFuncOn, DdNode * bFuncOnDc, int nFanins, int fAllPrimes, Vec_Str_t * vCube, int fMode );
-extern int                Abc_NtkBddToSop( Abc_Ntk_t * pNtk, int fDirect );
-extern void               Abc_NodeBddToCnf( Abc_Obj_t * pNode, Extra_MmFlex_t * pMmMan, Vec_Str_t * vCube, int fAllPrimes, char ** ppSop0, char ** ppSop1 );
-extern int                Abc_CountZddCubes( DdManager * dd, DdNode * zCover );
-extern void               Abc_NtkLogicMakeDirectSops( Abc_Ntk_t * pNtk );
-extern int                Abc_NtkSopToAig( Abc_Ntk_t * pNtk );
-extern int                Abc_NtkAigToBdd( Abc_Ntk_t * pNtk );
-extern int                Abc_NtkMapToSop( Abc_Ntk_t * pNtk );
-extern int                Abc_NtkToSop( Abc_Ntk_t * pNtk, int fDirect );
-extern int                Abc_NtkToBdd( Abc_Ntk_t * pNtk );
-extern int                Abc_NtkToAig( Abc_Ntk_t * pNtk );
+extern ABC_DLL int                Abc_NtkSopToBdd( Abc_Ntk_t * pNtk );
+extern ABC_DLL DdNode *           Abc_ConvertSopToBdd( DdManager * dd, char * pSop );
+extern ABC_DLL char *             Abc_ConvertBddToSop( Extra_MmFlex_t * pMan, DdManager * dd, DdNode * bFuncOn, DdNode * bFuncOnDc, int nFanins, int fAllPrimes, Vec_Str_t * vCube, int fMode );
+extern ABC_DLL int                Abc_NtkBddToSop( Abc_Ntk_t * pNtk, int fDirect );
+extern ABC_DLL void               Abc_NodeBddToCnf( Abc_Obj_t * pNode, Extra_MmFlex_t * pMmMan, Vec_Str_t * vCube, int fAllPrimes, char ** ppSop0, char ** ppSop1 );
+extern ABC_DLL int                Abc_CountZddCubes( DdManager * dd, DdNode * zCover );
+extern ABC_DLL void               Abc_NtkLogicMakeDirectSops( Abc_Ntk_t * pNtk );
+extern ABC_DLL int                Abc_NtkSopToAig( Abc_Ntk_t * pNtk );
+extern ABC_DLL int                Abc_NtkAigToBdd( Abc_Ntk_t * pNtk );
+extern ABC_DLL int                Abc_NtkMapToSop( Abc_Ntk_t * pNtk );
+extern ABC_DLL int                Abc_NtkToSop( Abc_Ntk_t * pNtk, int fDirect );
+extern ABC_DLL int                Abc_NtkToBdd( Abc_Ntk_t * pNtk );
+extern ABC_DLL int                Abc_NtkToAig( Abc_Ntk_t * pNtk );
 /*=== abcHaig.c ==========================================================*/
-extern int                Abc_NtkHaigStart( Abc_Ntk_t * pNtk );
-extern int                Abc_NtkHaigStop( Abc_Ntk_t * pNtk );
-extern Abc_Ntk_t *        Abc_NtkHaigUse( Abc_Ntk_t * pNtk );
+extern ABC_DLL int                Abc_NtkHaigStart( Abc_Ntk_t * pNtk );
+extern ABC_DLL int                Abc_NtkHaigStop( Abc_Ntk_t * pNtk );
+extern ABC_DLL Abc_Ntk_t *        Abc_NtkHaigUse( Abc_Ntk_t * pNtk );
 /*=== abcHie.c ==========================================================*/
-extern Abc_Ntk_t *        Abc_NtkFlattenLogicHierarchy( Abc_Ntk_t * pNtk );
-extern Abc_Ntk_t *        Abc_NtkConvertBlackboxes( Abc_Ntk_t * pNtk );
-extern Abc_Ntk_t *        Abc_NtkInsertNewLogic( Abc_Ntk_t * pNtkH, Abc_Ntk_t * pNtkL );
+extern ABC_DLL Abc_Ntk_t *        Abc_NtkFlattenLogicHierarchy( Abc_Ntk_t * pNtk );
+extern ABC_DLL Abc_Ntk_t *        Abc_NtkConvertBlackboxes( Abc_Ntk_t * pNtk );
+extern ABC_DLL Abc_Ntk_t *        Abc_NtkInsertNewLogic( Abc_Ntk_t * pNtkH, Abc_Ntk_t * pNtkL );
 /*=== abcLatch.c ==========================================================*/
-extern bool               Abc_NtkLatchIsSelfFeed( Abc_Obj_t * pLatch );
-extern int                Abc_NtkCountSelfFeedLatches( Abc_Ntk_t * pNtk );
-extern int                Abc_NtkRemoveSelfFeedLatches( Abc_Ntk_t * pNtk );
-extern Vec_Int_t *        Abc_NtkCollectLatchValues( Abc_Ntk_t * pNtk );
-extern void               Abc_NtkInsertLatchValues( Abc_Ntk_t * pNtk, Vec_Int_t * vValues );
-extern Abc_Obj_t *        Abc_NtkAddLatch( Abc_Ntk_t * pNtk, Abc_Obj_t * pDriver, Abc_InitType_t Init );
-extern void               Abc_NtkConvertDcLatches( Abc_Ntk_t * pNtk );
-extern Vec_Ptr_t *        Abc_NtkConverLatchNamesIntoNumbers( Abc_Ntk_t * pNtk );
+extern ABC_DLL bool               Abc_NtkLatchIsSelfFeed( Abc_Obj_t * pLatch );
+extern ABC_DLL int                Abc_NtkCountSelfFeedLatches( Abc_Ntk_t * pNtk );
+extern ABC_DLL int                Abc_NtkRemoveSelfFeedLatches( Abc_Ntk_t * pNtk );
+extern ABC_DLL Vec_Int_t *        Abc_NtkCollectLatchValues( Abc_Ntk_t * pNtk );
+extern ABC_DLL void               Abc_NtkInsertLatchValues( Abc_Ntk_t * pNtk, Vec_Int_t * vValues );
+extern ABC_DLL Abc_Obj_t *        Abc_NtkAddLatch( Abc_Ntk_t * pNtk, Abc_Obj_t * pDriver, Abc_InitType_t Init );
+extern ABC_DLL void               Abc_NtkConvertDcLatches( Abc_Ntk_t * pNtk );
+extern ABC_DLL Vec_Ptr_t *        Abc_NtkConverLatchNamesIntoNumbers( Abc_Ntk_t * pNtk );
  /*=== abcLib.c ==========================================================*/
-extern Abc_Lib_t *        Abc_LibCreate( char * pName );
-extern void               Abc_LibFree( Abc_Lib_t * pLib, Abc_Ntk_t * pNtk );
-extern void               Abc_LibPrint( Abc_Lib_t * pLib );
-extern int                Abc_LibAddModel( Abc_Lib_t * pLib, Abc_Ntk_t * pNtk );
-extern Abc_Ntk_t *        Abc_LibFindModelByName( Abc_Lib_t * pLib, char * pName );
-extern int                Abc_LibFindTopLevelModels( Abc_Lib_t * pLib );
-extern Abc_Ntk_t *        Abc_LibDeriveRoot( Abc_Lib_t * pLib );
+extern ABC_DLL Abc_Lib_t *        Abc_LibCreate( char * pName );
+extern ABC_DLL void               Abc_LibFree( Abc_Lib_t * pLib, Abc_Ntk_t * pNtk );
+extern ABC_DLL void               Abc_LibPrint( Abc_Lib_t * pLib );
+extern ABC_DLL int                Abc_LibAddModel( Abc_Lib_t * pLib, Abc_Ntk_t * pNtk );
+extern ABC_DLL Abc_Ntk_t *        Abc_LibFindModelByName( Abc_Lib_t * pLib, char * pName );
+extern ABC_DLL int                Abc_LibFindTopLevelModels( Abc_Lib_t * pLib );
+extern ABC_DLL Abc_Ntk_t *        Abc_LibDeriveRoot( Abc_Lib_t * pLib );
 /*=== abcMiter.c ==========================================================*/
-extern int                Abc_NtkMinimumBase( Abc_Ntk_t * pNtk );
-extern int                Abc_NodeMinimumBase( Abc_Obj_t * pNode );
-extern int                Abc_NtkRemoveDupFanins( Abc_Ntk_t * pNtk );
-extern int                Abc_NodeRemoveDupFanins( Abc_Obj_t * pNode );
+extern ABC_DLL int                Abc_NtkMinimumBase( Abc_Ntk_t * pNtk );
+extern ABC_DLL int                Abc_NodeMinimumBase( Abc_Obj_t * pNode );
+extern ABC_DLL int                Abc_NtkRemoveDupFanins( Abc_Ntk_t * pNtk );
+extern ABC_DLL int                Abc_NodeRemoveDupFanins( Abc_Obj_t * pNode );
 /*=== abcMiter.c ==========================================================*/
-extern Abc_Ntk_t *        Abc_NtkMiter( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb, int nPartSize, int fImplic, int fMulti );
-extern void               Abc_NtkMiterAddCone( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkMiter, Abc_Obj_t * pNode );
-extern Abc_Ntk_t *        Abc_NtkMiterAnd( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fOr, int fCompl2 );
-extern Abc_Ntk_t *        Abc_NtkMiterCofactor( Abc_Ntk_t * pNtk, Vec_Int_t * vPiValues );
-extern Abc_Ntk_t *        Abc_NtkMiterForCofactors( Abc_Ntk_t * pNtk, int Out, int In1, int In2 );
-extern Abc_Ntk_t *        Abc_NtkMiterQuantify( Abc_Ntk_t * pNtk, int In, int fExist );
-extern Abc_Ntk_t *        Abc_NtkMiterQuantifyPis( Abc_Ntk_t * pNtk );
-extern int                Abc_NtkMiterIsConstant( Abc_Ntk_t * pMiter );
-extern void               Abc_NtkMiterReport( Abc_Ntk_t * pMiter );
-extern Abc_Ntk_t *        Abc_NtkFrames( Abc_Ntk_t * pNtk, int nFrames, int fInitial );
+extern ABC_DLL Abc_Ntk_t *        Abc_NtkMiter( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb, int nPartSize, int fImplic, int fMulti );
+extern ABC_DLL void               Abc_NtkMiterAddCone( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkMiter, Abc_Obj_t * pNode );
+extern ABC_DLL Abc_Ntk_t *        Abc_NtkMiterAnd( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fOr, int fCompl2 );
+extern ABC_DLL Abc_Ntk_t *        Abc_NtkMiterCofactor( Abc_Ntk_t * pNtk, Vec_Int_t * vPiValues );
+extern ABC_DLL Abc_Ntk_t *        Abc_NtkMiterForCofactors( Abc_Ntk_t * pNtk, int Out, int In1, int In2 );
+extern ABC_DLL Abc_Ntk_t *        Abc_NtkMiterQuantify( Abc_Ntk_t * pNtk, int In, int fExist );
+extern ABC_DLL Abc_Ntk_t *        Abc_NtkMiterQuantifyPis( Abc_Ntk_t * pNtk );
+extern ABC_DLL int                Abc_NtkMiterIsConstant( Abc_Ntk_t * pMiter );
+extern ABC_DLL void               Abc_NtkMiterReport( Abc_Ntk_t * pMiter );
+extern ABC_DLL Abc_Ntk_t *        Abc_NtkFrames( Abc_Ntk_t * pNtk, int nFrames, int fInitial, int fVerbose );
 /*=== abcNames.c ====================================================*/
-extern char *             Abc_ObjName( Abc_Obj_t * pNode );
-extern char *             Abc_ObjAssignName( Abc_Obj_t * pObj, char * pName, char * pSuffix );
-extern char *             Abc_ObjNameSuffix( Abc_Obj_t * pObj, char * pSuffix );
-extern char *             Abc_ObjNameDummy( char * pPrefix, int Num, int nDigits );
-extern void               Abc_NtkTrasferNames( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew );
-extern void               Abc_NtkTrasferNamesNoLatches( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew );
-extern Vec_Ptr_t *        Abc_NodeGetFaninNames( Abc_Obj_t * pNode );
-extern Vec_Ptr_t *        Abc_NodeGetFakeNames( int nNames );
-extern void               Abc_NodeFreeNames( Vec_Ptr_t * vNames );
-extern char **            Abc_NtkCollectCioNames( Abc_Ntk_t * pNtk, int fCollectCos );
-extern int                Abc_NodeCompareNames( Abc_Obj_t ** pp1, Abc_Obj_t ** pp2 );
-extern void               Abc_NtkOrderObjsByName( Abc_Ntk_t * pNtk, int fComb );
-extern void               Abc_NtkAddDummyPiNames( Abc_Ntk_t * pNtk );
-extern void               Abc_NtkAddDummyPoNames( Abc_Ntk_t * pNtk );
-extern void               Abc_NtkAddDummyAssertNames( Abc_Ntk_t * pNtk );
-extern void               Abc_NtkAddDummyBoxNames( Abc_Ntk_t * pNtk );
-extern void               Abc_NtkShortNames( Abc_Ntk_t * pNtk );
+extern ABC_DLL char *             Abc_ObjName( Abc_Obj_t * pNode );
+extern ABC_DLL char *             Abc_ObjAssignName( Abc_Obj_t * pObj, char * pName, char * pSuffix );
+extern ABC_DLL char *             Abc_ObjNameSuffix( Abc_Obj_t * pObj, char * pSuffix );
+extern ABC_DLL char *             Abc_ObjNameDummy( char * pPrefix, int Num, int nDigits );
+extern ABC_DLL void               Abc_NtkTrasferNames( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew );
+extern ABC_DLL void               Abc_NtkTrasferNamesNoLatches( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew );
+extern ABC_DLL Vec_Ptr_t *        Abc_NodeGetFaninNames( Abc_Obj_t * pNode );
+extern ABC_DLL Vec_Ptr_t *        Abc_NodeGetFakeNames( int nNames );
+extern ABC_DLL void               Abc_NodeFreeNames( Vec_Ptr_t * vNames );
+extern ABC_DLL char **            Abc_NtkCollectCioNames( Abc_Ntk_t * pNtk, int fCollectCos );
+extern ABC_DLL int                Abc_NodeCompareNames( Abc_Obj_t ** pp1, Abc_Obj_t ** pp2 );
+extern ABC_DLL void               Abc_NtkOrderObjsByName( Abc_Ntk_t * pNtk, int fComb );
+extern ABC_DLL void               Abc_NtkAddDummyPiNames( Abc_Ntk_t * pNtk );
+extern ABC_DLL void               Abc_NtkAddDummyPoNames( Abc_Ntk_t * pNtk );
+extern ABC_DLL void               Abc_NtkAddDummyAssertNames( Abc_Ntk_t * pNtk );
+extern ABC_DLL void               Abc_NtkAddDummyBoxNames( Abc_Ntk_t * pNtk );
+extern ABC_DLL void               Abc_NtkShortNames( Abc_Ntk_t * pNtk );
 /*=== abcNetlist.c ==========================================================*/
-extern Abc_Ntk_t *        Abc_NtkToLogic( Abc_Ntk_t * pNtk );
-extern Abc_Ntk_t *        Abc_NtkToNetlist( Abc_Ntk_t * pNtk );
-extern Abc_Ntk_t *        Abc_NtkToNetlistBench( Abc_Ntk_t * pNtk );
+extern ABC_DLL Abc_Ntk_t *        Abc_NtkToLogic( Abc_Ntk_t * pNtk );
+extern ABC_DLL Abc_Ntk_t *        Abc_NtkToNetlist( Abc_Ntk_t * pNtk );
+extern ABC_DLL Abc_Ntk_t *        Abc_NtkToNetlistBench( Abc_Ntk_t * pNtk );
 /*=== abcNtbdd.c ==========================================================*/
-extern Abc_Ntk_t *        Abc_NtkDeriveFromBdd( DdManager * dd, DdNode * bFunc, char * pNamePo, Vec_Ptr_t * vNamesPi );
-extern Abc_Ntk_t *        Abc_NtkBddToMuxes( Abc_Ntk_t * pNtk );
-extern DdManager *        Abc_NtkBuildGlobalBdds( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDropInternal, int fReorder, int fVerbose );
-extern DdManager *        Abc_NtkFreeGlobalBdds( Abc_Ntk_t * pNtk, int fFreeMan );
-extern int                Abc_NtkSizeOfGlobalBdds( Abc_Ntk_t * pNtk );
+extern ABC_DLL Abc_Ntk_t *        Abc_NtkDeriveFromBdd( DdManager * dd, DdNode * bFunc, char * pNamePo, Vec_Ptr_t * vNamesPi );
+extern ABC_DLL Abc_Ntk_t *        Abc_NtkBddToMuxes( Abc_Ntk_t * pNtk );
+extern ABC_DLL DdManager *        Abc_NtkBuildGlobalBdds( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDropInternal, int fReorder, int fVerbose );
+extern ABC_DLL DdManager *        Abc_NtkFreeGlobalBdds( Abc_Ntk_t * pNtk, int fFreeMan );
+extern ABC_DLL int                Abc_NtkSizeOfGlobalBdds( Abc_Ntk_t * pNtk );
 /*=== abcNtk.c ==========================================================*/
-extern Abc_Ntk_t *        Abc_NtkAlloc( Abc_NtkType_t Type, Abc_NtkFunc_t Func, int fUseMemMan );
-extern Abc_Ntk_t *        Abc_NtkStartFrom( Abc_Ntk_t * pNtk, Abc_NtkType_t Type, Abc_NtkFunc_t Func );
-extern Abc_Ntk_t *        Abc_NtkStartFromNoLatches( Abc_Ntk_t * pNtk, Abc_NtkType_t Type, Abc_NtkFunc_t Func );
-extern void               Abc_NtkFinalize( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew );
-extern Abc_Ntk_t *        Abc_NtkStartRead( char * pName );
-extern void               Abc_NtkFinalizeRead( Abc_Ntk_t * pNtk );
-extern Abc_Ntk_t *        Abc_NtkDup( Abc_Ntk_t * pNtk );
-extern Abc_Ntk_t *        Abc_NtkCreateCone( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, char * pNodeName, int fUseAllCis );
-extern Abc_Ntk_t *        Abc_NtkCreateConeArray( Abc_Ntk_t * pNtk, Vec_Ptr_t * vRoots, int fUseAllCis );
-extern void               Abc_NtkAppendToCone( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, Vec_Ptr_t * vRoots );
-extern Abc_Ntk_t *        Abc_NtkCreateMffc( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, char * pNodeName );
-extern Abc_Ntk_t *        Abc_NtkCreateTarget( Abc_Ntk_t * pNtk, Vec_Ptr_t * vRoots, Vec_Int_t * vValues );
-extern Abc_Ntk_t *        Abc_NtkCreateFromNode( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode );
-extern Abc_Ntk_t *        Abc_NtkCreateWithNode( char * pSop );
-extern void               Abc_NtkDelete( Abc_Ntk_t * pNtk );
-extern void               Abc_NtkFixNonDrivenNets( Abc_Ntk_t * pNtk );
-extern void               Abc_NtkMakeComb( Abc_Ntk_t * pNtk, int fRemoveLatches );
+extern ABC_DLL Abc_Ntk_t *        Abc_NtkAlloc( Abc_NtkType_t Type, Abc_NtkFunc_t Func, int fUseMemMan );
+extern ABC_DLL Abc_Ntk_t *        Abc_NtkStartFrom( Abc_Ntk_t * pNtk, Abc_NtkType_t Type, Abc_NtkFunc_t Func );
+extern ABC_DLL Abc_Ntk_t *        Abc_NtkStartFromNoLatches( Abc_Ntk_t * pNtk, Abc_NtkType_t Type, Abc_NtkFunc_t Func );
+extern ABC_DLL void               Abc_NtkFinalize( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew );
+extern ABC_DLL Abc_Ntk_t *        Abc_NtkStartRead( char * pName );
+extern ABC_DLL void               Abc_NtkFinalizeRead( Abc_Ntk_t * pNtk );
+extern ABC_DLL Abc_Ntk_t *        Abc_NtkDup( Abc_Ntk_t * pNtk );
+extern ABC_DLL Abc_Ntk_t *        Abc_NtkCreateCone( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, char * pNodeName, int fUseAllCis );
+extern ABC_DLL Abc_Ntk_t *        Abc_NtkCreateConeArray( Abc_Ntk_t * pNtk, Vec_Ptr_t * vRoots, int fUseAllCis );
+extern ABC_DLL void               Abc_NtkAppendToCone( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, Vec_Ptr_t * vRoots );
+extern ABC_DLL Abc_Ntk_t *        Abc_NtkCreateMffc( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, char * pNodeName );
+extern ABC_DLL Abc_Ntk_t *        Abc_NtkCreateTarget( Abc_Ntk_t * pNtk, Vec_Ptr_t * vRoots, Vec_Int_t * vValues );
+extern ABC_DLL Abc_Ntk_t *        Abc_NtkCreateFromNode( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode );
+extern ABC_DLL Abc_Ntk_t *        Abc_NtkCreateWithNode( char * pSop );
+extern ABC_DLL void               Abc_NtkDelete( Abc_Ntk_t * pNtk );
+extern ABC_DLL void               Abc_NtkFixNonDrivenNets( Abc_Ntk_t * pNtk );
+extern ABC_DLL void               Abc_NtkMakeComb( Abc_Ntk_t * pNtk, int fRemoveLatches );
 /*=== abcObj.c ==========================================================*/
-extern Abc_Obj_t *        Abc_ObjAlloc( Abc_Ntk_t * pNtk, Abc_ObjType_t Type );
-extern void               Abc_ObjRecycle( Abc_Obj_t * pObj );
-extern Abc_Obj_t *        Abc_NtkCreateObj( Abc_Ntk_t * pNtk, Abc_ObjType_t Type );
-extern void               Abc_NtkDeleteObj( Abc_Obj_t * pObj );
-extern void               Abc_NtkDeleteObj_rec( Abc_Obj_t * pObj, int fOnlyNodes );
-extern void               Abc_NtkDeleteAll_rec( Abc_Obj_t * pObj );
-extern Abc_Obj_t *        Abc_NtkDupObj( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj, int fCopyName );
-extern Abc_Obj_t *        Abc_NtkDupBox( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pBox, int fCopyName );
-extern Abc_Obj_t *        Abc_NtkCloneObj( Abc_Obj_t * pNode );
-extern Abc_Obj_t *        Abc_NtkFindNode( Abc_Ntk_t * pNtk, char * pName );
-extern Abc_Obj_t *        Abc_NtkFindNet( Abc_Ntk_t * pNtk, char * pName );
-extern Abc_Obj_t *        Abc_NtkFindCi( Abc_Ntk_t * pNtk, char * pName );
-extern Abc_Obj_t *        Abc_NtkFindCo( Abc_Ntk_t * pNtk, char * pName );
-extern Abc_Obj_t *        Abc_NtkFindOrCreateNet( Abc_Ntk_t * pNtk, char * pName );
-extern Abc_Obj_t *        Abc_NtkCreateNodeConst0( Abc_Ntk_t * pNtk );
-extern Abc_Obj_t *        Abc_NtkCreateNodeConst1( Abc_Ntk_t * pNtk );
-extern Abc_Obj_t *        Abc_NtkCreateNodeInv( Abc_Ntk_t * pNtk, Abc_Obj_t * pFanin );
-extern Abc_Obj_t *        Abc_NtkCreateNodeBuf( Abc_Ntk_t * pNtk, Abc_Obj_t * pFanin );
-extern Abc_Obj_t *        Abc_NtkCreateNodeAnd( Abc_Ntk_t * pNtk, Vec_Ptr_t * vFanins );
-extern Abc_Obj_t *        Abc_NtkCreateNodeOr( Abc_Ntk_t * pNtk, Vec_Ptr_t * vFanins );
-extern Abc_Obj_t *        Abc_NtkCreateNodeExor( Abc_Ntk_t * pNtk, Vec_Ptr_t * vFanins );
-extern Abc_Obj_t *        Abc_NtkCreateNodeMux( Abc_Ntk_t * pNtk, Abc_Obj_t * pNodeC, Abc_Obj_t * pNode1, Abc_Obj_t * pNode0 );
-extern bool               Abc_NodeIsConst( Abc_Obj_t * pNode );
-extern bool               Abc_NodeIsConst0( Abc_Obj_t * pNode );    
-extern bool               Abc_NodeIsConst1( Abc_Obj_t * pNode );    
-extern bool               Abc_NodeIsBuf( Abc_Obj_t * pNode );    
-extern bool               Abc_NodeIsInv( Abc_Obj_t * pNode );    
-extern void               Abc_NodeComplement( Abc_Obj_t * pNode );
+extern ABC_DLL Abc_Obj_t *        Abc_ObjAlloc( Abc_Ntk_t * pNtk, Abc_ObjType_t Type );
+extern ABC_DLL void               Abc_ObjRecycle( Abc_Obj_t * pObj );
+extern ABC_DLL Abc_Obj_t *        Abc_NtkCreateObj( Abc_Ntk_t * pNtk, Abc_ObjType_t Type );
+extern ABC_DLL void               Abc_NtkDeleteObj( Abc_Obj_t * pObj );
+extern ABC_DLL void               Abc_NtkDeleteObj_rec( Abc_Obj_t * pObj, int fOnlyNodes );
+extern ABC_DLL void               Abc_NtkDeleteAll_rec( Abc_Obj_t * pObj );
+extern ABC_DLL Abc_Obj_t *        Abc_NtkDupObj( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj, int fCopyName );
+extern ABC_DLL Abc_Obj_t *        Abc_NtkDupBox( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pBox, int fCopyName );
+extern ABC_DLL Abc_Obj_t *        Abc_NtkCloneObj( Abc_Obj_t * pNode );
+extern ABC_DLL Abc_Obj_t *        Abc_NtkFindNode( Abc_Ntk_t * pNtk, char * pName );
+extern ABC_DLL Abc_Obj_t *        Abc_NtkFindNet( Abc_Ntk_t * pNtk, char * pName );
+extern ABC_DLL Abc_Obj_t *        Abc_NtkFindCi( Abc_Ntk_t * pNtk, char * pName );
+extern ABC_DLL Abc_Obj_t *        Abc_NtkFindCo( Abc_Ntk_t * pNtk, char * pName );
+extern ABC_DLL Abc_Obj_t *        Abc_NtkFindOrCreateNet( Abc_Ntk_t * pNtk, char * pName );
+extern ABC_DLL Abc_Obj_t *        Abc_NtkCreateNodeConst0( Abc_Ntk_t * pNtk );
+extern ABC_DLL Abc_Obj_t *        Abc_NtkCreateNodeConst1( Abc_Ntk_t * pNtk );
+extern ABC_DLL Abc_Obj_t *        Abc_NtkCreateNodeInv( Abc_Ntk_t * pNtk, Abc_Obj_t * pFanin );
+extern ABC_DLL Abc_Obj_t *        Abc_NtkCreateNodeBuf( Abc_Ntk_t * pNtk, Abc_Obj_t * pFanin );
+extern ABC_DLL Abc_Obj_t *        Abc_NtkCreateNodeAnd( Abc_Ntk_t * pNtk, Vec_Ptr_t * vFanins );
+extern ABC_DLL Abc_Obj_t *        Abc_NtkCreateNodeOr( Abc_Ntk_t * pNtk, Vec_Ptr_t * vFanins );
+extern ABC_DLL Abc_Obj_t *        Abc_NtkCreateNodeExor( Abc_Ntk_t * pNtk, Vec_Ptr_t * vFanins );
+extern ABC_DLL Abc_Obj_t *        Abc_NtkCreateNodeMux( Abc_Ntk_t * pNtk, Abc_Obj_t * pNodeC, Abc_Obj_t * pNode1, Abc_Obj_t * pNode0 );
+extern ABC_DLL bool               Abc_NodeIsConst( Abc_Obj_t * pNode );
+extern ABC_DLL bool               Abc_NodeIsConst0( Abc_Obj_t * pNode );    
+extern ABC_DLL bool               Abc_NodeIsConst1( Abc_Obj_t * pNode );    
+extern ABC_DLL bool               Abc_NodeIsBuf( Abc_Obj_t * pNode );    
+extern ABC_DLL bool               Abc_NodeIsInv( Abc_Obj_t * pNode );    
+extern ABC_DLL void               Abc_NodeComplement( Abc_Obj_t * pNode );
 /*=== abcPrint.c ==========================================================*/
-extern void               Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored, int fSaveBest, int fDumpResult, int fUseLutLib );
-extern void               Abc_NtkPrintIo( FILE * pFile, Abc_Ntk_t * pNtk );
-extern void               Abc_NtkPrintLatch( FILE * pFile, Abc_Ntk_t * pNtk );
-extern void               Abc_NtkPrintFanio( FILE * pFile, Abc_Ntk_t * pNtk );
-extern void               Abc_NtkPrintFanioNew( FILE * pFile, Abc_Ntk_t * pNtk );
-extern void               Abc_NodePrintFanio( FILE * pFile, Abc_Obj_t * pNode );
-extern void               Abc_NtkPrintFactor( FILE * pFile, Abc_Ntk_t * pNtk, int fUseRealNames );
-extern void               Abc_NodePrintFactor( FILE * pFile, Abc_Obj_t * pNode, int fUseRealNames );
-extern void               Abc_NtkPrintLevel( FILE * pFile, Abc_Ntk_t * pNtk, int fProfile, int fListNodes );
-extern void               Abc_NodePrintLevel( FILE * pFile, Abc_Obj_t * pNode );
-extern void               Abc_NtkPrintSkews( FILE * pFile, Abc_Ntk_t * pNtk, int fPrintAll );
-extern void               Abc_ObjPrint( FILE * pFile, Abc_Obj_t * pObj );
+extern ABC_DLL void               Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored, int fSaveBest, int fDumpResult, int fUseLutLib );
+extern ABC_DLL void               Abc_NtkPrintIo( FILE * pFile, Abc_Ntk_t * pNtk );
+extern ABC_DLL void               Abc_NtkPrintLatch( FILE * pFile, Abc_Ntk_t * pNtk );
+extern ABC_DLL void               Abc_NtkPrintFanio( FILE * pFile, Abc_Ntk_t * pNtk );
+extern ABC_DLL void               Abc_NtkPrintFanioNew( FILE * pFile, Abc_Ntk_t * pNtk );
+extern ABC_DLL void               Abc_NodePrintFanio( FILE * pFile, Abc_Obj_t * pNode );
+extern ABC_DLL void               Abc_NtkPrintFactor( FILE * pFile, Abc_Ntk_t * pNtk, int fUseRealNames );
+extern ABC_DLL void               Abc_NodePrintFactor( FILE * pFile, Abc_Obj_t * pNode, int fUseRealNames );
+extern ABC_DLL void               Abc_NtkPrintLevel( FILE * pFile, Abc_Ntk_t * pNtk, int fProfile, int fListNodes );
+extern ABC_DLL void               Abc_NodePrintLevel( FILE * pFile, Abc_Obj_t * pNode );
+extern ABC_DLL void               Abc_NtkPrintSkews( FILE * pFile, Abc_Ntk_t * pNtk, int fPrintAll );
+extern ABC_DLL void               Abc_ObjPrint( FILE * pFile, Abc_Obj_t * pObj );
 /*=== abcProve.c ==========================================================*/
-extern int                Abc_NtkMiterProve( Abc_Ntk_t ** ppNtk, void * pParams );
-extern int                Abc_NtkIvyProve( Abc_Ntk_t ** ppNtk, void * pPars );
+extern ABC_DLL int                Abc_NtkMiterProve( Abc_Ntk_t ** ppNtk, void * pParams );
+extern ABC_DLL int                Abc_NtkIvyProve( Abc_Ntk_t ** ppNtk, void * pPars );
 /*=== abcRec.c ==========================================================*/
-extern void               Abc_NtkRecStart( Abc_Ntk_t * pNtk, int nVars, int nCuts );
-extern void               Abc_NtkRecStop();
-extern void               Abc_NtkRecAdd( Abc_Ntk_t * pNtk );
-extern void               Abc_NtkRecPs();
-extern void               Abc_NtkRecFilter( int iVar, int iPlus );
-extern Abc_Ntk_t *        Abc_NtkRecUse();
-extern int                Abc_NtkRecIsRunning();
-extern int                Abc_NtkRecVarNum();
-extern Vec_Int_t *        Abc_NtkRecMemory();
-extern int                Abc_NtkRecStrashNode( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj, unsigned * pTruth, int nVars );
+extern ABC_DLL void               Abc_NtkRecStart( Abc_Ntk_t * pNtk, int nVars, int nCuts );
+extern ABC_DLL void               Abc_NtkRecStop();
+extern ABC_DLL void               Abc_NtkRecAdd( Abc_Ntk_t * pNtk );
+extern ABC_DLL void               Abc_NtkRecPs();
+extern ABC_DLL void               Abc_NtkRecFilter( int iVar, int iPlus );
+extern ABC_DLL Abc_Ntk_t *        Abc_NtkRecUse();
+extern ABC_DLL int                Abc_NtkRecIsRunning();
+extern ABC_DLL int                Abc_NtkRecVarNum();
+extern ABC_DLL Vec_Int_t *        Abc_NtkRecMemory();
+extern ABC_DLL int                Abc_NtkRecStrashNode( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj, unsigned * pTruth, int nVars );
 /*=== abcReconv.c ==========================================================*/
-extern Abc_ManCut_t *     Abc_NtkManCutStart( int nNodeSizeMax, int nConeSizeMax, int nNodeFanStop, int nConeFanStop );
-extern void               Abc_NtkManCutStop( Abc_ManCut_t * p );
-extern Vec_Ptr_t *        Abc_NtkManCutReadCutLarge( Abc_ManCut_t * p );
-extern Vec_Ptr_t *        Abc_NtkManCutReadCutSmall( Abc_ManCut_t * p );
-extern Vec_Ptr_t *        Abc_NtkManCutReadVisited( Abc_ManCut_t * p );
-extern Vec_Ptr_t *        Abc_NodeFindCut( Abc_ManCut_t * p, Abc_Obj_t * pRoot, bool fContain );
-extern void               Abc_NodeConeCollect( Abc_Obj_t ** ppRoots, int nRoots, Vec_Ptr_t * vFanins, Vec_Ptr_t * vVisited, int fIncludeFanins );
-extern DdNode *           Abc_NodeConeBdd( DdManager * dd, DdNode ** pbVars, Abc_Obj_t * pNode, Vec_Ptr_t * vFanins, Vec_Ptr_t * vVisited );
-extern DdNode *           Abc_NodeConeDcs( DdManager * dd, DdNode ** pbVarsX, DdNode ** pbVarsY, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vRoots, Vec_Ptr_t * vVisited );
-extern Vec_Ptr_t *        Abc_NodeCollectTfoCands( Abc_ManCut_t * p, Abc_Obj_t * pRoot, Vec_Ptr_t * vFanins, int LevelMax );
+extern ABC_DLL Abc_ManCut_t *     Abc_NtkManCutStart( int nNodeSizeMax, int nConeSizeMax, int nNodeFanStop, int nConeFanStop );
+extern ABC_DLL void               Abc_NtkManCutStop( Abc_ManCut_t * p );
+extern ABC_DLL Vec_Ptr_t *        Abc_NtkManCutReadCutLarge( Abc_ManCut_t * p );
+extern ABC_DLL Vec_Ptr_t *        Abc_NtkManCutReadCutSmall( Abc_ManCut_t * p );
+extern ABC_DLL Vec_Ptr_t *        Abc_NtkManCutReadVisited( Abc_ManCut_t * p );
+extern ABC_DLL Vec_Ptr_t *        Abc_NodeFindCut( Abc_ManCut_t * p, Abc_Obj_t * pRoot, bool fContain );
+extern ABC_DLL void               Abc_NodeConeCollect( Abc_Obj_t ** ppRoots, int nRoots, Vec_Ptr_t * vFanins, Vec_Ptr_t * vVisited, int fIncludeFanins );
+extern ABC_DLL DdNode *           Abc_NodeConeBdd( DdManager * dd, DdNode ** pbVars, Abc_Obj_t * pNode, Vec_Ptr_t * vFanins, Vec_Ptr_t * vVisited );
+extern ABC_DLL DdNode *           Abc_NodeConeDcs( DdManager * dd, DdNode ** pbVarsX, DdNode ** pbVarsY, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vRoots, Vec_Ptr_t * vVisited );
+extern ABC_DLL Vec_Ptr_t *        Abc_NodeCollectTfoCands( Abc_ManCut_t * p, Abc_Obj_t * pRoot, Vec_Ptr_t * vFanins, int LevelMax );
 /*=== abcRefs.c ==========================================================*/
-extern int                Abc_NodeMffcSize( Abc_Obj_t * pNode );
-extern int                Abc_NodeMffcSizeSupp( Abc_Obj_t * pNode );
-extern int                Abc_NodeMffcSizeStop( Abc_Obj_t * pNode );
-extern int                Abc_NodeMffcLabelAig( Abc_Obj_t * pNode );
-extern int                Abc_NodeMffcLabel( Abc_Obj_t * pNode );
-extern void               Abc_NodeMffsConeSupp( Abc_Obj_t * pNode, Vec_Ptr_t * vCone, Vec_Ptr_t * vSupp );
-extern int                Abc_NodeDeref_rec( Abc_Obj_t * pNode );
-extern int                Abc_NodeRef_rec( Abc_Obj_t * pNode );
+extern ABC_DLL int                Abc_NodeMffcSize( Abc_Obj_t * pNode );
+extern ABC_DLL int                Abc_NodeMffcSizeSupp( Abc_Obj_t * pNode );
+extern ABC_DLL int                Abc_NodeMffcSizeStop( Abc_Obj_t * pNode );
+extern ABC_DLL int                Abc_NodeMffcLabelAig( Abc_Obj_t * pNode );
+extern ABC_DLL int                Abc_NodeMffcLabel( Abc_Obj_t * pNode );
+extern ABC_DLL void               Abc_NodeMffsConeSupp( Abc_Obj_t * pNode, Vec_Ptr_t * vCone, Vec_Ptr_t * vSupp );
+extern ABC_DLL int                Abc_NodeDeref_rec( Abc_Obj_t * pNode );
+extern ABC_DLL int                Abc_NodeRef_rec( Abc_Obj_t * pNode );
 /*=== abcRefactor.c ==========================================================*/
-extern int                Abc_NtkRefactor( Abc_Ntk_t * pNtk, int nNodeSizeMax, int nConeSizeMax, bool fUpdateLevel, bool fUseZeros, bool fUseDcs, bool fVerbose );
+extern ABC_DLL int                Abc_NtkRefactor( Abc_Ntk_t * pNtk, int nNodeSizeMax, int nConeSizeMax, bool fUpdateLevel, bool fUseZeros, bool fUseDcs, bool fVerbose );
 /*=== abcRewrite.c ==========================================================*/
-extern int                Abc_NtkRewrite( Abc_Ntk_t * pNtk, int fUpdateLevel, int fUseZeros, int fVerbose, int fVeryVerbose, int fPlaceEnable );
+extern ABC_DLL int                Abc_NtkRewrite( Abc_Ntk_t * pNtk, int fUpdateLevel, int fUseZeros, int fVerbose, int fVeryVerbose, int fPlaceEnable );
 /*=== abcSat.c ==========================================================*/
-extern int                Abc_NtkMiterSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fVerbose, sint64 * pNumConfs, sint64 * pNumInspects );
-extern void *             Abc_NtkMiterSatCreate( Abc_Ntk_t * pNtk, int fAllPrimes );
+extern ABC_DLL int                Abc_NtkMiterSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fVerbose, sint64 * pNumConfs, sint64 * pNumInspects );
+extern ABC_DLL void *             Abc_NtkMiterSatCreate( Abc_Ntk_t * pNtk, int fAllPrimes );
 /*=== abcSop.c ==========================================================*/
-extern char *             Abc_SopRegister( Extra_MmFlex_t * pMan, char * pName );
-extern char *             Abc_SopStart( Extra_MmFlex_t * pMan, int nCubes, int nVars );
-extern char *             Abc_SopCreateConst0( Extra_MmFlex_t * pMan );
-extern char *             Abc_SopCreateConst1( Extra_MmFlex_t * pMan );
-extern char *             Abc_SopCreateAnd2( Extra_MmFlex_t * pMan, int fCompl0, int fCompl1 );
-extern char *             Abc_SopCreateAnd( Extra_MmFlex_t * pMan, int nVars, int * pfCompl );
-extern char *             Abc_SopCreateNand( Extra_MmFlex_t * pMan, int nVars );
-extern char *             Abc_SopCreateOr( Extra_MmFlex_t * pMan, int nVars, int * pfCompl );
-extern char *             Abc_SopCreateOrMultiCube( Extra_MmFlex_t * pMan, int nVars, int * pfCompl );
-extern char *             Abc_SopCreateNor( Extra_MmFlex_t * pMan, int nVars );
-extern char *             Abc_SopCreateXor( Extra_MmFlex_t * pMan, int nVars );
-extern char *             Abc_SopCreateXorSpecial( Extra_MmFlex_t * pMan, int nVars );
-extern char *             Abc_SopCreateNxor( Extra_MmFlex_t * pMan, int nVars );
-extern char *             Abc_SopCreateMux( Extra_MmFlex_t * pMan );
-extern char *             Abc_SopCreateInv( Extra_MmFlex_t * pMan );
-extern char *             Abc_SopCreateBuf( Extra_MmFlex_t * pMan );
-extern char *             Abc_SopCreateFromTruth( Extra_MmFlex_t * pMan, int nVars, unsigned * pTruth );
-extern char *             Abc_SopCreateFromIsop( Extra_MmFlex_t * pMan, int nVars, Vec_Int_t * vCover );
-extern int                Abc_SopGetCubeNum( char * pSop );
-extern int                Abc_SopGetLitNum( char * pSop );
-extern int                Abc_SopGetVarNum( char * pSop );
-extern int                Abc_SopGetPhase( char * pSop );
-extern int                Abc_SopGetIthCareLit( char * pSop, int i );
-extern void               Abc_SopComplement( char * pSop );
-extern bool               Abc_SopIsComplement( char * pSop );
-extern bool               Abc_SopIsConst0( char * pSop );
-extern bool               Abc_SopIsConst1( char * pSop );
-extern bool               Abc_SopIsBuf( char * pSop );
-extern bool               Abc_SopIsInv( char * pSop );
-extern bool               Abc_SopIsAndType( char * pSop );
-extern bool               Abc_SopIsOrType( char * pSop );
-extern int                Abc_SopIsExorType( char * pSop );
-extern bool               Abc_SopCheck( char * pSop, int nFanins );
-extern char *             Abc_SopFromTruthBin( char * pTruth );
-extern char *             Abc_SopFromTruthHex( char * pTruth );
-extern char *             Abc_SopEncoderPos( Extra_MmFlex_t * pMan, int iValue, int nValues );
-extern char *             Abc_SopEncoderLog( Extra_MmFlex_t * pMan, int iBit, int nValues );
-extern char *             Abc_SopDecoderPos( Extra_MmFlex_t * pMan, int nValues );
-extern char *             Abc_SopDecoderLog( Extra_MmFlex_t * pMan, int nValues );
+extern ABC_DLL char *             Abc_SopRegister( Extra_MmFlex_t * pMan, char * pName );
+extern ABC_DLL char *             Abc_SopStart( Extra_MmFlex_t * pMan, int nCubes, int nVars );
+extern ABC_DLL char *             Abc_SopCreateConst0( Extra_MmFlex_t * pMan );
+extern ABC_DLL char *             Abc_SopCreateConst1( Extra_MmFlex_t * pMan );
+extern ABC_DLL char *             Abc_SopCreateAnd2( Extra_MmFlex_t * pMan, int fCompl0, int fCompl1 );
+extern ABC_DLL char *             Abc_SopCreateAnd( Extra_MmFlex_t * pMan, int nVars, int * pfCompl );
+extern ABC_DLL char *             Abc_SopCreateNand( Extra_MmFlex_t * pMan, int nVars );
+extern ABC_DLL char *             Abc_SopCreateOr( Extra_MmFlex_t * pMan, int nVars, int * pfCompl );
+extern ABC_DLL char *             Abc_SopCreateOrMultiCube( Extra_MmFlex_t * pMan, int nVars, int * pfCompl );
+extern ABC_DLL char *             Abc_SopCreateNor( Extra_MmFlex_t * pMan, int nVars );
+extern ABC_DLL char *             Abc_SopCreateXor( Extra_MmFlex_t * pMan, int nVars );
+extern ABC_DLL char *             Abc_SopCreateXorSpecial( Extra_MmFlex_t * pMan, int nVars );
+extern ABC_DLL char *             Abc_SopCreateNxor( Extra_MmFlex_t * pMan, int nVars );
+extern ABC_DLL char *             Abc_SopCreateMux( Extra_MmFlex_t * pMan );
+extern ABC_DLL char *             Abc_SopCreateInv( Extra_MmFlex_t * pMan );
+extern ABC_DLL char *             Abc_SopCreateBuf( Extra_MmFlex_t * pMan );
+extern ABC_DLL char *             Abc_SopCreateFromTruth( Extra_MmFlex_t * pMan, int nVars, unsigned * pTruth );
+extern ABC_DLL char *             Abc_SopCreateFromIsop( Extra_MmFlex_t * pMan, int nVars, Vec_Int_t * vCover );
+extern ABC_DLL int                Abc_SopGetCubeNum( char * pSop );
+extern ABC_DLL int                Abc_SopGetLitNum( char * pSop );
+extern ABC_DLL int                Abc_SopGetVarNum( char * pSop );
+extern ABC_DLL int                Abc_SopGetPhase( char * pSop );
+extern ABC_DLL int                Abc_SopGetIthCareLit( char * pSop, int i );
+extern ABC_DLL void               Abc_SopComplement( char * pSop );
+extern ABC_DLL bool               Abc_SopIsComplement( char * pSop );
+extern ABC_DLL bool               Abc_SopIsConst0( char * pSop );
+extern ABC_DLL bool               Abc_SopIsConst1( char * pSop );
+extern ABC_DLL bool               Abc_SopIsBuf( char * pSop );
+extern ABC_DLL bool               Abc_SopIsInv( char * pSop );
+extern ABC_DLL bool               Abc_SopIsAndType( char * pSop );
+extern ABC_DLL bool               Abc_SopIsOrType( char * pSop );
+extern ABC_DLL int                Abc_SopIsExorType( char * pSop );
+extern ABC_DLL bool               Abc_SopCheck( char * pSop, int nFanins );
+extern ABC_DLL char *             Abc_SopFromTruthBin( char * pTruth );
+extern ABC_DLL char *             Abc_SopFromTruthHex( char * pTruth );
+extern ABC_DLL char *             Abc_SopEncoderPos( Extra_MmFlex_t * pMan, int iValue, int nValues );
+extern ABC_DLL char *             Abc_SopEncoderLog( Extra_MmFlex_t * pMan, int iBit, int nValues );
+extern ABC_DLL char *             Abc_SopDecoderPos( Extra_MmFlex_t * pMan, int nValues );
+extern ABC_DLL char *             Abc_SopDecoderLog( Extra_MmFlex_t * pMan, int nValues );
 /*=== abcStrash.c ==========================================================*/
-extern Abc_Ntk_t *        Abc_NtkStrash( Abc_Ntk_t * pNtk, int fAllNodes, int fCleanup, int fRecord );
-extern Abc_Obj_t *        Abc_NodeStrash( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode, int fRecord );
-extern int                Abc_NtkAppend( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fAddPos );
-extern Abc_Ntk_t *        Abc_NtkTopmost( Abc_Ntk_t * pNtk, int nLevels );
+extern ABC_DLL Abc_Ntk_t *        Abc_NtkStrash( Abc_Ntk_t * pNtk, int fAllNodes, int fCleanup, int fRecord );
+extern ABC_DLL Abc_Obj_t *        Abc_NodeStrash( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode, int fRecord );
+extern ABC_DLL int                Abc_NtkAppend( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fAddPos );
+extern ABC_DLL Abc_Ntk_t *        Abc_NtkTopmost( Abc_Ntk_t * pNtk, int nLevels );
 /*=== abcSweep.c ==========================================================*/
-extern int                Abc_NtkSweep( Abc_Ntk_t * pNtk, int fVerbose );
-extern int                Abc_NtkCleanup( Abc_Ntk_t * pNtk, int fVerbose );
-extern int                Abc_NtkCleanupSeq( Abc_Ntk_t * pNtk, int fLatchSweep, int fAutoSweep, int fVerbose );
+extern ABC_DLL int                Abc_NtkSweep( Abc_Ntk_t * pNtk, int fVerbose );
+extern ABC_DLL int                Abc_NtkCleanup( Abc_Ntk_t * pNtk, int fVerbose );
+extern ABC_DLL int                Abc_NtkCleanupSeq( Abc_Ntk_t * pNtk, int fLatchSweep, int fAutoSweep, int fVerbose );
 /*=== abcTiming.c ==========================================================*/
-extern Abc_Time_t *       Abc_NodeReadArrival( Abc_Obj_t * pNode );
-extern Abc_Time_t *       Abc_NodeReadRequired( Abc_Obj_t * pNode );
-extern Abc_Time_t *       Abc_NtkReadDefaultArrival( Abc_Ntk_t * pNtk );
-extern Abc_Time_t *       Abc_NtkReadDefaultRequired( Abc_Ntk_t * pNtk );
-extern void               Abc_NtkTimeSetDefaultArrival( Abc_Ntk_t * pNtk, float Rise, float Fall );
-extern void               Abc_NtkTimeSetDefaultRequired( Abc_Ntk_t * pNtk, float Rise, float Fall );
-extern void               Abc_NtkTimeSetArrival( Abc_Ntk_t * pNtk, int ObjId, float Rise, float Fall );
-extern void               Abc_NtkTimeSetRequired( Abc_Ntk_t * pNtk, int ObjId, float Rise, float Fall );
-extern void               Abc_NtkTimeInitialize( Abc_Ntk_t * pNtk );
-extern void               Abc_ManTimeStop( Abc_ManTime_t * p );
-extern void               Abc_ManTimeDup( Abc_Ntk_t * pNtkOld, Abc_Ntk_t * pNtkNew );
-extern void               Abc_NtkSetNodeLevelsArrival( Abc_Ntk_t * pNtk );
-extern float *            Abc_NtkGetCiArrivalFloats( Abc_Ntk_t * pNtk );
-extern Abc_Time_t *       Abc_NtkGetCiArrivalTimes( Abc_Ntk_t * pNtk );
-extern float              Abc_NtkDelayTrace( Abc_Ntk_t * pNtk );
-extern int                Abc_ObjLevelNew( Abc_Obj_t * pObj );
-extern int                Abc_ObjReverseLevelNew( Abc_Obj_t * pObj );
-extern int                Abc_ObjRequiredLevel( Abc_Obj_t * pObj );
-extern int                Abc_ObjReverseLevel( Abc_Obj_t * pObj );
-extern void               Abc_ObjSetReverseLevel( Abc_Obj_t * pObj, int LevelR );
-extern void               Abc_NtkStartReverseLevels( Abc_Ntk_t * pNtk, int nMaxLevelIncrease );
-extern void               Abc_NtkStopReverseLevels( Abc_Ntk_t * pNtk );
-extern void               Abc_NtkUpdateLevel( Abc_Obj_t * pObjNew, Vec_Vec_t * vLevels );
-extern void               Abc_NtkUpdateReverseLevel( Abc_Obj_t * pObjNew, Vec_Vec_t * vLevels );
-extern void               Abc_NtkUpdate( Abc_Obj_t * pObj, Abc_Obj_t * pObjNew, Vec_Vec_t * vLevels );
+extern ABC_DLL Abc_Time_t *       Abc_NodeReadArrival( Abc_Obj_t * pNode );
+extern ABC_DLL Abc_Time_t *       Abc_NodeReadRequired( Abc_Obj_t * pNode );
+extern ABC_DLL Abc_Time_t *       Abc_NtkReadDefaultArrival( Abc_Ntk_t * pNtk );
+extern ABC_DLL Abc_Time_t *       Abc_NtkReadDefaultRequired( Abc_Ntk_t * pNtk );
+extern ABC_DLL void               Abc_NtkTimeSetDefaultArrival( Abc_Ntk_t * pNtk, float Rise, float Fall );
+extern ABC_DLL void               Abc_NtkTimeSetDefaultRequired( Abc_Ntk_t * pNtk, float Rise, float Fall );
+extern ABC_DLL void               Abc_NtkTimeSetArrival( Abc_Ntk_t * pNtk, int ObjId, float Rise, float Fall );
+extern ABC_DLL void               Abc_NtkTimeSetRequired( Abc_Ntk_t * pNtk, int ObjId, float Rise, float Fall );
+extern ABC_DLL void               Abc_NtkTimeInitialize( Abc_Ntk_t * pNtk );
+extern ABC_DLL void               Abc_ManTimeStop( Abc_ManTime_t * p );
+extern ABC_DLL void               Abc_ManTimeDup( Abc_Ntk_t * pNtkOld, Abc_Ntk_t * pNtkNew );
+extern ABC_DLL void               Abc_NtkSetNodeLevelsArrival( Abc_Ntk_t * pNtk );
+extern ABC_DLL float *            Abc_NtkGetCiArrivalFloats( Abc_Ntk_t * pNtk );
+extern ABC_DLL Abc_Time_t *       Abc_NtkGetCiArrivalTimes( Abc_Ntk_t * pNtk );
+extern ABC_DLL float              Abc_NtkDelayTrace( Abc_Ntk_t * pNtk );
+extern ABC_DLL int                Abc_ObjLevelNew( Abc_Obj_t * pObj );
+extern ABC_DLL int                Abc_ObjReverseLevelNew( Abc_Obj_t * pObj );
+extern ABC_DLL int                Abc_ObjRequiredLevel( Abc_Obj_t * pObj );
+extern ABC_DLL int                Abc_ObjReverseLevel( Abc_Obj_t * pObj );
+extern ABC_DLL void               Abc_ObjSetReverseLevel( Abc_Obj_t * pObj, int LevelR );
+extern ABC_DLL void               Abc_NtkStartReverseLevels( Abc_Ntk_t * pNtk, int nMaxLevelIncrease );
+extern ABC_DLL void               Abc_NtkStopReverseLevels( Abc_Ntk_t * pNtk );
+extern ABC_DLL void               Abc_NtkUpdateLevel( Abc_Obj_t * pObjNew, Vec_Vec_t * vLevels );
+extern ABC_DLL void               Abc_NtkUpdateReverseLevel( Abc_Obj_t * pObjNew, Vec_Vec_t * vLevels );
+extern ABC_DLL void               Abc_NtkUpdate( Abc_Obj_t * pObj, Abc_Obj_t * pObjNew, Vec_Vec_t * vLevels );
 /*=== abcUtil.c ==========================================================*/
-extern void *             Abc_NtkAttrFree( Abc_Ntk_t * pNtk, int Attr, int fFreeMan );
-extern void               Abc_NtkIncrementTravId( Abc_Ntk_t * pNtk );
-extern void               Abc_NtkOrderCisCos( Abc_Ntk_t * pNtk );
-extern int                Abc_NtkGetCubeNum( Abc_Ntk_t * pNtk );
-extern int                Abc_NtkGetCubePairNum( Abc_Ntk_t * pNtk );
-extern int                Abc_NtkGetLitNum( Abc_Ntk_t * pNtk );
-extern int                Abc_NtkGetLitFactNum( Abc_Ntk_t * pNtk );
-extern int                Abc_NtkGetBddNodeNum( Abc_Ntk_t * pNtk );
-extern int                Abc_NtkGetAigNodeNum( Abc_Ntk_t * pNtk );
-extern int                Abc_NtkGetClauseNum( Abc_Ntk_t * pNtk );
-extern double             Abc_NtkGetMappedArea( Abc_Ntk_t * pNtk );
-extern int                Abc_NtkGetExorNum( Abc_Ntk_t * pNtk );
-extern int                Abc_NtkGetMuxNum( Abc_Ntk_t * pNtk );
-extern int                Abc_NtkGetChoiceNum( Abc_Ntk_t * pNtk );
-extern int                Abc_NtkGetFaninMax( Abc_Ntk_t * pNtk );
-extern int                Abc_NtkGetTotalFanins( Abc_Ntk_t * pNtk );
-extern void               Abc_NtkCleanCopy( Abc_Ntk_t * pNtk );
-extern void               Abc_NtkCleanData( Abc_Ntk_t * pNtk );
-extern void               Abc_NtkCleanEquiv( Abc_Ntk_t * pNtk );
-extern int                Abc_NtkCountCopy( Abc_Ntk_t * pNtk );
-extern Vec_Ptr_t *        Abc_NtkSaveCopy( Abc_Ntk_t * pNtk );
-extern void               Abc_NtkLoadCopy( Abc_Ntk_t * pNtk, Vec_Ptr_t * vCopies );
-extern void               Abc_NtkCleanNext( Abc_Ntk_t * pNtk );
-extern void               Abc_NtkCleanMarkA( Abc_Ntk_t * pNtk );
-extern Abc_Obj_t *        Abc_NodeFindCoFanout( Abc_Obj_t * pNode );
-extern Abc_Obj_t *        Abc_NodeFindNonCoFanout( Abc_Obj_t * pNode );
-extern Abc_Obj_t *        Abc_NodeHasUniqueCoFanout( Abc_Obj_t * pNode );
-extern bool               Abc_NtkLogicHasSimpleCos( Abc_Ntk_t * pNtk );
-extern int                Abc_NtkLogicMakeSimpleCos( Abc_Ntk_t * pNtk, bool fDuplicate );
-extern void               Abc_VecObjPushUniqueOrderByLevel( Vec_Ptr_t * p, Abc_Obj_t * pNode );
-extern bool               Abc_NodeIsExorType( Abc_Obj_t * pNode );
-extern bool               Abc_NodeIsMuxType( Abc_Obj_t * pNode );
-extern bool               Abc_NodeIsMuxControlType( Abc_Obj_t * pNode );
-extern Abc_Obj_t *        Abc_NodeRecognizeMux( Abc_Obj_t * pNode, Abc_Obj_t ** ppNodeT, Abc_Obj_t ** ppNodeE );
-extern int                Abc_NtkPrepareTwoNtks( FILE * pErr, Abc_Ntk_t * pNtk, char ** argv, int argc, Abc_Ntk_t ** ppNtk1, Abc_Ntk_t ** ppNtk2, int * pfDelete1, int * pfDelete2 );
-extern void               Abc_NodeCollectFanins( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes );
-extern void               Abc_NodeCollectFanouts( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes );
-extern Vec_Ptr_t *        Abc_NtkCollectLatches( Abc_Ntk_t * pNtk );
-extern int                Abc_NodeCompareLevelsIncrease( Abc_Obj_t ** pp1, Abc_Obj_t ** pp2 );
-extern int                Abc_NodeCompareLevelsDecrease( Abc_Obj_t ** pp1, Abc_Obj_t ** pp2 );
-extern Vec_Int_t *        Abc_NtkFanoutCounts( Abc_Ntk_t * pNtk );
-extern Vec_Ptr_t *        Abc_NtkCollectObjects( Abc_Ntk_t * pNtk );
-extern Vec_Int_t *        Abc_NtkGetCiIds( Abc_Ntk_t * pNtk );
-extern void               Abc_NtkReassignIds( Abc_Ntk_t * pNtk );
-extern int                Abc_ObjPointerCompare( void ** pp1, void ** pp2 );
-extern void               Abc_NtkTransferCopy( Abc_Ntk_t * pNtk );
+extern ABC_DLL void *             Abc_NtkAttrFree( Abc_Ntk_t * pNtk, int Attr, int fFreeMan );
+extern ABC_DLL void               Abc_NtkIncrementTravId( Abc_Ntk_t * pNtk );
+extern ABC_DLL void               Abc_NtkOrderCisCos( Abc_Ntk_t * pNtk );
+extern ABC_DLL int                Abc_NtkGetCubeNum( Abc_Ntk_t * pNtk );
+extern ABC_DLL int                Abc_NtkGetCubePairNum( Abc_Ntk_t * pNtk );
+extern ABC_DLL int                Abc_NtkGetLitNum( Abc_Ntk_t * pNtk );
+extern ABC_DLL int                Abc_NtkGetLitFactNum( Abc_Ntk_t * pNtk );
+extern ABC_DLL int                Abc_NtkGetBddNodeNum( Abc_Ntk_t * pNtk );
+extern ABC_DLL int                Abc_NtkGetAigNodeNum( Abc_Ntk_t * pNtk );
+extern ABC_DLL int                Abc_NtkGetClauseNum( Abc_Ntk_t * pNtk );
+extern ABC_DLL double             Abc_NtkGetMappedArea( Abc_Ntk_t * pNtk );
+extern ABC_DLL int                Abc_NtkGetExorNum( Abc_Ntk_t * pNtk );
+extern ABC_DLL int                Abc_NtkGetMuxNum( Abc_Ntk_t * pNtk );
+extern ABC_DLL int                Abc_NtkGetChoiceNum( Abc_Ntk_t * pNtk );
+extern ABC_DLL int                Abc_NtkGetFaninMax( Abc_Ntk_t * pNtk );
+extern ABC_DLL int                Abc_NtkGetTotalFanins( Abc_Ntk_t * pNtk );
+extern ABC_DLL void               Abc_NtkCleanCopy( Abc_Ntk_t * pNtk );
+extern ABC_DLL void               Abc_NtkCleanData( Abc_Ntk_t * pNtk );
+extern ABC_DLL void               Abc_NtkCleanEquiv( Abc_Ntk_t * pNtk );
+extern ABC_DLL int                Abc_NtkCountCopy( Abc_Ntk_t * pNtk );
+extern ABC_DLL Vec_Ptr_t *        Abc_NtkSaveCopy( Abc_Ntk_t * pNtk );
+extern ABC_DLL void               Abc_NtkLoadCopy( Abc_Ntk_t * pNtk, Vec_Ptr_t * vCopies );
+extern ABC_DLL void               Abc_NtkCleanNext( Abc_Ntk_t * pNtk );
+extern ABC_DLL void               Abc_NtkCleanMarkA( Abc_Ntk_t * pNtk );
+extern ABC_DLL Abc_Obj_t *        Abc_NodeFindCoFanout( Abc_Obj_t * pNode );
+extern ABC_DLL Abc_Obj_t *        Abc_NodeFindNonCoFanout( Abc_Obj_t * pNode );
+extern ABC_DLL Abc_Obj_t *        Abc_NodeHasUniqueCoFanout( Abc_Obj_t * pNode );
+extern ABC_DLL bool               Abc_NtkLogicHasSimpleCos( Abc_Ntk_t * pNtk );
+extern ABC_DLL int                Abc_NtkLogicMakeSimpleCos( Abc_Ntk_t * pNtk, bool fDuplicate );
+extern ABC_DLL void               Abc_VecObjPushUniqueOrderByLevel( Vec_Ptr_t * p, Abc_Obj_t * pNode );
+extern ABC_DLL bool               Abc_NodeIsExorType( Abc_Obj_t * pNode );
+extern ABC_DLL bool               Abc_NodeIsMuxType( Abc_Obj_t * pNode );
+extern ABC_DLL bool               Abc_NodeIsMuxControlType( Abc_Obj_t * pNode );
+extern ABC_DLL Abc_Obj_t *        Abc_NodeRecognizeMux( Abc_Obj_t * pNode, Abc_Obj_t ** ppNodeT, Abc_Obj_t ** ppNodeE );
+extern ABC_DLL int                Abc_NtkPrepareTwoNtks( FILE * pErr, Abc_Ntk_t * pNtk, char ** argv, int argc, Abc_Ntk_t ** ppNtk1, Abc_Ntk_t ** ppNtk2, int * pfDelete1, int * pfDelete2 );
+extern ABC_DLL void               Abc_NodeCollectFanins( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes );
+extern ABC_DLL void               Abc_NodeCollectFanouts( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes );
+extern ABC_DLL Vec_Ptr_t *        Abc_NtkCollectLatches( Abc_Ntk_t * pNtk );
+extern ABC_DLL int                Abc_NodeCompareLevelsIncrease( Abc_Obj_t ** pp1, Abc_Obj_t ** pp2 );
+extern ABC_DLL int                Abc_NodeCompareLevelsDecrease( Abc_Obj_t ** pp1, Abc_Obj_t ** pp2 );
+extern ABC_DLL Vec_Int_t *        Abc_NtkFanoutCounts( Abc_Ntk_t * pNtk );
+extern ABC_DLL Vec_Ptr_t *        Abc_NtkCollectObjects( Abc_Ntk_t * pNtk );
+extern ABC_DLL Vec_Int_t *        Abc_NtkGetCiIds( Abc_Ntk_t * pNtk );
+extern ABC_DLL void               Abc_NtkReassignIds( Abc_Ntk_t * pNtk );
+extern ABC_DLL int                Abc_ObjPointerCompare( void ** pp1, void ** pp2 );
+extern ABC_DLL void               Abc_NtkTransferCopy( Abc_Ntk_t * pNtk );
 /*=== abcVerify.c ==========================================================*/
-extern int *              Abc_NtkVerifyGetCleanModel( Abc_Ntk_t * pNtk, int nFrames );
-extern int *              Abc_NtkVerifySimulatePattern( Abc_Ntk_t * pNtk, int * pModel );
+extern ABC_DLL int *              Abc_NtkVerifyGetCleanModel( Abc_Ntk_t * pNtk, int nFrames );
+extern ABC_DLL int *              Abc_NtkVerifySimulatePattern( Abc_Ntk_t * pNtk, int * pModel );
 
 #ifdef __cplusplus
 }
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 0437f8a9..9b5ebddb 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -91,6 +91,7 @@ static int Abc_CommandOrPos          ( Abc_Frame_t * pAbc, int argc, char ** arg
 static int Abc_CommandAndPos         ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAppend         ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandFrames         ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandDFrames        ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandSop            ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandBdd            ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAig            ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -181,6 +182,7 @@ static int Abc_CommandFlowRetime     ( Abc_Frame_t * pAbc, int argc, char ** arg
 static int Abc_CommandSeqFpga        ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandSeqMap         ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandSeqSweep       ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandSeqSweepTest   ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandLcorr          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandSeqCleanup     ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandCycle          ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -345,6 +347,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Various",      "andpos",        Abc_CommandAndPos,           1 );
     Cmd_CommandAdd( pAbc, "Various",      "append",        Abc_CommandAppend,           1 );
     Cmd_CommandAdd( pAbc, "Various",      "frames",        Abc_CommandFrames,           1 );
+    Cmd_CommandAdd( pAbc, "Various",      "dframes",       Abc_CommandDFrames,          1 );
     Cmd_CommandAdd( pAbc, "Various",      "sop",           Abc_CommandSop,              0 );
     Cmd_CommandAdd( pAbc, "Various",      "bdd",           Abc_CommandBdd,              0 );
     Cmd_CommandAdd( pAbc, "Various",      "aig",           Abc_CommandAig,              0 );
@@ -432,6 +435,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
 //    Cmd_CommandAdd( pAbc, "Sequential",   "sfpga",         Abc_CommandSeqFpga,          1 );
 //    Cmd_CommandAdd( pAbc, "Sequential",   "smap",          Abc_CommandSeqMap,           1 );
     Cmd_CommandAdd( pAbc, "Sequential",   "ssweep",        Abc_CommandSeqSweep,         1 );
+    Cmd_CommandAdd( pAbc, "Sequential",   "testssw",       Abc_CommandSeqSweepTest,     0 );
     Cmd_CommandAdd( pAbc, "Sequential",   "lcorr",         Abc_CommandLcorr,            1 );
     Cmd_CommandAdd( pAbc, "Sequential",   "scleanup",      Abc_CommandSeqCleanup,       1 );
     Cmd_CommandAdd( pAbc, "Sequential",   "cycle",         Abc_CommandCycle,            1 );
@@ -5071,8 +5075,9 @@ int Abc_CommandFrames( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk, * pNtkTemp, * pNtkRes;
-    int fInitial;
     int nFrames;
+    int fInitial;
+    int fVerbose;
     int c;
 
     pNtk = Abc_FrameReadNtk(pAbc);
@@ -5080,10 +5085,11 @@ int Abc_CommandFrames( Abc_Frame_t * pAbc, int argc, char ** argv )
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
-    fInitial = 0;
     nFrames  = 5;
+    fInitial = 0;
+    fVerbose = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "Fih" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Fivh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -5101,6 +5107,9 @@ int Abc_CommandFrames( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'i':
             fInitial ^= 1;
             break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
         case 'h':
             goto usage;
         default:
@@ -5118,11 +5127,11 @@ int Abc_CommandFrames( Abc_Frame_t * pAbc, int argc, char ** argv )
     if ( !Abc_NtkIsStrash(pNtk) )
     {
         pNtkTemp = Abc_NtkStrash( pNtk, 0, 0, 0 );
-        pNtkRes  = Abc_NtkFrames( pNtkTemp, nFrames, fInitial );
+        pNtkRes  = Abc_NtkFrames( pNtkTemp, nFrames, fInitial, fVerbose );
         Abc_NtkDelete( pNtkTemp );
     }
     else
-        pNtkRes  = Abc_NtkFrames( pNtk, nFrames, fInitial );
+        pNtkRes  = Abc_NtkFrames( pNtk, nFrames, fInitial, fVerbose );
     if ( pNtkRes == NULL )
     {
         fprintf( pErr, "Unrolling the network has failed.\n" );
@@ -5133,15 +5142,129 @@ int Abc_CommandFrames( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: frames [-F num] [-ih]\n" );
+    fprintf( pErr, "usage: frames [-F num] [-ivh]\n" );
     fprintf( pErr, "\t         unrolls the network for a number of time frames\n" );
     fprintf( pErr, "\t-F num : the number of frames to unroll [default = %d]\n", nFrames );
     fprintf( pErr, "\t-i     : toggles initializing the first frame [default = %s]\n", fInitial? "yes": "no" );  
+    fprintf( pErr, "\t-v     : toggles outputting verbose information [default = %s]\n", fVerbose? "yes": "no" );  
+    fprintf( pErr, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandDFrames( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk, * pNtkTemp, * pNtkRes;
+    int nPrefix;
+    int nFrames;
+    int fInitial;
+    int fVerbose;
+    int c;
+
+    extern Abc_Ntk_t * Abc_NtkDarFrames( Abc_Ntk_t * pNtk, int nPrefix, int nFrames, int fInitial, int fVerbose );
+
+    pNtk = Abc_FrameReadNtk(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    nPrefix  = 5;
+    nFrames  = 5;
+    fInitial = 0;
+    fVerbose = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "NFivh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'N':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-N\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nPrefix = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nPrefix <= 0 ) 
+                goto usage;
+            break;
+        case 'F':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nFrames = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nFrames <= 0 ) 
+                goto usage;
+            break;
+        case 'i':
+            fInitial ^= 1;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+    if ( nPrefix > nFrames )
+    {
+        fprintf( pErr, "Prefix (%d) cannot be more than the number of frames (%d).\n", nPrefix, nFrames );
+        return 1;
+    }
+
+    // get the new network
+    if ( !Abc_NtkIsStrash(pNtk) )
+    {
+        pNtkTemp = Abc_NtkStrash( pNtk, 0, 0, 0 );
+        pNtkRes  = Abc_NtkDarFrames( pNtkTemp, nPrefix, nFrames, fInitial, fVerbose );
+        Abc_NtkDelete( pNtkTemp );
+    }
+    else
+        pNtkRes  = Abc_NtkDarFrames( pNtk, nPrefix, nFrames, fInitial, fVerbose );
+    if ( pNtkRes == NULL )
+    {
+        fprintf( pErr, "Unrolling the network has failed.\n" );
+        return 1;
+    }
+    // replace the current network
+    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: dframes [-NF num] [-ivh]\n" );
+    fprintf( pErr, "\t         unrolls the network with simplification\n" );
+    fprintf( pErr, "\t-N num : the number of frames to use as prefix [default = %d]\n", nPrefix );
+    fprintf( pErr, "\t-F num : the number of frames to unroll [default = %d]\n", nFrames );
+    fprintf( pErr, "\t-i     : toggles initializing the first frame [default = %s]\n", fInitial? "yes": "no" );  
+    fprintf( pErr, "\t-v     : toggles outputting verbose information [default = %s]\n", fVerbose? "yes": "no" );  
     fprintf( pErr, "\t-h     : print the command usage\n");
     return 1;
 }
 
 
+
 /**Function*************************************************************
 
   Synopsis    []
@@ -7352,6 +7475,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
 //    extern Abc_Ntk_t * Abc_NtkTestExor( Abc_Ntk_t * pNtk, int fVerbose );
 //    extern Abc_Ntk_t * Abc_NtkNtkTest( Abc_Ntk_t * pNtk, If_Lib_t * pLutLib );
     extern Abc_Ntk_t * Abc_NtkDarRetimeStep( Abc_Ntk_t * pNtk, int fVerbose );
+    extern void Abc_NtkDarTest( Abc_Ntk_t * pNtk );
 
 
 
@@ -7537,6 +7661,8 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
 */
 
 //    Abc_NtkDarPartition( pNtk );
+Abc_NtkDarTest( pNtk );
+return 0;
 
     pNtkRes = Abc_NtkDarRetimeStep( pNtk, 0 );
     if ( pNtkRes == NULL )
@@ -12891,6 +13017,170 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandSeqSweepTest( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    char * pFileName;
+    Fra_Ssw_t Pars, * pPars = &Pars;
+    int c;
+//    extern Abc_Ntk_t * Abc_NtkDarSeqSweep( Abc_Ntk_t * pNtk, Fra_Ssw_t * pPars );
+    extern int Fra_FraigInductionTest( char * pFileName, Fra_Ssw_t * pParams );
+
+    // set defaults
+    pPars->nPartSize  = 0;
+    pPars->nOverSize  = 0;
+    pPars->nFramesP   = 0;
+    pPars->nFramesK   = 1;
+    pPars->nMaxImps   = 5000;
+    pPars->nMaxLevs   = 0;
+    pPars->fUseImps   = 0;
+    pPars->fRewrite   = 0;
+    pPars->fFraiging  = 0;
+    pPars->fLatchCorr = 0;
+    pPars->fWriteImps = 0;
+    pPars->fUse1Hot   = 0;
+    pPars->fVerbose   = 0;
+    pPars->TimeLimit  = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "PQNFILirfletvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'P':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( stdout, "Command line switch \"-P\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nPartSize = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nPartSize < 2 ) 
+                goto usage;
+            break;
+        case 'Q':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( stdout, "Command line switch \"-Q\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nOverSize = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nOverSize < 0 ) 
+                goto usage;
+            break;
+        case 'N':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( stdout, "Command line switch \"-N\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nFramesP = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nFramesP < 0 ) 
+                goto usage;
+            break;
+        case 'F':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( stdout, "Command line switch \"-F\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nFramesK = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nFramesK <= 0 ) 
+                goto usage;
+            break;
+        case 'I':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( stdout, "Command line switch \"-I\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nMaxImps = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nMaxImps <= 0 ) 
+                goto usage;
+            break;
+        case 'L':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( stdout, "Command line switch \"-L\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nMaxLevs = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nMaxLevs <= 0 ) 
+                goto usage;
+            break;
+        case 'i':
+            pPars->fUseImps ^= 1;
+            break;
+        case 'r':
+            pPars->fRewrite ^= 1;
+            break;
+        case 'f':
+            pPars->fFraiging ^= 1;
+            break;
+        case 'l':
+            pPars->fLatchCorr ^= 1;
+            break;
+        case 'e':
+            pPars->fWriteImps ^= 1;
+            break;
+        case 't':
+            pPars->fUse1Hot ^= 1;
+            break;
+        case 'v':
+            pPars->fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    // get the input file name
+    if ( argc == globalUtilOptind + 1 )
+        pFileName = argv[globalUtilOptind];
+    else
+    {
+        printf( "File name should be given on the command line.\n" );
+        return 1;
+    }
+    Fra_FraigInductionTest( pFileName, pPars );
+    return 0;
+
+usage:
+    fprintf( stdout, "usage: testssw [-PQNFL num] [-lrfetvh] <file>\n" );
+    fprintf( stdout, "\t         performs sequential sweep using K-step induction\n" );
+    fprintf( stdout, "\t         (outputs a file with a set of pairs of equivalent nodes)\n" );
+    fprintf( stdout, "\t-P num : max partition size (0 = no partitioning) [default = %d]\n", pPars->nPartSize );
+    fprintf( stdout, "\t-Q num : partition overlap (0 = no overlap) [default = %d]\n", pPars->nOverSize );
+    fprintf( stdout, "\t-N num : number of time frames to use as the prefix [default = %d]\n", pPars->nFramesP );
+    fprintf( stdout, "\t-F num : number of time frames for induction (1=simple) [default = %d]\n", pPars->nFramesK );
+    fprintf( stdout, "\t-L num : max number of levels to consider (0=all) [default = %d]\n", pPars->nMaxLevs );
+//    fprintf( stdout, "\t-I num : max number of implications to consider [default = %d]\n", pPars->nMaxImps );
+//    fprintf( stdout, "\t-i     : toggle using implications [default = %s]\n", pPars->fUseImps? "yes": "no" );
+    fprintf( stdout, "\t-l     : toggle latch correspondence only [default = %s]\n", pPars->fLatchCorr? "yes": "no" );
+    fprintf( stdout, "\t-r     : toggle AIG rewriting [default = %s]\n", pPars->fRewrite? "yes": "no" );
+    fprintf( stdout, "\t-f     : toggle fraiging (combinational SAT sweeping) [default = %s]\n", pPars->fFraiging? "yes": "no" );
+    fprintf( stdout, "\t-e     : toggle writing implications as assertions [default = %s]\n", pPars->fWriteImps? "yes": "no" );
+    fprintf( stdout, "\t-t     : toggle using one-hotness conditions [default = %s]\n", pPars->fUse1Hot? "yes": "no" );
+    fprintf( stdout, "\t-v     : toggle verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" );
+    fprintf( stdout, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandLcorr( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index 7b7617e6..ca54e4e1 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -1491,6 +1491,7 @@ Abc_Ntk_t * Abc_NtkDarLatchSweep( Abc_Ntk_t * pNtk, int fLatchConst, int fLatchE
     if ( pMan->vFlopNums )
         Vec_IntFree( pMan->vFlopNums );
     pMan->vFlopNums = NULL;
+
     pMan = Aig_ManScl( pTemp = pMan, fLatchConst, fLatchEqual, fVerbose );
     Aig_ManStop( pTemp );
     pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
@@ -2083,6 +2084,38 @@ Abc_Ntk_t * Abc_NtkPhaseAbstract( Abc_Ntk_t * pNtk, int nFrames, int fIgnore, in
 
 /**Function*************************************************************
 
+  Synopsis    [Performs phase abstraction.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkDarFrames( Abc_Ntk_t * pNtk, int nPrefix, int nFrames, int fInit, int fVerbose )
+{
+    Abc_Ntk_t * pNtkAig;
+    Aig_Man_t * pMan, * pTemp;
+    pMan = Abc_NtkToDar( pNtk, 0, 0 );
+    pMan->nRegs = Abc_NtkLatchNum(pNtk);
+    pMan->nTruePis = Aig_ManPiNum(pMan) - Aig_ManRegNum(pMan); 
+    pMan->nTruePos = Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan); 
+    if ( pMan == NULL )
+        return NULL;
+    pMan = Saig_ManTimeframeSimplify( pTemp = pMan, nPrefix, nFrames, fInit, fVerbose );
+    Aig_ManStop( pTemp );
+    if ( pMan == NULL )
+        return NULL;
+    pNtkAig = Abc_NtkFromAigPhase( pMan );
+    pNtkAig->pName = Extra_UtilStrsav(pNtk->pName);
+    pNtkAig->pSpec = Extra_UtilStrsav(pNtk->pSpec);
+    Aig_ManStop( pMan );
+    return pNtkAig;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Performs BDD-based reachability analysis.]
 
   Description []
@@ -2107,6 +2140,38 @@ void Abc_NtkDarReach( Abc_Ntk_t * pNtk, int nBddMax, int nIterMax, int fPartitio
 }
 
 
+/**Function*************************************************************
+
+  Synopsis    [Performs BDD-based reachability analysis.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkDarTest( Abc_Ntk_t * pNtk )
+{
+    Aig_Man_t * pMan;
+    assert( Abc_NtkIsStrash(pNtk) );
+    pMan = Abc_NtkToDar( pNtk, 0, 1 );
+    pMan->nRegs = Abc_NtkLatchNum(pNtk);
+    pMan->nTruePis = Aig_ManPiNum(pMan) - Aig_ManRegNum(pMan); 
+    pMan->nTruePos = Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan); 
+    if ( pMan == NULL )
+        return;
+
+Aig_ManSetRegNum( pMan, pMan->nRegs );
+Aig_ManPrintStats( pMan );
+Saig_ManDumpBlif( pMan, "_temp_.blif" );
+Aig_ManStop( pMan );
+pMan = Saig_ManReadBlif( "_temp_.blif" );
+Aig_ManPrintStats( pMan );
+
+    Aig_ManStop( pMan );
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abcMiter.c b/src/base/abci/abcMiter.c
index 9bab238b..4e1022b8 100644
--- a/src/base/abci/abcMiter.c
+++ b/src/base/abci/abcMiter.c
@@ -766,7 +766,7 @@ void Abc_NtkMiterReport( Abc_Ntk_t * pMiter )
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkFrames( Abc_Ntk_t * pNtk, int nFrames, int fInitial )
+Abc_Ntk_t * Abc_NtkFrames( Abc_Ntk_t * pNtk, int nFrames, int fInitial, int fVerbose )
 {
     char Buffer[1000];
     ProgressBar * pProgress;
diff --git a/src/base/abci/abcVerify.c b/src/base/abci/abcVerify.c
index 328d2907..96a4566d 100644
--- a/src/base/abci/abcVerify.c
+++ b/src/base/abci/abcVerify.c
@@ -478,7 +478,7 @@ void Abc_NtkSecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nI
     }
 
     // create the timeframes
-    pFrames = Abc_NtkFrames( pMiter, nFrames, 1 );
+    pFrames = Abc_NtkFrames( pMiter, nFrames, 1, 0 );
     Abc_NtkDelete( pMiter );
     if ( pFrames == NULL )
     {
@@ -564,7 +564,7 @@ int Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nFr
     }
 
     // create the timeframes
-    pFrames = Abc_NtkFrames( pMiter, nFrames, 1 );
+    pFrames = Abc_NtkFrames( pMiter, nFrames, 1, 0 );
     Abc_NtkDelete( pMiter );
     if ( pFrames == NULL )
     {
@@ -777,7 +777,7 @@ void Abc_NtkGetSeqPoSupp( Abc_Ntk_t * pNtk, int iFrame, int iNumPo )
     Vec_Ptr_t * vSupp;
     int i, k;
     // get the timeframes of the network
-    pFrames = Abc_NtkFrames( pNtk, iFrame + 1, 0 );
+    pFrames = Abc_NtkFrames( pNtk, iFrame + 1, 0, 0 );
 //Abc_NtkShowAig( pFrames );
 
     // get the PO of the timeframes
diff --git a/src/base/main/main.h b/src/base/main/main.h
index b5cc0dfe..852b8f25 100644
--- a/src/base/main/main.h
+++ b/src/base/main/main.h
@@ -14,7 +14,7 @@
 
   Date        [Ver. 1.0. Started - June 20, 2005.]
 
-  Revision    [$Id: main.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+  Revision    [$Id: main.h,v 1.1 2008/05/14 22:13:13 wudenni Exp $]
 
 ***********************************************************************/
 
@@ -69,47 +69,57 @@ typedef struct Abc_Frame_t_      Abc_Frame_t;
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
+#ifdef WIN32
+#define DLLEXPORT __declspec(dllexport)
+#define DLLIMPORT __declspec(dllimport)
+#else  /* defined(WIN32) */
+#define DLLIMPORT
+#endif /* defined(WIN32) */
+
+#ifndef ABC_DLL
+#define ABC_DLL DLLIMPORT
+#endif
 
 /*=== main.c ===========================================================*/
-extern void            Abc_Start();
-extern void            Abc_Stop();
+extern ABC_DLL void            Abc_Start();
+extern ABC_DLL void            Abc_Stop();
 
 /*=== mainFrame.c ===========================================================*/
-extern Abc_Ntk_t *     Abc_FrameReadNtk( Abc_Frame_t * p );
-extern FILE *          Abc_FrameReadOut( Abc_Frame_t * p );
-extern FILE *          Abc_FrameReadErr( Abc_Frame_t * p );
-extern bool            Abc_FrameReadMode( Abc_Frame_t * p );
-extern bool            Abc_FrameSetMode( Abc_Frame_t * p, bool fNameMode );
-extern void            Abc_FrameRestart( Abc_Frame_t * p );
-extern bool            Abc_FrameShowProgress( Abc_Frame_t * p );
-
-extern void            Abc_FrameSetCurrentNetwork( Abc_Frame_t * p, Abc_Ntk_t * pNet );
-extern void            Abc_FrameSwapCurrentAndBackup( Abc_Frame_t * p );
-extern void            Abc_FrameReplaceCurrentNetwork( Abc_Frame_t * p, Abc_Ntk_t * pNet );
-extern void            Abc_FrameUnmapAllNetworks( Abc_Frame_t * p );
-extern void            Abc_FrameDeleteAllNetworks( Abc_Frame_t * p );
-
-extern void               Abc_FrameSetGlobalFrame( Abc_Frame_t * p );
-extern Abc_Frame_t *   Abc_FrameGetGlobalFrame();
-
-extern Vec_Ptr_t *     Abc_FrameReadStore();                  
-extern int             Abc_FrameReadStoreSize();              
-extern void *          Abc_FrameReadLibLut();                    
-extern void *          Abc_FrameReadLibGen();                    
-extern void *          Abc_FrameReadLibSuper();                  
-extern void *          Abc_FrameReadLibVer();                  
-extern void *          Abc_FrameReadManDd();                     
-extern void *          Abc_FrameReadManDec();                    
-extern char *          Abc_FrameReadFlag( char * pFlag ); 
-extern bool            Abc_FrameIsFlagEnabled( char * pFlag );
-
-extern void            Abc_FrameSetNtkStore( Abc_Ntk_t * pNtk ); 
-extern void            Abc_FrameSetNtkStoreSize( int nStored );  
-extern void            Abc_FrameSetLibLut( void * pLib );        
-extern void            Abc_FrameSetLibGen( void * pLib );        
-extern void            Abc_FrameSetLibSuper( void * pLib );      
-extern void            Abc_FrameSetLibVer( void * pLib );      
-extern void            Abc_FrameSetFlag( char * pFlag, char * pValue );
+extern ABC_DLL Abc_Ntk_t *     Abc_FrameReadNtk( Abc_Frame_t * p );
+extern ABC_DLL FILE *          Abc_FrameReadOut( Abc_Frame_t * p );
+extern ABC_DLL FILE *          Abc_FrameReadErr( Abc_Frame_t * p );
+extern ABC_DLL bool            Abc_FrameReadMode( Abc_Frame_t * p );
+extern ABC_DLL bool            Abc_FrameSetMode( Abc_Frame_t * p, bool fNameMode );
+extern ABC_DLL void            Abc_FrameRestart( Abc_Frame_t * p );
+extern ABC_DLL bool            Abc_FrameShowProgress( Abc_Frame_t * p );
+
+extern ABC_DLL void            Abc_FrameSetCurrentNetwork( Abc_Frame_t * p, Abc_Ntk_t * pNet );
+extern ABC_DLL void            Abc_FrameSwapCurrentAndBackup( Abc_Frame_t * p );
+extern ABC_DLL void            Abc_FrameReplaceCurrentNetwork( Abc_Frame_t * p, Abc_Ntk_t * pNet );
+extern ABC_DLL void            Abc_FrameUnmapAllNetworks( Abc_Frame_t * p );
+extern ABC_DLL void            Abc_FrameDeleteAllNetworks( Abc_Frame_t * p );
+
+extern ABC_DLL void               Abc_FrameSetGlobalFrame( Abc_Frame_t * p );
+extern ABC_DLL Abc_Frame_t *   Abc_FrameGetGlobalFrame();
+
+extern ABC_DLL Vec_Ptr_t *     Abc_FrameReadStore();                  
+extern ABC_DLL int             Abc_FrameReadStoreSize();              
+extern ABC_DLL void *          Abc_FrameReadLibLut();                    
+extern ABC_DLL void *          Abc_FrameReadLibGen();                    
+extern ABC_DLL void *          Abc_FrameReadLibSuper();                  
+extern ABC_DLL void *          Abc_FrameReadLibVer();                  
+extern ABC_DLL void *          Abc_FrameReadManDd();                     
+extern ABC_DLL void *          Abc_FrameReadManDec();                    
+extern ABC_DLL char *          Abc_FrameReadFlag( char * pFlag ); 
+extern ABC_DLL bool            Abc_FrameIsFlagEnabled( char * pFlag );
+
+extern ABC_DLL void            Abc_FrameSetNtkStore( Abc_Ntk_t * pNtk ); 
+extern ABC_DLL void            Abc_FrameSetNtkStoreSize( int nStored );  
+extern ABC_DLL void            Abc_FrameSetLibLut( void * pLib );        
+extern ABC_DLL void            Abc_FrameSetLibGen( void * pLib );        
+extern ABC_DLL void            Abc_FrameSetLibSuper( void * pLib );      
+extern ABC_DLL void            Abc_FrameSetLibVer( void * pLib );      
+extern ABC_DLL void            Abc_FrameSetFlag( char * pFlag, char * pValue );
 
 #ifdef __cplusplus
 }
diff --git a/src/base/main/mainInt.h b/src/base/main/mainInt.h
index f79f9126..b03a00fa 100644
--- a/src/base/main/mainInt.h
+++ b/src/base/main/mainInt.h
@@ -14,13 +14,13 @@
 
   Date        [Ver. 1.0. Started - June 20, 2005.]
 
-  Revision    [$Id: mainInt.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+  Revision    [$Id: mainInt.h,v 1.1 2008/05/14 22:13:13 wudenni Exp $]
 
 ***********************************************************************/
 
 #ifndef __MAIN_INT_H__
 #define __MAIN_INT_H__
-
+ 
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
@@ -93,21 +93,31 @@ struct Abc_Frame_t_
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
+#ifdef WIN32
+#define DLLEXPORT __declspec(dllexport)
+#define DLLIMPORT __declspec(dllimport)
+#else  /* defined(WIN32) */
+#define DLLIMPORT
+#endif /* defined(WIN32) */
+
+#ifndef ABC_DLL
+#define ABC_DLL DLLIMPORT
+#endif
 
 /*=== mvMain.c ===========================================================*/
-extern int             main( int argc, char * argv[] );
+extern ABC_DLL int             main( int argc, char * argv[] );
 /*=== mvInit.c ===================================================*/
-extern void            Abc_FrameInit( Abc_Frame_t * pAbc );
-extern void            Abc_FrameEnd( Abc_Frame_t * pAbc );
+extern ABC_DLL void            Abc_FrameInit( Abc_Frame_t * pAbc );
+extern ABC_DLL void            Abc_FrameEnd( Abc_Frame_t * pAbc );
 /*=== mvFrame.c =====================================================*/
-extern Abc_Frame_t *   Abc_FrameAllocate();
-extern void            Abc_FrameDeallocate( Abc_Frame_t * p );
+extern ABC_DLL Abc_Frame_t *   Abc_FrameAllocate();
+extern ABC_DLL void            Abc_FrameDeallocate( Abc_Frame_t * p );
 /*=== mvUtils.c =====================================================*/
-extern char *          Abc_UtilsGetVersion( Abc_Frame_t * pAbc );
-extern char *          Abc_UtilsGetUsersInput( Abc_Frame_t * pAbc );
-extern void            Abc_UtilsPrintHello( Abc_Frame_t * pAbc );
-extern void            Abc_UtilsPrintUsage( Abc_Frame_t * pAbc, char * ProgName );
-extern void            Abc_UtilsSource( Abc_Frame_t * pAbc );
+extern ABC_DLL char *          Abc_UtilsGetVersion( Abc_Frame_t * pAbc );
+extern ABC_DLL char *          Abc_UtilsGetUsersInput( Abc_Frame_t * pAbc );
+extern ABC_DLL void            Abc_UtilsPrintHello( Abc_Frame_t * pAbc );
+extern ABC_DLL void            Abc_UtilsPrintUsage( Abc_Frame_t * pAbc, char * ProgName );
+extern ABC_DLL void            Abc_UtilsSource( Abc_Frame_t * pAbc );
 
 #endif
 
diff --git a/src/misc/vec/vec.h b/src/misc/vec/vec.h
index 4091ac7f..ee82fc3e 100644
--- a/src/misc/vec/vec.h
+++ b/src/misc/vec/vec.h
@@ -72,6 +72,10 @@ typedef long long          sint64;
 #define ALLOC(type, num)     ((type *) malloc(sizeof(type) * (num)))
 #endif
 
+#ifndef CALLOC
+#define CALLOC(type, num)     ((type *) calloc((num), sizeof(type)))
+#endif
+
 #ifndef FREE
 #define FREE(obj)             ((obj) ? (free((char *) (obj)), (obj) = 0) : 0)
 #endif