merge

12 files changed, 159 insertions, 28 deletions

diff --git a/abclib.dsp b/abclib.dsp
index 82e0637c..67bf081e 100644
--- a/abclib.dsp
+++ b/abclib.dsp
@@ -1083,6 +1083,10 @@ SOURCE=.\src\base\acb\acbPar.h
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\base\acb\acbSets.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\base\acb\acbUtil.c
 # End Source File
 # End Group
@@ -4551,6 +4555,10 @@ SOURCE=.\src\aig\gia\giaCTas.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\aig\gia\giaCut.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\aig\gia\giaDfs.c
 # End Source File
 # Begin Source File
diff --git a/src/aig/gia/giaShow.c b/src/aig/gia/giaShow.c
index 3ca31d55..ead794eb 100644
--- a/src/aig/gia/giaShow.c
+++ b/src/aig/gia/giaShow.c
@@ -218,7 +218,7 @@ void Gia_ShowPath( Gia_Man_t * p, char * pFileName )
         {
             if ( (int)Gia_ObjLevel(p, pNode) != Level || !Vec_BitEntry(vPath, i) )
                 continue;
-            fprintf( pFile, "  Node%d [label = \"%d:%d\"", i, i, Gia_ObjIsAnd(pNode)? Gia_ObjLutSize(p, i) : 0 ); 
+            fprintf( pFile, "  Node%d [label = \"%d:%d\"", i, Vec_IntSize(p->vIdsOrig)?Vec_IntEntry(p->vIdsOrig,i):i, Gia_ObjIsAnd(pNode)?Gia_ObjLutSize(p, i):0 ); 
             fprintf( pFile, ", shape = ellipse" );
             if ( pNode->fMark0 )
                 fprintf( pFile, ", style = filled" );
diff --git a/src/base/abc/abcFunc.c b/src/base/abc/abcFunc.c
index 5d0261d7..f115231f 100644
--- a/src/base/abc/abcFunc.c
+++ b/src/base/abc/abcFunc.c
@@ -1028,11 +1028,15 @@ Gia_Man_t * Abc_NtkAigToGia( Abc_Ntk_t * p, int fGiaSimple )
         }
         pNode->iTemp = Abc_LitNotCond( pHopObj->iData, Hop_IsComplement( (Hop_Obj_t *)pNode->pData ) );
     }
-    Vec_PtrFree( vNodes );
     // create primary outputs
     Abc_NtkForEachCo( p, pNode, i )
         Gia_ManAppendCo( pNew, Abc_ObjFanin0(pNode)->iTemp );
     Gia_ManSetRegNum( pNew, Abc_NtkLatchNum(p) );
+    // copy original IDs
+    pNew->vIdsOrig = Vec_IntStart( Gia_ManObjNum(pNew) );
+    Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pNode, i )
+        Vec_IntWriteEntry( pNew->vIdsOrig, Abc_Lit2Var(pNode->iTemp), Abc_ObjId(pNode) );
+    Vec_PtrFree( vNodes );
     // finish mapping 
     assert( Gia_ManObjNum(pNew) <= nObjs );
     assert( pNew->vMapping == NULL );
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index b7c9e0cd..55e14545 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -12385,6 +12385,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
 //        Cba_PrsReadBlifTest();
     }
 //    Abc_NtkComputePaths( Abc_FrameReadNtk(pAbc) );
+    Acb_DataReadTest();
     return 0;
 usage:
     Abc_Print( -2, "usage: test [-CKDNM] [-aovwh] <file_name>\n" );
diff --git a/src/base/acb/acb.h b/src/base/acb/acb.h
index 17962dc8..7c228acb 100644
--- a/src/base/acb/acb.h
+++ b/src/base/acb/acb.h
@@ -92,6 +92,7 @@ struct Acb_Ntk_t_
     Vec_Wec_t       vFanouts;   // fanouts
     Vec_Wec_t       vCnfs;      // CNF
     Vec_Str_t       vCnf;       // CNF
+    Vec_Int_t       vSuppOld;   // previous support
     // other
     Vec_Que_t *     vQue;       // temporary
     Vec_Int_t       vCover;     // temporary
@@ -574,6 +575,7 @@ static inline void Acb_NtkFree( Acb_Ntk_t * p )
     Vec_WecErase( &p->vFanouts );
     Vec_WecErase( &p->vCnfs );    
     Vec_StrErase( &p->vCnf );    
+    Vec_IntErase( &p->vSuppOld );    
     // other
     Vec_QueFreeP( &p->vQue );
     Vec_IntErase( &p->vCover );    
@@ -972,6 +974,7 @@ extern int         Acb_NtkComputeLevelD( Acb_Ntk_t * p, Vec_Int_t * vTfo );
 extern void        Acb_NtkUpdateLevelD( Acb_Ntk_t * p, int iObj );
 extern void        Acb_NtkUpdateTiming( Acb_Ntk_t * p, int iObj );
 
+extern void        Acb_NtkPrintNode( Acb_Ntk_t * p, int iObj );
 extern int         Acb_NtkCreateNode( Acb_Ntk_t * p, word uTruth, Vec_Int_t * vSupp );
 extern void        Acb_NtkUpdateNode( Acb_Ntk_t * p, int Pivot, word uTruth, Vec_Int_t * vSupp );
 
diff --git a/src/base/acb/acbMfs.c b/src/base/acb/acbMfs.c
index a17a179a..d8c6fb16 100644
--- a/src/base/acb/acbMfs.c
+++ b/src/base/acb/acbMfs.c
@@ -433,14 +433,6 @@ void Acb_NtkPrintVec( Acb_Ntk_t * p, Vec_Int_t * vVec, char * pName )
         printf( "%d ", vVec->pArray[i] );
     printf( "\n" );
 }
-void Acb_NtkPrintNode( Acb_Ntk_t * p, int Node )
-{
-    int k, iFanin, * pFanins;
-    printf( "Node %d : ", Node );
-    Acb_ObjForEachFaninFast( p, Node, pFanins, iFanin, k )
-        printf( "%d ", iFanin );
-    printf( "\n" );
-}
 void Acb_NtkPrintVec2( Acb_Ntk_t * p, Vec_Int_t * vVec, char * pName )
 {
     int i;
@@ -486,7 +478,8 @@ Vec_Int_t * Acb_NtkDivisors( Acb_Ntk_t * p, int Pivot, int nTfiLevMin, int fDela
     int k, iFanin, * pFanins;
     Vec_Int_t * vDivs = Vec_IntAlloc( 100 );
     Acb_NtkIncTravId( p );
-    if ( fDelay ) // delay-oriented
+//    if ( fDelay ) // delay-oriented
+    if ( 0 ) // delay-oriented
     {
         // start from critical fanins
         assert( Acb_ObjLevelD( p, Pivot ) > 1 );
@@ -805,7 +798,7 @@ Vec_Int_t * Acb_NtkWindow( Acb_Ntk_t * p, int Pivot, int nTfiLevs, int nTfoLevs,
     // mark limited TFO of the divisors
     vMarked = Acb_ObjMarkTfo( p, vDivs, Pivot, nTfoLevMax, nFanMax );
     // collect TFO and roots
-    Acb_ObjDeriveTfo( p, Pivot, nTfoLevMax, nFanMax, &vTfo, &vRoots, fDelay );
+    Acb_ObjDeriveTfo( p, Pivot, nTfoLevMax, nFanMax, &vTfo, &vRoots, 0 );//fDelay );
     if ( fVerbose ) Acb_NtkPrintVec( p, vTfo, "vTfo" );
     if ( fVerbose ) Acb_NtkPrintVec( p, vRoots, "vRoots" );
     // collect side inputs of the TFO
@@ -1599,8 +1592,8 @@ void Acb_NtkOpt( Acb_Ntk_t * pNtk, Acb_Par_t * pPars )
                 if ( iObj < nNodes && !Vec_BitEntry(vVisited, iObj) && Acb_NtkObjMffcEstimate(pNtk, iObj) >= n )
                 {
                     pMan->nNodes++;
-                    //if ( iObj != 7 )
-                    //    continue;
+                    if ( iObj != 103 )
+                        continue;
                     //Acb_NtkOptNode( pMan, iObj );
                     while ( (RetValue = Acb_NtkOptNode(pMan, iObj)) && Acb_ObjFaninNum(pNtk, iObj) );                    
                     Vec_BitWriteEntry( vVisited, iObj, 1 );
@@ -1609,14 +1602,16 @@ void Acb_NtkOpt( Acb_Ntk_t * pNtk, Acb_Par_t * pPars )
     }
     else
     {
+        int Value;
         Acb_NtkUpdateTiming( pNtk, -1 ); // compute delay information
-        while ( Vec_QueTopPriority(pNtk->vQue) > 0 )
+        while ( (Value = (int)Vec_QueTopPriority(pNtk->vQue)) > 0 )
         {
             int iObj = Vec_QuePop(pNtk->vQue);
             if ( !Acb_ObjType(pNtk, iObj) )
                 continue;
-            //if ( iObj != 28 )
-            //    continue;
+            if ( iObj != 103 )
+                continue;
+            //printf( "Trying node %4d (%4d) ", iObj, Value );
             Acb_NtkOptNode( pMan, iObj ); 
         }
     }
diff --git a/src/base/acb/acbSets.c b/src/base/acb/acbSets.c
new file mode 100644
index 00000000..362910d9
--- /dev/null
+++ b/src/base/acb/acbSets.c
@@ -0,0 +1,54 @@
+/**CFile****************************************************************
+
+  FileName    [acbSets.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Hierarchical word-level netlist.]
+
+  Synopsis    [Reading data from file.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - July 21, 2015.]
+
+  Revision    [$Id: acbSets.c,v 1.00 2014/11/29 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "acb.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Acb_DataReadTest()
+{
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/base/acb/acbUtil.c b/src/base/acb/acbUtil.c
index 4b839ec2..2d56a553 100644
--- a/src/base/acb/acbUtil.c
+++ b/src/base/acb/acbUtil.c
@@ -55,11 +55,15 @@ void Acb_ObjCollectTfi_rec( Acb_Ntk_t * p, int iObj, int fTerm )
 }
 Vec_Int_t * Acb_ObjCollectTfi( Acb_Ntk_t * p, int iObj, int fTerm )
 {
-    int i;
+    int i, Node;
     Vec_IntClear( &p->vArray0 );
     Acb_NtkIncTravId( p );
     if ( iObj > 0 )
+    {
+        Vec_IntForEachEntry( &p->vSuppOld, Node, i )
+            Acb_ObjCollectTfi_rec( p, Node, fTerm );
         Acb_ObjCollectTfi_rec( p, iObj, fTerm );
+    }
     else
         Acb_NtkForEachCo( p, iObj, i )
             Acb_ObjCollectTfi_rec( p, iObj, fTerm );
@@ -267,10 +271,12 @@ void Acb_NtkPrintPaths( Acb_Ntk_t * p )
     int iObj;
     Acb_NtkForEachObj( p, iObj )
     {
-        printf( "Obj = %5d : ", iObj );
-        printf( "PathD = %5d  ", Acb_ObjPathD(p, iObj) );
-        printf( "PathR = %5d  ", Acb_ObjPathR(p, iObj) );
-        printf( "Paths = %5d  ", Acb_ObjPathD(p, iObj) + Acb_ObjPathR(p, iObj) );
+        printf( "Obj = %5d :   ",   iObj );
+        printf( "LevelD = %5d  ",   Acb_ObjLevelD(p, iObj) );
+        printf( "LevelR = %5d    ", Acb_ObjLevelR(p, iObj) );
+        printf( "PathD = %5d  ",    Acb_ObjPathD(p, iObj) );
+        printf( "PathR = %5d    ",  Acb_ObjPathR(p, iObj) );
+        printf( "Paths = %5d  ",    Acb_ObjPathD(p, iObj) * Acb_ObjPathR(p, iObj) );
         printf( "\n" );
     }
 }
@@ -323,7 +329,7 @@ void Acb_ObjUpdatePriority( Acb_Ntk_t * p, int iObj )
         p->vQue = Vec_QueAlloc( 1000 );
         Vec_QueSetPriority( p->vQue, Vec_FltArrayP(&p->vCounts) );
     }
-    nPaths = Acb_ObjPathD(p, iObj) + Acb_ObjPathR(p, iObj);
+    nPaths = Acb_ObjPathD(p, iObj) * Acb_ObjPathR(p, iObj);
     Acb_ObjSetCounts( p, iObj, (float)nPaths );
     if ( Vec_QueIsMember( p->vQue, iObj ) )
     {
@@ -394,6 +400,14 @@ void Acb_NtkUpdateTiming( Acb_Ntk_t * p, int iObj )
   SeeAlso     []
 
 ***********************************************************************/
+void Acb_NtkPrintNode( Acb_Ntk_t * p, int iObj )
+{
+    int k, iFanin, * pFanins; 
+    printf( "Node %5d : ", iObj );
+    Acb_ObjForEachFaninFast( p, iObj, pFanins, iFanin, k )
+        printf( "%d ", iFanin );
+    printf( "LevelD = %d. LevelR = %d.\n", Acb_ObjLevelD(p, iObj), Acb_ObjLevelR(p, iObj) );
+}
 int Acb_NtkCreateNode( Acb_Ntk_t * p, word uTruth, Vec_Int_t * vSupp )
 {
     int Pivot = Acb_ObjAlloc( p, ABC_OPER_LUT, Vec_IntSize(vSupp), 0 );
@@ -432,14 +446,28 @@ void Acb_NtkResetNode( Acb_Ntk_t * p, int Pivot, word uTruth, Vec_Int_t * vSupp
             Acb_NtkResetNode( p, iFanin, 0, NULL );
     Vec_IntFree( vFanins );
 }
+void Acb_NtkSaveSupport( Acb_Ntk_t * p, int iObj )
+{
+    int k, iFanin, * pFanins; 
+    Vec_IntClear( &p->vSuppOld );
+    Acb_ObjForEachFaninFast( p, iObj, pFanins, iFanin, k )
+        Vec_IntPush( &p->vSuppOld, iFanin );
+}
 void Acb_NtkUpdateNode( Acb_Ntk_t * p, int Pivot, word uTruth, Vec_Int_t * vSupp )
 {
+    //int Level = Acb_ObjLevelD(p, Pivot);
+    Acb_NtkSaveSupport( p, Pivot );
+    //Acb_NtkPrintNode( p, Pivot );
     Acb_NtkResetNode( p, Pivot, uTruth, vSupp );
     Acb_ObjComputeLevelD( p, Pivot );
+    //assert( Level > Acb_ObjLevelD(p, Pivot) );
+    //Acb_NtkPrintNode( p, Pivot );
     if ( p->vQue == NULL )
         Acb_NtkUpdateLevelD( p, Pivot );
     else
-        Acb_NtkUpdateTiming( p, Pivot );
+//        Acb_NtkUpdateTiming( p, Pivot );
+        Acb_NtkUpdateTiming( p, -1 );
+    Vec_IntClear( &p->vSuppOld );
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/acb/module.make b/src/base/acb/module.make
index ce5dcaeb..06affeff 100644
--- a/src/base/acb/module.make
+++ b/src/base/acb/module.make
@@ -3,4 +3,5 @@ SRC +=    src/base/acb/acbAbc.c \
     src/base/acb/acbCom.c \
     src/base/acb/acbFunc.c \
     src/base/acb/acbMfs.c \
+    src/base/acb/acbSets.c \
     src/base/acb/acbUtil.c 
diff --git a/src/misc/util/utilNam.c b/src/misc/util/utilNam.c
index 6cb180c0..30a68c63 100644
--- a/src/misc/util/utilNam.c
+++ b/src/misc/util/utilNam.c
@@ -131,11 +131,15 @@ void Abc_NamStop( Abc_Nam_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NamPrint( Abc_Nam_t * p )
+void Abc_NamPrint( Abc_Nam_t * p, char * pFileName )
 {
+    FILE * pFile = pFileName ? fopen( pFileName, "wb" ) : stdout;
     int h, i;
+    if ( pFile == NULL ) { printf( "Count node open file %s\n", pFileName ); return; }
     Vec_IntForEachEntryStart( &p->vInt2Handle, h, i, 1 )
-        Abc_Print( 1, "%d=\n%s\n", i, Abc_NamHandleToStr(p, h) );
+        fprintf( pFile, "%8d = %s\n", i, Abc_NamHandleToStr(p, h) );
+    if ( pFile != stdout )
+        fclose(pFile);
 }
 
 /**Function*************************************************************
@@ -275,6 +279,22 @@ int Abc_NamStrHash( const char * pStr, const char * pLim, int nTableSize )
     }
     return uHash % nTableSize;
 }
+// https://en.wikipedia.org/wiki/Jenkins_hash_function
+int Abc_NamStrHash2( const char * pStr, const char * pLim, int nTableSize ) 
+{
+    int nSize = pLim ? pLim - pStr : -1;
+    int i = 0; unsigned hash = 0;
+    while ( i != nSize && pStr[i] ) 
+    {
+        hash += pStr[i++];
+        hash += hash << 10;
+        hash ^= hash >> 6;
+    }
+    hash += hash << 3;
+    hash ^= hash >> 11;
+    hash += hash << 15;
+    return (int)(hash % nTableSize);
+}
 
 /**Function*************************************************************
 
diff --git a/src/misc/util/utilNam.h b/src/misc/util/utilNam.h
index 8083a566..8e054fc1 100644
--- a/src/misc/util/utilNam.h
+++ b/src/misc/util/utilNam.h
@@ -52,7 +52,7 @@ typedef struct Abc_Nam_t_           Abc_Nam_t;
 /*=== utilNam.c ===============================================================*/
 extern Abc_Nam_t *     Abc_NamStart( int nObjs, int nAveSize );
 extern void            Abc_NamStop( Abc_Nam_t * p );
-extern void            Abc_NamPrint( Abc_Nam_t * p );
+extern void            Abc_NamPrint( Abc_Nam_t * p, char * pFileName );
 extern Abc_Nam_t *     Abc_NamRef( Abc_Nam_t * p );
 extern void            Abc_NamDeref( Abc_Nam_t * p );
 extern int             Abc_NamObjNumMax( Abc_Nam_t * p );
diff --git a/src/misc/vec/vecHsh.h b/src/misc/vec/vecHsh.h
index de9a038a..4f15f6f0 100644
--- a/src/misc/vec/vecHsh.h
+++ b/src/misc/vec/vecHsh.h
@@ -140,7 +140,24 @@ static inline int Hsh_IntManEntryNum( Hsh_IntMan_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-static inline int Hsh_IntManHash( unsigned * pData, int nSize, int nTableSize )
+// https://en.wikipedia.org/wiki/Jenkins_hash_function
+static inline int Hsh_IntManHash( unsigned * pData, int nSize, int nTableSize ) 
+{
+    int i = 0; unsigned hash = 0;
+    unsigned char * pDataC = (unsigned char *)pData;
+    nSize <<= 2;
+    while ( i != nSize ) 
+    {
+        hash += pDataC[i++];
+        hash += hash << 10;
+        hash ^= hash >> 6;
+    }
+    hash += hash << 3;
+    hash ^= hash >> 11;
+    hash += hash << 15;
+    return (int)(hash % nTableSize);
+}
+static inline int Hsh_IntManHash2( unsigned * pData, int nSize, int nTableSize )
 {
     static int s_Primes[7] = { 4177, 5147, 5647, 6343, 7103, 7873, 8147 };
     unsigned char * pDataC = (unsigned char *)pData;