Improvements to the new technology mapper.

6 files changed, 216 insertions, 76 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 35c6ebb5..1a30a95c 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -242,16 +242,19 @@ struct Jf_Par_t_
     int            nRounds;
     int            DelayTarget;
     int            fAreaOnly;
+    int            fOptEdge;
     int            fCoarsen;
     int            fCutMin;
     int            fUseTts;
+    int            fGenCnf;
     int            fVerbose;
     int            fVeryVerbose;
     int            nLutSizeMax;
     int            nCutNumMax;
-    int            Delay;
-    int            Area;
-    int            Edge;
+    word           Delay;
+    word           Area;
+    word           Edge;
+    word           Clause;
 };
 
 static inline unsigned     Gia_ObjCutSign( unsigned ObjId )       { return (1 << (ObjId & 31));                                 }
diff --git a/src/aig/gia/giaJf.c b/src/aig/gia/giaJf.c
index eb6278b2..ee135422 100644
--- a/src/aig/gia/giaJf.c
+++ b/src/aig/gia/giaJf.c
@@ -41,7 +41,8 @@ struct Jf_Cut_t_
     float            Flow;        // flow
     int              Time;        // arrival time
     int              iFunc;       // function 
-    int              pCut[JF_LEAF_MAX+1]; // cut
+    int              Cost;        // cut cost
+    int              pCut[JF_LEAF_MAX+2]; // cut
 };
 
 typedef struct Jf_Man_t_ Jf_Man_t; 
@@ -50,6 +51,7 @@ struct Jf_Man_t_
     Gia_Man_t *      pGia;        // user's manager
     Jf_Par_t *       pPars;       // users parameter
     Sdm_Man_t *      pDsd;        // extern DSD manager
+    Vec_Int_t *      vCnfs;       // costs of elementary CNFs
     Vec_Mem_t *      vTtMem;      // truth table memory and hash table
     Vec_Int_t        vCuts;       // cuts for each node
     Vec_Int_t        vArr;        // arrival time
@@ -78,8 +80,14 @@ static inline float  Jf_ObjRefs( Jf_Man_t * p, int i )      { return Vec_FltEntr
 //static inline int    Jf_ObjLit( int i, int c )            { return i;                                                }
 static inline int    Jf_ObjLit( int i, int c )              { return Abc_Var2Lit( i, c );                              }
 
-static inline int    Jf_CutSize( int * pCut )               { return pCut[0] & 0x1F;                                   }
-static inline int    Jf_CutFunc( int * pCut )               { return (pCut[0] >> 5);                                   }
+static inline int    Jf_CutSize( int * pCut )               { return pCut[0] & 0xF;                                    }  //  4 bits
+static inline int    Jf_CutCost( int * pCut )               { return (pCut[0] >> 4) & 0x3F;                            }  //  6 bits
+static inline int    Jf_CutFunc( int * pCut )               { return (pCut[0] >> 10);                                  }  // 22 bits
+static inline int    Jf_CutSetAll( int f, int c, int s )    { return (f << 10) | (c << 4) | s;                         }
+static inline void   Jf_CutSetSize( int * pCut, int s )     { assert(s>=0 && s<16); pCut[0] ^= (Jf_CutSize(pCut) ^ s); }
+static inline void   Jf_CutSetCost( int * pCut, int c )     { assert(c>=0 && c<64); pCut[0] ^=((Jf_CutCost(pCut) ^ c) << 4); }
+static inline void   Jf_CutSetFunc( int * pCut, int f )     { assert(f>=0); pCut[0] ^=((Jf_CutFunc(pCut) ^ f) << 10);  }
+
 static inline int    Jf_CutFuncClass( int * pCut )          { return Abc_Lit2Var(Jf_CutFunc(pCut));                    }
 static inline int    Jf_CutFuncCompl( int * pCut )          { return Abc_LitIsCompl(Jf_CutFunc(pCut));                 }
 static inline int *  Jf_CutLits( int * pCut )               { return pCut + 1;                                         }
@@ -87,9 +95,11 @@ static inline int    Jf_CutLit( int * pCut, int i )         { assert(i);return p
 //static inline int    Jf_CutVar( int * pCut, int i )         { assert(i); return pCut[i];                               }
 static inline int    Jf_CutVar( int * pCut, int i )         {  assert(i);return Abc_Lit2Var(pCut[i]);                  }
 static inline int    Jf_CutIsTriv( int * pCut, int i )      { return Jf_CutSize(pCut) == 1 && Jf_CutVar(pCut, 1) == i; } 
+static inline int    Jf_CutCnfSizeF( Jf_Man_t * p, int f )  { return Vec_IntEntry( p->vCnfs, f );                      }
+static inline int    Jf_CutCnfSize( Jf_Man_t * p, int * c ) { return Jf_CutCnfSizeF( p, Jf_CutFuncClass(c) );          }
 
-static inline int    Jf_ObjFunc0( Gia_Obj_t * p, int * q )  { return Abc_LitNotCond(Jf_CutFunc(q), Gia_ObjFaninC0(p)); } 
-static inline int    Jf_ObjFunc1( Gia_Obj_t * p, int * q )  { return Abc_LitNotCond(Jf_CutFunc(q), Gia_ObjFaninC1(p)); } 
+static inline int    Jf_ObjFunc0( Gia_Obj_t * p, int * c )  { return Abc_LitNotCond(Jf_CutFunc(c), Gia_ObjFaninC0(p)); } 
+static inline int    Jf_ObjFunc1( Gia_Obj_t * p, int * c )  { return Abc_LitNotCond(Jf_CutFunc(c), Gia_ObjFaninC1(p)); } 
 
 #define Jf_ObjForEachCut( pList, pCut, i )   for ( i = 0, pCut = pList + 1; i < pList[0]; i++, pCut += Jf_CutSize(pCut) + 1 )
 #define Jf_CutForEachLit( pCut, Lit, i )     for ( i = 1; i <= Jf_CutSize(pCut) && (Lit = Jf_CutLit(pCut, i)); i++ )
@@ -226,9 +236,7 @@ Jf_Man_t * Jf_ManAlloc( Gia_Man_t * pGia, Jf_Par_t * pPars )
     p = ABC_CALLOC( Jf_Man_t, 1 );
     p->pGia      = pGia;
     p->pPars     = pPars;
-    if ( pPars->fCutMin && !pPars->fUseTts )
-        p->pDsd  = Sdm_ManRead();
-    else if ( pPars->fCutMin && pPars->fUseTts )
+    if ( pPars->fCutMin && pPars->fUseTts )
     {
         word uTruth; int Value;
         p->vTtMem    = Vec_MemAlloc( 1, 12 ); // 32 KB/page for 6-var functions
@@ -236,6 +244,15 @@ Jf_Man_t * Jf_ManAlloc( Gia_Man_t * pGia, Jf_Par_t * pPars )
         uTruth = ABC_CONST(0x0000000000000000); Value = Vec_MemHashInsert( p->vTtMem, &uTruth ); assert( Value == 0 );
         uTruth = ABC_CONST(0xAAAAAAAAAAAAAAAA); Value = Vec_MemHashInsert( p->vTtMem, &uTruth ); assert( Value == 1 );
     }
+    else if ( pPars->fCutMin && !pPars->fUseTts )
+    {
+        p->pDsd = Sdm_ManRead();
+        if ( pPars->fGenCnf )
+        {
+            p->vCnfs = Vec_IntStart( 595 );
+            Sdm_ManReadCnfCosts( p->pDsd, Vec_IntArray(p->vCnfs), Vec_IntSize(p->vCnfs) );
+        }
+    }
     Vec_IntFill( &p->vCuts, Gia_ManObjNum(pGia), 0 );
     Vec_IntFill( &p->vArr,  Gia_ManObjNum(pGia), 0 );
     Vec_IntFill( &p->vDep,  Gia_ManObjNum(pGia), 0 );
@@ -268,6 +285,7 @@ void Jf_ManFree( Jf_Man_t * p )
         Vec_MemHashFree( p->vTtMem );
         Vec_MemFree( p->vTtMem );
     }
+    Vec_IntFreeP( &p->vCnfs );
     Vec_SetFree_( &p->pMem );
     Vec_IntFreeP( &p->vTemp );
     ABC_FREE( p );
@@ -690,55 +708,63 @@ static inline void Jf_ObjSortCuts( Jf_Cut_t ** pSto, int nSize )
   SeeAlso     []
 
 ***********************************************************************/
-int Jf_CutRef_rec( Jf_Man_t * p, int * pCut, int fEdge, int Limit )
+int Jf_CutRef_rec( Jf_Man_t * p, int * pCut )
 {
-    int i, Var, Count = 0;
-    if ( Limit == 0 ) // terminal
-        return 0;
+    int i, Var, Count = Jf_CutCost(pCut);
     Jf_CutForEachVar( pCut, Var, i )
-        if ( Gia_ObjRefIncId( p->pGia, Var ) == 0 && !Jf_CutIsTriv(Jf_ObjCutBest(p, Var), Var) )
-                Count += Jf_CutRef_rec( p, Jf_ObjCutBest(p, Var), fEdge, Limit - 1 );
-    return Count + (fEdge ? (1 << 5) + Jf_CutSize(pCut) : 1);
-//    return Count + (fEdge ? Jf_CutSize(pCut) : 1);
+        if ( !Gia_ObjRefIncId(p->pGia, Var) && !Jf_CutIsTriv(Jf_ObjCutBest(p, Var), Var) )
+            Count += Jf_CutRef_rec( p, Jf_ObjCutBest(p, Var) );
+    return Count;
 }
-int Jf_CutDeref_rec( Jf_Man_t * p, int * pCut, int fEdge, int Limit )
+int Jf_CutDeref_rec( Jf_Man_t * p, int * pCut )
 {
-    int i, Var, Count = 0;
-    if ( Limit == 0 ) // terminal
-        return 0;
+    int i, Var, Count = Jf_CutCost(pCut);
     Jf_CutForEachVar( pCut, Var, i )
-        if ( Gia_ObjRefDecId( p->pGia, Var ) == 0 && !Jf_CutIsTriv(Jf_ObjCutBest(p, Var), Var) )
-            Count += Jf_CutDeref_rec( p, Jf_ObjCutBest(p, Var), fEdge, Limit - 1 );
-    return Count + (fEdge ? (1 << 5) + Jf_CutSize(pCut) : 1);
-//    return Count + (fEdge ? Jf_CutSize(pCut) : 1);
+        if ( !Gia_ObjRefDecId(p->pGia, Var) && !Jf_CutIsTriv(Jf_ObjCutBest(p, Var), Var) )
+            Count += Jf_CutDeref_rec( p, Jf_ObjCutBest(p, Var) );
+    return Count;
 }
-static inline int Jf_CutElaOld( Jf_Man_t * p, int * pCut, int fEdge )
+static inline int Jf_CutAreaOld( Jf_Man_t * p, int * pCut )
 {
-    int Ela1 = Jf_CutRef_rec( p, pCut, fEdge, ABC_INFINITY );
-    int Ela2 = Jf_CutDeref_rec( p, pCut, fEdge, ABC_INFINITY );
+    int Ela1, Ela2;
+    assert( p->pPars->fGenCnf || Jf_CutCost(pCut) > 0 );
+    Ela1 = Jf_CutRef_rec( p, pCut );
+    Ela2 = Jf_CutDeref_rec( p, pCut );
     assert( Ela1 == Ela2 );
     return Ela1;
 }
-int Jf_CutRef2_rec( Jf_Man_t * p, int * pCut, int fEdge, int Limit )
+
+int Jf_CutAreaRef_rec( Jf_Man_t * p, int * pCut, int Limit )
+{
+    int i, Var, Count = Jf_CutCost(pCut);
+    Jf_CutForEachVar( pCut, Var, i )
+    {
+        if ( Gia_ObjRefIncId(p->pGia, Var) == 0 && !Jf_CutIsTriv(Jf_ObjCutBest(p, Var), Var) && Limit > 1 )
+            Count += Jf_CutAreaRef_rec( p, Jf_ObjCutBest(p, Var), Limit - 1 );
+        Vec_IntPush( p->vTemp, Var );
+    }
+    return Count;
+}
+int Jf_CutAreaRefEdge_rec( Jf_Man_t * p, int * pCut, int Limit )
 {
-    int i, Var, Count = 0;
-    if ( Limit == 0 ) // terminal
-        return 0;
+    int i, Var, Count = (Jf_CutCost(pCut) << 4) | Jf_CutSize(pCut);
     Jf_CutForEachVar( pCut, Var, i )
     {
-        if ( Gia_ObjRefIncId( p->pGia, Var ) == 0 && !Jf_CutIsTriv(Jf_ObjCutBest(p, Var), Var) )
-            Count += Jf_CutRef2_rec( p, Jf_ObjCutBest(p, Var), fEdge, Limit - 1 );
+        if ( Gia_ObjRefIncId(p->pGia, Var) == 0 && !Jf_CutIsTriv(Jf_ObjCutBest(p, Var), Var) && Limit > 1 )
+            Count += Jf_CutAreaRefEdge_rec( p, Jf_ObjCutBest(p, Var), Limit - 1 );
         Vec_IntPush( p->vTemp, Var );
     }
-    return Count + (fEdge ? (1 << 5) + Jf_CutSize(pCut) : 1);
-//    return Count + (fEdge ? Jf_CutSize(pCut) : 1);
+    return Count;
 }
-static inline int Jf_CutEla( Jf_Man_t * p, int * pCut, int fEdge )
+static inline int Jf_CutArea( Jf_Man_t * p, int * pCut, int fEdge )
 {
-    int nRecurLimit = ABC_INFINITY;
     int Ela, Entry, i;
+    assert( p->pPars->fGenCnf || Jf_CutCost(pCut) > 0 );
     Vec_IntClear( p->vTemp );
-    Ela = Jf_CutRef2_rec( p, pCut, fEdge, nRecurLimit );
+    if ( fEdge )
+        Ela = Jf_CutAreaRefEdge_rec( p, pCut, ABC_INFINITY );
+    else
+        Ela = Jf_CutAreaRef_rec( p, pCut, ABC_INFINITY );
     Vec_IntForEachEntry( p->vTemp, Entry, i )
         Gia_ObjRefDecId( p->pGia, Entry );
     return Ela;
@@ -916,7 +942,7 @@ int Jf_TtComputeForCut( Jf_Man_t * p, int iFuncLit0, int iFuncLit1, int * pCut0,
 static inline void Jf_ObjAssignCut( Jf_Man_t * p, Gia_Obj_t * pObj )
 {
     int iObj = Gia_ObjId(p->pGia, pObj);
-    int pClause[3] = { 1, (2 << 5) | 1, Jf_ObjLit(iObj, 0) }; // set function
+    int pClause[3] = { 1, Jf_CutSetAll(2, 0, 1), Jf_ObjLit(iObj, 0) }; // set function
     assert( Gia_ObjIsCi(pObj) || Gia_ObjIsBuf(pObj) );
     Vec_IntWriteEntry( &p->vCuts, iObj, Vec_SetAppend( &p->pMem, pClause, 3 ) );
 }
@@ -952,7 +978,7 @@ void Jf_ObjComputeCuts( Jf_Man_t * p, Gia_Obj_t * pObj, int fEdge )
     int        nOldSupp, Config, i, k, c = 0;
     // prepare cuts
     for ( i = 0; i <= CutNum+1; i++ )
-        pSto[i] = Sto + i, pSto[i]->iFunc = 0;
+        pSto[i] = Sto + i, pSto[i]->Cost = 0, pSto[i]->iFunc = ~0;
     // compute signatures
     pCuts0 = Jf_ObjCuts( p, Gia_ObjFaninId0(pObj, iObj) );
     Jf_ObjForEachCut( pCuts0, pCut0, i )
@@ -998,9 +1024,7 @@ void Jf_ObjComputeCuts( Jf_Man_t * p, Gia_Obj_t * pObj, int fEdge )
             assert( pSto[c]->pCut[0] <= nOldSupp );
             if ( pSto[c]->pCut[0] < nOldSupp )
                 pSto[c]->Sign = Jf_CutGetSign( pSto[c]->pCut );
-            //pSto[c]->Cost = Sdm_ManReadDsdClauseNum( p->pDsd, Abc_Lit2Var(pSto[c]->iFunc) );
         }
-//        Jf_CutCheck( pSto[c]->pCut );
         p->CutCount[2]++;
         pSto[c]->Time = p->pPars->fAreaOnly ? 0 : Jf_CutArr(p, pSto[c]->pCut);
         pSto[c]->Flow = Jf_CutFlow(p, pSto[c]->pCut);
@@ -1013,7 +1037,7 @@ void Jf_ObjComputeCuts( Jf_Man_t * p, Gia_Obj_t * pObj, int fEdge )
     if ( !Jf_ObjIsUnit(pObj) && !Jf_ObjHasCutWithSize(pSto, c, 2) )
     {
         assert( Jf_ObjIsUnit(Gia_ObjFanin0(pObj)) && Jf_ObjIsUnit(Gia_ObjFanin1(pObj)) );
-        pSto[c]->iFunc = p->pPars->fCutMin ? 4 : 0; // set function (DSD only!)
+        if ( p->pPars->fCutMin ) pSto[c]->iFunc = 4;  // set function (DSD only!)
         pSto[c]->pCut[0] = 2; 
         pSto[c]->pCut[1] = Jf_ObjLit(Gia_ObjFaninId0(pObj, iObj), Gia_ObjFaninC0(pObj)); 
         pSto[c]->pCut[2] = Jf_ObjLit(Gia_ObjFaninId1(pObj, iObj), Gia_ObjFaninC1(pObj)); 
@@ -1022,7 +1046,7 @@ void Jf_ObjComputeCuts( Jf_Man_t * p, Gia_Obj_t * pObj, int fEdge )
     // add elementary cut
     if ( Jf_ObjIsUnit(pObj) && !(p->pPars->fCutMin && Jf_ObjHasCutWithSize(pSto, c, 1)) )
     {
-        pSto[c]->iFunc = p->pPars->fCutMin ? 2 : 0; // set function
+        if ( p->pPars->fCutMin ) pSto[c]->iFunc = 2;  // set function
         pSto[c]->pCut[0] = 1;
         pSto[c]->pCut[1] = Jf_ObjLit(iObj, 0);
         c++;
@@ -1030,22 +1054,26 @@ void Jf_ObjComputeCuts( Jf_Man_t * p, Gia_Obj_t * pObj, int fEdge )
     // reorder cuts
 //    Jf_ObjSortCuts( pSto + 1, c - 1 );
 //    Jf_ObjCheckPtrs( pSto, CutNum );
-    p->CutCount[3] += c;
+    // find cost of the best cut
+    pSto[0]->Cost = p->pPars->fGenCnf ? Jf_CutCnfSizeF(p, Abc_Lit2Var(pSto[0]->iFunc)) : 1;
+    assert( pSto[0]->Cost >= 0 );
     // save best info
     assert( pSto[0]->Flow >= 0 );
     Vec_IntWriteEntry( &p->vArr,  iObj, pSto[0]->Time );
-    Vec_FltWriteEntry( &p->vFlow, iObj, (pSto[0]->Flow + (fEdge ? pSto[0]->pCut[0] : 1)) / Jf_ObjRefs(p, iObj) );
+    Vec_FltWriteEntry( &p->vFlow, iObj, (pSto[0]->Flow + (fEdge ? pSto[0]->pCut[0] : pSto[0]->Cost)) / Jf_ObjRefs(p, iObj) );
     // add cuts to storage cuts
     Vec_IntClear( p->vTemp );
     Vec_IntPush( p->vTemp, c );
     for ( i = 0; i < c; i++ )
     {
         assert( pSto[i]->pCut[0] <= 6 );
-        Vec_IntPush( p->vTemp, (pSto[i]->iFunc << 5) | pSto[i]->pCut[0] );
+        pSto[i]->Cost = p->pPars->fGenCnf ? Jf_CutCnfSizeF(p, Abc_Lit2Var(pSto[i]->iFunc)) : 1;
+        Vec_IntPush( p->vTemp, Jf_CutSetAll(pSto[i]->iFunc, pSto[i]->Cost, pSto[i]->pCut[0]) );
         for ( k = 1; k <= pSto[i]->pCut[0]; k++ )
             Vec_IntPush( p->vTemp, pSto[i]->pCut[k] );
     }
     Vec_IntWriteEntry( &p->vCuts, iObj, Vec_SetAppend(&p->pMem, Vec_IntArray(p->vTemp), Vec_IntSize(p->vTemp)) );
+    p->CutCount[3] += c;
 }
 void Jf_ManComputeCuts( Jf_Man_t * p, int fEdge )
 {
@@ -1118,7 +1146,7 @@ int Jf_ManComputeDelay( Jf_Man_t * p, int fEval )
 int Jf_ManComputeRefs( Jf_Man_t * p )
 {
     Gia_Obj_t * pObj; 
-    float nRefsNew; int i;
+    float nRefsNew; int i, * pCut;
     float * pRefs = Vec_FltArray(&p->vRefs);
     float * pFlow = Vec_FltArray(&p->vFlow);
     assert( p->pGia->pRefs != NULL );
@@ -1131,13 +1159,18 @@ int Jf_ManComputeRefs( Jf_Man_t * p )
         else if ( Gia_ObjIsAnd(pObj) && Gia_ObjRefNum(p->pGia, pObj) > 0 )
         {
             assert( Jf_ObjIsUnit(pObj) );
-            Jf_CutRef( p, Jf_ObjCutBest(p, i) );
-            p->pPars->Edge += Jf_CutSize(Jf_ObjCutBest(p, i));
+            pCut = Jf_ObjCutBest(p, i);
+            Jf_CutRef( p, pCut );
+            if ( p->pPars->fGenCnf )
+            p->pPars->Clause += Jf_CutCnfSize(p, pCut);
+            p->pPars->Edge += Jf_CutSize(pCut);
             p->pPars->Area++;
         }
         // blend references and normalize flow
-//        nRefsNew = Abc_MaxFloat( 1, 0.25 * pRefs[i] + 0.75 * p->pGia->pRefs[i] );
-        nRefsNew = Abc_MaxFloat( 1, 0.9 * pRefs[i] + 0.2 * p->pGia->pRefs[i] );
+        if ( p->pPars->fOptEdge )
+            nRefsNew = Abc_MaxFloat( 1, 0.8 * pRefs[i] + 0.2 * p->pGia->pRefs[i] );
+        else
+            nRefsNew = Abc_MaxFloat( 1, 0.2 * pRefs[i] + 0.8 * p->pGia->pRefs[i] );
         pFlow[i] = pFlow[i] * pRefs[i] / nRefsNew;
         pRefs[i] = nRefsNew;
         assert( pFlow[i] >= 0 );
@@ -1167,13 +1200,16 @@ void Jf_ObjComputeBestCut( Jf_Man_t * p, Gia_Obj_t * pObj, int fEdge, int fEla )
     Jf_ObjForEachCut( pCuts, pCut, i )
     {
         if ( Jf_CutIsTriv(pCut, iObj) ) continue;
-        Area = fEla ? Jf_CutEla(p, pCut, fEdge) : Jf_CutFlow(p, pCut);
+        if ( fEdge && !fEla ) 
+            Jf_CutSetCost(pCut, Jf_CutSize(pCut));
+        assert( p->pPars->fGenCnf || Jf_CutCost(pCut) > 0 );
+        Area = fEla ? Jf_CutArea(p, pCut, fEdge) : Jf_CutFlow(p, pCut) + Jf_CutCost(pCut);
         if ( pCutBest == NULL || AreaBest > Area || (AreaBest == Area && TimeBest > (Time = Jf_CutArr(p, pCut))) )
             pCutBest = pCut, AreaBest = Area, TimeBest = Time;
     }
     Vec_IntWriteEntry( &p->vArr,  iObj, Jf_CutArr(p, pCutBest) );
     if ( !fEla )
-    Vec_FltWriteEntry( &p->vFlow, iObj, (AreaBest + (fEdge ? 10 + Jf_CutSize(pCut) : 1)) / Jf_ObjRefs(p, iObj) );
+    Vec_FltWriteEntry( &p->vFlow, iObj, AreaBest / Jf_ObjRefs(p, iObj) );
     Jf_ObjSetBestCut( pCuts, pCutBest, p->vTemp );
 //    Jf_CutPrint( Jf_ObjCutBest(p, iObj) ); printf( "\n" );
 }
@@ -1192,21 +1228,25 @@ void Jf_ManPropagateEla( Jf_Man_t * p, int fEdge )
 {
     Gia_Obj_t * pObj; 
     int i, CostBef, CostAft;
-    p->pPars->Area = p->pPars->Edge = 0;
+    p->pPars->Area = p->pPars->Edge = p->pPars->Clause = 0;
     Gia_ManForEachObjReverse( p->pGia, pObj, i )
         if ( Gia_ObjIsBuf(pObj) )
             Jf_ObjPropagateBuf( p, pObj, 1 );
         else if ( Gia_ObjIsAnd(pObj) && Gia_ObjRefNum(p->pGia, pObj) > 0 )
         {
             assert( Jf_ObjIsUnit(pObj) );
-            CostBef = Jf_CutDeref_rec( p, Jf_ObjCutBest(p, i), fEdge, ABC_INFINITY );
+            CostBef = Jf_CutDeref_rec( p, Jf_ObjCutBest(p, i) );
             Jf_ObjComputeBestCut( p, pObj, fEdge, 1 );
-            CostAft = Jf_CutRef_rec( p, Jf_ObjCutBest(p, i), fEdge, ABC_INFINITY );
-//            assert( CostBef >= CostAft ); // does not hold because of JF_EDGE_LIM
+            CostAft = Jf_CutRef_rec( p, Jf_ObjCutBest(p, i) );
+//            if ( CostBef != CostAft )  printf( "%d -> %d   ", CostBef, CostAft );
+            assert( CostBef >= CostAft ); // does not hold because of JF_EDGE_LIM
+            if ( p->pPars->fGenCnf )
+            p->pPars->Clause += Jf_CutCnfSize(p, Jf_ObjCutBest(p, i));
             p->pPars->Edge += Jf_CutSize(Jf_ObjCutBest(p, i));
             p->pPars->Area++;
         }
     p->pPars->Delay = Jf_ManComputeDelay( p, 1 );
+//    printf( "\n" );
 }
 
 /**Function*************************************************************
@@ -1246,13 +1286,10 @@ Gia_Man_t * Jf_ManDeriveMappingGia( Jf_Man_t * p )
        if ( Gia_ObjIsBuf(pObj) || Gia_ObjRefNum(p->pGia, pObj) == 0 )
             continue;
         pCut = Jf_ObjCutBest( p, i );
-        Class = Jf_CutFuncClass( pCut );
-        if ( p->pPars->fUseTts )
-            uTruth = *Vec_MemReadEntry(p->vTtMem, Class);
-        else
-            uTruth = Sdm_ManReadDsdTruth(p->pDsd, Class);
 //        printf( "Best cut of node %d:  ", i );  Jf_CutPrint(pCut);
-//        assert( Sdm_ManReadDsdVarNum( p->pDsd, Class ) == Jf_CutSize(pCut) );
+        Class = Jf_CutFuncClass( pCut );
+        uTruth = p->pPars->fUseTts ? *Vec_MemReadEntry(p->vTtMem, Class) : Sdm_ManReadDsdTruth(p->pDsd, Class);
+        assert( p->pDsd == NULL || Sdm_ManReadDsdVarNum(p->pDsd, Class) == Jf_CutSize(pCut) );
         if ( Jf_CutSize(pCut) == 0 )
         {
             assert( Class == 0 );
@@ -1313,7 +1350,7 @@ void Jf_ManDeriveMapping( Jf_Man_t * p )
     Gia_Obj_t * pObj; 
     int i, k, * pCut;
     assert( !p->pPars->fCutMin );
-    vMapping = Vec_IntAlloc( Gia_ManObjNum(p->pGia) + p->pPars->Edge + p->pPars->Area * 2 );
+    vMapping = Vec_IntAlloc( Gia_ManObjNum(p->pGia) + (int)p->pPars->Edge + (int)p->pPars->Area * 2 );
     Vec_IntFill( vMapping, Gia_ManObjNum(p->pGia), 0 );
     Gia_ManForEachAnd( p->pGia, pObj, i )
     {
@@ -1351,9 +1388,11 @@ void Jf_ManSetDefaultPars( Jf_Par_t * pPars )
     pPars->nRounds      =  1;
     pPars->DelayTarget  = -1;
     pPars->fAreaOnly    =  1;
+    pPars->fOptEdge     =  1; 
     pPars->fCoarsen     =  0;
     pPars->fCutMin      =  0;
     pPars->fUseTts      =  0;
+    pPars->fGenCnf      =  0;
     pPars->fVerbose     =  0;
     pPars->fVeryVerbose =  0;
     pPars->nLutSizeMax  =  JF_LEAF_MAX;
@@ -1367,6 +1406,8 @@ void Jf_ManPrintStats( Jf_Man_t * p, char * pTitle )
     printf( "Level =%6d   ", p->pPars->Delay );
     printf( "Area =%9d   ",  p->pPars->Area );
     printf( "Edge =%9d   ",  p->pPars->Edge );
+    if ( p->pPars->fGenCnf )
+    printf( "Cnf =%9d   ",   p->pPars->Clause );
     Abc_PrintTime( 1, "Time", Abc_Clock() - p->clkStart );
     fflush( stdout );
 }
@@ -1374,17 +1415,20 @@ Gia_Man_t * Jf_ManPerformMapping( Gia_Man_t * pGia, Jf_Par_t * pPars )
 {
     Gia_Man_t * pNew = pGia;
     Jf_Man_t * p; int i;
+    assert( !pPars->fCutMin || pPars->nLutSize <= 6 );
+    if ( pPars->fGenCnf )
+        pPars->fCutMin = 1, pPars->fUseTts = pPars->fOptEdge = 0;
     if ( pPars->fCutMin && pPars->fUseTts )
         pPars->fCoarsen = 0;
     p = Jf_ManAlloc( pGia, pPars );
     p->pCutCmp = pPars->fAreaOnly ? Jf_CutCompareArea : Jf_CutCompareDelay;
     Jf_ManComputeCuts( p, 0 );
-    Jf_ManComputeRefs( p );                  Jf_ManPrintStats( p, "Start" );
+    Jf_ManComputeRefs( p );                         Jf_ManPrintStats( p, "Start" );
     for ( i = 0; i < pPars->nRounds; i++ )
     {
-        Jf_ManPropagateFlow( p, 1 );         Jf_ManPrintStats( p, "Flow " );
-        Jf_ManPropagateEla( p, 0 );          Jf_ManPrintStats( p, "Area " );
-        Jf_ManPropagateEla( p, 1 );          Jf_ManPrintStats( p, "Edge " );
+        Jf_ManPropagateFlow( p, pPars->fOptEdge );  Jf_ManPrintStats( p, "Flow " );
+        Jf_ManPropagateEla( p, 0 );                 Jf_ManPrintStats( p, "Area " );
+        Jf_ManPropagateEla( p, 1 );                 Jf_ManPrintStats( p, "Edge " );
     }
     if ( p->pPars->fCutMin )
         pNew = Jf_ManDeriveMappingGia(p);
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 475cbb5b..727107a9 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -29847,7 +29847,7 @@ int Abc_CommandAbc9Jf( Abc_Frame_t * pAbc, int argc, char ** argv )
     int c;
     Jf_ManSetDefaultPars( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "KCRDacmtvwh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "KCRDaekmtcvwh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -29904,7 +29904,10 @@ int Abc_CommandAbc9Jf( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'a':
             pPars->fAreaOnly ^= 1;
             break;
-        case 'c':
+        case 'e':
+            pPars->fOptEdge ^= 1;
+            break;
+        case 'k':
             pPars->fCoarsen ^= 1;
             break;
         case 'm':
@@ -29913,6 +29916,9 @@ int Abc_CommandAbc9Jf( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 't':
             pPars->fUseTts ^= 1;
             break;
+        case 'c':
+            pPars->fGenCnf ^= 1;
+            break;
         case 'v':
             pPars->fVerbose ^= 1;
             break;
@@ -29951,16 +29957,18 @@ usage:
         sprintf(Buffer, "best possible" );
     else
         sprintf(Buffer, "%d", pPars->DelayTarget );
-    Abc_Print( -2, "usage: &jf [-KCRD num] [-acmtvwh]\n" );
+    Abc_Print( -2, "usage: &jf [-KCRD num] [-akmtcvwh]\n" );
     Abc_Print( -2, "\t           performs technology mapping of the network\n" );
     Abc_Print( -2, "\t-K num   : LUT size for the mapping (2 <= K <= %d) [default = %d]\n", pPars->nLutSizeMax, pPars->nLutSize );
     Abc_Print( -2, "\t-C num   : the max number of priority cuts (1 <= C <= %d) [default = %d]\n", pPars->nCutNumMax, pPars->nCutNum );
     Abc_Print( -2, "\t-R num   : the number of mapping rounds [default = %d]\n", pPars->nRounds );
     Abc_Print( -2, "\t-D num   : sets the delay constraint for the mapping [default = %s]\n", Buffer );
     Abc_Print( -2, "\t-a       : toggles area-oriented mapping [default = %s]\n", pPars->fAreaOnly? "yes": "no" );
-    Abc_Print( -2, "\t-c       : toggles coarsening the subject graph [default = %s]\n", pPars->fCoarsen? "yes": "no" );
+    Abc_Print( -2, "\t-e       : toggles edge vs node minimization [default = %s]\n", pPars->fOptEdge? "yes": "no" );
+    Abc_Print( -2, "\t-k       : toggles coarsening the subject graph [default = %s]\n", pPars->fCoarsen? "yes": "no" );
     Abc_Print( -2, "\t-m       : toggles cut minimization [default = %s]\n", pPars->fCutMin? "yes": "no" );
     Abc_Print( -2, "\t-t       : toggles truth tables for minimization [default = %s]\n", pPars->fUseTts? "yes": "no" );
+    Abc_Print( -2, "\t-c       : toggles mapping for CNF generation [default = %s]\n", pPars->fGenCnf? "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");
diff --git a/src/map/if/ifTruth.c b/src/map/if/ifTruth.c
index bdbb2e1f..e41acfd6 100644
--- a/src/map/if/ifTruth.c
+++ b/src/map/if/ifTruth.c
@@ -675,6 +675,42 @@ int If_CutComputeTruth2( If_Man_t * p, If_Cut_t * pCut, If_Cut_t * pCut0, If_Cut
     return 0;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Truth table computation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+/*
+int If_CutComputeTruth3( If_Man_t * p, If_Cut_t * pCut, If_Cut_t * pCut0, If_Cut_t * pCut1, int fCompl0, int fCompl1 )
+{
+    int fCompl, truthId;
+    int iFuncLit0   = pCut0->iDsd;
+    int iFuncLit1   = pCut1->iDsd;
+    int nWords      = Abc_TtWordNum( pCut->nLimit );
+    word * pTruth0s = Vec_MemReadEntry( p->vTtMem, Abc_Lit2Var(iFuncLit0) );
+    word * pTruth1s = Vec_MemReadEntry( p->vTtMem, Abc_Lit2Var(iFuncLit1) );
+    word * pTruth0  = (word *)p->puTemp[0];
+    word * pTruth1  = (word *)p->puTemp[1];
+    word * pTruth   = (word *)p->puTemp[2];
+    Abc_TtCopy( pTruth0, pTruth0s, nWords, fCompl0 ^ pCut0->fCompl ^ Abc_LitIsCompl(iFuncLit0) );
+    Abc_TtCopy( pTruth1, pTruth1s, nWords, fCompl1 ^ pCut1->fCompl ^ Abc_LitIsCompl(iFuncLit1) );
+    Abc_TtStretch( pTruth0, pCut->nLimit, pCut0->pLeaves, pCut0->nLeaves, pCut->pLeaves, pCut->nLeaves );
+    Abc_TtStretch( pTruth1, pCut->nLimit, pCut1->pLeaves, pCut1->nLeaves, pCut->pLeaves, pCut->nLeaves );
+    fCompl         = (pTruth0[0] & pTruth1[0] & 1);
+    Abc_TtAnd( pTruth, pTruth0, pTruth1, nWords, fCompl );
+    pCut->nLeaves  = Abc_TtMinBase( pTruth, pCut->pLeaves, pCut->nLeaves );
+    truthId        = Vec_MemHashInsert( p->vTtMem, pTruth );
+    pCut->iDsd     = Abc_Var2Lit( truthId, fCompl );
+    assert( (pTruth[0] & 1) == 0 );
+    return 1;
+}
+*/
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/misc/extra/extra.h b/src/misc/extra/extra.h
index f4dcd154..982a6f5e 100644
--- a/src/misc/extra/extra.h
+++ b/src/misc/extra/extra.h
@@ -226,6 +226,7 @@ extern int         Sdm_ManReadDsdAndNum( Sdm_Man_t * p, int iDsd );
 extern int         Sdm_ManReadDsdClauseNum( Sdm_Man_t * p, int iDsd );
 extern word        Sdm_ManReadDsdTruth( Sdm_Man_t * p, int iDsd );
 extern char *      Sdm_ManReadDsdStr( Sdm_Man_t * p, int iDsd );
+extern void        Sdm_ManReadCnfCosts( Sdm_Man_t * p, int * pCosts, int nCosts );
 
 /*=== extraUtilProgress.c ================================================================*/
 
diff --git a/src/misc/extra/extraUtilDsd.c b/src/misc/extra/extraUtilDsd.c
index 1af58940..a349ff9f 100644
--- a/src/misc/extra/extraUtilDsd.c
+++ b/src/misc/extra/extraUtilDsd.c
@@ -1014,6 +1014,14 @@ char * Sdm_ManReadDsdStr( Sdm_Man_t * p, int iDsd )
 {
     return p->pDsd6[iDsd].pStr;
 }
+void Sdm_ManReadCnfCosts( Sdm_Man_t * p, int * pCosts, int nCosts )
+{
+    int i;
+    assert( nCosts == DSD_CLASS_NUM );
+    pCosts[0] = pCosts[1] = 0;
+    for ( i = 2; i < DSD_CLASS_NUM; i++ )
+        pCosts[i] = Sdm_ManReadDsdClauseNum( p, i );
+}
 
 
 /**Function*************************************************************
@@ -1104,6 +1112,46 @@ void Sdm_ManTest()
     Sdm_ManFree( p );
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+/*
+void Sdm_ManCompareCnfSizes()
+{
+    Vec_Int_t * vMemory;
+    word uTruth;
+    int i, nSop0, nSop1, nVars, nCla, RetValue;
+    vMemory = Vec_IntAlloc( 1 << 16 );
+    for ( i = 1; i < DSD_CLASS_NUM; i++ )
+    {
+        uTruth = Sdm_ManReadDsdTruth( s_SdmMan, i );
+        nVars = Sdm_ManReadDsdVarNum( s_SdmMan, i );
+        nCla = Sdm_ManReadDsdClauseNum( s_SdmMan, i );
+
+        RetValue = Kit_TruthIsop( &uTruth, nVars, vMemory, 0 );
+        nSop0 = Vec_IntSize(vMemory);
+
+        uTruth = ~uTruth;
+        RetValue = Kit_TruthIsop( &uTruth, nVars, vMemory, 0 );
+        nSop1 = Vec_IntSize(vMemory);
+
+        if ( nSop0 + nSop1 != nCla )
+            printf( "Class %4d : %d + %d != %d\n", i, nSop0, nSop1, nCla );
+        else
+            printf( "Class %4d : %d + %d == %d\n", i, nSop0, nSop1, nCla );
+    }
+    Vec_IntFree( vMemory );
+}
+*/
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////