Version abc70121

15 files changed, 559 insertions, 82 deletions

diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index 5774afbc..849a888a 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -570,9 +570,9 @@ extern void               Abc_NtkFraigStoreClean();
 /*=== abcFunc.c ==========================================================*/
 extern int                Abc_NtkSopToBdd( Abc_Ntk_t * pNtk );
 extern DdNode *           Abc_ConvertSopToBdd( DdManager * dd, char * pSop );
-extern char *             Abc_ConvertBddToSop( Extra_MmFlex_t * pMan, DdManager * dd, DdNode * bFuncOn, DdNode * bFuncOnDc, int nFanins, Vec_Str_t * vCube, int fMode );
+extern char *             Abc_ConvertBddToSop( Extra_MmFlex_t * pMan, DdManager * dd, DdNode * bFuncOn, DdNode * bFuncOnDc, int nFanins, int fAllPrimes, Vec_Str_t * vCube, int fMode );
 extern int                Abc_NtkBddToSop( Abc_Ntk_t * pNtk, int fDirect );
-extern void               Abc_NodeBddToCnf( Abc_Obj_t * pNode, Extra_MmFlex_t * pMmMan, Vec_Str_t * vCube, char ** ppSop0, char ** ppSop1 );
+extern void               Abc_NodeBddToCnf( Abc_Obj_t * pNode, Extra_MmFlex_t * pMmMan, Vec_Str_t * vCube, int fAllPrimes, char ** ppSop0, char ** ppSop1 );
 extern int                Abc_CountZddCubes( DdManager * dd, DdNode * zCover );
 extern void               Abc_NtkLogicMakeDirectSops( Abc_Ntk_t * pNtk );
 extern int                Abc_NtkSopToAig( Abc_Ntk_t * pNtk );
@@ -726,7 +726,7 @@ extern int                Abc_NtkRefactor( Abc_Ntk_t * pNtk, int nNodeSizeMax, i
 extern int                Abc_NtkRewrite( Abc_Ntk_t * pNtk, int fUpdateLevel, int fUseZeros, int fVerbose, int fVeryVerbose );
 /*=== abcSat.c ==========================================================*/
 extern int                Abc_NtkMiterSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fJFront, int fVerbose, sint64 * pNumConfs, sint64 * pNumInspects );
-extern solver *           Abc_NtkMiterSatCreate( Abc_Ntk_t * pNtk, int fJFront );
+extern solver *           Abc_NtkMiterSatCreate( Abc_Ntk_t * pNtk, int fJFront, int fAllPrimes );
 /*=== abcSop.c ==========================================================*/
 extern char *             Abc_SopRegister( Extra_MmFlex_t * pMan, char * pName );
 extern char *             Abc_SopStart( Extra_MmFlex_t * pMan, int nCubes, int nVars );
diff --git a/src/base/abc/abcFunc.c b/src/base/abc/abcFunc.c
index 59f736e5..421a64cf 100644
--- a/src/base/abc/abcFunc.c
+++ b/src/base/abc/abcFunc.c
@@ -184,7 +184,7 @@ void Abc_NtkLogicMakeDirectSops( Abc_Ntk_t * pNtk )
         if ( Abc_SopIsComplement(pNode->pData) )
         {
             bFunc = Abc_ConvertSopToBdd( dd, pNode->pData );  Cudd_Ref( bFunc );
-            pNode->pData = Abc_ConvertBddToSop( pNtk->pManFunc, dd, bFunc, bFunc, Abc_ObjFaninNum(pNode), vCube, 1 );
+            pNode->pData = Abc_ConvertBddToSop( pNtk->pManFunc, dd, bFunc, bFunc, Abc_ObjFaninNum(pNode), 0, vCube, 1 );
             Cudd_RecursiveDeref( dd, bFunc );
             assert( !Abc_SopIsComplement(pNode->pData) );
         }
@@ -233,7 +233,7 @@ int Abc_NtkBddToSop( Abc_Ntk_t * pNtk, int fDirect )
     {
         assert( pNode->pData );
         bFunc = pNode->pData;
-        pNode->pNext = (Abc_Obj_t *)Abc_ConvertBddToSop( pManNew, dd, bFunc, bFunc, Abc_ObjFaninNum(pNode), vCube, fMode );
+        pNode->pNext = (Abc_Obj_t *)Abc_ConvertBddToSop( pManNew, dd, bFunc, bFunc, Abc_ObjFaninNum(pNode), 0, vCube, fMode );
         if ( pNode->pNext == NULL )
         {
             Extra_MmFlexStop( pManNew );
@@ -273,7 +273,7 @@ int Abc_NtkBddToSop( Abc_Ntk_t * pNtk, int fDirect )
   SeeAlso     []
 
 ***********************************************************************/
-char * Abc_ConvertBddToSop( Extra_MmFlex_t * pMan, DdManager * dd, DdNode * bFuncOn, DdNode * bFuncOnDc, int nFanins, Vec_Str_t * vCube, int fMode )
+char * Abc_ConvertBddToSop( Extra_MmFlex_t * pMan, DdManager * dd, DdNode * bFuncOn, DdNode * bFuncOnDc, int nFanins, int fAllPrimes, Vec_Str_t * vCube, int fMode )
 {
     int fVerify = 0;
     char * pSop;
@@ -301,6 +301,7 @@ char * Abc_ConvertBddToSop( Extra_MmFlex_t * pMan, DdManager * dd, DdNode * bFun
 
     if ( fMode == -1 )
     { // try both phases
+        assert( fAllPrimes == 0 );
 
         // get the ZDD of the negative polarity
         bCover = Cudd_zddIsop( dd, Cudd_Not(bFuncOnDc), Cudd_Not(bFuncOn), &zCover0 );
@@ -335,20 +336,36 @@ char * Abc_ConvertBddToSop( Extra_MmFlex_t * pMan, DdManager * dd, DdNode * bFun
     else if ( fMode == 0 )
     {
         // get the ZDD of the negative polarity
-        bCover = Cudd_zddIsop( dd, Cudd_Not(bFuncOnDc), Cudd_Not(bFuncOn), &zCover );
-        Cudd_Ref( zCover );
-        Cudd_Ref( bCover );
-        Cudd_RecursiveDeref( dd, bCover );
+        if ( fAllPrimes )
+        {
+            zCover = Extra_zddPrimes( dd, Cudd_Not(bFuncOnDc) ); 
+            Cudd_Ref( zCover );
+        }
+        else
+        {
+            bCover = Cudd_zddIsop( dd, Cudd_Not(bFuncOnDc), Cudd_Not(bFuncOn), &zCover );
+            Cudd_Ref( zCover );
+            Cudd_Ref( bCover );
+            Cudd_RecursiveDeref( dd, bCover );
+        }
         nCubes = Abc_CountZddCubes( dd, zCover );
         fPhase = 0;
     }
     else if ( fMode == 1 )
     {
         // get the ZDD of the positive polarity
-        bCover = Cudd_zddIsop( dd, bFuncOn, bFuncOnDc, &zCover );
-        Cudd_Ref( zCover );
-        Cudd_Ref( bCover );
-        Cudd_RecursiveDeref( dd, bCover );
+        if ( fAllPrimes )
+        {
+            zCover = Extra_zddPrimes( dd, bFuncOnDc ); 
+            Cudd_Ref( zCover );
+        }
+        else
+        {
+            bCover = Cudd_zddIsop( dd, bFuncOn, bFuncOnDc, &zCover );
+            Cudd_Ref( zCover );
+            Cudd_Ref( bCover );
+            Cudd_RecursiveDeref( dd, bCover );
+        }
         nCubes = Abc_CountZddCubes( dd, zCover );
         fPhase = 1;
     }
@@ -462,11 +479,11 @@ int Abc_ConvertZddToSop( DdManager * dd, DdNode * zCover, char * pSop, int nFani
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NodeBddToCnf( Abc_Obj_t * pNode, Extra_MmFlex_t * pMmMan, Vec_Str_t * vCube, char ** ppSop0, char ** ppSop1 )
+void Abc_NodeBddToCnf( Abc_Obj_t * pNode, Extra_MmFlex_t * pMmMan, Vec_Str_t * vCube, int fAllPrimes, char ** ppSop0, char ** ppSop1 )
 {
     assert( Abc_NtkIsBddLogic(pNode->pNtk) ); 
-    *ppSop0 = Abc_ConvertBddToSop( pMmMan, pNode->pNtk->pManFunc, pNode->pData, pNode->pData, Abc_ObjFaninNum(pNode), vCube, 0 );
-    *ppSop1 = Abc_ConvertBddToSop( pMmMan, pNode->pNtk->pManFunc, pNode->pData, pNode->pData, Abc_ObjFaninNum(pNode), vCube, 1 );
+    *ppSop0 = Abc_ConvertBddToSop( pMmMan, pNode->pNtk->pManFunc, pNode->pData, pNode->pData, Abc_ObjFaninNum(pNode), fAllPrimes, vCube, 0 );
+    *ppSop1 = Abc_ConvertBddToSop( pMmMan, pNode->pNtk->pManFunc, pNode->pData, pNode->pData, Abc_ObjFaninNum(pNode), fAllPrimes, vCube, 1 );
 }
 
 
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index ff63bbd9..f6c180da 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -72,6 +72,7 @@ static int Abc_CommandComb           ( Abc_Frame_t * pAbc, int argc, char ** arg
 static int Abc_CommandMiter          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandDemiter        ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandOrPos          ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAndPos         ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAppend         ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandFrames         ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandSop            ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -207,6 +208,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Various",      "miter",         Abc_CommandMiter,            1 );
     Cmd_CommandAdd( pAbc, "Various",      "demiter",       Abc_CommandDemiter,          1 );
     Cmd_CommandAdd( pAbc, "Various",      "orpos",         Abc_CommandOrPos,            1 );
+    Cmd_CommandAdd( pAbc, "Various",      "andpos",        Abc_CommandAndPos,           1 );
     Cmd_CommandAdd( pAbc, "Various",      "append",        Abc_CommandAppend,           1 );
     Cmd_CommandAdd( pAbc, "Various",      "frames",        Abc_CommandFrames,           1 );
     Cmd_CommandAdd( pAbc, "Various",      "sop",           Abc_CommandSop,              0 );
@@ -2038,25 +2040,30 @@ int Abc_CommandRenode( Abc_Frame_t * pAbc, int argc, char ** argv )
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk, * pNtkRes;
     int nLutSize, nCutsMax, c;
+    int nFlowIters, nAreaIters;
     int fArea;
     int fUseBdds;
     int fUseSops;
+    int fUseCnfs;
     int fVerbose;
-    extern Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nLutSize, int nCutsMax, int fArea, int fUseBdds, int fUseSops, int fVerbose );
+    extern Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nLutSize, int nCutsMax, int nFlowIters, int nAreaIters, int fArea, int fUseBdds, int fUseSops, int fUseCnfs, int fVerbose );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
-    nLutSize  =  8;
-    nCutsMax  =  5;
-    fArea     =  0;
-    fUseBdds  =  0;
-    fUseSops  =  0;
-    fVerbose  =  0;
+    nLutSize   =  8;
+    nCutsMax   =  5;
+    nFlowIters =  1;
+    nAreaIters =  1;
+    fArea      =  0;
+    fUseBdds   =  0;
+    fUseSops   =  0;
+    fUseCnfs   =  0;
+    fVerbose   =  0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "KCabsvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "KCFAabscvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -2082,6 +2089,28 @@ int Abc_CommandRenode( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( nCutsMax < 0 ) 
                 goto usage;
             break;
+        case 'F':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-F\" should be followed by a positive integer.\n" );
+                goto usage;
+            }
+            nFlowIters = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nFlowIters < 0 ) 
+                goto usage;
+            break;
+        case 'A':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-A\" should be followed by a positive integer.\n" );
+                goto usage;
+            }
+            nAreaIters = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nAreaIters < 0 ) 
+                goto usage;
+            break;
         case 'a':
             fArea ^= 1;
             break;
@@ -2091,6 +2120,9 @@ int Abc_CommandRenode( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 's':
             fUseSops ^= 1;
             break;
+        case 'c':
+            fUseCnfs ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -2101,9 +2133,9 @@ int Abc_CommandRenode( Abc_Frame_t * pAbc, int argc, char ** argv )
         }
     }
 
-    if ( fUseBdds && fUseSops )
+    if ( fUseBdds && fUseSops || fUseBdds && fUseCnfs || fUseSops && fUseCnfs )
     {
-        fprintf( pErr, "Cannot optimize both BDDs and SOPs at the same time.\n" );
+        fprintf( pErr, "Cannot optimize two parameters at the same time.\n" );
         return 1;
     }
 
@@ -2131,7 +2163,7 @@ int Abc_CommandRenode( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     // get the new network
-    pNtkRes = Abc_NtkRenode( pNtk, nLutSize, nCutsMax, fArea, fUseBdds, fUseSops, fVerbose );
+    pNtkRes = Abc_NtkRenode( pNtk, nLutSize, nCutsMax, nFlowIters, nAreaIters, fArea, fUseBdds, fUseSops, fUseCnfs, fVerbose );
     if ( pNtkRes == NULL )
     {
         fprintf( pErr, "Renoding has failed.\n" );
@@ -2142,13 +2174,16 @@ int Abc_CommandRenode( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: renode [-K num] [-C num] [-sbav]\n" );
+    fprintf( pErr, "usage: renode [-K num] [-C num] [-F num] [-A num] [-sbcav]\n" );
     fprintf( pErr, "\t          transforms the AIG into a logic network with larger nodes\n" );
     fprintf( pErr, "\t          while minimizing the number of FF literals of the node SOPs\n" );
     fprintf( pErr, "\t-K num  : the max cut size for renoding (2 < num < %d) [default = %d]\n", IF_MAX_FUNC_LUTSIZE+1, nLutSize );
     fprintf( pErr, "\t-C num  : the max number of cuts used at a node (1 < num < 2^12) [default = %d]\n", nCutsMax );
+    fprintf( pErr, "\t-F num  : the number of area flow recovery iterations (num >= 0) [default = %d]\n", nFlowIters );
+    fprintf( pErr, "\t-A num  : the number of exact area recovery iterations (num >= 0) [default = %d]\n", nAreaIters );
     fprintf( pErr, "\t-s      : toggles minimizing SOP cubes instead of FF lits [default = %s]\n", fUseSops? "yes": "no" );
     fprintf( pErr, "\t-b      : toggles minimizing BDD nodes instead of FF lits [default = %s]\n", fUseBdds? "yes": "no" );
+    fprintf( pErr, "\t-c      : toggles minimizing CNF clauses instead of FF lits [default = %s]\n", fUseCnfs? "yes": "no" );
     fprintf( pErr, "\t-a      : toggles area-oriented mapping [default = %s]\n", fArea? "yes": "no" );
     fprintf( pErr, "\t-v      : print verbose information [default = %s]\n", fVerbose? "yes": "no" ); 
     fprintf( pErr, "\t-h      : print the command usage\n");
@@ -3450,7 +3485,7 @@ int Abc_CommandOrPos( Abc_Frame_t * pAbc, int argc, char ** argv )
     Abc_Ntk_t * pNtk;//, * pNtkRes;
     int fComb;
     int c;
-    extern int Abc_NtkOrPos( Abc_Ntk_t * pNtk );
+    extern int Abc_NtkCombinePos( Abc_Ntk_t * pNtk, int fAnd );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
@@ -3489,7 +3524,7 @@ int Abc_CommandOrPos( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     // get the new network
-    if ( !Abc_NtkOrPos( pNtk ) )
+    if ( !Abc_NtkCombinePos( pNtk, 0 ) )
     {
         fprintf( pErr, "ORing the POs has failed.\n" );
         return 1;
@@ -3517,6 +3552,79 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandAndPos( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk;//, * pNtkRes;
+    int fComb;
+    int c;
+    extern int Abc_NtkCombinePos( Abc_Ntk_t * pNtk, int fAnd );
+
+    pNtk = Abc_FrameReadNtk(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "ch" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'c':
+            fComb ^= 1;
+            break;
+        default:
+            goto usage;
+        }
+    }
+
+    if ( !Abc_NtkIsStrash(pNtk) )
+    {
+        fprintf( pErr, "The network is not strashed.\n" );
+        return 1;
+    }
+
+    if ( Abc_NtkPoNum(pNtk) == 1 )
+    {
+        fprintf( pErr, "The network already has one PO.\n" );
+        return 1;
+    }
+
+    if ( Abc_NtkLatchNum(pNtk) )
+    {
+        fprintf( pErr, "The miter has latches. ORing is not performed.\n" );
+        return 1;
+    }
+
+    // get the new network
+    if ( !Abc_NtkCombinePos( pNtk, 1 ) )
+    {
+        fprintf( pErr, "ANDing the POs has failed.\n" );
+        return 1;
+    }
+    // replace the current network
+//    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: andpos [-h]\n" );
+    fprintf( pErr, "\t        creates single-output miter by ANDing the POs of the current network\n" );
+//    fprintf( pErr, "\t-c    : computes combinational miter (latches as POs) [default = %s]\n", fComb? "yes": "no" );
+    fprintf( pErr, "\t-h    : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandAppend( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
@@ -5286,6 +5394,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
 //    extern Abc_Ntk_t * Abc_NtkNewAig( Abc_Ntk_t * pNtk );
 //    extern Abc_Ntk_t * Abc_NtkIvy( Abc_Ntk_t * pNtk );
     extern void Abc_NtkMaxFlowTest( Abc_Ntk_t * pNtk );
+    extern int Pr_ManProofTest( char * pFileName );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
@@ -5379,7 +5488,8 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
     // replace the current network
     Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
 */
-    Abc_NtkMaxFlowTest( pNtk );
+//    Abc_NtkMaxFlowTest( pNtk );
+    Pr_ManProofTest( "trace.cnf" );
     return 0;
 
 usage:
@@ -7524,6 +7634,8 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
     // user-controlable paramters
     pPars->nLutSize    =  4;
     pPars->nCutsMax    =  8;
+    pPars->nFlowIters  =  1;
+    pPars->nAreaIters  =  2;
     pPars->DelayTarget = -1;
     pPars->fPreprocess =  1;
     pPars->fArea       =  0;
@@ -7542,7 +7654,7 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
     pPars->pFuncCost   =  NULL;   
 
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "KCDpaflrstvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "KCFADpaflrstvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -7570,6 +7682,28 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( pPars->nCutsMax < 0 ) 
                 goto usage;
             break;
+        case 'F':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-F\" should be followed by a positive integer.\n" );
+                goto usage;
+            }
+            pPars->nFlowIters = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nFlowIters < 0 ) 
+                goto usage;
+            break;
+        case 'A':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-A\" should be followed by a positive integer.\n" );
+                goto usage;
+            }
+            pPars->nAreaIters = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nAreaIters < 0 ) 
+                goto usage;
+            break;
         case 'D':
             if ( globalUtilOptind >= argc )
             {
@@ -7705,10 +7839,12 @@ usage:
         sprintf( LutSize, "library" );
     else
         sprintf( LutSize, "%d", pPars->nLutSize );
-    fprintf( pErr, "usage: if [-K num] [-C num] [-D float] [-pafrsvh]\n" );
+    fprintf( pErr, "usage: if [-K num] [-C num] [-F num] [-A num] [-D float] [-pafrsvh]\n" );
     fprintf( pErr, "\t           performs FPGA technology mapping of the network\n" );
     fprintf( pErr, "\t-K num   : the number of LUT inputs (2 < num < %d) [default = %s]\n", IF_MAX_LUTSIZE+1, LutSize );
     fprintf( pErr, "\t-C num   : the max number of cuts to use (1 < num < 2^12) [default = %d]\n", pPars->nCutsMax );
+    fprintf( pErr, "\t-F num   : the number of area flow recovery iterations (num >= 0) [default = %d]\n", pPars->nFlowIters );
+    fprintf( pErr, "\t-A num   : the number of exact area recovery iterations (num >= 0) [default = %d]\n", pPars->nAreaIters );
     fprintf( pErr, "\t-D float : sets the delay constraint for the mapping [default = %s]\n", Buffer );  
     fprintf( pErr, "\t-p       : toggles preprocessing using several starting points [default = %s]\n", pPars->fPreprocess? "yes": "no" );
     fprintf( pErr, "\t-a       : toggles area-oriented mapping [default = %s]\n", pPars->fArea? "yes": "no" );
@@ -9143,11 +9279,9 @@ int Abc_CommandSat( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     else
     {
-        Abc_Ntk_t * pTemp;
-        pTemp = Abc_NtkStrash( pNtk, 0, 0 );
-        RetValue = Abc_NtkMiterSat( pTemp, (sint64)nConfLimit, (sint64)nInsLimit, fJFront, fVerbose, NULL, NULL );
-        pNtk->pModel = pTemp->pModel;  pTemp->pModel = NULL;
-        Abc_NtkDelete( pTemp );
+        assert( Abc_NtkIsLogic(pNtk) );
+        Abc_NtkLogicToBdd( pNtk );
+        RetValue = Abc_NtkMiterSat( pNtk, (sint64)nConfLimit, (sint64)nInsLimit, fJFront, fVerbose, NULL, NULL );
     }
 
     // verify that the pattern is correct
diff --git a/src/base/abci/abcIf.c b/src/base/abci/abcIf.c
index 871bf148..887f6cc9 100644
--- a/src/base/abci/abcIf.c
+++ b/src/base/abci/abcIf.c
@@ -31,6 +31,8 @@ static Abc_Ntk_t * Abc_NtkFromIf( If_Man_t * pIfMan, Abc_Ntk_t * pNtk );
 static Abc_Obj_t * Abc_NodeFromIf_rec( Abc_Ntk_t * pNtkNew, If_Man_t * pIfMan, If_Obj_t * pIfObj, Vec_Int_t * vCover );
 static Hop_Obj_t * Abc_NodeIfToHop( Hop_Man_t * pHopMan, If_Man_t * pIfMan, If_Obj_t * pIfObj );
 static Vec_Ptr_t * Abc_NtkFindGoodOrder( Abc_Ntk_t * pNtk );
+
+extern void Abc_NtkBddReorder( Abc_Ntk_t * pNtk, int fVerbose );
  
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -122,6 +124,11 @@ If_Man_t * Abc_NtkToIf( Abc_Ntk_t * pNtk, If_Par_t * pPars )
     // start the mapping manager and set its parameters
     pIfMan = If_ManStart( pPars );
 
+    // print warning about excessive memory usage
+    if ( 1.0 * Abc_NtkObjNum(pNtk) * pIfMan->nEntrySize / (1<<30) > 0.5 )
+        printf( "Warning: The mapper is about to allocate %.1f Gb for to represent %d cuts per node.\n", 
+            1.0 * Abc_NtkObjNum(pNtk) * pIfMan->nEntrySize / (1<<30), pPars->nCutsMax );
+
     // create PIs and remember them in the old nodes
     Abc_AigConst1(pNtk)->pCopy = (Abc_Obj_t *)If_ManConst1( pIfMan );
     Abc_NtkForEachCi( pNtk, pNode, i )
@@ -177,7 +184,7 @@ Abc_Ntk_t * Abc_NtkFromIf( If_Man_t * pIfMan, Abc_Ntk_t * pNtk )
     Vec_Int_t * vCover;
     int i, nDupGates;
     // create the new network
-    if ( pIfMan->pPars->fUseBdds )
+    if ( pIfMan->pPars->fUseBdds || pIfMan->pPars->fUseCnfs )
         pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_BDD );
     else if ( pIfMan->pPars->fUseSops )
         pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_SOP );
@@ -206,6 +213,11 @@ Abc_Ntk_t * Abc_NtkFromIf( If_Man_t * pIfMan, Abc_Ntk_t * pNtk )
     pNodeNew = (Abc_Obj_t *)If_ObjCopy( If_ManConst1(pIfMan) );
     if ( Abc_ObjFanoutNum(pNodeNew) == 0 )
         Abc_NtkDeleteObj( pNodeNew );
+    // minimize the node
+    if ( pIfMan->pPars->fUseCnfs || pIfMan->pPars->fUseBdds )
+        Abc_NtkSweep( pNtkNew, 0 );
+    if ( pIfMan->pPars->fUseBdds )
+        Abc_NtkBddReorder( pNtkNew, 0 );
     // decouple the PO driver nodes to reduce the number of levels
     nDupGates = Abc_NtkLogicMakeSimpleCos( pNtkNew, 1 );
 //    if ( nDupGates && If_ManReadVerbose(pIfMan) )
@@ -239,28 +251,28 @@ Abc_Obj_t * Abc_NodeFromIf_rec( Abc_Ntk_t * pNtkNew, If_Man_t * pIfMan, If_Obj_t
     // create a new node 
     pNodeNew = Abc_NtkCreateNode( pNtkNew );
     pCutBest = If_ObjCutBest( pIfObj );
-    If_CutForEachLeaf( pIfMan, pCutBest, pIfLeaf, i )
-        Abc_ObjAddFanin( pNodeNew, Abc_NodeFromIf_rec(pNtkNew, pIfMan, pIfLeaf, vCover) );
+    if ( pIfMan->pPars->fUseCnfs )
+    {
+        If_CutForEachLeafReverse( pIfMan, pCutBest, pIfLeaf, i )
+            Abc_ObjAddFanin( pNodeNew, Abc_NodeFromIf_rec(pNtkNew, pIfMan, pIfLeaf, vCover) );
+    }
+    else
+    {
+        If_CutForEachLeaf( pIfMan, pCutBest, pIfLeaf, i )
+            Abc_ObjAddFanin( pNodeNew, Abc_NodeFromIf_rec(pNtkNew, pIfMan, pIfLeaf, vCover) );
+    }
     // derive the function of this node
     if ( pIfMan->pPars->fTruth )
     {
         if ( pIfMan->pPars->fUseBdds )
         { 
-            extern void Abc_NodeBddReorder( void * p, Abc_Obj_t * pNode );
             // transform truth table into the BDD 
             pNodeNew->pData = Kit_TruthToBdd( pNtkNew->pManFunc, If_CutTruth(pCutBest), If_CutLeaveNum(pCutBest), 0 );  Cudd_Ref(pNodeNew->pData); 
-            if ( pNodeNew->pData == Cudd_ReadLogicZero(pNtkNew->pManFunc) || pNodeNew->pData == Cudd_ReadOne(pNtkNew->pManFunc) )
-            {
-                // replace the node by a constant node
-                pNodeNew = pNodeNew->pData == Cudd_ReadOne(pNtkNew->pManFunc) ? Abc_NtkCreateNodeConst1(pNtkNew) : Abc_NtkCreateNodeConst0(pNtkNew);
-            }
-            else
-            {
-                // make sure the node is minimum base
-                Abc_NodeMinimumBase( pNodeNew );
-                // reorder the fanins to minimize the BDD size
-                Abc_NodeBddReorder( pIfMan->pPars->pReoMan, pNodeNew );
-            }
+        }
+        else if ( pIfMan->pPars->fUseCnfs )
+        { 
+            // transform truth table into the BDD 
+            pNodeNew->pData = Kit_TruthToBdd( pNtkNew->pManFunc, If_CutTruth(pCutBest), If_CutLeaveNum(pCutBest), 1 );  Cudd_Ref(pNodeNew->pData); 
         }
         else if ( pIfMan->pPars->fUseSops ) 
         {
diff --git a/src/base/abci/abcMiter.c b/src/base/abci/abcMiter.c
index ddbbf671..15a81723 100644
--- a/src/base/abci/abcMiter.c
+++ b/src/base/abci/abcMiter.c
@@ -1039,7 +1039,7 @@ int Abc_NtkDemiter( Abc_Ntk_t * pNtk )
 
 /**Function*************************************************************
 
-  Synopsis    [ORs the outputs.]
+  Synopsis    [Computes OR or AND of the POs.]
 
   Description []
 
@@ -1048,16 +1048,23 @@ int Abc_NtkDemiter( Abc_Ntk_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkOrPos( Abc_Ntk_t * pNtk )
+int Abc_NtkCombinePos( Abc_Ntk_t * pNtk, int fAnd )
 {
     Abc_Obj_t * pNode, * pMiter;
     int i;
     assert( Abc_NtkIsStrash(pNtk) );
     assert( Abc_NtkLatchNum(pNtk) == 0 );
-    // OR the POs
-    pMiter = Abc_ObjNot( Abc_AigConst1(pNtk) );
+    // start the result
+    if ( fAnd )
+        pMiter = Abc_AigConst1(pNtk);
+    else
+        pMiter = Abc_ObjNot( Abc_AigConst1(pNtk) );
+    // perform operations on the POs
     Abc_NtkForEachPo( pNtk, pNode, i )
-        pMiter = Abc_AigOr( pNtk->pManFunc, pMiter, Abc_ObjChild0(pNode) );
+        if ( fAnd )
+            pMiter = Abc_AigAnd( pNtk->pManFunc, pMiter, Abc_ObjChild0(pNode) );
+        else
+            pMiter = Abc_AigOr( pNtk->pManFunc, pMiter, Abc_ObjChild0(pNode) );
     // remove the POs and their names
     for ( i = Abc_NtkPoNum(pNtk) - 1; i >= 0; i-- )
         Abc_NtkDeleteObj( Abc_NtkPo(pNtk, i) );
diff --git a/src/base/abci/abcRefactor.c b/src/base/abci/abcRefactor.c
index 0328d8d3..834e33aa 100644
--- a/src/base/abci/abcRefactor.c
+++ b/src/base/abci/abcRefactor.c
@@ -233,7 +233,7 @@ p->timeDcs += clock() - clk;
 
     // get the SOP of the cut
 clk = clock();
-    pSop = Abc_ConvertBddToSop( NULL, p->dd, bNodeFunc, bNodeFunc, vFanins->nSize, p->vCube, -1 );
+    pSop = Abc_ConvertBddToSop( NULL, p->dd, bNodeFunc, bNodeFunc, vFanins->nSize, 0, p->vCube, -1 );
 p->timeSop += clock() - clk;
 
     // get the factored form
diff --git a/src/base/abci/abcRenode.c b/src/base/abci/abcRenode.c
index 462d9da3..af3f55cf 100644
--- a/src/base/abci/abcRenode.c
+++ b/src/base/abci/abcRenode.c
@@ -29,6 +29,7 @@
 
 static int Abc_NtkRenodeEvalBdd( If_Cut_t * pCut );
 static int Abc_NtkRenodeEvalSop( If_Cut_t * pCut );
+static int Abc_NtkRenodeEvalCnf( If_Cut_t * pCut );
 static int Abc_NtkRenodeEvalAig( If_Cut_t * pCut );
 
 static reo_man * s_pReo      = NULL;
@@ -50,7 +51,7 @@ static Vec_Int_t * s_vMemory = NULL;
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nFaninMax, int nCubeMax, int fArea, int fUseBdds, int fUseSops, int fVerbose )
+Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nFaninMax, int nCubeMax, int nFlowIters, int nAreaIters, int fArea, int fUseBdds, int fUseSops, int fUseCnfs, int fVerbose )
 {
     extern Abc_Ntk_t * Abc_NtkIf( Abc_Ntk_t * pNtk, If_Par_t * pPars );
     If_Par_t Pars, * pPars = &Pars;
@@ -64,6 +65,8 @@ Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nFaninMax, int nCubeMax, int fA
     // user-controlable paramters
     pPars->nLutSize    =  nFaninMax;
     pPars->nCutsMax    =  nCubeMax;
+    pPars->nFlowIters  =  nFlowIters;
+    pPars->nAreaIters  =  nAreaIters;
     pPars->DelayTarget = -1;
     pPars->fPreprocess =  1;
     pPars->fArea       =  fArea;
@@ -81,10 +84,16 @@ Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nFaninMax, int nCubeMax, int fA
     pPars->pTimesArr   =  NULL;   
     pPars->fUseBdds    =  fUseBdds;
     pPars->fUseSops    =  fUseSops;
+    pPars->fUseCnfs    =  fUseCnfs;
     if ( fUseBdds )
         pPars->pFuncCost = Abc_NtkRenodeEvalBdd;
     else if ( fUseSops )
         pPars->pFuncCost = Abc_NtkRenodeEvalSop;
+    else if ( fUseCnfs )
+    {
+        pPars->fArea = 1;
+        pPars->pFuncCost = Abc_NtkRenodeEvalCnf;
+    }
     else
         pPars->pFuncCost = Abc_NtkRenodeEvalAig;
 
@@ -176,6 +185,39 @@ int Abc_NtkRenodeEvalSop( If_Cut_t * pCut )
 
 /**Function*************************************************************
 
+  Synopsis    [Computes the cost based on two ISOPs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkRenodeEvalCnf( If_Cut_t * pCut )
+{
+    int i, RetValue, nClauses;
+    for ( i = 0; i < If_CutLeaveNum(pCut); i++ )
+        pCut->pPerm[i] = 1;
+    // compute ISOP for the positive phase
+    RetValue = Kit_TruthIsop( If_CutTruth(pCut), If_CutLeaveNum(pCut), s_vMemory, 0 );
+    if ( RetValue == -1 )
+        return ABC_INFINITY;
+    assert( RetValue == 0 || RetValue == 1 );
+    nClauses = Vec_IntSize( s_vMemory );
+    // compute ISOP for the negative phase
+    Kit_TruthNot( If_CutTruth(pCut), If_CutTruth(pCut), If_CutLeaveNum(pCut) );
+    RetValue = Kit_TruthIsop( If_CutTruth(pCut), If_CutLeaveNum(pCut), s_vMemory, 0 );
+    Kit_TruthNot( If_CutTruth(pCut), If_CutTruth(pCut), If_CutLeaveNum(pCut) );
+    if ( RetValue == -1 )
+        return ABC_INFINITY;
+    assert( RetValue == 0 || RetValue == 1 );
+    nClauses += Vec_IntSize( s_vMemory );
+    return nClauses;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Computes the cost based on the factored form.]
 
   Description []
diff --git a/src/base/abci/abcSat.c b/src/base/abci/abcSat.c
index 55498288..cf67db6d 100644
--- a/src/base/abci/abcSat.c
+++ b/src/base/abci/abcSat.c
@@ -24,6 +24,7 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+static solver * Abc_NtkMiterSatCreateLogic( Abc_Ntk_t * pNtk, int fAllPrimes );
 extern Vec_Int_t * Abc_NtkGetCiSatVarNums( Abc_Ntk_t * pNtk );
 static nMuxes;
 
@@ -53,7 +54,6 @@ int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int
     if ( pNumInspects )
         *pNumInspects = 0;
 
-    assert( Abc_NtkIsStrash(pNtk) );
     assert( Abc_NtkLatchNum(pNtk) == 0 );
 
 //    if ( Abc_NtkPoNum(pNtk) > 1 )
@@ -61,7 +61,7 @@ int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int
 
     // load clauses into the solver
     clk = clock();
-    pSat = Abc_NtkMiterSatCreate( pNtk, fJFront );
+    pSat = Abc_NtkMiterSatCreate( pNtk, fJFront, 0 );
     if ( pSat == NULL )
         return 1;
 //    printf( "Created SAT problem with %d variable and %d clauses. ", solver_nvars(pSat), solver_nclauses(pSat) );
@@ -121,6 +121,9 @@ int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int
     if ( pNumInspects )
         *pNumInspects = (int)pSat->solver_stats.inspects;
 
+Sat_SolverTraceWrite( pSat, NULL, NULL, 0 );
+Sat_SolverTraceStop( pSat );
+
     solver_delete( pSat );
     return RetValue;
 }
@@ -660,14 +663,17 @@ Quits :
   SeeAlso     []
 
 ***********************************************************************/
-solver * Abc_NtkMiterSatCreate( Abc_Ntk_t * pNtk, int fJFront )
+solver * Abc_NtkMiterSatCreate( Abc_Ntk_t * pNtk, int fJFront, int fAllPrimes )
 {
     solver * pSat;
     Abc_Obj_t * pNode;
     int RetValue, i, clk = clock();
 
-    nMuxes = 0;
+    assert( Abc_NtkIsStrash(pNtk) || Abc_NtkIsBddLogic(pNtk) );
+    if ( Abc_NtkIsBddLogic(pNtk) )
+        return Abc_NtkMiterSatCreateLogic(pNtk, fAllPrimes);
 
+    nMuxes = 0;
     pSat = solver_new();
     RetValue = Abc_NtkMiterSatCreateInt( pSat, pNtk, fJFront );
     Abc_NtkForEachObj( pNtk, pNode, i )
@@ -684,6 +690,242 @@ solver * Abc_NtkMiterSatCreate( Abc_Ntk_t * pNtk, int fJFront )
 }
 
 
+
+
+/**Function*************************************************************
+
+  Synopsis    [Adds clauses for the internal node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NodeAddClauses( solver * pSat, char * pSop0, char * pSop1, Abc_Obj_t * pNode, Vec_Int_t * vVars )
+{
+    Abc_Obj_t * pFanin;
+    int i, c, nFanins;
+    int RetValue;
+    char * pCube;
+
+    nFanins = Abc_ObjFaninNum( pNode );
+    assert( nFanins == Abc_SopGetVarNum( pSop0 ) );
+
+//    if ( nFanins == 0 )
+    if ( Cudd_Regular(pNode->pData) == Cudd_ReadOne(pNode->pNtk->pManFunc) )
+    {
+        vVars->nSize = 0;
+//        if ( Abc_SopIsConst1(pSop1) )
+        if ( !Cudd_IsComplement(pNode->pData) )
+            Vec_IntPush( vVars, toLit(pNode->Id) );
+        else
+            Vec_IntPush( vVars, neg(toLit(pNode->Id)) );
+        RetValue = solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
+        if ( !RetValue ) 
+        {
+            printf( "The CNF is trivially UNSAT.\n" );
+            return 0;
+        }
+        return 1;
+    }
+ 
+    // add clauses for the negative phase
+    for ( c = 0; ; c++ )
+    {
+        // get the cube
+        pCube = pSop0 + c * (nFanins + 3);
+        if ( *pCube == 0 )
+            break;
+        // add the clause
+        vVars->nSize = 0;
+        Abc_ObjForEachFanin( pNode, pFanin, i )
+        {
+            if ( pCube[i] == '0' )
+                Vec_IntPush( vVars, toLit(pFanin->Id) );
+            else if ( pCube[i] == '1' )
+                Vec_IntPush( vVars, neg(toLit(pFanin->Id)) );
+        }
+        Vec_IntPush( vVars, neg(toLit(pNode->Id)) );
+        RetValue = solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
+        if ( !RetValue ) 
+        {
+            printf( "The CNF is trivially UNSAT.\n" );
+            return 0;
+        }
+    }
+
+    // add clauses for the positive phase
+    for ( c = 0; ; c++ )
+    {
+        // get the cube
+        pCube = pSop1 + c * (nFanins + 3);
+        if ( *pCube == 0 )
+            break;
+        // add the clause
+        vVars->nSize = 0;
+        Abc_ObjForEachFanin( pNode, pFanin, i )
+        {
+            if ( pCube[i] == '0' )
+                Vec_IntPush( vVars, toLit(pFanin->Id) );
+            else if ( pCube[i] == '1' )
+                Vec_IntPush( vVars, neg(toLit(pFanin->Id)) );
+        }
+        Vec_IntPush( vVars, toLit(pNode->Id) );
+        RetValue = solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
+        if ( !RetValue ) 
+        {
+            printf( "The CNF is trivially UNSAT.\n" );
+            return 0;
+        }
+    }
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Adds clauses for the PO node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NodeAddClausesTop( solver * pSat, Abc_Obj_t * pNode, Vec_Int_t * vVars )
+{
+    Abc_Obj_t * pFanin;
+    int RetValue;
+
+    pFanin = Abc_ObjFanin0(pNode);
+    if ( Abc_ObjFaninC0(pNode) )
+    {
+        vVars->nSize = 0;
+        Vec_IntPush( vVars, toLit(pFanin->Id) );
+        Vec_IntPush( vVars, toLit(pNode->Id) );
+        RetValue = solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
+        if ( !RetValue ) 
+        {
+            printf( "The CNF is trivially UNSAT.\n" );
+            return 0;
+        }
+
+        vVars->nSize = 0;
+        Vec_IntPush( vVars, neg(toLit(pFanin->Id)) );
+        Vec_IntPush( vVars, neg(toLit(pNode->Id)) );
+        RetValue = solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
+        if ( !RetValue ) 
+        {
+            printf( "The CNF is trivially UNSAT.\n" );
+            return 0;
+        }
+    }
+    else
+    {
+        vVars->nSize = 0;
+        Vec_IntPush( vVars, neg(toLit(pFanin->Id)) );
+        Vec_IntPush( vVars, toLit(pNode->Id) );
+        RetValue = solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
+        if ( !RetValue ) 
+        {
+            printf( "The CNF is trivially UNSAT.\n" );
+            return 0;
+        }
+
+        vVars->nSize = 0;
+        Vec_IntPush( vVars, toLit(pFanin->Id) );
+        Vec_IntPush( vVars, neg(toLit(pNode->Id)) );
+        RetValue = solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
+        if ( !RetValue ) 
+        {
+            printf( "The CNF is trivially UNSAT.\n" );
+            return 0;
+        }
+    }
+
+    vVars->nSize = 0;
+    Vec_IntPush( vVars, toLit(pNode->Id) );
+    RetValue = solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
+    if ( !RetValue ) 
+    {
+        printf( "The CNF is trivially UNSAT.\n" );
+        return 0;
+    }
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Sets up the SAT solver.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+solver * Abc_NtkMiterSatCreateLogic( Abc_Ntk_t * pNtk, int fAllPrimes )
+{
+    solver * pSat;
+    Extra_MmFlex_t * pMmFlex;
+    Abc_Obj_t * pNode;
+    Vec_Str_t * vCube;
+    Vec_Int_t * vVars;
+    char * pSop0, * pSop1;
+    int i;
+
+    assert( Abc_NtkIsBddLogic(pNtk) );
+
+    // transfer the IDs to the copy field
+    Abc_NtkForEachPi( pNtk, pNode, i )
+        pNode->pCopy = (void *)pNode->Id;
+
+    // start the data structures
+    pSat    = solver_new();
+    pMmFlex = Extra_MmFlexStart();
+    vCube   = Vec_StrAlloc( 100 );
+    vVars   = Vec_IntAlloc( 100 );
+
+Sat_SolverTraceStart( pSat, "trace.cnf" );
+
+    // add clauses for each internal nodes
+    Abc_NtkForEachNode( pNtk, pNode, i )
+    {
+        // derive SOPs for both phases of the node
+        Abc_NodeBddToCnf( pNode, pMmFlex, vCube, fAllPrimes, &pSop0, &pSop1 );
+        // add the clauses to the solver
+        if ( !Abc_NodeAddClauses( pSat, pSop0, pSop1, pNode, vVars ) )
+        {
+            solver_delete( pSat );
+            pSat = NULL;
+            goto finish;
+        }
+    }
+    // add clauses for each PO
+    Abc_NtkForEachPo( pNtk, pNode, i )
+    {
+        if ( !Abc_NodeAddClausesTop( pSat, pNode, vVars ) )
+        {
+            solver_delete( pSat );
+            pSat = NULL;
+            goto finish;
+        }
+    }
+
+finish:
+    // delete
+    Vec_StrFree( vCube );
+    Vec_IntFree( vVars );
+    Extra_MmFlexStop( pMmFlex );
+    return pSat;
+}
+
+
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abcStrash.c b/src/base/abci/abcStrash.c
index 9af6dc00..b6aecef9 100644
--- a/src/base/abci/abcStrash.c
+++ b/src/base/abci/abcStrash.c
@@ -49,7 +49,7 @@ Abc_Ntk_t * Abc_NtkRestrash( Abc_Ntk_t * pNtk, bool fCleanup )
     extern int timeRetime;
     Abc_Ntk_t * pNtkAig;
     Abc_Obj_t * pObj;
-    int i, nNodes, RetValue;
+    int i, nNodes;//, RetValue;
     assert( Abc_NtkIsStrash(pNtk) );
 //timeRetime = clock();
     // print warning about choice nodes
@@ -79,8 +79,8 @@ Abc_Ntk_t * Abc_NtkRestrash( Abc_Ntk_t * pNtk, bool fCleanup )
         return NULL;
     }
 //timeRetime = clock() - timeRetime;
-    if ( RetValue = Abc_NtkRemoveSelfFeedLatches(pNtkAig) )
-        printf( "Modified %d self-feeding latches. The result will not verify.\n", RetValue );
+//    if ( RetValue = Abc_NtkRemoveSelfFeedLatches(pNtkAig) )
+//        printf( "Modified %d self-feeding latches. The result will not verify.\n", RetValue );
     return pNtkAig;
 
 }
diff --git a/src/base/abci/abcVerify.c b/src/base/abci/abcVerify.c
index ec0ba8ca..f3a069f4 100644
--- a/src/base/abci/abcVerify.c
+++ b/src/base/abci/abcVerify.c
@@ -417,6 +417,12 @@ int * Abc_NtkVerifySimulatePattern( Abc_Ntk_t * pNtk, int * pModel )
         pNtk = Abc_NtkStrash(pNtk, 0, 0);
         fStrashed = 1;
     }
+/*
+    printf( "Counter example: " );
+    Abc_NtkForEachCi( pNtk, pNode, i )
+        printf( " %d", pModel[i] );
+    printf( "\n" );
+*/
     // increment the trav ID
     Abc_NtkIncrementTravId( pNtk );
     // set the CI values
diff --git a/src/base/io/io.c b/src/base/io/io.c
index f50faa11..8d5b8ad6 100644
--- a/src/base/io/io.c
+++ b/src/base/io/io.c
@@ -1212,12 +1212,17 @@ int IoCommandWriteCnf( Abc_Frame_t * pAbc, int argc, char **argv )
 {
     char * pFileName;
     int c;
+    int fAllPrimes;
 
+    fAllPrimes = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "ph" ) ) != EOF )
     {
         switch ( c )
         {
+            case 'p':
+                fAllPrimes ^= 1;
+                break;
             case 'h':
                 goto usage;
             default:
@@ -1228,13 +1233,23 @@ int IoCommandWriteCnf( Abc_Frame_t * pAbc, int argc, char **argv )
         goto usage;
     // get the output file name
     pFileName = argv[globalUtilOptind];
+    // check if the feature will be used
+    if ( Abc_NtkIsStrash(pAbc->pNtkCur) && fAllPrimes )
+    {
+        fAllPrimes = 0;
+        printf( "Warning: Selected option to write all primes has no effect when deriving CNF from AIG.\n" );
+    }
     // call the corresponding file writer
-    Io_Write( pAbc->pNtkCur, pFileName, IO_FILE_CNF );
+    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 [-h] <file>\n" );
+    fprintf( pAbc->Err, "usage: write_cnf [-ph] <file>\n" );
     fprintf( pAbc->Err, "\t         write the miter cone into a CNF file\n" );
+    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" );
     return 1;
diff --git a/src/base/io/io.h b/src/base/io/io.h
index 55339790..78bc4563 100644
--- a/src/base/io/io.h
+++ b/src/base/io/io.h
@@ -100,7 +100,7 @@ extern void               Io_WriteBlifMvNetlist( Abc_Ntk_t * pNtk, char * FileNa
 /*=== abcWriteBench.c =========================================================*/
 extern int                Io_WriteBench( Abc_Ntk_t * pNtk, char * FileName );
 /*=== abcWriteCnf.c ===========================================================*/
-extern int                Io_WriteCnf( Abc_Ntk_t * pNtk, char * FileName );
+extern int                Io_WriteCnf( Abc_Ntk_t * pNtk, char * FileName, int fAllPrimes );
 /*=== abcWriteDot.c ===========================================================*/
 extern void               Io_WriteDot( Abc_Ntk_t * pNtk, char * FileName );
 extern void               Io_WriteDotNtk( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesShow, char * pFileName, int fGateNames, int fUseReverse );
diff --git a/src/base/io/ioUtil.c b/src/base/io/ioUtil.c
index ba390a2f..ed197ab4 100644
--- a/src/base/io/ioUtil.c
+++ b/src/base/io/ioUtil.c
@@ -220,7 +220,7 @@ void Io_Write( Abc_Ntk_t * pNtk, char * pFileName, Io_FileType_t FileType )
     // write non-netlist types
     if ( FileType == IO_FILE_CNF )
     {
-        Io_WriteCnf( pNtk, pFileName );
+        Io_WriteCnf( pNtk, pFileName, 0 );
         return;
     }
     if ( FileType == IO_FILE_DOT )
diff --git a/src/base/io/ioWriteCnf.c b/src/base/io/ioWriteCnf.c
index 24612566..f12a1297 100644
--- a/src/base/io/ioWriteCnf.c
+++ b/src/base/io/ioWriteCnf.c
@@ -41,14 +41,13 @@ static Abc_Ntk_t * s_pNtk = NULL;
   SeeAlso     []
 
 ***********************************************************************/
-int Io_WriteCnf( Abc_Ntk_t * pNtk, char * pFileName )
+int Io_WriteCnf( Abc_Ntk_t * pNtk, char * pFileName, int fAllPrimes )
 {
     solver * pSat;
-    if ( !Abc_NtkIsStrash(pNtk) )
-    {
-        fprintf( stdout, "Io_WriteCnf(): Currently can only process AIGs.\n" );
-        return 0;
-    }
+    if ( Abc_NtkIsStrash(pNtk) )
+        printf( "Io_WriteCnf() warning: Generating CNF by applying heuristic AIG to CNF conversion.\n" );
+    else
+        printf( "Io_WriteCnf() warning: Generating CNF by convering logic nodes into CNF clauses.\n" );
     if ( Abc_NtkPoNum(pNtk) != 1 )
     {
         fprintf( stdout, "Io_WriteCnf(): Currently can only process the miter (the network with one PO).\n" );
@@ -64,8 +63,11 @@ int Io_WriteCnf( Abc_Ntk_t * pNtk, char * pFileName )
         fprintf( stdout, "The network has no logic nodes. No CNF file is generaled.\n" );
         return 0;
     }
+    // convert to logic BDD network
+    if ( Abc_NtkIsLogic(pNtk) )
+        Abc_NtkLogicToBdd( pNtk );
     // create solver with clauses
-    pSat = Abc_NtkMiterSatCreate( pNtk, 0 );
+    pSat = Abc_NtkMiterSatCreate( pNtk, 0, fAllPrimes );
     if ( pSat == NULL )
     {
         fprintf( stdout, "The problem is trivially UNSAT. No CNF file is generated.\n" );
diff --git a/src/base/seq/seqAigCore.c b/src/base/seq/seqAigCore.c
index 21215af6..42fa14a2 100644
--- a/src/base/seq/seqAigCore.c
+++ b/src/base/seq/seqAigCore.c
@@ -352,7 +352,7 @@ int Seq_NtkImplementRetimingBackward( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMoves, int
     printf( "The number of ANDs in the AIG = %5d.\n", Abc_NtkNodeNum(pNtkMiter) );
 
     // transform the miter into a logic network for efficient CNF construction
-//    pNtkCnf = Abc_NtkRenode( pNtkMiter, 0, 100, 1, 0, 0 );
+//    pNtkCnf = Abc_Ntk_Renode( pNtkMiter, 0, 100, 1, 0, 0 );
 //    Abc_NtkDelete( pNtkMiter );
     pNtkCnf = pNtkMiter;