Added printing MFFC sizes and deriving TT from SOP.

8 files changed, 138 insertions, 12 deletions

diff --git a/abclib.dsp b/abclib.dsp
index ed97dec6..5c8c5b91 100644
--- a/abclib.dsp
+++ b/abclib.dsp
@@ -4155,6 +4155,10 @@ SOURCE=.\src\aig\au\auBridge.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\aig\au\auCone.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\aig\au\auCore.c
 # End Source File
 # Begin Source File
@@ -4167,10 +4171,22 @@ SOURCE=.\src\aig\au\auCut.h
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\aig\au\auData.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\aig\au\auDec.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\aig\au\auDecomp.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\au\auDiv.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\aig\au\auDsd.c
 # End Source File
 # Begin Source File
@@ -4179,6 +4195,10 @@ SOURCE=.\src\aig\au\auFanout.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\aig\au\auFour.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\aig\au\auInt.h
 # End Source File
 # Begin Source File
@@ -4195,6 +4215,10 @@ SOURCE=.\src\aig\au\auNtk.h
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\aig\au\auResub.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\aig\au\auSweep.c
 # End Source File
 # Begin Source File
@@ -4203,6 +4227,14 @@ SOURCE=.\src\aig\au\auTable.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\aig\au\auTruth.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\au\auTruth.h
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\aig\au\auUtil.c
 # End Source File
 # End Group
diff --git a/src/aig/dar/darCore.c b/src/aig/dar/darCore.c
index 9811757c..a80277d5 100644
--- a/src/aig/dar/darCore.c
+++ b/src/aig/dar/darCore.c
@@ -56,6 +56,8 @@ void Dar_ManDefaultRwrParams( Dar_RwrPar_t * pPars )
     pPars->fVeryVerbose =  0;
 }
 
+#define MAX_VAL 10
+
 /**Function*************************************************************
 
   Synopsis    []
@@ -76,6 +78,7 @@ int Dar_ManRewrite( Aig_Man_t * pAig, Dar_RwrPar_t * pPars )
     Aig_Obj_t * pObj, * pObjNew;
     int i, k, nNodesOld, nNodeBefore, nNodeAfter, Required;
     int clk = 0, clkStart, Counter = 0;
+    int nMffcSize, nMffcGains[MAX_VAL+1][MAX_VAL+1] = {{0}};
     // prepare the library
     Dar_LibPrepare( pPars->nSubgMax ); 
     // create rewriting manager
@@ -154,13 +157,14 @@ p->timeCuts += clock() - clk;
 
         // evaluate the cuts
         p->GainBest = -1;
-        Required = pAig->vLevelR? Aig_ObjRequiredLevel(pAig, pObj) : ABC_INFINITY;
+        nMffcSize   = -1;
+        Required    = pAig->vLevelR? Aig_ObjRequiredLevel(pAig, pObj) : ABC_INFINITY;
         Dar_ObjForEachCut( pObj, pCut, k )
         {
             int nLeavesOld = pCut->nLeaves;
             if ( pCut->nLeaves == 3 )
                 pCut->pLeaves[pCut->nLeaves++] = 0;
-            Dar_LibEval( p, pObj, pCut, Required );
+            Dar_LibEval( p, pObj, pCut, Required, &nMffcSize );
             pCut->nLeaves = nLeavesOld; 
         }
         // check the best gain
@@ -169,6 +173,7 @@ p->timeCuts += clock() - clk;
 //            Aig_ObjOrderAdvance( pAig );
             continue;
         }
+//        nMffcGains[p->GainBest < MAX_VAL ? p->GainBest : MAX_VAL][nMffcSize < MAX_VAL ? nMffcSize : MAX_VAL]++;
         // remove the old cuts
         Dar_ObjSetCuts( pObj, NULL );
         // if we end up here, a rewriting step is accepted
@@ -185,6 +190,18 @@ p->timeCuts += clock() - clk;
         p->ClassGains[p->ClassBest] += nNodeBefore - nNodeAfter;
     }
 //    Aig_ManOrderStop( pAig );
+/*
+    printf( "Distribution of gain (row) by MFFC size (column) %s 0-costs:\n", p->pPars->fUseZeros? "with":"without" );
+    for ( k = 0; k <= MAX_VAL; k++ )
+        printf( "<%4d> ", k );
+    printf( "\n" );
+    for ( i = 0; i <= MAX_VAL; i++ )
+    {
+        for ( k = 0; k <= MAX_VAL; k++ )
+            printf( "%6d ", nMffcGains[i][k] );
+        printf( "\n" );
+    }
+*/
 
 p->timeTotal = clock() - clkStart;
 p->timeOther = p->timeTotal - p->timeCuts - p->timeEval;
diff --git a/src/aig/dar/darInt.h b/src/aig/dar/darInt.h
index 70831534..23e89d3c 100644
--- a/src/aig/dar/darInt.h
+++ b/src/aig/dar/darInt.h
@@ -147,7 +147,7 @@ extern Vec_Int_t *     Dar_LibReadPrios();
 extern void            Dar_LibStart();
 extern void            Dar_LibStop();
 extern void            Dar_LibReturnCanonicals( unsigned * pCanons );
-extern void            Dar_LibEval( Dar_Man_t * p, Aig_Obj_t * pRoot, Dar_Cut_t * pCut, int Required );
+extern void            Dar_LibEval( Dar_Man_t * p, Aig_Obj_t * pRoot, Dar_Cut_t * pCut, int Required, int * pnMffcSize );
 extern Aig_Obj_t *     Dar_LibBuildBest( Dar_Man_t * p );
 /*=== darMan.c ============================================================*/
 extern Dar_Man_t *     Dar_ManStart( Aig_Man_t * pAig, Dar_RwrPar_t * pPars );
diff --git a/src/aig/dar/darLib.c b/src/aig/dar/darLib.c
index 52fd36b3..bf78577c 100644
--- a/src/aig/dar/darLib.c
+++ b/src/aig/dar/darLib.c
@@ -915,7 +915,7 @@ int Dar_LibEval_rec( Dar_LibObj_t * pObj, int Out, int nNodesSaved, int Required
   SeeAlso     []
 
 ***********************************************************************/
-void Dar_LibEval( Dar_Man_t * p, Aig_Obj_t * pRoot, Dar_Cut_t * pCut, int Required )
+void Dar_LibEval( Dar_Man_t * p, Aig_Obj_t * pRoot, Dar_Cut_t * pCut, int Required, int * pnMffcSize )
 {
     int fTraining = 0;
     float PowerSaved, PowerAdded;
@@ -961,6 +961,7 @@ void Dar_LibEval( Dar_Man_t * p, Aig_Obj_t * pRoot, Dar_Cut_t * pCut, int Requir
         p->GainBest   = nNodesGained;
         p->ClassBest  = Class;
         assert( p->LevelBest <= Required );
+        *pnMffcSize   = nNodesSaved;
     }
 clk = clock() - clk;
 p->ClassTimes[Class] += clk;
diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index fbd6b479..74c4b01a 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -748,7 +748,7 @@ extern ABC_DLL void               Abc_NtkPrintStats( Abc_Ntk_t * pNtk, int fFact
 extern ABC_DLL void               Abc_NtkPrintIo( FILE * pFile, Abc_Ntk_t * pNtk );
 extern ABC_DLL void               Abc_NtkPrintLatch( FILE * pFile, Abc_Ntk_t * pNtk );
 extern ABC_DLL void               Abc_NtkPrintFanio( FILE * pFile, Abc_Ntk_t * pNtk );
-extern ABC_DLL void               Abc_NtkPrintFanioNew( FILE * pFile, Abc_Ntk_t * pNtk );
+extern ABC_DLL void               Abc_NtkPrintFanioNew( FILE * pFile, Abc_Ntk_t * pNtk, int fMffc );
 extern ABC_DLL void               Abc_NodePrintFanio( FILE * pFile, Abc_Obj_t * pNode );
 extern ABC_DLL void               Abc_NtkPrintFactor( FILE * pFile, Abc_Ntk_t * pNtk, int fUseRealNames );
 extern ABC_DLL void               Abc_NodePrintFactor( FILE * pFile, Abc_Obj_t * pNode, int fUseRealNames );
@@ -836,6 +836,7 @@ extern ABC_DLL char *             Abc_SopEncoderPos( Mem_Flex_t * pMan, int iVal
 extern ABC_DLL char *             Abc_SopEncoderLog( Mem_Flex_t * pMan, int iBit, int nValues );
 extern ABC_DLL char *             Abc_SopDecoderPos( Mem_Flex_t * pMan, int nValues );
 extern ABC_DLL char *             Abc_SopDecoderLog( Mem_Flex_t * pMan, int nValues );
+extern ABC_DLL word               Abc_SopToTruth( char * pSop, int nInputs );
 /*=== abcStrash.c ==========================================================*/
 extern ABC_DLL Abc_Ntk_t *        Abc_NtkStrash( Abc_Ntk_t * pNtk, int fAllNodes, int fCleanup, int fRecord );
 extern ABC_DLL Abc_Obj_t *        Abc_NodeStrash( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode, int fRecord );
diff --git a/src/base/abc/abcSop.c b/src/base/abc/abcSop.c
index e562a32a..2a4cf7d2 100644
--- a/src/base/abc/abcSop.c
+++ b/src/base/abc/abcSop.c
@@ -1149,6 +1149,58 @@ char * Abc_SopDecoderLog( Mem_Flex_t * pMan, int nValues )
     return pResult;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Computes truth table of the node.]
+ 
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+word Abc_SopToTruth( char * pSop, int nInputs )
+{
+    static word Truth[8] = {
+        0xAAAAAAAAAAAAAAAA,
+        0xCCCCCCCCCCCCCCCC,
+        0xF0F0F0F0F0F0F0F0,
+        0xFF00FF00FF00FF00,
+        0xFFFF0000FFFF0000,
+        0xFFFFFFFF00000000,
+        0x0000000000000000,
+        0xFFFFFFFFFFFFFFFF
+    };
+    word Cube, Result = 0;
+    int v, lit = 0;
+    int nVars = Abc_SopGetVarNum(pSop);
+    assert( nVars >= 0 && nVars <= 6 );
+    assert( nVars == nInputs );
+    do {
+        Cube = Truth[7];
+        for ( v = 0; v < nVars; v++, lit++ )
+        {
+            if ( pSop[lit] == '1' )
+                Cube &=  Truth[v];
+            else if ( pSop[lit] == '0' )
+                Cube &= ~Truth[v];
+            else if ( pSop[lit] != '-' )
+                assert( 0 );
+        }
+        Result |= Cube;
+        assert( pSop[lit] == ' ' );
+        lit++;
+        lit++;
+        assert( pSop[lit] == '\n' );
+        lit++;
+    } while ( pSop[lit] );
+    if ( Abc_SopIsComplement(pSop) )
+        Result = ~Result;
+    return Result;
+}
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index c525cda1..123bed95 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -1231,15 +1231,20 @@ int Abc_CommandPrintFanio( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
     int c;
+    int fMffc;
     int fVerbose;
 
     // set defaults
+    fMffc    = 0;
     fVerbose = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "mvh" ) ) != EOF )
     {
         switch ( c )
         {
+        case 'm':
+            fMffc ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -1260,12 +1265,13 @@ int Abc_CommandPrintFanio( Abc_Frame_t * pAbc, int argc, char ** argv )
     if ( fVerbose )
         Abc_NtkPrintFanio( stdout, pNtk );
     else
-        Abc_NtkPrintFanioNew( stdout, pNtk );
+        Abc_NtkPrintFanioNew( stdout, pNtk, fMffc );
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: print_fanio [-vh]\n" );
+    Abc_Print( -2, "usage: print_fanio [-mvh]\n" );
     Abc_Print( -2, "\t        prints the statistics about fanins/fanouts of all nodes\n" );
+    Abc_Print( -2, "\t-m    : toggles printing MFFC sizes instead of fanouts [default = %s]\n", fMffc? "yes": "no" );
     Abc_Print( -2, "\t-v    : toggles verbose way of printing the stats [default = %s]\n", fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h    : print the command usage\n");
     return 1;
@@ -8682,8 +8688,10 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
 
 /*
 {
-    extern Abc_Ntk_t * Au_ManTransformTest( Abc_Ntk_t * pAig );
-    pNtkRes = Au_ManTransformTest( pNtk );
+//    extern Abc_Ntk_t * Au_ManTransformTest( Abc_Ntk_t * pAig );
+    extern Abc_Ntk_t * Au_ManResubTest( Abc_Ntk_t * pAig );
+//    pNtkRes = Au_ManTransformTest( pNtk );
+    pNtkRes = Au_ManResubTest( pNtk );
     if ( pNtkRes == NULL )
     {
         Abc_Print( -1, "Command has failed.\n" );
@@ -8693,12 +8701,20 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
     Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
 }
 */
+
 /*
 {
     extern void Au_DsdVecTest( int nVars );
     Au_DsdVecTest( 6 );
 }
 */
+{
+//    extern void Au_NtkReadFour( Abc_Ntk_t * pNtk );
+//    extern void Au_Data4VerifyFour();
+//    Au_NtkReadFour( pNtk );
+//    Au_Data4VerifyFour();
+}
+
 
 //    Abc_NtkCheckAbsorb( pNtk, 4 );
 /*
diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c
index bd5f986f..3b0ab94a 100644
--- a/src/base/abci/abcPrint.c
+++ b/src/base/abci/abcPrint.c
@@ -535,7 +535,7 @@ void Abc_NtkPrintFanio( FILE * pFile, Abc_Ntk_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NtkPrintFanioNew( FILE * pFile, Abc_Ntk_t * pNtk )
+void Abc_NtkPrintFanioNew( FILE * pFile, Abc_Ntk_t * pNtk, int fMffc )
 {
     char Buffer[100];
     Abc_Obj_t * pNode;
@@ -548,9 +548,13 @@ void Abc_NtkPrintFanioNew( FILE * pFile, Abc_Ntk_t * pNtk )
     nFaninsAll = nFanoutsAll = 0;
     Abc_NtkForEachNode( pNtk, pNode, i )
     {
+        if ( fMffc && Abc_ObjFanoutNum(pNode) == 1 )
+            continue;
         nFanins  = Abc_ObjFaninNum(pNode);
         if ( Abc_NtkIsNetlist(pNtk) )
             nFanouts = Abc_ObjFanoutNum( Abc_ObjFanout0(pNode) );
+        else if ( fMffc )
+            nFanouts = Abc_NodeMffcSize(pNode);
         else
             nFanouts = Abc_ObjFanoutNum(pNode);
         nFaninsAll  += nFanins;
@@ -567,12 +571,15 @@ void Abc_NtkPrintFanioNew( FILE * pFile, Abc_Ntk_t * pNtk )
     // count the number of fanins and fanouts
     Abc_NtkForEachNode( pNtk, pNode, i )
     {
+        if ( fMffc && Abc_ObjFanoutNum(pNode) == 1 )
+            continue;
         nFanins  = Abc_ObjFaninNum(pNode);
         if ( Abc_NtkIsNetlist(pNtk) )
             nFanouts = Abc_ObjFanoutNum( Abc_ObjFanout0(pNode) );
+        else if ( fMffc )
+            nFanouts = Abc_NodeMffcSize(pNode);
         else
             nFanouts = Abc_ObjFanoutNum(pNode);
-//            nFanouts = Abc_NodeMffcSize(pNode);
 
         if ( nFanins < 10 )
             Vec_IntAddToEntry( vFanins, nFanins, 1 );