summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/aig/gia/giaKf.c12
-rw-r--r--src/base/abci/abc.c56
-rw-r--r--src/base/cmd/cmdStarter.c2
-rw-r--r--src/base/wlc/wlcReadVer.c2
-rw-r--r--src/map/if/if.h2
-rw-r--r--src/map/if/ifDsd.c222
-rw-r--r--src/map/if/ifTest.c12
-rw-r--r--src/map/if/ifTune.c74
-rw-r--r--src/proof/abs/absPth.c2
-rw-r--r--src/proof/cec/cecSplit.c12
10 files changed, 331 insertions, 65 deletions
diff --git a/src/aig/gia/giaKf.c b/src/aig/gia/giaKf.c
index 083bf95c..caa88bfc 100644
--- a/src/aig/gia/giaKf.c
+++ b/src/aig/gia/giaKf.c
@@ -21,7 +21,7 @@
#include "gia.h"
#include "misc/vec/vecSet.h"
-//#ifdef ABC_USE_PTHREADS
+#ifdef ABC_USE_PTHREADS
#ifdef _WIN32
#include "../lib/pthread.h"
@@ -30,7 +30,7 @@
#include <unistd.h>
#endif
-//#endif
+#endif
ABC_NAMESPACE_IMPL_START
@@ -38,6 +38,13 @@ ABC_NAMESPACE_IMPL_START
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
+#ifndef ABC_USE_PTHREADS
+
+void Kf_ManSetDefaultPars( Jf_Par_t * pPars ) {}
+Gia_Man_t * Kf_ManPerformMapping( Gia_Man_t * pGia, Jf_Par_t * pPars ) { return NULL; }
+
+#else // pthreads are used
+
#define KF_LEAF_MAX 16
#define KF_CUT_MAX 32
#define KF_PROC_MAX 32
@@ -1328,6 +1335,7 @@ Gia_Man_t * Kf_ManPerformMapping( Gia_Man_t * pGia, Jf_Par_t * pPars )
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
+#endif // pthreads are used
ABC_NAMESPACE_IMPL_END
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 091b3b88..c39eea0a 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -15489,7 +15489,14 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
}
if ( p == NULL )
+ {
+ if ( LutSize > DAU_MAX_VAR || pPars->nLutSize > DAU_MAX_VAR )
+ {
+ printf( "Size of required DSD manager (%d) exceeds the precompiled limit (%d) (change parameter DAU_MAX_VAR).\n", LutSize, DAU_MAX_VAR );
+ return 0;
+ }
Abc_FrameSetManDsd( If_DsdManAlloc(pPars->nLutSize, LutSize) );
+ }
}
if ( pPars->fUserRecLib )
@@ -15913,7 +15920,7 @@ int Abc_CommandDsdFree( Abc_Frame_t * pAbc, int argc, char ** argv )
{
if ( !Abc_FrameReadManDsd2() )
{
- Abc_Print( 1, "The DSD manager is not started.\n" );
+ Abc_Print( -1, "The DSD manager is not started.\n" );
return 0;
}
Abc_FrameSetManDsd2( NULL );
@@ -15922,7 +15929,7 @@ int Abc_CommandDsdFree( Abc_Frame_t * pAbc, int argc, char ** argv )
{
if ( !Abc_FrameReadManDsd() )
{
- Abc_Print( 1, "The DSD manager is not started.\n" );
+ Abc_Print( -1, "The DSD manager is not started.\n" );
return 0;
}
Abc_FrameSetManDsd( NULL );
@@ -16000,7 +16007,7 @@ int Abc_CommandDsdPs( Abc_Frame_t * pAbc, int argc, char ** argv )
{
if ( !Abc_FrameReadManDsd2() )
{
- Abc_Print( 1, "The DSD manager is not started.\n" );
+ Abc_Print( -1, "The DSD manager is not started.\n" );
return 0;
}
If_DsdManPrint( (If_DsdMan_t *)Abc_FrameReadManDsd2(), NULL, Number, Support, fOccurs, fTtDump, fVerbose );
@@ -16009,7 +16016,7 @@ int Abc_CommandDsdPs( Abc_Frame_t * pAbc, int argc, char ** argv )
{
if ( !Abc_FrameReadManDsd() )
{
- Abc_Print( 1, "The DSD manager is not started.\n" );
+ Abc_Print( -1, "The DSD manager is not started.\n" );
return 0;
}
If_DsdManPrint( (If_DsdMan_t *)Abc_FrameReadManDsd(), NULL, Number, Support, fOccurs, fTtDump, fVerbose );
@@ -16043,10 +16050,10 @@ usage:
int Abc_CommandDsdTune( Abc_Frame_t * pAbc, int argc, char ** argv )
{
char * pStruct = NULL;
- int c, fVerbose = 0, fFast = 0, fAdd = 0, fSpec = 0, LutSize = 0, nConfls = 10000;
+ int c, fVerbose = 0, fFast = 0, fAdd = 0, fSpec = 0, LutSize = 0, nConfls = 10000, nProcs = 1;
If_DsdMan_t * pDsdMan = (If_DsdMan_t *)Abc_FrameReadManDsd();
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "KCSfasvh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "KCPSfasvh" ) ) != EOF )
{
switch ( c )
{
@@ -16070,6 +16077,15 @@ int Abc_CommandDsdTune( Abc_Frame_t * pAbc, int argc, char ** argv )
nConfls = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
break;
+ case 'P':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-P\" should be followed by a floating point number.\n" );
+ goto usage;
+ }
+ nProcs = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ break;
case 'S':
if ( globalUtilOptind >= argc )
{
@@ -16099,20 +16115,21 @@ int Abc_CommandDsdTune( Abc_Frame_t * pAbc, int argc, char ** argv )
}
if ( !Abc_FrameReadManDsd() )
{
- Abc_Print( 1, "The DSD manager is not started.\n" );
+ Abc_Print( -1, "The DSD manager is not started.\n" );
return 0;
}
if ( pStruct )
- Id_DsdManTuneStr( pDsdMan, pStruct, nConfls, fVerbose );
+ Id_DsdManTuneStr( pDsdMan, pStruct, nConfls, nProcs, fVerbose );
else
If_DsdManTune( pDsdMan, LutSize, fFast, fAdd, fSpec, fVerbose );
return 0;
usage:
- Abc_Print( -2, "usage: dsd_tune [-KC num] [-fasvh] [-S str]\n" );
+ Abc_Print( -2, "usage: dsd_tune [-KCP num] [-fasvh] [-S str]\n" );
Abc_Print( -2, "\t tunes DSD manager for the given LUT size\n" );
Abc_Print( -2, "\t-K num : LUT size used for tuning [default = %d]\n", LutSize );
Abc_Print( -2, "\t-C num : the maximum number of conflicts [default = %d]\n", nConfls );
+ Abc_Print( -2, "\t-P num : the maximum number of processes [default = %d]\n", nProcs );
Abc_Print( -2, "\t-f : toggles using fast check [default = %s]\n", fFast? "yes": "no" );
Abc_Print( -2, "\t-a : toggles adding tuning to the current one [default = %s]\n", fAdd? "yes": "no" );
Abc_Print( -2, "\t-s : toggles using specialized check [default = %s]\n", fSpec? "yes": "no" );
@@ -16153,7 +16170,7 @@ int Abc_CommandDsdMerge( Abc_Frame_t * pAbc, int argc, char ** argv )
}
if ( !Abc_FrameReadManDsd() )
{
- Abc_Print( 1, "The DSD manager is not started.\n" );
+ Abc_Print( -1, "The DSD manager is not started.\n" );
return 0;
}
pArgvNew = argv + globalUtilOptind;
@@ -16223,7 +16240,7 @@ int Abc_CommandDsdClean( Abc_Frame_t * pAbc, int argc, char ** argv )
}
if ( !Abc_FrameReadManDsd() )
{
- Abc_Print( 1, "The DSD manager is not started.\n" );
+ Abc_Print( -1, "The DSD manager is not started.\n" );
return 0;
}
If_DsdManClean( (If_DsdMan_t *)Abc_FrameReadManDsd(), fVerbose );
@@ -30804,6 +30821,16 @@ int Abc_CommandAbc9Dsdb( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Abc_CommandAbc9Dsdb(): There is no AIG.\n" );
return 1;
}
+ if ( nLutSize > DAU_MAX_VAR )
+ {
+ printf( "Abc_CommandAbc9Dsdb(): Size of the required DSD manager (%d) exceeds the precompiled limit (%d) (change parameter DAU_MAX_VAR).\n", nLutSize, DAU_MAX_VAR );
+ return 0;
+ }
+ if ( Abc_FrameReadManDsd2() && nLutSize > If_DsdManVarNum(Abc_FrameReadManDsd2()) )
+ {
+ printf( "Abc_CommandAbc9Dsdb(): Incompatible size of the DSD manager (run \"dsd_free -b\").\n" );
+ return 0;
+ }
if ( nLevelMax || nTimeWindow )
pTemp = Gia_ManPerformDsdBalanceWin( pAbc->pGia, nLevelMax, nTimeWindow, nLutSize, nCutNum, nRelaxRatio, fVerbose );
else
@@ -31329,7 +31356,14 @@ int Abc_CommandAbc9If( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
}
if ( p == NULL )
+ {
+ if ( LutSize > DAU_MAX_VAR || pPars->nLutSize > DAU_MAX_VAR )
+ {
+ printf( "Size of required DSD manager (%d) exceeds the precompiled limit (%d) (change parameter DAU_MAX_VAR).\n", LutSize, DAU_MAX_VAR );
+ return 0;
+ }
Abc_FrameSetManDsd( If_DsdManAlloc(pPars->nLutSize, LutSize) );
+ }
}
if ( pPars->fUserRecLib )
diff --git a/src/base/cmd/cmdStarter.c b/src/base/cmd/cmdStarter.c
index 16810baa..47cdd9ed 100644
--- a/src/base/cmd/cmdStarter.c
+++ b/src/base/cmd/cmdStarter.c
@@ -248,7 +248,7 @@ void Cmd_RunStarter( char * pFileName, char * pBinary, char * pCommand, int nCor
fflush( stdout );
}
-#endif
+#endif // pthreads are used
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
diff --git a/src/base/wlc/wlcReadVer.c b/src/base/wlc/wlcReadVer.c
index 34197e1b..32375ac0 100644
--- a/src/base/wlc/wlcReadVer.c
+++ b/src/base/wlc/wlcReadVer.c
@@ -134,7 +134,7 @@ int Wlc_PrsWriteErrorMessage( Wlc_Prs_t * p, char * pCur, const char * format, .
break;
sprintf( p->sError, "%s (line %d): %s\n", p->pFileName, iLine+1, pMessage );
}
- free( pMessage );
+ ABC_FREE( pMessage );
return 0;
}
void Wlc_PrsPrintErrorMessage( Wlc_Prs_t * p )
diff --git a/src/map/if/if.h b/src/map/if/if.h
index 0f217d20..1d5dec16 100644
--- a/src/map/if/if.h
+++ b/src/map/if/if.h
@@ -539,7 +539,7 @@ extern If_DsdMan_t * If_DsdManAlloc( int nVars, int nLutSize );
extern void If_DsdManAllocIsops( If_DsdMan_t * p, int nLutSize );
extern void If_DsdManPrint( If_DsdMan_t * p, char * pFileName, int Number, int Support, int fOccurs, int fTtDump, int fVerbose );
extern void If_DsdManTune( If_DsdMan_t * p, int LutSize, int fFast, int fAdd, int fSpec, int fVerbose );
-extern void Id_DsdManTuneStr( If_DsdMan_t * p, char * pStruct, int nConfls, int fVerbose );
+extern void Id_DsdManTuneStr( If_DsdMan_t * p, char * pStruct, int nConfls, int nProcs, int fVerbose );
extern void If_DsdManFree( If_DsdMan_t * p, int fVerbose );
extern void If_DsdManSave( If_DsdMan_t * p, char * pFileName );
extern If_DsdMan_t * If_DsdManLoad( char * pFileName );
diff --git a/src/map/if/ifDsd.c b/src/map/if/ifDsd.c
index d6d0f801..a8224d63 100644
--- a/src/map/if/ifDsd.c
+++ b/src/map/if/ifDsd.c
@@ -26,6 +26,17 @@
#include "aig/gia/gia.h"
#include "bool/kit/kit.h"
+#ifdef ABC_USE_PTHREADS
+
+#ifdef _WIN32
+#include "../lib/pthread.h"
+#else
+#include <pthread.h>
+#include <unistd.h>
+#endif
+
+#endif
+
ABC_NAMESPACE_IMPL_START
@@ -206,6 +217,7 @@ If_DsdMan_t * If_DsdManAlloc( int nVars, int LutSize )
{
If_DsdMan_t * p; int v;
char pFileName[10];
+ assert( nVars <= DAU_MAX_VAR );
sprintf( pFileName, "%02d.dsd", nVars );
p = ABC_CALLOC( If_DsdMan_t, 1 );
p->pStore = Abc_UtilStrsav( pFileName );
@@ -1213,10 +1225,9 @@ void If_DsdManComputeTruth_rec( If_DsdMan_t * p, int iDsd, word * pRes, unsigned
assert( 0 );
}
-word * If_DsdManComputeTruth( If_DsdMan_t * p, int iDsd, unsigned char * pPermLits )
+void If_DsdManComputeTruthPtr( If_DsdMan_t * p, int iDsd, unsigned char * pPermLits, word * pRes )
{
int nSupp = 0;
- word * pRes = p->pTtElems[DAU_MAX_VAR];
If_DsdObj_t * pObj = If_DsdVecObj( &p->vObjs, Abc_Lit2Var(iDsd) );
if ( iDsd == 0 )
Abc_TtConst0( pRes, p->nWords );
@@ -1231,6 +1242,11 @@ word * If_DsdManComputeTruth( If_DsdMan_t * p, int iDsd, unsigned char * pPermLi
else
If_DsdManComputeTruth_rec( p, iDsd, pRes, pPermLits, &nSupp );
assert( nSupp == If_DsdVecLitSuppSize(&p->vObjs, iDsd) );
+}
+word * If_DsdManComputeTruth( If_DsdMan_t * p, int iDsd, unsigned char * pPermLits )
+{
+ word * pRes = p->pTtElems[DAU_MAX_VAR];
+ If_DsdManComputeTruthPtr( p, iDsd, pPermLits, pRes );
return pRes;
}
@@ -2259,6 +2275,7 @@ extern Ifn_Ntk_t * Ifn_NtkParse( char * pStr );
extern int Ifn_NtkMatch( Ifn_Ntk_t * p, word * pTruth, int nVars, int nConfls, int fVerbose, int fVeryVerbose );
extern void Ifn_NtkPrint( Ifn_Ntk_t * p );
extern int Ifn_NtkLutSizeMax( Ifn_Ntk_t * p );
+extern int Ifn_NtkInputNum( Ifn_Ntk_t * p );
/**Function*************************************************************
@@ -2271,7 +2288,7 @@ extern int Ifn_NtkLutSizeMax( Ifn_Ntk_t * p );
SeeAlso []
***********************************************************************/
-void Id_DsdManTuneStr( If_DsdMan_t * p, char * pStruct, int nConfls, int fVerbose )
+void Id_DsdManTuneStr1( If_DsdMan_t * p, char * pStruct, int nConfls, int fVerbose )
{
int fVeryVerbose = 0;
ProgressBar * pProgress = NULL;
@@ -2281,6 +2298,14 @@ void Id_DsdManTuneStr( If_DsdMan_t * p, char * pStruct, int nConfls, int fVerbos
abctime clk = Abc_Clock();
// parse the structure
Ifn_Ntk_t * pNtk = Ifn_NtkParse( pStruct );
+ if ( If_DsdManVarNum(p) > Ifn_NtkInputNum(pNtk) )
+ {
+ printf( "The support of DSD manager (%d) exceeds the support of the structure (%d).\n", If_DsdManVarNum(p), Ifn_NtkInputNum(pNtk) );
+ ABC_FREE( pNtk );
+ return;
+ }
+ if ( If_DsdManVarNum(p) < Ifn_NtkInputNum(pNtk) )
+ printf( "Warning: The support of DSD manager (%d) is less than the support of the structure (%d).\n", If_DsdManVarNum(p), Ifn_NtkInputNum(pNtk) );
LutSize = Ifn_NtkLutSizeMax(pNtk);
// print
if ( fVerbose )
@@ -2316,8 +2341,199 @@ void Id_DsdManTuneStr( If_DsdMan_t * p, char * pStruct, int nConfls, int fVerbos
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
if ( fVeryVerbose )
If_DsdManPrintDistrib( p );
+ ABC_FREE( pNtk );
+}
+
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+#ifndef ABC_USE_PTHREADS
+void Id_DsdManTuneStr( If_DsdMan_t * p, char * pStruct, int nConfls, int nProcs, int fVerbose )
+{
+ Id_DsdManTuneStr1( p, pStruct, nConfls, fVerbose );
+}
+#else // pthreads are used
+
+
+#define PAR_THR_MAX 100
+typedef struct Ifn_ThData_t_
+{
+ Ifn_Ntk_t * pNtk; // network
+ word pTruth[DAU_MAX_WORD];
+ int nVars; // support
+ int Id; // object
+ int nConfls; // conflicts
+ int Result; // result
+ int Status; // state
+ abctime clkUsed; // total runtime
+} Ifn_ThData_t;
+void * Ifn_WorkerThread( void * pArg )
+{
+ Ifn_ThData_t * pThData = (Ifn_ThData_t *)pArg;
+ volatile int * pPlace = &pThData->Status;
+ abctime clk;
+ while ( 1 )
+ {
+ while ( *pPlace == 0 );
+ assert( pThData->Status == 1 );
+ if ( pThData->Id == -1 )
+ {
+ pthread_exit( NULL );
+ assert( 0 );
+ return NULL;
+ }
+ clk = Abc_Clock();
+ pThData->Result = Ifn_NtkMatch( pThData->pNtk, pThData->pTruth, pThData->nVars, pThData->nConfls, 0, 0 );
+ pThData->clkUsed += Abc_Clock() - clk;
+ pThData->Status = 0;
+// printf( "Finished object %d\n", pThData->Id );
+ }
+ assert( 0 );
+ return NULL;
+}
+void Id_DsdManTuneStr( If_DsdMan_t * p, char * pStruct, int nConfls, int nProcs, int fVerbose )
+{
+ int fVeryVerbose = 0;
+ ProgressBar * pProgress = NULL;
+ int i, k, nVars, LutSize;
+ abctime clk = Abc_Clock();
+ Ifn_Ntk_t * pNtk;
+ If_DsdObj_t * pObj;
+ if ( nProcs == 1 )
+ {
+ Id_DsdManTuneStr1( p, pStruct, nConfls, fVerbose );
+ return;
+ }
+ if ( nProcs > PAR_THR_MAX )
+ {
+ printf( "The number of processes (%d) exceeds the precompiled limit (%d).\n", nProcs, PAR_THR_MAX );
+ return;
+ }
+ // parse the structure
+ pNtk = Ifn_NtkParse( pStruct );
+ if ( pNtk == NULL )
+ return;
+ if ( If_DsdManVarNum(p) > Ifn_NtkInputNum(pNtk) )
+ {
+ printf( "The support of DSD manager (%d) exceeds the support of the structure (%d).\n", If_DsdManVarNum(p), Ifn_NtkInputNum(pNtk) );
+ ABC_FREE( pNtk );
+ return;
+ }
+ if ( If_DsdManVarNum(p) < Ifn_NtkInputNum(pNtk) )
+ printf( "Warning: The support of DSD manager (%d) is less than the support of the structure (%d).\n", If_DsdManVarNum(p), Ifn_NtkInputNum(pNtk) );
+ // check the largest LUT
+ LutSize = Ifn_NtkLutSizeMax(pNtk);
+ if ( fVerbose )
+ {
+ printf( "Considering programmable cell: " );
+ Ifn_NtkPrint( pNtk );
+ printf( "Largest LUT size = %d.\n", LutSize );
+ }
+ ABC_FREE( pNtk );
+ // clean the attributes
+ If_DsdVecForEachObj( &p->vObjs, pObj, i )
+ pObj->fMark = 0;
+ pProgress = Extra_ProgressBarStart( stdout, Vec_PtrSize(&p->vObjs) );
+
+ // perform concurrent solving
+ {
+ pthread_t WorkerThread[PAR_THR_MAX];
+ Ifn_ThData_t ThData[PAR_THR_MAX];
+ abctime clk, clkUsed = 0;
+ int status, fRunning = 1, iCurrentObj = 0;
+ // start the threads
+ for ( i = 0; i < nProcs; i++ )
+ {
+ ThData[i].pNtk = Ifn_NtkParse( pStruct );
+ ThData[i].nVars = -1; // support
+ ThData[i].Id = -1; // object
+ ThData[i].nConfls = nConfls; // conflicts
+ ThData[i].Result = -1; // result
+ ThData[i].Status = 0; // state
+ ThData[i].clkUsed = 0; // total runtime
+ status = pthread_create( WorkerThread + i, NULL, Ifn_WorkerThread, (void *)(ThData + i) ); assert( status == 0 );
+ }
+ // run the threads
+ while ( fRunning || iCurrentObj < Vec_PtrSize(&p->vObjs) )
+ {
+ for ( i = 0; i < nProcs; i++ )
+ {
+ if ( ThData[i].Status )
+ continue;
+ assert( ThData[i].Status == 0 );
+ if ( ThData[i].Id >= 0 )
+ {
+ //printf( "Closing obj %d with Thread %d:\n", ThData[i].Id, i );
+ assert( ThData[i].Result == 0 || ThData[i].Result == 1 );
+ if ( ThData[i].Result == 1 )
+ If_DsdVecObjSetMark( &p->vObjs, ThData[i].Id );
+ ThData[i].Id = -1;
+ ThData[i].Result = -1;
+ }
+ for ( k = iCurrentObj; k < Vec_PtrSize(&p->vObjs); k++ )
+ {
+ if ( (k & 0x3FF) == 0 )
+ Extra_ProgressBarUpdate( pProgress, k, NULL );
+ pObj = If_DsdVecObj( &p->vObjs, k );
+ nVars = If_DsdObjSuppSize(pObj);
+ if ( nVars <= LutSize )
+ continue;
+ clk = Abc_Clock();
+ If_DsdManComputeTruthPtr( p, Abc_Var2Lit(k, 0), NULL, ThData[i].pTruth );
+ clkUsed += Abc_Clock() - clk;
+ ThData[i].nVars = nVars;
+ ThData[i].Id = k;
+ ThData[i].Result = -1;
+ ThData[i].Status = 1;
+ //printf( "Scheduling %d for Thread %d\n", ThData[i].Id, i );
+ iCurrentObj = k+1;
+ break;
+ }
+ }
+ fRunning = 0;
+ for ( i = 0; i < nProcs; i++ )
+ if ( ThData[i].Status == 1 || (ThData[i].Status == 0 && ThData[i].Id >= 0) )
+ fRunning = 1;
+ //printf( "fRunning %d\n", fRunning );
+ }
+ // stop the threads
+ for ( i = 0; i < nProcs; i++ )
+ {
+ assert( ThData[i].Status == 0 );
+ ThData[i].Id = -1;
+ ThData[i].Status = 1;
+ ABC_FREE( ThData[i].pNtk );
+ }
+ if ( fVerbose )
+ {
+ printf( "Main : " );
+ Abc_PrintTime( 1, "Time", clkUsed );
+ for ( i = 0; i < nProcs; i++ )
+ {
+ printf( "Thread %d : ", i );
+ Abc_PrintTime( 1, "Time", ThData[i].clkUsed );
+ }
+ }
+ }
+
+ Extra_ProgressBarStop( pProgress );
+ printf( "Finished matching %d functions. ", Vec_PtrSize(&p->vObjs) );
+ Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+ if ( fVeryVerbose )
+ If_DsdManPrintDistrib( p );
}
+#endif // pthreads are used
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/map/if/ifTest.c b/src/map/if/ifTest.c
index bbadaca2..fa9a6444 100644
--- a/src/map/if/ifTest.c
+++ b/src/map/if/ifTest.c
@@ -21,7 +21,7 @@
#include "if.h"
#include "aig/gia/gia.h"
-//#ifdef ABC_USE_PTHREADS
+#ifdef ABC_USE_PTHREADS
#ifdef _WIN32
#include "../lib/pthread.h"
@@ -30,7 +30,7 @@
#include <unistd.h>
#endif
-//#endif
+#endif
ABC_NAMESPACE_IMPL_START
@@ -38,6 +38,12 @@ ABC_NAMESPACE_IMPL_START
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
+#ifndef ABC_USE_PTHREADS
+
+// do nothing
+
+#else // pthreads are used
+
static inline word * Gia_ParTestObj( Gia_Man_t * p, int Id ) { return (word *)p->pData + Id * p->iData; }
static inline void Gia_ParTestAlloc( Gia_Man_t * p, int nWords ) { assert( !p->pData ); p->pData = (unsigned *)ABC_ALLOC(word, Gia_ManObjNum(p) * nWords); p->iData = nWords; }
static inline void Gia_ParTestFree( Gia_Man_t * p ) { ABC_FREE( p->pData ); p->iData = 0; }
@@ -339,6 +345,8 @@ void Gia_ParTest( Gia_Man_t * p, int nWords, int nProcs )
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
+#endif // pthreads are used
+
ABC_NAMESPACE_IMPL_END
diff --git a/src/map/if/ifTune.c b/src/map/if/ifTune.c
index 817b0a2e..7dc7f75f 100644
--- a/src/map/if/ifTune.c
+++ b/src/map/if/ifTune.c
@@ -166,6 +166,10 @@ int Ifn_NtkLutSizeMax( Ifn_Ntk_t * p )
LutSize = Abc_MaxInt( LutSize, (int)p->Nodes[i].nFanins );
return LutSize;
}
+int Ifn_NtkInputNum( Ifn_Ntk_t * p )
+{
+ return p->nInps;
+}
/**Function*************************************************************
@@ -240,18 +244,24 @@ int Ifn_ManStrCheck( char * pStr, int * pnInps, int * pnObjs )
*pnObjs = MaxDef;
return 1;
}
-Ifn_Ntk_t * Ifn_NtkParse( char * pStr )
+int Ifn_ErrorMessage( const char * format, ... )
+{
+ char * pMessage;
+ va_list args;
+ va_start( args, format );
+ pMessage = vnsprintf( format, args );
+ va_end( args );
+ printf( "%s", pMessage );
+ ABC_FREE( pMessage );
+ return 0;
+}
+int Ifn_NtkParseInt( char * pStr, Ifn_Ntk_t * p )
{
int i, k, n, f, nFans, iFan;
- static Ifn_Ntk_t P, * p = &P;
- memset( p, 0, sizeof(Ifn_Ntk_t) );
if ( !Ifn_ManStrCheck(pStr, &p->nInps, &p->nObjs) )
- return NULL;
+ return 0;
if ( p->nInps > IFN_INS )
- {
- printf( "The number of variables (%d) exceeds predefined limit (%d). Recompile with different value of IFN_INS.\n", p->nInps, IFN_INS );
- return NULL;
- }
+ return Ifn_ErrorMessage( "The number of variables (%d) exceeds predefined limit (%d). Recompile with different value of IFN_INS.\n", p->nInps, IFN_INS );
assert( p->nInps > 1 && p->nInps < p->nObjs && p->nInps <= IFN_INS && p->nObjs < 2*IFN_INS );
for ( i = p->nInps; i < p->nObjs; i++ )
{
@@ -260,10 +270,7 @@ Ifn_Ntk_t * Ifn_NtkParse( char * pStr )
if ( pStr[k] == 'a' + i && pStr[k+1] == '=' )
break;
if ( pStr[k] == 0 )
- {
- printf( "Cannot find definition of signal %c.\n", 'a' + i );
- return NULL;
- }
+ return Ifn_ErrorMessage( "Cannot find definition of signal %c.\n", 'a' + i );
if ( pStr[k+2] == '(' )
p->Nodes[i].Type = IF_DSD_AND, Next = ')';
else if ( pStr[k+2] == '[' )
@@ -273,32 +280,20 @@ Ifn_Ntk_t * Ifn_NtkParse( char * pStr )
else if ( pStr[k+2] == '{' )
p->Nodes[i].Type = IF_DSD_PRIME, Next = '}';
else
- {
- printf( "Cannot find openning operation symbol in the defition of of signal %c.\n", 'a' + i );
- return NULL;
- }
+ return Ifn_ErrorMessage( "Cannot find openning operation symbol in the defition of of signal %c.\n", 'a' + i );
for ( n = k + 3; pStr[n]; n++ )
if ( pStr[n] == Next )
break;
if ( pStr[n] == 0 )
- {
- printf( "Cannot find closing operation symbol in the defition of of signal %c.\n", 'a' + i );
- return NULL;
- }
+ return Ifn_ErrorMessage( "Cannot find closing operation symbol in the defition of of signal %c.\n", 'a' + i );
nFans = n - k - 3;
if ( nFans < 1 || nFans > 8 )
- {
- printf( "Cannot find matching operation symbol in the defition of of signal %c.\n", 'a' + i );
- return NULL;
- }
+ return Ifn_ErrorMessage( "Cannot find matching operation symbol in the defition of of signal %c.\n", 'a' + i );
for ( f = 0; f < nFans; f++ )
{
iFan = pStr[k + 3 + f] - 'a';
if ( iFan < 0 || iFan >= i )
- {
- printf( "Fanin number %d is signal %d is out of range.\n", f, 'a' + i );
- return NULL;
- }
+ return Ifn_ErrorMessage( "Fanin number %d is signal %d is out of range.\n", f, 'a' + i );
p->Nodes[i].Fanins[f] = iFan;
}
p->Nodes[i].nFanins = nFans;
@@ -316,19 +311,15 @@ Ifn_Ntk_t * Ifn_NtkParse( char * pStr )
}
// if ( p->nConstr )
// printf( "Total constraints = %d\n", p->nConstr );
-
-/*
- // constraints
- p->nConstr = 5;
- p->pConstr[0] = (0 << 16) | 1;
-
- p->pConstr[1] = (2 << 16) | 3;
- p->pConstr[2] = (3 << 16) | 4;
-
- p->pConstr[3] = (6 << 16) | 7;
- p->pConstr[4] = (7 << 16) | 8;
-*/
- return p;
+ return 1;
+}
+Ifn_Ntk_t * Ifn_NtkParse( char * pStr )
+{
+ Ifn_Ntk_t * p = ABC_CALLOC( Ifn_Ntk_t, 1 );
+ if ( Ifn_NtkParseInt( pStr, p ) )
+ return p;
+ ABC_FREE( p );
+ return NULL;
}
/**Function*************************************************************
@@ -805,6 +796,7 @@ void Ifn_NtkRead()
Dau_DsdPrintFromTruth( pTruth, nVars );
// get the given function
RetValue = Ifn_NtkMatch( p, pTruth, nVars, 0, 1, 1 );
+ ABC_FREE( p );
}
////////////////////////////////////////////////////////////////////////
diff --git a/src/proof/abs/absPth.c b/src/proof/abs/absPth.c
index bd3f2dcb..f04a20d1 100644
--- a/src/proof/abs/absPth.c
+++ b/src/proof/abs/absPth.c
@@ -194,7 +194,7 @@ int Gia_GlaProveCheck( int fVerbose )
return 1;
}
-#endif
+#endif // pthreads are used
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
diff --git a/src/proof/cec/cecSplit.c b/src/proof/cec/cecSplit.c
index e5e9a9a4..0984c234 100644
--- a/src/proof/cec/cecSplit.c
+++ b/src/proof/cec/cecSplit.c
@@ -26,7 +26,7 @@
#include "misc/util/utilTruth.h"
//#include "bdd/cudd/cuddInt.h"
-//#ifdef ABC_USE_PTHREADS
+#ifdef ABC_USE_PTHREADS
#ifdef _WIN32
#include "../lib/pthread.h"
@@ -35,7 +35,7 @@
#include <unistd.h>
#endif
-//#endif
+#endif
ABC_NAMESPACE_IMPL_START
@@ -44,6 +44,12 @@ ABC_NAMESPACE_IMPL_START
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
+#ifndef ABC_USE_PTHREADS
+
+int Cec_GiaSplitTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nIterMax, int LookAhead, int fVerbose, int fVeryVerbose ) { return -1; }
+
+#else // pthreads are used
+
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
@@ -822,6 +828,8 @@ void Cec_GiaPrintCofStats2( Gia_Man_t * p )
}
}
+#endif // pthreads are used
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
generated by cgit v1.2.3 (git 2.25.1) at 2024-08-10 21:47:32 +0000