New technology mapper.

src/base/abci/abc.c

@@ -29522,7 +29522,7 @@ int Abc_CommandAbc9If2( Abc_Frame_t * pAbc, int argc, char ** argv )
     // set defaults
     Mpm_ManSetParsDefault( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "KDtmzvwh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "KDtmzrcuvwh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -29532,8 +29532,8 @@ int Abc_CommandAbc9If2( Abc_Frame_t * pAbc, int argc, char ** argv )
                 Abc_Print( -1, "Command line switch \"-K\" should be followed by a positive integer.\n" );
                 goto usage;
             }
-            globalUtilOptind++;
             nLutSize = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
             if ( nLutSize < 2 || nLutSize > 16 )
             {
                 Abc_Print( -1, "LUT size %d is not supported.\n", nLutSize );
@@ -29562,6 +29562,15 @@ int Abc_CommandAbc9If2( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'z':
             pPars->fDeriveLuts ^= 1;
             break;
+        case 'r':
+            pPars->fOneRound ^= 1;
+            break;
+        case 'c':
+            pPars->fMap4Cnf ^= 1;
+            break;
+        case 'u':
+            pPars->fMap4Aig ^= 1;
+            break;
         case 'v':
             pPars->fVerbose ^= 1;
             break;
@@ -29575,6 +29584,8 @@ int Abc_CommandAbc9If2( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     if ( pPars->pLib == NULL )
         pPars->pLib = Mpm_LibLutSetSimple( nLutSize );
+    if ( pPars->fMap4Cnf )
+        pPars->fUseDsd = 1;
     if ( pPars->fCutMin )
 //        pPars->fUseTruth = 1;
         pPars->fUseDsd = 1;
@@ -29594,13 +29605,16 @@ usage:
         sprintf(Buffer, "best possible" );
     else
         sprintf(Buffer, "%d", pPars->DelayTarget );
-    Abc_Print( -2, "usage: &if2 [-KD num] [-tmzvwh]\n" );
+    Abc_Print( -2, "usage: &if2 [-KD num] [-tmzrcuvwh]\n" );
     Abc_Print( -2, "\t           performs technology mapping of the network\n" );
     Abc_Print( -2, "\t-K num   : sets the LUT size for the mapping [default = %d]\n", nLutSize );
     Abc_Print( -2, "\t-D num   : sets the delay constraint for the mapping [default = %s]\n", Buffer );
     Abc_Print( -2, "\t-t       : enables using AND/XOR/MUX nodes instead of simple AIG [default = %s]\n", pPars->fUseGates? "yes": "no" );
     Abc_Print( -2, "\t-m       : enables cut minimization by removing vacuous variables [default = %s]\n", pPars->fCutMin? "yes": "no" );
     Abc_Print( -2, "\t-z       : toggles deriving LUTs when mapping into LUT structures [default = %s]\n", pPars->fDeriveLuts? "yes": "no" );
+    Abc_Print( -2, "\t-r       : toggles using one round of mapping [default = %s]\n", pPars->fOneRound? "yes": "no" );
+    Abc_Print( -2, "\t-c       : toggles mapping for CNF computation [default = %s]\n", pPars->fMap4Cnf? "yes": "no" );
+    Abc_Print( -2, "\t-u       : toggles mapping for AIG computation [default = %s]\n", pPars->fMap4Aig? "yes": "no" );
     Abc_Print( -2, "\t-v       : toggles verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-w       : toggles very verbose output [default = %s]\n", pPars->fVeryVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h       : prints the command usage\n");

src/base/abci/abcDec.c

@@ -357,6 +357,7 @@ void Abc_TruthStoreRead( char * pFileName, Abc_TtStore_t * p )
 void Abc_TtStoreWrite( char * pFileName, Abc_TtStore_t * p, int fBinary )
 {
     FILE * pFile;
+    char pBuffer[1000];
     int i, nBytes = 8 * Abc_Truth6WordNum( p->nVars );
     pFile = fopen( pFileName, "wb" );
     if ( pFile == NULL )
@@ -369,7 +370,11 @@ void Abc_TtStoreWrite( char * pFileName, Abc_TtStore_t * p, int fBinary )
         if ( fBinary )
             fwrite( p->pFuncs[i], nBytes, 1, pFile );
         else
-            Abc_TruthWriteHex( pFile, p->pFuncs[i], p->nVars ), fprintf( pFile, "\n" );
+        {
+            Abc_TruthWriteHex( pFile, p->pFuncs[i], p->nVars ), fprintf( pFile, "    " );
+            Dau_DsdDecompose( p->pFuncs[i], p->nVars, 0, (int)(p->nVars <= 10), pBuffer );
+            fprintf( pFile, "%s\n", pBuffer );
+        }
     }
     fclose( pFile );
 }

src/map/mpm/mpm.h

@@ -63,7 +63,10 @@ struct Mpm_Par_t_
     int              fUseTruth;
     int              fUseDsd;
     int              fCutMin;
+    int              fOneRound;
     int              fDeriveLuts;
+    int              fMap4Cnf;
+    int              fMap4Aig;
     int              fVerbose;
     int              fVeryVerbose;
 };

src/map/mpm/mpmAbc.c

@@ -20,7 +20,6 @@
 
 #include "aig/gia/gia.h"
 #include "mpmInt.h"
-#include "misc/util/utilTruth.h"
 
 ABC_NAMESPACE_IMPL_START
 

src/map/mpm/mpmCore.c

@@ -51,8 +51,11 @@ void Mpm_ManSetParsDefault( Mpm_Par_t * p )
     p->fUseTruth      =      0;  // uses truth tables
     p->fUseDsd        =      0;  // uses DSDs
     p->fCutMin        =      0;  // enables cut minimization
+    p->fOneRound      =      0;  // enabled one round
     p->DelayTarget    =     -1;  // delay target
     p->fDeriveLuts    =      0;  // use truth tables to derive AIG structure
+    p->fMap4Cnf       =      0;  // mapping for CNF
+    p->fMap4Aig       =      0;  // mapping for AIG
     p->fVerbose       =      0;  // verbose output
     p->fVeryVerbose   =      0;  // verbose output
 }

src/map/mpm/mpmInt.h

@@ -32,10 +32,11 @@
 #include <assert.h>
 
 //#include "misc/tim/tim.h"
+#include "misc/mem/mem2.h"
 #include "misc/vec/vec.h"
 #include "misc/vec/vecMem.h"
 #include "misc/vec/vecHsh.h"
-#include "misc/mem/mem2.h"
+#include "misc/util/utilTruth.h"
 #include "mpmMig.h"
 #include "mpm.h"
 
@@ -83,6 +84,8 @@ typedef struct Mpm_Dsd_t_ Mpm_Dsd_t;
 struct Mpm_Dsd_t_
 {
     int              nVars;                    // support size
+    int              nAnds;                    // the number of AND gates
+    int              nClauses;                 // the number of CNF clauses
     word             uTruth;                   // truth table
     char *           pStr;                     // description 
 };
@@ -124,6 +127,10 @@ struct Mpm_Man_t_
     Vec_Mem_t *      vTtMem;                   // truth table memory and hash table
     int              funcCst0;                 // constant 0
     int              funcVar0;                 // variable 0
+    word             Truth0[1024];
+    word             Truth1[1024];
+    word             TruthC[1024];
+    word             Truth[1024];
     // DSD
     Mpm_Dsd_t *      pDsd6;                    // NPN class information
     Hsh_IntMan_t *   pHash;                    // maps DSD functions into NPN classes
@@ -242,7 +249,7 @@ extern void                  Mpm_CutPrint( Mpm_Cut_t * pCut );
 extern void                  Mpm_ManPrepare( Mpm_Man_t * p );
 extern void                  Mpm_ManPerform( Mpm_Man_t * p );
 /*=== mpmTruth.c ===========================================================*/
-extern int                   Mpm_CutComputeTruth6( Mpm_Man_t * p, Mpm_Cut_t * pCut, Mpm_Cut_t * pCut0, Mpm_Cut_t * pCut1, Mpm_Cut_t * pCutC, int fCompl0, int fCompl1, int fComplC, int Type );
+extern int                   Mpm_CutComputeTruth( Mpm_Man_t * p, Mpm_Cut_t * pCut, Mpm_Cut_t * pCut0, Mpm_Cut_t * pCut1, Mpm_Cut_t * pCutC, int fCompl0, int fCompl1, int fComplC, int Type );
 
 extern void                  Kit_DsdPrintFromTruth( unsigned * pTruth, int nVars );
 

src/map/mpm/mpmMan.c

@@ -48,6 +48,8 @@ Mpm_Man_t * Mpm_ManStart( Mig_Man_t * pMig, Mpm_Par_t * pPars )
     int i;
     assert( sizeof(Mpm_Uni_t) % sizeof(word) == 0 );      // aligned info to word boundary
     assert( pPars->nNumCuts <= MPM_CUT_MAX );
+    assert( !pPars->fUseTruth || pPars->pLib->LutMax <= 16 );
+    assert( !pPars->fUseDsd || pPars->pLib->LutMax <= 6 );
     Mig_ManSetRefs( pMig, 1 );
     // alloc
     p = ABC_CALLOC( Mpm_Man_t, 1 );
@@ -81,12 +83,11 @@ Mpm_Man_t * Mpm_ManStart( Mig_Man_t * pMig, Mpm_Par_t * pPars )
     assert( !p->pPars->fUseTruth || !p->pPars->fUseDsd );
     if ( p->pPars->fUseTruth )
     { 
-        word Truth = 0;
         p->vTtMem = Vec_MemAlloc( p->nTruWords, 12 ); // 32 KB/page for 6-var functions
         Vec_MemHashAlloc( p->vTtMem, 10000 );
-        p->funcCst0 = Vec_MemHashInsert( p->vTtMem, &Truth );
-        Truth = ABC_CONST(0xAAAAAAAAAAAAAAAA);
-        p->funcVar0 = Vec_MemHashInsert( p->vTtMem, &Truth );
+        p->funcCst0 = Vec_MemHashInsert( p->vTtMem, p->Truth );
+        Abc_TtUnit( p->Truth, p->nTruWords );
+        p->funcVar0 = Vec_MemHashInsert( p->vTtMem, p->Truth );
     }
     else if ( p->pPars->fUseDsd )
     {
@@ -112,6 +113,16 @@ Mpm_Man_t * Mpm_ManStart( Mig_Man_t * pMig, Mpm_Par_t * pPars )
 ***********************************************************************/
 void Mpm_ManStop( Mpm_Man_t * p )
 {
+    if ( p->pPars->fUseTruth )
+    {
+        char * pFileName = "truths.txt";
+        FILE * pFile = fopen( pFileName, "wb" );
+        Vec_MemDump( pFile, p->vTtMem );
+        fclose( pFile );
+        printf( "Dumpted %d %d-var truth tables into file \"%s\" (%.2f MB).\n", 
+            Vec_MemEntryNum(p->vTtMem), p->nLutSize, pFileName,
+            (16.0 * p->nTruWords + 1.0) * Vec_MemEntryNum(p->vTtMem) / (1 << 20) );
+    }
     if ( p->pPars->fUseDsd )
         Mpm_ManPrintDsdStats( p );
     if ( p->vTtMem ) 

src/map/mpm/mpmMap.c

@@ -19,7 +19,6 @@
 ***********************************************************************/
 
 #include "mpmInt.h"
-#include "misc/util/utilTruth.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -167,6 +166,14 @@ static inline int Mpm_ManSetIsBigger( Mpm_Man_t * p, Mpm_Cut_t * pCut, int nTota
   SeeAlso     []
 
 ***********************************************************************/
+static inline int Mpm_CutGetArea( Mpm_Man_t * p, Mpm_Cut_t * pCut )  
+{
+    if ( p->pPars->fMap4Cnf )
+        return MPM_UNIT_AREA * p->pDsd6[Abc_Lit2Var(pCut->iFunc)].nClauses;
+    if ( p->pPars->fMap4Aig )
+        return MPM_UNIT_AREA * p->pDsd6[Abc_Lit2Var(pCut->iFunc)].nAnds;
+    return p->pLibLut->pLutAreas[pCut->nLeaves];
+}
 static inline word Mpm_CutGetSign( Mpm_Cut_t * pCut )  
 {
     int i, iLeaf;
@@ -204,7 +211,7 @@ static inline Mpm_Uni_t * Mpm_CutSetupInfo( Mpm_Man_t * p, Mpm_Cut_t * pCut, int
     }
 
     pUnit->mTime    = ArrTime;
-    pUnit->mArea    = p->pLibLut->pLutAreas[pCut->nLeaves];
+    pUnit->mArea    = Mpm_CutGetArea( p, pCut );
     pUnit->mEdge    = MPM_UNIT_EDGE * pCut->nLeaves;
     pUnit->mAveRefs = 0;
     pUnit->Cost     = 0;
@@ -444,7 +451,7 @@ static inline void Mpm_ObjPrepareFanins( Mpm_Man_t * p, Mig_Obj_t * pObj )
 ***********************************************************************/
 static inline int Mpm_ObjDeriveCut( Mpm_Man_t * p, Mpm_Cut_t ** pCuts, Mpm_Cut_t * pCut )
 {
-    int i, c, iObj;
+    int i, c, iObj, fDisj = 1;
     // clean present objects
 //    Vec_IntForEachEntry( &p->vObjPresUsed, iObj, i )
 //        p->pObjPres[iObj] = (unsigned char)0xFF; 
@@ -488,6 +495,8 @@ static inline int Mpm_ObjDeriveCut( Mpm_Man_t * p, Mpm_Cut_t ** pCuts, Mpm_Cut_t
                 p->pObjPres[iObj] = pCut->nLeaves;        
                 pCut->pLeaves[pCut->nLeaves++] = pCuts[c]->pLeaves[i];
             }
+            else
+                fDisj = 0;
             p->uPermMask[c] ^= (((i & 7) ^ 7) << (3*p->pObjPres[iObj]));
             assert( Abc_Lit2Var(pCuts[c]->pLeaves[i]) == Abc_Lit2Var(pCut->pLeaves[p->pObjPres[iObj]]) );
             if ( pCuts[c]->pLeaves[i] != pCut->pLeaves[p->pObjPres[iObj]] )
@@ -495,6 +504,7 @@ static inline int Mpm_ObjDeriveCut( Mpm_Man_t * p, Mpm_Cut_t ** pCuts, Mpm_Cut_t
         }
 //        Mpm_ManPrintPerm( p->uPermMask[c] ); printf( "\n" );
     }
+//    printf( "%d", fDisj );
     pCut->hNext    = 0;
     pCut->iFunc    = 0;  pCut->iFunc = ~pCut->iFunc;
     pCut->fUseless = 0;
@@ -525,7 +535,7 @@ p->timeMerge += clock() - clk;
 
     // derive truth table
     if ( p->pPars->fUseTruth )
-        Mpm_CutComputeTruth6( p, pCut, pCuts[0], pCuts[1], pCuts[2], Mig_ObjFaninC0(pObj), Mig_ObjFaninC1(pObj), Mig_ObjFaninC2(pObj), Mig_ObjNodeType(pObj) ); 
+        Mpm_CutComputeTruth( p, pCut, pCuts[0], pCuts[1], pCuts[2], Mig_ObjFaninC0(pObj), Mig_ObjFaninC1(pObj), Mig_ObjFaninC2(pObj), Mig_ObjNodeType(pObj) ); 
     else if ( p->pPars->fUseDsd )
     {
         if ( !Mpm_CutComputeDsd6( p, pCut, pCuts[0], pCuts[1], pCuts[2], Mig_ObjFaninC0(pObj), Mig_ObjFaninC1(pObj), Mig_ObjFaninC2(pObj), Mig_ObjNodeType(pObj) ) )
@@ -694,6 +704,8 @@ static inline void Mpm_ManFinalizeRound( Mpm_Man_t * p )
     p->GloArea = 0;
     p->GloEdge = 0;
     p->GloRequired = Mpm_ManFindArrivalMax(p);
+    if ( p->pPars->DelayTarget != -1 )
+        p->GloRequired = Abc_MaxInt( p->GloRequired, p->pPars->DelayTarget );
     Mpm_ManCleanMapRefs( p );
     Mpm_ManCleanRequired( p );
     Mig_ManForEachObjReverse( p->pMig, pObj )
@@ -716,7 +728,7 @@ static inline void Mpm_ManFinalizeRound( Mpm_Man_t * p )
                     pRequired[iLeaf] = Abc_MinInt( pRequired[iLeaf], Required - pDelays[i] );
                     pMapRefs [iLeaf]++;
                 }
-                p->GloArea += p->pLibLut->pLutAreas[pCut->nLeaves];
+                p->GloArea += Mpm_CutGetArea( p, pCut );
                 p->GloEdge += pCut->nLeaves;
             }
         }
@@ -816,7 +828,7 @@ void Mpm_ManPerformRound( Mpm_Man_t * p )
     Mig_ManForEachNode( p->pMig, pObj )
         Mpm_ManDeriveCuts( p, pObj );
     Mpm_ManFinalizeRound( p );
-    printf( "Del =%5d.  Ar =%8d.  Edge =%8d.  Cut =%10d. Max =%10d.  Tru =%6d. Small =%5d. ", 
+    printf( "Del =%5d.  Ar =%8d.  Edge =%8d.  Cut =%10d. Max =%8d.  Tru =%8d. Small =%6d. ", 
         p->GloRequired, p->GloArea, p->GloEdge, 
         p->nCutsMerged, p->pManCuts->nEntriesMax, 
         p->vTtMem ? p->vTtMem->nEntries : 0, p->nSmallSupp );
@@ -824,8 +836,17 @@ void Mpm_ManPerformRound( Mpm_Man_t * p )
 }
 void Mpm_ManPerform( Mpm_Man_t * p )
 {
+    if ( p->pPars->fMap4Cnf )
+    {
+        p->pCutCmp = Mpm_CutCompareArea;
+        Mpm_ManPerformRound( p );   
+    }
+    else
+    {
         p->pCutCmp = Mpm_CutCompareDelay;
         Mpm_ManPerformRound( p );
+        if ( p->pPars->fOneRound )
+            return;
     
         p->pCutCmp = Mpm_CutCompareDelay2;
         Mpm_ManPerformRound( p );
@@ -842,6 +863,7 @@ void Mpm_ManPerform( Mpm_Man_t * p )
         p->pCutCmp = Mpm_CutCompareArea2;
         Mpm_ManComputeEstRefs( p );
         Mpm_ManPerformRound( p );
+    }
 }
 
 

src/map/mpm/mpmPre.c

@@ -26,6 +26,7 @@
 #include "misc/vec/vec.h"
 #include "misc/vec/vecHsh.h"
 #include "misc/extra/extra.h"
+#include "bool/kit/kit.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -37,7 +38,8 @@ ABC_NAMESPACE_IMPL_START
 typedef struct Ifd_Obj_t_ Ifd_Obj_t;
 struct Ifd_Obj_t_
 {
-    unsigned          nFreq : 24;   // frequency
+    unsigned          nFreq : 18;   // frequency
+    unsigned          nAnds :  6;   // number of AND gates
     unsigned          nSupp :  5;   // support size
     unsigned          Type  :  2;   // type
     unsigned          fWay  :  1;   // transparent edge
@@ -53,11 +55,10 @@ struct Ifd_Man_t_
     // hashing operations
     Vec_Int_t *       vArgs;     // iDsd1 op iDsdC
     Vec_Int_t *       vRes;      // result of operation
-    Vec_Int_t *       vOffs;     // offsets in the array of permutations
-    Vec_Str_t *       vPerms;    // storage for permutations
     Hsh_IntMan_t *    vHash;     // hash table 
     Vec_Int_t *       vMarks;    // marks where given N begins
     Vec_Wrd_t *       vTruths;   // truth tables
+    Vec_Int_t *       vClauses;  // truth tables
     // other data
     Vec_Int_t *       vSuper;
 
@@ -72,6 +73,7 @@ static inline Ifd_Obj_t * Ifd_ManObj( Ifd_Man_t * p, int i )           { assert(
 static inline Ifd_Obj_t * Ifd_ManObjFromLit( Ifd_Man_t * p, int iLit ) { return Ifd_ManObj( p, Abc_Lit2Var(iLit) );                                             }
 static inline int         Ifd_ObjId( Ifd_Man_t * p, Ifd_Obj_t * pObj ) { assert( pObj - p->pObjs >= 0 && pObj - p->pObjs < p->nObjs );  return pObj - p->pObjs; }
 static inline int         Ifd_LitSuppSize( Ifd_Man_t * p, int iLit )   { return iLit > 0 ? Ifd_ManObjFromLit(p, iLit)->nSupp : 0;                               }
+static inline int         Ifd_LitNumAnds( Ifd_Man_t * p, int iLit )    { return iLit > 0 ? Ifd_ManObjFromLit(p, iLit)->nAnds : 0;                               }
 
 #define Ifd_ManForEachNodeWithSupp( p, nVars, pLeaf, i )                       \
     for ( i = Vec_IntEntry(p->vMarks, nVars); (i < Vec_IntEntry(p->vMarks, nVars+1)) && (pLeaf = Ifd_ManObj(p, i)); i++ )
@@ -105,8 +107,6 @@ Ifd_Man_t * Ifd_ManStart()
     // hashing operations
     p->vArgs      = Vec_IntAlloc( 4000 );
     p->vRes       = Vec_IntAlloc( 1000 );
-//    p->vOffs      = Vec_IntAlloc( 1000 );
-//    p->vPerms     = Vec_StrAlloc( 1000 );
     p->vHash      = Hsh_IntManStart( p->vArgs, 4, 1000 );
     p->vMarks     = Vec_IntAlloc( 100 );
     Vec_IntPush( p->vMarks, 0 );
@@ -115,6 +115,7 @@ Ifd_Man_t * Ifd_ManStart()
     // other data
     p->vSuper     = Vec_IntAlloc( 1000 );
     p->vTruths    = Vec_WrdAlloc( 1000 );
+    p->vClauses   = Vec_IntAlloc( 1000 );
     return p;
 }
 void Ifd_ManStop( Ifd_Man_t * p )
@@ -129,9 +130,8 @@ void Ifd_ManStop( Ifd_Man_t * p )
 
     Vec_IntFreeP( &p->vArgs );
     Vec_IntFreeP( &p->vRes );
-//    Vec_IntFree( p->vOffs );
-//    Vec_StrFree( p->vPerms );
     Vec_WrdFreeP( &p->vTruths );
+    Vec_IntFreeP( &p->vClauses );
     Vec_IntFreeP( &p->vMarks );
     Hsh_IntManStop( p->vHash );
     Vec_IntFreeP( &p->vSuper );
@@ -193,7 +193,11 @@ void Ifd_ManPrint( Ifd_Man_t * p )
     for ( i = 0; i < p->nObjs; i++ )
     {
         word Fun = Vec_WrdEntry( p->vTruths, i );
-        printf( "    { %d, ABC_CONST(", Extra_TruthSupportSize((unsigned *)&Fun, 6) );
+        printf( "    { " );
+        printf( "%d, ", Extra_TruthSupportSize((unsigned *)&Fun, 6) );
+        printf( "%2d, ", Ifd_LitNumAnds(p, Abc_Var2Lit(i, 0)) );
+        printf( "%2d, ", Vec_IntEntry(p->vClauses, i) );
+        printf( "ABC_CONST(" );
         Extra_PrintHex( stdout, (unsigned *)&Fun, 6 ); 
         printf( "), \"" );
         Ifd_ObjPrint( p, Abc_Var2Lit( i, 0 ) );
@@ -276,6 +280,69 @@ void Ifd_ManTruthAll( Ifd_Man_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Mpm_ComputeCnfSizeOne( word Truth, int nVars, Vec_Int_t * vCover, Vec_Str_t * vCnf )
+{
+    Vec_StrClear( vCnf );
+    if ( Truth == 0 || ~Truth == 0 )
+    {
+//        assert( nVars == 0 );
+        Vec_StrPush( vCnf, (char)(Truth == 0) );
+        Vec_StrPush( vCnf, (char)-1 );
+        return 1;
+    }
+    else 
+    {
+        int i, k, c, RetValue, Literal, Cube, nCubes = 0;
+        assert( nVars > 0 );
+        for ( c = 0; c < 2; c ++ )
+        {
+            Truth = c ? ~Truth : Truth;
+            RetValue = Kit_TruthIsop( (unsigned *)&Truth, nVars, vCover, 0 );
+            assert( RetValue == 0 );
+            nCubes += Vec_IntSize( vCover );
+            Vec_IntForEachEntry( vCover, Cube, i )
+            {
+                for ( k = 0; k < nVars; k++ )
+                {
+                    Literal = 3 & (Cube >> (k << 1));
+                    if ( Literal == 1 )      // '0'  -> pos lit
+                        Vec_StrPush( vCnf, (char)Abc_Var2Lit(k, 0) );
+                    else if ( Literal == 2 ) // '1'  -> neg lit
+                        Vec_StrPush( vCnf, (char)Abc_Var2Lit(k, 1) );
+                    else if ( Literal != 0 )
+                        assert( 0 );
+                }
+                Vec_StrPush( vCnf, (char)Abc_Var2Lit(nVars, c) );
+                Vec_StrPush( vCnf, (char)-1 );
+            }
+        }
+        return nCubes;
+    }
+}
+void Mpm_ComputeCnfSizeAll( Ifd_Man_t * p )
+{
+    Vec_Int_t * vCover = Vec_IntAlloc( 1 << 16 );
+    Vec_Str_t * vCnf = Vec_StrAlloc( 1000 );
+    word Truth;
+    int i;
+    assert( Vec_IntSize(p->vClauses) == 0 );
+    Vec_WrdForEachEntry( p->vTruths, Truth, i )
+        Vec_IntPush( p->vClauses, Mpm_ComputeCnfSizeOne(Truth, 6, vCover, vCnf) );
+    Vec_IntFree( vCover );
+    Vec_StrFree( vCnf );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Canonicizing DSD structures.]
 
   Description []
@@ -326,7 +393,7 @@ int Ifd_ManHashFindOrAdd( Ifd_Man_t * p, int iDsd0, int iDsd1, int iDsdC, int Ty
         iObj = Vec_IntEntry(p->vRes, Value);
         Vec_IntShrink( p->vArgs, Vec_IntSize(p->vArgs) - 4 );
         pObj = Ifd_ManObj( p, iObj );
-        pObj->nFreq++;
+//        pObj->nFreq++;
         assert( (int)pObj->Type == Type );
         assert( (int)pObj->nSupp == Ifd_LitSuppSize(p, iDsd0) + Ifd_LitSuppSize(p, iDsd1) + Ifd_LitSuppSize(p, iDsdC) );
     }
@@ -337,8 +404,9 @@ int Ifd_ManHashFindOrAdd( Ifd_Man_t * p, int iDsd0, int iDsd1, int iDsdC, int Ty
         assert( p->nObjs < p->nObjsAlloc );
         iObj = p->nObjs;
         pObj = Ifd_ManObj( p, p->nObjs++ );
-        pObj->nFreq = 1;
+//        pObj->nFreq = 1;
         pObj->nSupp = Ifd_LitSuppSize(p, iDsd0) + Ifd_LitSuppSize(p, iDsd1) + Ifd_LitSuppSize(p, iDsdC); 
+        pObj->nAnds = Ifd_LitNumAnds(p, iDsd0) + Ifd_LitNumAnds(p, iDsd1) + Ifd_LitNumAnds(p, iDsdC) + ((Type == 1) ? 1 : 3); 
         pObj->Type  = Type;
         if ( Type == 1 )
             pObj->fWay = 0;
@@ -615,6 +683,7 @@ Vec_Wrd_t * Ifd_ManDsdTruths( int nVars )
         Vec_IntPush( pMan->vMarks, pMan->nObjs );
     }
     Ifd_ManTruthAll( pMan );
+    Mpm_ComputeCnfSizeAll( pMan );
 //    Ifd_ManPrint( pMan );
     vTruths = pMan->vTruths; pMan->vTruths = NULL;
     Ifd_ManStop( pMan );

src/map/mpm/mpmTruth.c

@@ -19,7 +19,6 @@
 ***********************************************************************/
 
 #include "mpmInt.h"
-#include "misc/util/utilTruth.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -28,13 +27,40 @@ ABC_NAMESPACE_IMPL_START
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+//#define MPM_TRY_NEW
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
 
-  Synopsis    [Performs truth table computation.]
+  Synopsis    [Unifies variable order.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Mpm_TruthStretch( word * pTruth, Mpm_Cut_t * pCut, Mpm_Cut_t * pCut0, int nLimit )
+{
+    int i, k;
+    for ( i = (int)pCut->nLeaves - 1, k = (int)pCut0->nLeaves - 1; i >= 0 && k >= 0; i-- )
+    {
+        if ( pCut0->pLeaves[k] < pCut->pLeaves[i] )
+            continue;
+        assert( pCut0->pLeaves[k] == pCut->pLeaves[i] );
+        if ( k < i )
+            Abc_TtSwapVars( pTruth, nLimit, k, i );
+        k--;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs truth table support minimization.]
 
   Description []
                
@@ -80,22 +106,57 @@ static inline int Mpm_CutTruthMinimize6( Mpm_Man_t * p, Mpm_Cut_t * pCut )
     pCut->iFunc = Abc_Var2Lit( Vec_MemHashInsert(p->vTtMem, &t), Abc_LitIsCompl(pCut->iFunc) );
     return 1;
 }
-static inline word Mpm_TruthStretch6( word Truth, Mpm_Cut_t * pCut, Mpm_Cut_t * pCut0, int nLimit )
+static inline int Mpm_CutTruthMinimize7( Mpm_Man_t * p, Mpm_Cut_t * pCut )
 {
-    int i, k;
-    for ( i = (int)pCut->nLeaves - 1, k = (int)pCut0->nLeaves - 1; i >= 0 && k >= 0; i-- )
+    unsigned uSupport;
+    int i, k, nSuppSize;
+    // compute the support of the cut's function
+    word * pTruth = Mpm_CutTruth( p, Abc_Lit2Var(pCut->iFunc) );
+    uSupport = Abc_TtSupportAndSize( pTruth, Mpm_CutLeafNum(pCut), &nSuppSize );
+    if ( nSuppSize == Mpm_CutLeafNum(pCut) )
+        return 0;
+    p->nSmallSupp += (int)(nSuppSize < 2);
+    // update leaves and signature
+    Abc_TtCopy( p->Truth, pTruth, p->nTruWords, 0 );
+    for ( i = k = 0; i < Mpm_CutLeafNum(pCut); i++ )
+    {
+        if ( ((uSupport >> i) & 1) )
         {
-        if ( pCut0->pLeaves[k] < pCut->pLeaves[i] )
-            continue;
-        assert( pCut0->pLeaves[k] == pCut->pLeaves[i] );
             if ( k < i )
-            Abc_TtSwapVars( &Truth, nLimit, k, i );
-        k--;
+            {
+                pCut->pLeaves[k] = pCut->pLeaves[i];
+                Abc_TtSwapVars( p->Truth, p->nLutSize, k, i );
+            }
+            k++;
+        }
+        else
+        {
+            int iObj = Abc_Lit2Var( pCut->pLeaves[i] );
+            int Res = Vec_IntRemove( &p->vObjPresUsed, iObj );
+            assert( Res == 1 );
+            p->pObjPres[iObj] = (unsigned char)0xFF; 
         }
-    return Truth;
+    }
+    assert( k == nSuppSize );
+    pCut->nLeaves = nSuppSize;
+    assert( nSuppSize == Abc_TtSupportSize(p->Truth, 6) );
+    // save the result
+    pCut->iFunc = Abc_Var2Lit( Vec_MemHashInsert(p->vTtMem, p->Truth), Abc_LitIsCompl(pCut->iFunc) );
+    return 1;
 }
-//#define MPM_TRY_NEW
-int Mpm_CutComputeTruth6( Mpm_Man_t * p, Mpm_Cut_t * pCut, Mpm_Cut_t * pCut0, Mpm_Cut_t * pCut1, Mpm_Cut_t * pCutC, int fCompl0, int fCompl1, int fComplC, int Type )
+
+/**Function*************************************************************
+
+  Synopsis    [Performs truth table computation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Mpm_CutComputeTruth6( Mpm_Man_t * p, Mpm_Cut_t * pCut, Mpm_Cut_t * pCut0, Mpm_Cut_t * pCut1, Mpm_Cut_t * pCutC, int fCompl0, int fCompl1, int fComplC, int Type )
 {
     word * pTruth0 = Mpm_CutTruth( p, Abc_Lit2Var(pCut0->iFunc) );
     word * pTruth1 = Mpm_CutTruth( p, Abc_Lit2Var(pCut1->iFunc) );
@@ -103,13 +164,13 @@ int Mpm_CutComputeTruth6( Mpm_Man_t * p, Mpm_Cut_t * pCut, Mpm_Cut_t * pCut0, Mp
     word t0 = (fCompl0 ^ pCut0->fCompl ^ Abc_LitIsCompl(pCut0->iFunc)) ? ~*pTruth0 : *pTruth0;
     word t1 = (fCompl1 ^ pCut1->fCompl ^ Abc_LitIsCompl(pCut1->iFunc)) ? ~*pTruth1 : *pTruth1;
     word tC = 0, t = 0;
-    t0 = Mpm_TruthStretch6( t0, pCut, pCut0, p->nLutSize );
-    t1 = Mpm_TruthStretch6( t1, pCut, pCut1, p->nLutSize );
+    Mpm_TruthStretch( &t0, pCut, pCut0, p->nLutSize );
+    Mpm_TruthStretch( &t1, pCut, pCut1, p->nLutSize );
     if ( pCutC )
     {
         pTruthC = Mpm_CutTruth( p, Abc_Lit2Var(pCutC->iFunc) );
         tC = (fComplC ^ pCutC->fCompl ^ Abc_LitIsCompl(pCutC->iFunc)) ? ~*pTruthC : *pTruthC;
-        tC = Mpm_TruthStretch6( tC, pCut, pCutC, p->nLutSize );
+        Mpm_TruthStretch( &tC, pCut, pCutC, p->nLutSize );
     }
     assert( p->nLutSize <= 6 );
     if ( Type == 1 )
@@ -127,19 +188,60 @@ int Mpm_CutComputeTruth6( Mpm_Man_t * p, Mpm_Cut_t * pCut, Mpm_Cut_t * pCut0, Mp
     }
     else
         pCut->iFunc = Abc_Var2Lit( Vec_MemHashInsert( p->vTtMem, &t ), 0 );
-
+    if ( p->pPars->fCutMin )
+        return Mpm_CutTruthMinimize6( p, pCut );
+    return 1;
+}
+static inline int Mpm_CutComputeTruth7( Mpm_Man_t * p, Mpm_Cut_t * pCut, Mpm_Cut_t * pCut0, Mpm_Cut_t * pCut1, Mpm_Cut_t * pCutC, int fCompl0, int fCompl1, int fComplC, int Type )
+{
+    word * pTruth0 = Mpm_CutTruth( p, Abc_Lit2Var(pCut0->iFunc) );
+    word * pTruth1 = Mpm_CutTruth( p, Abc_Lit2Var(pCut1->iFunc) );
+    word * pTruthC = NULL;
+    Abc_TtCopy( p->Truth0, pTruth0, p->nTruWords, fCompl0 ^ pCut0->fCompl ^ Abc_LitIsCompl(pCut0->iFunc) );
+    Abc_TtCopy( p->Truth1, pTruth1, p->nTruWords, fCompl1 ^ pCut1->fCompl ^ Abc_LitIsCompl(pCut1->iFunc) );
+    Mpm_TruthStretch( p->Truth0, pCut, pCut0, p->nLutSize );
+    Mpm_TruthStretch( p->Truth1, pCut, pCut1, p->nLutSize );
+    if ( pCutC )
+    {
+        pTruthC = Mpm_CutTruth( p, Abc_Lit2Var(pCutC->iFunc) );
+        Abc_TtCopy( p->TruthC, pTruthC, p->nTruWords, fComplC ^ pCutC->fCompl ^ Abc_LitIsCompl(pCutC->iFunc) );
+        Mpm_TruthStretch( p->TruthC, pCut, pCutC, p->nLutSize );
+    }
+    if ( Type == 1 )
+        Abc_TtAnd( p->Truth, p->Truth0, p->Truth1, p->nTruWords, 0 );
+    else if ( Type == 2 )
+        Abc_TtXor( p->Truth, p->Truth0, p->Truth1, p->nTruWords, 0 );
+    else if ( Type == 3 )
+        Abc_TtMux( p->Truth, p->TruthC, p->Truth1, p->Truth0, p->nTruWords );
+    else assert( 0 );
+    // save the result
+    if ( p->Truth[0] & 1 )
+    {
+        Abc_TtNot( p->Truth, p->nTruWords );
+        pCut->iFunc = Abc_Var2Lit( Vec_MemHashInsert( p->vTtMem, p->Truth ), 1 );
+    }
+    else
+        pCut->iFunc = Abc_Var2Lit( Vec_MemHashInsert( p->vTtMem, p->Truth ), 0 );
+    if ( p->pPars->fCutMin )
+        return Mpm_CutTruthMinimize7( p, pCut );
+    return 1;
+}
+int Mpm_CutComputeTruth( Mpm_Man_t * p, Mpm_Cut_t * pCut, Mpm_Cut_t * pCut0, Mpm_Cut_t * pCut1, Mpm_Cut_t * pCutC, int fCompl0, int fCompl1, int fComplC, int Type )
+{
+    int RetValue;
+    if ( p->nLutSize <= 6 )
+        RetValue = Mpm_CutComputeTruth6( p, pCut, pCut0, pCut1, pCutC, fCompl0, fCompl1, fComplC, Type );
+    else
+        RetValue = Mpm_CutComputeTruth7( p, pCut, pCut0, pCut1, pCutC, fCompl0, fCompl1, fComplC, Type );
 #ifdef MPM_TRY_NEW
     {
         extern unsigned Abc_TtCanonicize( word * pTruth, int nVars, char * pCanonPerm );
-        word tCopy = t;
         char pCanonPerm[16];
-        Abc_TtCanonicize( &tCopy, p->nLutSize, pCanonPerm );
+        memcpy( p->Truth0, p->Truth, sizeof(word) * p->nTruWords );
+        Abc_TtCanonicize( p->Truth0, pCut->nLimit, pCanonPerm );
     }
 #endif
-
-    if ( p->pPars->fCutMin )
-        return Mpm_CutTruthMinimize6( p, pCut );
-    return 0;
+    return RetValue;
 }
 
 ////////////////////////////////////////////////////////////////////////

src/misc/util/utilTruth.h

@@ -128,6 +128,12 @@ static inline void Abc_TtFill( word * pOut, int nWords )
     for ( w = 0; w < nWords; w++ )
         pOut[w] = ~(word)0;
 }
+static inline void Abc_TtUnit( word * pOut, int nWords )
+{
+    int w;
+    for ( w = 0; w < nWords; w++ )
+        pOut[w] = s_Truths6[0];
+}
 static inline void Abc_TtNot( word * pOut, int nWords )
 {
     int w;

src/misc/vec/vecMem.h

@@ -268,16 +268,26 @@ static inline void Vec_MemShrink( Vec_Mem_t * p, int nEntriesNew )
   SeeAlso     []
 
 ***********************************************************************/
-static inline void Vec_MemPrint( Vec_Mem_t * p )
+static inline void Vec_MemDumpDigit( FILE * pFile, int HexDigit )
+{
+    assert( HexDigit >= 0 && HexDigit < 16 );
+    if ( HexDigit < 10 )
+        fprintf( pFile, "%d", HexDigit );
+    else
+        fprintf( pFile, "%c", 'A' + HexDigit-10 );
+}
+static inline void Vec_MemDump( FILE * pFile, Vec_Mem_t * pVec )
 {
     word * pEntry;
-    int i;
-    printf( "Memory vector has %d entries: ", Vec_MemEntryNum(p) );
-    Vec_MemForEachEntry( p, pEntry, i )
+    int i, w, d;
+    if ( pFile == stdout )
+        printf( "Memory vector has %d entries: ", Vec_MemEntryNum(pVec) );
+    Vec_MemForEachEntry( pVec, pEntry, i )
     {
-        printf( "%3d : ", i );
-        // add printout here
-        printf( "\n" );
+        for ( w = pVec->nEntrySize - 1; w >= 0; w-- )
+            for ( d = 15; d >= 0; d-- )
+                Vec_MemDumpDigit( pFile, (int)(pEntry[w] >> (d<<2)) & 15 );
+        fprintf( pFile, "\n" );
     }
 }