summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--abcexe.dsp4
-rw-r--r--src/aig/gia/giaAbsGla2.c37
-rw-r--r--src/aig/gia/giaAbsPth.c119
-rw-r--r--src/aig/ioa/ioaReadAig.c3
-rw-r--r--src/base/abci/abc.c13
-rw-r--r--src/base/abci/abcDar.c2
-rw-r--r--src/base/main/mainMC.c4
-rw-r--r--src/proof/pdr/pdrCnf.c4
-rw-r--r--src/proof/pdr/pdrInt.h1
-rw-r--r--src/proof/pdr/pdrMan.c3
-rw-r--r--src/sat/cnf/cnf.h5
-rw-r--r--src/sat/cnf/cnfCore.c93
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*************************************************************
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-17 17:31:12 +0000