Experiments with don't-cares.

3 files changed, 196 insertions, 60 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 01bffece..4b03cf87 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -5777,6 +5777,7 @@ int Abc_CommandMfse( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -1, "Command is only applicable to LUT size no more than 6.\n" );
         return 1;
     }
+    Abc_NtkToSop( pNtk, -1, ABC_INFINITY );
     pNtkNew = Abc_NtkOptMfse( pNtk, pPars );
     if ( pNtkNew == NULL )
     {
diff --git a/src/base/acb/acbAbc.c b/src/base/acb/acbAbc.c
index 9be3bdab..dd97816c 100644
--- a/src/base/acb/acbAbc.c
+++ b/src/base/acb/acbAbc.c
@@ -209,11 +209,11 @@ void Acb_ParSetDefault( Acb_Par_t * pPars )
 {
     memset( pPars, 0, sizeof(Acb_Par_t) );
     pPars->nLutSize     =    4;    // LUT size
-    pPars->nTfoLevMax   =    1;    // the maximum fanout levels
+    pPars->nTfoLevMax   =    2;    // the maximum fanout levels
     pPars->nTfiLevMax   =    2;    // the maximum fanin levels
-    pPars->nFanoutMax   =   10;    // the maximum number of fanouts
-    pPars->nDivMax      =   16;    // the maximum divisor count
-    pPars->nTabooMax    =    4;    // the minimum MFFC size
+    pPars->nFanoutMax   =   20;    // the maximum number of fanouts
+    pPars->nDivMax      =   24;    // the maximum divisor count
+    pPars->nTabooMax    =    1;    // the minimum MFFC size
     pPars->nGrowthLevel =    0;    // the maximum allowed growth in level
     pPars->nBTLimit     =    0;    // the maximum number of conflicts in one SAT run
     pPars->nNodesMax    =    0;    // the maximum number of nodes to try
diff --git a/src/base/acb/acbMfs.c b/src/base/acb/acbMfs.c
index a536a08b..f13ab9f5 100644
--- a/src/base/acb/acbMfs.c
+++ b/src/base/acb/acbMfs.c
@@ -255,11 +255,10 @@ Cnf_Dat_t * Acb_NtkWindow2Cnf( Acb_Ntk_t * p, Vec_Int_t * vWinObjs, int Pivot )
   SeeAlso     []
 
 ***********************************************************************/
-sat_solver * Acb_NtkWindow2Solver( Cnf_Dat_t * pCnf, int PivotVar, int nDivs, int nTimes )
+int Acb_NtkWindow2Solver( sat_solver * pSat, Cnf_Dat_t * pCnf, int PivotVar, int nDivs, int nTimes )
 {
     int n, i, RetValue, nRounds = nTimes <= 2 ? nTimes-1 : 2;
     Vec_Int_t * vFlips = Cnf_DataCollectFlipLits( pCnf, PivotVar );
-    sat_solver * pSat = sat_solver_new(); 
     sat_solver_setnvars( pSat, nTimes * pCnf->nVars + nRounds * nDivs + 1 );
     assert( nTimes == 1 || nTimes == 2 || nTimes == 6 );
     for ( n = 0; n < nTimes; n++ )
@@ -272,7 +271,7 @@ sat_solver * Acb_NtkWindow2Solver( Cnf_Dat_t * pCnf, int PivotVar, int nDivs, in
             {
                 Vec_IntFree( vFlips );
                 sat_solver_delete( pSat );
-                return NULL;
+                return 0;
             }
         }
         if ( n & 1 )
@@ -297,9 +296,9 @@ sat_solver * Acb_NtkWindow2Solver( Cnf_Dat_t * pCnf, int PivotVar, int nDivs, in
     if ( RetValue == 0 )
     {
         sat_solver_delete( pSat );
-        return NULL;    
+        return 0;    
     }
-    return pSat;
+    return 1;
 }
 
 
@@ -324,6 +323,22 @@ void Acb_NtkPrintVec( Acb_Ntk_t * p, Vec_Int_t * vVec, char * pName )
         printf( "%d ", Vec_IntEntry(&p->vArray2, vVec->pArray[i]) );
     printf( "\n" );
 }
+void Acb_NtkPrintNode( Acb_Ntk_t * p, int Node )
+{
+    int k, iFanin, * pFanins;
+    printf( "Node %d : ", Vec_IntEntry(&p->vArray2, Node) );
+    Acb_ObjForEachFaninFast( p, Node, pFanins, iFanin, k )
+        printf( "%d ", Vec_IntEntry(&p->vArray2, iFanin) );
+    printf( "\n" );
+}
+void Acb_NtkPrintVec2( Acb_Ntk_t * p, Vec_Int_t * vVec, char * pName )
+{
+    int i;
+    printf( "%s: \n", pName );
+    for ( i = 0; i < vVec->nSize; i++ )
+        Acb_NtkPrintNode( p, vVec->pArray[i] );
+    printf( "\n" );
+}
 
 /**Function*************************************************************
 
@@ -400,16 +415,15 @@ Vec_Int_t * Acb_NtkDivisors( Acb_Ntk_t * p, int Pivot, int * pTaboo, int nTaboo,
   SeeAlso     []
 
 ***********************************************************************/
-void Acb_ObjMarkTfo_rec( Acb_Ntk_t * p, int iObj, int Pivot, int nTfoLevMax, int nFanMax )
+void Acb_ObjMarkTfo_rec( Acb_Ntk_t * p, int iObj, int nTfoLevMax, int nFanMax )
 {
     int iFanout, i;
     if ( Acb_ObjSetTravIdCur(p, iObj) )
         return;
-//printf( "Labeling %d.\n", Vec_IntEntry(&p->vArray2, iObj) );
-    if ( Acb_ObjLevelD(p, iObj) > nTfoLevMax || Acb_ObjFanoutNum(p, iObj) > nFanMax || iObj == Pivot )
+    if ( Acb_ObjLevelD(p, iObj) > nTfoLevMax || Acb_ObjFanoutNum(p, iObj) > nFanMax )
         return;
     Acb_ObjForEachFanout( p, iObj, iFanout, i )
-        Acb_ObjMarkTfo_rec( p, iFanout, Pivot, nTfoLevMax, nFanMax );
+        Acb_ObjMarkTfo_rec( p, iFanout, nTfoLevMax, nFanMax );
 }
 void Acb_ObjMarkTfo( Acb_Ntk_t * p, Vec_Int_t * vDivs, int Pivot, int nTfoLevMax, int nFanMax )
 {
@@ -417,7 +431,7 @@ void Acb_ObjMarkTfo( Acb_Ntk_t * p, Vec_Int_t * vDivs, int Pivot, int nTfoLevMax
     Acb_NtkIncTravId( p );
     Acb_ObjSetTravIdCur( p, Pivot );
     Vec_IntForEachEntry( vDivs, iObj, i )
-        Acb_ObjMarkTfo_rec( p, iObj, Pivot, nTfoLevMax, nFanMax );
+        Acb_ObjMarkTfo_rec( p, iObj, nTfoLevMax, nFanMax );
 }
 
 /**Function*************************************************************
@@ -767,7 +781,7 @@ static inline void Acb_ObjUpdateFanoutCount( Acb_Ntk_t * p, int iObj, int AddOn
         Acb_ObjFanoutVec(p, iFanin)->nSize += AddOn;
 }
 
-int Acb_NtkCollectTaboo( Acb_Ntk_t * p, int Pivot, int nTabooMax, int * pTaboo )
+int Acb_NtkCollectTaboo( Acb_Ntk_t * p, int Pivot, int Next, int nTabooMax, int * pTaboo )
 {
     int i, k, iFanin, * pFanins, nTaboo = 0;
     if ( nTabooMax == 0 ) // delay optimization
@@ -780,9 +794,15 @@ int Acb_NtkCollectTaboo( Acb_Ntk_t * p, int Pivot, int nTabooMax, int * pTaboo )
     else // area optimization
     {
         // check if the node has any area critical fanins
+//        Acb_ObjForEachFaninFast( p, Pivot, pFanins, iFanin, k )
+//            if ( !Acb_ObjIsCi(p, iFanin) && Acb_ObjFanoutNum(p, iFanin) == 1 )
+//                break;
+        // collect this critical fanin
+        assert( Next > 0 && !Acb_ObjIsCio(p, Next) && Acb_ObjFanoutNum(p, Next) == 1 );
         Acb_ObjForEachFaninFast( p, Pivot, pFanins, iFanin, k )
-            if ( !Acb_ObjIsCi(p, iFanin) && Acb_ObjFanoutNum(p, iFanin) == 1 )
+            if ( iFanin == Next )
                 break;
+        assert( k < Acb_ObjFaninNum(p, Pivot) );
         if ( k < Acb_ObjFaninNum(p, Pivot) ) // there is fanin
         {
             // mark pivot
@@ -886,72 +906,169 @@ Vec_Int_t * Acb_NtkFindSupp( Acb_Ntk_t * p, sat_solver * pSat2, int nVars, int n
     return vSupp;
 }
 
-void Acb_NtkOptNode( Acb_Ntk_t * p, int Pivot, int nTabooMax, int nDivMax, int nTfoLevs, int nFanMax, int nLutSize, int fVerbose )
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+typedef struct Acb_Mfs_t_ Acb_Mfs_t;
+struct Acb_Mfs_t_
 {
-    Cnf_Dat_t * pCnf;
+    Acb_Ntk_t *     pNtk;        // network
+    Acb_Par_t *     pPars;       // parameters
+    sat_solver *    pSat[3];     // SAT solvers
+    int             nOvers;      // overflows
+    int             nNodes;      // nodes
+    int             nWins;       // windows
+    int             nWinsAll;    // windows
+    int             nDivsAll;    // windows
+    int             nChanges[3]; // changes
+    abctime         timeTotal;
+    abctime         timeCnf;
+    abctime         timeSol;
+    abctime         timeWin;
+    abctime         timeSat;
+    abctime         timeSatU;
+    abctime         timeSatS;
+};
+Acb_Mfs_t * Acb_MfsStart( Acb_Ntk_t * pNtk, Acb_Par_t * pPars )
+{
+    Acb_Mfs_t * p = ABC_CALLOC( Acb_Mfs_t, 1 );
+    p->pNtk       = pNtk;
+    p->pPars      = pPars;
+    p->timeTotal  = Abc_Clock();
+    p->pSat[0]    = sat_solver_new();
+    p->pSat[1]    = sat_solver_new();
+    p->pSat[2]    = sat_solver_new();
+    return p;
+}
+void Acb_MfsStop( Acb_Mfs_t * p )
+{
+    sat_solver_delete( p->pSat[0] );
+    sat_solver_delete( p->pSat[1] );
+    sat_solver_delete( p->pSat[2] );
+    ABC_FREE( p );
+}
+int Acb_NtkOptNode( Acb_Mfs_t * p, int Pivot, int Next )
+{
+    Cnf_Dat_t * pCnf; abctime clk;
     Vec_Int_t * vWin, * vSupp = NULL;
-    sat_solver * pSat1 = NULL, * pSat2 = NULL, * pSat3 = NULL;
-    int c, PivotVar, nDivs = 0; word uTruth;
-    int pTaboo[16], nTaboo = Acb_NtkCollectTaboo( p, Pivot, nTabooMax, pTaboo );
+    int c, PivotVar, nDivs = 0, RetValue = 0; word uTruth;
+    int pTaboo[16], nTaboo = Acb_NtkCollectTaboo( p->pNtk, Pivot, Next, p->pPars->nTabooMax, pTaboo );
     if ( nTaboo == 0 )
-        return;
-    assert( nTabooMax == 0 || nTaboo <= nTabooMax );
+        return RetValue;
+    p->nWins++;
+    assert( p->pPars->nTabooMax == 0 || nTaboo <= p->pPars->nTabooMax );
     assert( nTaboo <= 16 );
+    //printf( "Trying node %d with fanin %d\n", Pivot, Next );
 
     // compute divisors and window for this target node with these taboo nodes
-    vWin = Acb_NtkWindow( p, Pivot, pTaboo, nTaboo, nDivMax, nTfoLevs, nFanMax, &nDivs );
+    clk = Abc_Clock();
+    vWin = Acb_NtkWindow( p->pNtk, Pivot, pTaboo, nTaboo, p->pPars->nDivMax, p->pPars->nTfoLevMax, p->pPars->nFanoutMax, &nDivs );
+    p->nWinsAll += Vec_IntSize(vWin);
+    p->nDivsAll += nDivs;
+    p->timeWin  += Abc_Clock() - clk;
     PivotVar = Vec_IntFind( vWin, Abc_Var2Lit(Pivot, 0) );
-    if ( fVerbose )
-    printf( "Node %d: Window contains %d objects and %d divisors.  ", Vec_IntEntry(&p->vArray2, Pivot), Vec_IntSize(vWin), nDivs );
+    if ( p->pPars->fVerbose )
+    printf( "Node %d: Window contains %d objects and %d divisors.  ", Vec_IntEntry(&p->pNtk->vArray2, Pivot), Vec_IntSize(vWin), nDivs );
 //    Acb_WinPrint( p, vWin, Pivot, nDivs );
 //    return;
+    if ( nDivs >= 2 * p->pPars->nDivMax )
+    {
+        p->nOvers++;
+        if ( p->pPars->fVerbose )
+            printf( "Too many divisors.\n" );
+        Vec_IntFree( vWin );
+        return RetValue;
+    }
 
-    // derive CNF and SAT solvers
-    pCnf  = Acb_NtkWindow2Cnf( p, vWin, Pivot );
-    pSat1 = Acb_NtkWindow2Solver( pCnf, PivotVar, nDivs, 1 );
+    // derive CNF 
+    clk = Abc_Clock();
+    pCnf  = Acb_NtkWindow2Cnf( p->pNtk, vWin, Pivot );
+    p->timeCnf += Abc_Clock() - clk;
+    // derive SAT solver
+    clk = Abc_Clock();
+    Acb_NtkWindow2Solver( p->pSat[0], pCnf, PivotVar, nDivs, 1 );
+    p->timeSol += Abc_Clock() - clk;
     // check constants
     for ( c = 0; c < 2; c++ )
     {
         int Lit = Abc_Var2Lit( PivotVar, c );
-        int status = sat_solver_solve( pSat1, &Lit, &Lit + 1, 0, 0, 0, 0 );
+        int status = sat_solver_solve( p->pSat[0], &Lit, &Lit + 1, 0, 0, 0, 0 );
         if ( status == l_False )
         {
-            if ( fVerbose )
+            p->nChanges[0]++;
+            if ( p->pPars->fVerbose )
             printf( "Found constant %d.\n", c );
-            Acb_NtkUpdateNode( p, Pivot, c ? ~(word)0 : 0, NULL );
+            Acb_NtkUpdateNode( p->pNtk, Pivot, c ? ~(word)0 : 0, NULL );
+            RetValue = 1;
             goto cleanup;
         }
         assert( status == l_True );
     }
 
+    // derive SAT solver
+    clk = Abc_Clock();
+    Acb_NtkWindow2Solver( p->pSat[1], pCnf, PivotVar, nDivs, 2 );
+    p->timeSol += Abc_Clock() - clk;
     // check for one-node implementation
-    pSat2 = Acb_NtkWindow2Solver( pCnf, PivotVar, nDivs, 2 );
-    vSupp = Acb_NtkFindSupp( p, pSat2, pCnf->nVars, nDivs );
-    if ( Vec_IntSize(vSupp) <= nLutSize )
+    clk = Abc_Clock();
+    vSupp = Acb_NtkFindSupp( p->pNtk, p->pSat[1], pCnf->nVars, nDivs );
+    p->timeSat += Abc_Clock() - clk;
+    if ( Vec_IntSize(vSupp) <= p->pPars->nLutSize )
     {
-        if ( fVerbose )
+        p->nChanges[1]++;
+        if ( p->pPars->fVerbose )
         printf( "Found %d inputs: ", Vec_IntSize(vSupp) );
-        uTruth = Acb_ComputeFunction( pSat1, PivotVar, sat_solver_nvars(pSat1)-1, vSupp );
-        if ( fVerbose )
+        uTruth = Acb_ComputeFunction( p->pSat[1], PivotVar, sat_solver_nvars(p->pSat[1])-1, vSupp );
+        if ( p->pPars->fVerbose )
         Extra_PrintHex( stdout, (unsigned *)&uTruth, Vec_IntSize(vSupp) ); 
-        if ( fVerbose )
+        if ( p->pPars->fVerbose )
         printf( "\n" );
         // create support in terms of nodes
         Vec_IntRemap( vSupp, vWin );
         Vec_IntLits2Vars( vSupp, 0 );
-        Acb_NtkUpdateNode( p, Pivot, uTruth, vSupp );
+        Acb_NtkUpdateNode( p->pNtk, Pivot, uTruth, vSupp );
+        RetValue = 1;
         goto cleanup;
     }
-    if ( fVerbose )
+    if ( p->pPars->fVerbose )
     printf( "\n" );
 
 cleanup:
-    if ( pSat1 ) sat_solver_delete( pSat1 );
-    if ( pSat2 ) sat_solver_delete( pSat2 );
-    if ( pSat3 ) sat_solver_delete( pSat3 );
+    sat_solver_restart( p->pSat[0] );
+    sat_solver_restart( p->pSat[1] );
+    sat_solver_restart( p->pSat[2] );
     Cnf_DataFree( pCnf );
     Vec_IntFree( vWin );
     Vec_IntFreeP( &vSupp );
+    return RetValue;
+}
+void Acb_NtkOptNodeTop( Acb_Mfs_t * p, int Pivot )
+{
+    if ( p->pPars->fArea )
+    {
+        p->nNodes++;
+        while ( 1 )
+        {
+            int k, iFanin, * pFanins;
+            Acb_ObjForEachFaninFast( p->pNtk, Pivot, pFanins, iFanin, k )
+                if ( !Acb_ObjIsCi(p->pNtk, iFanin) && Acb_ObjFanoutNum(p->pNtk, iFanin) == 1 && Acb_NtkOptNode(p, Pivot, iFanin) )
+                    break;
+            if ( k == Acb_ObjFaninNum(p->pNtk, Pivot) ) // no change
+                break;
+        }
+    }
+    else
+    {
+        assert( 0 );
+    }
 }
 
 
@@ -966,36 +1083,54 @@ cleanup:
   SeeAlso     []
 
 ***********************************************************************/
-void Acb_NtkOpt( Acb_Ntk_t * p, Acb_Par_t * pPars )
-{
-    if ( pPars->fVerbose )
-        printf( "Performing %s-oriented optimization with DivMax = %d. TfoLev = %d. LutSize = %d.\n", 
-            pPars->fArea ? "area" : "delay", pPars->nDivMax, pPars->nTfoLevMax, pPars->nLutSize );
-    Acb_NtkCreateFanout( p );  // fanout data structure
-    Acb_NtkCleanObjFuncs( p ); // SAT variables
-    Acb_NtkCleanObjCnfs( p );  // CNF representations
-    if ( pPars->fArea )
+void Acb_NtkOpt( Acb_Ntk_t * pNtk, Acb_Par_t * pPars )
+{
+    Acb_Mfs_t * pMan = Acb_MfsStart( pNtk, pPars );
+    //if ( pPars->fVerbose )
+        printf( "%s-optimization parameters: TabooMax(M) = %d  DivMax(D) = %d  TfoLev(O) = %d  LutSize = %d\n", 
+            pMan->pPars->fArea ? "Area" : "Delay", pMan->pPars->nTabooMax, pMan->pPars->nDivMax, pMan->pPars->nTfoLevMax, pMan->pPars->nLutSize );
+    Acb_NtkCreateFanout( pMan->pNtk );  // fanout data structure
+    Acb_NtkCleanObjFuncs( pMan->pNtk ); // SAT variables
+    Acb_NtkCleanObjCnfs( pMan->pNtk );  // CNF representations
+    if ( pMan->pPars->fArea )
     {
         int iObj;
-        Acb_NtkUpdateLevelD( p, -1 ); // compute forward logic level
-        Acb_NtkForEachNode( p, iObj )
+        Acb_NtkUpdateLevelD( pMan->pNtk, -1 ); // compute forward logic level
+        Acb_NtkForEachNode( pMan->pNtk, iObj )
         {
             //if ( iObj != 433 )
             //    continue;
-            Acb_NtkOptNode( p, iObj, pPars->nTabooMax, pPars->nDivMax, pPars->nTfoLevMax, pPars->nFanoutMax, pPars->nLutSize, pPars->fVerbose );
+            Acb_NtkOptNodeTop( pMan, iObj );
         }
     }
     else
     {
-        Acb_NtkUpdateTiming( p, -1 ); // compute delay information
-        while ( Vec_QueTopPriority(p->vQue) > 0 )
+        Acb_NtkUpdateTiming( pMan->pNtk, -1 ); // compute delay information
+        while ( Vec_QueTopPriority(pMan->pNtk->vQue) > 0 )
         {
-            int iObj = Vec_QuePop(p->vQue);
+            int iObj = Vec_QuePop(pMan->pNtk->vQue);
             //if ( iObj != 28 )
             //    continue;
-            Acb_NtkOptNode( p, iObj, 0, pPars->nDivMax, pPars->nTfoLevMax, pPars->nFanoutMax, pPars->nLutSize, pPars->fVerbose ); 
+            Acb_NtkOptNodeTop( pMan, iObj ); 
         }
     }
+    //if ( pPars->fVerbose )
+    {
+        pMan->timeTotal = Abc_Clock() - pMan->timeTotal;
+        printf( "Node = %d  Win = %d (Ave = %d)  DivAve = %d   Change = %d  Const = %d  Node1 = %d  Node2 = %d   Over = %d\n", 
+            pMan->nNodes, pMan->nWins, pMan->nWinsAll/Abc_MaxInt(1, pMan->nWins), pMan->nDivsAll/Abc_MaxInt(1, pMan->nWins),
+            pMan->nChanges[0] + pMan->nChanges[1] + pMan->nChanges[2],
+            pMan->nChanges[0], pMan->nChanges[1], pMan->nChanges[2], pMan->nOvers );
+        ABC_PRTP( "Windowing  ", pMan->timeWin,    pMan->timeTotal );
+        ABC_PRTP( "CNF compute", pMan->timeCnf,    pMan->timeTotal );
+        ABC_PRTP( "Make solver", pMan->timeSol,    pMan->timeTotal );
+        ABC_PRTP( "SAT solving", pMan->timeSat,    pMan->timeTotal );
+//        ABC_PRTP( "  unsat    ", pMan->timeSatU,   pMan->timeTotal );
+//        ABC_PRTP( "  sat      ", pMan->timeSatS,   pMan->timeTotal );
+        ABC_PRTP( "TOTAL      ", pMan->timeTotal,  pMan->timeTotal );
+        fflush( stdout );
+    }
+    Acb_MfsStop( pMan );
 }
 
 ////////////////////////////////////////////////////////////////////////