Experiments with precomputation and matching.

abclib.dsp

@@ -2539,6 +2539,10 @@ SOURCE=.\src\opt\sfm\sfmSat.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\opt\sfm\sfmTime.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\opt\sfm\sfmWin.c
 # End Source File
 # End Group

src/base/abci/abc.c

@@ -5160,7 +5160,7 @@ int Abc_CommandMfs3( Abc_Frame_t * pAbc, int argc, char ** argv )
     // set defaults
     Sfm_ParSetDefault3( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "OIFLHDMCNPdazospvwh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "OIFLHDMCNPdamzospvwh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -5280,6 +5280,9 @@ int Abc_CommandMfs3( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'a':
             pPars->fArea ^= 1;
             break;
+        case 'm':
+            pPars->fUseAndOr ^= 1;
+            break;
         case 'z':
             pPars->fZeroCost ^= 1;
             break;
@@ -5319,7 +5322,7 @@ int Abc_CommandMfs3( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: mfs3 [-OIFLHDMCNP <num>] [-azospvwh]\n" );
+    Abc_Print( -2, "usage: mfs3 [-OIFLHDMCNP <num>] [-amzospvwh]\n" );
     Abc_Print( -2, "\t           performs don't-care-based optimization of mapped networks\n" );
     Abc_Print( -2, "\t-O <num> : the number of levels in the TFO cone (0 <= num) [default = %d]\n",             pPars->nTfoLevMax );
     Abc_Print( -2, "\t-I <num> : the number of levels in the TFI cone (1 <= num) [default = %d]\n",             pPars->nTfiLevMax );
@@ -5331,7 +5334,8 @@ usage:
     Abc_Print( -2, "\t-C <num> : the max number of conflicts in one SAT run (0 = no limit) [default = %d]\n",   pPars->nBTLimit );
     Abc_Print( -2, "\t-N <num> : the max number of nodes to try (0 = all) [default = %d]\n",                    pPars->nNodesMax );
     Abc_Print( -2, "\t-P <num> : one particular node to try (0 = none) [default = %d]\n",                       pPars->iNodeOne );
-    Abc_Print( -2, "\t-a       : toggle minimizing area or area+edges [default = %s]\n",                        pPars->fArea? "area": "area+edges" );
+    Abc_Print( -2, "\t-a       : toggle area minimization [default = %s]\n",                                    pPars->fArea? "yes": "no" );
+    Abc_Print( -2, "\t-m       : toggle detecting multi-input AND/OR gates [default = %s]\n",                   pPars->fUseAndOr? "yes": "no" );
     Abc_Print( -2, "\t-z       : toggle zero-cost replacements [default = %s]\n",                               pPars->fZeroCost? "yes": "no" );
     Abc_Print( -2, "\t-o       : toggle using old implementation for comparison [default = %s]\n",              pPars->fRrOnly? "yes": "no" );
     Abc_Print( -2, "\t-s       : toggle using simulation [default = %s]\n",                                     pPars->fUseSim? "yes": "no" );
@@ -11030,7 +11034,7 @@ int Abc_CommandTestColor( Abc_Frame_t * pAbc, int argc, char ** argv )
 ***********************************************************************/
 int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-//    Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
+    Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
     int nCutMax      =  1;
     int nLeafMax     =  4;
     int nDivMax      =  2;
@@ -11237,6 +11241,8 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
     {
 //        extern void Cba_PrsReadBlifTest();
 //        Cba_PrsReadBlifTest();
+        extern void Sfm_TimTest( Abc_Ntk_t * pNtk );
+        Sfm_TimTest( pNtk );
     }
     return 0;
 usage:

src/opt/sfm/module.make

@@ -4,4 +4,5 @@ SRC +=    src/opt/sfm/sfmCnf.c \
     src/opt/sfm/sfmLib.c \
     src/opt/sfm/sfmNtk.c \
     src/opt/sfm/sfmSat.c \
+    src/opt/sfm/sfmTime.c \
     src/opt/sfm/sfmWin.c

src/opt/sfm/sfm.h

@@ -58,6 +58,7 @@ struct Sfm_Par_t_
     int             fRrOnly;       // perform redundance removal
     int             fArea;         // performs optimization for area
     int             fMoreEffort;   // performs high-affort minimization
+    int             fUseAndOr;     // enable internal detection of AND/OR gates
     int             fZeroCost;     // enable zero-cost replacement
     int             fUseSim;       // enable simulation
     int             fPrintDecs;    // enable printing decompositions

src/opt/sfm/sfmDec.c

@@ -147,6 +147,9 @@ void Sfm_ParSetDefault3( Sfm_Par_t * pPars )
     pPars->nWinSizeMax  =  300;  // the maximum window size
     pPars->nGrowthLevel =    0;  // the maximum allowed growth in level
     pPars->nBTLimit     = 5000;  // the maximum number of conflicts in one SAT run
+    pPars->fUseAndOr    =    0;  // enable internal detection of AND/OR gates
+    pPars->fZeroCost    =    0;  // enable zero-cost replacement
+    pPars->fUseSim      =    0;  // enable simulation
     pPars->fArea        =    0;  // performs optimization for area
     pPars->fVerbose     =    0;  // enable basic stats
     pPars->fVeryVerbose =    0;  // enable detailed stats
@@ -900,8 +903,9 @@ int Sfm_DecPeformDec_rec( Sfm_Dec_t * p, word * pTruth, int * pSupp, int * pAssu
             printf( "Found variable %s%d.\n", Abc_LitIsCompl(Impls[0]) ? "!":"", pSupp[0] );
         return 1;        
     }
-/*
+
     // try using all implications at once
+    if ( p->pPars->fUseAndOr )
     for ( c = 0; c < 2; c++ )
     {
         if ( Vec_IntSize(&p->vImpls[!c]) < 2 )
@@ -965,7 +969,7 @@ int Sfm_DecPeformDec_rec( Sfm_Dec_t * p, word * pTruth, int * pSupp, int * pAssu
                 *Vec_WrdEntryP(&p->vSets[c], i) |= ((word)1 << p->nPats[c]);
         p->uMask[c] |= ((word)1 << p->nPats[c]++);
     }
-*/
+
     // find the best cofactoring variable
     Var = -1, CostMin = ABC_INFINITY;
     for ( c = 0; c < 2; c++ )