Version abc70121

abc.dsp

@@ -1166,6 +1166,10 @@ SOURCE=.\src\sat\asat\jfront.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\sat\asat\satTrace.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\sat\asat\solver.c
 # End Source File
 # Begin Source File
@@ -1345,6 +1349,18 @@ SOURCE=.\src\sat\bsat\satUtil.c
 SOURCE=.\src\sat\bsat\satVec.h
 # End Source File
 # End Group
+# Begin Group "proof"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\sat\proof\pr.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\proof\pr.h
+# End Source File
+# End Group
 # End Group
 # Begin Group "opt"
 

abc.rc

 # global parameters
 set check         # checks intermediate networks
 #set checkfio      # prints warnings when fanins/fanouts are duplicated
-#set checkread     # checks new networks after reading from file
+set checkread     # checks new networks after reading from file
 #set backup        # saves backup networks retrived by "undo" and "recall"
 set savesteps 1   # sets the maximum number of backup networks to save 
 set progressbar   # display the progress bar

src/aig/ivy/ivyCut.c

@@ -930,6 +930,8 @@ Ivy_Store_t * Ivy_NodeFindCutsAll( Ivy_Man_t * p, Ivy_Obj_t * pObj, int nLeaves
 */
             iLeaf0 = Ivy_ObjId( Ivy_ObjRealFanin(Ivy_ObjFanin0(pLeaf)) );
             iLeaf1 = Ivy_ObjId( Ivy_ObjRealFanin(Ivy_ObjFanin1(pLeaf)) );
+//            if ( iLeaf0 == iLeaf1 ) // strange situation observed on Jan 18, 2007
+//                continue;
             if ( !Ivy_NodeCutPrescreen( pCut, iLeaf0, iLeaf1 ) )
                 continue;
             if ( iLeaf0 > iLeaf1 )

src/aig/ivy/ivyFraig.c

@@ -252,7 +252,7 @@ int Ivy_FraigProve( Ivy_Man_t ** ppManAig, void * pPars )
     Prove_Params_t * pParams = pPars;
     Ivy_FraigParams_t Params, * pIvyParams = &Params; 
     Ivy_Man_t * pManAig, * pManTemp;
-    int RetValue, nIter, Counter, clk, timeStart = clock();
+    int RetValue, nIter, clk, timeStart = clock();//, Counter;
     sint64 nSatConfs, nSatInspects;
 
     // start the network and parameters
@@ -314,12 +314,14 @@ int Ivy_FraigProve( Ivy_Man_t ** ppManAig, void * pPars )
 
         // try rewriting
         if ( pParams->fUseRewriting )
-        {
+        { // bug in Ivy_NodeFindCutsAll() when leaves are identical!
+/*
             clk = clock();
             Counter = (int)(pParams->nRewritingLimitStart * pow(pParams->nRewritingLimitMulti,nIter));
             pManAig = Ivy_ManRwsat( pManAig, 0 );  
             RetValue = Ivy_FraigMiterStatus( pManAig );
             Ivy_FraigMiterPrint( pManAig, "Rewriting  ", clk, pParams->fVerbose );
+*/
         }
         if ( RetValue >= 0 )
             break;
@@ -368,6 +370,15 @@ int Ivy_FraigProve( Ivy_Man_t ** ppManAig, void * pPars )
         s_nInsLimitGlobal = 0;        
         RetValue = Ivy_FraigMiterStatus( pManAig );
         Ivy_FraigMiterPrint( pManAig, "SAT solving", clk, pParams->fVerbose );
+        // make sure that the sover never returns "undecided" when infinite resource limits are set
+        if( RetValue == -1 && pParams->nTotalInspectLimit == 0 &&
+            pParams->nTotalBacktrackLimit == 0 )
+        {
+            extern void Prove_ParamsPrint( Prove_Params_t * pParams );
+            Prove_ParamsPrint( pParams );
+            printf("ERROR: ABC has returned \"undecided\" in spite of no limits...\n");
+            exit(1);
+        }
     }
 
     // assign the model if it was proved by rewriting (const 1 miter)

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 );

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
+        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
+        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 );
 }
 
 

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,11 +2040,13 @@ 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);
@@ -2051,12 +2055,15 @@ int Abc_CommandRenode( Abc_Frame_t * pAbc, int argc, char ** argv )
     // set defaults
     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

src/base/abci/abcIf.c

@@ -32,6 +32,8 @@ static Abc_Obj_t * Abc_NodeFromIf_rec( Abc_Ntk_t * pNtkNew, If_Man_t * pIfMan, I
 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 ( 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
+        else if ( pIfMan->pPars->fUseCnfs )
         { 
-                // make sure the node is minimum base
-                Abc_NodeMinimumBase( pNodeNew );
-                // reorder the fanins to minimize the BDD size
-                Abc_NodeBddReorder( pIfMan->pPars->pReoMan, pNodeNew );
-            }
+            // 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 ) 
         {

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,15 +1048,22 @@ 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
+    // 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 )
+        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-- )

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

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 []

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                                ///
 ////////////////////////////////////////////////////////////////////////

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;
 
 }

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

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
+    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;

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 );

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 )

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" );

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;
 

src/map/if/if.h

@@ -45,6 +45,8 @@ extern "C" {
 #define IF_MAX_LUTSIZE       32
 // the largest possible number of LUT inputs when funtionality of the LUTs are computed
 #define IF_MAX_FUNC_LUTSIZE  15
+// a very large number
+#define IF_INFINITY          100000000   
 
 // object types
 typedef enum { 
@@ -75,6 +77,8 @@ struct If_Par_t_
     // user-controlable paramters
     int                nLutSize;      // the LUT size
     int                nCutsMax;      // the max number of cuts
+    int                nFlowIters;    // the number of iterations of area recovery
+    int                nAreaIters;    // the number of iterations of area recovery
     float              DelayTarget;   // delay target
     int                fPreprocess;   // preprossing
     int                fArea;         // area-oriented mapping
@@ -88,6 +92,7 @@ struct If_Par_t_
     int                fUsePerm;      // use permutation (delay info)
     int                fUseBdds;      // sets local BDDs at the nodes
     int                fUseSops;      // sets local SOPs at the nodes
+    int                fUseCnfs;      // sets local CNFs at the nodes
     int                nLatches;      // the number of latches in seq mapping
     int                fLiftLeaves;   // shift the leaves for seq mapping
     If_Lib_t *         pLutLib;       // the LUT library
@@ -276,6 +281,8 @@ static inline float      If_CutLutArea( If_Man_t * p, If_Cut_t * pCut )      { r
 // iterator over the leaves of the cut
 #define If_CutForEachLeaf( p, pCut, pLeaf, i )                                 \
     for ( i = 0; (i < (int)(pCut)->nLeaves) && ((pLeaf) = If_ManObj(p, (pCut)->pLeaves[i])); i++ )
+#define If_CutForEachLeafReverse( p, pCut, pLeaf, i )                                 \
+    for ( i = (int)(pCut)->nLeaves - 1; (i >= 0) && ((pLeaf) = If_ManObj(p, (pCut)->pLeaves[i])); i-- )
 //#define If_CutForEachLeaf( p, pCut, pLeaf, i )                                 \
 //    for ( i = 0; (i < (int)(pCut)->nLeaves) && ((pLeaf) = If_ManObj(p, p->pPars->fLiftLeaves? (pCut)->pLeaves[i] >> 8 : (pCut)->pLeaves[i])); i++ )
 // iterator over the leaves of the sequential cut

src/map/if/ifCore.c

@@ -42,8 +42,6 @@
 int If_ManPerformMapping( If_Man_t * p )
 {
     If_Obj_t * pObj;
-    int nItersFlow = 1;
-    int nItersArea = 2;
     int clkTotal = clock();
     int RetValue, i;
 
@@ -74,14 +72,14 @@ int If_ManPerformMapping( If_Man_t * p )
     if ( p->pPars->fExpRed && !p->pPars->fTruth )
         If_ManImproveMapping( p );
     // area flow oriented mapping
-    for ( i = 0; i < nItersFlow; i++ )
+    for ( i = 0; i < p->pPars->nFlowIters; i++ )
     {
         If_ManPerformMappingRound( p, p->pPars->nCutsMax, 1, 1, "Flow" );
         if ( p->pPars->fExpRed && !p->pPars->fTruth )
             If_ManImproveMapping( p );
     }
     // area oriented mapping
-    for ( i = 0; i < nItersArea; i++ )
+    for ( i = 0; i < p->pPars->nAreaIters; i++ )
     {
         If_ManPerformMappingRound( p, p->pPars->nCutsMax, 2, 1, "Area" );
         if ( p->pPars->fExpRed && !p->pPars->fTruth )

src/map/if/ifMap.c

@@ -86,7 +86,7 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode )
             pObj->EstRefs = (float)((2.0 * pObj->EstRefs + pObj->nRefs) / 3.0);
     }
     if ( Mode && pObj->nRefs > 0 )
-        If_CutDeref( p, If_ObjCutBest(pObj), 100 );
+        If_CutDeref( p, If_ObjCutBest(pObj), IF_INFINITY );
 
     // save the best cut as one of the candidate cuts
     p->nCuts = 0;
@@ -97,7 +97,7 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode )
         pCut = If_ObjCutBest(pObj);
         pCut->Delay = If_CutDelay( p, pCut );
         assert( pCut->Delay <= pObj->Required + p->fEpsilon );
-        pCut->Area  = (Mode == 2)? If_CutAreaDerefed( p, pCut, 100 ) : If_CutFlow( p, pCut );
+        pCut->Area  = (Mode == 2)? If_CutAreaDerefed( p, pCut, IF_INFINITY ) : If_CutFlow( p, pCut );
         // save the best cut from the previous iteration
         If_CutCopy( p->ppCuts[p->nCuts++], pCut );
         p->nCutsMerged++;
@@ -135,7 +135,7 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode )
         if ( Mode && pCut->Delay > pObj->Required + p->fEpsilon )
             continue;
         // compute area of the cut (this area may depend on the application specific cost)
-        pCut->Area = (Mode == 2)? If_CutAreaDerefed( p, pCut, 100 ) : If_CutFlow( p, pCut );
+        pCut->Area = (Mode == 2)? If_CutAreaDerefed( p, pCut, IF_INFINITY ) : If_CutFlow( p, pCut );
         pCut->AveRefs = (Mode == 0)? (float)0.0 : If_CutAverageRefs( p, pCut );
         // make sure the cut is the last one (after filtering it may not be so)
         assert( pCut == p->ppCuts[iCut] );
@@ -160,7 +160,7 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode )
     assert( p->pPars->fSeqMap || If_ObjCutBest(pObj)->nLeaves > 1 );
     // ref the selected cut
     if ( Mode && pObj->nRefs > 0 )
-        If_CutRef( p, If_ObjCutBest(pObj), 100 );
+        If_CutRef( p, If_ObjCutBest(pObj), IF_INFINITY );
 }
 
 /**Function*************************************************************
@@ -182,7 +182,7 @@ void If_ObjPerformMappingChoice( If_Man_t * p, If_Obj_t * pObj, int Mode )
     assert( pObj->pEquiv != NULL );
     // prepare
     if ( Mode && pObj->nRefs > 0 )
-        If_CutDeref( p, If_ObjCutBest(pObj), 100 );
+        If_CutDeref( p, If_ObjCutBest(pObj), IF_INFINITY );
     // prepare room for the next cut
     p->nCuts = 0;
     iCut = p->nCuts;
@@ -207,7 +207,7 @@ void If_ObjPerformMappingChoice( If_Man_t * p, If_Obj_t * pObj, int Mode )
             // set the phase attribute
             pCut->fCompl ^= (pObj->fPhase ^ pTemp->fPhase);
             // compute area of the cut (this area may depend on the application specific cost)
-            pCut->Area = (Mode == 2)? If_CutAreaDerefed( p, pCut, 100 ) : If_CutFlow( p, pCut );
+            pCut->Area = (Mode == 2)? If_CutAreaDerefed( p, pCut, IF_INFINITY ) : If_CutFlow( p, pCut );
             pCut->AveRefs = (Mode == 0)? (float)0.0 : If_CutAverageRefs( p, pCut );
             // make sure the cut is the last one (after filtering it may not be so)
             assert( pCut == p->ppCuts[iCut] );
@@ -237,7 +237,7 @@ void If_ObjPerformMappingChoice( If_Man_t * p, If_Obj_t * pObj, int Mode )
     assert( p->pPars->fSeqMap || If_ObjCutBest(pObj)->nLeaves > 1 );
     // ref the selected cut
     if ( Mode && pObj->nRefs > 0 )
-        If_CutRef( p, If_ObjCutBest(pObj), 100 );
+        If_CutRef( p, If_ObjCutBest(pObj), IF_INFINITY );
 }
 
 /**Function*************************************************************

src/map/if/ifReduce.c

@@ -156,17 +156,17 @@ void If_ManImproveNodeExpand( If_Man_t * p, If_Obj_t * pObj, int nLimit, Vec_Ptr
     // get the delay
     DelayOld = pCut->Delay;
     // get the area
-    AreaBef = If_CutAreaRefed( p, pCut, 100000 );
+    AreaBef = If_CutAreaRefed( p, pCut, IF_INFINITY );
 //    if ( AreaBef == 1 )
 //        return;
     // the cut is non-trivial
     If_ManImproveNodePrepare( p, pObj, nLimit, vFront, vFrontOld, vVisited );
     // iteratively modify the cut
-    If_CutDeref( p, pCut, 100000 );
+    If_CutDeref( p, pCut, IF_INFINITY );
     CostBef = If_ManImproveCutCost( p, vFront );
     If_ManImproveNodeFaninCompact( p, pObj, nLimit, vFront, vVisited );
     CostAft = If_ManImproveCutCost( p, vFront );
-    If_CutRef( p, pCut, 100000 );
+    If_CutRef( p, pCut, IF_INFINITY );
     assert( CostBef >= CostAft );
     // clean up
     Vec_PtrForEachEntry( vVisited, pFanin, i )
@@ -175,11 +175,11 @@ void If_ManImproveNodeExpand( If_Man_t * p, If_Obj_t * pObj, int nLimit, Vec_Ptr
     If_ManImproveNodeUpdate( p, pObj, vFront );
     pCut->Delay = If_CutDelay( p, pCut );
     // get the new area
-    AreaAft = If_CutAreaRefed( p, pCut, 100000 );
+    AreaAft = If_CutAreaRefed( p, pCut, IF_INFINITY );
     if ( AreaAft > AreaBef || pCut->Delay > pObj->Required + p->fEpsilon )
     {
         If_ManImproveNodeUpdate( p, pObj, vFrontOld );
-        AreaAft = If_CutAreaRefed( p, pCut, 100000 );
+        AreaAft = If_CutAreaRefed( p, pCut, IF_INFINITY );
         assert( AreaAft == AreaBef );
         pCut->Delay = DelayOld;
     }
@@ -257,13 +257,13 @@ void If_ManImproveNodeUpdate( If_Man_t * p, If_Obj_t * pObj, Vec_Ptr_t * vFront
     int i;
     pCut = If_ObjCutBest(pObj);
     // deref node's cut
-    If_CutDeref( p, pCut, 10000 );
+    If_CutDeref( p, pCut, IF_INFINITY );
     // update the node's cut
     pCut->nLeaves = Vec_PtrSize(vFront);
     Vec_PtrForEachEntry( vFront, pFanin, i )
         pCut->pLeaves[i] = pFanin->Id;
     // ref the new cut
-    If_CutRef( p, pCut, 10000 );
+    If_CutRef( p, pCut, IF_INFINITY );
 }
 
 
@@ -506,9 +506,9 @@ void If_ManImproveNodeReduce( If_Man_t * p, If_Obj_t * pObj, int nLimit )
 
     // deref the cut if the node is refed
     if ( pObj->nRefs > 0 )
-        If_CutDeref( p, pCut, 100000 );
+        If_CutDeref( p, pCut, IF_INFINITY );
     // get the area
-    AreaBef = If_CutAreaDerefed( p, pCut, 100000 );
+    AreaBef = If_CutAreaDerefed( p, pCut, IF_INFINITY );
     // get the fanin support
     if ( pFanin0->nRefs > 2 && pCut0->Delay < pObj->Required + p->fEpsilon )
 //    if ( pSupp0->nRefs > 0 && pSupp0->Delay < pSupp->DelayR ) // this leads to 2% worse results
@@ -534,7 +534,7 @@ void If_ManImproveNodeReduce( If_Man_t * p, If_Obj_t * pObj, int nLimit )
     if ( RetValue )
     {
         pCutR->Delay = If_CutDelay( p, pCutR );
-        AreaAft = If_CutAreaDerefed( p, pCutR, 100000 );
+        AreaAft = If_CutAreaDerefed( p, pCutR, IF_INFINITY );
         // update the best cut
         if ( AreaAft < AreaBef - p->fEpsilon && pCutR->Delay < pObj->Required + p->fEpsilon )
             If_CutCopy( pCut, pCutR );
@@ -543,7 +543,7 @@ void If_ManImproveNodeReduce( If_Man_t * p, If_Obj_t * pObj, int nLimit )
     pCut->Delay = If_CutDelay( p, pCut );
     // ref the cut if the node is refed
     if ( pObj->nRefs > 0 )
-        If_CutRef( p, pCut, 100000 );
+        If_CutRef( p, pCut, IF_INFINITY );
 }
 
 /**Function*************************************************************

src/map/mio/mioFunc.c

@@ -213,7 +213,7 @@ int Mio_GateParseFormula( Mio_Gate_t * pGate )
     Cudd_Ref( pGate->bFunc );
 
     // derive the cover (SOP)
-    pGate->pSop = Abc_ConvertBddToSop( pGate->pLib->pMmFlex, dd, pGate->bFunc, pGate->bFunc, nPins, pGate->pLib->vCube, -1 );
+    pGate->pSop = Abc_ConvertBddToSop( pGate->pLib->pMmFlex, dd, pGate->bFunc, pGate->bFunc, nPins, 0, pGate->pLib->vCube, -1 );
     return 0;
 }
 

src/misc/extra/extra.h

@@ -169,6 +169,7 @@ extern int          Extra_bddIsVar( DdNode * bFunc );
 extern DdNode *     Extra_bddCreateAnd( DdManager * dd, int nVars );
 extern DdNode *     Extra_bddCreateOr( DdManager * dd, int nVars );
 extern DdNode *     Extra_bddCreateExor( DdManager * dd, int nVars );
+extern DdNode *     Extra_zddPrimes( DdManager * dd, DdNode * F );
 
 /*=== extraBddKmap.c ================================================================*/
 

src/misc/extra/extraBddMisc.c

@@ -55,6 +55,8 @@ static DdNode * extraTransferPermute( DdManager * ddS, DdManager * ddD, DdNode *
 static void ddSupportStep(DdNode *f, int *support);
 static void ddClearFlag(DdNode *f);
 
+static DdNode* extraZddPrimes( DdManager *dd, DdNode* F );
+
 /**AutomaticEnd***************************************************************/
 
 /*---------------------------------------------------------------------------*/
@@ -890,6 +892,30 @@ DdNode * Extra_bddCreateExor( DdManager * dd, int nVars )
     return bFunc;
 }
 
+/**Function********************************************************************
+
+  Synopsis    [Computes the set of primes as a ZDD.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+DdNode * Extra_zddPrimes( DdManager * dd, DdNode * F )
+{
+    DdNode    *res;
+    do {
+        dd->reordered = 0;
+        res = extraZddPrimes(dd, F);
+        if ( dd->reordered == 1 )
+            printf("\nReordering in Extra_zddPrimes()\n");
+    } while (dd->reordered == 1);
+    return(res);
+
+} /* end of Extra_zddPrimes */
+
 
 /*---------------------------------------------------------------------------*/
 /* Definition of internal functions                                          */
@@ -1246,6 +1272,201 @@ ddClearFlag(
 } /* end of ddClearFlag */
 
 
+/**Function********************************************************************
+
+  Synopsis    [Composed three subcovers into one ZDD.]
+
+  Description []
+
+  SideEffects [None]
+
+  SeeAlso     []
+
+******************************************************************************/
+DdNode *
+extraComposeCover( 
+  DdManager* dd,    /* the manager */
+  DdNode* zC0,     /* the pointer to the negative var cofactor */ 
+  DdNode* zC1,     /* the pointer to the positive var cofactor */ 
+  DdNode* zC2,     /* the pointer to the cofactor without var */ 
+  int TopVar)    /* the index of the positive ZDD var */
+{
+    DdNode * zRes, * zTemp;
+    /* compose with-neg-var and without-var using the neg ZDD var */
+    zTemp = cuddZddGetNode( dd, 2*TopVar + 1, zC0, zC2 );
+    if ( zTemp == NULL ) 
+    {
+        Cudd_RecursiveDerefZdd(dd, zC0);
+        Cudd_RecursiveDerefZdd(dd, zC1);
+        Cudd_RecursiveDerefZdd(dd, zC2);
+        return NULL;
+    }
+    cuddRef( zTemp );
+    cuddDeref( zC0 );
+    cuddDeref( zC2 );
+
+    /* compose with-pos-var and previous result using the pos ZDD var */
+    zRes = cuddZddGetNode( dd, 2*TopVar, zC1, zTemp );
+    if ( zRes == NULL ) 
+    {
+        Cudd_RecursiveDerefZdd(dd, zC1);
+        Cudd_RecursiveDerefZdd(dd, zTemp);
+        return NULL;
+    }
+    cuddDeref( zC1 );
+    cuddDeref( zTemp );
+    return zRes;
+} /* extraComposeCover */
+
+/**Function********************************************************************
+
+  Synopsis    [Performs the recursive step of prime computation.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+DdNode* extraZddPrimes( DdManager *dd, DdNode* F )
+{
+    DdNode *zRes;
+
+    if ( F == Cudd_Not( dd->one ) )
+        return dd->zero;
+    if ( F == dd->one )
+        return dd->one;
+
+    /* check cache */
+    zRes = cuddCacheLookup1Zdd(dd, extraZddPrimes, F);
+    if (zRes)
+        return(zRes);
+    {
+        /* temporary variables */
+        DdNode *bF01, *zP0, *zP1;
+        /* three components of the prime set */
+        DdNode *zResE, *zResP, *zResN;
+        int fIsComp = Cudd_IsComplement( F );
+
+        /* find cofactors of F */
+        DdNode * bF0 = Cudd_NotCond( Cudd_E( F ), fIsComp );
+        DdNode * bF1 = Cudd_NotCond( Cudd_T( F ), fIsComp );
+
+        /* find the intersection of cofactors */
+        bF01 = cuddBddAndRecur( dd, bF0, bF1 );
+        if ( bF01 == NULL ) return NULL;
+        cuddRef( bF01 );
+
+        /* solve the problems for cofactors */
+        zP0 = extraZddPrimes( dd, bF0 );
+        if ( zP0 == NULL )
+        {
+            Cudd_RecursiveDeref( dd, bF01 );
+            return NULL;
+        }
+        cuddRef( zP0 );
+
+        zP1 = extraZddPrimes( dd, bF1 );
+        if ( zP1 == NULL )
+        {
+            Cudd_RecursiveDeref( dd, bF01 );
+            Cudd_RecursiveDerefZdd( dd, zP0 );
+            return NULL;
+        }
+        cuddRef( zP1 );
+
+        /* check for local unateness */
+        if ( bF01 == bF0 )       /* unate increasing */
+        {
+            /* intersection is useless */
+            cuddDeref( bF01 );
+            /* the primes of intersection are the primes of F0 */
+            zResE = zP0;
+            /* there are no primes with negative var */
+            zResN = dd->zero;
+            cuddRef( zResN );
+            /* primes with positive var are primes of F1 that are not primes of F01 */
+            zResP = cuddZddDiff( dd, zP1, zP0 );
+            if ( zResP == NULL )  
+            {
+                Cudd_RecursiveDerefZdd( dd, zResE );
+                Cudd_RecursiveDerefZdd( dd, zResN );
+                Cudd_RecursiveDerefZdd( dd, zP1 );
+                return NULL;
+            }
+            cuddRef( zResP );
+            Cudd_RecursiveDerefZdd( dd, zP1 );
+        }
+        else if ( bF01 == bF1 ) /* unate decreasing */
+        {
+            /* intersection is useless */
+            cuddDeref( bF01 );
+            /* the primes of intersection are the primes of F1 */
+            zResE = zP1;
+            /* there are no primes with positive var */
+            zResP = dd->zero;
+            cuddRef( zResP );
+            /* primes with negative var are primes of F0 that are not primes of F01 */
+            zResN = cuddZddDiff( dd, zP0, zP1 );
+            if ( zResN == NULL )  
+            {
+                Cudd_RecursiveDerefZdd( dd, zResE );
+                Cudd_RecursiveDerefZdd( dd, zResP );
+                Cudd_RecursiveDerefZdd( dd, zP0 );
+                return NULL;
+            }
+            cuddRef( zResN );
+            Cudd_RecursiveDerefZdd( dd, zP0 );
+        }
+        else /* not unate */
+        {
+            /* primes without the top var are primes of F10 */
+            zResE = extraZddPrimes( dd, bF01 );
+            if ( zResE == NULL )  
+            {
+                Cudd_RecursiveDerefZdd( dd, bF01 );
+                Cudd_RecursiveDerefZdd( dd, zP0 );
+                Cudd_RecursiveDerefZdd( dd, zP1 );
+                return NULL;
+            }
+            cuddRef( zResE );
+            Cudd_RecursiveDeref( dd, bF01 );
+
+            /* primes with the negative top var are those of P0 that are not in F10 */
+            zResN = cuddZddDiff( dd, zP0, zResE );
+            if ( zResN == NULL )  
+            {
+                Cudd_RecursiveDerefZdd( dd, zResE );
+                Cudd_RecursiveDerefZdd( dd, zP0 );
+                Cudd_RecursiveDerefZdd( dd, zP1 );
+                return NULL;
+            }
+            cuddRef( zResN );
+            Cudd_RecursiveDerefZdd( dd, zP0 );
+
+            /* primes with the positive top var are those of P1 that are not in F10 */
+            zResP = cuddZddDiff( dd, zP1, zResE );
+            if ( zResP == NULL )  
+            {
+                Cudd_RecursiveDerefZdd( dd, zResE );
+                Cudd_RecursiveDerefZdd( dd, zResN );
+                Cudd_RecursiveDerefZdd( dd, zP1 );
+                return NULL;
+            }
+            cuddRef( zResP );
+            Cudd_RecursiveDerefZdd( dd, zP1 );
+        }
+
+        zRes = extraComposeCover( dd, zResN, zResP, zResE, Cudd_Regular(F)->index );
+        if ( zRes == NULL ) return NULL;
+
+        /* insert the result into cache */
+        cuddCacheInsert1(dd, extraZddPrimes, F, zRes);
+        return zRes;
+    }
+} /* end of extraZddPrimes */
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////

src/opt/kit/kitFactor.c

@@ -64,7 +64,7 @@ Kit_Graph_t * Kit_SopFactor( Vec_Int_t * vCover, int fCompl, int nVars, Vec_Int_
     // check for trivial functions
     if ( Vec_IntSize(vCover) == 0 )
         return Kit_GraphCreateConst0();
-    if ( Vec_IntSize(vCover) == 1 && Vec_IntEntry(vCover, 0) == (int)Kit_CubeMask(nVars) )
+    if ( Vec_IntSize(vCover) == 1 && Vec_IntEntry(vCover, 0) == 0 ) //(int)Kit_CubeMask(2 * nVars) )
         return Kit_GraphCreateConst1();
 
     // prepare memory manager

src/opt/kit/kitIsop.c

@@ -72,6 +72,7 @@ int Kit_TruthIsop( unsigned * puTruth, int nVars, Vec_Int_t * vMemory, int fTryB
     assert( Extra_TruthIsEqual( puTruth, pResult, nVars ) );
     if ( pcRes->nCubes == 0 || (pcRes->nCubes == 1 && pcRes->pCubes[0] == 0) )
     {
+        vMemory->pArray[0] = 0;
         Vec_IntShrink( vMemory, pcRes->nCubes );
         return 0;
     }

src/opt/res/resDivs.c

@@ -25,8 +25,6 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static int Res_WinVisitMffc( Res_Win_t * p );
-
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////

src/sat/asat/satTrace.c

+/**CFile****************************************************************
+
+  FileName    [satTrace.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [C-language MiniSat solver.]
+
+  Synopsis    [Records the trace of SAT solving in the CNF form.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: satTrace.c,v 1.4 2005/09/16 22:55:03 casem Exp $]
+
+***********************************************************************/
+
+#include <stdio.h>
+#include <assert.h>
+#include "solver.h"
+
+/*
+    The trace of SAT solving contains the original clause of the problem
+    along with the learned clauses derived during SAT solving.
+    The first line of the resulting file contains 3 numbers instead of 2:
+    c <num_vars> <num_all_clauses> <num_root_clauses>
+*/
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static inline int  lit_var  (lit l)        { return l >> 1; }
+static inline int  lit_sign (lit l)        { return l & 1; }
+static inline int  lit_print(lit l)        { return lit_sign(l)? -lit_var(l)-1 : lit_var(l)+1; }
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Start the trace recording.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Sat_SolverTraceStart( solver * pSat, char * pName )
+{
+    assert( pSat->pFile == NULL );
+    pSat->pFile = fopen( pName, "w" );
+    fprintf( pSat->pFile, "                                        \n" );
+    pSat->nClauses = 0;
+    pSat->nRoots = 0;
+}   
+
+/**Function*************************************************************
+
+  Synopsis    [Stops the trace recording.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Sat_SolverTraceStop( solver * pSat )
+{
+    if ( pSat->pFile == NULL )
+        return;
+    rewind( pSat->pFile );
+    fprintf( pSat->pFile, "p %d %d %d", solver_nvars(pSat), pSat->nClauses, pSat->nRoots );
+    fclose( pSat->pFile );
+    pSat->pFile = NULL;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Writes one clause into the trace file.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Sat_SolverTraceWrite( solver * pSat, int * pBeg, int * pEnd, int fRoot )
+{
+    if ( pSat->pFile == NULL )
+        return;
+    pSat->nClauses++;
+    pSat->nRoots += fRoot;
+    for ( ; pBeg < pEnd ; pBeg++ )
+        fprintf( pSat->pFile, " %d", lit_print(*pBeg) );
+    fprintf( pSat->pFile, " 0\n" );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+

src/sat/asat/solver.c

@@ -20,6 +20,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 // Modified to compile with MS Visual Studio 6.0 by Alan Mishchenko
 
 #include <stdio.h>
+#include <string.h>
 #include <assert.h>
 #include <math.h>
 #include <time.h>
@@ -505,6 +506,8 @@ static void solver_record(solver* s, veci* cls)
     clause* c     = (veci_size(cls) > 1) ? clause_new(s,begin,end,1) : (clause*)0;
     enqueue(s,*begin,c);
 
+Sat_SolverTraceWrite( s, begin, end, 0 );
+
     assert(veci_size(cls) > 0);
 
     if (c != 0) {
@@ -948,6 +951,7 @@ static lbool solver_search(solver* s, int nof_conflicts, int nof_learnts)
 solver* solver_new(void)
 {
     solver* s = (solver*)malloc(sizeof(solver));
+    memset( s, 0, sizeof(solver) );
 
     // initialize vectors
     vec_new(&s->clauses);
@@ -1100,7 +1104,10 @@ bool solver_addclause(solver* s, lit* begin, lit* end)
 
     if (j == begin)          // empty clause
         return 0;
-    else if (j - begin == 1) // unit clause
+
+Sat_SolverTraceWrite( s, begin, end, 1 );
+
+    if (j - begin == 1) // unit clause
         return enqueue(s,*begin,(clause*)0);
 
     // create new clause

src/sat/asat/solver.h

@@ -91,6 +91,11 @@ extern void    Asat_SatPrintStats( FILE * pFile, solver * p );
 extern void    Asat_SolverSetPrefVars( solver * s, int * pPrefVars, int nPrefVars );
 extern void    Asat_SolverSetFactors( solver * s, float * pFactors );
 
+// trace recording
+extern void    Sat_SolverTraceStart( solver * pSat, char * pName );
+extern void    Sat_SolverTraceStop( solver * pSat );
+extern void    Sat_SolverTraceWrite( solver * pSat, int * pBeg, int * pEnd, int fRoot );
+
 // J-frontier support
 extern Asat_JMan_t * Asat_JManStart( solver * pSat, void * vCircuit );
 extern void          Asat_JManStop(  solver * pSat );
@@ -170,6 +175,11 @@ struct solver_t
     int      timeTotal;
     int      timeSelect;
     int      timeUpdate;
+
+    // trace recording
+    FILE *   pFile;
+    int      nClauses;
+    int      nRoots;
 };
  
 #ifdef __cplusplus

src/sat/csat/csat_apis.c

@@ -90,7 +90,7 @@ ABC_Manager ABC_InitManager()
     // set default parameters for CEC
     Prove_ParamsSetDefault( &mng->Params );
     // set infinite resource limit for the final mitering
-    mng->Params.nMiteringLimitLast = ABC_INFINITY;
+//    mng->Params.nMiteringLimitLast = ABC_INFINITY;
     return mng;
 }
 

src/sat/fraig/fraigMan.c

@@ -74,6 +74,39 @@ void Prove_ParamsSetDefault( Prove_Params_t * pParams )
 
 /**Function*************************************************************
 
+  Synopsis    [Prints out the current values of CEC engine parameters.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Prove_ParamsPrint( Prove_Params_t * pParams )
+{
+    printf( "CEC enging parameters:\n" );
+    printf( "Fraiging enabled: %s\n", pParams->fUseFraiging? "yes":"no" );
+    printf( "Rewriting enabled: %s\n", pParams->fUseRewriting? "yes":"no" );
+    printf( "BDD construction enabled: %s\n", pParams->fUseBdds? "yes":"no" );
+    printf( "Verbose output enabled: %s\n", pParams->fVerbose? "yes":"no" );
+    printf( "Solver iterations: %d\n", pParams->nItersMax );
+    printf( "Starting mitering limit: %d\n", pParams->nMiteringLimitStart );
+    printf( "Multiplicative coeficient for mitering: %.2f\n", pParams->nMiteringLimitMulti );
+    printf( "Starting number of rewriting iterations: %d\n", pParams->nRewritingLimitStart );
+    printf( "Multiplicative coeficient for rewriting: %.2f\n", pParams->nRewritingLimitMulti );
+    printf( "Starting number of conflicts in fraiging: %d\n", pParams->nFraigingLimitMulti );
+    printf( "Multiplicative coeficient for fraiging: %.2f\n", pParams->nRewritingLimitMulti );
+    printf( "BDD size limit for bailing out: %.2f\n", pParams->nBddSizeLimit );
+    printf( "BDD reordering enabled: %s\n", pParams->fBddReorder? "yes":"no" );
+    printf( "Last-gasp mitering limit: %d\n", pParams->nMiteringLimitLast );
+    printf( "Total conflict limit: %d\n", pParams->nTotalBacktrackLimit );
+    printf( "Total inspection limit: %d\n", pParams->nTotalInspectLimit );
+    printf( "Parameter dump complete.\n" );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Sets the default parameters of the package.]
 
   Description [This set of parameters is tuned for equivalence checking.]

src/sat/proof/pr.c

+/**CFile****************************************************************
+
+  FileName    [pr.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Proof recording.]
+
+  Synopsis    [Core procedures of the package.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: pr.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include <stdio.h>
+#include <stdlib.h>
+#include <string.h>
+#include <assert.h>
+#include <time.h>
+#include "vec.h"
+#include "pr.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef unsigned lit;
+
+typedef struct Pr_Cls_t_ Pr_Cls_t;
+struct Pr_Cls_t_
+{
+    unsigned        uTruth;       // interpolant
+    void *          pProof;       // the proof node 
+//    void *          pAntis;       // the anticedents
+    Pr_Cls_t *      pNext;        // the next clause
+    Pr_Cls_t *      pNext0;       // the next 0-watch
+    Pr_Cls_t *      pNext1;       // the next 0-watch
+    int             Id;           // the clause ID
+    unsigned        fA     :  1;  // belongs to A
+    unsigned        fRoot  :  1;  // original clause
+    unsigned        fVisit :  1;  // visited clause
+    unsigned        nLits  : 24;  // the number of literals
+    lit             pLits[0];     // literals of this clause
+};
+
+struct Pr_Man_t_
+{
+    // general data
+    int             fProofWrite;  // writes the proof file
+    int             fProofVerif;  // verifies the proof
+    int             nVars;        // the number of variables
+    int             nVarsAB;      // the number of global variables
+    int             nRoots;       // the number of root clauses
+    int             nClauses;     // the number of all clauses
+    int             nClausesA;    // the number of clauses of A 
+    Pr_Cls_t *      pHead;        // the head clause
+    Pr_Cls_t *      pTail;        // the tail clause
+    Pr_Cls_t *      pLearnt;      // the tail clause
+    Pr_Cls_t *      pEmpty;       // the empty clause
+    // internal BCP
+    int             nRootSize;    // the number of root level assignments
+    int             nTrailSize;   // the number of assignments made 
+    lit *           pTrail;       // chronological order of assignments (size nVars)
+    lit *           pAssigns;     // assignments by variable (size nVars) 
+    char *          pSeens;       // temporary mark (size nVars)
+    char *          pVarTypes;    // variable type (size nVars) [1=A, 0=B, <0=AB]
+    Pr_Cls_t **     pReasons;     // reasons for each assignment (size nVars)          
+    Pr_Cls_t **     pWatches;     // watched clauses for each literal (size 2*nVars)          
+    int             nVarsAlloc;   // the allocated size of arrays
+    // proof recording
+    void *          pManProof;    // proof manager
+    int             Counter;      // counter of resolved clauses
+    // memory management
+    int             nChunkSize;   // the number of bytes in a chunk
+    int             nChunkUsed;   // the number of bytes used in the last chunk
+    char *          pChunkLast;   // the last memory chunk
+    // internal verification
+    lit *           pResLits;     // the literals of the resolvent   
+    int             nResLits;     // the number of literals of the resolvent
+    int             nResLitsAlloc;// the number of literals of the resolvent
+    // runtime stats
+    int             timeBcp;
+    int             timeTrace;
+    int             timeRead;
+    int             timeTotal;
+};
+
+#ifndef PRT
+#define PRT(a,t)  printf("%s = ", (a)); printf("%6.2f sec\n", (float)(t)/(float)(CLOCKS_PER_SEC))
+#endif
+
+// variable assignments 
+static const lit  LIT_UNDEF = 0xffffffff;
+
+// variable/literal conversions (taken from MiniSat)
+static inline lit   toLit    (int v)        { return v + v;  }
+static inline lit   toLitCond(int v, int c) { return v + v + (c != 0); }
+static inline lit   lit_neg  (lit l)        { return l ^ 1;  }
+static inline int   lit_var  (lit l)        { return l >> 1; }
+static inline int   lit_sign (lit l)        { return l & 1;  }
+static inline int   lit_print(lit l)        { return lit_sign(l)? -lit_var(l)-1 : lit_var(l)+1; }
+static inline lit   lit_read (int s)        { return s > 0 ? toLit(s-1) : lit_neg(toLit(-s-1)); }
+static inline int   lit_check(lit l, int n) { return l >= 0 && lit_var(l) < n;                  }
+
+// iterators through the clauses
+#define Pr_ManForEachClause( p, pCls )        for( pCls = p->pHead; pCls; pCls = pCls->pNext )
+#define Pr_ManForEachClauseRoot( p, pCls )    for( pCls = p->pHead; pCls != p->pLearnt; pCls = pCls->pNext )
+#define Pr_ManForEachClauseLearnt( p, pCls )  for( pCls = p->pLearnt; pCls; pCls = pCls->pNext )
+
+// static procedures
+static char *     Pr_ManMemoryFetch( Pr_Man_t * p, int nBytes );
+static void       Pr_ManMemoryStop( Pr_Man_t * p );
+static void       Pr_ManResize( Pr_Man_t * p, int nVarsNew );
+
+// exported procedures
+extern Pr_Man_t * Pr_ManAlloc( int nVarsAlloc );
+extern void       Pr_ManFree( Pr_Man_t * p );
+extern int        Pr_ManAddClause( Pr_Man_t * p, lit * pBeg, lit * pEnd, int fRoot, int fClauseA );
+extern int        Pr_ManProofWrite( Pr_Man_t * p );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Allocate proof manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Pr_Man_t * Pr_ManAlloc( int nVarsAlloc )
+{
+    Pr_Man_t * p;
+    // allocate the manager
+    p = (Pr_Man_t *)malloc( sizeof(Pr_Man_t) );
+    memset( p, 0, sizeof(Pr_Man_t) );
+    // allocate internal arrays
+    Pr_ManResize( p, nVarsAlloc? nVarsAlloc : 256 );
+    // set the starting number of variables
+    p->nVars = 0;
+    // memory management
+    p->nChunkSize = (1<<18); // use 256K chunks
+    // verification
+    p->nResLitsAlloc = (1<<16);
+    p->pResLits = malloc( sizeof(lit) * p->nResLitsAlloc );
+    // parameters
+    p->fProofWrite = 0;
+    p->fProofVerif = 0;
+    return p;    
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Resize proof manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Pr_ManResize( Pr_Man_t * p, int nVarsNew )
+{
+    // check if resizing is needed
+    if ( p->nVarsAlloc < nVarsNew )
+    {
+        int nVarsAllocOld = p->nVarsAlloc;
+        // find the new size
+        if ( p->nVarsAlloc == 0 )
+            p->nVarsAlloc = 1;
+        while ( p->nVarsAlloc < nVarsNew ) 
+            p->nVarsAlloc *= 2;
+        // resize the arrays
+        p->pTrail    = (lit *)      realloc( p->pTrail,    sizeof(lit) * p->nVarsAlloc );
+        p->pAssigns  = (lit *)      realloc( p->pAssigns,  sizeof(lit) * p->nVarsAlloc );
+        p->pSeens    = (char *)     realloc( p->pSeens,    sizeof(char) * p->nVarsAlloc );
+        p->pVarTypes = (char *)     realloc( p->pVarTypes, sizeof(char) * p->nVarsAlloc );
+        p->pReasons  = (Pr_Cls_t **)realloc( p->pReasons,  sizeof(Pr_Cls_t *) * p->nVarsAlloc );
+        p->pWatches  = (Pr_Cls_t **)realloc( p->pWatches,  sizeof(Pr_Cls_t *) * p->nVarsAlloc*2 );
+        // clean the free space
+        memset( p->pAssigns  + nVarsAllocOld, 0xff, sizeof(lit) * (p->nVarsAlloc - nVarsAllocOld) );
+        memset( p->pSeens    + nVarsAllocOld, 0, sizeof(char) * (p->nVarsAlloc - nVarsAllocOld) );
+        memset( p->pVarTypes + nVarsAllocOld, 0, sizeof(char) * (p->nVarsAlloc - nVarsAllocOld) );
+        memset( p->pReasons  + nVarsAllocOld, 0, sizeof(Pr_Cls_t *) * (p->nVarsAlloc - nVarsAllocOld) );
+        memset( p->pWatches  + nVarsAllocOld, 0, sizeof(Pr_Cls_t *) * (p->nVarsAlloc - nVarsAllocOld)*2 );
+    }
+    // adjust the number of variables
+    if ( p->nVars < nVarsNew )
+        p->nVars = nVarsNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Deallocate proof manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Pr_ManFree( Pr_Man_t * p )
+{
+    printf( "Runtime stats:\n" );
+PRT( "Reading ", p->timeRead  );
+PRT( "BCP     ", p->timeBcp   );
+PRT( "Trace   ", p->timeTrace );
+PRT( "TOTAL   ", p->timeTotal );
+
+    Pr_ManMemoryStop( p );
+    free( p->pTrail );
+    free( p->pAssigns );
+    free( p->pSeens );
+    free( p->pVarTypes );
+    free( p->pReasons );
+    free( p->pWatches );
+    free( p->pResLits );
+    free( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Adds one clause to the watcher list.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Pr_ManWatchClause( Pr_Man_t * p, Pr_Cls_t * pClause, lit Lit )
+{
+    assert( lit_check(Lit, p->nVars) );
+    if ( pClause->pLits[0] == Lit )
+        pClause->pNext0 = p->pWatches[lit_neg(Lit)];  
+    else
+    {
+        assert( pClause->pLits[1] == Lit );
+        pClause->pNext1 = p->pWatches[lit_neg(Lit)];  
+    }
+    p->pWatches[lit_neg(Lit)] = pClause;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Adds one clause to the manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Pr_ManAddClause( Pr_Man_t * p, lit * pBeg, lit * pEnd, int fRoot, int fClauseA )
+{
+    Pr_Cls_t * pClause;
+    lit Lit, * i, * j;
+    int nSize, VarMax;
+
+    // process the literals
+    if ( pBeg < pEnd )
+    {
+        // insertion sort
+        VarMax = lit_var( *pBeg );
+        for ( i = pBeg + 1; i < pEnd; i++ )
+        {
+            Lit = *i;
+            VarMax = lit_var(Lit) > VarMax ? lit_var(Lit) : VarMax;
+            for ( j = i; j > pBeg && *(j-1) > Lit; j-- )
+                *j = *(j-1);
+            *j = Lit;
+        }
+        // make sure there is no duplicated variables
+        for ( i = pBeg + 1; i < pEnd; i++ )
+            assert( lit_var(*(i-1)) != lit_var(*i) );
+        // resize the manager
+        Pr_ManResize( p, VarMax+1 );
+    }
+
+    // get memory for the clause
+    nSize = sizeof(Pr_Cls_t) + sizeof(lit) * (pEnd - pBeg);
+    pClause = (Pr_Cls_t *)Pr_ManMemoryFetch( p, nSize );
+    memset( pClause, 0, sizeof(Pr_Cls_t) );
+
+    // assign the clause
+    assert( !fClauseA || fRoot ); // clause of A is always a root clause
+    p->nRoots += fRoot;
+    p->nClausesA += fClauseA;
+    pClause->Id = p->nClauses++;
+    pClause->fA = fClauseA;
+    pClause->fRoot = fRoot;
+    pClause->nLits = pEnd - pBeg;
+    memcpy( pClause->pLits, pBeg, sizeof(lit) * (pEnd - pBeg) );
+
+    // add the clause to the list
+    if ( p->pHead == NULL )
+        p->pHead = pClause;
+    if ( p->pTail == NULL )
+        p->pTail = pClause;
+    else
+    {
+        p->pTail->pNext = pClause;
+        p->pTail = pClause;
+    }
+
+    // mark the first learnt clause
+    if ( p->pLearnt == NULL && !pClause->fRoot )
+        p->pLearnt = pClause;
+
+    // add the empty clause
+    if ( pClause->nLits == 0 )
+    {
+        if ( p->pEmpty )
+            printf( "More than one empty clause!\n" );
+        p->pEmpty = pClause;
+    }
+
+    // create watcher lists for the root clauses
+    if ( fRoot && pClause->nLits > 1 )
+    {
+        Pr_ManWatchClause( p, pClause, pClause->pLits[0] );
+        Pr_ManWatchClause( p, pClause, pClause->pLits[1] );
+    }
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Fetches memory.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Pr_ManMemoryFetch( Pr_Man_t * p, int nBytes )
+{
+    char * pMem;
+    if ( p->pChunkLast == NULL || nBytes > p->nChunkSize - p->nChunkUsed )
+    {
+        pMem = (char *)malloc( p->nChunkSize );
+        *(char **)pMem = p->pChunkLast;
+        p->pChunkLast = pMem;
+        p->nChunkUsed = sizeof(char *);
+    }
+    pMem = p->pChunkLast + p->nChunkUsed;
+    p->nChunkUsed += nBytes;
+    return pMem;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Frees memory manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Pr_ManMemoryStop( Pr_Man_t * p )
+{
+    char * pMem, * pNext;
+    if ( p->pChunkLast == NULL )
+        return;
+    for ( pMem = p->pChunkLast; pNext = *(char **)pMem; pMem = pNext )
+        free( pMem );
+    free( pMem );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Records the proof.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Extra_PrintBinary_( FILE * pFile, unsigned Sign[], int nBits )
+{
+    int Remainder, nWords;
+    int w, i;
+
+    Remainder = (nBits%(sizeof(unsigned)*8));
+    nWords    = (nBits/(sizeof(unsigned)*8)) + (Remainder>0);
+
+    for ( w = nWords-1; w >= 0; w-- )
+        for ( i = ((w == nWords-1 && Remainder)? Remainder-1: 31); i >= 0; i-- )
+            fprintf( pFile, "%c", '0' + (int)((Sign[w] & (1<<i)) > 0) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints the interpolant for one clause.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Pr_ManPrintInterOne( Pr_Man_t * p, Pr_Cls_t * pClause )
+{
+    printf( "Clause %2d :  ", pClause->Id );
+    Extra_PrintBinary_( stdout, &pClause->uTruth, (1 << p->nVarsAB) );
+    printf( "\n" );
+}
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Records implication.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Pr_ManEnqueue( Pr_Man_t * p, lit Lit, Pr_Cls_t * pReason )
+{
+    int Var = lit_var(Lit);
+    if ( p->pAssigns[Var] != LIT_UNDEF )
+        return p->pAssigns[Var] == Lit;
+    p->pAssigns[Var] = Lit;
+    p->pReasons[Var] = pReason;
+    p->pTrail[p->nTrailSize++] = Lit;
+//printf( "assigning var %d value %d\n", Var, !lit_sign(Lit) );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Records implication.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Pr_ManCancelUntil( Pr_Man_t * p, int Level )
+{
+    lit Lit;
+    int i, Var;
+    for ( i = p->nTrailSize - 1; i >= Level; i-- )
+    {
+        Lit = p->pTrail[i];
+        Var = lit_var( Lit );
+        p->pReasons[Var] = NULL;
+        p->pAssigns[Var] = LIT_UNDEF;
+//printf( "cancelling var %d\n", Var );
+    }
+    p->nTrailSize = Level;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Propagate one assignment.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Pr_Cls_t * Pr_ManPropagateOne( Pr_Man_t * p, lit Lit )
+{
+    Pr_Cls_t ** ppPrev, * pCur, * pTemp;
+    lit LitF = lit_neg(Lit);
+    int i;
+    // iterate through the literals
+    ppPrev = p->pWatches + Lit;
+    for ( pCur = p->pWatches[Lit]; pCur; pCur = *ppPrev )
+    {
+        // make sure the false literal is in the second literal of the clause
+        if ( pCur->pLits[0] == LitF )
+        {
+            pCur->pLits[0] = pCur->pLits[1];
+            pCur->pLits[1] = LitF;
+            pTemp = pCur->pNext0;
+            pCur->pNext0 = pCur->pNext1;
+            pCur->pNext1 = pTemp;
+        }
+        assert( pCur->pLits[1] == LitF );
+
+        // if the first literal is true, the clause is satisfied
+        if ( pCur->pLits[0] == p->pAssigns[lit_var(pCur->pLits[0])] )
+        {
+            ppPrev = &pCur->pNext1;
+            continue;
+        }
+
+        // look for a new literal to watch
+        for ( i = 2; i < (int)pCur->nLits; i++ )
+        {
+            // skip the case when the literal is false
+            if ( lit_neg(pCur->pLits[i]) == p->pAssigns[lit_var(pCur->pLits[i])] )
+                continue;
+            // the literal is either true or unassigned - watch it
+            pCur->pLits[1] = pCur->pLits[i];
+            pCur->pLits[i] = LitF;
+            // remove this clause from the watch list of Lit
+            *ppPrev = pCur->pNext1;
+            // add this clause to the watch list of pCur->pLits[i] (now it is pCur->pLits[1])
+            Pr_ManWatchClause( p, pCur, pCur->pLits[1] );
+            break;
+        }
+        if ( i < (int)pCur->nLits ) // found new watch
+            continue;
+
+        // clause is unit - enqueue new implication
+        if ( Pr_ManEnqueue(p, pCur->pLits[0], pCur) )
+        {
+            ppPrev = &pCur->pNext1;
+            continue;
+        }
+
+        // conflict detected - return the conflict clause
+        return pCur;
+    }
+    return NULL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Propagate the current assignments.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Pr_Cls_t * Pr_ManPropagate( Pr_Man_t * p, int Start )
+{
+    Pr_Cls_t * pClause;
+    int i;
+    int clk = clock();
+    for ( i = Start; i < p->nTrailSize; i++ )
+    {
+        pClause = Pr_ManPropagateOne( p, p->pTrail[i] );
+        if ( pClause )
+        {
+p->timeBcp += clock() - clk;
+            return pClause;
+        }
+    }
+p->timeBcp += clock() - clk;
+    return NULL;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Prints the clause.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Pr_ManPrintClause( Pr_Cls_t * pClause )
+{
+    int i;
+    printf( "Clause ID = %d. Proof = %d. {", pClause->Id, (int)pClause->pProof );
+    for ( i = 0; i < (int)pClause->nLits; i++ )
+        printf( " %d", pClause->pLits[i] );
+    printf( " }\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints the resolvent.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Pr_ManPrintResolvent( lit * pResLits, int nResLits )
+{
+    int i;
+    printf( "Resolvent: {" );
+    for ( i = 0; i < nResLits; i++ )
+        printf( " %d", pResLits[i] );
+    printf( " }\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Writes one root clause into a file.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Pr_ManProofWriteOne( Pr_Man_t * p, Pr_Cls_t * pClause )
+{
+    pClause->pProof = (void *)++p->Counter;
+
+    if ( p->fProofWrite )
+    {
+        int v;
+        fprintf( p->pManProof, "%d", (int)pClause->pProof );
+        for ( v = 0; v < (int)pClause->nLits; v++ )
+            fprintf( p->pManProof, " %d", lit_print(pClause->pLits[v]) );
+        fprintf( p->pManProof, " 0 0\n" );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Traces the proof for one clause.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Pr_ManProofTraceOne( Pr_Man_t * p, Pr_Cls_t * pConflict, Pr_Cls_t * pFinal )
+{
+    Pr_Cls_t * pReason;
+    int i, v, Var, PrevId;
+    int fPrint = 0;
+    int clk = clock();
+
+    // collect resolvent literals
+    if ( p->fProofVerif )
+    {
+        assert( (int)pConflict->nLits <= p->nResLitsAlloc );
+        memcpy( p->pResLits, pConflict->pLits, sizeof(lit) * pConflict->nLits );
+        p->nResLits = pConflict->nLits;
+    }
+
+    // mark all the variables in the conflict as seen
+    for ( v = 0; v < (int)pConflict->nLits; v++ )
+        p->pSeens[lit_var(pConflict->pLits[v])] = 1;
+
+    // start the anticedents
+//    pFinal->pAntis = Vec_PtrAlloc( 32 );
+//    Vec_PtrPush( pFinal->pAntis, pConflict );
+
+    if ( p->nClausesA )
+        pFinal->uTruth = pConflict->uTruth;
+   
+    // follow the trail backwards
+    PrevId = (int)pConflict->pProof;
+    for ( i = p->nTrailSize - 1; i >= 0; i-- )
+    {
+        // skip literals that are not involved
+        Var = lit_var(p->pTrail[i]);
+        if ( !p->pSeens[Var] )
+            continue;
+
+        // skip literals of the resulting clause
+        pReason = p->pReasons[Var];
+        if ( pReason == NULL )
+            continue;
+        assert( p->pTrail[i] == pReason->pLits[0] );
+
+        // record the reason clause
+        assert( pReason->pProof > 0 );
+        p->Counter++;
+        if ( p->fProofWrite )
+            fprintf( p->pManProof, "%d * %d %d 0\n", p->Counter, PrevId, (int)pReason->pProof );
+        PrevId = p->Counter;
+
+        if ( p->nClausesA )
+        {
+            if ( p->pVarTypes[Var] == 1 ) // var of A
+                pFinal->uTruth |= pReason->uTruth;
+            else
+                pFinal->uTruth &= pReason->uTruth;
+        }
+ 
+        // resolve the temporary resolvent with the reason clause
+        if ( p->fProofVerif )
+        {
+            int v1, v2; 
+            if ( fPrint )
+                Pr_ManPrintResolvent( p->pResLits, p->nResLits );
+            // check that the var is present in the resolvent
+            for ( v1 = 0; v1 < p->nResLits; v1++ )
+                if ( lit_var(p->pResLits[v1]) == Var )
+                    break;
+            if ( v1 == p->nResLits )
+                printf( "Recording clause %d: Cannot find variable %d in the temporary resolvent.\n", pFinal->Id, Var );
+            if ( p->pResLits[v1] != lit_neg(pReason->pLits[0]) )
+                printf( "Recording clause %d: The resolved variable %d is in the wrong polarity.\n", pFinal->Id, Var );
+            // remove this variable from the resolvent
+            assert( lit_var(p->pResLits[v1]) == Var );
+            p->nResLits--;
+            for ( ; v1 < p->nResLits; v1++ )
+                p->pResLits[v1] = p->pResLits[v1+1];
+            // add variables of the reason clause
+            for ( v2 = 1; v2 < (int)pReason->nLits; v2++ )
+            {
+                for ( v1 = 0; v1 < p->nResLits; v1++ )
+                    if ( lit_var(p->pResLits[v1]) == lit_var(pReason->pLits[v2]) )
+                        break;
+                // if it is a new variable, add it to the resolvent
+                if ( v1 == p->nResLits ) 
+                {
+                    if ( p->nResLits == p->nResLitsAlloc )
+                        printf( "Recording clause %d: Ran out of space for intermediate resolvent.\n, pFinal->Id" );
+                    p->pResLits[ p->nResLits++ ] = pReason->pLits[v2];
+                    continue;
+                }
+                // if the variable is the same, the literal should be the same too
+                if ( p->pResLits[v1] == pReason->pLits[v2] )
+                    continue;
+                // the literal is different
+                printf( "Recording clause %d: Trying to resolve the clause with more than one opposite literal.\n", pFinal->Id );
+            }
+        }
+
+        // add the variables to seen
+        for ( v = 1; v < (int)pReason->nLits; v++ )
+            p->pSeens[lit_var(pReason->pLits[v])] = 1;
+
+//        Vec_PtrPush( pFinal->pAntis, pReason );
+    }
+
+    // unmark all seen variables
+    for ( i = p->nTrailSize - 1; i >= 0; i-- )
+        p->pSeens[lit_var(p->pTrail[i])] = 0;
+
+    // use the resulting clause to check the correctness of resolution
+    if ( p->fProofVerif )
+    {
+        int v1, v2; 
+        if ( fPrint )
+            Pr_ManPrintResolvent( p->pResLits, p->nResLits );
+        for ( v1 = 0; v1 < p->nResLits; v1++ )
+        {
+            for ( v2 = 0; v2 < (int)pFinal->nLits; v2++ )
+                if ( pFinal->pLits[v2] == p->pResLits[v1] )
+                    break;
+            if ( v2 < (int)pFinal->nLits )
+                continue;
+            break;
+        }
+        if ( v1 < p->nResLits )
+        {
+            printf( "Recording clause %d: The final resolvent is wrong.\n", pFinal->Id );
+            Pr_ManPrintClause( pConflict );
+            Pr_ManPrintResolvent( p->pResLits, p->nResLits );
+            Pr_ManPrintClause( pFinal );
+        }
+    }
+p->timeTrace += clock() - clk;
+
+    // return the proof pointer 
+    if ( p->nClausesA )
+    {
+        Pr_ManPrintInterOne( p, pFinal );
+    }
+    return p->Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Records the proof for one clause.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Pr_ManProofRecordOne( Pr_Man_t * p, Pr_Cls_t * pClause )
+{
+    Pr_Cls_t * pConflict;
+    int i;
+
+    // empty clause never ends up there
+    assert( pClause->nLits > 0 );
+    if ( pClause->nLits == 0 )
+        printf( "Error: Empty clause is attempted.\n" );
+
+    // add assumptions to the trail
+    assert( !pClause->fRoot );
+    assert( p->nTrailSize == p->nRootSize );
+    for ( i = 0; i < (int)pClause->nLits; i++ )
+        if ( !Pr_ManEnqueue( p, lit_neg(pClause->pLits[i]), NULL ) )
+        {
+            assert( 0 ); // impossible
+            return 0;
+        }
+
+    // propagate the assumptions
+    pConflict = Pr_ManPropagate( p, p->nRootSize );
+    if ( pConflict == NULL )
+    {
+        assert( 0 ); // cannot prove
+        return 0;
+    }
+
+    // construct the proof
+    pClause->pProof = (void *)Pr_ManProofTraceOne( p, pConflict, pClause );
+
+    // undo to the root level
+    Pr_ManCancelUntil( p, p->nRootSize );
+
+    // add large clauses to the watched lists
+    if ( pClause->nLits > 1 )
+    {
+        Pr_ManWatchClause( p, pClause, pClause->pLits[0] );
+        Pr_ManWatchClause( p, pClause, pClause->pLits[1] );
+        return 1;
+    }
+    assert( pClause->nLits == 1 );
+
+    // if the clause proved is unit, add it and propagate
+    if ( !Pr_ManEnqueue( p, pClause->pLits[0], pClause ) )
+    {
+        assert( 0 ); // impossible
+        return 0;
+    }
+
+    // propagate the assumption
+    pConflict = Pr_ManPropagate( p, p->nRootSize );
+    if ( pConflict )
+    {
+        // construct the proof
+        p->pEmpty->pProof = (void *)Pr_ManProofTraceOne( p, pConflict, p->pEmpty );
+        printf( "Found last conflict after adding unit clause number %d!\n", pClause->Id );
+        return 0;
+    }
+
+    // update the root level
+    p->nRootSize = p->nTrailSize;
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Propagate the root clauses.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Pr_ManProcessRoots( Pr_Man_t * p )
+{
+    Pr_Cls_t * pClause;
+    int Counter;
+
+    // make sure the root clauses are preceeding the learnt clauses
+    Counter = 0;
+    Pr_ManForEachClause( p, pClause )
+    {
+        assert( (int)pClause->fA    == (Counter < (int)p->nClausesA) );
+        assert( (int)pClause->fRoot == (Counter < (int)p->nRoots)    );
+        Counter++;
+    }
+    assert( p->nClauses == Counter );
+
+    // make sure the last clause if empty
+    assert( p->pTail->nLits == 0 );
+
+    // go through the root unit clauses
+    p->nTrailSize = 0;
+    Pr_ManForEachClauseRoot( p, pClause )
+    {
+        // empty clause and large clauses
+        if ( pClause->nLits != 1 )
+            continue;
+        // unit clause
+        assert( lit_check(pClause->pLits[0], p->nVars) );
+        if ( !Pr_ManEnqueue( p, pClause->pLits[0], pClause ) )
+        {
+            // detected root level conflict
+            printf( "Pr_ManProcessRoots(): Detected a root-level conflict\n" );
+            assert( 0 );
+            return 0;
+        }
+    }
+
+    // propagate the root unit clauses
+    pClause = Pr_ManPropagate( p, 0 );
+    if ( pClause )
+    {
+        // detected root level conflict
+        printf( "Pr_ManProcessRoots(): Detected a root-level conflict\n" );
+        assert( 0 );
+        return 0;
+    }
+
+    // set the root level
+    p->nRootSize = p->nTrailSize;
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Records the proof.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Pr_ManPrepareInter( Pr_Man_t * p )
+{
+    unsigned uTruths[5] = { 0xAAAAAAAA, 0xCCCCCCCC, 0xF0F0F0F0, 0xFF00FF00, 0xFFFF0000 };
+    Pr_Cls_t * pClause;
+    int Var, v;
+
+    // mark the variable encountered in the clauses of A
+    Pr_ManForEachClauseRoot( p, pClause )
+    {
+        if ( !pClause->fA )
+            break;
+        for ( v = 0; v < (int)pClause->nLits; v++ )
+            p->pVarTypes[lit_var(pClause->pLits[v])] = 1;
+    }
+
+    // check variables that appear in clauses of B
+    p->nVarsAB = 0;
+    Pr_ManForEachClauseRoot( p, pClause )
+    {
+        if ( pClause->fA )
+            continue;
+        for ( v = 0; v < (int)pClause->nLits; v++ )
+        {
+            Var = lit_var(pClause->pLits[v]);
+            if ( p->pVarTypes[Var] == 1 ) // var of A
+            {
+                // change it into a global variable
+                p->nVarsAB++;
+                p->pVarTypes[Var] = -1;
+            }
+        }
+    }
+
+    // order global variables
+    p->nVarsAB = 0;
+    for ( v = 0; v < p->nVars; v++ )
+        if ( p->pVarTypes[v] == -1 )
+            p->pVarTypes[v] -= p->nVarsAB++;
+printf( "There are %d global variables.\n", p->nVarsAB );
+
+    // set interpolants for root clauses
+    Pr_ManForEachClauseRoot( p, pClause )
+    {
+        if ( !pClause->fA ) // clause of B
+        {
+            pClause->uTruth = ~0;
+            Pr_ManPrintInterOne( p, pClause );
+            continue;
+        }
+        // clause of A
+        pClause->uTruth = 0;
+        for ( v = 0; v < (int)pClause->nLits; v++ )
+        {
+            Var = lit_var(pClause->pLits[v]);
+            if ( p->pVarTypes[Var] < 0 ) // global var
+            {
+                if ( lit_sign(pClause->pLits[v]) ) // negative var
+                    pClause->uTruth |= ~uTruths[ -p->pVarTypes[Var]-1 ];
+                else
+                    pClause->uTruth |= uTruths[ -p->pVarTypes[Var]-1 ];
+            }
+        }
+        Pr_ManPrintInterOne( p, pClause );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Records the proof.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Pr_ManProofWrite( Pr_Man_t * p )
+{
+    Pr_Cls_t * pClause;
+    int RetValue = 1;
+
+    // propagate root level assignments
+    Pr_ManProcessRoots( p );
+
+    // prepare the interpolant computation
+    if ( p->nClausesA )
+        Pr_ManPrepareInter( p );
+
+    // construct proof for each clause
+    // start the proof
+    if ( p->fProofWrite )
+        p->pManProof = fopen( "proof.cnf_", "w" );
+    p->Counter = 0;
+
+    // write the root clauses
+    Pr_ManForEachClauseRoot( p, pClause )
+        Pr_ManProofWriteOne( p, pClause );
+
+    // consider each learned clause
+    Pr_ManForEachClauseLearnt( p, pClause )
+    {
+        if ( !Pr_ManProofRecordOne( p, pClause ) )
+        {
+            RetValue = 0;
+            break;
+        }
+    }
+
+    if ( p->nClausesA )
+    {
+        printf( "Interpolant:  " );
+    }
+
+
+    // stop the proof
+    if ( p->fProofWrite )
+    {
+        fclose( p->pManProof );
+        p->pManProof = NULL;    
+    }
+    return RetValue;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Reads clauses from file.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Pr_Man_t * Pr_ManProofRead( char * pFileName )
+{
+    Pr_Man_t * p = NULL;
+    char * pCur, * pBuffer = NULL;
+    int * pArray = NULL;
+    FILE * pFile;
+    int RetValue, Counter, nNumbers, Temp;
+    int nClauses, nClausesA, nRoots, nVars;
+
+    // open the file
+    pFile = fopen( pFileName, "r" );
+    if ( pFile == NULL )
+    {
+        printf( "Count not open input file \"%s\".\n", pFileName );
+        return NULL;
+    }
+
+    // read the file
+    pBuffer = (char *)malloc( (1<<16) );
+    for ( Counter = 0; fgets( pBuffer, (1<<16), pFile ); )
+    {
+        if ( pBuffer[0] == 'c' )
+            continue;
+        if ( pBuffer[0] == 'p' )
+        {
+            assert( p == NULL );
+            nClausesA = 0;
+            RetValue = sscanf( pBuffer + 1, "%d %d %d %d", &nVars, &nClauses, &nRoots, &nClausesA );
+            if ( RetValue != 3 && RetValue != 4 )
+            {
+                printf( "Wrong input file format.\n" );
+            }
+            p = Pr_ManAlloc( nVars );
+            pArray = (int *)malloc( sizeof(int) * (nVars + 10) );
+            continue;
+        }
+        // skip empty lines
+        for ( pCur = pBuffer; *pCur; pCur++ )
+            if ( !(*pCur == ' ' || *pCur == '\t' || *pCur == '\r' || *pCur == '\n') )
+                break;
+        if ( *pCur == 0 )
+            continue;
+        // scan the numbers from file
+        nNumbers = 0;
+        pCur = pBuffer;
+        while ( *pCur )
+        {
+            // skip spaces
+            for ( ; *pCur && *pCur == ' '; pCur++ );
+            // read next number
+            Temp = 0;
+            sscanf( pCur, "%d", &Temp );
+            if ( Temp == 0 )
+                break;
+            pArray[ nNumbers++ ] = lit_read( Temp );
+            // skip non-spaces
+            for ( ; *pCur && *pCur != ' '; pCur++ );
+        }
+        // add the clause
+        if ( !Pr_ManAddClause( p, pArray, pArray + nNumbers, Counter < nRoots, Counter < nClausesA ) )
+        {
+            printf( "Bad clause number %d.\n", Counter );
+            return NULL;
+        }
+        // count the clauses
+        Counter++;
+    }
+    // check the number of clauses
+    if ( Counter != nClauses )
+        printf( "Expected %d clauses but read %d.\n", nClauses, Counter );
+
+    // finish
+    if ( pArray ) free( pArray );
+    if ( pBuffer ) free( pBuffer );
+    fclose( pFile );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Records the proof.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+/*
+int Pr_ManProofCount_rec( Pr_Cls_t * pClause )
+{
+    Pr_Cls_t * pNext;
+    int i, Counter;    
+    if ( pClause->fRoot )
+        return 0;
+    if ( pClause->fVisit )
+        return 0;
+    pClause->fVisit = 1;
+    // count the number of visited clauses
+    Counter = 1;
+    Vec_PtrForEachEntry( pClause->pAntis, pNext, i )
+        Counter += Pr_ManProofCount_rec( pNext );
+    return Counter;
+}
+*/
+
+/**Function*************************************************************
+
+  Synopsis    [Records the proof.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Pr_ManProofTest( char * pFileName )
+{
+    Pr_Man_t * p;
+    int clk, clkTotal = clock();
+
+clk = clock();
+    p = Pr_ManProofRead( pFileName );
+p->timeRead = clock() - clk;
+    if ( p == NULL )
+        return 0;
+
+    Pr_ManProofWrite( p );
+
+    // print stats
+/*
+    nUsed = Pr_ManProofCount_rec( p->pEmpty );
+    printf( "Roots = %d. Learned = %d. Total = %d. Steps = %d.  Ave = %.2f.  Used = %d. Ratio = %.2f. \n", 
+        p->nRoots, p->nClauses-p->nRoots, p->nClauses, p->Counter,  
+        1.0*(p->Counter-p->nRoots)/(p->nClauses-p->nRoots),
+        nUsed, 1.0*nUsed/(p->nClauses-p->nRoots)  );
+*/
+    printf( "Vars = %d. Roots = %d. Learned = %d. Resolution steps = %d.  Ave = %.2f.\n", 
+        p->nVars, p->nRoots, p->nClauses-p->nRoots, p->Counter,  
+        1.0*(p->Counter-p->nRoots)/(p->nClauses-p->nRoots)  );
+
+p->timeTotal = clock() - clkTotal;
+    Pr_ManFree( p );
+    return 1;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+

src/sat/proof/pr.h

+/**CFile****************************************************************
+
+  FileName    [pr.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Proof recording.]
+
+  Synopsis    [External declarations.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: pr.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+ 
+#ifndef __PR_H__
+#define __PR_H__
+
+#ifdef __cplusplus
+extern "C" {
+#endif
+
+#ifdef _WIN32
+#define inline __inline // compatible with MS VS 6.0
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Pr_Man_t_ Pr_Man_t;
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFINITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                    FUNCTION DECLARATIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== pr.c ==========================================================*/
+ 
+#ifdef __cplusplus
+}
+#endif
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+

src/sat/proof/stats.txt

+UC Berkeley, ABC 1.01 (compiled Jan 20 2007 16:47:34)
+abc.rc: No such file or directory
+Loaded "abc.rc" from the parent directory.
+abc 01> test
+Found last conflict after adding unit clause number 10229!
+Roots = 7184. Learned = 3047. Total = 10231. Steps = 196361.  Ave = 62.09.  Used = 2224. Ratio = 0.73.
+Runtime stats:
+Reading  =   0.03 sec
+BCP      =   0.32 sec
+Trace    =   0.06 sec
+TOTAL    =   0.43 sec
+abc 01> test
+Found last conflict after adding unit clause number 7676!
+Roots = 6605. Learned = 1073. Total = 7678. Steps = 52402.  Ave = 42.68.  Used = 1011. Ratio = 0.94.
+Runtime stats:
+Reading  =   0.01 sec
+BCP      =   0.02 sec
+Trace    =   0.02 sec
+TOTAL    =   0.06 sec
+abc 01> test
+Found last conflict after adding unit clause number 37868!
+Roots = 15443. Learned = 22427. Total = 37870. Steps = 2365472.  Ave = 104.79.  Used = 19763. Ratio = 0.88.
+Runtime stats:
+Reading  =   0.20 sec
+BCP      =  14.67 sec
+Trace    =   0.56 sec
+TOTAL    =  15.74 sec
+abc 01>
+
+
+abc 05> wb ibm_bmc/len25u_renc.blif
+abc 05> ps
+(no name)    : i/o =  348/   1  lat =    0  nd =  3648  bdd  = 15522  lev = 246
+abc 05> sat -v
+==================================[MINISAT]===================================
+| Conflicts |     ORIGINAL     |              LEARNT              | Progress |
+|           | Clauses Literals |   Limit Clauses Literals  Lit/Cl |          |
+==============================================================================
+|         0 |   17413    54996 |    5804       0        0     0.0 |  0.000 % |
+|       100 |   17413    54996 |    6384     100      606     6.1 |  0.417 % |
+|       250 |   17413    54996 |    7023     250     1586     6.3 |  0.417 % |
+|       476 |   17413    54996 |    7725     476     3288     6.9 |  0.417 % |
+|       813 |   17413    54996 |    8498     813     7586     9.3 |  0.417 % |
+|      1319 |   17403    54970 |    9347    1318    14848    11.3 |  0.442 % |
+|      2078 |   17403    54970 |   10282    2076    40186    19.4 |  0.466 % |
+|      3217 |   17397    54948 |   11310    3208    99402    31.0 |  0.466 % |
+|      4926 |   17392    54930 |   12441    4911   131848    26.8 |  0.491 % |
+|      7489 |   17392    54930 |   13686    7474   204217    27.3 |  0.491 % |
+|     11336 |   17357    54829 |   15054   11310   332863    29.4 |  0.638 % |
+|     17103 |   17346    54794 |   16559    9130   203029    22.2 |  0.687 % |
+|     25752 |   17288    54606 |   18215    9083   176982    19.5 |  0.834 % |
+|     38727 |   17266    54536 |   20037   12674   278949    22.0 |  0.883 % |
+|     58188 |   17240    54453 |   22041   11905   255255    21.4 |  0.957 % |
+==============================================================================
+Start =   15. Conf =  79435. Dec = 130967. Prop = 24083434. Insp = 136774586.
+Total runtime =   18.66 sec.  Var select =    0.00 sec.  Var update =    0.00 sec.
+UNSATISFIABLE  Time =  18.69 sec
+abc 05>
+abc 05> test
+Found last conflict after adding unit clause number 96902!
+Roots = 17469. Learned = 79435. Total = 96904. Steps = 9700042.  Ave = 121.89.  Used = 57072. Ratio = 0.72.
+Runtime stats:
+Reading  =   1.26 sec
+BCP      = 204.99 sec
+Trace    =   2.85 sec
+TOTAL    = 209.85 sec
\ No newline at end of file