From 117bc0dbcd4265eb04ed0c47979ec5953a983879 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 14 Sep 2012 21:20:37 -0700 Subject: Prepared &gla to try abstracting and proving concurrently. --- abcexe.dsp | 4 +- src/aig/gia/giaAbsGla2.c | 37 +++++++-------- src/aig/gia/giaAbsPth.c | 119 +++++++++++++++++++++++++++-------------------- src/aig/ioa/ioaReadAig.c | 3 +- src/base/abci/abc.c | 13 +----- src/base/abci/abcDar.c | 2 +- src/base/main/mainMC.c | 4 +- src/proof/pdr/pdrCnf.c | 4 +- src/proof/pdr/pdrInt.h | 1 + src/proof/pdr/pdrMan.c | 3 ++ src/sat/cnf/cnf.h | 5 +- src/sat/cnf/cnfCore.c | 93 +++++++++++++++++------------------- 12 files changed, 147 insertions(+), 141 deletions(-) diff --git a/abcexe.dsp b/abcexe.dsp index df1c4459..c8c4f8f8 100644 --- a/abcexe.dsp +++ b/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 diff --git a/src/aig/gia/giaAbsGla2.c b/src/aig/gia/giaAbsGla2.c index 24ea351a..432b4f70 100644 --- a/src/aig/gia/giaAbsGla2.c +++ b/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 ) diff --git a/src/aig/gia/giaAbsPth.c b/src/aig/gia/giaAbsPth.c index 12abf1d4..e0069132 100644 --- a/src/aig/gia/giaAbsPth.c +++ b/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 /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/ioa/ioaReadAig.c b/src/aig/ioa/ioaReadAig.c index 6c87f430..1d1dcbe2 100644 --- a/src/aig/ioa/ioaReadAig.c +++ b/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; diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index fe054071..1ecab451 100644 --- a/src/base/abci/abc.c +++ b/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(); diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c index 8278fa16..60911e59 100644 --- a/src/base/abci/abcDar.c +++ b/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; } diff --git a/src/base/main/mainMC.c b/src/base/main/mainMC.c index 7fec111c..43d3ea85 100644 --- a/src/base/main/mainMC.c +++ b/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(); } } diff --git a/src/proof/pdr/pdrCnf.c b/src/proof/pdr/pdrCnf.c index d9137592..0f993e67 100644 --- a/src/proof/pdr/pdrCnf.c +++ b/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 ); } diff --git a/src/proof/pdr/pdrInt.h b/src/proof/pdr/pdrInt.h index f24cb81d..36cea069 100644 --- a/src/proof/pdr/pdrInt.h +++ b/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 diff --git a/src/proof/pdr/pdrMan.c b/src/proof/pdr/pdrMan.c index 36d577dd..41941a37 100644 --- a/src/proof/pdr/pdrMan.c +++ b/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 diff --git a/src/sat/cnf/cnf.h b/src/sat/cnf/cnf.h index 1119db3e..f4c96709 100644 --- a/src/sat/cnf/cnf.h +++ b/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 ); diff --git a/src/sat/cnf/cnfCore.c b/src/sat/cnf/cnfCore.c index f08ea6d1..b32d0c7a 100644 --- a/src/sat/cnf/cnfCore.c +++ b/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************************************************************* -- cgit v1.2.3