Prepared &gla to try abstracting and proving concurrently.

abcexe.dsp

@@ -50,7 +50,7 @@ BSC32=bscmake.exe
 # ADD BSC32 /nologo
 LINK32=link.exe
 # ADD BASE LINK32 kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32.lib ole32.lib oleaut32.lib uuid.lib odbc32.lib odbccp32.lib kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32.lib ole32.lib oleaut32.lib uuid.lib odbc32.lib odbccp32.lib /nologo /subsystem:console /machine:I386
-# ADD LINK32 kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32.lib ole32.lib oleaut32.lib uuid.lib odbc32.lib odbccp32.lib kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32.lib ole32.lib oleaut32.lib uuid.lib odbc32.lib odbccp32.lib lib\abcr.lib /nologo /subsystem:console /incremental:yes /debug /machine:I386 /out:"_TEST/abc.exe"
+# ADD LINK32 kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32.lib ole32.lib oleaut32.lib uuid.lib odbc32.lib odbccp32.lib kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32.lib ole32.lib oleaut32.lib uuid.lib odbc32.lib odbccp32.lib lib\abcr.lib lib\pthreadVC2.lib /nologo /subsystem:console /incremental:yes /debug /machine:I386 /out:"_TEST/abc.exe"
 
 !ELSEIF  "$(CFG)" == "abcexe - Win32 Debug"
 
@@ -74,7 +74,7 @@ BSC32=bscmake.exe
 # ADD BSC32 /nologo
 LINK32=link.exe
 # ADD BASE LINK32 kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32.lib ole32.lib oleaut32.lib uuid.lib odbc32.lib odbccp32.lib kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32.lib ole32.lib oleaut32.lib uuid.lib odbc32.lib odbccp32.lib /nologo /subsystem:console /debug /machine:I386 /pdbtype:sept
-# ADD LINK32 kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32.lib ole32.lib oleaut32.lib uuid.lib odbc32.lib odbccp32.lib kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32.lib ole32.lib oleaut32.lib uuid.lib odbc32.lib odbccp32.lib lib\abcd.lib /nologo /subsystem:console /debug /machine:I386 /out:"_TEST/abc.exe"
+# ADD LINK32 kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32.lib ole32.lib oleaut32.lib uuid.lib odbc32.lib odbccp32.lib kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32.lib ole32.lib oleaut32.lib uuid.lib odbc32.lib odbccp32.lib lib\abcd.lib lib\pthreadVC2.lib /nologo /subsystem:console /debug /machine:I386 /out:"_TEST/abc.exe"
 
 !ENDIF 
 

src/aig/gia/giaAbsGla2.c

@@ -129,7 +129,6 @@ static inline int Ga2_ObjFindOrAddLit( Ga2_Man_t * p, Gia_Obj_t * pObj, int f )
 // calling pthreads
 extern void Gia_Ga2ProveAbsracted( char * pFileName, int fVerbose );
 extern void Gia_Ga2ProveCancel( int fVerbose );
-extern void Gia_Ga2ProveFinish( int fVerbose );
 extern int  Gia_Ga2ProveCheck( int fVerbose );
 
 ////////////////////////////////////////////////////////////////////////
@@ -1513,7 +1512,7 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
     Ga2_Man_t * p;
     Vec_Int_t * vCore, * vPPis;
     clock_t clk2, clk = clock();
-    int Status = l_Undef, RetValue = -1, iFrameTryProve = -1, fOneIsSent = 0;
+    int Status = l_Undef, RetValue = -1, iFrameTryToProve = -1, fOneIsSent = 0;
     int i, c, f, Lit;
     // check trivial case 
     assert( Gia_ManPoNum(pAig) == 1 ); 
@@ -1616,26 +1615,27 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
                     p->nCexes++;
                     p->timeSat += clock() - clk2;
 
-                    clk2 = clock();
-                    vPPis = Ga2_ManRefine( p );
-                    p->timeCex += clock() - clk2;
-                    if ( vPPis == NULL )
-                    {
-                        if ( pPars->fVerbose )
-                            Ga2_ManAbsPrintFrame( p, f, sat_solver2_nconflicts(p->pSat)-nConflsBeg, c, clock() - clk, 1 );
-                        goto finish;
-                    }
-
                     // cancel old one if it was sent
                     if ( Abc_FrameIsBridgeMode() && fOneIsSent )
                     {
                         Gia_Ga2SendCancel( p, pPars->fVerbose );
                         fOneIsSent = 0;
                     }
-                    if ( iFrameTryProve >= 0 )
+                    if ( iFrameTryToProve >= 0 )
                     {
                         Gia_Ga2ProveCancel( pPars->fVerbose );
-                        iFrameTryProve = -1;
+                        iFrameTryToProve = -1;
+                    }
+
+                    // perform refinement
+                    clk2 = clock();
+                    vPPis = Ga2_ManRefine( p );
+                    p->timeCex += clock() - clk2;
+                    if ( vPPis == NULL )
+                    {
+                        if ( pPars->fVerbose )
+                            Ga2_ManAbsPrintFrame( p, f, sat_solver2_nconflicts(p->pSat)-nConflsBeg, c, clock() - clk, 1 );
+                        goto finish;
                     }
 
                     if ( c == 0 )
@@ -1780,11 +1780,11 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
                 if ( p->pPars->fCallProver )
                 {
                     // cancel old one if it is proving
-                    if ( iFrameTryProve >= 0 )
+                    if ( iFrameTryToProve >= 0 )
                         Gia_Ga2ProveCancel( pPars->fVerbose );
                     // prove new one
                     Gia_Ga2ProveAbsracted( Ga2_GlaGetFileName(p, 1), pPars->fVerbose );
-                    iFrameTryProve = f;
+                    iFrameTryToProve = f;
                 }
                 // speak to the bridge
                 if ( Abc_FrameIsBridgeMode() )
@@ -1812,12 +1812,11 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
 finish:
     Prf_ManStopP( &p->pSat->pPrf2 );
     // cancel old one if it is proving
-    if ( iFrameTryProve >= 0 )
+    if ( iFrameTryToProve >= 0 )
         Gia_Ga2ProveCancel( pPars->fVerbose );
-    Gia_Ga2ProveFinish( pPars->fVerbose );
     // analize the results
     if ( RetValue == 1 )
-        Abc_Print( 1, "GLA completed %d frames and proved abstraction derived in frame %d.  ", p->pPars->iFrameProved+1, iFrameTryProve );
+        Abc_Print( 1, "GLA completed %d frames and proved abstraction derived in frame %d.  ", p->pPars->iFrameProved+1, iFrameTryToProve );
     else if ( pAig->pCexSeq == NULL )
     {
 //        if ( pAig->vGateClasses != NULL )

src/aig/gia/giaAbsPth.c

@@ -22,7 +22,7 @@
 #include "proof/pdr/pdr.h"
 
 // comment this out to disable pthreads
-//#define ABC_USE_PTHREADS
+#define ABC_USE_PTHREADS
 
 #ifdef ABC_USE_PTHREADS
 
@@ -41,43 +41,31 @@ ABC_NAMESPACE_IMPL_START
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Start and stop proving abstracted model.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
 #ifndef ABC_USE_PTHREADS
 
 void Gia_Ga2ProveAbsracted( char * pFileName, int fVerbose ) {}
 void Gia_Ga2ProveCancel( int fVerbose )                      {}
-void Gia_Ga2ProveFinish( int fVerbose )                      {}
 int  Gia_Ga2ProveCheck( int fVerbose )                       { return 0; }
 
 #else // pthreads are used
 
 // information given to the thread
-typedef struct Abs_Pair_t_
+typedef struct Abs_ThData_t_
 {
     char * pFileName;
     int    fVerbose;
     int    RunId;
-} Abs_Pair_t;
+} Abs_ThData_t;
 
-// the last valid thread
-static int g_nRunIds = 0;
-int Abs_CallBackToStop( int RunId ) { assert( RunId <= g_nRunIds ); return RunId < g_nRunIds; }
+// mutext to control access to shared variables
+pthread_mutex_t g_mutex = PTHREAD_MUTEX_INITIALIZER;
+static volatile int g_nRunIds = 0;             // the number of the last prover instance
+static volatile int g_fAbstractionProved = 0;  // set to 1 when prover successed to prove
 
+// call back procedure for PDR
+int Abs_CallBackToStop( int RunId ) { assert( RunId <= g_nRunIds ); return RunId < g_nRunIds; }
 
+// test procedure to replace PDR
 int Pdr_ManSolve_test( Aig_Man_t * pAig, Pdr_Par_t * pPars, Abc_Cex_t ** ppCex )
 {
     char * p = ABC_ALLOC( char, 111 );
@@ -90,16 +78,30 @@ int Pdr_ManSolve_test( Aig_Man_t * pAig, Pdr_Par_t * pPars, Abc_Cex_t ** ppCex )
     return -1;
 }
 
-static int g_fAbstractionProved = 0;
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Create one thread]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 void * Abs_ProverThread( void * pArg )
 {
-    Abs_Pair_t * pPair = (Abs_Pair_t *)pArg;
+    Abs_ThData_t * pThData = (Abs_ThData_t *)pArg;
     Pdr_Par_t Pars, * pPars = &Pars;
     Aig_Man_t * pAig, * pTemp;
-    int RetValue;
-    pAig = Ioa_ReadAiger( pPair->pFileName, 0 );
+    int RetValue, status;
+    pAig = Ioa_ReadAiger( pThData->pFileName, 0 );
     if ( pAig == NULL )
-        Abc_Print( 1, "\nCannot open file \"%s\".\n", pPair->pFileName );
+        Abc_Print( 1, "\nCannot open file \"%s\".\n", pThData->pFileName );
     else
     {
         // synthesize abstraction
@@ -108,28 +110,33 @@ void * Abs_ProverThread( void * pArg )
         // call PDR
         Pdr_ManSetDefaultParams( pPars );
         pPars->fSilent = 1;
-        pPars->RunId = pPair->RunId;
+        pPars->RunId = pThData->RunId;
         pPars->pFuncStop = Abs_CallBackToStop;
         RetValue = Pdr_ManSolve( pAig, pPars, NULL );
 //        RetValue = Pdr_ManSolve_test( pAig, pPars, NULL );
         // update the result
-        g_fAbstractionProved = (RetValue == 1);
+        if ( RetValue == 1 )
+        {
+            status = pthread_mutex_lock(&g_mutex);  assert( status == 0 );
+            g_fAbstractionProved = 1;
+            status = pthread_mutex_unlock(&g_mutex);  assert( status == 0 );
+        }
         // free memory
         Aig_ManStop( pAig );
         // quit this thread
-        if ( pPair->fVerbose )
+        if ( pThData->fVerbose )
         {
             if ( RetValue == 1 )
-                Abc_Print( 1, "\nProved abstraction %d.\n", pPair->RunId );
+                Abc_Print( 1, "\nProved abstraction %d.\n", pThData->RunId );
             else if ( RetValue == 0 )
-                Abc_Print( 1, "\nDisproved abstraction %d.\n", pPair->RunId );
+                Abc_Print( 1, "\nDisproved abstraction %d.\n", pThData->RunId );
             else if ( RetValue == -1 )
-                Abc_Print( 1, "\nCancelled abstraction %d.\n", pPair->RunId );
+                Abc_Print( 1, "\nCancelled abstraction %d.\n", pThData->RunId );
             else assert( 0 );
         }
     }
-    ABC_FREE( pPair->pFileName );
-    ABC_FREE( pPair );
+    ABC_FREE( pThData->pFileName );
+    ABC_FREE( pThData );
     // quit this thread
     pthread_exit( NULL );
     assert(0);
@@ -137,38 +144,48 @@ void * Abs_ProverThread( void * pArg )
 }
 void Gia_Ga2ProveAbsracted( char * pFileName, int fVerbose )
 {
-    Abs_Pair_t * pPair;
+    Abs_ThData_t * pThData;
     pthread_t ProverThread;
-    int RetValue;
+    int status;
     assert( pFileName != NULL );
-    g_fAbstractionProved = 0;
     // disable verbosity
     fVerbose = 0;
+    // reset the proof 
+    status = pthread_mutex_lock(&g_mutex);  assert( status == 0 );
+    g_fAbstractionProved = 0;
+    status = pthread_mutex_unlock(&g_mutex);  assert( status == 0 );
+    // collect thread data
+    pThData = ABC_CALLOC( Abs_ThData_t, 1 );
+    pThData->pFileName = Abc_UtilStrsav( (void *)pFileName );
+    pThData->fVerbose = fVerbose;
+    status = pthread_mutex_lock(&g_mutex);  assert( status == 0 );
+    pThData->RunId = ++g_nRunIds;
+    status = pthread_mutex_unlock(&g_mutex);  assert( status == 0 );
     // create thread
-    pPair = ABC_CALLOC( Abs_Pair_t, 1 );
-    pPair->pFileName = Abc_UtilStrsav( (void *)pFileName );
-    pPair->fVerbose = fVerbose;
-    pPair->RunId = ++g_nRunIds;
-    if ( fVerbose )  Abc_Print( 1, "\nTrying to prove abstraction %d.\n", pPair->RunId );
-    RetValue = pthread_create( &ProverThread, NULL, Abs_ProverThread, pPair );
-    assert( RetValue == 0 );
+    if ( fVerbose )  Abc_Print( 1, "\nTrying to prove abstraction %d.\n", pThData->RunId );
+    status = pthread_create( &ProverThread, NULL, Abs_ProverThread, pThData );
+    assert( status == 0 );
 }
 void Gia_Ga2ProveCancel( int fVerbose )
 {
+    int status;
+    status = pthread_mutex_lock(&g_mutex);  assert( status == 0 );
     g_nRunIds++;
-}
-void Gia_Ga2ProveFinish( int fVerbose )
-{
-    g_fAbstractionProved = 0;
+    status = pthread_mutex_unlock(&g_mutex);  assert( status == 0 );
 }
 int Gia_Ga2ProveCheck( int fVerbose )
 {
-    return g_fAbstractionProved;
+    int status;
+    if ( g_fAbstractionProved == 0 )
+        return 0;
+    status = pthread_mutex_lock(&g_mutex);  assert( status == 0 );
+    g_fAbstractionProved = 0;
+    status = pthread_mutex_unlock(&g_mutex);  assert( status == 0 );
+    return 1;
 }
 
 #endif
 
-
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////

src/aig/ioa/ioaReadAig.c

@@ -447,8 +447,9 @@ Aig_Man_t * Ioa_ReadAiger( char * pFileName, int fCheck )
     if ( pNew )
     {
         pName = Ioa_FileNameGeneric( pFileName );
+        ABC_FREE( pNew->pName );
         pNew->pName = Abc_UtilStrsav( pName );
-//        pNew->pSpec = Ioa_UtilStrsav( pFileName );
+        pNew->pSpec = Abc_UtilStrsav( pFileName );
         ABC_FREE( pName );
     }
     return pNew;

src/base/abci/abc.c

@@ -871,22 +871,11 @@ void Abc_End( Abc_Frame_t * pAbc )
 {
     extern Abc_Frame_t * Abc_FrameGetGlobalFrame();
     Abc_FrameClearDesign(); 
-
-    {
-//        extern void Au_TabManPrint();
-//        Au_TabManPrint();
-    }
-
-//    Dar_LibDumpPriorities();
+    Cnf_ManFree();
     {
         extern int Abc_NtkCompareAndSaveBest( Abc_Ntk_t * pNtk );
         Abc_NtkCompareAndSaveBest( NULL );
     }
-
-    {
-//        extern void Cnf_ClearMemory();
-        Cnf_ClearMemory();
-    }
     {
         extern void Dar_LibStop();
         Dar_LibStop();

src/base/abci/abcDar.c

@@ -1386,7 +1386,7 @@ Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName, int fFastAlgo,
     // write CNF into a file
     Cnf_DataWriteIntoFile( pCnf, pFileName, 0 );
     Cnf_DataFree( pCnf );
-    Cnf_ClearMemory();
+    Cnf_ManFree();
     Aig_ManStop( pMan );
     return pNtkNew;
 }

src/base/main/mainMC.c

@@ -101,7 +101,7 @@ int main( int argc, char * argv[] )
         {
             extern void Dar_LibStart();
             extern void Dar_LibStop();
-            extern void Cnf_ClearMemory();
+            extern void Cnf_ManFree();
 
             Fra_SecSetDefaultParams( pSecPar );
             pSecPar->TimeLimit       = 600;
@@ -112,7 +112,7 @@ int main( int argc, char * argv[] )
             Dar_LibStart();
             RetValue = Fra_FraigSec( pAig, pSecPar, NULL );
             Dar_LibStop();
-            Cnf_ClearMemory();
+            Cnf_ManFree();
         }
     }
 

src/proof/pdr/pdrCnf.c

@@ -270,7 +270,7 @@ static inline sat_solver * Pdr_ManNewSolver1( sat_solver * pSat, Pdr_Man_t * p,
     {
         int nRegs = p->pAig->nRegs;
         p->pAig->nRegs = Aig_ManCoNum(p->pAig);
-        p->pCnf1 = Cnf_Derive( p->pAig, Aig_ManCoNum(p->pAig) );
+        p->pCnf1 = Cnf_DeriveWithMan( p->pCnfMan, p->pAig, Aig_ManCoNum(p->pAig) );
         p->pAig->nRegs = nRegs;
         assert( p->vVar2Reg == NULL );
         p->vVar2Reg = Vec_IntStartFull( p->pCnf1->nVars );
@@ -300,7 +300,7 @@ static inline sat_solver * Pdr_ManNewSolver2( sat_solver * pSat, Pdr_Man_t * p,
     assert( pSat );
     if ( p->pCnf2 == NULL )
     {
-        p->pCnf2     = Cnf_DeriveOther( p->pAig, 0 );
+        p->pCnf2     = Cnf_DeriveOtherWithMan( p->pCnfMan, p->pAig, 0 );
         p->pvId2Vars = ABC_CALLOC( Vec_Int_t *, Aig_ManObjNumMax(p->pAig) );
         p->vVar2Ids  = Vec_PtrAlloc( 256 );
     }

src/proof/pdr/pdrInt.h

@@ -68,6 +68,7 @@ struct Pdr_Man_t_
     Pdr_Par_t * pPars;     // parameters
     Aig_Man_t * pAig;      // user's AIG
     // static CNF representation
+    Cnf_Man_t * pCnfMan;   // CNF manager
     Cnf_Dat_t * pCnf1;     // CNF for this AIG
     Vec_Int_t * vVar2Reg;  // mapping of SAT var into registers
     // dynamic CNF representation

src/proof/pdr/pdrMan.c

@@ -67,6 +67,7 @@ Pdr_Man_t * Pdr_ManStart( Aig_Man_t * pAig, Pdr_Par_t * pPars, Vec_Int_t * vPrio
     p->vRes     = Vec_IntAlloc( 100 );  // final result
     p->vSuppLits= Vec_IntAlloc( 100 );  // support literals
     p->pCubeJust= Pdr_SetAlloc( Saig_ManRegNum(pAig) );
+    p->pCnfMan  = Cnf_ManStart();
     // additional AIG data-members
     if ( pAig->pFanData == NULL )
         Aig_ManFanoutStart( pAig );
@@ -127,6 +128,8 @@ void Pdr_ManStop( Pdr_Man_t * p )
         Vec_IntFreeP( &p->pvId2Vars[i] );
     ABC_FREE( p->pvId2Vars );
     Vec_VecFreeP( (Vec_Vec_t **)&p->vVar2Ids );
+    // CNF manager
+    Cnf_ManStop( p->pCnfMan );
     // internal use
     Vec_IntFreeP( &p->vPrio   );  // priority flops
     Vec_IntFree( p->vLits     );  // array of literals

src/sat/cnf/cnf.h

@@ -127,9 +127,12 @@ static inline void         Cnf_ObjSetBestCut( Aig_Obj_t * pObj, Cnf_Cut_t * pCut
 /*=== cnfCore.c ========================================================*/
 extern Vec_Int_t *     Cnf_DeriveMappingArray( Aig_Man_t * pAig );
 extern Cnf_Dat_t *     Cnf_Derive( Aig_Man_t * pAig, int nOutputs );
+extern Cnf_Dat_t *     Cnf_DeriveWithMan( Cnf_Man_t * p, Aig_Man_t * pAig, int nOutputs );
 extern Cnf_Dat_t *     Cnf_DeriveOther( Aig_Man_t * pAig, int fSkipTtMin );
+extern Cnf_Dat_t *     Cnf_DeriveOtherWithMan( Cnf_Man_t * p, Aig_Man_t * pAig, int fSkipTtMin );
+extern void            Cnf_ManPrepare();
 extern Cnf_Man_t *     Cnf_ManRead();
-extern void            Cnf_ClearMemory();
+extern void            Cnf_ManFree();
 /*=== cnfCut.c ========================================================*/
 extern Cnf_Cut_t *     Cnf_CutCreate( Cnf_Man_t * p, Aig_Obj_t * pObj );
 extern void            Cnf_CutPrint( Cnf_Cut_t * pCut );

src/sat/cnf/cnfCore.c

@@ -32,6 +32,37 @@ static Cnf_Man_t * s_pManCnf = NULL;
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cnf_ManPrepare()
+{
+    if ( s_pManCnf == NULL )
+    {
+        printf( "\n\nCreating CNF manager!!!!!\n\n" );
+        s_pManCnf = Cnf_ManStart();
+    }
+}
+Cnf_Man_t * Cnf_ManRead()
+{
+    return s_pManCnf;
+}
+void Cnf_ManFree()
+{
+    if ( s_pManCnf == NULL )
+        return;
+    Cnf_ManStop( s_pManCnf );
+    s_pManCnf = NULL;
+}
+
 
 /**Function*************************************************************
 
@@ -52,10 +83,7 @@ Vec_Int_t * Cnf_DeriveMappingArray( Aig_Man_t * pAig )
     Aig_MmFixed_t * pMemCuts;
     clock_t clk;
     // allocate the CNF manager
-    if ( s_pManCnf == NULL )
-        s_pManCnf = Cnf_ManStart();
-    // connect the managers
-    p = s_pManCnf;
+    p = Cnf_ManStart();
     p->pManAig = pAig;
 
     // generate cuts for all nodes, assign cost, and find best cuts
@@ -83,6 +111,7 @@ p->timeSave = clock() - clk;
 //ABC_PRT( "Cuts   ", p->timeCuts );
 //ABC_PRT( "Map    ", p->timeMap  );
 //ABC_PRT( "Saving ", p->timeSave );
+    Cnf_ManStop( p );
     return vResult;
 }
  
@@ -97,18 +126,13 @@ p->timeSave = clock() - clk;
   SeeAlso     []
 
 ***********************************************************************/
-Cnf_Dat_t * Cnf_Derive( Aig_Man_t * pAig, int nOutputs )
+Cnf_Dat_t * Cnf_DeriveWithMan( Cnf_Man_t * p, Aig_Man_t * pAig, int nOutputs )
 {
-    Cnf_Man_t * p;
     Cnf_Dat_t * pCnf;
     Vec_Ptr_t * vMapped;
     Aig_MmFixed_t * pMemCuts;
     clock_t clk;
-    // allocate the CNF manager
-    if ( s_pManCnf == NULL )
-        s_pManCnf = Cnf_ManStart();
     // connect the managers
-    p = s_pManCnf;
     p->pManAig = pAig;
 
     // generate cuts for all nodes, assign cost, and find best cuts
@@ -138,6 +162,11 @@ p->timeSave = clock() - clk;
 //ABC_PRT( "Saving ", p->timeSave );
     return pCnf;
 }
+Cnf_Dat_t * Cnf_Derive( Aig_Man_t * pAig, int nOutputs )
+{
+    Cnf_ManPrepare();
+    return Cnf_DeriveWithMan( s_pManCnf, pAig, nOutputs );
+}
  
 /**Function*************************************************************
 
@@ -150,18 +179,13 @@ p->timeSave = clock() - clk;
   SeeAlso     []
 
 ***********************************************************************/
-Cnf_Dat_t * Cnf_DeriveOther( Aig_Man_t * pAig, int fSkipTtMin )
+Cnf_Dat_t * Cnf_DeriveOtherWithMan( Cnf_Man_t * p, Aig_Man_t * pAig, int fSkipTtMin )
 {
-    Cnf_Man_t * p;
     Cnf_Dat_t * pCnf;
     Vec_Ptr_t * vMapped;
     Aig_MmFixed_t * pMemCuts;
     clock_t clk;
-    // allocate the CNF manager
-    if ( s_pManCnf == NULL )
-        s_pManCnf = Cnf_ManStart();
     // connect the managers
-    p = s_pManCnf;
     p->pManAig = pAig;
 
     // generate cuts for all nodes, assign cost, and find best cuts
@@ -192,43 +216,12 @@ p->timeSave = clock() - clk;
 //ABC_PRT( "Saving ", p->timeSave );
     return pCnf;
 }
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Cnf_Man_t * Cnf_ManRead()
-{
-    return s_pManCnf;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Cnf_ClearMemory()
+Cnf_Dat_t * Cnf_DeriveOther( Aig_Man_t * pAig, int fSkipTtMin )
 {
-    if ( s_pManCnf == NULL )
-        return;
-    Cnf_ManStop( s_pManCnf );
-    s_pManCnf = NULL;
+    Cnf_ManPrepare();
+    return Cnf_DeriveOtherWithMan( s_pManCnf, pAig, fSkipTtMin );
 }
 
-
 #if 0
 
 /**Function*************************************************************