Experiments with word-level data structures.

6 files changed, 241 insertions, 33 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index d871905c..488f12cf 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -1312,6 +1312,8 @@ 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_ManDupNoBuf( Gia_Man_t * p );  
+extern Gia_Man_t *         Gia_ManDupMap( Gia_Man_t * p, Vec_Int_t * vMap );
 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_ManDupRemovePis( Gia_Man_t * p, int nRemPis );
diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c
index 55f8901f..4f094b48 100644
--- a/src/aig/gia/giaDup.c
+++ b/src/aig/gia/giaDup.c
@@ -811,6 +811,55 @@ Gia_Man_t * Gia_ManDupRemovePis( Gia_Man_t * p, int nRemPis )
     Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
     return pNew;
 }
+Gia_Man_t * Gia_ManDupNoBuf( Gia_Man_t * p )
+{
+    Gia_Man_t * pNew;
+    Gia_Obj_t * pObj;
+    int i;
+    pNew = Gia_ManStart( Gia_ManObjNum(p) );
+    pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+    Gia_ManConst0(p)->Value = 0;
+    Gia_ManForEachObj1( p, pObj, i )
+    {
+        if ( Gia_ObjIsBuf(pObj) )
+            pObj->Value = Gia_ObjFanin0Copy(pObj);
+        else if ( Gia_ObjIsAnd(pObj) )
+            pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+        else if ( Gia_ObjIsCi(pObj) )
+            pObj->Value = Gia_ManAppendCi( pNew );
+        else if ( Gia_ObjIsCo(pObj) )
+            pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+    }
+    Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
+    return pNew;
+}
+Gia_Man_t * Gia_ManDupMap( Gia_Man_t * p, Vec_Int_t * vMap )
+{
+    Gia_Man_t * pNew, * pTemp;
+    Gia_Obj_t * pObj;
+    int i;
+    pNew = Gia_ManStart( Gia_ManObjNum(p) );
+    pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+    Gia_ManConst0(p)->Value = 0;
+    Gia_ManHashAlloc( pNew );
+    Gia_ManForEachObj1( p, pObj, i )
+    {
+        if ( Vec_IntEntry(vMap, i) >= 0 )
+            pObj->Value = Gia_ManObj( p, Vec_IntEntry(vMap, i) )->Value;
+        else if ( Gia_ObjIsAnd(pObj) )
+            pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+        else if ( Gia_ObjIsCi(pObj) )
+            pObj->Value = Gia_ManAppendCi( pNew );
+        else if ( Gia_ObjIsCo(pObj) )
+            pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+    }
+    pNew = Gia_ManCleanup( pTemp = pNew );
+    Gia_ManStop( pTemp );
+    Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
+    return pNew;
+}
 
 /**Function*************************************************************
 
@@ -865,7 +914,9 @@ Gia_Man_t * Gia_ManDupPerm( Gia_Man_t * p, Vec_Int_t * vPiPerm )
 //    Vec_IntFree( vPiPermInv );
     Gia_ManForEachObj1( p, pObj, i )
     {
-        if ( Gia_ObjIsAnd(pObj) )
+        if ( Gia_ObjIsBuf(pObj) )
+            pObj->Value = Gia_ManAppendBuf( pNew, Gia_ObjFanin0Copy(pObj) );
+        else if ( Gia_ObjIsAnd(pObj) )
             pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
         else if ( Gia_ObjIsCi(pObj) )
         {
@@ -1086,7 +1137,7 @@ Gia_Man_t * Gia_ManDupAppendNew( Gia_Man_t * pOne, Gia_Man_t * pTwo )
     Gia_ManSetRegNum( pNew, Gia_ManRegNum(pOne) + Gia_ManRegNum(pTwo) );
     return pNew;
 }
-void Gia_ManDupRebuild( Gia_Man_t * pNew, Gia_Man_t * p, Vec_Int_t * vLits )
+void Gia_ManDupRebuild( Gia_Man_t * pNew, Gia_Man_t * p, Vec_Int_t * vLits, int fBufs )
 {
     Gia_Obj_t * pObj; int i;
     assert( Vec_IntSize(vLits) == Gia_ManCiNum(p) );
@@ -1094,7 +1145,10 @@ void Gia_ManDupRebuild( Gia_Man_t * pNew, Gia_Man_t * p, Vec_Int_t * vLits )
     Gia_ManForEachCi( p, pObj, i )
         pObj->Value = Vec_IntEntry(vLits, i);
     Gia_ManForEachAnd( p, pObj, i )
-        pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+        if ( fBufs && Gia_ObjIsBuf(pObj) )
+            pObj->Value = Gia_ManAppendBuf( pNew, Gia_ObjFanin0Copy(pObj) );
+        else
+            pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
     Vec_IntClear( vLits );
     Gia_ManForEachCo( p, pObj, i )
         Vec_IntPush( vLits, Gia_ObjFanin0Copy(pObj) );
@@ -2980,8 +3034,15 @@ Gia_Man_t * Gia_ManMiterInverse( Gia_Man_t * pBot, Gia_Man_t * pTop, int fDualOu
     Gia_ManHashAlloc( pNew );
     Gia_ManForEachCi( pBot, pObj, i )
         pObj->Value = Gia_ManAppendCi( pNew );
-    Gia_ManForEachCo( pBot, pObj, i )
-        Gia_ManMiter_rec( pNew, pBot, Gia_ObjFanin0(pObj) );
+//    Gia_ManForEachCo( pBot, pObj, i )
+//        Gia_ManMiter_rec( pNew, pBot, Gia_ObjFanin0(pObj) );
+    Gia_ManForEachAnd( pBot, pObj, i )
+    {
+        if ( Gia_ObjIsBuf(pObj) )
+            pObj->Value = Gia_ManAppendBuf( pNew, Gia_ObjFanin0Copy(pObj) );
+        else if ( Gia_ObjIsAnd(pObj) )
+            pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+    }
     Gia_ManForEachCo( pBot, pObj, i )
         pObj->Value = Gia_ObjFanin0Copy(pObj);
     Gia_ManForEachCi( pTop, pObj, i )
@@ -2989,8 +3050,15 @@ Gia_Man_t * Gia_ManMiterInverse( Gia_Man_t * pBot, Gia_Man_t * pTop, int fDualOu
             pObj->Value = Gia_ManCi(pBot, i)->Value;
         else
             pObj->Value = Gia_ManCo(pBot, i-nInputs1)->Value;
-    Gia_ManForEachCo( pTop, pObj, i )
-        Gia_ManMiter_rec( pNew, pTop, Gia_ObjFanin0(pObj) );
+//    Gia_ManForEachCo( pTop, pObj, i )
+//        Gia_ManMiter_rec( pNew, pTop, Gia_ObjFanin0(pObj) );
+    Gia_ManForEachAnd( pTop, pObj, i )
+    {
+        if ( Gia_ObjIsBuf(pObj) )
+            pObj->Value = Gia_ManAppendBuf( pNew, Gia_ObjFanin0Copy(pObj) );
+        else if ( Gia_ObjIsAnd(pObj) )
+            pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+    }
     Gia_ManForEachCo( pTop, pObj, i )
     {
         if ( fDualOut )
@@ -3007,6 +3075,14 @@ Gia_Man_t * Gia_ManMiterInverse( Gia_Man_t * pBot, Gia_Man_t * pTop, int fDualOu
     Gia_ManHashStop( pNew );
     pNew = Gia_ManCleanup( pTemp = pNew );
     Gia_ManStop( pTemp );
+    assert( (pBot->vBarBufs == NULL) == (pTop->vBarBufs == NULL) );
+    if ( pBot->vBarBufs )
+    {
+        pNew->vBarBufs = Vec_IntAlloc( 1000 );
+        Vec_IntAppend( pNew->vBarBufs, pBot->vBarBufs );
+        Vec_IntAppend( pNew->vBarBufs, pTop->vBarBufs );
+        //printf( "Miter has %d buffers (%d groups).\n", pNew->nBufs, Vec_IntSize(pNew->vBarBufs) );
+    }
     return pNew;
 }
 
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 06d7cb08..db0446c9 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -13996,6 +13996,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
     //Dau_NetworkEnumTest();
     //Extra_SimulationTest( nDivMax, nNumOnes, fNewOrder );
     //Mnist_ExperimentWithScaling( nDecMax );
+    //Gyx_ProblemSolveTest();
     return 0;
 usage:
     Abc_Print( -2, "usage: test [-CKDNM] [-aovwh] <file_name>\n" );
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index f6818010..677cb7d0 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -658,6 +658,33 @@ Abc_Ntk_t * Abc_NtkFromAigPhase( Aig_Man_t * pMan )
 }
 
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkFromGiaCollapse( Gia_Man_t * pGia )
+{
+    Aig_Man_t * pMan = Gia_ManToAig( pGia, 0 ); int Res;
+    Abc_Ntk_t * pNtk = Abc_NtkFromAigPhase( pMan ), * pTemp;
+    //pNtk->pName      = Extra_UtilStrsav(pGia->pName);
+    Aig_ManStop( pMan );
+    // collapse the network 
+    pNtk = Abc_NtkCollapse( pTemp = pNtk, 10000, 0, 1, 0, 0, 0 );
+    Abc_NtkDelete( pTemp );
+    if ( pNtk == NULL )
+        return 0;
+    Res = Abc_NtkGetBddNodeNum( pNtk );
+    Abc_NtkDelete( pNtk );
+    return Res == 0;
+}
+
 
 /**Function*************************************************************
 
diff --git a/src/base/wln/wlnCom.c b/src/base/wln/wlnCom.c
index 90ac4faa..a010c7c2 100644
--- a/src/base/wln/wlnCom.c
+++ b/src/base/wln/wlnCom.c
@@ -276,7 +276,7 @@ usage:
 int Abc_CommandSolve( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     extern void Rtl_LibBlast( Rtl_Lib_t * pLib );
-    extern void Rtl_LibBlast2( Rtl_Lib_t * pLib, Vec_Int_t * vRoots );
+    extern void Rtl_LibBlast2( Rtl_Lib_t * pLib, Vec_Int_t * vRoots, int fInv );
     extern void Rtl_LibSolve( Rtl_Lib_t * pLib, void * pNtk );
     extern void Rtl_LibPreprocess( Rtl_Lib_t * pLib );
     extern void Wln_SolveWithGuidance( char * pFileName, Rtl_Lib_t * p );
@@ -327,7 +327,7 @@ int Abc_CommandSolve( Abc_Frame_t * pAbc, int argc, char ** argv )
         if ( fOldBlast )
             Rtl_LibBlast( pLib );
         else
-            Rtl_LibBlast2( pLib, NULL );
+            Rtl_LibBlast2( pLib, NULL, 0 );
         if ( fPrepro )
             Rtl_LibPreprocess( pLib );
         Rtl_LibSolve( pLib, NULL );
diff --git a/src/base/wln/wlnRead.c b/src/base/wln/wlnRead.c
index 95d2dd31..43003075 100644
--- a/src/base/wln/wlnRead.c
+++ b/src/base/wln/wlnRead.c
@@ -73,6 +73,7 @@ struct Rtl_Ntk_t_
     int                   Slice0;    // first slice
     int                   Slice1;    // last slice
     int                   iCopy;     // place in array
+    int                   fRoot;     // denote root network
 };
 
 static inline int         Rtl_LibNtkNum( Rtl_Lib_t * pLib )                { return Vec_PtrSize(pLib->vNtks);                  }
@@ -155,6 +156,7 @@ static inline int         Rtl_SigIsConcat( int s )                         { ret
     Rtl_CellForEachConnect( p, pCell, Par, Val, i ) if ( i <  Rtl_CellInputNum(pCell) ) continue; else
 
 extern Gia_Man_t * Cec4_ManSimulateTest3( Gia_Man_t * p, int nBTLimit, int fVerbose );
+extern int         Abc_NtkFromGiaCollapse( Gia_Man_t * pGia );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -1750,16 +1752,34 @@ void Rtl_NtkBlastConnect( Gia_Man_t * pNew, Rtl_Ntk_t * p, int * pCon )
 void Rtl_NtkBlastHierarchy( Gia_Man_t * pNew, Rtl_Ntk_t * p, int * pCell )
 {
     extern Gia_Man_t * Rtl_NtkBlast( Rtl_Ntk_t * p );
-    extern void Gia_ManDupRebuild( Gia_Man_t * pNew, Gia_Man_t * p, Vec_Int_t * vLits );
+    extern void Gia_ManDupRebuild( Gia_Man_t * pNew, Gia_Man_t * p, Vec_Int_t * vLits, int fBufs );
+    extern int Gia_ManFindFirst( Rtl_Ntk_t * p, int * pnOuts );
     Rtl_Ntk_t * pModel = Rtl_NtkModule( p, Rtl_CellModule(pCell)-ABC_INFINITY );
+    int nOuts1, iFirst1 = Gia_ManFindFirst( pModel, &nOuts1 );
     int k, Par, Val, nBits = 0;
+    //printf( "Blasting %s -> %s...\n", Rtl_NtkName(p), Rtl_NtkName(pModel) );
     Vec_IntClear( &p->vBitTemp );
     Rtl_CellForEachInput( p, pCell, Par, Val, k )
         Rtl_NtkCollectSignalRange( p, Val );
 //    if ( pModel->pGia == NULL )
 //        pModel->pGia = Rtl_NtkBlast( pModel );
     assert( pModel->pGia );
-    Gia_ManDupRebuild( pNew, pModel->pGia, &p->vBitTemp );
+    if ( pModel->fRoot )
+    {
+        Vec_IntForEachEntry( &p->vBitTemp, Val, k )
+            Vec_IntWriteEntry( &p->vBitTemp, k, (k >= iFirst1 && k < iFirst1 + nOuts1) ? Gia_ManAppendBuf(pNew, Val) : Val );
+        Vec_IntPush( pNew->vBarBufs, Abc_Var2Lit(pModel->NameId, 0) );
+    }
+    Gia_ManDupRebuild( pNew, pModel->pGia, &p->vBitTemp, !pModel->fRoot );
+    if ( !pModel->fRoot )
+        Vec_IntAppend( pNew->vBarBufs, pModel->pGia->vBarBufs );
+    if ( pModel->fRoot )
+    {
+        Vec_IntForEachEntry( &p->vBitTemp, Val, k )
+            Vec_IntWriteEntry( &p->vBitTemp, k, Gia_ManAppendBuf(pNew, Val) );
+        Vec_IntPush( pNew->vBarBufs, Abc_Var2Lit(pModel->NameId, 1) );
+        printf( "Added %d and %d output buffers for module %s.\n", nOuts1, Vec_IntSize(&p->vBitTemp), Rtl_NtkName(pModel) );
+    }
     Rtl_CellForEachOutput( p, pCell, Par, Val, k )
         nBits += Rtl_NtkInsertSignalRange( p, Val, Vec_IntArray(&p->vBitTemp)+nBits, Vec_IntSize(&p->vBitTemp)-nBits );
     assert( nBits == Vec_IntSize(&p->vBitTemp) );
@@ -1821,6 +1841,16 @@ char * Rtl_ShortenName( char * pName, int nSize )
     Buffer[nSize-0] = 0;
     return Buffer;
 }
+void Rtl_NtkPrintBufs( Rtl_Ntk_t * p, Vec_Int_t * vBufs )
+{
+    int i, Lit;
+    if ( Vec_IntSize(vBufs) )
+        printf( "Found %d buffers:  ", p->pGia->nBufs );
+    Vec_IntForEachEntry( vBufs, Lit, i )
+        printf( "%s (%c)  ", Rtl_LibStr(p->pLib, Abc_Lit2Var(Lit)), Abc_LitIsCompl(Lit)? 'o' : 'i' );
+    if ( Vec_IntSize(vBufs) )
+        printf( "\n" );
+}
 Gia_Man_t * Rtl_NtkBlast( Rtl_Ntk_t * p )
 {
     Gia_Man_t * pTemp, * pNew = Gia_ManStart( 1000 );
@@ -2068,6 +2098,7 @@ printf( "Blasting %s...\r", Rtl_NtkName(p) );
     Rtl_NtkBlastMap( p, nBits );
     assert( p->pGia == NULL );
     p->pGia = Gia_ManStart( 1000 );
+    p->pGia->vBarBufs = Vec_IntAlloc( 1000 );
     Rtl_NtkBlastInputs( p->pGia, p );
     Gia_ManHashAlloc( p->pGia );
     for ( i = 0; i < p->nOutputs; i++ )
@@ -2081,7 +2112,10 @@ printf( "Blasting %s...\r", Rtl_NtkName(p) );
     Rtl_NtkBlastOutputs( p->pGia, p );
     Rtl_NtkMapWires( p, 1 );
     p->pGia = Gia_ManCleanup( pTemp = p->pGia );
+    ABC_SWAP( Vec_Int_t *, p->pGia->vBarBufs, pTemp->vBarBufs );
     Gia_ManStop( pTemp );
+//    if ( p->fRoot )
+//        Rtl_NtkPrintBufs( p, p->pGia->vBarBufs );
 
 sprintf( Buffer, "new%02d.aig", counter++ );
 Gia_AigerWrite( p->pGia, Buffer, 0, 0, 0 );
@@ -2103,7 +2137,7 @@ void Rtl_LibMark_rec( Rtl_Ntk_t * pNtk )
     assert( pNtk->iCopy == -2 );
     pNtk->iCopy = -1;
 }
-void Rtl_LibBlast2( Rtl_Lib_t * pLib, Vec_Int_t * vRoots )
+void Rtl_LibBlast2( Rtl_Lib_t * pLib, Vec_Int_t * vRoots, int fInv )
 {
     Rtl_Ntk_t * pNtk; int i, iNtk;
     Vec_PtrForEachEntry( Rtl_Ntk_t *, pLib->vNtks, pNtk, i )
@@ -2111,9 +2145,13 @@ void Rtl_LibBlast2( Rtl_Lib_t * pLib, Vec_Int_t * vRoots )
     if ( vRoots )
     {
         Vec_PtrForEachEntry( Rtl_Ntk_t *, pLib->vNtks, pNtk, i )
-            pNtk->iCopy = -2;
+            pNtk->iCopy = -2, pNtk->fRoot = 0;
         Vec_IntForEachEntry( vRoots, iNtk, i )
-            Rtl_LibMark_rec( Rtl_LibNtk(pLib, iNtk) );
+        {
+            Rtl_Ntk_t * pNtk = Rtl_LibNtk(pLib, iNtk);
+            pNtk->fRoot = fInv;
+            Rtl_LibMark_rec( pNtk );
+        }
     }
     Vec_PtrForEachEntry( Rtl_Ntk_t *, pLib->vNtks, pNtk, i )
         if ( pNtk->iCopy == -1 && pNtk->pGia == NULL )
@@ -2211,15 +2249,18 @@ finish:
         if ( p != p1 && p != p2 )
             Gia_ManStopP( &p->pGia );
     //Rtl_LibBlast( pLib );
-    Rtl_LibBlast2( pLib, NULL );
+    Rtl_LibBlast2( pLib, NULL, 0 );
 }
 void Rtl_LibSolve( Rtl_Lib_t * pLib, void * pNtk )
 {
+    extern Gia_Man_t * Gia_ManReduceBuffers( Rtl_Lib_t * pLib, Gia_Man_t * p );
     abctime clk = Abc_Clock(); int Status;
-    Rtl_Ntk_t * pTop = pNtk ? (Rtl_Ntk_t *)pNtk : Rtl_LibTop( pLib );
-    Gia_Man_t * pSwp = Cec4_ManSimulateTest3( pTop->pGia, 1000000, 0 );
+    Rtl_Ntk_t * pTop  = pNtk ? (Rtl_Ntk_t *)pNtk : Rtl_LibTop( pLib );
+    Gia_Man_t * pGia2 = Gia_ManReduceBuffers( pLib, pTop->pGia );
+    Gia_Man_t * pSwp  = Cec4_ManSimulateTest3( pGia2, 1000000, 0 );
     int RetValue = Gia_ManAndNum(pSwp);
     Gia_ManStop( pSwp );
+    Gia_ManStop( pGia2 );
     if ( RetValue == 0 )
         printf( "Verification problem solved after SAT sweeping!  " );
     else
@@ -2263,14 +2304,19 @@ void Wln_SolveEqual( Rtl_Lib_t * p, int iNtk1, int iNtk2 )
     else if ( 1 )
     {
         Gia_Man_t * pGia = Gia_ManMiter( pNtk1->pGia, pNtk2->pGia, 0, 0, 0, 0, 0 );
-        Gia_Man_t * pNew = Cec4_ManSimulateTest3( pGia, 10000000, 0 );
-        //printf( "Miter %d -> %d\n",  Gia_ManAndNum(pGia),  Gia_ManAndNum(pNew) );
-        if ( Gia_ManAndNum(pNew) == 0 )
-            Abc_Print( 1, "Networks are equivalent.  " );
+        if ( Abc_NtkFromGiaCollapse( pGia ) )
+            Abc_Print( 1, "Networks are equivalent after collapsing.  " );
         else
-            Abc_Print( 1, "Networks are UNDECIDED.  " );
-        Gia_ManStopP( &pNew );
-        Gia_ManStopP( &pGia );
+        {
+            Gia_Man_t * pNew = Cec4_ManSimulateTest3( pGia, 10000000, 0 );
+            //printf( "Miter %d -> %d\n",  Gia_ManAndNum(pGia),  Gia_ManAndNum(pNew) );
+            if ( Gia_ManAndNum(pNew) == 0 )
+                Abc_Print( 1, "Networks are equivalent.  " );
+            else
+                Abc_Print( 1, "Networks are UNDECIDED.  " );
+            Gia_ManStopP( &pNew );
+            Gia_ManStopP( &pGia );
+        }
     }
     else
     {
@@ -2284,7 +2330,7 @@ void Wln_SolveEqual( Rtl_Lib_t * p, int iNtk1, int iNtk2 )
 }
 int Gia_ManFindFirst( Rtl_Ntk_t * p, int * pnOuts )
 {
-    int i, * pWire, iFirst = -1, Counts[4] = {0}, nBits = 0;
+    int i, * pWire, Counts[4] = {0}, nBits = 0;
     assert( p->nOutputs == 1 );
     Rtl_NtkForEachWire( p, pWire, i )
     {
@@ -2316,9 +2362,49 @@ Gia_Man_t * Gia_ManMoveSharedFirst( Gia_Man_t * pGia, int iFirst, int nBits )
             if ( n == (i >= iFirst && i < iFirst + nBits) )
                 Vec_IntPush( vPiPerm, i );
     pTemp = Gia_ManDupPerm( pGia, vPiPerm );
+    if ( pGia->vBarBufs )
+        pTemp->vBarBufs = Vec_IntDup( pGia->vBarBufs );
     Vec_IntFree( vPiPerm );
     return pTemp;
 }
+Vec_Int_t * Gia_ManCollectBufs( Gia_Man_t * p, int iFirst, int nBufs )
+{
+    Vec_Int_t * vRes = Vec_IntAlloc( 100 );
+    Gia_Obj_t * pObj; int i, iBuf = 0;
+    assert( iFirst >= 0 && iFirst + nBufs < p->nBufs );
+    Gia_ManForEachAnd( p, pObj, i )
+    {
+        if ( Gia_ObjIsBuf(pObj) && iBuf >= iFirst && iBuf < iFirst + nBufs )
+            Vec_IntPush( vRes, i );
+        iBuf += Gia_ObjIsBuf(pObj);
+    }
+    assert( iBuf == p->nBufs );
+    return vRes;
+}
+Gia_Man_t * Gia_ManReduceBuffers( Rtl_Lib_t * pLib, Gia_Man_t * p )
+{
+    Gia_Man_t * pNew;
+    Vec_Int_t * vMap = Vec_IntStartFull( Gia_ManObjNum(p) );
+    Vec_Int_t * vOne = Gia_ManCollectBufs( p, 0,       64 );
+    Vec_Int_t * vTwo = Gia_ManCollectBufs( p, 1280-64, 64 );
+    //Vec_Int_t * vOne = Gia_ManCollectBufs( p, 0,      1280/2 );
+    //Vec_Int_t * vTwo = Gia_ManCollectBufs( p, 1280/2, 1280/2 );
+    int i, One, Two;
+    printf( "Reducing %d buffers... Size(vOne) = %d. Size(vTwo) = %d. \n", p->nBufs, Vec_IntSize(vOne), Vec_IntSize(vTwo) );
+    assert( p->nBufs == 1280 );
+    Vec_IntForEachEntryTwo( vOne, vTwo, One, Two, i )
+        Vec_IntWriteEntry( vMap, Two, One );
+    Vec_IntFree( vOne );
+    Vec_IntFree( vTwo );
+Gia_ManPrintStats( p, NULL );
+    //pNew = Gia_ManDupNoBuf( p );
+    pNew = Gia_ManDupMap( p, vMap );
+Gia_ManPrintStats( pNew, NULL );
+    Vec_IntFree( vMap );
+    //Rtl_NtkPrintBufs( pNtk1, pGia->vBarBufs );
+    //printf( "Found %d buffers.\n", p->nBufs );
+    return pNew;
+}
 void Wln_SolveInverse( Rtl_Lib_t * p, int iNtk1, int iNtk2 )
 {
     abctime clk = Abc_Clock(); 
@@ -2331,14 +2417,26 @@ void Wln_SolveInverse( Rtl_Lib_t * p, int iNtk1, int iNtk2 )
     Gia_Man_t * pGia2 = Gia_ManMoveSharedFirst( pNtk2->pGia, iFirst2, nOuts2 );
     if ( 1 )
     {
+        char * pFileName  = "inv_miter.aig";
         Gia_Man_t * pGia  = Gia_ManMiterInverse( pGia1, pGia2, 0, 0 );
-        Gia_Man_t * pNew  = Cec4_ManSimulateTest3( pGia, 10000000, 0 );
-        //printf( "Miter %d -> %d\n",  Gia_ManAndNum(pGia),  Gia_ManAndNum(pNew) );
-        if ( Gia_ManAndNum(pNew) == 0 )
-            Abc_Print( 1, "Networks are equivalent.  " );
+        //Gia_Man_t * pGia2 = Gia_ManReduceBuffers( p, pGia );
+        Gia_Man_t * pGia2 = Gia_ManDupNoBuf( pGia );
+        printf( "Dumping inverse miter into file \"%s\".\n", pFileName );
+        Gia_AigerWrite( pGia2, pFileName, 0, 0, 0 );
+        if ( Abc_NtkFromGiaCollapse( pGia2 ) )
+            Abc_Print( 1, "Networks are equivalent after collapsing.  " );
         else
-            Abc_Print( 1, "Networks are UNDECIDED.  " );
-        Gia_ManStopP( &pNew );
+        {
+            Gia_Man_t * pNew  = Cec4_ManSimulateTest3( pGia2, 10000000, 0 );
+            Rtl_NtkPrintBufs( pNtk1, pGia->vBarBufs );
+            //printf( "Miter %d -> %d\n",  Gia_ManAndNum(pGia),  Gia_ManAndNum(pNew) );
+            if ( Gia_ManAndNum(pNew) == 0 )
+                Abc_Print( 1, "Networks are equivalent.  " );
+            else
+                Abc_Print( 1, "Networks are UNDECIDED.  " );
+            Gia_ManStopP( &pNew );
+        }
+        Gia_ManStopP( &pGia2 );
         Gia_ManStopP( &pGia );
     }
     else
@@ -2358,6 +2456,7 @@ void Wln_SolveProperty( Rtl_Lib_t * p, int iNtk )
 {
     Rtl_Ntk_t * pNtk = Rtl_LibNtk( p, iNtk );
     printf( "\nProving property \"%s\".\n", Rtl_NtkName(pNtk) );
+    Rtl_NtkPrintBufs( pNtk, pNtk->pGia->vBarBufs );
     Rtl_LibSolve( p, pNtk );
 }
 Vec_Int_t * Wln_ReadNtkRoots( Rtl_Lib_t * p, Vec_Wec_t * vGuide ) 
@@ -2390,13 +2489,16 @@ void Wln_SolveWithGuidance( char * pFileName, Rtl_Lib_t * p )
 {
     extern Vec_Wec_t * Wln_ReadGuidance( char * pFileName, Abc_Nam_t * p );
     Vec_Wec_t * vGuide = Wln_ReadGuidance( pFileName, p->pManName );
-    Vec_Int_t * vRoots, * vLevel; int i, iNtk1, iNtk2;
+    Vec_Int_t * vRoots, * vLevel; int i, iNtk1, iNtk2, fInv = 0;
+    Vec_WecForEachLevel( vGuide, vLevel, i )
+        if ( Vec_IntEntry( vLevel, 1 ) == Rtl_LibStrId(p, "inverse") )
+            fInv = 1;
     Vec_IntFillExtra( p->vMap, Abc_NamObjNumMax(p->pManName), -1 );
     Rtl_LibSetReplace( p, vGuide );
     Rtl_LibUpdateBoxes( p );
     Rtl_LibReorderModules( p );
     vRoots = Wln_ReadNtkRoots( p, vGuide );
-    Rtl_LibBlast2( p, vRoots );
+    Rtl_LibBlast2( p, vRoots, fInv );
     Vec_WecForEachLevel( vGuide, vLevel, i )
     {
         int Prove = Vec_IntEntry( vLevel, 0 );