Experimental resubstitution.

src/aig/gia/gia.h

@@ -1704,6 +1704,7 @@ extern int                 Gia_ManCheckSuppOverlap( Gia_Man_t * p, int iNode1, i
 extern int                 Gia_ManCountPisWithFanout( Gia_Man_t * p );
 extern int                 Gia_ManCountPosWithNonZeroDrivers( Gia_Man_t * p );
 extern void                Gia_ManUpdateCopy( Vec_Int_t * vCopy, Gia_Man_t * p );
+extern Vec_Int_t *         Gia_ManComputeDistance( Gia_Man_t * p, int iObj, Vec_Int_t * vObjs, int fVerbose );
 
 /*=== giaCTas.c ===========================================================*/
 typedef struct Tas_Man_t_  Tas_Man_t;

src/aig/gia/giaSimBase.c

@@ -343,7 +343,7 @@ void Gia_ManSimPatWrite( char * pFileName, Vec_Wrd_t * vSimsIn, int nWords )
     for ( i = 0; i < nNodes; i++ )
         Gia_ManSimPatWriteOne( pFile, Vec_WrdEntryP(vSimsIn, i*nWords), nWords );
     fclose( pFile );
-    printf( "Written %d words of simulation data into file \"%s\".\n", nWords, pFileName );
+    printf( "Written %d words of simulation data for %d objects into file \"%s\".\n", nWords, Vec_WrdSize(vSimsIn)/nWords, pFileName );
 }
 int Gia_ManSimPatReadOne( char c )
 {
@@ -358,7 +358,7 @@ int Gia_ManSimPatReadOne( char c )
     assert( Digit >= 0 && Digit < 16 );
     return Digit;
 }
-Vec_Wrd_t * Gia_ManSimPatRead( char * pFileName )
+Vec_Wrd_t * Gia_ManSimPatRead( char * pFileName, int * pnWords )
 {
     Vec_Wrd_t * vSimsIn = NULL; 
     int c, nWords = -1, nChars = 0; word Num = 0;
@@ -384,7 +384,9 @@ Vec_Wrd_t * Gia_ManSimPatRead( char * pFileName )
     }
     assert( Vec_WrdSize(vSimsIn) % nWords == 0 );
     fclose( pFile );
-    printf( "Read %d words of simulation data.\n", nWords );
+    printf( "Read %d words of simulation data for %d objects.\n", nWords, Vec_WrdSize(vSimsIn)/nWords );
+    if ( pnWords )
+        *pnWords = nWords;
     return vSimsIn;
 }
 

src/aig/gia/giaUtil.c

@@ -2290,6 +2290,94 @@ Gia_Man_t * Gia_ManDupWithMuxPos( Gia_Man_t * p )
     return pNew;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Collect distance info.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManRingAdd( Gia_Man_t * p, int iObj, Vec_Int_t * vRes, Vec_Int_t * vDists, int Dist )
+{
+    if ( Gia_ObjIsTravIdCurrentId(p, iObj) )
+        return;
+    Gia_ObjSetTravIdCurrentId(p, iObj);
+    Vec_IntWriteEntry( vDists, iObj, Dist );
+    Vec_IntPush( vRes, iObj );
+}
+void Gia_ManCollectRing( Gia_Man_t * p, Vec_Int_t * vStart, Vec_Int_t * vRes, Vec_Int_t * vDists )
+{
+    int i, k, iObj, iFan;
+    Vec_IntForEachEntry( vStart, iObj, i )
+    {
+        int Weight = Vec_IntEntry( vDists, iObj );
+        Gia_Obj_t * pObj = Gia_ManObj(p, iObj);
+        assert( Weight > 0 );
+        if ( Gia_ObjIsAnd(pObj) )
+        {
+            Gia_ManRingAdd( p, Gia_ObjFaninId0(pObj, iObj), vRes, vDists, Weight + 1*!Gia_ObjIsBuf(Gia_ObjFanin0(pObj)) );
+            Gia_ManRingAdd( p, Gia_ObjFaninId1(pObj, iObj), vRes, vDists, Weight + 1*!Gia_ObjIsBuf(Gia_ObjFanin1(pObj)) );
+        }
+        Gia_ObjForEachFanoutStaticId( p, iObj, iFan, k )
+            Gia_ManRingAdd( p, iFan, vRes, vDists, Weight + 1*!Gia_ObjIsBuf(Gia_ManObj(p, iFan)) );
+    }
+}
+Vec_Int_t * Gia_ManComputeDistanceInt( Gia_Man_t * p, int iTarg, Vec_Int_t * vObjs, int fVerbose )
+{
+    int i, iObj;
+    Vec_Int_t * vDists, * vStart, * vNexts;
+    vStart = Vec_IntAlloc( 100 );
+    vNexts = Vec_IntAlloc( 100 );
+    vDists = Vec_IntStart( Gia_ManObjNum(p) );
+    Gia_ManIncrementTravId( p );
+    if ( vObjs )
+    {
+        Vec_IntForEachEntry( vObjs, iObj, i )
+        {
+            Gia_ObjSetTravIdCurrentId(p, iObj);
+            Vec_IntWriteEntry( vDists, iObj, 1 );
+            Vec_IntPush( vStart, iObj );
+        }
+    }
+    else
+    {
+        Gia_ObjSetTravIdCurrentId(p, iTarg);
+        Vec_IntWriteEntry( vDists, iTarg, 1 );
+        Vec_IntPush( vStart, iTarg );
+    }
+    for ( i = 0; ; i++ )
+    {
+        if ( fVerbose )
+            printf( "Ring %2d : %6d\n", i, Vec_IntSize(vDists)-Vec_IntCountZero(vDists) );        
+        Gia_ManCollectRing( p, vStart, vNexts, vDists );
+        if ( Vec_IntSize(vNexts) == 0 )
+            break;
+        Vec_IntClear( vStart );
+        ABC_SWAP( Vec_Int_t, *vStart, *vNexts );
+    }
+    Vec_IntFree( vStart );
+    Vec_IntFree( vNexts );
+    return vDists;
+}
+Vec_Int_t * Gia_ManComputeDistance( Gia_Man_t * p, int iObj, Vec_Int_t * vObjs, int fVerbose )
+{
+    Vec_Int_t * vDists;
+    if ( p->vFanoutNums )
+        vDists = Gia_ManComputeDistanceInt( p, iObj, vObjs, fVerbose );
+    else
+    {
+        Gia_ManStaticFanoutStart( p );
+        vDists = Gia_ManComputeDistanceInt( p, iObj, vObjs, fVerbose );
+        Gia_ManStaticFanoutStop( p );
+    }
+    return vDists;
+}
+
+
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///

src/base/abci/abc.c

@@ -437,6 +437,7 @@ static int Abc_CommandAbc9Shrink             ( Abc_Frame_t * pAbc, int argc, cha
 static int Abc_CommandAbc9Fx                 ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Balance            ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9BalanceLut         ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9Resub              ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Syn2               ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Syn3               ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Syn4               ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -1156,6 +1157,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "ABC9",         "&fx",           Abc_CommandAbc9Fx,           0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&b",            Abc_CommandAbc9Balance,      0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&blut",         Abc_CommandAbc9BalanceLut,   0 );
+    Cmd_CommandAdd( pAbc, "ABC9",         "&resub",        Abc_CommandAbc9Resub,        0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&syn2",         Abc_CommandAbc9Syn2,         0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&syn3",         Abc_CommandAbc9Syn3,         0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&syn4",         Abc_CommandAbc9Syn4,         0 );
@@ -34780,6 +34782,104 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandAbc9Resub( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    extern Gia_Man_t * Gia_ManResub1( char * pFileName, int nNodes, int nSupp, int nDivs, int fVerbose, int fVeryVerbose );
+    extern Gia_Man_t * Gia_ManResub2( Gia_Man_t * pGia, int nNodes, int nSupp, int nDivs, int fVerbose, int fVeryVerbose );
+    Gia_Man_t * pTemp;
+    int nNodes       =  0;
+    int nSupp        =  0;
+    int nDivs        =  0;
+    int c, fVerbose  =  0;
+    int fVeryVerbose =  0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "NSDvwh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'N':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( 1, "Command line switch \"-N\" should be followed by a floating point number.\n" );
+                return 0;
+            }
+            nNodes = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nNodes < 0 )
+                goto usage;
+            break;
+        case 'S':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( 1, "Command line switch \"-S\" should be followed by a floating point number.\n" );
+                return 0;
+            }
+            nSupp = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nSupp < 0 )
+                goto usage;
+            break;
+        case 'D':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( 1, "Command line switch \"-D\" should be followed by a floating point number.\n" );
+                return 0;
+            }
+            nDivs = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nDivs < 0 )
+                goto usage;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'w':
+            fVeryVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( argc == globalUtilOptind + 1 )
+    {
+        pTemp = Gia_ManResub1( argv[globalUtilOptind], nNodes, nSupp, nDivs, fVerbose, fVeryVerbose );
+        Abc_FrameUpdateGia( pAbc, pTemp );
+        return 0;
+    }
+    if ( pAbc->pGia == NULL )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9Resub(): There is no AIG.\n" );
+        return 1;
+    }
+    pTemp = Gia_ManResub2( pAbc->pGia, nNodes, nSupp, nDivs, fVerbose, fVeryVerbose );
+    Abc_FrameUpdateGia( pAbc, pTemp );
+    return 0;
+
+usage:
+    Abc_Print( -2, "usage: &resub [-NSD num] [-vwh]\n" );
+    Abc_Print( -2, "\t           performs AIG resubstitution\n" );
+    Abc_Print( -2, "\t-N num   : the limit on added nodes (num >= 0) [default = %d]\n",     nNodes );
+    Abc_Print( -2, "\t-S num   : the limit on support size (num > 0) [default = %d]\n",     nSupp );
+    Abc_Print( -2, "\t-D num   : the limit on divisor count (num > 0) [default = %d]\n",    nDivs );
+    Abc_Print( -2, "\t-v       : toggles printing verbose information [default = %s]\n",    fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-w       : toggles printing additional information [default = %s]\n", fVeryVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-h       : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandAbc9Syn2( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Gia_Man_t * pTemp;

src/base/acb/acbFunc.c

@@ -1541,7 +1541,7 @@ char * Acb_EnumerateSatAssigns( sat_solver * pSat, int PivotVar, int FreeVar, Ve
     {
         if ( iMint == 1000 )
         {
-            //if ( Vec_IntSize(vDivVars) == 0 )
+            if ( Vec_IntSize(vDivVars) == 0 )
             {
                 printf( "Assuming constant 0 function.\n" );
                 Vec_StrClear( vTempSop );
@@ -2511,7 +2511,7 @@ int Acb_NtkEcoPerform( Acb_Ntk_t * pNtkF, Acb_Ntk_t * pNtkG, char * pFileName[4]
 
     abctime clk  = Abc_Clock();
     int nTargets = Vec_IntSize(&pNtkF->vTargets);
-    int TimeOut  = fCisOnly ? 0 : 60;  // 60 seconds
+    int TimeOut  = fCisOnly ? 0 : 120;  // 60 seconds
     int RetValue = 1;
 
     // compute various sets of nodes

src/base/acb/acbUtil.c

@@ -671,6 +671,8 @@ int Acb_NtkExtract( char * pFileName0, char * pFileName1, int fUseXors, int fVer
         int nTargets = Vec_IntSize(&pNtkF->vTargets);
         Gia_Man_t * pGiaF = Acb_NtkToGia2( pNtkF, fUseBuf, fUseXors, &pNtkF->vTargets, 0 );
         Gia_Man_t * pGiaG = Acb_NtkToGia2( pNtkG, 0,       0,        NULL, nTargets );
+        pGiaF->pSpec = Abc_UtilStrsav( pNtkF->pDesign->pSpec );
+        pGiaG->pSpec = Abc_UtilStrsav( pNtkG->pDesign->pSpec );
         assert( Acb_NtkCiNum(pNtkF) == Acb_NtkCiNum(pNtkG) );
         assert( Acb_NtkCoNum(pNtkF) == Acb_NtkCoNum(pNtkG) );
         *ppGiaF  = pGiaF;
@@ -784,6 +786,8 @@ int Abc_NtkExtract( char * pFileName0, char * pFileName1, int fUseXors, int fVer
         Gia_Man_t * pGiaG = Abc_NtkToGia2( pNtkG, 0 );
         assert( Abc_NtkCiNum(pNtkF) == Abc_NtkCiNum(pNtkG) );
         assert( Abc_NtkCoNum(pNtkF) == Abc_NtkCoNum(pNtkG) );
+        pGiaF->pSpec = Abc_UtilStrsav( pNtkF->pSpec );
+        pGiaG->pSpec = Abc_UtilStrsav( pNtkG->pSpec );
         *ppGiaF  = pGiaF;
         *ppGiaG  = pGiaG;
         *pvNodes = Abc_NtkCollectCopies( pNtkF, pGiaF, pvNodesR, pvPolar );

src/misc/util/utilTruth.h

@@ -365,6 +365,141 @@ static inline int Abc_TtIntersect( word * pIn1, word * pIn2, int nWords, int fCo
     }
     return 0;
 }
+static inline int Abc_TtIntersectOne( word * pOut, int fComp, word * pIn, int fComp0, int nWords )
+{
+    int w;
+    if ( fComp0 )
+    {
+        if ( fComp )
+        {
+            for ( w = 0; w < nWords; w++ )
+                if ( ~pIn[w] & ~pOut[w] )
+                    return 1;
+        }
+        else
+        {
+            for ( w = 0; w < nWords; w++ )
+                if ( ~pIn[w] & pOut[w] )
+                    return 1;
+        }
+    }
+    else
+    {
+        if ( fComp )
+        {
+            for ( w = 0; w < nWords; w++ )
+                if ( pIn[w] & ~pOut[w] )
+                    return 1;
+        }
+        else
+        {
+            for ( w = 0; w < nWords; w++ )
+                if ( pIn[w] & pOut[w] )
+                    return 1;
+        }
+    }
+    return 0;
+}
+static inline int Abc_TtIntersectTwo( word * pOut, int fComp, word * pIn0, int fComp0, word * pIn1, int fComp1, int nWords )
+{
+    int w;
+    if ( fComp0 && fComp1 )
+    {
+        if ( fComp )
+        {
+            for ( w = 0; w < nWords; w++ )
+                if ( ~pIn0[w] & ~pIn1[w] & ~pOut[w] )
+                    return 1;
+        }
+        else
+        {
+            for ( w = 0; w < nWords; w++ )
+                if ( ~pIn0[w] & ~pIn1[w] & pOut[w] )
+                    return 1;
+        }
+    }
+    else if ( fComp0 )
+    {
+        if ( fComp )
+        {
+            for ( w = 0; w < nWords; w++ )
+                if ( ~pIn0[w] & pIn1[w] & ~pOut[w] )
+                    return 1;
+        }
+        else
+        {
+            for ( w = 0; w < nWords; w++ )
+                if ( ~pIn0[w] & pIn1[w] & pOut[w] )
+                    return 1;
+        }
+    }
+    else if ( fComp1 )
+    {
+        if ( fComp )
+        {
+            for ( w = 0; w < nWords; w++ )
+                if ( pIn0[w] & ~pIn1[w] & ~pOut[w] )
+                    return 1;
+        }
+        else
+        {
+            for ( w = 0; w < nWords; w++ )
+                if ( pIn0[w] & ~pIn1[w] & pOut[w] )
+                    return 1;
+        }
+    }
+    else 
+    {
+        if ( fComp )
+        {
+            for ( w = 0; w < nWords; w++ )
+                if ( pIn0[w] & pIn1[w] & ~pOut[w] )
+                    return 1;
+        }
+        else
+        {
+            for ( w = 0; w < nWords; w++ )
+                if ( pIn0[w] & pIn1[w] & pOut[w] )
+                    return 1;
+        }
+    }
+    return 0;
+}
+static inline int Abc_TtIntersectXor( word * pOut, int fComp, word * pIn0, word * pIn1, int fComp01, int nWords )
+{
+    int w;
+    if ( fComp01 )
+    {
+        if ( fComp )
+        {
+            for ( w = 0; w < nWords; w++ )
+                if ( ~(pIn0[w] ^ pIn1[w]) & ~pOut[w] )
+                    return 1;
+        }
+        else 
+        {
+            for ( w = 0; w < nWords; w++ )
+                if ( ~(pIn0[w] ^ pIn1[w]) & pOut[w] )
+                    return 1;
+        }
+    }
+    else
+    {
+        if ( fComp )
+        {
+            for ( w = 0; w < nWords; w++ )
+                if ( (pIn0[w] ^ pIn1[w]) & ~pOut[w] )
+                    return 1;
+        }
+        else 
+        {
+            for ( w = 0; w < nWords; w++ )
+                if ( (pIn0[w] ^ pIn1[w]) & pOut[w] )
+                    return 1;
+        }
+    }
+    return 0;
+}
 static inline int Abc_TtEqual( word * pIn1, word * pIn2, int nWords )
 {
     int w;
@@ -1869,6 +2004,17 @@ static inline int Abc_TtCountOnesVecXor( word * x, word * y, int nWords )
         Count += Abc_TtCountOnes( x[w] ^ y[w] );
     return Count;
 }
+static inline int Abc_TtCountOnesVecXorMask( word * x, word * y, int fCompl, word * pMask, int nWords )
+{
+    int w, Count = 0;
+    if ( fCompl )
+        for ( w = 0; w < nWords; w++ )
+            Count += Abc_TtCountOnes( pMask[w] & (x[w] ^ ~y[w]) );
+    else
+        for ( w = 0; w < nWords; w++ )
+            Count += Abc_TtCountOnes( pMask[w] & (x[w] ^ y[w]) );
+    return Count;
+}
 static inline int Abc_TtAndXorSum( word * pOut, word * pIn1, word * pIn2, int nWords )
 {
     int w, Count = 0;

src/misc/vec/vecInt.h

@@ -1397,6 +1397,14 @@ static inline void Vec_IntSortMulti( Vec_Int_t * p, int nMulti, int fReverse )
         qsort( (void *)p->pArray, (size_t)(p->nSize/nMulti), nMulti*sizeof(int), 
                 (int (*)(const void *, const void *)) Vec_IntSortCompare1 );
 }
+static inline int Vec_IntIsSorted( Vec_Int_t * p, int fReverse )
+{
+    int i;
+    for ( i = 1; i < p->nSize; i++ )
+        if ( fReverse ? (p->pArray[i-1] < p->pArray[i]) : (p->pArray[i-1] > p->pArray[i]) )
+            return 0;
+    return 1;            
+}
 
 /**Function*************************************************************