Version abc70703

4 files changed, 486 insertions, 37 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 36311596..d5bdd444 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -331,7 +331,10 @@ void Abc_Init( Abc_Frame_t * pAbc )
 //    Kit_TruthCountMintermsPrecomp();
 //    Kit_DsdPrecompute4Vars();
 
-    Dar_LibStart();
+    {
+        extern void Dar_LibStart();
+        Dar_LibStart();
+    }
 } 
 
 /**Function*************************************************************
@@ -347,7 +350,10 @@ void Abc_Init( Abc_Frame_t * pAbc )
 ***********************************************************************/
 void Abc_End()
 {
-    Dar_LibStop();
+    {
+        extern void Dar_LibStop();
+        Dar_LibStop();
+    }
 
     Abc_NtkFraigStoreClean();
 //    Rwt_Man4ExplorePrint();
@@ -2915,7 +2921,7 @@ int Abc_CommandLutpack( Abc_Frame_t * pAbc, int argc, char ** argv )
     memset( pPars, 0, sizeof(Lut_Par_t) );
     pPars->nLutsMax     =  4; // (N) the maximum number of LUTs in the structure
     pPars->nLutsOver    =  3; // (Q) the maximum number of LUTs not in the MFFC
-    pPars->nVarsShared  =  0; // (S) the maximum number of shared variables (crossbars)
+    pPars->nVarsShared  =  3; // (S) the maximum number of shared variables (crossbars)
     pPars->nGrowthLevel =  1;
     pPars->fSatur       =  1;
     pPars->fZeroCost    =  0; 
@@ -5942,6 +5948,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
     extern void Abc_NtkCompareSupports( Abc_Ntk_t * pNtk );
     extern void Abc_NtkCompareCones( Abc_Ntk_t * pNtk );
     extern Abc_Ntk_t * Abc_NtkDar( Abc_Ntk_t * pNtk );
+    extern Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
@@ -6057,7 +6064,8 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( pErr, "Network should be strashed. Command has failed.\n" );
         return 1;
     }
-    pNtkRes = Abc_NtkDar( pNtk );
+//    pNtkRes = Abc_NtkDar( pNtk );
+    pNtkRes = Abc_NtkDarToCnf( pNtk, "any.cnf" );
     if ( pNtkRes == NULL )
     {
         fprintf( pErr, "Command has failed.\n" );
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index a936f9bf..c2988cbb 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -20,6 +20,7 @@
 
 #include "abc.h"
 #include "dar.h"
+#include "cnf.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -317,6 +318,130 @@ Dar_CnfFree( pCnf );
 }
 
 
+/**Function*************************************************************
+
+  Synopsis    [Gives the current ABC network to AIG manager for processing.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkConstructFromCnf( Abc_Ntk_t * pNtk, Cnf_Man_t * p, Vec_Ptr_t * vMapped )
+{
+    Abc_Ntk_t * pNtkNew;
+    Abc_Obj_t * pNode, * pNodeNew;
+    Dar_Obj_t * pObj, * pLeaf;
+    Cnf_Cut_t * pCut;
+    Vec_Int_t * vCover;
+    unsigned uTruth;
+    int i, k, nDupGates;
+    // create the new network
+    pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_SOP );
+    // make the mapper point to the new network
+    Dar_ManConst1(p->pManAig)->pData = Abc_NtkCreateNodeConst1(pNtkNew);
+    Abc_NtkForEachCi( pNtk, pNode, i )
+        Dar_ManPi(p->pManAig, i)->pData = pNode->pCopy;
+    // process the nodes in topological order
+    vCover = Vec_IntAlloc( 1 << 16 );
+    Vec_PtrForEachEntry( vMapped, pObj, i )
+    {
+        // create new node
+        pNodeNew = Abc_NtkCreateNode( pNtkNew );
+        // add fanins according to the cut
+        pCut = pObj->pData;
+        Cnf_CutForEachLeaf( p->pManAig, pCut, pLeaf, k )
+            Abc_ObjAddFanin( pNodeNew, pLeaf->pData );
+        // add logic function
+        if ( pCut->nFanins < 5 )
+        {
+            uTruth = 0xFFFF & *Cnf_CutTruth(pCut);
+            Cnf_SopConvertToVector( p->pSops[uTruth], p->pSopSizes[uTruth], vCover );
+            pNodeNew->pData = Abc_SopCreateFromIsop( pNtkNew->pManFunc, pCut->nFanins, vCover );
+        }
+        else
+            pNodeNew->pData = Abc_SopCreateFromIsop( pNtkNew->pManFunc, pCut->nFanins, pCut->vIsop[1] );
+        // save the node
+        pObj->pData = pNodeNew;
+    }
+    Vec_IntFree( vCover );
+    // add the CO drivers
+    Abc_NtkForEachCo( pNtk, pNode, i )
+    {
+        pObj = Dar_ManPo(p->pManAig, i);
+        pNodeNew = Abc_ObjNotCond( Dar_ObjFanin0(pObj)->pData, Dar_ObjFaninC0(pObj) );
+        Abc_ObjAddFanin( pNode->pCopy, pNodeNew );
+    }
+
+    // remove the constant node if not used
+    pNodeNew = (Abc_Obj_t *)Dar_ManConst1(p->pManAig)->pData;
+    if ( Abc_ObjFanoutNum(pNodeNew) == 0 )
+        Abc_NtkDeleteObj( pNodeNew );
+    // minimize the node
+//    Abc_NtkSweep( pNtkNew, 0 );
+    // decouple the PO driver nodes to reduce the number of levels
+    nDupGates = Abc_NtkLogicMakeSimpleCos( pNtkNew, 1 );
+//    if ( nDupGates && If_ManReadVerbose(pIfMan) )
+//        printf( "Duplicated %d gates to decouple the CO drivers.\n", nDupGates );
+    if ( !Abc_NtkCheck( pNtkNew ) )
+        fprintf( stdout, "Abc_NtkConstructFromCnf(): Network check has failed.\n" );
+    return pNtkNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Gives the current ABC network to AIG manager for processing.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName )
+{
+    Abc_Ntk_t * pNtkNew = NULL;
+    Cnf_Man_t * pCnf;
+    Dar_Man_t * pMan;
+    Cnf_Dat_t * pData;
+    assert( Abc_NtkIsStrash(pNtk) );
+    // convert to the AIG manager
+    pMan = Abc_NtkToDar( pNtk );
+    if ( pMan == NULL )
+        return NULL;
+    if ( !Dar_ManCheck( pMan ) )
+    {
+        printf( "Abc_NtkDarToCnf: AIG check has failed.\n" );
+        Dar_ManStop( pMan );
+        return NULL;
+    }
+    // perform balance
+    Dar_ManPrintStats( pMan );
+
+    // derive CNF
+    pCnf = Cnf_ManStart();
+    pData = Cnf_Derive( pCnf, pMan );
+
+    {
+        Vec_Ptr_t * vMapped;
+        vMapped = Cnf_ManScanMapping( pCnf, 1 );
+        pNtkNew = Abc_NtkConstructFromCnf( pNtk, pCnf, vMapped );
+        Vec_PtrFree( vMapped );
+    }
+
+    Dar_ManStop( pMan );
+    Cnf_ManStop( pCnf );
+
+    // write CNF into a file
+//    Cnf_DataWriteIntoFile( pData, pFileName );
+    Cnf_DataFree( pData );
+
+    return pNtkNew;
+}
+
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/base/abci/abcDsdRes.c b/src/base/abci/abcDsdRes.c
index 83e1c241..3aa71a15 100644
--- a/src/base/abci/abcDsdRes.c
+++ b/src/base/abci/abcDsdRes.c
@@ -69,6 +69,7 @@ struct Lut_Man_t_
     Vec_Int_t *  vCover; 
     Vec_Vec_t *  vLevels;
     // temporary variables
+    int          fCofactoring;          // working in the cofactoring mode
     int          pRefs[LUT_SIZE_MAX];   // fanin reference counters 
     int          pCands[LUT_SIZE_MAX];  // internal nodes pointing only to the leaves
     // truth table representation
@@ -106,6 +107,8 @@ static inline int         If_IsComplement( If_Obj_t * p )   { return (int )(((un
 
 extern void Res_UpdateNetworkLevel( Abc_Obj_t * pObjNew, Vec_Vec_t * vLevels );
 
+static If_Obj_t * Abc_LutIfManMapMulti( Lut_Man_t * p, unsigned * pTruth, int nLeaves, If_Obj_t ** ppLeaves );
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -1003,62 +1006,81 @@ If_Obj_t * Abc_LutIfManMap_New_rec( Lut_Man_t * p, Kit_DsdNtk_t * pNtk, int iLit
   SeeAlso     []
 
 ***********************************************************************/
-/*
 int Abc_LutFindBestCofactoring( Lut_Man_t * p, Kit_DsdNtk_t * pNtk, unsigned * pTruth, int nVars )
 {
-    Kit_DsdNtk_t * pNtk0, * pNtk1, * pTemp;
-//    Kit_DsdObj_t * pRoot;
-    unsigned * pCofs2[2] = { pNtk->pMem, pNtk->pMem + Kit_TruthWordNum(pNtk->nVars) };
-    unsigned i, * pTruth;
-    int MaxBlock
-        Verbose = 0;
-    int RetValue = 0;
+    Kit_DsdNtk_t * pNtk0, * pNtk1;//, * pTemp;
+    unsigned * pCofs2[3] = { pNtk->pMem, pNtk->pMem + Kit_TruthWordNum(pNtk->nVars), pNtk->pMem + 2 * Kit_TruthWordNum(pNtk->nVars) };
+    int i, MaxBlock0, MaxBlock1, MaxBlockBest = 1000, VarBest = -1;
+    int fVerbose = 1;
 
     if ( fVerbose )
     {
-        printf( "Function: " );
+//        printf( "Function: " );
 //        Extra_PrintBinary( stdout, pTruth, (1 << nVars) ); 
-        Extra_PrintHexadecimal( stdout, pTruth, nVars ); 
+//        Extra_PrintHexadecimal( stdout, pTruth, nVars ); 
+        printf( "\n" );
         printf( "\n" );
+        printf( "V =%2d: ", pNtk->nVars );
         Kit_DsdPrint( stdout, pNtk );
     }
     for ( i = 0; i < nVars; i++ )
     {
         Kit_TruthCofactor0New( pCofs2[0], pTruth, nVars, i );
-        pNtk0 = Kit_DsdDecompose( pCofs2[0], nVars );
-        pNtk0 = Kit_DsdExpand( pTemp = pNtk0 );
-        Kit_DsdNtkFree( pTemp );
+        Kit_TruthCofactor1New( pCofs2[1], pTruth, nVars, i );
+        Kit_TruthXor( pCofs2[2], pCofs2[0], pCofs2[1], nVars ); 
 
+        pNtk0 = Kit_DsdDecompose( pCofs2[0], nVars );
+        MaxBlock0 = Kit_DsdNonDsdSizeMax( pNtk0 );
+//        pNtk0 = Kit_DsdExpand( pTemp = pNtk0 );
+//        Kit_DsdNtkFree( pTemp );
         if ( fVerbose )
         {
+            printf( "Variable %2d: Diff = %6d.\n", i, Kit_TruthCountOnes(pCofs2[2], nVars) );
+
             printf( "Cof%d0: ", i );
             Kit_DsdPrint( stdout, pNtk0 );
         }
 
-        Kit_TruthCofactor1New( pCofs2[1], pTruth, nVars, i );
         pNtk1 = Kit_DsdDecompose( pCofs2[1], nVars );
-        pNtk1 = Kit_DsdExpand( pTemp = pNtk1 );
-        Kit_DsdNtkFree( pTemp );
-
+        MaxBlock1 = Kit_DsdNonDsdSizeMax( pNtk1 );
+//        pNtk1 = Kit_DsdExpand( pTemp = pNtk1 );
+//        Kit_DsdNtkFree( pTemp );
         if ( fVerbose )
         {
             printf( "Cof%d1: ", i );
             Kit_DsdPrint( stdout, pNtk1 );
         }
 
-        if ( Kit_DsdCheckVar4Dec2( pNtk0, pNtk1 ) )
-            RetValue = 1;
+        if ( fVerbose )
+        {
+            printf( "MaxBlock0 = %2d. MaxBlock1 = %2d. ", MaxBlock0, MaxBlock1 );
+            if ( MaxBlock0 < p->pPars->nLutSize && MaxBlock1 < p->pPars->nLutSize )
+                printf( "  feasible\n" );
+            else
+                printf( "infeasible\n" );
+        }
+
+        if ( MaxBlock0 < p->pPars->nLutSize && MaxBlock1 < p->pPars->nLutSize )
+        {
+            if ( MaxBlockBest > ABC_MAX(MaxBlock0, MaxBlock1) )
+            {
+                MaxBlockBest = ABC_MAX(MaxBlock0, MaxBlock1);
+                VarBest = i;
+            }
+        }
 
         Kit_DsdNtkFree( pNtk0 );
         Kit_DsdNtkFree( pNtk1 );
     }
     if ( fVerbose )
+    {
+        printf( "Best variable = %d.\n", VarBest ); 
         printf( "\n" );
-
-    return RetValue;
-    
+    }
+    return VarBest;
+   
 }
-*/
+
 /**Function*************************************************************
 
   Synopsis    [Prepares the mapping manager.]
@@ -1070,7 +1092,7 @@ int Abc_LutFindBestCofactoring( Lut_Man_t * p, Kit_DsdNtk_t * pNtk, unsigned * p
   SeeAlso     []
 
 ***********************************************************************/
-If_Obj_t * Abc_LutIfManMap_rec( Lut_Man_t * p, Kit_DsdNtk_t * pNtk, int iLit )
+If_Obj_t * Abc_LutIfManMap_rec( Lut_Man_t * p, Kit_DsdNtk_t * pNtk, int iLit, If_Obj_t * pResult )
 {
     Kit_Graph_t * pGraph;
     Kit_DsdObj_t * pObj;
@@ -1092,8 +1114,8 @@ If_Obj_t * Abc_LutIfManMap_rec( Lut_Man_t * p, Kit_DsdNtk_t * pNtk, int iLit )
     if ( pObj->Type == KIT_DSD_AND )
     {
         assert( pObj->nFans == 2 );
-        pFansNew[0] = Abc_LutIfManMap_rec( p, pNtk, pObj->pFans[0] );
-        pFansNew[1] = Abc_LutIfManMap_rec( p, pNtk, pObj->pFans[1] );
+        pFansNew[0] = pResult? pResult : Abc_LutIfManMap_rec( p, pNtk, pObj->pFans[0], NULL );
+        pFansNew[1] = Abc_LutIfManMap_rec( p, pNtk, pObj->pFans[1], NULL );
         if ( pFansNew[0] == NULL || pFansNew[1] == NULL )
             return NULL;
         pObjNew = If_ManCreateAnd( p->pIfMan, If_Regular(pFansNew[0]), If_IsComplement(pFansNew[0]), If_Regular(pFansNew[1]), If_IsComplement(pFansNew[1]) ); 
@@ -1102,8 +1124,8 @@ If_Obj_t * Abc_LutIfManMap_rec( Lut_Man_t * p, Kit_DsdNtk_t * pNtk, int iLit )
     if ( pObj->Type == KIT_DSD_XOR )
     {
         assert( pObj->nFans == 2 );
-        pFansNew[0] = Abc_LutIfManMap_rec( p, pNtk, pObj->pFans[0] );
-        pFansNew[1] = Abc_LutIfManMap_rec( p, pNtk, pObj->pFans[1] );
+        pFansNew[0] = pResult? pResult : Abc_LutIfManMap_rec( p, pNtk, pObj->pFans[0], NULL );
+        pFansNew[1] = Abc_LutIfManMap_rec( p, pNtk, pObj->pFans[1], NULL );
         if ( pFansNew[0] == NULL || pFansNew[1] == NULL )
             return NULL;
         fCompl ^= 1 ^ If_IsComplement(pFansNew[0]) ^ If_IsComplement(pFansNew[1]);
@@ -1116,11 +1138,22 @@ If_Obj_t * Abc_LutIfManMap_rec( Lut_Man_t * p, Kit_DsdNtk_t * pNtk, int iLit )
     // solve for the inputs
     Kit_DsdObjForEachFanin( pNtk, pObj, iLitFanin, i )
     {
-        pFansNew[i] = Abc_LutIfManMap_rec( p, pNtk, iLitFanin );
+        if ( i == 0 )
+            pFansNew[i] = pResult? pResult : Abc_LutIfManMap_rec( p, pNtk, iLitFanin, NULL );
+        else
+            pFansNew[i] = Abc_LutIfManMap_rec( p, pNtk, iLitFanin, NULL );
         if ( pFansNew[i] == NULL )
             return NULL;
     }
 
+    // find best cofactoring variable
+//    if ( pObj->nFans > 3 )
+//        Kit_DsdCofactoring( Kit_DsdObjTruth(pObj), pObj->nFans, NULL, 4, 1 );
+    if ( !p->fCofactoring && p->pPars->nVarsShared > 0 && (int)pObj->nFans > p->pPars->nLutSize )
+//        return Abc_LutIfManMapMulti( p, Kit_DsdObjTruth(pObj), pObj->nFans, pFansNew );
+        Abc_LutIfManMapMulti( p, Kit_DsdObjTruth(pObj), pObj->nFans, pFansNew );
+
+
     // derive the factored form
     pGraph = Kit_TruthToGraph( Kit_DsdObjTruth(pObj), pObj->nFans, p->vCover );
     if ( pGraph == NULL )
@@ -1194,7 +1227,7 @@ int Abc_LutCutUpdate( Lut_Man_t * p, Lut_Cut_t * pCut, Kit_DsdNtk_t * pNtk )
     If_ManSetupCiCutSets( p->pIfMan );
     // create the internal nodes
 //    pDriver = Abc_LutIfManMap_New_rec( p, pNtk, pNtk->Root );
-    pDriver = Abc_LutIfManMap_rec( p, pNtk, pNtk->Root );
+    pDriver = Abc_LutIfManMap_rec( p, pNtk, pNtk->Root, NULL );
     if ( pDriver == NULL )
         return 0;
     // create the PO node
@@ -1460,6 +1493,280 @@ int Abc_LutResynthesize( Abc_Ntk_t * pNtk, Lut_Par_t * pPars )
     return 1;
 }
 
+
+
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Records variable order.]
+
+  Description [Increaments Order[x][y] by 1 if x should be above y in the DSD.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_LutCreateVarOrder( Kit_DsdNtk_t * pNtk, char pTable[][16] )
+{
+    Kit_DsdObj_t * pObj;
+    unsigned uSuppFanins, k;
+    int Above[16], Below[16];
+    int nAbove, nBelow, iFaninLit, i, x, y;
+    // iterate through the nodes
+    Kit_DsdNtkForEachObj( pNtk, pObj, i )
+    {
+        // collect fanin support of this node
+        nAbove = 0;
+        uSuppFanins = 0;
+        Kit_DsdObjForEachFanin( pNtk, pObj, iFaninLit, k )
+        {
+            if ( Kit_DsdLitIsLeaf( pNtk, iFaninLit ) )
+                Above[nAbove++] = Kit_DsdLit2Var(iFaninLit);
+            else
+                uSuppFanins |= Kit_DsdLitSupport( pNtk, iFaninLit );
+        }
+        // find the below variables
+        nBelow = 0;
+        for ( y = 0; y < 16; y++ )
+            if ( uSuppFanins & (1 << y) )
+                Below[nBelow++] = y;
+        // create all pairs
+        for ( x = 0; x < nAbove; x++ )
+            for ( y = 0; y < nBelow; y++ )
+                pTable[Above[x]][Below[y]]++;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates commmon variable order.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_LutCreateCommonOrder( char pTable[][16], int pOrder[], int nLeaves )
+{
+    int Score[16] = {0};
+    int i, y, x;
+    // compute scores for each leaf
+    for ( i = 0; i < nLeaves; i++ )
+    {
+        for ( y = 0; y < nLeaves; y++ )
+            Score[i] += pTable[i][y];
+        for ( x = 0; x < nLeaves; x++ )
+            Score[i] -= pTable[x][i];
+    }
+/*
+    printf( "Scores: " );
+    for ( i = 0; i < nLeaves; i++ )
+        printf( "%d ", Score[i] );
+    printf( "\n" );
+*/
+    // sort the scores
+    Extra_BubbleSort( pOrder, Score, nLeaves, 0 );
+/*
+    printf( "Scores: " );
+    for ( i = 0; i < nLeaves; i++ )
+        printf( "%d ", Score[pOrder[i]] );
+    printf( "\n" );
+*/
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prepares the mapping manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+If_Obj_t * Abc_LutIfManMapMulti_rec( Lut_Man_t * p, Kit_DsdNtk_t ** ppNtks, int * piLits, int * piCofVar, int nCBars, If_Obj_t ** ppLeaves, int nLeaves, int * pOrder )
+{
+    Kit_DsdObj_t * pObj;
+    If_Obj_t * pObjsNew[4][8], * pResPrev;
+    unsigned uSupps[8], uSuppFanin;
+    int piLitsNew[8], pDecision[8] = {0};
+    int i, v, k, nSize = (1 << nCBars);
+
+    // find which of the variables is highest in the order
+
+    // go though non-trivial components
+    for ( i = 0; i < nSize; i++ )
+    {
+        if ( piLits[i] == -1 )
+            continue;
+        pObj = Kit_DsdNtkObj( ppNtks[i], Kit_DsdLit2Var(piLits[i]) );
+        uSuppFanin = pObj? Kit_DsdLitSupport( ppNtks[i], pObj->pFans[0] ) : 0;
+        uSupps[i] = Kit_DsdLitSupport( ppNtks[i], piLits[i] ) & ~uSuppFanin;
+    }
+    // find the variable that appears the highest in the order
+    for ( v = 0; v < nLeaves; v++ )
+    {
+        for ( i = 0; i < nSize; i++ )
+            if ( uSupps[i] & (1 << pOrder[v]) )
+                break;
+    }
+    assert( v < nLeaves );
+    // pull out all components that have this variable
+    for ( i = 0; i < nSize; i++ )
+        pDecision[i] = ( uSupps[i] & (1 << pOrder[v]) );
+
+
+    // iterate over the nodes
+    for ( i = 0; i < nSize; i++ )
+    {
+        pObj = Kit_DsdNtkObj( ppNtks[i], Kit_DsdLit2Var(piLits[i]) );
+        if ( pDecision[i] )
+            piLitsNew[i] = pObj->pFans[0];
+        else
+            piLitsNew[i] = piLits[i];
+    }
+
+    // call again
+    pResPrev = Abc_LutIfManMapMulti_rec( p, ppNtks, piLitsNew, piCofVar, nCBars, ppLeaves, nLeaves, pOrder );
+
+    // create new set of nodes
+    for ( i = 0; i < nSize; i++ )
+    {
+        if ( pDecision[i] )
+            pObjsNew[nCBars][i] = Abc_LutIfManMap_rec( p, ppNtks[i], piLits[i], pResPrev );
+        else
+            pObjsNew[nCBars][i] = pResPrev;
+    }
+
+    // create MUX using these outputs
+    for ( k = nCBars; k > 0; k-- )
+    {
+        nSize /= 2;
+        for ( i = 0; i < nSize; i++ )
+            pObjsNew[k-1][i] = If_ManCreateMnux( p->pIfMan, pObjsNew[k][2*i+0], pObjsNew[k][2*i+1], ppLeaves[piCofVar[k-1]] );
+    }
+    assert( nCBars == 1 && nSize == 1 );
+    return If_NotCond( pObjsNew[0][0], nCBars & 1 );  
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prepares the mapping manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+If_Obj_t * Abc_LutIfManMapMulti( Lut_Man_t * p, unsigned * pTruth, int nVars, If_Obj_t ** ppLeaves )
+{
+    If_Obj_t * pResult;
+    Kit_DsdNtk_t * ppNtks[8] = {0}, * pTemp;
+    int piCofVar[4], pOrder[16] = {0}, pPrios[16], pFreqs[16] = {0}, piLits[16];
+    int i, k, nCBars, nSize, nMemSize;
+    unsigned * ppCofs[4][8], uSupport;
+    char pTable[16][16] = {0};
+    int fVerbose = 1;
+
+    // allocate storage for cofactors
+    nMemSize = Kit_TruthWordNum(nVars);
+    ppCofs[0][0] = ALLOC( unsigned, 32 * nMemSize );
+    nSize = 0;
+    for ( i = 0; i < 4; i++ )
+    for ( k = 0; k < 8; k++ )
+        ppCofs[i][k] = ppCofs[0][0] + nMemSize * nSize++;
+    assert( nSize == 32 );
+
+    // find the best cofactoring variables
+    nCBars = Kit_DsdCofactoring( pTruth, nVars, piCofVar, p->pPars->nVarsShared, 0 );
+
+    // copy the function
+    Kit_TruthCopy( ppCofs[0][0], pTruth, nVars );
+
+    // decompose w.r.t. these variables
+    for ( k = 0; k < nCBars; k++ )
+    {
+        nSize = (1 << k);
+        for ( i = 0; i < nSize; i++ )
+        {
+            Kit_TruthCofactor0New( ppCofs[k+1][2*i+0], ppCofs[k][i], nVars, piCofVar[k] );
+            Kit_TruthCofactor1New( ppCofs[k+1][2*i+1], ppCofs[k][i], nVars, piCofVar[k] );
+        }
+    }
+    nSize = (1 << nCBars);
+    // compute variable frequences
+    for ( i = 0; i < nSize; i++ )
+    {
+        uSupport = Kit_TruthSupport( ppCofs[nCBars][i], nVars );
+        for ( k = 0; k < nVars; k++ )
+            if ( uSupport & (1<<k) )
+                pFreqs[k]++;
+    }
+    // compute DSD networks
+    for ( i = 0; i < nSize; i++ )
+    {
+        ppNtks[i] = Kit_DsdDecompose( ppCofs[nCBars][i], nVars );
+        ppNtks[i] = Kit_DsdExpand( pTemp = ppNtks[i] );
+        Kit_DsdNtkFree( pTemp );
+        if ( fVerbose )
+        {
+            printf( "Cof%d%d: ", nCBars, i );
+            Kit_DsdPrint( stdout, ppNtks[i] );
+        }
+    }
+    free( ppCofs[0][0] );
+
+    // find common variable order
+    for ( i = 0; i < nSize; i++ )
+    {
+        Kit_DsdGetSupports( ppNtks[i] );
+        Abc_LutCreateVarOrder( ppNtks[i], pTable );
+    }
+    Abc_LutCreateCommonOrder( pTable, pOrder, nVars );
+
+    printf( "Common variable order: " );
+    for ( i = 0; i < nVars; i++ )
+        printf( "%c ", 'a' + pOrder[i] );
+    printf( "\n" );
+
+    // derive variable priority
+    for ( i = 0; i < 16; i++ )
+        pPrios[i] = 16;
+    for ( i = 0; i < nVars; i++ )
+        pPrios[pOrder[i]] = i;
+
+    // transform all networks according to the variable order
+    for ( i = 0; i < nSize; i++ )
+    {
+        ppNtks[i] = Kit_DsdShrink( pTemp = ppNtks[i], pPrios );
+        Kit_DsdNtkFree( pTemp );
+        Kit_DsdGetSupports( ppNtks[i] );
+        // undec nodes should be rotated in such a way that the first input has as many shared inputs as possible
+        Kit_DsdRotate( ppNtks[i], pFreqs );
+        // collect the roots
+        piLits[i] = ppNtks[i]->Root;
+    }
+/*
+    p->fCofactoring = 1;
+    pResult = Abc_LutIfManMapMulti_rec( p, ppNtks[nCBars], piLits, piCofVar, nCBars, ppLeaves, nVars, pOrder );
+    p->fCofactoring = 0;
+*/
+    // free the networks
+    for ( i = 0; i < 8; i++ )
+        if ( ppNtks[i] )
+            Kit_DsdNtkFree( ppNtks[i] );
+
+    return pResult;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/io/io.c b/src/base/io/io.c
index 09d1a8a5..e1d4de97 100644
--- a/src/base/io/io.c
+++ b/src/base/io/io.c
@@ -1414,13 +1414,19 @@ int IoCommandWriteCnf( Abc_Frame_t * pAbc, int argc, char **argv )
     char * pFileName;
     int c;
     int fAllPrimes;
+    int fNewAlgo;
+    extern Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName );
 
+    fNewAlgo = 1;
     fAllPrimes = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "ph" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "nph" ) ) != EOF )
     {
         switch ( c )
         {
+            case 'n':
+                fNewAlgo ^= 1;
+                break;
             case 'p':
                 fAllPrimes ^= 1;
                 break;
@@ -1441,15 +1447,18 @@ int IoCommandWriteCnf( Abc_Frame_t * pAbc, int argc, char **argv )
         printf( "Warning: Selected option to write all primes has no effect when deriving CNF from AIG.\n" );
     }
     // call the corresponding file writer
-    if ( fAllPrimes )
+    if ( fNewAlgo )
+        Abc_NtkDarToCnf( pAbc->pNtkCur, pFileName );
+    else if ( fAllPrimes )
         Io_WriteCnf( pAbc->pNtkCur, pFileName, 1 );
     else
         Io_Write( pAbc->pNtkCur, pFileName, IO_FILE_CNF );
     return 0;
 
 usage:
-    fprintf( pAbc->Err, "usage: write_cnf [-ph] <file>\n" );
+    fprintf( pAbc->Err, "usage: write_cnf [-nph] <file>\n" );
     fprintf( pAbc->Err, "\t         write the miter cone into a CNF file\n" );
+    fprintf( pAbc->Err, "\t-n     : toggle using new algorithm [default = %s]\n", fNewAlgo? "yes" : "no" );
     fprintf( pAbc->Err, "\t-p     : toggle using all primes to enhance implicativity [default = %s]\n", fAllPrimes? "yes" : "no" );
     fprintf( pAbc->Err, "\t-h     : print the help massage\n" );
     fprintf( pAbc->Err, "\tfile   : the name of the file to write\n" );