Changes to LUT mappers.

1 files changed, 87 insertions, 11 deletions

diff --git a/src/map/if/ifSat.c b/src/map/if/ifSat.c
index 3fec34e0..cfce7369 100644
--- a/src/map/if/ifSat.c
+++ b/src/map/if/ifSat.c
@@ -42,7 +42,7 @@ ABC_NAMESPACE_IMPL_START
   SeeAlso     []
 
 ***********************************************************************/
-sat_solver * If_ManSatBuildXY( int nLutSize )
+void * If_ManSatBuildXY( int nLutSize )
 {
     int nMintsL = (1 << nLutSize);
     int nMintsF = (1 << (2 * nLutSize - 1));
@@ -59,6 +59,54 @@ sat_solver * If_ManSatBuildXY( int nLutSize )
 
 /**Function*************************************************************
 
+  Synopsis    [Verification for 6-input function.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static word If_ManSat6ComposeLut4( int t, word f[4], int k )
+{
+    int m, v, nMints = (1 << k);
+    word c, r = 0;
+    assert( k <= 4 );
+    for ( m = 0; m < nMints; m++ )
+    {
+        if ( !((t >> m) & 1) )
+            continue;
+        c = ~(word)0;
+        for ( v = 0; v < k; v++ )
+            c &= ((m >> v) & 1) ? f[v] : ~f[v];
+        r |= c;
+    }
+    return r;
+}
+word If_ManSat6Truth( word uBound, word uFree, int * pBSet, int nBSet, int * pSSet, int nSSet, int * pFSet, int nFSet )
+{
+    word r, q, f[4];
+    int i, k = 0;
+    // bound set vars
+    for ( i = 0; i < nSSet; i++ )
+        f[k++] = s_Truths6[pSSet[i]];
+    for ( i = 0; i < nBSet; i++ )
+        f[k++] = s_Truths6[pBSet[i]];
+    q = If_ManSat6ComposeLut4( (int)(uBound & 0xffff), f, k );
+    // free set vars
+    k = 0;
+    f[k++] = q;
+    for ( i = 0; i < nSSet; i++ )
+        f[k++] = s_Truths6[pSSet[i]];
+    for ( i = 0; i < nFSet; i++ )
+        f[k++] = s_Truths6[pFSet[i]];
+    r = If_ManSat6ComposeLut4( (int)(uFree & 0xffff), f, k );
+    return r;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Returns config string for the given truth table.]
 
   Description []
@@ -68,14 +116,16 @@ sat_solver * If_ManSatBuildXY( int nLutSize )
   SeeAlso     []
 
 ***********************************************************************/
-int If_ManSatCheckXY( sat_solver * p, int nLutSize, word * pTruth, int nVars, unsigned uSet, word * pTBound, word * pTFree, Vec_Int_t * vLits )
+int If_ManSatCheckXY( void * pSat, int nLutSize, word * pTruth, int nVars, unsigned uSet, word * pTBound, word * pTFree, Vec_Int_t * vLits )
 {
-    int iBSet, nBSet = 0;
-    int iSSet, nSSet = 0;
-    int iFSet, nFSet = 0;
+    sat_solver * p = (sat_solver *)pSat;
+    int iBSet, nBSet = 0, pBSet[IF_MAX_FUNC_LUTSIZE];
+    int iSSet, nSSet = 0, pSSet[IF_MAX_FUNC_LUTSIZE];
+    int iFSet, nFSet = 0, pFSet[IF_MAX_FUNC_LUTSIZE];
     int nMintsL = (1 << nLutSize);
     int nMintsF = (1 << (2 * nLutSize - 1));
     int v, Value, m, mNew, nMintsFNew, nMintsLNew;
+    word Res;
     // collect variable sets
     Dau_DecSortSet( uSet, nVars, &nBSet, &nSSet, &nFSet );
     assert( nBSet + nSSet + nFSet == nVars );
@@ -94,13 +144,13 @@ int If_ManSatCheckXY( sat_solver * p, int nLutSize, word * pTruth, int nVars, un
             if ( Value == 0 ) // FS
             {
                 if ( ((m >> v) & 1) )
-                    mNew |= 1 << (nLutSize + nSSet + iFSet);
+                    mNew |= 1 << (nLutSize + nSSet + iFSet), pFSet[iFSet] = v;
                 iFSet++;
             }
             else if ( Value == 1 ) // BS
             {
                 if ( ((m >> v) & 1) )
-                    mNew |= 1 << (nSSet + iBSet);
+                    mNew |= 1 << (nSSet + iBSet), pBSet[iBSet] = v;
                 iBSet++;
             }
             else if ( Value == 3 ) // SS
@@ -109,6 +159,7 @@ int If_ManSatCheckXY( sat_solver * p, int nLutSize, word * pTruth, int nVars, un
                 {
                     mNew |= 1 << iSSet;
                     mNew |= 1 << (nLutSize + iSSet);
+                    pSSet[iSSet] = v;
                 }
                 iSSet++;
             }
@@ -143,11 +194,36 @@ int If_ManSatCheckXY( sat_solver * p, int nLutSize, word * pTruth, int nVars, un
     // collect configs
     assert( nSSet + nFSet + 1 <= nLutSize );
     *pTFree = 0;
-    nMintsLNew = (1 << (nSSet + nFSet + 1));
+    nMintsLNew = (1 << (1 + nSSet + nFSet));
     for ( m = 0; m < nMintsLNew; m++ )
         if ( sat_solver_var_value(p, nMintsL+m) )
             Abc_TtSetBit( pTFree, m );
-    *pTFree = Abc_Tt6Stretch( *pTFree, nSSet + nFSet + 1 );
+    *pTFree = Abc_Tt6Stretch( *pTFree, 1 + nSSet + nFSet );
+    if ( nVars != 6 )
+        return 1;
+    // verify the result
+    Res = If_ManSat6Truth( *pTBound, *pTFree, pBSet, nBSet, pSSet, nSSet, pFSet, nFSet );
+    if ( pTruth[0] != Res )
+    {
+        Dau_DsdPrintFromTruth( pTruth,  nVars );
+        Dau_DsdPrintFromTruth( &Res,    nVars );
+        Dau_DsdPrintFromTruth( pTBound, nSSet+nBSet );
+        Dau_DsdPrintFromTruth( pTFree,  nSSet+nFSet+1 );
+        printf( "Verification failed!\n" );
+    }
+/*
+    else
+    {
+//        Kit_DsdPrintFromTruth( (unsigned*)pTBound, nSSet+nBSet   ); printf( "\n" );
+//        Kit_DsdPrintFromTruth( (unsigned*)pTFree,  nSSet+nFSet+1 ); printf( "\n" );
+
+        Dau_DsdPrintFromTruth( pTruth,  nVars );
+        Dau_DsdPrintFromTruth( &Res,    nVars );
+        Dau_DsdPrintFromTruth( pTBound, nSSet+nBSet   );
+        Dau_DsdPrintFromTruth( pTFree,  nSSet+nFSet+1 );
+        printf( "Verification OK!\n" );
+    }
+*/
     return 1;
 }
 
@@ -166,7 +242,7 @@ void If_ManSatTest2()
 {
     int nVars = 6;
     int nLutSize = 4;
-    sat_solver * p = If_ManSatBuildXY( nLutSize );
+    sat_solver * p = (sat_solver *)If_ManSatBuildXY( nLutSize );
 //    char * pDsd = "(abcdefg)";
 //    char * pDsd = "([a!bc]d!e)";
     char * pDsd = "0123456789ABCDEF{abcdef}";
@@ -194,7 +270,7 @@ void If_ManSatTest()
 {
     int nVars = 4;
     int nLutSize = 3;
-    sat_solver * p = If_ManSatBuildXY( nLutSize );
+    sat_solver * p = (sat_solver *)If_ManSatBuildXY( nLutSize );
     word t = 0x183C, * pTruth = &t;
     word uBound, uFree;
     unsigned uSet;