Various changes.

13 files changed, 127 insertions, 47 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index af5c82b8..c0a49004 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -609,6 +609,7 @@ static inline void         Gia_ObjSetTravIdPrevious( Gia_Man_t * p, Gia_Obj_t *
 static inline int          Gia_ObjIsTravIdCurrent( Gia_Man_t * p, Gia_Obj_t * pObj )          { assert( Gia_ObjId(p, pObj) < p->nTravIdsAlloc ); return (p->pTravIds[Gia_ObjId(p, pObj)] == p->nTravIds);          }
 static inline int          Gia_ObjIsTravIdPrevious( Gia_Man_t * p, Gia_Obj_t * pObj )         { assert( Gia_ObjId(p, pObj) < p->nTravIdsAlloc ); return (p->pTravIds[Gia_ObjId(p, pObj)] == p->nTravIds - 1);      }
 static inline void         Gia_ObjSetTravIdCurrentId( Gia_Man_t * p, int Id )                 { assert( Id < p->nTravIdsAlloc ); p->pTravIds[Id] = p->nTravIds;                     }
+static inline void         Gia_ObjSetTravIdPreviousId( Gia_Man_t * p, int Id )                { assert( Id < p->nTravIdsAlloc ); p->pTravIds[Id] = p->nTravIds - 1;                 }
 static inline int          Gia_ObjIsTravIdCurrentId( Gia_Man_t * p, int Id )                  { assert( Id < p->nTravIdsAlloc ); return (p->pTravIds[Id] == p->nTravIds);           }
 static inline int          Gia_ObjIsTravIdPreviousId( Gia_Man_t * p, int Id )                 { assert( Id < p->nTravIdsAlloc ); return (p->pTravIds[Id] == p->nTravIds - 1);       }
 
@@ -1509,7 +1510,7 @@ extern void                Gia_ManWriteMiniLut( Gia_Man_t * pGia, char * pFileNa
 extern void                Gia_ManCountMuxXor( Gia_Man_t * p, int * pnMuxes, int * pnXors );
 extern void                Gia_ManPrintMuxStats( Gia_Man_t * p );
 extern Gia_Man_t *         Gia_ManDupMuxes( Gia_Man_t * p, int Limit );
-extern Gia_Man_t *         Gia_ManDupNoMuxes( Gia_Man_t * p );
+extern Gia_Man_t *         Gia_ManDupNoMuxes( Gia_Man_t * p, int fSkipBufs );
 /*=== giaPat.c ===========================================================*/
 extern void                Gia_SatVerifyPattern( Gia_Man_t * p, Gia_Obj_t * pRoot, Vec_Int_t * vCex, Vec_Int_t * vVisit );
 /*=== giaRetime.c ===========================================================*/
diff --git a/src/aig/gia/giaBalAig.c b/src/aig/gia/giaBalAig.c
index a3a0719e..5603b410 100644
--- a/src/aig/gia/giaBalAig.c
+++ b/src/aig/gia/giaBalAig.c
@@ -449,7 +449,7 @@ Gia_Man_t * Gia_ManBalance( Gia_Man_t * p, int fSimpleAnd, int fStrict, int fVer
     Gia_ManTransferTiming( pNew1, pNew );
     if ( fVerbose )      Gia_ManPrintStats( pNew1, NULL );
     Gia_ManStop( pNew );
-    pNew2 = Gia_ManDupNoMuxes( pNew1 );
+    pNew2 = Gia_ManDupNoMuxes( pNew1, 0 );
     Gia_ManTransferTiming( pNew2, pNew1 );
     if ( fVerbose )      Gia_ManPrintStats( pNew2, NULL );
     Gia_ManStop( pNew1 );
@@ -1083,7 +1083,7 @@ Gia_Man_t * Gia_ManAreaBalance( Gia_Man_t * p, int fSimpleAnd, int nNewNodesMax,
     Gia_ManStop( pNew );
     Vec_IntFreeP( &vCiLevels );
     // derive the final result
-    pNew2 = Gia_ManDupNoMuxes( pNew1 );
+    pNew2 = Gia_ManDupNoMuxes( pNew1, 0 );
     Gia_ManTransferTiming( pNew2, pNew1 );
     if ( fVerbose )     Gia_ManPrintStats( pNew2, NULL );
     Gia_ManStop( pNew1 );
diff --git a/src/aig/gia/giaBalLut.c b/src/aig/gia/giaBalLut.c
index 4402e36f..c90910c9 100644
--- a/src/aig/gia/giaBalLut.c
+++ b/src/aig/gia/giaBalLut.c
@@ -965,7 +965,7 @@ Gia_Man_t * Gia_ManBalanceLut( Gia_Man_t * p, int nLutSize, int nCutNum, int fVe
     pNew1 = Gia_ManBalanceInt( pNew, nLutSize, nCutNum, fVerbose );
     if ( fVerbose )      Gia_ManPrintStats( pNew1, NULL );
     Gia_ManStop( pNew );
-    pNew2 = Gia_ManDupNoMuxes( pNew1 );
+    pNew2 = Gia_ManDupNoMuxes( pNew1, 0 );
     if ( fVerbose )      Gia_ManPrintStats( pNew2, NULL );
     Gia_ManStop( pNew1 );
     return pNew2;
diff --git a/src/aig/gia/giaFanout.c b/src/aig/gia/giaFanout.c
index 6a940354..44e79ba2 100644
--- a/src/aig/gia/giaFanout.c
+++ b/src/aig/gia/giaFanout.c
@@ -214,7 +214,7 @@ Vec_Int_t * Gia_ManStartFanoutMap( Gia_Man_t * p, Vec_Int_t * vFanoutNums )
     Gia_Obj_t * pObj;
     int i, iOffset;
     iOffset  = Gia_ManObjNum(p);
-    vEdgeMap = Vec_IntStart( iOffset + Gia_ManMuxNum(p) + 2 * Gia_ManAndNum(p) + Gia_ManCoNum(p) );
+    vEdgeMap = Vec_IntStart( iOffset + Gia_ManMuxNum(p) + 2 * Gia_ManAndNum(p) + Gia_ManCoNum(p) - Gia_ManBufNum(p) );
     Gia_ManForEachObj( p, pObj, i )
     {
         Vec_IntWriteEntry( vEdgeMap, i, iOffset );
@@ -261,9 +261,8 @@ void Gia_ManStaticFanoutStart( Gia_Man_t * p )
             Gia_ObjSetFanout( p, pFanin, iFanout, pObj );
             Vec_IntAddToEntry( vCounts, Gia_ObjId(p, pFanin), 1 );
         }
-        if ( Gia_ObjIsAnd(pObj) )
+        if ( Gia_ObjIsAnd(pObj) && !Gia_ObjIsBuf(pObj) )
         {
-
             pFanin = Gia_ObjFanin1(pObj);
             iFanout = Vec_IntEntry( vCounts, Gia_ObjId(p, pFanin) );
             Gia_ObjSetFanout( p, pFanin, iFanout, pObj );
diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c
index 447ecea9..adb7abc0 100644
--- a/src/aig/gia/giaMan.c
+++ b/src/aig/gia/giaMan.c
@@ -556,6 +556,8 @@ void Gia_ManPrintStats( Gia_Man_t * p, Gps_Par_t * pPars )
         Abc_Print( 1, "  bb = %d", Gia_ManBlackBoxNum(p) );
     if ( Gia_ManBufNum(p) )
         Abc_Print( 1, "  buf = %d", Gia_ManBufNum(p) );
+    if ( Gia_ManXorNum(p) && p->pMuxes == NULL )
+        Abc_Print( 1, "  xor = %d", Gia_ManXorNum(p) );
     if ( pPars && pPars->fMuxXor )
         printf( "\nXOR/MUX " ), Gia_ManPrintMuxStats( p );
     if ( pPars && pPars->fSwitch )
diff --git a/src/aig/gia/giaMuxes.c b/src/aig/gia/giaMuxes.c
index 5182336f..932029cc 100644
--- a/src/aig/gia/giaMuxes.c
+++ b/src/aig/gia/giaMuxes.c
@@ -157,7 +157,7 @@ Gia_Man_t * Gia_ManDupMuxes( Gia_Man_t * p, int Limit )
   SeeAlso     []
 
 ***********************************************************************/
-Gia_Man_t * Gia_ManDupNoMuxes( Gia_Man_t * p )
+Gia_Man_t * Gia_ManDupNoMuxes( Gia_Man_t * p, int fSkipBufs )
 {
     Gia_Man_t * pNew, * pTemp;
     Gia_Obj_t * pObj;
@@ -176,7 +176,7 @@ Gia_Man_t * Gia_ManDupNoMuxes( Gia_Man_t * p )
         else if ( Gia_ObjIsCo(pObj) )
             pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
         else if ( Gia_ObjIsBuf(pObj) )
-            pObj->Value = Gia_ManAppendBuf( pNew, Gia_ObjFanin0Copy(pObj) );
+            pObj->Value = fSkipBufs ? Gia_ObjFanin0Copy(pObj) : Gia_ManAppendBuf( pNew, Gia_ObjFanin0Copy(pObj) );
         else if ( Gia_ObjIsMuxId(p, i) )
             pObj->Value = Gia_ManHashMux( pNew, Gia_ObjFanin2Copy(p, pObj), Gia_ObjFanin1Copy(pObj), Gia_ObjFanin0Copy(pObj) );
         else if ( Gia_ObjIsXor(pObj) )
@@ -207,7 +207,7 @@ Gia_Man_t * Gia_ManDupMuxesTest( Gia_Man_t * p )
 {
     Gia_Man_t * pNew, * pNew2;
     pNew = Gia_ManDupMuxes( p, 2 );
-    pNew2 = Gia_ManDupNoMuxes( pNew );
+    pNew2 = Gia_ManDupNoMuxes( pNew, 0 );
     Gia_ManPrintStats( p, NULL );
     Gia_ManPrintStats( pNew, NULL );
     Gia_ManPrintStats( pNew2, NULL );
@@ -287,7 +287,7 @@ Gia_Man_t * Gia_ManDupMuxRestructure( Gia_Man_t * p )
 {
     Gia_Man_t * pTemp, * pNew = Gia_ManDupMuxes( p, 2 );
     pNew = Gia_ManMuxRestructure( pTemp = pNew );  Gia_ManStop( pTemp );
-    pNew = Gia_ManDupNoMuxes( pTemp = pNew );      Gia_ManStop( pTemp );
+    pNew = Gia_ManDupNoMuxes( pTemp = pNew, 0 );   Gia_ManStop( pTemp );
     return pNew;
 }
 
diff --git a/src/aig/gia/giaSimBase.c b/src/aig/gia/giaSimBase.c
index 825c01ca..64bacc28 100644
--- a/src/aig/gia/giaSimBase.c
+++ b/src/aig/gia/giaSimBase.c
@@ -54,6 +54,7 @@ struct Gia_SimAbsMan_t_
     int            nWords;     // word count
     Vec_Wrd_t *    vSims;      // candidate simulation info
     Vec_Int_t *    vResub;     // the result
+    int            fVerbose;   // verbose
     // intermediate result
     Vec_Int_t *    vValues;       // function values in each pattern
     Vec_Int_t *    vPatPairs;     // used minterms
@@ -181,8 +182,8 @@ Vec_Wrd_t * Gia_ManSimCombine( int nInputs, Vec_Wrd_t * vBase, Vec_Wrd_t * vAddO
     assert( nWordsUse <= nWordsAddOn );
     for ( i = 0; i < nInputs; i++ )
     {
-        word * pSimsB = Vec_WrdEntryP( vBase,  i * nWordsBase );
-        word * pSimsA = Vec_WrdEntryP( vAddOn, i * nWordsAddOn );
+        word * pSimsB = nWordsBase  ? Vec_WrdEntryP( vBase,  i * nWordsBase )  : NULL;
+        word * pSimsA = nWordsAddOn ? Vec_WrdEntryP( vAddOn, i * nWordsAddOn ) : NULL;
         for ( w = 0; w < nWordsBase; w++ )
             Vec_WrdPush( vSimsIn, pSimsB[w] );
         for ( w = 0; w < nWordsUse; w++ )
@@ -769,14 +770,20 @@ int Gia_ManSimRelCompare( Gia_Man_t * p, int nWords, Vec_Wrd_t * vSims, int nWor
 }
 void Gia_ManSimRelCollectOutputs( Gia_Man_t * p, int nWords, Vec_Wrd_t * vSims, int nWordsOut, Vec_Wrd_t * vSimsOut, Vec_Wrd_t * vRel )
 {
-    int i, m, nMints = nWords / nWordsOut;
+    int i, m, nMints = nWords / nWordsOut, Count = 0;
     assert( Vec_WrdSize(vSims)    == nWords   * Gia_ManObjNum(p) );
     assert( Vec_WrdSize(vSimsOut) == nWordsOut * Gia_ManCoNum(p) );
     assert( Vec_WrdSize(vRel)     == nWordsOut * nMints );
     for ( i = 0; i < 64 * nWordsOut; i++ )
+    {
+        int CountMints = 0;
         for ( m = 0; m < nMints; m++ )
             if ( Gia_ManSimRelCompare(p, nWords, vSims, nWordsOut, vSimsOut, i, m) )
-                Abc_TtSetBit( Vec_WrdArray(vRel), i*nMints+m );
+                Abc_TtSetBit( Vec_WrdArray(vRel), i*nMints+m ), CountMints++;
+        Count += CountMints == 0;
+    }
+    if ( Count )
+        printf( "The relation is not well-defined for %d (out of %d) patterns.\n", Count, 64 * nWordsOut );
 }
 Vec_Wrd_t * Gia_ManSimRel( Gia_Man_t * p, Vec_Int_t * vObjs, Vec_Wrd_t * vVals )
 {
@@ -819,38 +826,86 @@ Vec_Wrd_t * Gia_ManSimRel( Gia_Man_t * p, Vec_Int_t * vObjs, Vec_Wrd_t * vVals )
   SeeAlso     []
 
 ***********************************************************************/
+void Gia_ManSimRelCheckFuncs( Gia_Man_t * p, Vec_Wrd_t * vRel, int nOuts, Vec_Wrd_t * vFuncs )
+{
+    int i, k, m, Values[32], nErrors = 0, nMints = 1 << nOuts, nWords = Vec_WrdSize(vRel) / nMints;
+    assert( Vec_WrdSize(vFuncs) == 2 * nOuts * nWords );
+    assert( nOuts <= 32 );
+    for ( i = 0; i < 64 * nWords; i++ )
+    {
+        for ( k = 0; k < nOuts; k++ )
+        {
+            int Value0 = Abc_TtGetBit( Vec_WrdEntryP(vFuncs, (2*k+0)*nWords), i );
+            int Value1 = Abc_TtGetBit( Vec_WrdEntryP(vFuncs, (2*k+1)*nWords), i );
+            if ( Value0 && !Value1 )
+                Values[k] = 1;
+            else if ( !Value0 && Value1 )
+                Values[k] = 2;
+            else if ( !Value0 && !Value1 )
+                Values[k] = 3;
+            else assert( 0 );
+        }
+        for ( m = 0; m < nMints; m++ )
+        {
+            for ( k = 0; k < nOuts; k++ )
+                if ( ((Values[k] >> ((m >> k) & 1)) & 1) == 0 )
+                    break;
+            if ( k < nOuts )
+                continue;
+            if ( Abc_TtGetBit( Vec_WrdArray(vRel), i*nMints+m ) )
+                continue;
+            if ( nErrors++ == 0 )
+                printf( "For pattern %d, minterm %d produced by function is not in the relation.\n", i, m );
+        }
+    }
+    if ( nErrors )    
+        printf( "Total number of similar errors = %d.\n", nErrors );
+    else
+        printf( "The function agrees with the relation.\n" );
+}
 Vec_Wrd_t * Gia_ManSimRelDeriveFuncs( Gia_Man_t * p, Vec_Wrd_t * vRel, int nOuts )
 {
-    int i, k, m, nMints = 1 << nOuts, nWords = Vec_WrdSize(vRel) / nMints;
-    Vec_Wrd_t * vFuncs = Vec_WrdStart( nOuts * nWords );
+    int i, k, m, Count = 0, nMints = 1 << nOuts, nWords = Vec_WrdSize(vRel) / nMints;
+    Vec_Wrd_t * vFuncs = Vec_WrdStart( 2 * nOuts * nWords );
     assert( Vec_WrdSize(vRel) % nMints == 0 );
     for ( i = 0; i < 64 * nWords; i++ )
     {
         for ( m = 0; m < nMints; m++ )
             if ( Abc_TtGetBit( Vec_WrdArray(vRel), i*nMints+m ) )
                 break;
-        assert( m < nMints );
+        Count += m == nMints;
         for ( k = 0; k < nOuts; k++ )
             if ( (m >> k) & 1 )
-                Abc_TtSetBit( Vec_WrdEntryP(vFuncs, k*nWords), i );
+                Abc_TtSetBit( Vec_WrdEntryP(vFuncs, (2*k+1)*nWords), i );
+            else
+                Abc_TtSetBit( Vec_WrdEntryP(vFuncs, (2*k+0)*nWords), i );
     }
+    if ( Count )
+        printf( "The relation is not well-defined for %d (out of %d) patterns.\n", Count, 64 * nWords );
+    else
+        printf( "The relation was successfully determized without don't-cares for %d patterns.\n", 64 * nWords );
+    Gia_ManSimRelCheckFuncs( p, vRel, nOuts, vFuncs );
     return vFuncs;
 }
 Vec_Wrd_t * Gia_ManSimRelDeriveFuncs2( Gia_Man_t * p, Vec_Wrd_t * vRel, int nOuts )
 {
-    int i, k, m, nMints = 1 << nOuts, nWords = Vec_WrdSize(vRel) / nMints;
+    int i, k, m, nDCs[32] = {0}, Count = 0, nMints = 1 << nOuts, nWords = Vec_WrdSize(vRel) / nMints;
     Vec_Wrd_t * vFuncs = Vec_WrdStart( 2 * nOuts * nWords );
     assert( Vec_WrdSize(vRel) % nMints == 0 );
+    assert( nOuts <= 32 );
     for ( i = 0; i < 64 * nWords; i++ )
     {
         for ( m = 0; m < nMints; m++ )
             if ( Abc_TtGetBit( Vec_WrdArray(vRel), i*nMints+m ) )
                 break;
-        assert( m < nMints );
+        Count += m == nMints;
         for ( k = 0; k < nOuts; k++ )
         {
             if ( Abc_TtGetBit( Vec_WrdArray(vRel), i*nMints+(m^(1<<k)) ) )
+            {
+                nDCs[k]++;
                 continue;
+            }
             if ( (m >> k) & 1 )
                 Abc_TtSetBit( Vec_WrdEntryP(vFuncs, (2*k+1)*nWords), i );
             else
@@ -873,6 +928,17 @@ Vec_Wrd_t * Gia_ManSimRelDeriveFuncs2( Gia_Man_t * p, Vec_Wrd_t * vRel, int nOut
             printf( "\n" );
         }
     }
+    if ( Count )
+        printf( "The relation is not well-defined for %d (out of %d) patterns.\n", Count, 64 * nWords );
+    else
+    {
+        printf( "The relation was successfully determized with don't-cares for %d patterns.\n", 64 * nWords );
+        printf( "Don't-cares in each output:" );
+        for ( k = 0; k < nOuts; k++ )
+            printf( "   %d = %d", k, nDCs[k] );
+        printf( "\n" );
+    }
+    Gia_ManSimRelCheckFuncs( p, vRel, nOuts, vFuncs );
     return vFuncs;
 }
 
@@ -986,7 +1052,7 @@ Vec_Int_t * Gia_Sim5CollectValues( word * pOffSet, word * pOnSet, int nWords )
     //printf( "Offset = %d.  Onset = %d.  Dcset = %d.\n", Count[0], Count[1], 64*nWords - Count[0] - Count[1] );
     return vBits;
 }
-Gia_SimAbsMan_t * Gia_SimAbsAlloc( Gia_Man_t * pGia, word * pOffSet, word * pOnSet, Vec_Wrd_t * vSims, int nWords, Vec_Int_t * vResub )
+Gia_SimAbsMan_t * Gia_SimAbsAlloc( Gia_Man_t * pGia, word * pOffSet, word * pOnSet, Vec_Wrd_t * vSims, int nWords, Vec_Int_t * vResub, int fVerbose )
 {
     Gia_SimAbsMan_t * p = ABC_CALLOC( Gia_SimAbsMan_t, 1 );
     p->pGia      = pGia;
@@ -996,6 +1062,7 @@ Gia_SimAbsMan_t * Gia_SimAbsAlloc( Gia_Man_t * pGia, word * pOffSet, word * pOnS
     p->nWords    = nWords;
     p->vSims     = vSims;
     p->vResub    = vResub;
+    p->fVerbose  = fVerbose;
     p->vValues      = Gia_Sim5CollectValues( pOffSet, pOnSet, nWords );
     p->vPatPairs    = Vec_IntAlloc( 100 );
     p->vCoverTable  = Vec_WrdAlloc( 10000 );
@@ -1158,13 +1225,16 @@ void Gia_SimAbsSolve( Gia_SimAbsMan_t * p )
         pSimTable = Vec_WrdEntryP( p->vCoverTable, p->nWordsTable * iArgMax );
         Abc_TtSharp( p->pTableTemp, p->pTableTemp, pSimTable, p->nWordsTable );
     }
-    printf( "Solution %2d for covering problem [%5d x %5d]: ", Vec_IntSize(p->vResub), Vec_IntSize(p->vPatPairs)/2, p->nCands );
-    Vec_IntForEachEntry( p->vResub, iPat, i )
-        printf( "%6d ", iPat );
-    for ( ; i < 12; i++ )
-        printf( "       " );
-    printf( "   " );
-    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+    if ( p->fVerbose )
+    {
+        printf( "Solution %2d for covering problem [%5d x %5d]: ", Vec_IntSize(p->vResub), Vec_IntSize(p->vPatPairs)/2, p->nCands );
+        Vec_IntForEachEntry( p->vResub, iPat, i )
+            printf( "%6d ", iPat );
+        for ( ; i < 12; i++ )
+            printf( "       " );
+        printf( "   " );
+        Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+    }
 }
 int Gia_SimAbsRefine( Gia_SimAbsMan_t * p )
 {
@@ -1196,7 +1266,10 @@ int Gia_SimAbsRefine( Gia_SimAbsMan_t * p )
         //printf( "iPat1 = %d  iPat2 = %d   Mint = %d\n", Value ? iPat : i, Value ? i : iPat, iMint );
         Count++;
         if ( Count == 64 )
+        {
+            ABC_FREE( pFanins );
             return 1;
+        }
     }
     //printf( "Refinement added %d minterm pairs.\n", Count );
     ABC_FREE( pFanins );
@@ -1216,7 +1289,8 @@ void Gia_SimAbsInit( Gia_SimAbsMan_t * p )
     Vec_Int_t * vValue0 = Gia_SimAbsFind( p->vValues, 0 );
     Vec_Int_t * vValue1 = Gia_SimAbsFind( p->vValues, 1 );
     Vec_IntClear( p->vPatPairs );
-    printf( "There are %d offset and %d onset minterms (%d pairs).\n", Vec_IntSize(vValue0), Vec_IntSize(vValue1), Vec_IntSize(vValue0)*Vec_IntSize(vValue1) );
+    printf( "There are %d offset and %d onset minterms (%d pairs) and %d divisors.\n", 
+        Vec_IntSize(vValue0), Vec_IntSize(vValue1), Vec_IntSize(vValue0)*Vec_IntSize(vValue1), p->nCands );
     Abc_Random( 1 );
     assert( Vec_IntSize(vValue0) > 0 );
     assert( Vec_IntSize(vValue1) > 0 );
@@ -1239,10 +1313,11 @@ void Gia_SimAbsInit( Gia_SimAbsMan_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Int_t * Gia_SimAbsPerformOne( Gia_Man_t * pGia, word * pOffSet, word * pOnSet, Vec_Wrd_t * vSimsCands, int nWords )
+Vec_Int_t * Gia_SimAbsPerformOne( Gia_Man_t * pGia, word * pOffSet, word * pOnSet, Vec_Wrd_t * vSimsCands, int nWords, int fVerbose )
 {
+    abctime clk = Abc_Clock();
     Vec_Int_t * vResub  = Vec_IntAlloc( 10 );
-    Gia_SimAbsMan_t * p = Gia_SimAbsAlloc( pGia, pOffSet, pOnSet, vSimsCands, nWords, vResub );
+    Gia_SimAbsMan_t * p = Gia_SimAbsAlloc( pGia, pOffSet, pOnSet, vSimsCands, nWords, vResub, fVerbose );
     Gia_SimAbsInit( p );
     while ( 1 )
     {
@@ -1251,11 +1326,10 @@ Vec_Int_t * Gia_SimAbsPerformOne( Gia_Man_t * pGia, word * pOffSet, word * pOnSe
             break;
     }
     Gia_SimAbsFree( p );
+    Abc_PrintTime( 1, "Resubstitution time", Abc_Clock() - clk );
     return vResub;
 }
 
-
-
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/gia/giaStr.c b/src/aig/gia/giaStr.c
index 68d478b8..085738c3 100644
--- a/src/aig/gia/giaStr.c
+++ b/src/aig/gia/giaStr.c
@@ -1357,7 +1357,7 @@ Gia_Man_t * Str_NtkBalance( Gia_Man_t * pGia, Str_Ntk_t * p, int nLutSize, int f
     ABC_FREE( pNew->vCopies.pArray );
     Gia_ManHashStop( pNew );
     Gia_ManSetRegNum( pNew, Gia_ManRegNum(pGia) );
-    pNew = Gia_ManDupNoMuxes( pTemp = pNew );
+    pNew = Gia_ManDupNoMuxes( pTemp = pNew, 0 );
     Gia_ManStop( pTemp );
 //    if ( pGia->pManTime != NULL )
 //        pNew->pManTime = Tim_ManDup( (Tim_Man_t *)pGia->pManTime, 0 );
diff --git a/src/aig/gia/giaUtil.c b/src/aig/gia/giaUtil.c
index 072c9872..d0ec969f 100644
--- a/src/aig/gia/giaUtil.c
+++ b/src/aig/gia/giaUtil.c
@@ -694,7 +694,8 @@ void Gia_ManCreateValueRefs( Gia_Man_t * p )
         if ( Gia_ObjIsAnd(pObj) )
         {
             Gia_ObjFanin0(pObj)->Value++;
-            Gia_ObjFanin1(pObj)->Value++;
+            if ( !Gia_ObjIsBuf(pObj) )
+                Gia_ObjFanin1(pObj)->Value++;
         }
         else if ( Gia_ObjIsCo(pObj) )
             Gia_ObjFanin0(pObj)->Value++;
@@ -723,7 +724,8 @@ void Gia_ManCreateRefs( Gia_Man_t * p )
         if ( Gia_ObjIsAnd(pObj) )
         {
             Gia_ObjRefFanin0Inc( p, pObj );
-            Gia_ObjRefFanin1Inc( p, pObj );
+            if ( !Gia_ObjIsBuf(pObj) )
+                Gia_ObjRefFanin1Inc( p, pObj );
             if ( Gia_ObjIsMuxId(p, i) )
                 Gia_ObjRefFanin2Inc( p, pObj );
         }
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index ed4de2e4..61f7f06b 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -31891,7 +31891,7 @@ int Abc_CommandAbc9Strash( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     else if ( pAbc->pGia->pMuxes )
     {
-        pTemp = Gia_ManDupNoMuxes( pAbc->pGia );
+        pTemp = Gia_ManDupNoMuxes( pAbc->pGia, 0 );
         if ( !Abc_FrameReadFlag("silentmode") )
             printf( "Generated AIG from AND/XOR/MUX graph.\n" );
     }
diff --git a/src/base/acb/acbFunc.c b/src/base/acb/acbFunc.c
index f063f7fb..e7fe2f53 100644
--- a/src/base/acb/acbFunc.c
+++ b/src/base/acb/acbFunc.c
@@ -245,7 +245,7 @@ void * Acb_VerilogSimpleParse( Vec_Int_t * vBuffer, Abc_Nam_t * pNames )
             vCur = vWires;
         else if ( Token >= ACB_BUF && Token <= ACB_XNOR )
         {
-            char * pToken = Abc_NamStr(pNames, Vec_IntEntry(vBuffer, i+1));
+            //char * pToken = Abc_NamStr(pNames, Vec_IntEntry(vBuffer, i+1));
             Vec_IntPush( vTypes, Token );
             Vec_IntPush( vTypes, Vec_IntSize(vFanins) );
             vCur = vFanins;
@@ -1976,7 +1976,7 @@ Vec_Str_t * Acb_GenerateInstance2( Vec_Ptr_t * vIns, Vec_Ptr_t * vOuts )
     Vec_Str_t * vStr = Vec_StrAlloc( 100 );
     Vec_StrAppend( vStr, "  patch p0 (" );
     Vec_PtrForEachEntry( char *, vOuts, pName, i )
-        Vec_StrPrintF( vStr, "%s .%s(target_%s)", i ? ",":"", pName, pName );
+        Vec_StrPrintF( vStr, "%s .%s(t%d_%s)", i ? ",":"", pName, i, pName );
     Vec_PtrForEachEntry( char *, vIns, pName, i )
         Vec_StrPrintF( vStr, ", .%s(%s)", pName, pName );
     Vec_StrAppend( vStr, " );\n\n" );
diff --git a/src/base/acb/acbUtil.c b/src/base/acb/acbUtil.c
index 6c409c45..39c97859 100644
--- a/src/base/acb/acbUtil.c
+++ b/src/base/acb/acbUtil.c
@@ -519,10 +519,12 @@ int Acb_ObjToGia2( Gia_Man_t * pNew, Acb_Ntk_t * p, int iObj, Vec_Int_t * vTemp,
         return 0;
     if ( Type == ABC_OPER_CONST_T ) 
         return 1;
-    if ( Type == ABC_OPER_BIT_BUF ) 
-        return Vec_IntEntry(vTemp, 0);
-    if ( Type == ABC_OPER_BIT_INV ) 
-        return Abc_LitNot( Vec_IntEntry(vTemp, 0) );
+    if ( Type == ABC_OPER_BIT_BUF || Type == ABC_OPER_BIT_INV ) 
+    {
+        Res = fUseXors ? Gia_ManAppendBuf(pNew, Vec_IntEntry(vTemp, 0)) : Vec_IntEntry(vTemp, 0);
+        //Res = Vec_IntEntry(vTemp, 0);
+        return Abc_LitNotCond( Res, Type == ABC_OPER_BIT_INV );
+    }
     if ( Type == ABC_OPER_BIT_AND || Type == ABC_OPER_BIT_NAND )
     {
         Res = 1;
@@ -886,7 +888,7 @@ void Acb_NtkInsert( char * pFileNameIn, char * pFileNameOut, Vec_Ptr_t * vNames,
     else
     {
         Vec_PtrForEachEntry( char *, vNames, pName, i )
-            fprintf( pFile, " target_%s%s", pName, i==Vec_PtrSize(vNames)-1 ? ";" : "," );
+            fprintf( pFile, " t%d_%s%s", i, pName, i==Vec_PtrSize(vNames)-1 ? ";" : "," );
     }
     fprintf( pFile, "\n\n" );
     if ( fNumber )
@@ -897,7 +899,7 @@ void Acb_NtkInsert( char * pFileNameIn, char * pFileNameOut, Vec_Ptr_t * vNames,
     else
     {
         Vec_PtrForEachEntry( char *, vNames, pName, i )
-            fprintf( pFile, "  buf( %s, target_%s );    // t_%d\n", pName, pName, i );
+            fprintf( pFile, "  buf( %s, t%d_%s );\n", pName, i, pName );
     }
     fprintf( pFile, "\n" );
     for ( k = Pos2; pBuffer[k]; k++ )
diff --git a/src/base/ver/verStream.c b/src/base/ver/verStream.c
index 134bb2f9..4dca9ef6 100644
--- a/src/base/ver/verStream.c
+++ b/src/base/ver/verStream.c
@@ -454,7 +454,7 @@ char * Ver_StreamGetWord( Ver_Stream_t * p, char * pCharsToStop )
 ***********************************************************************/
 void Ver_StreamMove( Ver_Stream_t * p )
 {
-    if ( !strncmp(p->pBufferCur+1, "z_g_", 4) )
+    if ( !strncmp(p->pBufferCur+1, "z_g_", 4) || !strncmp(p->pBufferCur+1, "co_g", 3) )
         while ( p->pBufferCur[0] != '(' )
             p->pBufferCur++;
 }