Synchronizing various data-structures.

11 files changed, 452 insertions, 23 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index f8e36a4f..b5f073b3 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -163,6 +163,10 @@ struct Gia_Man_t_
     Gia_Man_t *    pAigExtra;     // combinational logic of holes
     Vec_Flt_t *    vInArrs;       // PI arrival times
     Vec_Flt_t *    vOutReqs;      // PO required times
+    Vec_Int_t *    vCiArrs;       // CI arrival times
+    Vec_Int_t *    vCoReqs;       // CO required times
+    Vec_Int_t *    vCoArrs;       // CO arrival times
+    int            And2Delay;     // delay of the AND gate 
     float          DefInArrs;     // default PI arrival times
     float          DefOutReqs;    // default PO required times
     Vec_Int_t *    vSwitching;    // switching activity
@@ -1207,6 +1211,7 @@ extern Gia_Man_t *         Gia_ManDupLastPis( Gia_Man_t * p, int nLastPis );
 extern Gia_Man_t *         Gia_ManDupFlip( Gia_Man_t * p, int * pInitState );
 extern Gia_Man_t *         Gia_ManDupCycled( Gia_Man_t * pAig, Abc_Cex_t * pCex, int nFrames );
 extern Gia_Man_t *         Gia_ManDup( Gia_Man_t * p );  
+extern Gia_Man_t *         Gia_ManDup2( Gia_Man_t * p1, Gia_Man_t * p2 );
 extern Gia_Man_t *         Gia_ManDupWithAttributes( Gia_Man_t * p );  
 extern Gia_Man_t *         Gia_ManDupZero( Gia_Man_t * p );
 extern Gia_Man_t *         Gia_ManDupPerm( Gia_Man_t * p, Vec_Int_t * vPiPerm );
diff --git a/src/aig/gia/giaBalAig.c b/src/aig/gia/giaBalAig.c
index 680b7fc8..018bfcaf 100644
--- a/src/aig/gia/giaBalAig.c
+++ b/src/aig/gia/giaBalAig.c
@@ -392,6 +392,13 @@ Gia_Man_t * Gia_ManBalanceInt( Gia_Man_t * p, int fStrict )
     Gia_ManConst0(p)->Value = 0;
     Gia_ManForEachCi( p, pObj, i )
         pObj->Value = Gia_ManAppendCi( pNew );
+    // set arrival times for the input of the new AIG
+    if ( p->vCiArrs )
+    {
+        int Id, And2Delay = p->And2Delay ? p->And2Delay : 1;
+        Gia_ManForEachCiId( pNew, Id, i )
+            Vec_IntWriteEntry( pNew->vLevels, Id, Vec_IntEntry(p->vCiArrs, i)/And2Delay );
+    }
     // create internal nodes
     Gia_ManHashStart( pNew );
     Gia_ManForEachBuf( p, pObj, i )
@@ -430,11 +437,14 @@ Gia_Man_t * Gia_ManBalance( Gia_Man_t * p, int fSimpleAnd, int fStrict, int fVer
     Gia_Man_t * pNew, * pNew1, * pNew2;
     if ( fVerbose )      Gia_ManPrintStats( p, NULL );
     pNew = fSimpleAnd ? Gia_ManDup( p ) : Gia_ManDupMuxes( p, 2 );
+    Gia_ManTransferTiming( pNew, p );
     if ( fVerbose )      Gia_ManPrintStats( pNew, NULL );
     pNew1 = Gia_ManBalanceInt( pNew, fStrict );
+    Gia_ManTransferTiming( pNew1, pNew );
     if ( fVerbose )      Gia_ManPrintStats( pNew1, NULL );
     Gia_ManStop( pNew );
     pNew2 = Gia_ManDupNoMuxes( pNew1 );
+    Gia_ManTransferTiming( pNew2, pNew1 );
     if ( fVerbose )      Gia_ManPrintStats( pNew2, NULL );
     Gia_ManStop( pNew1 );
     return pNew2;
@@ -1032,33 +1042,47 @@ Gia_Man_t * Gia_ManAreaBalance( Gia_Man_t * p, int fSimpleAnd, int nNewNodesMax,
 {
     Gia_Man_t * pNew0, * pNew, * pNew1, * pNew2;
     Vec_Int_t * vCiLevels;
+    // set arrival times for the input of the new AIG
+    if ( p->vCiArrs )
+    {
+        int i, Id, And2Delay = p->And2Delay ? p->And2Delay : 1;
+        Vec_IntFreeP( &p->vLevels );
+        p->vLevels = Vec_IntStart( Gia_ManObjNum(p) );
+        Gia_ManForEachCiId( p, Id, i )
+            Vec_IntWriteEntry( p->vLevels, Id, Vec_IntEntry(p->vCiArrs, i)/And2Delay );
+    }
     // determine CI levels
     if ( p->pManTime && p->vLevels == NULL )
         Gia_ManLevelWithBoxes( p );
     vCiLevels = Gia_ManGetCiLevels( p );
     // get the starting manager
-    pNew0 = Gia_ManHasMapping(p) ? (Gia_Man_t *)Dsm_ManDeriveGia(p, 0) : p;
+    pNew0 = Gia_ManHasMapping(p) ? (Gia_Man_t *)Dsm_ManDeriveGia(p, 0) : Gia_ManDup(p);
+    Gia_ManTransferTiming( pNew0, p );
     if ( fVerbose )     Gia_ManPrintStats( pNew0, NULL );
     // derive internal manager
     pNew = fSimpleAnd ? Gia_ManDup( pNew0 ) : Gia_ManDupMuxes( pNew0, 2 );
+    Gia_ManTransferTiming( pNew, pNew0 );
     if ( fVerbose )     Gia_ManPrintStats( pNew, NULL );
     if ( pNew0 != p ) Gia_ManStop( pNew0 );
     // perform the operation
     pNew1 = Dam_ManAreaBalanceInt( pNew, vCiLevels, nNewNodesMax, fVerbose, fVeryVerbose );
+    Gia_ManTransferTiming( pNew1, pNew );
     if ( fVerbose )     Gia_ManPrintStats( pNew1, NULL );
     Gia_ManStop( pNew );
     Vec_IntFreeP( &vCiLevels );
     // derive the final result
     pNew2 = Gia_ManDupNoMuxes( pNew1 );
+    Gia_ManTransferTiming( pNew2, pNew1 );
     if ( fVerbose )     Gia_ManPrintStats( pNew2, NULL );
     Gia_ManStop( pNew1 );
     // normalize if needed
     if ( !Gia_ManIsNormalized(pNew2) )
     {
         pNew2 = Gia_ManDupNormalize( pNew1 = pNew2, 0 );
+        Gia_ManTransferTiming( pNew2, pNew1 );
         Gia_ManStop( pNew1 );
     }
-    Gia_ManTransferTiming( pNew2, p );
+    //Gia_ManTransferTiming( pNew2, p );
     return pNew2;
 }
 
diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c
index 5e7dc639..19715e2e 100644
--- a/src/aig/gia/giaDup.c
+++ b/src/aig/gia/giaDup.c
@@ -718,6 +718,31 @@ Gia_Man_t * Gia_ManDup( Gia_Man_t * p )
         pNew->pCexSeq = Abc_CexDup( p->pCexSeq, Gia_ManRegNum(p) );
     return pNew;
 }
+Gia_Man_t * Gia_ManDup2( Gia_Man_t * p1, Gia_Man_t * p2 )
+{
+    Gia_Man_t * pNew;
+    Gia_Obj_t * pObj;
+    int i;
+    assert( Gia_ManCiNum(p1) == Gia_ManCiNum(p2) );
+    assert( Gia_ManCoNum(p1) == Gia_ManCoNum(p2) );
+    pNew = Gia_ManStart( Gia_ManObjNum(p1) + Gia_ManObjNum(p2) );
+    Gia_ManHashStart( pNew );
+    Gia_ManConst0(p1)->Value = 0;
+    Gia_ManConst0(p2)->Value = 0;
+    Gia_ManForEachCi( p1, pObj, i )
+        pObj->Value = Gia_ManCi(p2, i)->Value = Gia_ManAppendCi( pNew );
+    Gia_ManForEachAnd( p1, pObj, i )
+        pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+    Gia_ManForEachAnd( p2, pObj, i )
+        pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+    Gia_ManForEachCo( p1, pObj, i )
+        pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+    Gia_ManForEachCo( p2, pObj, i )
+        pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+    Gia_ManSetRegNum( pNew, Gia_ManRegNum(p1) );
+    Gia_ManHashStop( pNew );
+    return pNew;
+}
 Gia_Man_t * Gia_ManDupWithAttributes( Gia_Man_t * p )
 {
     Gia_Man_t * pNew = Gia_ManDup(p);
diff --git a/src/aig/gia/giaIf.c b/src/aig/gia/giaIf.c
index 0f656b03..0e4686d8 100644
--- a/src/aig/gia/giaIf.c
+++ b/src/aig/gia/giaIf.c
@@ -2118,6 +2118,13 @@ void Gia_ManTransferPacking( Gia_Man_t * p, Gia_Man_t * pGia )
 }
 void Gia_ManTransferTiming( Gia_Man_t * p, Gia_Man_t * pGia )
 {
+    if ( pGia->vCiArrs || pGia->vCoReqs || pGia->vCoArrs )
+    {
+        p->vCiArrs     = pGia->vCiArrs;     pGia->vCiArrs    = NULL;
+        p->vCoReqs     = pGia->vCoReqs;     pGia->vCoReqs    = NULL;
+        p->vCoArrs     = pGia->vCoArrs;     pGia->vCoArrs    = NULL;
+        p->And2Delay   = pGia->And2Delay;
+    }
     if ( pGia->vInArrs || pGia->vOutReqs )
     {
         p->vInArrs     = pGia->vInArrs;     pGia->vInArrs     = NULL;
@@ -2146,6 +2153,70 @@ void Gia_ManTransferTiming( Gia_Man_t * p, Gia_Man_t * pGia )
 
 /**Function*************************************************************
 
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_FrameMiniAigSetCiArrivals( Abc_Frame_t * pAbc, int * pArrivals )
+{
+    Gia_Man_t * pGia;
+    if ( pArrivals == NULL )
+        { printf( "Arrival times are not given.\n" ); return; }
+    if ( pAbc == NULL )
+        { printf( "ABC framework is not initialized by calling Abc_Start().\n" ); return; }
+    pGia = Abc_FrameReadGia( pAbc );
+    if ( pGia == NULL )
+        { printf( "Current network in ABC framework is not defined.\n" ); return; }
+    Vec_IntFreeP( &pGia->vCiArrs );
+    pGia->vCiArrs = Vec_IntAllocArrayCopy( pArrivals, Gia_ManCiNum(pGia) );
+}
+void Abc_FrameMiniAigSetCoRequireds( Abc_Frame_t * pAbc, int * pRequireds )
+{
+    Gia_Man_t * pGia;
+    if ( pRequireds == NULL )
+        { printf( "Required times are not given.\n" ); return; }
+    if ( pAbc == NULL )
+        { printf( "ABC framework is not initialized by calling Abc_Start().\n" ); return; }
+    pGia = Abc_FrameReadGia( pAbc );
+    if ( pGia == NULL )
+        { printf( "Current network in ABC framework is not defined.\n" ); return; }
+    Vec_IntFreeP( &pGia->vCoReqs );
+    pGia->vCoReqs = Vec_IntAllocArrayCopy( pRequireds, Gia_ManCoNum(pGia) );
+}
+int * Abc_FrameMiniAigReadCoArrivals( Abc_Frame_t * pAbc )
+{
+    Vec_Int_t * vArrs; int * pArrs;
+    Gia_Man_t * pGia;
+    if ( pAbc == NULL )
+        { printf( "ABC framework is not initialized by calling Abc_Start()\n" ); return NULL; }
+    pGia = Abc_FrameReadGia( pAbc );
+    if ( pGia == NULL )
+        { printf( "Current network in ABC framework is not defined.\n" ); return NULL; }
+    if ( pGia->vCoArrs == NULL )
+        { printf( "Current network in ABC framework has no CO arrival times.\n" ); return NULL; }
+    vArrs = Vec_IntDup( pGia->vCoArrs );
+    pArrs = Vec_IntReleaseArray( vArrs );
+    Vec_IntFree( vArrs );
+    return pArrs;
+}
+void Abc_FrameMiniAigSetAndGateDelay( Abc_Frame_t * pAbc, int Delay )
+{
+    Gia_Man_t * pGia;
+    if ( pAbc == NULL )
+        printf( "ABC framework is not initialized by calling Abc_Start()\n" );
+    pGia = Abc_FrameReadGia( pAbc );
+    if ( pGia == NULL )
+        printf( "Current network in ABC framework is not defined.\n" );
+    pGia->And2Delay = Delay;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Interface of LUT mapping package.]
 
   Description []
@@ -2159,9 +2230,23 @@ Gia_Man_t * Gia_ManPerformMappingInt( Gia_Man_t * p, If_Par_t * pPars )
 {
     extern void Gia_ManIffTest( Gia_Man_t * pGia, If_LibLut_t * pLib, int fVerbose );
     Gia_Man_t * pNew;
-    If_Man_t * pIfMan;
+    If_Man_t * pIfMan; int i, Entry;
     assert( pPars->pTimesArr == NULL );
     assert( pPars->pTimesReq == NULL );
+    if ( p->vCiArrs )
+    {
+        assert( Vec_IntSize(p->vCiArrs) == Gia_ManCiNum(p) );
+        pPars->pTimesArr = ABC_CALLOC( float, Gia_ManCiNum(p) );
+        Vec_IntForEachEntry( p->vCiArrs, Entry, i )
+            pPars->pTimesArr[i] = (float)Entry;
+    }
+    if ( p->vCoReqs )
+    {
+        assert( Vec_IntSize(p->vCoReqs) == Gia_ManCoNum(p) );
+        pPars->pTimesReq = ABC_CALLOC( float, Gia_ManCoNum(p) );
+        Vec_IntForEachEntry( p->vCoReqs, Entry, i )
+            pPars->pTimesReq[i] = (float)Entry;
+    }
     ABC_FREE( p->pCellStr );
     Vec_IntFreeP( &p->vConfigs );
     // disable cut minimization when GIA strucure is needed
@@ -2202,6 +2287,14 @@ Gia_Man_t * Gia_ManPerformMappingInt( Gia_Man_t * p, If_Par_t * pPars )
         pNew = Gia_ManFromIfAig( pIfMan );
     else
         pNew = Gia_ManFromIfLogic( pIfMan );
+    if ( p->vCiArrs || p->vCoReqs )
+    {
+        If_Obj_t * pIfObj;
+        Vec_IntFreeP( &p->vCoArrs );
+        p->vCoArrs = Vec_IntAlloc( Gia_ManCoNum(p) );
+        If_ManForEachCo( pIfMan, pIfObj, i )
+            Vec_IntPush( p->vCoArrs, (int)If_ObjArrTime(If_ObjFanin0(pIfObj)) );
+    }
     If_ManStop( pIfMan );
     // transfer name
     assert( pNew->pName == NULL );
diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c
index 9ccab495..65ff46b5 100644
--- a/src/aig/gia/giaMan.c
+++ b/src/aig/gia/giaMan.c
@@ -128,6 +128,9 @@ void Gia_ManStop( Gia_Man_t * p )
     ABC_FREE( p->pCellStr );
     Vec_FltFreeP( &p->vInArrs );
     Vec_FltFreeP( &p->vOutReqs );
+    Vec_IntFreeP( &p->vCiArrs );
+    Vec_IntFreeP( &p->vCoReqs );
+    Vec_IntFreeP( &p->vCoArrs );
     Gia_ManStopP( &p->pAigExtra );
     Vec_IntFree( p->vCis );
     Vec_IntFree( p->vCos );
diff --git a/src/aig/gia/giaMini.c b/src/aig/gia/giaMini.c
index 67805d44..8d7e6801 100644
--- a/src/aig/gia/giaMini.c
+++ b/src/aig/gia/giaMini.c
@@ -20,7 +20,7 @@
 
 #include "gia.h"
 #include "opt/dau/dau.h"
-#include "base/main/main.h"
+#include "base/main/mainInt.h"
 #include "misc/util/utilTruth.h"
 #include "aig/miniaig/miniaig.h"
 #include "aig/miniaig/minilut.h"
@@ -57,7 +57,7 @@ int Gia_ObjFromMiniFanin1Copy( Gia_Man_t * pGia, Vec_Int_t * vCopies, Mini_Aig_t
     int Lit = Mini_AigNodeFanin1( p, Id );
     return Abc_LitNotCond( Vec_IntEntry(vCopies, Abc_Lit2Var(Lit)), Abc_LitIsCompl(Lit) );
 }
-Gia_Man_t * Gia_ManFromMiniAig( Mini_Aig_t * p )
+Gia_Man_t * Gia_ManFromMiniAig( Mini_Aig_t * p, Vec_Int_t ** pvCopies )
 {
     Gia_Man_t * pGia, * pTemp;
     Vec_Int_t * vCopies;
@@ -85,9 +85,14 @@ Gia_Man_t * Gia_ManFromMiniAig( Mini_Aig_t * p )
     }
     Gia_ManHashStop( pGia );
     assert( Vec_IntSize(vCopies) == nNodes );
-    Vec_IntFree( vCopies );
+    if ( pvCopies )
+        *pvCopies = vCopies;
+    else
+        Vec_IntFree( vCopies );
     Gia_ManSetRegNum( pGia, Mini_AigRegNum(p) );
     pGia = Gia_ManCleanup( pTemp = pGia );
+    if ( pvCopies )
+        Gia_ManDupRemapLiterals( *pvCopies, pTemp );
     Gia_ManStop( pTemp );
     return pGia;
 }
@@ -141,8 +146,11 @@ void Abc_FrameGiaInputMiniAig( Abc_Frame_t * pAbc, void * p )
     Gia_Man_t * pGia;
     if ( pAbc == NULL )
         printf( "ABC framework is not initialized by calling Abc_Start()\n" );
-    pGia = Gia_ManFromMiniAig( (Mini_Aig_t *)p );
+    Gia_ManStopP( &pAbc->pGiaMiniAig );
+    Vec_IntFreeP( &pAbc->vCopyMiniAig );
+    pGia = Gia_ManFromMiniAig( (Mini_Aig_t *)p, &pAbc->vCopyMiniAig );
     Abc_FrameUpdateGia( pAbc, pGia );
+    pAbc->pGiaMiniAig = Gia_ManDup( pGia );
 //    Gia_ManDelete( pGia );
 }
 void * Abc_FrameGiaOutputMiniAig( Abc_Frame_t * pAbc )
@@ -170,7 +178,7 @@ void * Abc_FrameGiaOutputMiniAig( Abc_Frame_t * pAbc )
 Gia_Man_t * Gia_ManReadMiniAig( char * pFileName )
 {
     Mini_Aig_t * p = Mini_AigLoad( pFileName );
-    Gia_Man_t * pGia = Gia_ManFromMiniAig( p );
+    Gia_Man_t * pGia = Gia_ManFromMiniAig( p, NULL );
     ABC_FREE( pGia->pName );
     pGia->pName = Extra_FileNameGeneric( pFileName ); 
     Mini_AigStop( p );
@@ -197,7 +205,7 @@ void Gia_ManWriteMiniAig( Gia_Man_t * pGia, char * pFileName )
   SeeAlso     []
 
 ***********************************************************************/
-Gia_Man_t * Gia_ManFromMiniLut( Mini_Lut_t * p )
+Gia_Man_t * Gia_ManFromMiniLut( Mini_Lut_t * p, Vec_Int_t ** pvCopies )
 {
     Gia_Man_t * pGia, * pTemp;
     Vec_Int_t * vCopies;
@@ -239,9 +247,14 @@ Gia_Man_t * Gia_ManFromMiniLut( Mini_Lut_t * p )
     Vec_IntFree( vLits );
     Gia_ManHashStop( pGia );
     assert( Vec_IntSize(vCopies) == nNodes );
-    Vec_IntFree( vCopies );
+    if ( pvCopies )
+        *pvCopies = vCopies;
+    else
+        Vec_IntFree( vCopies );
     Gia_ManSetRegNum( pGia, Mini_LutRegNum(p) );
     pGia = Gia_ManCleanup( pTemp = pGia );
+    if ( pvCopies )
+        Gia_ManDupRemapLiterals( *pvCopies, pTemp );
     Gia_ManStop( pTemp );
     return pGia;
 }
@@ -357,19 +370,24 @@ void Abc_FrameGiaInputMiniLut( Abc_Frame_t * pAbc, void * p )
     Gia_Man_t * pGia;
     if ( pAbc == NULL )
         printf( "ABC framework is not initialized by calling Abc_Start()\n" );
-    pGia = Gia_ManFromMiniLut( (Mini_Lut_t *)p );
+    pGia = Gia_ManFromMiniLut( (Mini_Lut_t *)p, NULL );
     Abc_FrameUpdateGia( pAbc, pGia );
 //    Gia_ManDelete( pGia );
 }
 void * Abc_FrameGiaOutputMiniLut( Abc_Frame_t * pAbc )
 {
+    Mini_Lut_t * pRes = NULL;
     Gia_Man_t * pGia;
     if ( pAbc == NULL )
         printf( "ABC framework is not initialized by calling Abc_Start()\n" );
+    Gia_ManStopP( &pAbc->pGiaMiniLut );
+    Vec_IntFreeP( &pAbc->vCopyMiniLut );
     pGia = Abc_FrameReadGia( pAbc );
     if ( pGia == NULL )
         printf( "Current network in ABC framework is not defined.\n" );
-    return Gia_ManToMiniLut( pGia );
+    pRes = Gia_ManToMiniLut( pGia );
+    pAbc->pGiaMiniLut = Gia_ManFromMiniLut( pRes, &pAbc->vCopyMiniLut );
+    return pRes;
 }
 
 /**Function*************************************************************
@@ -386,7 +404,7 @@ void * Abc_FrameGiaOutputMiniLut( Abc_Frame_t * pAbc )
 Gia_Man_t * Gia_ManReadMiniLut( char * pFileName )
 {
     Mini_Lut_t * p = Mini_LutLoad( pFileName );
-    Gia_Man_t * pGia = Gia_ManFromMiniLut( p );
+    Gia_Man_t * pGia = Gia_ManFromMiniLut( p, NULL );
     ABC_FREE( pGia->pName );
     pGia->pName = Extra_FileNameGeneric( pFileName ); 
     Mini_LutStop( p );
@@ -399,6 +417,102 @@ void Gia_ManWriteMiniLut( Gia_Man_t * pGia, char * pFileName )
     Mini_LutStop( p );
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int * Gia_ManMapMiniLut2MiniAig( Gia_Man_t * p, Gia_Man_t * p1, Gia_Man_t * p2, Vec_Int_t * vMap1, Vec_Int_t * vMap2 )
+{
+    int * pRes = ABC_FALLOC( int, Vec_IntSize(vMap2) );
+    Vec_Int_t * vMap = Vec_IntStartFull( Gia_ManObjNum(p) );
+    int i, Entry, iRepr, fCompl, iLit;
+    Gia_Obj_t * pObj;
+    Gia_ManSetPhase( p1 );
+    Gia_ManSetPhase( p2 );
+    Vec_IntForEachEntry( vMap1, Entry, i )
+    {
+        if ( Entry == -1 )
+            continue;
+        pObj = Gia_ManObj( p1, Abc_Lit2Var(Entry) );
+        if ( ~pObj->Value == 0 )
+            continue;
+        fCompl = Abc_LitIsCompl(Entry) ^ pObj->fPhase;
+        iRepr = Gia_ObjReprSelf(p, Abc_Lit2Var(pObj->Value));
+        Vec_IntWriteEntry( vMap, iRepr, Abc_Var2Lit(i, fCompl) );
+    }
+    Vec_IntForEachEntry( vMap2, Entry, i )
+    {
+        if ( Entry == -1 )
+            continue;
+        pObj = Gia_ManObj( p2, Abc_Lit2Var(Entry) );
+        if ( ~pObj->Value == 0 )
+            continue;
+        fCompl = Abc_LitIsCompl(Entry) ^ pObj->fPhase;
+        iRepr = Gia_ObjReprSelf(p, Abc_Lit2Var(pObj->Value));
+        if ( (iLit = Vec_IntEntry(vMap, iRepr)) == -1 )
+            continue;
+        pRes[i] = Abc_LitNotCond( iLit, fCompl ^ Abc_LitIsCompl(iLit) );
+    }
+    Vec_IntFill( vMap, Gia_ManCoNum(p1), -1 );
+    Vec_IntForEachEntry( vMap1, Entry, i )
+    {
+        if ( Entry == -1 )
+            continue;
+        pObj = Gia_ManObj( p1, Abc_Lit2Var(Entry) );
+        if ( !Gia_ObjIsCo(pObj) )
+            continue;
+        Vec_IntWriteEntry( vMap, Gia_ObjCioId(pObj), i );
+    }
+    Vec_IntForEachEntry( vMap2, Entry, i )
+    {
+        if ( Entry == -1 )
+            continue;
+        pObj = Gia_ManObj( p2, Abc_Lit2Var(Entry) );
+        if ( !Gia_ObjIsCo(pObj) )
+            continue;
+        assert( pRes[i] == -1 );
+        pRes[i] = Abc_Var2Lit( Vec_IntEntry(vMap, Gia_ObjCioId(pObj)), 0 );
+        assert( pRes[i] != -1 );
+    }
+    Vec_IntFree( vMap );
+    return pRes;
+}
+int * Abc_FrameReadMiniLutNameMapping( Abc_Frame_t * pAbc )
+{
+    int fVerbose = 0;
+    int nConfs = 1000;
+    Gia_Man_t * pGia, * pTemp;
+    int * pRes = NULL;
+    if ( pAbc->pGiaMiniAig == NULL )
+        printf( "GIA derived from MiniAig is not available.\n" );
+    if ( pAbc->pGiaMiniLut == NULL )
+        printf( "GIA derived from MiniLut is not available.\n" );
+    if ( pAbc->pGiaMiniAig == NULL || pAbc->pGiaMiniLut == NULL )
+        return NULL;
+    pGia = Gia_ManDup2( pAbc->pGiaMiniAig, pAbc->pGiaMiniLut );
+    //Gia_AigerWrite( pGia, "aig_m_lut.aig", 0, 0 );
+    // compute equivalences in this AIG
+    pTemp = Gia_ManComputeGiaEquivs( pGia, nConfs, fVerbose );
+    Gia_ManStop( pTemp );
+    //if ( fVerbose )
+    //    Abc_PrintTime( 1, "Equivalence computation time", Abc_Clock() - clk );
+    //if ( fVerbose )
+    //    Gia_ManPrintStats( pGia, NULL );
+    //Vec_IntPrint( pAbc->vCopyMiniAig );
+    //Vec_IntPrint( pAbc->vCopyMiniLut );
+    pRes = Gia_ManMapMiniLut2MiniAig( pGia, pAbc->pGiaMiniAig, pAbc->pGiaMiniLut, pAbc->vCopyMiniAig, pAbc->vCopyMiniLut );
+    Gia_ManStop( pGia );
+    return pRes;
+}
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/miniaig/minilut.h b/src/aig/miniaig/minilut.h
index e84428d4..fb5c6f06 100644
--- a/src/aig/miniaig/minilut.h
+++ b/src/aig/miniaig/minilut.h
@@ -123,9 +123,9 @@ static int      Mini_LutNodeConst1()                           { return 1;
 
 static int      Mini_LutNodeNum( Mini_Lut_t * p )              { return p->nSize;             }
 static int      Mini_LutNodeIsConst( Mini_Lut_t * p, int Id )  { assert( Id >= 0 ); return Id == 0 || Id == 1; }
-static int      Mini_LutNodeIsPi( Mini_Lut_t * p, int Id )     { assert( Id >= 0 ); return Id > 0 && Mini_LutNodeFanin( p, Id, 0 ) == MINI_LUT_NULL; }
-static int      Mini_LutNodeIsPo( Mini_Lut_t * p, int Id )     { assert( Id >= 0 ); return Id > 0 && Mini_LutNodeFanin( p, Id, 0 ) != MINI_LUT_NULL && Mini_LutNodeFanin( p, Id, 1 ) == MINI_LUT_NULL2; }
-static int      Mini_LutNodeIsNode( Mini_Lut_t * p, int Id )   { assert( Id >= 0 ); return Id > 0 && Mini_LutNodeFanin( p, Id, 0 ) != MINI_LUT_NULL && Mini_LutNodeFanin( p, Id, 1 ) != MINI_LUT_NULL2; }
+static int      Mini_LutNodeIsPi( Mini_Lut_t * p, int Id )     { assert( Id >= 0 ); return Id > 1 && Mini_LutNodeFanin( p, Id, 0 ) == MINI_LUT_NULL; }
+static int      Mini_LutNodeIsPo( Mini_Lut_t * p, int Id )     { assert( Id >= 0 ); return Id > 1 && Mini_LutNodeFanin( p, Id, 0 ) != MINI_LUT_NULL && Mini_LutNodeFanin( p, Id, 1 ) == MINI_LUT_NULL2; }
+static int      Mini_LutNodeIsNode( Mini_Lut_t * p, int Id )   { assert( Id >= 0 ); return Id > 1 && Mini_LutNodeFanin( p, Id, 0 ) != MINI_LUT_NULL && Mini_LutNodeFanin( p, Id, 1 ) != MINI_LUT_NULL2; }
 
 static int      Mini_LutSize( Mini_Lut_t * p )                 { return p->LutSize;           }
 
diff --git a/src/base/main/mainFrame.c b/src/base/main/mainFrame.c
index cd4ff2c7..7d9edecf 100644
--- a/src/base/main/mainFrame.c
+++ b/src/base/main/mainFrame.c
@@ -227,6 +227,12 @@ void Abc_FrameDeallocate( Abc_Frame_t * p )
     Vec_IntFreeP( &p->pAbcWlcInv );
     Abc_NamDeref( s_GlobalFrame->pJsonStrs );
     Vec_WecFreeP(&s_GlobalFrame->vJsonObjs );    
+
+    Gia_ManStopP( &p->pGiaMiniAig );
+    Gia_ManStopP( &p->pGiaMiniLut );
+    Vec_IntFreeP( &p->vCopyMiniAig );
+    Vec_IntFreeP( &p->vCopyMiniLut );
+
     ABC_FREE( p );
     s_GlobalFrame = NULL;
 }
diff --git a/src/base/main/mainInt.h b/src/base/main/mainInt.h
index 278a9191..30671fcb 100644
--- a/src/base/main/mainInt.h
+++ b/src/base/main/mainInt.h
@@ -137,6 +137,10 @@ struct Abc_Frame_t_
 #ifdef ABC_USE_CUDD
     DdManager *     dd;            // temporary BDD package
 #endif
+    Gia_Man_t *     pGiaMiniAig; 
+    Gia_Man_t *     pGiaMiniLut; 
+    Vec_Int_t *     vCopyMiniAig;
+    Vec_Int_t *     vCopyMiniLut;
 };
 
 typedef void (*Abc_Frame_Initialization_Func)( Abc_Frame_t * pAbc );
diff --git a/src/map/if/ifLibLut.c b/src/map/if/ifLibLut.c
index 1033cc1f..94946390 100644
--- a/src/map/if/ifLibLut.c
+++ b/src/map/if/ifLibLut.c
@@ -19,6 +19,7 @@
 ***********************************************************************/
 
 #include "if.h"
+#include "base/main/mainInt.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -27,8 +28,6 @@ ABC_NAMESPACE_IMPL_START
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static inline char * If_UtilStrsav( char *s ) {  return !s ? s : strcpy(ABC_ALLOC(char, strlen(s)+1), s);  }
-
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -44,6 +43,162 @@ static inline char * If_UtilStrsav( char *s ) {  return !s ? s : strcpy(ABC_ALLO
   SeeAlso     []
 
 ***********************************************************************/
+If_LibLut_t * If_LibLutReadString( char * pStr )
+{
+    If_LibLut_t * p;
+    Vec_Ptr_t * vStrs;
+    char * pToken, * pBuffer, * pStrNew, * pStrMem;
+    int i, k, j;
+
+    if ( pStr == NULL || pStr[0] == 0 )
+        return NULL;
+
+    vStrs = Vec_PtrAlloc( 1000 );
+    pStrNew = pStrMem = Abc_UtilStrsav( pStr );
+    while ( *pStrNew )
+    {
+        Vec_PtrPush( vStrs, pStrNew );
+        while ( *pStrNew != '\n' )
+            pStrNew++;
+        while ( *pStrNew == '\n' )
+            *pStrNew++ = '\0';
+    }
+
+    p = ABC_ALLOC( If_LibLut_t, 1 );
+    memset( p, 0, sizeof(If_LibLut_t) );
+
+    i = 1;
+    //while ( fgets( pBuffer, 1000, pFile ) != NULL )
+    Vec_PtrForEachEntry( char *, vStrs, pBuffer, j )
+    {
+        if ( pBuffer[0] == 0 )
+            continue;
+        pToken = strtok( pBuffer, " \t\n" );
+        if ( pToken == NULL )
+            continue;
+        if ( pToken[0] == '#' )
+            continue;
+        if ( i != atoi(pToken) )
+        {
+            Abc_Print( 1, "Error in the LUT library string.\n" );
+            ABC_FREE( p->pName );
+            ABC_FREE( p );
+            ABC_FREE( pStrMem );
+            Vec_PtrFree( vStrs );
+            return NULL;
+        }
+
+        // read area
+        pToken = strtok( NULL, " \t\n" );
+        p->pLutAreas[i] = (float)atof(pToken);
+
+        // read delays
+        k = 0;
+        while ( (pToken = strtok( NULL, " \t\n" )) )
+            p->pLutDelays[i][k++] = (float)atof(pToken);
+
+        // check for out-of-bound
+        if ( k > i )
+        {
+            Abc_Print( 1, "LUT %d has too many pins (%d). Max allowed is %d.\n", i, k, i );
+            ABC_FREE( p->pName );
+            ABC_FREE( p );
+            ABC_FREE( pStrMem );
+            Vec_PtrFree( vStrs );
+            return NULL;
+        }
+
+        // check if var delays are specified
+        if ( k > 1 )
+            p->fVarPinDelays = 1;
+
+        if ( i == IF_MAX_LUTSIZE )
+        {
+            Abc_Print( 1, "Skipping LUTs of size more than %d.\n", i );
+            ABC_FREE( p->pName );
+            ABC_FREE( p );
+            ABC_FREE( pStrMem );
+            Vec_PtrFree( vStrs );
+            return NULL;
+        }
+        i++;
+    }
+    p->LutMax = i-1;
+
+    // check the library
+    if ( p->fVarPinDelays )
+    {
+        for ( i = 1; i <= p->LutMax; i++ )
+            for ( k = 0; k < i; k++ )
+            {
+                if ( p->pLutDelays[i][k] <= 0.0 )
+                    Abc_Print( 0, "Pin %d of LUT %d has delay %f. Pin delays should be non-negative numbers. Technology mapping may not work correctly.\n", 
+                        k, i, p->pLutDelays[i][k] );
+                if ( k && p->pLutDelays[i][k-1] > p->pLutDelays[i][k] )
+                    Abc_Print( 0, "Pin %d of LUT %d has delay %f. Pin %d of LUT %d has delay %f. Pin delays should be in non-decreasing order. Technology mapping may not work correctly.\n", 
+                        k-1, i, p->pLutDelays[i][k-1], 
+                        k, i, p->pLutDelays[i][k] );
+            }
+    }
+    else
+    {
+        for ( i = 1; i <= p->LutMax; i++ )
+        {
+            if ( p->pLutDelays[i][0] <= 0.0 )
+                Abc_Print( 0, "LUT %d has delay %f. Pin delays should be non-negative numbers. Technology mapping may not work correctly.\n", 
+                    i, p->pLutDelays[i][0] );
+        }
+    }
+
+    // cleanup
+    ABC_FREE( pStrMem );
+    Vec_PtrFree( vStrs );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Sets the library associated with the string.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_FrameSetLutLibrary( Abc_Frame_t * pAbc, char * pLutLibString )
+{
+    If_LibLut_t * pLib = If_LibLutReadString( pLutLibString );
+    if ( pLib == NULL )
+    {
+        fprintf( stdout, "Reading LUT library from string has failed.\n" );
+        return 0;
+    }
+    // replace the current library
+    If_LibLutFree( (If_LibLut_t *)Abc_FrameReadLibLut() );
+    Abc_FrameSetLibLut( pLib );
+    return 1;
+}
+int Abc_FrameSetLutLibraryTest( Abc_Frame_t * pAbc )
+{
+    char * pStr = "1 1.00  1000\n2 1.00  1000 1200\n3 1.00  1000 1200 1400\n4 1.00  1000 1200 1400 1600\n5 1.00  1000 1200 1400 1600 1800\n6 1.00  1000 1200 1400 1600 1800 2000\n\n\n";
+    Abc_FrameSetLutLibrary( pAbc, pStr );
+    return 1;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Reads the description of LUTs from the LUT library file.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 If_LibLut_t * If_LibLutRead( char * FileName )
 {
     char pBuffer[1000], * pToken;
@@ -60,7 +215,7 @@ If_LibLut_t * If_LibLutRead( char * FileName )
 
     p = ABC_ALLOC( If_LibLut_t, 1 );
     memset( p, 0, sizeof(If_LibLut_t) );
-    p->pName = If_UtilStrsav( FileName );
+    p->pName = Abc_UtilStrsav( FileName );
 
     i = 1;
     while ( fgets( pBuffer, 1000, pFile ) != NULL )
@@ -159,7 +314,7 @@ If_LibLut_t * If_LibLutDup( If_LibLut_t * p )
     If_LibLut_t * pNew;
     pNew = ABC_ALLOC( If_LibLut_t, 1 );
     *pNew = *p;
-    pNew->pName = If_UtilStrsav( pNew->pName );
+    pNew->pName = Abc_UtilStrsav( pNew->pName );
     return pNew;
 }
 
diff --git a/src/map/if/ifTime.c b/src/map/if/ifTime.c
index c2ba40e8..9ceef147 100644
--- a/src/map/if/ifTime.c
+++ b/src/map/if/ifTime.c
@@ -315,6 +315,9 @@ void If_ManComputeRequired( If_Man_t * p )
     If_ManMarkMapping( p );
     if ( p->pManTim == NULL )
     {
+        // get the global required times
+        p->RequiredGlo = If_ManDelayMax( p, 0 );
+
         // consider the case when the required times are given
         if ( p->pPars->pTimesReq && !p->pPars->fAreaOnly )
         {
@@ -340,9 +343,6 @@ void If_ManComputeRequired( If_Man_t * p )
         }
         else
         {
-            // get the global required times
-            p->RequiredGlo = If_ManDelayMax( p, 0 );
-
             // find new delay target
             if ( p->pPars->nRelaxRatio && p->pPars->DelayTargetNew == 0 )
                 p->pPars->DelayTargetNew = p->RequiredGlo * (100.0 + p->pPars->nRelaxRatio) / 100.0;