Changes to LUT mappers.

3 files changed, 148 insertions, 44 deletions

diff --git a/src/map/if/if.h b/src/map/if/if.h
index c8b04ef1..cf26c53c 100644
--- a/src/map/if/if.h
+++ b/src/map/if/if.h
@@ -572,6 +572,9 @@ extern void            If_ObjPerformMappingChoice( If_Man_t * p, If_Obj_t * pObj
 extern int             If_ManPerformMappingRound( If_Man_t * p, int nCutsUsed, int Mode, int fPreprocess, int fFirst, char * pLabel );
 /*=== ifReduce.c ==========================================================*/
 extern void            If_ManImproveMapping( If_Man_t * p );
+/*=== ifSat.c ==========================================================*/
+extern void *          If_ManSatBuildXY( int nLutSize );
+extern int             If_ManSatCheckXY( void * pSat, int nLutSize, word * pTruth, int nVars, unsigned uSet, word * pTBound, word * pTFree, 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 af586ce2..63341ad3 100644
--- a/src/map/if/ifDsd.c
+++ b/src/map/if/ifDsd.c
@@ -62,7 +62,8 @@ struct If_DsdMan_t_
     Mem_Flex_t *   pMem;           // memory for nodes
     Vec_Ptr_t *    vObjs;          // objects
     Vec_Int_t *    vNexts;         // next pointers
-    Vec_Int_t *    vNodes;         // temp
+    Vec_Int_t *    vTemp1;         // temp
+    Vec_Int_t *    vTemp2;         // temp
     word **        pTtElems;       // elementary TTs
     Vec_Mem_t *    vTtMem;         // truth table memory and hash table
     Vec_Ptr_t *    vTtDecs;        // truth table decompositions
@@ -198,7 +199,8 @@ If_DsdMan_t * If_DsdManAlloc( int nVars, int LutSize )
     p->vNexts  = Vec_IntAlloc( 10000 );
     If_DsdObjAlloc( p, IF_DSD_CONST0, 0 );
     If_DsdObjAlloc( p, IF_DSD_VAR, 0 )->nSupp = 1;
-    p->vNodes   = Vec_IntAlloc( 32 );
+    p->vTemp1   = Vec_IntAlloc( 32 );
+    p->vTemp2   = Vec_IntAlloc( 32 );
     p->pTtElems = If_ManDsdTtElems();
     p->vTtDecs  = Vec_PtrAlloc( 1000 );
     p->vTtMem   = Vec_MemAlloc( Abc_TtWordNum(nVars), 12 );
@@ -227,7 +229,8 @@ void If_DsdManFree( If_DsdMan_t * p, int fVerbose )
     Vec_VecFree( (Vec_Vec_t *)p->vTtDecs );
     Vec_MemHashFree( p->vTtMem );
     Vec_MemFreeP( &p->vTtMem );
-    Vec_IntFreeP( &p->vNodes );
+    Vec_IntFreeP( &p->vTemp1 );
+    Vec_IntFreeP( &p->vTemp2 );
     Vec_IntFreeP( &p->vNexts );
     Vec_PtrFreeP( &p->vObjs );
     Mem_FlexStop( p->pMem, 0 );
@@ -662,20 +665,29 @@ If_DsdMan_t * If_DsdManLoad( char * pFileName )
   SeeAlso     []
 
 ***********************************************************************/
-void If_DsdManCollect_rec( If_DsdMan_t * p, int Id, Vec_Int_t * vNodes )
+void If_DsdManCollect_rec( If_DsdMan_t * p, int Id, Vec_Int_t * vNodes, Vec_Int_t * vFirsts, int * pnSupp )
 {
-    int i, iFanin;
+    int i, iFanin, iFirst;
     If_DsdObj_t * pObj = If_DsdVecObj( p->vObjs, Id );
-    if ( If_DsdObjType(pObj) == IF_DSD_CONST0 || If_DsdObjType(pObj) == IF_DSD_VAR )
+    if ( If_DsdObjType(pObj) == IF_DSD_CONST0 )
+        return;
+    if ( If_DsdObjType(pObj) == IF_DSD_VAR )
+    {
+        (*pnSupp)++;
         return;
+    }
+    iFirst = *pnSupp;
     If_DsdObjForEachFaninLit( p->vObjs, pObj, iFanin, i )
-        If_DsdManCollect_rec( p, Abc_Lit2Var(iFanin), vNodes );
+        If_DsdManCollect_rec( p, Abc_Lit2Var(iFanin), vNodes, vFirsts, pnSupp );
     Vec_IntPush( vNodes, Id );
+    Vec_IntPush( vFirsts, iFirst );
 }
-void If_DsdManCollect( If_DsdMan_t * p, int Id, Vec_Int_t * vNodes )
+void If_DsdManCollect( If_DsdMan_t * p, int Id, Vec_Int_t * vNodes, Vec_Int_t * vFirsts )
 {
+    int nSupp = 0;
     Vec_IntClear( vNodes );
-    If_DsdManCollect_rec( p, Id, vNodes );
+    Vec_IntClear( vFirsts );
+    If_DsdManCollect_rec( p, Id, vNodes, vFirsts, &nSupp );
 }
 
 /**Function*************************************************************
@@ -1129,7 +1141,7 @@ void If_DsdManGetSuppSizes( If_DsdMan_t * p, If_DsdObj_t * pObj, int * pSSizes )
         pSSizes[i] = If_DsdObjSuppSize(pFanin);    
 }
 // checks if there is a way to package some fanins 
-unsigned If_DsdManCheckAndXor( If_DsdMan_t * p, If_DsdObj_t * pObj, int nSuppAll, int LutSize, int fDerive, int fVerbose )
+unsigned If_DsdManCheckAndXor( If_DsdMan_t * p, int iFirst, If_DsdObj_t * pObj, int nSuppAll, int LutSize, int fDerive, int fVerbose )
 {
     int i[6], LimitOut, SizeIn, SizeOut, pSSizes[DAU_MAX_VAR];
     int nFans = If_DsdObjFaninNum(pObj), pFirsts[DAU_MAX_VAR];
@@ -1148,7 +1160,8 @@ unsigned If_DsdManCheckAndXor( If_DsdMan_t * p, If_DsdObj_t * pObj, int nSuppAll
         if ( !fDerive )
             return ~0;
         If_DsdManComputeFirst( p, pObj, pFirsts );
-        return If_DsdSign(p, pObj, i[0], pFirsts[i[0]], 0) | If_DsdSign(p, pObj, i[1], pFirsts[i[1]], 0);
+        return If_DsdSign(p, pObj, i[0], iFirst + pFirsts[i[0]], 0) | 
+               If_DsdSign(p, pObj, i[1], iFirst + pFirsts[i[1]], 0);
     }
     if ( pObj->nFans == 3 )
         return 0;
@@ -1163,7 +1176,9 @@ unsigned If_DsdManCheckAndXor( If_DsdMan_t * p, If_DsdObj_t * pObj, int nSuppAll
         if ( !fDerive )
             return ~0;
         If_DsdManComputeFirst( p, pObj, pFirsts );
-        return If_DsdSign(p, pObj, i[0], pFirsts[i[0]], 0) | If_DsdSign(p, pObj, i[1], pFirsts[i[1]], 0) | If_DsdSign(p, pObj, i[2], pFirsts[i[2]], 0);
+        return If_DsdSign(p, pObj, i[0], iFirst + pFirsts[i[0]], 0) | 
+               If_DsdSign(p, pObj, i[1], iFirst + pFirsts[i[1]], 0) | 
+               If_DsdSign(p, pObj, i[2], iFirst + pFirsts[i[2]], 0);
     }
     if ( pObj->nFans == 4 )
         return 0;
@@ -1179,12 +1194,15 @@ unsigned If_DsdManCheckAndXor( If_DsdMan_t * p, If_DsdObj_t * pObj, int nSuppAll
         if ( !fDerive )
             return ~0;
         If_DsdManComputeFirst( p, pObj, pFirsts );
-        return If_DsdSign(p, pObj, i[0], pFirsts[i[0]], 0) | If_DsdSign(p, pObj, i[1], pFirsts[i[1]], 0) | If_DsdSign(p, pObj, i[2], pFirsts[i[2]], 0) | If_DsdSign(p, pObj, i[3], pFirsts[i[3]], 0);
+        return If_DsdSign(p, pObj, i[0], iFirst + pFirsts[i[0]], 0) | 
+               If_DsdSign(p, pObj, i[1], iFirst + pFirsts[i[1]], 0) | 
+               If_DsdSign(p, pObj, i[2], iFirst + pFirsts[i[2]], 0) | 
+               If_DsdSign(p, pObj, i[3], iFirst + pFirsts[i[3]], 0);
     }
     return 0;
 }
 // checks if there is a way to package some fanins 
-unsigned If_DsdManCheckMux( If_DsdMan_t * p, If_DsdObj_t * pObj, int nSuppAll, int LutSize, int fDerive, int fVerbose )
+unsigned If_DsdManCheckMux( If_DsdMan_t * p, int iFirst, If_DsdObj_t * pObj, int nSuppAll, int LutSize, int fDerive, int fVerbose )
 {
     int LimitOut, SizeIn, SizeOut, pSSizes[DAU_MAX_VAR], pFirsts[DAU_MAX_VAR];
     assert( If_DsdObjFaninNum(pObj) == 3 );
@@ -1194,28 +1212,28 @@ unsigned If_DsdManCheckMux( If_DsdMan_t * p, If_DsdObj_t * pObj, int nSuppAll, i
     assert( LimitOut < LutSize );
     // first input
     SizeIn = pSSizes[0] + pSSizes[1];
-    SizeOut = pSSizes[2];
+    SizeOut = pSSizes[0] + pSSizes[2] + 1;
     if ( SizeIn <= LutSize && SizeOut <= LimitOut )
     {
         if ( !fDerive )
             return ~0;
         If_DsdManComputeFirst( p, pObj, pFirsts );
-        return If_DsdSign(p, pObj, 0, pFirsts[0], 1) | If_DsdSign(p, pObj, 1, pFirsts[1], 0);
+        return If_DsdSign(p, pObj, 0, iFirst + pFirsts[0], 1) | If_DsdSign(p, pObj, 1, iFirst + pFirsts[1], 0);
     }
     // second input
     SizeIn = pSSizes[0] + pSSizes[2];
-    SizeOut = pSSizes[1];
+    SizeOut = pSSizes[0] + pSSizes[1] + 1;
     if ( SizeIn <= LutSize && SizeOut <= LimitOut )
     {
         if ( !fDerive )
             return ~0;
         If_DsdManComputeFirst( p, pObj, pFirsts );
-        return If_DsdSign(p, pObj, 0, pFirsts[0], 1) | If_DsdSign(p, pObj, 2, pFirsts[2], 0);
+        return If_DsdSign(p, pObj, 0, iFirst + pFirsts[0], 1) | If_DsdSign(p, pObj, 2, iFirst + pFirsts[2], 0);
     }
     return 0;
 }
 // checks if there is a way to package some fanins 
-unsigned If_DsdManCheckPrime( If_DsdMan_t * p, If_DsdObj_t * pObj, int nSuppAll, int LutSize, int fDerive, int fVerbose )
+unsigned If_DsdManCheckPrime( If_DsdMan_t * p, int iFirst, If_DsdObj_t * pObj, int nSuppAll, int LutSize, int fDerive, int fVerbose )
 {
     int i, v, set, LimitOut, SizeIn, SizeOut, pSSizes[DAU_MAX_VAR], pFirsts[DAU_MAX_VAR];
     int truthId = If_DsdObjTruthId( p, pObj );
@@ -1245,7 +1263,7 @@ Dau_DecPrintSets( vSets, nFans );
                 SizeIn += pSSizes[v];
                 SizeOut += pSSizes[v];
             }
-            else assert( Value == 0 );
+            else assert( 0 );
             if ( SizeIn > LutSize || SizeOut > LimitOut )
                 break;
         }
@@ -1262,10 +1280,10 @@ Dau_DecPrintSets( vSets, nFans );
                 if ( Value == 0 )
                 {}
                 else if ( Value == 1 )
-                    uSign |= If_DsdSign(p, pObj, v, pFirsts[v], 0);
+                    uSign |= If_DsdSign(p, pObj, v, iFirst + pFirsts[v], 0);
                 else if ( Value == 3 )
-                    uSign |= If_DsdSign(p, pObj, v, pFirsts[v], 1);
-                else assert( Value == 0 );
+                    uSign |= If_DsdSign(p, pObj, v, iFirst + pFirsts[v], 1);
+                else assert( 0 );
             }
             return uSign;
         }
@@ -1274,7 +1292,13 @@ Dau_DecPrintSets( vSets, nFans );
 }
 unsigned If_DsdManCheckXY( If_DsdMan_t * p, int iDsd, int LutSize, int fDerive, int fVerbose )
 {
-    If_DsdObj_t * pObj, * pTemp; int i, Mask;
+    If_DsdObj_t * pObj, * pTemp; 
+    int i, Mask, iFirst;
+    if ( 193 == iDsd )
+    {
+        int s = 0;
+        If_DsdManPrintOne( stdout, p, Abc_Lit2Var(iDsd), NULL, 1 );
+    }
     pObj = If_DsdVecObj( p->vObjs, Abc_Lit2Var(iDsd) );
     if ( fVerbose )
     If_DsdManPrintOne( stdout, p, Abc_Lit2Var(iDsd), NULL, 0 );
@@ -1284,20 +1308,21 @@ unsigned If_DsdManCheckXY( If_DsdMan_t * p, int iDsd, int LutSize, int fDerive,
         printf( "    Trivial\n" );
         return ~0;
     }
-    If_DsdManCollect( p, pObj->Id, p->vNodes );
-    If_DsdVecForEachObjVec( p->vNodes, p->vObjs, pTemp, i )
+    If_DsdManCollect( p, pObj->Id, p->vTemp1, p->vTemp2 );
+    If_DsdVecForEachObjVec( p->vTemp1, p->vObjs, pTemp, i )
         if ( If_DsdObjSuppSize(pTemp) <= LutSize && If_DsdObjSuppSize(pObj) - If_DsdObjSuppSize(pTemp) <= LutSize - 1 )
         {
             if ( fVerbose )
             printf( "    Dec using node " );
             if ( fVerbose )
             If_DsdManPrintOne( stdout, p, pTemp->Id, NULL, 1 );
-            return ~0;
+            iFirst = Vec_IntEntry(p->vTemp2, i);
+            return If_DsdSign_rec(p, pTemp, &iFirst);
         }
-    If_DsdVecForEachObjVec( p->vNodes, p->vObjs, pTemp, i )
+    If_DsdVecForEachObjVec( p->vTemp1, p->vObjs, pTemp, i )
         if ( (If_DsdObjType(pTemp) == IF_DSD_AND || If_DsdObjType(pTemp) == IF_DSD_XOR) && If_DsdObjFaninNum(pTemp) > 2 && If_DsdObjSuppSize(pTemp) > LutSize )
         {
-            if ( (Mask = If_DsdManCheckAndXor(p, pTemp, If_DsdObjSuppSize(pObj), LutSize, fDerive, fVerbose)) )
+            if ( (Mask = If_DsdManCheckAndXor(p, Vec_IntEntry(p->vTemp2, i), pTemp, If_DsdObjSuppSize(pObj), LutSize, fDerive, fVerbose)) )
             {
                 if ( fVerbose )
                 printf( "    " );
@@ -1308,10 +1333,10 @@ unsigned If_DsdManCheckXY( If_DsdMan_t * p, int iDsd, int LutSize, int fDerive,
                 return Mask;
             }
         }
-    If_DsdVecForEachObjVec( p->vNodes, p->vObjs, pTemp, i )
+    If_DsdVecForEachObjVec( p->vTemp1, p->vObjs, pTemp, i )
         if ( If_DsdObjType(pTemp) == IF_DSD_MUX && If_DsdObjSuppSize(pTemp) > LutSize )
         {
-            if ( (Mask = If_DsdManCheckMux(p, pTemp, If_DsdObjSuppSize(pObj), LutSize, fDerive, fVerbose)) )
+            if ( (Mask = If_DsdManCheckMux(p, Vec_IntEntry(p->vTemp2, i), pTemp, If_DsdObjSuppSize(pObj), LutSize, fDerive, fVerbose)) )
             {
                 if ( fVerbose )
                 printf( "    " );
@@ -1322,10 +1347,10 @@ unsigned If_DsdManCheckXY( If_DsdMan_t * p, int iDsd, int LutSize, int fDerive,
                 return Mask;
             }
         }
-    If_DsdVecForEachObjVec( p->vNodes, p->vObjs, pTemp, i )
+    If_DsdVecForEachObjVec( p->vTemp1, p->vObjs, pTemp, i )
         if ( If_DsdObjType(pTemp) == IF_DSD_PRIME && If_DsdObjSuppSize(pTemp) > LutSize )
         {
-            if ( (Mask = If_DsdManCheckPrime(p, pTemp, If_DsdObjSuppSize(pObj), LutSize, fDerive, fVerbose)) )
+            if ( (Mask = If_DsdManCheckPrime(p, Vec_IntEntry(p->vTemp2, i), pTemp, If_DsdObjSuppSize(pObj), LutSize, fDerive, fVerbose)) )
             {
                 if ( fVerbose )
                 printf( "    " );
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;