Exploration of Sasao's decomposition and minor improvements.

src/base/abc/abcFunc.c

@@ -52,7 +52,7 @@ extern int Abc_CountZddCubes( DdManager * dd, DdNode * zCover );
   SeeAlso     []
 
 ***********************************************************************/
-DdNode * Abc_ConvertSopToBdd( DdManager * dd, char * pSop )
+DdNode * Abc_ConvertSopToBdd( DdManager * dd, char * pSop, DdNode ** pbVars )
 {
     DdNode * bSum, * bCube, * bTemp, * bVar;
     char * pCube;
@@ -65,7 +65,7 @@ DdNode * Abc_ConvertSopToBdd( DdManager * dd, char * pSop )
     {
         for ( v = 0; v < nVars; v++ )
         {
-            bSum  = Cudd_bddXor( dd, bTemp = bSum, Cudd_bddIthVar(dd, v) );   Cudd_Ref( bSum );
+            bSum  = Cudd_bddXor( dd, bTemp = bSum, pbVars? pbVars[v] : Cudd_bddIthVar(dd, v) );   Cudd_Ref( bSum );
             Cudd_RecursiveDeref( dd, bTemp );
         }
     }
@@ -78,9 +78,9 @@ DdNode * Abc_ConvertSopToBdd( DdManager * dd, char * pSop )
             Abc_CubeForEachVar( pCube, Value, v )
             {
                 if ( Value == '0' )
-                    bVar = Cudd_Not( Cudd_bddIthVar( dd, v ) );
+                    bVar = Cudd_Not( pbVars? pbVars[v] : Cudd_bddIthVar( dd, v ) );
                 else if ( Value == '1' )
-                    bVar = Cudd_bddIthVar( dd, v );
+                    bVar = pbVars? pbVars[v] : Cudd_bddIthVar( dd, v );
                 else
                     continue;
                 bCube  = Cudd_bddAnd( dd, bTemp = bCube, bVar );   Cudd_Ref( bCube );
@@ -128,7 +128,7 @@ int Abc_NtkSopToBdd( Abc_Ntk_t * pNtk )
     Abc_NtkForEachNode( pNtk, pNode, i )
     {
         assert( pNode->pData );
-        pNode->pData = Abc_ConvertSopToBdd( dd, (char *)pNode->pData );
+        pNode->pData = Abc_ConvertSopToBdd( dd, (char *)pNode->pData, NULL );
         if ( pNode->pData == NULL )
         {
             printf( "Abc_NtkSopToBdd: Error while converting SOP into BDD.\n" );
@@ -282,7 +282,7 @@ char * Abc_ConvertBddToSop( Mem_Flex_t * pMan, DdManager * dd, DdNode * bFuncOn,
     // verify
     if ( fVerify )
     {
-        bFuncNew = Abc_ConvertSopToBdd( dd, pSop );  Cudd_Ref( bFuncNew );
+        bFuncNew = Abc_ConvertSopToBdd( dd, pSop, NULL );  Cudd_Ref( bFuncNew );
         if ( bFuncOn == bFuncOnDc )
         {
             if ( bFuncNew != bFuncOn )
@@ -483,7 +483,7 @@ void Abc_NtkLogicMakeDirectSops( Abc_Ntk_t * pNtk )
     Abc_NtkForEachNode( pNtk, pNode, i )
         if ( Abc_SopIsComplement((char *)pNode->pData) )
         {
-            bFunc = Abc_ConvertSopToBdd( dd, (char *)pNode->pData );  Cudd_Ref( bFunc );
+            bFunc = Abc_ConvertSopToBdd( dd, (char *)pNode->pData, NULL );  Cudd_Ref( bFunc );
             pNode->pData = Abc_ConvertBddToSop( (Mem_Flex_t *)pNtk->pManFunc, dd, bFunc, bFunc, Abc_ObjFaninNum(pNode), 0, vCube, 1 );
             Cudd_RecursiveDeref( dd, bFunc );
             assert( !Abc_SopIsComplement((char *)pNode->pData) );

src/base/abci/abc.c

@@ -8665,9 +8665,9 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
 */
 
 /*
-//    Bbl_ManSimpleDemo();
-//    pNtkRes = Abc_NtkCRetime( pNtk );
-    pNtkRes = NULL;
+{
+    extern Abc_Ntk_t * Abc_NtkBddDec( Abc_Ntk_t * pNtk, int fVerbose );
+    pNtkRes = Abc_NtkBddDec( pNtk, fVerbose );
     if ( pNtkRes == NULL )
     {
         Abc_Print( -1, "Command has failed.\n" );
@@ -8675,11 +8675,19 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     // replace the current network
     Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+}
 */
 
+//    Abc_NtkCheckAbsorb( pNtk, 4 );
+
+    if ( fBmc )
+        Abc_NktMffcServerTest( pNtk );
+    else
+        Abc_ResPartitionTest( pNtk );
+
 //    Abc_NtkHelloWorld( pNtk );
 //    Abc_NktMffcTest( pNtk );
-    Abc_NktMffcServerTest( pNtk );
+//    Abc_NktMffcServerTest( pNtk );
     return 0;
 usage:
     Abc_Print( -2, "usage: test [-h] <file_name>\n" );

src/base/abci/abcLutmin.c

@@ -40,6 +40,76 @@ ABC_NAMESPACE_IMPL_START
 
 /**Function*************************************************************
 
+  Synopsis    [Check if a LUT can absort a fanin.]
+
+  Description [The fanins are (c, d0, d1).]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_ObjCheckAbsorb( Abc_Obj_t * pObj, Abc_Obj_t * pPivot, int nLutSize, Vec_Ptr_t * vFanins )
+{
+    Abc_Obj_t * pFanin;
+    int i;
+    assert( Abc_ObjIsNode(pObj) && Abc_ObjIsNode(pPivot) );
+    // add fanins of the node
+    Vec_PtrClear( vFanins );
+    Abc_ObjForEachFanin( pObj, pFanin, i )
+        if ( pFanin != pPivot )
+            Vec_PtrPush( vFanins, pFanin );
+    // add fanins of the fanin
+    Abc_ObjForEachFanin( pPivot, pFanin, i )
+    {
+        Vec_PtrPushUnique( vFanins, pFanin );
+        if ( Vec_PtrSize(vFanins) > nLutSize )
+            return 0;
+    }
+    return 1;
+} 
+
+/**Function*************************************************************
+
+  Synopsis    [Check how many times a LUT can absorb a fanin.]
+
+  Description [The fanins are (c, d0, d1).]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkCheckAbsorb( Abc_Ntk_t * pNtk, int nLutSize )
+{
+    Vec_Int_t * vCounts;
+    Vec_Ptr_t * vFanins;
+    Abc_Obj_t * pObj, * pFanin;
+    int i, k, Counter = 0, Counter2 = 0, clk = clock();
+    vCounts = Vec_IntStart( Abc_NtkObjNumMax(pNtk) );
+    vFanins = Vec_PtrAlloc( 100 );
+    Abc_NtkForEachNode( pNtk, pObj, i )
+    Abc_ObjForEachFanin( pObj, pFanin, k )
+        if ( Abc_ObjIsNode(pFanin) && Abc_ObjCheckAbsorb( pObj, pFanin, nLutSize, vFanins ) )
+        {
+            Vec_IntAddToEntry( vCounts, Abc_ObjId(pFanin), 1 );
+            Counter++;
+        }
+    Vec_PtrFree( vFanins );
+    Abc_NtkForEachNode( pNtk, pObj, i )
+        if ( Vec_IntEntry(vCounts, Abc_ObjId(pObj)) == Abc_ObjFanoutNum(pObj) )
+        {
+//            printf( "%d ", Abc_ObjId(pObj) );
+            Counter2++;
+        }
+    printf( "Absorted = %6d. (%6.2f %%)   Fully = %6d. (%6.2f %%)  ", 
+        Counter,  100.0 * Counter  / Abc_NtkNodeNum(pNtk), 
+        Counter2, 100.0 * Counter2 / Abc_NtkNodeNum(pNtk) );
+    Abc_PrintTime( 1, "Time", clock() - clk );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Implements 2:1 MUX using one 3-LUT.]
 
   Description [The fanins are (c, d0, d1).]

src/base/abci/abcMffc.c

@@ -1244,7 +1244,7 @@ void Abc_NktMffcServerTest( Abc_Ntk_t * pNtk )
             continue;
         Cost = 1.0 * Vec_IntSize(vGlob)/(Vec_IntSize(vLeaves) + Vec_IntSize(vRoots));
         CostAll += Cost;
-        if ( Cost < 0.4 )
+        if ( Cost < 0.5 )
             continue;
 
         printf( "%6d : Root =%3d. Leaf =%3d. Node =%4d. ", 
@@ -1254,7 +1254,7 @@ void Abc_NktMffcServerTest( Abc_Ntk_t * pNtk )
             printf( "%d ", Entry );
         printf( "\n" );
 
-        sprintf( pFileName, "%s_mffc%04d_%02d.blif", Abc_NtkName(pNtk), i, Vec_IntSize(vGlob) );
+        sprintf( pFileName, "%sc%04di%02dn%02d.blif", Abc_NtkName(pNtk), i, Vec_IntSize(vLeaves), Vec_IntSize(vGlob) );
         Abc_NktMffcPrintInt( pFileName, pNtk, vRoots, vGlob, vLeaves );
     }
     Vec_IntFree( vLeaves );

src/opt/dec/decFactor.c

@@ -366,12 +366,12 @@ Mvc_Cover_t * Dec_ConvertSopToMvc( char * pSop )
 ***********************************************************************/
 int Dec_FactorVerify( char * pSop, Dec_Graph_t * pFForm )
 {
-    extern DdNode * Abc_ConvertSopToBdd( DdManager * dd, char * pSop );
+    extern DdNode * Abc_ConvertSopToBdd( DdManager * dd, char * pSop, DdNode ** pbVars );
     extern DdNode * Dec_GraphDeriveBdd( DdManager * dd, Dec_Graph_t * pGraph );
     DdManager * dd = (DdManager *)Abc_FrameReadManDd();
     DdNode * bFunc1, * bFunc2;
     int RetValue;
-    bFunc1 = Abc_ConvertSopToBdd( dd, pSop );    Cudd_Ref( bFunc1 );
+    bFunc1 = Abc_ConvertSopToBdd( dd, pSop, NULL );    Cudd_Ref( bFunc1 );
     bFunc2 = Dec_GraphDeriveBdd( dd, pFForm );   Cudd_Ref( bFunc2 );
 //Extra_bddPrint( dd, bFunc1 ); printf("\n");
 //Extra_bddPrint( dd, bFunc2 ); printf("\n");