Changes to LUT mappers.

3 files changed, 264 insertions, 8 deletions

diff --git a/src/map/if/if.h b/src/map/if/if.h
index 8af5cff3..8693e74e 100644
--- a/src/map/if/if.h
+++ b/src/map/if/if.h
@@ -520,6 +520,7 @@ extern int             If_CluCheckExt3( void * p, word * pTruth, int nVars, int
 extern If_DsdMan_t *   If_DsdManAlloc( int nVars, int nLutSize );
 extern void            If_DsdManDump( If_DsdMan_t * p );
 extern void            If_DsdManPrint( If_DsdMan_t * p, char * pFileName, int fVerbose );
+extern void            If_DsdManTune( If_DsdMan_t * p, int LutSize, int fFast, int fSpec, int fVerbose );
 extern void            If_DsdManFree( If_DsdMan_t * p, int fVerbose );
 extern void            If_DsdManSave( If_DsdMan_t * p, char * pFileName );
 extern If_DsdMan_t *   If_DsdManLoad( char * pFileName );
@@ -574,10 +575,12 @@ extern int             If_ManPerformMappingRound( If_Man_t * p, int nCutsUsed, i
 extern void            If_ManImproveMapping( If_Man_t * p );
 /*=== ifSat.c ==========================================================*/
 extern void *          If_ManSatBuildXY( int nLutSize );
+extern void *          If_ManSatBuild55();
 extern void *          If_ManSatBuildXYZ( int nLutSize );
 extern void            If_ManSatUnbuild( void * p );
 extern int             If_ManSatCheckXY( void * pSat, int nLutSize, word * pTruth, int nVars, unsigned uSet, word * pTBound, word * pTFree, Vec_Int_t * vLits );
 extern unsigned        If_ManSatCheckXYall( void * pSat, int nLutSize, word * pTruth, int nVars, Vec_Int_t * vLits );
+extern unsigned        If_ManSatCheck55all( void * pSat, word * pTruth, int nVars, Vec_Int_t * vLits );
 /*=== ifSeq.c =============================================================*/
 extern int             If_ManPerformMappingSeq( If_Man_t * p );
 /*=== ifTime.c ============================================================*/
diff --git a/src/map/if/ifDsd.c b/src/map/if/ifDsd.c
index 5222c376..e1a4f2b5 100644
--- a/src/map/if/ifDsd.c
+++ b/src/map/if/ifDsd.c
@@ -20,6 +20,7 @@
 
 #include "if.h"
 #include "misc/extra/extra.h"
+#include "sat/bsat/satSolver.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -102,6 +103,7 @@ static inline void          If_DsdVecObjIncRef( Vec_Ptr_t * p, int iObj )
 static inline If_DsdObj_t * If_DsdObjFanin( Vec_Ptr_t * p, If_DsdObj_t * pObj, int i ) { assert(i < (int)pObj->nFans); return If_DsdVecObj(p, Abc_Lit2Var(pObj->pFans[i])); }
 static inline int           If_DsdVecObjMark( Vec_Ptr_t * p, int iObj )                { return If_DsdVecObj( p, iObj )->fMark;                                             }
 static inline void          If_DsdVecObjSetMark( Vec_Ptr_t * p, int iObj )             { If_DsdVecObj( p, iObj )->fMark = 1;                                                }
+static inline void          If_DsdVecObjClearMark( Vec_Ptr_t * p, int iObj )           { If_DsdVecObj( p, iObj )->fMark = 0;                                                }
 
 #define If_DsdVecForEachObj( vVec, pObj, i )                \
     Vec_PtrForEachEntry( If_DsdObj_t *, vVec, pObj, i )
@@ -365,10 +367,39 @@ void If_DsdManPrintOne( FILE * pFile, If_DsdMan_t * p, int iObjId, unsigned char
         fprintf( pFile, "\n" );
     assert( nSupp == If_DsdVecObjSuppSize(p->vObjs, iObjId) );
 }
+void If_DsdManPrintDistrib( If_DsdMan_t * p )
+{
+    If_DsdObj_t * pObj;
+    int CountAll[IF_MAX_FUNC_LUTSIZE] = {0};
+    int CountNon[IF_MAX_FUNC_LUTSIZE] = {0};
+    int i, nVars, CountNonTotal = 0;
+    If_DsdVecForEachObj( p->vObjs, pObj, i )
+    {
+        nVars = If_DsdObjSuppSize(pObj);
+        CountAll[nVars]++;
+        if ( !If_DsdVecObjMark(p->vObjs, i) )
+            continue;
+        CountNon[nVars]++;
+        CountNonTotal++;
+    }
+    for ( i = 0; i <= p->nVars; i++ )
+    {
+        printf( "%3d :  ", i );
+        printf( "All = %8d  ", CountAll[i] );
+        printf( "Non = %8d ",  CountNon[i] );
+        printf( "(%6.2f %%)",  100.0 * CountNon[i] / CountAll[i] );
+        printf( "\n" );
+    }
+    printf( "All :  " );
+    printf( "All = %8d  ", Vec_PtrSize(p->vObjs) );
+    printf( "Non = %8d ",  CountNonTotal );
+    printf( "(%6.2f %%)",  100.0 * CountNonTotal / Vec_PtrSize(p->vObjs) );
+    printf( "\n" );
+}
 void If_DsdManPrint( If_DsdMan_t * p, char * pFileName, int fVerbose )
 {
     If_DsdObj_t * pObj;
-    int i, DsdMax = 0, CountUsed = 0, CountNonDsdStr = 0;
+    int i, DsdMax = 0, CountUsed = 0, CountNonDsdStr = 0, CountMarked = 0;
     FILE * pFile;
     pFile = pFileName ? fopen( pFileName, "wb" ) : stdout;
     if ( pFileName && pFile == NULL )
@@ -382,9 +413,11 @@ void If_DsdManPrint( If_DsdMan_t * p, char * pFileName, int fVerbose )
             DsdMax = Abc_MaxInt( DsdMax, pObj->nFans ); 
         CountNonDsdStr += If_DsdManCheckNonDec_rec( p, pObj->Id );
         CountUsed += ( If_DsdVecObjRef(p->vObjs, pObj->Id) > 0 );
+        CountMarked += If_DsdVecObjMark( p->vObjs, i );
     }
     fprintf( pFile, "Total number of objects    = %8d\n", Vec_PtrSize(p->vObjs) );
     fprintf( pFile, "Externally used objects    = %8d\n", CountUsed );
+    fprintf( pFile, "Marked objects             = %8d\n", CountMarked );
     fprintf( pFile, "Non-DSD objects (max =%2d)  = %8d\n", DsdMax, Vec_MemEntryNum(p->vTtMem) );
     fprintf( pFile, "Non-DSD structures         = %8d\n", CountNonDsdStr );
     fprintf( pFile, "Unique table hits          = %8d\n", p->nUniqueHits );
@@ -392,11 +425,15 @@ void If_DsdManPrint( If_DsdMan_t * p, char * pFileName, int fVerbose )
     fprintf( pFile, "Memory used for objects    = %8.2f MB.\n", 1.0*Mem_FlexReadMemUsage(p->pMem)/(1<<20) );
     fprintf( pFile, "Memory used for hash table = %8.2f MB.\n", 1.0*sizeof(int)*p->nBins/(1<<20) );
     fprintf( pFile, "Memory used for array      = %8.2f MB.\n", 1.0*sizeof(void *)*Vec_PtrCap(p->vObjs)/(1<<20) );
-    Abc_PrintTime( 1, "Time DSD   ", p->timeDsd    );
-    Abc_PrintTime( 1, "Time canon ", p->timeCanon-p->timeCheck  );
-    Abc_PrintTime( 1, "Time check ", p->timeCheck  );
-    Abc_PrintTime( 1, "Time check2", p->timeCheck2 );
-    Abc_PrintTime( 1, "Time verify", p->timeVerify );
+    If_DsdManPrintDistrib( p );
+    if ( p->timeDsd )
+    {
+        Abc_PrintTime( 1, "Time DSD   ", p->timeDsd    );
+        Abc_PrintTime( 1, "Time canon ", p->timeCanon-p->timeCheck  );
+        Abc_PrintTime( 1, "Time check ", p->timeCheck  );
+        Abc_PrintTime( 1, "Time check2", p->timeCheck2 );
+        Abc_PrintTime( 1, "Time verify", p->timeVerify );
+    }
 //    If_DsdManHashProfile( p );
 //    If_DsdManDump( p );
 //    If_DsdManDumpAll( p );
@@ -1442,6 +1479,84 @@ void If_DsdManTest()
     Vec_IntFree( vSets );
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void If_DsdManTune( If_DsdMan_t * p, int LutSize, int fFast, int fSpec, int fVerbose )
+{
+    ProgressBar * pProgress = NULL;
+    If_DsdObj_t * pObj;
+    sat_solver * pSat = NULL;
+    sat_solver * pSat5 = NULL;
+    Vec_Int_t * vLits = Vec_IntAlloc( 1000 );
+    int i, Value, nVars;
+    word * pTruth;
+    pSat = (sat_solver *)If_ManSatBuildXY( LutSize );
+    if ( LutSize == 5 && fSpec )
+        pSat5 = (sat_solver *)If_ManSatBuild55();
+    If_DsdVecForEachObj( p->vObjs, pObj, i )
+        pObj->fMark = 0;
+    pProgress = Extra_ProgressBarStart( stdout, Vec_PtrSize(p->vObjs) );
+    If_DsdVecForEachObj( p->vObjs, pObj, i )
+    {
+        Extra_ProgressBarUpdate( pProgress, i, NULL );
+        nVars = If_DsdObjSuppSize(pObj);
+        if ( nVars <= LutSize )
+            continue;
+        if ( LutSize == 5 && fSpec )
+        {
+            if ( nVars == 9 )
+            {
+                pTruth = If_DsdManComputeTruth( p, Abc_Var2Lit(i, 0), NULL );
+                Value = If_ManSatCheck55all( pSat5, pTruth, nVars, vLits );
+            }
+            else
+            {
+                if ( If_DsdManCheckXY(p, Abc_Var2Lit(i, 0), LutSize, 0, 0) )
+                    continue;
+                if ( fFast )
+                    Value = 0;
+                else
+                {
+                    pTruth = If_DsdManComputeTruth( p, Abc_Var2Lit(i, 0), NULL );
+                    Value = If_ManSatCheckXYall( pSat, LutSize, pTruth, nVars, vLits );
+                }
+            }
+        }
+        else
+        {
+            if ( If_DsdManCheckXY(p, Abc_Var2Lit(i, 0), LutSize, 0, 0) )
+                continue;
+            if ( fFast )
+                Value = 0;
+            else
+            {
+                pTruth = If_DsdManComputeTruth( p, Abc_Var2Lit(i, 0), NULL );
+                Value = If_ManSatCheckXYall( pSat, LutSize, pTruth, nVars, vLits );
+            }
+        }
+        if ( Value )
+            continue;
+        If_DsdVecObjSetMark( p->vObjs, i );
+    }
+    if ( pProgress )
+        Extra_ProgressBarStop( pProgress );
+    If_ManSatUnbuild( pSat5 );
+    If_ManSatUnbuild( pSat );
+    Vec_IntFree( vLits );
+    if ( fVerbose )
+        If_DsdManPrintDistrib( p );
+}
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/map/if/ifSat.c b/src/map/if/ifSat.c
index a0fc5737..9f4ea631 100644
--- a/src/map/if/ifSat.c
+++ b/src/map/if/ifSat.c
@@ -268,6 +268,128 @@ int If_ManSatCheckXY( void * pSat, int nLutSize, word * pTruth, int nVars, unsig
     }
     return 1;
 }
+int If_ManSatCheck55( void * pSat, word * pTruth, int nVars, int * pPerm9, word * pTBound, word * pTFree, Vec_Int_t * vLits )
+{
+    sat_solver * p = (sat_solver *)pSat;
+    int v, Value, m, mNew;
+    int nMintsL = 16;
+    // remap minterms
+    Vec_IntFill( vLits, 512, -1 );
+    for ( m = 0; m < (1 << nVars); m++ )
+    {
+        mNew = 0;
+        for ( v = 0; v < 9; v++ )
+        {
+            assert( pPerm9[v] < nVars );
+            if ( ((m >> pPerm9[v]) & 1) )
+                mNew |= (1 << v);
+        }
+        assert( Vec_IntEntry(vLits, mNew) == -1 );
+        Vec_IntWriteEntry( vLits, mNew, Abc_TtGetBit(pTruth, m) );
+    }
+    // find assumptions
+    v = 0;
+    Vec_IntForEachEntry( vLits, Value, m )
+        if ( Value >= 0 )
+            Vec_IntWriteEntry( vLits, v++, Abc_Var2Lit(2 * nMintsL + m, !Value) );
+    Vec_IntShrink( vLits, v );
+    // run SAT solver
+    Value = sat_solver_solve( p, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), 0, 0, 0, 0 );
+    if ( Value != l_True )
+        return 0;
+    if ( pTBound && pTFree )
+    {
+        // collect config
+        *pTBound = 0;
+        for ( m = 0; m < nMintsL; m++ )
+            if ( sat_solver_var_value(p, m) )
+                Abc_TtSetBit( pTBound, m );
+        *pTBound = Abc_Tt6Stretch( *pTBound, 4 );
+        // collect configs
+        *pTFree = 0;
+        for ( m = 0; m < nMintsL; m++ )
+            if ( sat_solver_var_value(p, nMintsL+m) )
+                Abc_TtSetBit( pTFree, m );
+        *pTFree = Abc_Tt6Stretch( *pTFree, 4 );
+    }
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns config string for the given truth table.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+unsigned If_ManSatCheck55all_int( void * pSat, word * pTruth, int nVars, Vec_Int_t * vLits )
+{
+    int Combs[10][5] = {
+        {0,1,2,3,4}, 
+        {0,2,1,3,4}, 
+        {0,3,1,2,4}, 
+        {0,4,1,2,3}, 
+        {1,2,0,3,4}, 
+        {1,3,0,2,4}, 
+        {1,4,0,2,3}, 
+        {2,3,0,1,4}, 
+        {2,4,0,1,3}, 
+        {3,4,0,1,2}
+    };
+    int pPerm9[9], Mark[9], i[6], k, n, c;
+    assert( nVars == 9 || nVars == 8 || nVars == 7 );
+    for ( i[0] = 0;      i[0] < nVars; i[0]++ )
+    for ( i[1] = i[0]+1; i[1] < nVars; i[1]++ )
+    for ( i[2] = i[1]+1; i[2] < nVars; i[2]++ )
+    for ( i[3] = i[2]+1; i[3] < nVars; i[3]++ )
+    for ( i[4] = i[3]+1; i[4] < nVars; i[4]++ )
+    {
+        // add remaining ones
+        n = 5;
+        for ( k = 0; k < nVars; k++ )
+            Mark[k] = 0;
+        for ( k = 0; k < 5; k++ )
+            Mark[i[k]] = 1;
+        for ( k = 0; k < nVars; k++ )
+            if ( Mark[k] == 0 )
+                pPerm9[n++] = k;
+        assert( n == nVars );
+        for ( ; n < 9; n++ )
+            pPerm9[n] = pPerm9[n-1];
+        assert( n == 9 );
+        // current ones
+        for ( c = 0; c < 10; c++ )
+        {
+            for ( n = 0; n < 5; n++ )
+                pPerm9[n] = i[Combs[c][n]];
+            // try different combinations
+            for ( k = 5; k < nVars; k++ )
+            {
+                ABC_SWAP( int, pPerm9[5], pPerm9[k] );
+                if ( If_ManSatCheck55(pSat, pTruth, nVars, pPerm9, NULL, NULL, vLits) )
+                {
+//                    for ( k = 0; k < 9; k++ )
+//                        printf( "%c", 'a' + pPerm9[k] );
+//                    printf( "\n" );
+                    return 1;
+                }
+                ABC_SWAP( int, pPerm9[5], pPerm9[k] );
+            }
+        }
+    }
+    return 0;
+}
+unsigned If_ManSatCheck55all( void * pSat, word * pTruth, int nVars, Vec_Int_t * vLits )
+{
+//    abctime clk = Abc_Clock();
+    unsigned Value = If_ManSatCheck55all_int( pSat, pTruth, nVars, vLits );
+//    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+    return Value;
+}
 
 /**Function*************************************************************
 
@@ -408,6 +530,7 @@ unsigned If_ManSatCheckXYall_int( void * pSat, int nLutSize, word * pTruth, int
         for ( i[3] = i[2]+1; i[3] < nVars; i[3]++ )
         for ( i[4] = i[3]+1; i[4] < nVars; i[4]++ )
         {
+            uSet = (1 << (2*i[0])) | (1 << (2*i[1])) | (1 << (2*i[2])) | (1 << (2*i[3])) | (1 << (2*i[4]));
             for ( s[0] = 0;      s[0] < nLutSize; s[0]++ )
             for ( s[1] = s[0]+1; s[1] < nLutSize; s[1]++ )
             for ( s[2] = s[1]+1; s[2] < nLutSize; s[2]++ )
@@ -538,8 +661,7 @@ void If_ManSatTest2()
     sat_solver_delete(p);
     Vec_IntFree( vLits );
 }
-
-void If_ManSatTest()
+void If_ManSatTest3()
 {
     int nVars = 6;
     int nLutSize = 4;
@@ -558,6 +680,22 @@ void If_ManSatTest()
     sat_solver_delete(p);
     Vec_IntFree( vLits );
 }
+void If_ManSatTest()
+{
+    int nVars = 9;
+    sat_solver * p = (sat_solver *)If_ManSatBuild55();
+//    char * pDsd = "[([(ab)cde]f)ghi]";
+//    char * pDsd = "[([(hi)cde]f)gab]";
+    char * pDsd = "[(0123{(hi)cde}f)gab]";
+    word * pTruth = Dau_DsdToTruth( pDsd, nVars );
+    Vec_Int_t * vLits = Vec_IntAlloc( 1000 );
+    if ( If_ManSatCheck55all( p, pTruth, nVars, vLits ) )
+        printf( "Found!\n" );
+    else
+        printf( "Not found!\n" );
+    sat_solver_delete(p);
+    Vec_IntFree( vLits );
+}
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///