Improving integration of the 'if' mapper with GIA.

6 files changed, 211 insertions, 231 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index f0769e79..952168d2 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -310,7 +310,7 @@ static inline int          Gia_ManMuxNum( Gia_Man_t * p )      { return p->nMuxe
 static inline int          Gia_ManCandNum( Gia_Man_t * p )     { return Gia_ManCiNum(p) + Gia_ManAndNum(p);                                }
 static inline int          Gia_ManConstrNum( Gia_Man_t * p )   { return p->nConstrs;                                                       }
 static inline void         Gia_ManFlipVerbose( Gia_Man_t * p ) { p->fVerbose ^= 1;                                                         } 
-static inline int          Gia_ManWithChoices( Gia_Man_t * p ) { return p->pReprs != NULL;                                                 } 
+static inline int          Gia_ManWithChoices( Gia_Man_t * p ) { return p->pSibls != NULL;                                                 } 
 
 static inline Gia_Obj_t *  Gia_ManConst0( Gia_Man_t * p )      { return p->pObjs;                                                          }
 static inline Gia_Obj_t *  Gia_ManConst1( Gia_Man_t * p )      { return Gia_Not(Gia_ManConst0(p));                                         }
diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c
index 965d6ce3..17440e65 100644
--- a/src/aig/gia/giaDup.c
+++ b/src/aig/gia/giaDup.c
@@ -1875,7 +1875,7 @@ Gia_Man_t * Gia_ManMiter( Gia_Man_t * p0, Gia_Man_t * p1, int nInsDup, int fDual
         Gia_ManForEachCi( p0, pObj, i )
             pObj->Value = Gia_ManAppendCi( pNew );
         Gia_ManForEachCi( p1, pObj, i )
-            if ( i < Gia_ManPiNum(p1) - nInsDup )
+            if ( i < Gia_ManCiNum(p1) - nInsDup )
                 pObj->Value = Gia_ObjToLit( pNew, Gia_ManCi(pNew, i) );
             else
                 pObj->Value = Gia_ManAppendCi( pNew );
diff --git a/src/aig/gia/giaIf.c b/src/aig/gia/giaIf.c
index 10f65af1..e3a78ac9 100644
--- a/src/aig/gia/giaIf.c
+++ b/src/aig/gia/giaIf.c
@@ -408,82 +408,6 @@ int Gia_ManNodeIfSopToGia( Gia_Man_t * pNew, If_Man_t * p, If_Cut_t * pCut, Vec_
 
 /**Function*************************************************************
 
-  Synopsis    [Recursively derives the local AIG for the cut.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Gia_ManNodeIfToGia_rec( Gia_Man_t * pNew, If_Man_t * pIfMan, If_Obj_t * pIfObj, Vec_Ptr_t * vVisited, int fHash )
-{
-    If_Cut_t * pCut;
-    If_Obj_t * pTemp;
-    int iFunc, iFunc0, iFunc1;
-    // get the best cut
-    pCut = If_ObjCutBest(pIfObj);
-    // if the cut is visited, return the result
-    if ( If_CutDataInt(pCut) )
-        return If_CutDataInt(pCut);
-    // mark the node as visited
-    Vec_PtrPush( vVisited, pCut );
-    // insert the worst case
-    If_CutSetDataInt( pCut, ~0 );
-    // skip in case of primary input
-    if ( If_ObjIsCi(pIfObj) )
-        return If_CutDataInt(pCut);
-    // compute the functions of the children
-    for ( pTemp = pIfObj; pTemp; pTemp = pTemp->pEquiv )
-    {
-        iFunc0 = Gia_ManNodeIfToGia_rec( pNew, pIfMan, pTemp->pFanin0, vVisited, fHash );
-        if ( iFunc0 == ~0 )
-            continue;
-        iFunc1 = Gia_ManNodeIfToGia_rec( pNew, pIfMan, pTemp->pFanin1, vVisited, fHash );
-        if ( iFunc1 == ~0 )
-            continue;
-        // both branches are solved
-        if ( fHash )
-            iFunc = Gia_ManHashAnd( pNew, Abc_LitNotCond(iFunc0, pTemp->fCompl0), Abc_LitNotCond(iFunc1, pTemp->fCompl1) ); 
-        else
-            iFunc = Gia_ManAppendAnd( pNew, Abc_LitNotCond(iFunc0, pTemp->fCompl0), Abc_LitNotCond(iFunc1, pTemp->fCompl1) ); 
-        if ( pTemp->fPhase != pIfObj->fPhase )
-            iFunc = Abc_LitNot(iFunc);
-        If_CutSetDataInt( pCut, iFunc );
-        break;
-    }
-    return If_CutDataInt(pCut);
-}
-int Gia_ManNodeIfToGia( Gia_Man_t * pNew, If_Man_t * pIfMan, If_Obj_t * pIfObj, Vec_Int_t * vLeaves, int fHash )
-{
-    If_Cut_t * pCut;
-    If_Obj_t * pLeaf;
-    int i, iRes;
-    // get the best cut
-    pCut = If_ObjCutBest(pIfObj);
-    assert( pCut->nLeaves > 1 );
-    // set the leaf variables
-    If_CutForEachLeaf( pIfMan, pCut, pLeaf, i )
-        If_CutSetDataInt( If_ObjCutBest(pLeaf), Vec_IntEntry(vLeaves, i) );
-    // recursively compute the function while collecting visited cuts
-    Vec_PtrClear( pIfMan->vTemp );
-    iRes = Gia_ManNodeIfToGia_rec( pNew, pIfMan, pIfObj, pIfMan->vTemp, fHash ); 
-    if ( iRes == ~0 )
-    {
-        Abc_Print( -1, "Gia_ManNodeIfToGia(): Computing local AIG has failed.\n" );
-        return ~0;
-    }
-    // clean the cuts
-    If_CutForEachLeaf( pIfMan, pCut, pLeaf, i )
-        If_CutSetDataInt( If_ObjCutBest(pLeaf), 0 );
-    Vec_PtrForEachEntry( If_Cut_t *, pIfMan->vTemp, pCut, i )
-        If_CutSetDataInt( pCut, 0 );
-    return iRes;
-}
-
-/**Function*************************************************************
-
   Synopsis    [Converts IF into GIA manager.]
 
   Description []
@@ -493,7 +417,7 @@ int Gia_ManNodeIfToGia( Gia_Man_t * pNew, If_Man_t * pIfMan, If_Obj_t * pIfObj,
   SeeAlso     []
 
 ***********************************************************************/
-Gia_Man_t * Gia_ManFromIf( If_Man_t * pIfMan )
+Gia_Man_t * Gia_ManFromIfAig( If_Man_t * pIfMan )
 {
     int fHash = 0;
     Gia_Man_t * pNew;
@@ -501,10 +425,9 @@ Gia_Man_t * Gia_ManFromIf( If_Man_t * pIfMan )
     If_Cut_t * pCutBest;
     Vec_Int_t * vLeaves;
     Vec_Int_t * vCover;
-    unsigned * pTruth;
-    int Counter, iOffset, nItems = 0;
-    int i, k, w, GiaId;
+    int i, k;
     assert( pIfMan->pPars->pLutStruct == NULL );
+    assert( pIfMan->pPars->fDelayOpt || pIfMan->pPars->fUserRecLib );
     // create new manager
     pNew = Gia_ManStart( If_ManObjNum(pIfMan) );
     Gia_ManHashAlloc( pNew );
@@ -524,137 +447,23 @@ Gia_Man_t * Gia_ManFromIf( If_Man_t * pIfMan )
             If_CutForEachLeaf( pIfMan, pCutBest, pIfLeaf, k )
                 Vec_IntPush( vLeaves, pIfLeaf->iCopy );
             // get the functionality
-            if ( pIfMan->pPars->pLutStruct )
-                pIfObj->iCopy = Kit_TruthToGia( pNew, If_CutTruth(pCutBest), If_CutLeaveNum(pCutBest), vCover, vLeaves, fHash );
-            else if ( pIfMan->pPars->fDelayOpt )
+            if ( pIfMan->pPars->fDelayOpt )
                 pIfObj->iCopy = Gia_ManNodeIfSopToGia( pNew, pIfMan, pCutBest, vLeaves, fHash );
             else if ( pIfMan->pPars->fUserRecLib )
                 pIfObj->iCopy = Abc_RecToGia3( pNew, pIfMan, pCutBest, vLeaves, fHash );
-            else
-                pIfObj->iCopy = Gia_ManNodeIfToGia( pNew, pIfMan, pIfObj, vLeaves, fHash );
-            // complement the node if the TT was used and the cut was complemented
-            if ( pIfMan->pPars->pLutStruct )
-                pIfObj->iCopy = Abc_LitNotCond( pIfObj->iCopy, pCutBest->fCompl );
-            // count entries in the mapping array
-            nItems += 2 + If_CutLeaveNum( pCutBest );
+            else assert( 0 );
         }
         else if ( If_ObjIsCi(pIfObj) )
             pIfObj->iCopy = Gia_ManAppendCi(pNew);
         else if ( If_ObjIsCo(pIfObj) )
             pIfObj->iCopy = Gia_ManAppendCo( pNew, Abc_LitNotCond(If_ObjFanin0(pIfObj)->iCopy, If_ObjFaninC0(pIfObj)) );
         else if ( If_ObjIsConst1(pIfObj) )
-        {
             pIfObj->iCopy = 1;
-            nItems += 2; 
-        }
         else assert( 0 );
     }
     Vec_IntFree( vCover );
     Vec_IntFree( vLeaves );
     Gia_ManHashStop( pNew );
-
-    // GIA after mapping with choices may end up with dangling nodes
-    // which participate as leaves of some cuts used in the mapping
-    // such nodes are marked here and skipped when mapping is derived
-    Counter = Gia_ManMarkDangling(pNew);
-//    if ( pIfMan->pPars->fVerbose && Counter )
-    if ( Counter )
-        printf( "GIA after mapping has %d dangling nodes.\n", Counter );
-
-    // create mapping
-    iOffset = Gia_ManObjNum(pNew);
-    pNew->pMapping = ABC_CALLOC( int, iOffset + nItems );
-    assert( pNew->vTruths == NULL );
-    if ( pIfMan->pPars->pLutStruct )
-        pNew->vTruths = Vec_IntAlloc( 1000 );
-    If_ManForEachObj( pIfMan, pIfObj, i )
-    {
-        if ( pIfObj->nRefs == 0 && !If_ObjIsTerm(pIfObj) )
-            continue;
-        if ( If_ObjIsAnd(pIfObj) )
-        { 
-            GiaId = Abc_Lit2Var( pIfObj->iCopy );
-            if ( !Gia_ObjIsAnd(Gia_ManObj(pNew, GiaId)) ) // skip trivial node
-                continue;
-            assert( Gia_ObjIsAnd(Gia_ManObj(pNew, GiaId)) );
-            if ( !Gia_ManObj(pNew, GiaId)->fMark0 ) // skip dangling node
-                continue;
-            // get the best cut
-            pCutBest = If_ObjCutBest( pIfObj );
-            // copy the truth tables
-            pTruth = NULL;
-            if ( pNew->vTruths )
-            { 
-                // copy truth table
-                for ( w = 0; w < pIfMan->nTruthWords; w++ )
-                    Vec_IntPush( pNew->vTruths, If_CutTruth(pCutBest)[w] );
-                pTruth = (unsigned *)(Vec_IntArray(pNew->vTruths) + Vec_IntSize(pNew->vTruths) - pIfMan->nTruthWords);
-                // complement 
-                if ( pCutBest->fCompl ^ Abc_LitIsCompl(pIfObj->iCopy) )
-                    for ( w = 0; w < pIfMan->nTruthWords; w++ )
-                        pTruth[w] = ~pTruth[w];
-            }
-            // create node
-            pNew->pMapping[GiaId]     = iOffset;
-            pNew->pMapping[iOffset++] = If_CutLeaveNum(pCutBest);
-            If_CutForEachLeaf( pIfMan, pCutBest, pIfLeaf, k )
-            {
-                int FaninId = Abc_Lit2Var(pIfLeaf->iCopy);
-                if ( pTruth && Abc_LitIsCompl(pIfLeaf->iCopy) )
-                    Kit_TruthChangePhase( pTruth, If_CutLeaveNum(pCutBest), k );
-                if ( !Gia_ManObj(pNew, FaninId)->fMark0 ) // skip dangling node
-                {
-                    // update truth table
-                    if ( pTruth )
-                    {
-                        extern void If_CluSwapVars( word * pTruth, int nVars, int * V2P, int * P2V, int iVar, int jVar );
-                        if ( If_CutLeaveNum(pCutBest) >= 6 )
-                            If_CluSwapVars( (word*)pTruth, If_CutLeaveNum(pCutBest), NULL, NULL, k, If_CutLeaveNum(pCutBest)-1 );
-                        else
-                        {
-                            word Truth = ((word)pTruth[0] << 32) | (word)pTruth[0];
-                            If_CluSwapVars( &Truth, 6, NULL, NULL, k, If_CutLeaveNum(pCutBest)-1 );
-                            pTruth[0] = (Truth & 0xFFFFFFFF);
-                        }
-                    }
-                    pNew->pMapping[iOffset-k-1]--;
-                    continue;
-                }
-                assert( FaninId < GiaId );
-                pNew->pMapping[iOffset++] = FaninId;
-            }
-            pNew->pMapping[iOffset++] = GiaId;
-        }
-        else if ( If_ObjIsConst1(pIfObj) )
-        {
-            // create node
-            pNew->pMapping[0] = iOffset;
-            pNew->pMapping[iOffset++] = 0;
-            pNew->pMapping[iOffset++] = 0;
-/*
-            if ( pNew->vTruths )
-            {
-                printf( "%d ", nLeaves );
-                for ( w = 0; w < pIfMan->nTruthWords; w++ )
-                    Vec_IntPush( pNew->vTruths, 0 );
-            }
-*/
-        }
-    }
-    pNew->nOffset = iOffset;
-    Gia_ManCleanMark0( pNew );
-//    assert( iOffset == Gia_ManObjNum(pNew) + nItems );
-//    if ( pIfMan->pManTim )
-//        pNew->pManTime = Tim_ManDup( pIfMan->pManTim, 0 );
-    // verify that COs have mapping
-    {
-        Gia_Obj_t * pObj;
-        Gia_ManForEachCo( pNew, pObj, i )
-        {
-            if ( Gia_ObjIsAnd(Gia_ObjFanin0(pObj)) )
-                assert( pNew->pMapping[Gia_ObjFaninId0p(pNew, pObj)] != 0 );
-        }
-    }
     return pNew;
 }
 
@@ -670,15 +479,15 @@ Gia_Man_t * Gia_ManFromIf( If_Man_t * pIfMan )
   SeeAlso     []
 
 ***********************************************************************/
-int Gia_ManFromIfStrCreateLut( Gia_Man_t * pNew, word * pRes, Vec_Int_t * vLeaves, Vec_Int_t * vCover, Vec_Int_t * vMapping, Vec_Int_t * vMapping2 )
+int Gia_ManFromIfLogicCreateLut( Gia_Man_t * pNew, word * pRes, Vec_Int_t * vLeaves, Vec_Int_t * vCover, Vec_Int_t * vMapping, Vec_Int_t * vMapping2 )
 {
     int i, iLit, iObjLit1;
     iObjLit1 = Kit_TruthToGia( pNew, (unsigned *)pRes, Vec_IntSize(vLeaves), vCover, vLeaves, 0 );
     // write mapping
     Vec_IntSetEntry( vMapping, Abc_Lit2Var(iObjLit1), Vec_IntSize(vMapping2) );
     Vec_IntPush( vMapping2, Vec_IntSize(vLeaves) );
-    Vec_IntForEachEntry( vLeaves, iLit, i )
-        assert( Abc_Lit2Var(iLit) < Abc_Lit2Var(iObjLit1) );
+//    Vec_IntForEachEntry( vLeaves, iLit, i )
+//        assert( Abc_Lit2Var(iLit) < Abc_Lit2Var(iObjLit1) );
     Vec_IntForEachEntry( vLeaves, iLit, i )
         Vec_IntPush( vMapping2, Abc_Lit2Var(iLit)  );
     Vec_IntPush( vMapping2, Abc_Lit2Var(iObjLit1) );
@@ -697,11 +506,37 @@ int Gia_ManFromIfStrCreateLut( Gia_Man_t * pNew, word * pRes, Vec_Int_t * vLeave
   SeeAlso     []
 
 ***********************************************************************/
-int Gia_ManFromIfStrNode( Gia_Man_t * pNew, int iObj, Vec_Int_t * vLeaves, Vec_Int_t * vLeavesTemp, 
+int Gia_ManFromIfLogicNode( Gia_Man_t * pNew, int iObj, Vec_Int_t * vLeaves, Vec_Int_t * vLeavesTemp, 
     word * pRes, char * pStr, Vec_Int_t * vCover, Vec_Int_t * vMapping, Vec_Int_t * vMapping2, Vec_Int_t * vPacking )
 {
     int nLeaves = Vec_IntSize(vLeaves);
     int i, Length, nLutLeaf, nLutLeaf2, nLutRoot, iObjLit1, iObjLit2, iObjLit3;
+    // check simple case
+    static word s_Truths6[6] = {
+        ABC_CONST(0xAAAAAAAAAAAAAAAA),
+        ABC_CONST(0xCCCCCCCCCCCCCCCC),
+        ABC_CONST(0xF0F0F0F0F0F0F0F0),
+        ABC_CONST(0xFF00FF00FF00FF00),
+        ABC_CONST(0xFFFF0000FFFF0000),
+        ABC_CONST(0xFFFFFFFF00000000)
+    };
+/*
+    if ( *pRes == 0 || ~*pRes == 0 )
+        return Abc_LitNotCond( 0, ~*pRes == 0 );
+    for ( i = 0; i < Vec_IntSize(vLeaves); i++ )
+        if ( *pRes == s_Truths6[i] || ~*pRes == s_Truths6[i] )
+            return Abc_LitNotCond( Vec_IntEntry(vLeaves, i), ~*pRes == s_Truths6[i] );
+*/
+/*
+    if ( *pRes == 0 || ~*pRes == 0 )
+        printf( "Const\n" );
+    for ( i = 0; i < Vec_IntSize(vLeaves); i++ )
+        if ( *pRes == s_Truths6[i] || ~*pRes == s_Truths6[i] )
+            printf( "Literal\n" );
+*/
+    // check if there is no LUT structures
+    if ( pStr == NULL )
+        return Gia_ManFromIfLogicCreateLut( pNew, pRes, vLeaves, vCover, vMapping, vMapping2 );
 
     // quit if parameters are wrong
     Length = strlen(pStr);
@@ -730,7 +565,7 @@ int Gia_ManFromIfStrNode( Gia_Man_t * pNew, int iObj, Vec_Int_t * vLeaves, Vec_I
     if ( nLeaves <= Abc_MaxInt( nLutLeaf2, Abc_MaxInt(nLutLeaf, nLutRoot) ) )
     {
         // create mapping
-        iObjLit1 = Gia_ManFromIfStrCreateLut( pNew, pRes, vLeaves, vCover, vMapping, vMapping2 );
+        iObjLit1 = Gia_ManFromIfLogicCreateLut( pNew, pRes, vLeaves, vCover, vMapping, vMapping2 );
         // write packing
         Vec_IntPush( vPacking, 1 );
         Vec_IntPush( vPacking, Abc_Lit2Var(iObjLit1) );
@@ -811,7 +646,7 @@ int Gia_ManFromIfStrNode( Gia_Man_t * pNew, int iObj, Vec_Int_t * vLeaves, Vec_I
         Vec_IntClear( vLeavesTemp );
         for ( i = 0; i < pLut1[0]; i++ )
             Vec_IntPush( vLeavesTemp, Vec_IntEntry(vLeaves, pLut1[2+i]) );
-        iObjLit1 = Gia_ManFromIfStrCreateLut( pNew, &Func1, vLeavesTemp, vCover, vMapping, vMapping2 );
+        iObjLit1 = Gia_ManFromIfLogicCreateLut( pNew, &Func1, vLeavesTemp, vCover, vMapping, vMapping2 );
 
         if ( Length == 3 && pLut2[0] > 0 )
         {
@@ -834,7 +669,7 @@ int Gia_ManFromIfStrNode( Gia_Man_t * pNew, int iObj, Vec_Int_t * vLeaves, Vec_I
                     Vec_IntPush( vLeavesTemp, iObjLit1 );
                 else
                     Vec_IntPush( vLeavesTemp, Vec_IntEntry(vLeaves, pLut2[2+i]) );
-            iObjLit2 = Gia_ManFromIfStrCreateLut( pNew, &Func2, vLeavesTemp, vCover, vMapping, vMapping2 );
+            iObjLit2 = Gia_ManFromIfLogicCreateLut( pNew, &Func2, vLeavesTemp, vCover, vMapping, vMapping2 );
 
             // write packing
             Vec_IntPush( vPacking, 3 );
@@ -872,7 +707,7 @@ int Gia_ManFromIfStrNode( Gia_Man_t * pNew, int iObj, Vec_Int_t * vLeaves, Vec_I
                 Vec_IntPush( vLeavesTemp, iObjLit2 );
             else
                 Vec_IntPush( vLeavesTemp, Vec_IntEntry(vLeaves, pLut0[2+i]) );
-        iObjLit3 = Gia_ManFromIfStrCreateLut( pNew, &Func0, vLeavesTemp, vCover, vMapping, vMapping2 );
+        iObjLit3 = Gia_ManFromIfLogicCreateLut( pNew, &Func0, vLeavesTemp, vCover, vMapping, vMapping2 );
 
         // write packing
         Vec_IntPush( vPacking, Abc_Lit2Var(iObjLit3) );
@@ -881,6 +716,81 @@ int Gia_ManFromIfStrNode( Gia_Man_t * pNew, int iObj, Vec_Int_t * vLeaves, Vec_I
     return iObjLit3;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Recursively derives the local AIG for the cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Gia_ManNodeIfToGia_rec( Gia_Man_t * pNew, If_Man_t * pIfMan, If_Obj_t * pIfObj, Vec_Ptr_t * vVisited, int fHash )
+{
+    If_Cut_t * pCut;
+    If_Obj_t * pTemp;
+    int iFunc, iFunc0, iFunc1;
+    // get the best cut
+    pCut = If_ObjCutBest(pIfObj);
+    // if the cut is visited, return the result
+    if ( If_CutDataInt(pCut) )
+        return If_CutDataInt(pCut);
+    // mark the node as visited
+    Vec_PtrPush( vVisited, pCut );
+    // insert the worst case
+    If_CutSetDataInt( pCut, ~0 );
+    // skip in case of primary input
+    if ( If_ObjIsCi(pIfObj) )
+        return If_CutDataInt(pCut);
+    // compute the functions of the children
+    for ( pTemp = pIfObj; pTemp; pTemp = pTemp->pEquiv )
+    {
+        iFunc0 = Gia_ManNodeIfToGia_rec( pNew, pIfMan, pTemp->pFanin0, vVisited, fHash );
+        if ( iFunc0 == ~0 )
+            continue;
+        iFunc1 = Gia_ManNodeIfToGia_rec( pNew, pIfMan, pTemp->pFanin1, vVisited, fHash );
+        if ( iFunc1 == ~0 )
+            continue;
+        // both branches are solved
+        if ( fHash )
+            iFunc = Gia_ManHashAnd( pNew, Abc_LitNotCond(iFunc0, pTemp->fCompl0), Abc_LitNotCond(iFunc1, pTemp->fCompl1) ); 
+        else
+            iFunc = Gia_ManAppendAnd( pNew, Abc_LitNotCond(iFunc0, pTemp->fCompl0), Abc_LitNotCond(iFunc1, pTemp->fCompl1) ); 
+        if ( pTemp->fPhase != pIfObj->fPhase )
+            iFunc = Abc_LitNot(iFunc);
+        If_CutSetDataInt( pCut, iFunc );
+        break;
+    }
+    return If_CutDataInt(pCut);
+}
+int Gia_ManNodeIfToGia( Gia_Man_t * pNew, If_Man_t * pIfMan, If_Obj_t * pIfObj, Vec_Int_t * vLeaves, int fHash )
+{
+    If_Cut_t * pCut;
+    If_Obj_t * pLeaf;
+    int i, iRes;
+    // get the best cut
+    pCut = If_ObjCutBest(pIfObj);
+    assert( pCut->nLeaves > 1 );
+    // set the leaf variables
+    If_CutForEachLeaf( pIfMan, pCut, pLeaf, i )
+        If_CutSetDataInt( If_ObjCutBest(pLeaf), Vec_IntEntry(vLeaves, i) );
+    // recursively compute the function while collecting visited cuts
+    Vec_PtrClear( pIfMan->vTemp );
+    iRes = Gia_ManNodeIfToGia_rec( pNew, pIfMan, pIfObj, pIfMan->vTemp, fHash ); 
+    if ( iRes == ~0 )
+    {
+        Abc_Print( -1, "Gia_ManNodeIfToGia(): Computing local AIG has failed.\n" );
+        return ~0;
+    }
+    // clean the cuts
+    If_CutForEachLeaf( pIfMan, pCut, pLeaf, i )
+        If_CutSetDataInt( If_ObjCutBest(pLeaf), 0 );
+    Vec_PtrForEachEntry( If_Cut_t *, pIfMan->vTemp, pCut, i )
+        If_CutSetDataInt( pCut, 0 );
+    return iRes;
+}
 
 /**Function*************************************************************
 
@@ -893,21 +803,54 @@ int Gia_ManFromIfStrNode( Gia_Man_t * pNew, int iObj, Vec_Int_t * vLeaves, Vec_I
   SeeAlso     []
 
 ***********************************************************************/
-Gia_Man_t * Gia_ManFromIfStr( If_Man_t * pIfMan )
+static inline word Gia_ManTt6Stretch( word t, int nVars )
+{
+    assert( nVars >= 0 );
+    if ( nVars == 0 )
+        nVars++, t = (t & 0x1) | ((t & 0x1) << 1);
+    if ( nVars == 1 )
+        nVars++, t = (t & 0x3) | ((t & 0x3) << 2);
+    if ( nVars == 2 )
+        nVars++, t = (t & 0xF) | ((t & 0xF) << 4);
+    if ( nVars == 3 )
+        nVars++, t = (t & 0xFF) | ((t & 0xFF) << 8);
+    if ( nVars == 4 )
+        nVars++, t = (t & 0xFFFF) | ((t & 0xFFFF) << 16);
+    if ( nVars == 5 )
+        nVars++, t = (t & 0xFFFFFFFF) | ((t & 0xFFFFFFFF) << 32);
+    assert( nVars == 6 );
+    return t;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Converts IF into GIA manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManFromIfLogic( If_Man_t * pIfMan )
 {
     Gia_Man_t * pNew;
     If_Cut_t * pCutBest;
     If_Obj_t * pIfObj, * pIfLeaf;
-    Vec_Int_t * vMapping, * vMapping2, * vPacking;
+    Vec_Int_t * vMapping, * vMapping2, * vPacking = NULL;
     Vec_Int_t * vLeaves, * vLeaves2, * vCover;
+    word Truth = 0, * pTruthTable;
     int i, k, Entry;
-    assert( pIfMan->pPars->pLutStruct != NULL );
-    assert( pIfMan->pPars->nLutSize >= 6 ); // if 5, need to change (word *)If_CutTruth(pCutBest) below
+    assert( !pIfMan->pPars->fDeriveLuts || pIfMan->pPars->fTruth );
     // start mapping and packing
     vMapping  = Vec_IntStart( If_ManObjNum(pIfMan) );
     vMapping2 = Vec_IntStart( 1 );
-    vPacking  = Vec_IntAlloc( 1000 );
-    Vec_IntPush( vPacking, 0 );
+    if ( pIfMan->pPars->fDeriveLuts && pIfMan->pPars->pLutStruct )
+    {
+        vPacking = Vec_IntAlloc( 1000 );
+        Vec_IntPush( vPacking, 0 );
+    }
     // create new manager
     pNew = Gia_ManStart( If_ManObjNum(pIfMan) );
     // iterate through nodes used in the mapping
@@ -926,9 +869,33 @@ Gia_Man_t * Gia_ManFromIfStr( If_Man_t * pIfMan )
             Vec_IntClear( vLeaves );
             If_CutForEachLeaf( pIfMan, pCutBest, pIfLeaf, k )
                 Vec_IntPush( vLeaves, pIfLeaf->iCopy );
-            // perform decomposition of the cut
-            pIfObj->iCopy = Gia_ManFromIfStrNode( pNew, i, vLeaves, vLeaves2, (word *)If_CutTruth(pCutBest), pIfMan->pPars->pLutStruct, vCover, vMapping, vMapping2, vPacking );
-            pIfObj->iCopy = Abc_LitNotCond( pIfObj->iCopy, pCutBest->fCompl );
+            // perform one of the two types of mapping: with and without structures
+            if ( pIfMan->pPars->fDeriveLuts && pIfMan->pPars->fTruth )
+            {
+                // adjust the truth table
+                int nSize = pIfMan->pPars->nLutSize;
+                pTruthTable = (word *)If_CutTruth(pCutBest);
+                if ( nSize < 6 )
+                {
+                    Truth = Gia_ManTt6Stretch( *pTruthTable, nSize );
+                    pTruthTable = &Truth;
+                }
+                // perform decomposition of the cut
+                pIfObj->iCopy = Gia_ManFromIfLogicNode( pNew, i, vLeaves, vLeaves2, pTruthTable, pIfMan->pPars->pLutStruct, vCover, vMapping, vMapping2, vPacking );
+                pIfObj->iCopy = Abc_LitNotCond( pIfObj->iCopy, pCutBest->fCompl );
+            }
+            else
+            {
+                pIfObj->iCopy = Gia_ManNodeIfToGia( pNew, pIfMan, pIfObj, vLeaves, 0 );
+                // write mapping
+                Vec_IntSetEntry( vMapping, Abc_Lit2Var(pIfObj->iCopy), Vec_IntSize(vMapping2) );
+                Vec_IntPush( vMapping2, Vec_IntSize(vLeaves) );
+                Vec_IntForEachEntry( vLeaves, Entry, k )
+                    assert( Abc_Lit2Var(Entry) < Abc_Lit2Var(pIfObj->iCopy) );
+                Vec_IntForEachEntry( vLeaves, Entry, k )
+                    Vec_IntPush( vMapping2, Abc_Lit2Var(Entry)  );
+                Vec_IntPush( vMapping2, Abc_Lit2Var(pIfObj->iCopy) );
+            }
         }
         else if ( If_ObjIsCi(pIfObj) )
             pIfObj->iCopy = Gia_ManAppendCi(pNew);
@@ -1057,7 +1024,8 @@ void Gia_ManTransferMapping( Gia_Man_t * pGia, Gia_Man_t * p )
 {
     Gia_Obj_t * pObj;
     int i, k, iFan;
-    assert( pGia->pMapping != NULL );
+    if ( pGia->pMapping == NULL )
+        return;
     Gia_ManMappingVerify( pGia );
     Vec_IntFreeP( &p->vMapping );
     p->vMapping = Vec_IntAlloc( 2 * Gia_ManObjNum(p) );
@@ -1144,6 +1112,9 @@ Gia_Man_t * Gia_ManPerformMapping( Gia_Man_t * p, void * pp )
     Gia_Man_t * pNew;
     If_Man_t * pIfMan;
     If_Par_t * pPars = (If_Par_t *)pp;
+    // disable cut minimization
+    if ( !(pPars->fDelayOpt || pPars->fUserRecLib) && !pPars->fDeriveLuts )//&& Gia_ManWithChoices(p) )
+        pPars->fCutMin = 0; // not compatible with deriving result
     // reconstruct GIA according to the hierarchy manager
     assert( pPars->pTimesArr == NULL );
     assert( pPars->pTimesReq == NULL );
@@ -1178,19 +1149,16 @@ Gia_Man_t * Gia_ManPerformMapping( Gia_Man_t * p, void * pp )
         return NULL;
     }
     // transform the result of mapping into the new network
-    if ( pIfMan->pPars->pLutStruct )
-        pNew = Gia_ManFromIfStr( pIfMan );
+    if ( pIfMan->pPars->fDelayOpt || pIfMan->pPars->fUserRecLib )
+        pNew = Gia_ManFromIfAig( pIfMan );
     else
-        pNew = Gia_ManFromIf( pIfMan );
+        pNew = Gia_ManFromIfLogic( pIfMan );
     If_ManStop( pIfMan );
     // transfer name
     assert( pNew->pName == NULL );
     pNew->pName = Abc_UtilStrsav( p->pName );
     pNew->pSpec = Abc_UtilStrsav( p->pSpec );
     Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
-    // unmap in case of SOP balancing
-//    if ( pIfMan->pPars->fDelayOpt )
-//        Vec_IntFreeP( &pNew->vMapping );
     // return the original (unmodified by the mapper) timing manager
     pNew->pManTime   = p->pManTime;   p->pManTime   = NULL;
     pNew->pAigExtra  = p->pAigExtra;  p->pAigExtra  = NULL;
@@ -1203,12 +1171,9 @@ Gia_Man_t * Gia_ManPerformMapping( Gia_Man_t * p, void * pp )
     pNew->pManTime   = p->pManTime;   p->pManTime   = NULL;
     pNew->pAigExtra  = p->pAigExtra;  p->pAigExtra  = NULL;
     pNew->nAnd2Delay = p->nAnd2Delay; p->nAnd2Delay = 0;
-//    pNew->vPacking  = p->vPacking;  p->vPacking = NULL;
     Gia_ManStop( p );
-
 //    printf( "PERFORMING VERIFICATION:\n" );
 //    Gia_ManVerifyWithBoxes( pNew, NULL );
-
     return pNew;
 }
 
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index aeb146e2..57cb9739 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -28362,9 +28362,10 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
     char * FileName, * pTemp;
     char ** pArgvNew;
     int c, nArgcNew, fMiter = 0;
+    int fDumpMiter = 0;
     Cec_ManCecSetDefaultParams( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "CTmvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "CTmdvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -28393,6 +28394,9 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'm':
             fMiter ^= 1;
             break;
+        case 'd':
+            fDumpMiter ^= 1;
+            break;
         case 'v':
             pPars->fVerbose ^= 1;
             break;
@@ -28448,6 +28452,11 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
     pMiter = Gia_ManMiter( pAbc->pGia, pSecond, 0, 1, 0, pPars->fVerbose );
     if ( pMiter )
     {
+        if ( fDumpMiter )
+        {
+            Abc_Print( 0, "The verification miter is written into file \"%s\".\n", "cec_miter.aig" );
+            Gia_AigerWrite( pMiter, "cec_miter.aig", 0, 0 );
+        }
         pAbc->Status = Cec_ManVerify( pMiter, pPars );
         Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexComb );
         Gia_ManStop( pMiter );
@@ -28456,11 +28465,12 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &cec [-CT num] [-mvh]\n" );
+    Abc_Print( -2, "usage: &cec [-CT num] [-mdvh]\n" );
     Abc_Print( -2, "\t         new combinational equivalence checker\n" );
     Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit );
     Abc_Print( -2, "\t-T num : approximate runtime limit in seconds [default = %d]\n", pPars->TimeLimit );
     Abc_Print( -2, "\t-m     : toggle miter vs. two circuits [default = %s]\n", fMiter? "miter":"two circuits");
+    Abc_Print( -2, "\t-d     : toggle dumping dual-output miter [default = %s]\n", fDumpMiter? "yes":"no");
     Abc_Print( -2, "\t-v     : toggle verbose output [default = %s]\n", pPars->fVerbose? "yes":"no");
     Abc_Print( -2, "\t-h     : print the command usage\n");
     return 1;
@@ -28824,7 +28834,7 @@ int Abc_CommandAbc9If( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     pPars->pLutLib = (If_LibLut_t *)pAbc->pLibLut;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "KCFAGDEWSqaflepmrsdbgyojikcvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "KCFAGDEWSqaflepmrsdbgyojikczvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -28986,6 +28996,9 @@ int Abc_CommandAbc9If( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'c':
             pPars->fEnableRealPos ^= 1;
             break;
+        case 'z':
+            pPars->fDeriveLuts ^= 1;
+            break;
         case 'v':
             pPars->fVerbose ^= 1;
             break;
@@ -29092,7 +29105,7 @@ int Abc_CommandAbc9If( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     // enable truth table computation if cut minimization is selected
-    if ( pPars->fCutMin )
+    if ( pPars->fCutMin || pPars->fDeriveLuts )
     {
         pPars->fTruth = 1;
         pPars->fExpRed = 0;
@@ -29165,7 +29178,7 @@ usage:
         sprintf(LutSize, "library" );
     else
         sprintf(LutSize, "%d", pPars->nLutSize );
-    Abc_Print( -2, "usage: &if [-KCFAG num] [-DEW float] [-S str] [-qarlepmsdbgyojikcvh]\n" );
+    Abc_Print( -2, "usage: &if [-KCFAG num] [-DEW float] [-S str] [-qarlepmsdbgyojikczvh]\n" );
     Abc_Print( -2, "\t           performs FPGA technology mapping of the network\n" );
     Abc_Print( -2, "\t-K num   : the number of LUT inputs (2 < num < %d) [default = %s]\n", IF_MAX_LUTSIZE+1, LutSize );
     Abc_Print( -2, "\t-C num   : the max number of priority cuts (0 < num < 2^12) [default = %d]\n", pPars->nCutsMax );
@@ -29194,6 +29207,7 @@ usage:
     Abc_Print( -2, "\t-i       : toggles enabling additional check [default = %s]\n", pPars->fEnableCheck08? "yes": "no" );
     Abc_Print( -2, "\t-k       : toggles enabling additional check [default = %s]\n", pPars->fEnableCheck10? "yes": "no" );
     Abc_Print( -2, "\t-c       : toggles enabling additional feature [default = %s]\n", pPars->fEnableRealPos? "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-v       : toggles verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h       : prints the command usage\n");
     return 1;
diff --git a/src/base/abci/abcRec3.c b/src/base/abci/abcRec3.c
index 68bb8cdc..cf90a79d 100644
--- a/src/base/abci/abcRec3.c
+++ b/src/base/abci/abcRec3.c
@@ -1149,7 +1149,7 @@ int Abc_RecToGia3( Gia_Man_t * pMan, If_Man_t * pIfMan, If_Cut_t * pCut, Vec_Int
     assert( Gia_ObjIsAnd(pGiaTemp) );
     iGiaObj = Vec_IntEntry(p->vLabels, Gia_ObjNum(pGia, pGiaTemp) + nLeaves);
     // complement the result if needed
-    return Abc_LitNotCond( iGiaObj,  Gia_ObjFaninC0(pGiaPo) ^ ((uCanonPhase >> nLeaves) & 1) );    
+    return Abc_LitNotCond( iGiaObj,  Gia_ObjFaninC0(pGiaPo) ^ ((uCanonPhase >> nLeaves) & 1) ^ pCut->fCompl );    
 }
 
 
diff --git a/src/map/if/if.h b/src/map/if/if.h
index 902754dd..ca5937fd 100644
--- a/src/map/if/if.h
+++ b/src/map/if/if.h
@@ -119,6 +119,7 @@ struct If_Par_t_
     int                fEnableCheck10;// enable additional checking
     int                fEnableRealPos;// enable additional feature
     int                fUseDsd;       // compute DSD of the cut functions
+    int                fDeriveLuts;   // enables deriving LUT structures
     int                fVerbose;      // the verbosity flag
     char *             pLutStruct;    // LUT structure
     float              WireDelay;     // wire delay