luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Merge branch 'berkeley-abc:master' into fix-retime-segfault

This commit is contained in:
Philippe Sauter 2023-08-10 13:56:20 +02:00 committed by GitHub
parent 0f7d05d531 e387ddf849
commit 0fa51fd627
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
18 changed files with 1159 additions and 261 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
.gitignore vendored
View File

@ -6,6 +6,7 @@ ReleaseLib/
ReleaseExe/
ReleaseExt/
_/
_TEST/
lib/abc*
lib/m114*

1
src/aig/gia/giaDeep.c
View File

@ -120,6 +120,7 @@ Gia_Man_t * Gia_ManDeepSynOne( int nNoImpr, int TimeOut, int nAnds, int Seed, in
}
if ( nTimeToStop && Abc_Clock() > nTimeToStop )
{
if ( !Abc_FrameIsBatchMode() )
printf( "Runtime limit (%d sec) is reached after %d iterations.\n", TimeOut, i );
break;
}

52
src/aig/gia/giaSimBase.c
View File

@ -3689,6 +3689,58 @@ Vec_Str_t * Gia_ManComputeRange( Gia_Man_t * p )
return vOut;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_ManComparePrint( Gia_Man_t * p, Gia_Man_t * q )
{
Vec_Wrd_t * vSimsPi = Vec_WrdStartTruthTables( Gia_ManCiNum(p) );
Vec_Wrd_t * vSimsP = Gia_ManSimPatSimOut( p, vSimsPi, 0 );
Vec_Wrd_t * vSimsQ = Gia_ManSimPatSimOut( q, vSimsPi, 0 );
int i, k, nWords = Vec_WrdSize(vSimsPi) / Gia_ManCiNum(p), Count = 0;
Gia_Obj_t * pObjP, * pObjQ;
Gia_ManSetPhase( p );
Gia_ManSetPhase( q );
Gia_ManForEachObj( p, pObjP, i ) {
word * pSim = Vec_WrdEntryP( vSimsP, i * nWords );
if ( pSim[0] & 1 ) Abc_TtNot( pSim, nWords );
}
Gia_ManForEachObj( q, pObjQ, i ) {
word * pSim = Vec_WrdEntryP( vSimsQ, i * nWords );
if ( pSim[0] & 1 ) Abc_TtNot( pSim, nWords );
}
Gia_ManForEachAnd( q, pObjQ, i ) {
word * pSimQ = Vec_WrdEntryP( vSimsQ, i * nWords );
int fFirst = 1;
Gia_ManForEachObj( p, pObjP, k ) {
word * pSimP = Vec_WrdEntryP( vSimsP, k * nWords );
if ( !Abc_TtEqual(pSimQ, pSimP, nWords) )
continue;
if ( fFirst ) {
printf( "%5d :", i );
fFirst = 0;
Count++;
}
printf( " %5d(%d)", k, pObjQ->fPhase ^ pObjP->fPhase );
}
if ( !fFirst )
printf( "\n");
}
printf( "Found %d equivalent nodes.\n", Count );
Vec_WrdFree( vSimsP );
Vec_WrdFree( vSimsQ );
Vec_WrdFree( vSimsPi );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

185
src/aig/gia/giaStoch.c
View File

@ -22,6 +22,19 @@
#include "base/main/main.h"
#include "base/cmd/cmd.h"
#ifdef ABC_USE_PTHREADS
#ifdef _WIN32
#include "../lib/pthread.h"
#else
#include <pthread.h>
#include <unistd.h>
#endif
#endif
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
@ -32,6 +45,169 @@ ABC_NAMESPACE_IMPL_START
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Processing on a single core.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Gia_Man_t * Gia_StochProcessOne( Gia_Man_t * p, char * pScript, int Rand, int TimeSecs )
{
Gia_Man_t * pNew;
char FileName[100], Command[1000];
sprintf( FileName, "%06x.aig", Rand );
Gia_AigerWrite( p, FileName, 0, 0, 0 );
sprintf( Command, "./abc -q \"&read %s; %s; &write %s\"", FileName, pScript, FileName );
if ( system( (char *)Command ) )
{
fprintf( stderr, "The following command has returned non-zero exit status:\n" );
fprintf( stderr, "\"%s\"\n", (char *)Command );
fprintf( stderr, "Sorry for the inconvenience.\n" );
fflush( stdout );
unlink( FileName );
return Gia_ManDup(p);
}
pNew = Gia_AigerRead( FileName, 0, 0, 0 );
unlink( FileName );
if ( pNew && Gia_ManAndNum(pNew) < Gia_ManAndNum(p) )
return pNew;
Gia_ManStopP( &pNew );
return Gia_ManDup(p);
}
void Gia_StochProcessArray( Vec_Ptr_t * vGias, char * pScript, int TimeSecs, int fVerbose )
{
Gia_Man_t * pGia, * pNew; int i;
Vec_Int_t * vRands = Vec_IntAlloc( Vec_PtrSize(vGias) );
Abc_Random(1);
for ( i = 0; i < Vec_PtrSize(vGias); i++ )
Vec_IntPush( vRands, Abc_Random(0) % 0x1000000 );
Vec_PtrForEachEntry( Gia_Man_t *, vGias, pGia, i )
{
pNew = Gia_StochProcessOne( pGia, pScript, Vec_IntEntry(vRands, i), TimeSecs );
Gia_ManStop( pGia );
Vec_PtrWriteEntry( vGias, i, pNew );
}
Vec_IntFree( vRands );
}
/**Function*************************************************************
Synopsis [Processing on a many cores.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
#ifndef ABC_USE_PTHREADS
void Gia_StochProcess( Vec_Ptr_t * vGias, char * pScript, int nProcs, int TimeSecs, int fVerbose )
{
Gia_StochProcessArray( vGias, pScript, TimeSecs, fVerbose );
}
#else // pthreads are used
#define PAR_THR_MAX 100
typedef struct Gia_StochThData_t_
{
Vec_Ptr_t * vGias;
char * pScript;
int Index;
int Rand;
int nTimeOut;
int fWorking;
} Gia_StochThData_t;
void * Gia_StochWorkerThread( void * pArg )
{
Gia_StochThData_t * pThData = (Gia_StochThData_t *)pArg;
volatile int * pPlace = &pThData->fWorking;
Gia_Man_t * pGia, * pNew;
while ( 1 )
{
while ( *pPlace == 0 );
assert( pThData->fWorking );
if ( pThData->Index == -1 )
{
pthread_exit( NULL );
assert( 0 );
return NULL;
}
pGia = (Gia_Man_t *)Vec_PtrEntry( pThData->vGias, pThData->Index );
pNew = Gia_StochProcessOne( pGia, pThData->pScript, pThData->Rand, pThData->nTimeOut );
Gia_ManStop( pGia );
Vec_PtrWriteEntry( pThData->vGias, pThData->Index, pNew );
pThData->fWorking = 0;
}
assert( 0 );
return NULL;
}
void Gia_StochProcess( Vec_Ptr_t * vGias, char * pScript, int nProcs, int TimeSecs, int fVerbose )
{
Gia_StochThData_t ThData[PAR_THR_MAX];
pthread_t WorkerThread[PAR_THR_MAX];
int i, k, status;
if ( fVerbose )
printf( "Running concurrent synthesis with %d processes.\n", nProcs );
fflush( stdout );
if ( nProcs < 2 )
return Gia_StochProcessArray( vGias, pScript, TimeSecs, fVerbose );
// subtract manager thread
nProcs--;
assert( nProcs >= 1 && nProcs <= PAR_THR_MAX );
// start threads
Abc_Random(1);
for ( i = 0; i < nProcs; i++ )
{
ThData[i].vGias = vGias;
ThData[i].pScript = pScript;
ThData[i].Index = -1;
ThData[i].Rand = Abc_Random(0) % 0x1000000;
ThData[i].nTimeOut = TimeSecs;
ThData[i].fWorking = 0;
status = pthread_create( WorkerThread + i, NULL, Gia_StochWorkerThread, (void *)(ThData + i) ); assert( status == 0 );
}
// look at the threads
for ( k = 0; k < Vec_PtrSize(vGias); k++ )
{
for ( i = 0; i < nProcs; i++ )
{
if ( ThData[i].fWorking )
continue;
ThData[i].Index = k;
ThData[i].fWorking = 1;
break;
}
if ( i == nProcs )
k--;
}
// wait till threads finish
for ( i = 0; i < nProcs; i++ )
if ( ThData[i].fWorking )
i = -1;
// stop threads
for ( i = 0; i < nProcs; i++ )
{
assert( !ThData[i].fWorking );
// stop
ThData[i].Index = -1;
ThData[i].fWorking = 1;
}
}
#endif // pthreads are used
/**Function*************************************************************
Synopsis []
@ -184,7 +360,7 @@ Gia_Man_t * Gia_ManDupDivideOne( Gia_Man_t * p, Vec_Int_t * vCis, Vec_Int_t * vA
pNew->vMapping = vMapping;
return pNew;
}
Vec_Ptr_t * Gia_ManDupDivide( Gia_Man_t * p, Vec_Wec_t * vCis, Vec_Wec_t * vAnds, Vec_Wec_t * vCos, char * pScript )
Vec_Ptr_t * Gia_ManDupDivide( Gia_Man_t * p, Vec_Wec_t * vCis, Vec_Wec_t * vAnds, Vec_Wec_t * vCos, char * pScript, int nProcs, int TimeOut )
{
Vec_Ptr_t * vAigs = Vec_PtrAlloc( Vec_WecSize(vCis) ); int i;
for ( i = 0; i < Vec_WecSize(vCis); i++ )
@ -192,7 +368,8 @@ Vec_Ptr_t * Gia_ManDupDivide( Gia_Man_t * p, Vec_Wec_t * vCis, Vec_Wec_t * vAnds
Gia_ManCollectNodes( p, Vec_WecEntry(vCis, i), Vec_WecEntry(vAnds, i), Vec_WecEntry(vCos, i) );
Vec_PtrPush( vAigs, Gia_ManDupDivideOne(p, Vec_WecEntry(vCis, i), Vec_WecEntry(vAnds, i), Vec_WecEntry(vCos, i)) );
}
Gia_ManStochSynthesis( vAigs, pScript );
//Gia_ManStochSynthesis( vAigs, pScript );
Gia_StochProcess( vAigs, pScript, nProcs, TimeOut, 0 );
return vAigs;
}
Gia_Man_t * Gia_ManDupStitch( Gia_Man_t * p, Vec_Wec_t * vCis, Vec_Wec_t * vAnds, Vec_Wec_t * vCos, Vec_Ptr_t * vAigs, int fHash )
@ -388,7 +565,7 @@ Vec_Wec_t * Gia_ManStochOutputs( Gia_Man_t * p, Vec_Wec_t * vAnds )
SeeAlso []
***********************************************************************/
void Gia_ManStochSyn( int nMaxSize, int nIters, int TimeOut, int Seed, int fVerbose, char * pScript )
void Gia_ManStochSyn( int nMaxSize, int nIters, int TimeOut, int Seed, int fVerbose, char * pScript, int nProcs )
{
abctime nTimeToStop = TimeOut ? Abc_Clock() + TimeOut * CLOCKS_PER_SEC : 0;
abctime clkStart = Abc_Clock();
@ -407,7 +584,7 @@ void Gia_ManStochSyn( int nMaxSize, int nIters, int TimeOut, int Seed, int fVerb
Vec_Wec_t * vAnds = Gia_ManStochNodes( pGia, nMaxSize, Abc_Random(0) & 0x7FFFFFFF );
Vec_Wec_t * vIns = Gia_ManStochInputs( pGia, vAnds );
Vec_Wec_t * vOuts = Gia_ManStochOutputs( pGia, vAnds );
Vec_Ptr_t * vAigs = Gia_ManDupDivide( pGia, vIns, vAnds, vOuts, pScript );
Vec_Ptr_t * vAigs = Gia_ManDupDivide( pGia, vIns, vAnds, vOuts, pScript, nProcs, TimeOut );
Gia_Man_t * pNew = Gia_ManDupStitchMap( pGia, vIns, vAnds, vOuts, vAigs );
int fMapped = Gia_ManHasMapping(pGia) && Gia_ManHasMapping(pNew);
Abc_FrameUpdateGia( Abc_FrameGetGlobalFrame(), pNew );

10
src/base/abc/abcAig.c
View File

@ -897,6 +897,16 @@ void Abc_AigReplace_int( Abc_Aig_t * pMan, Abc_Obj_t * pOld, Abc_Obj_t * pNew, i
{
if ( Abc_ObjIsCo(pFanout) )
{
pFanin1 = Abc_ObjRegular( pNew );
if ( pFanin1->fMarkB )
Abc_AigRemoveFromLevelStructureR( pMan->vLevelsR, pFanin1 );
if ( fUpdateLevel && pMan->pNtkAig->vLevelsR )
{
Abc_ObjSetReverseLevel( pFanin1, Abc_ObjReverseLevel(pOld) );
assert( pFanin1->fMarkB == 0 );
pFanin1->fMarkB = 1;
Vec_VecPush( pMan->vLevelsR, Abc_ObjReverseLevel(pFanin1), pFanin1 );
}
Abc_ObjPatchFanin( pFanout, pOld, pNew );
continue;
}

36
src/base/abc/abcFunc.c
View File

@ -1265,6 +1265,42 @@ int Abc_NtkToAig( Abc_Ntk_t * pNtk )
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_ObjFaninSort( Abc_Obj_t * pObj )
{
Vec_Int_t * vFanins = Abc_ObjFaninVec( pObj );
char * pCube, * pSop = (char*)pObj->pData;
int i, j, nVars = Abc_SopGetVarNum( pSop );
assert( nVars == Vec_IntSize(vFanins) );
for ( i = 0; i < Vec_IntSize(vFanins); i++ )
for ( j = i+1; j < Vec_IntSize(vFanins); j++ )
{
if ( Vec_IntEntry(vFanins, i) < Vec_IntEntry(vFanins, j) )
continue;
ABC_SWAP( int, Vec_IntArray(vFanins)[i], Vec_IntArray(vFanins)[j] );
for ( pCube = pSop; *pCube; pCube += nVars + 3 ) {
ABC_SWAP( char, pCube[i], pCube[j] );
}
}
}
void Abc_NtkFaninSort( Abc_Ntk_t * pNtk )
{
Abc_Obj_t * pObj; int i;
assert( Abc_NtkIsSopLogic(pNtk) );
Abc_NtkForEachNode( pNtk, pObj, i )
Abc_ObjFaninSort( pObj );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

215
src/base/abci/abc.c
View File

@ -540,6 +540,7 @@ static int Abc_CommandAbc9PoPart ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandAbc9GroupProve ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9MultiProve ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9SplitProve ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9SplitSat ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Bmc ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9SBmc ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9ChainBmc ( Abc_Frame_t * pAbc, int argc, char ** argv );
@ -1300,6 +1301,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "ABC9", "&gprove", Abc_CommandAbc9GroupProve, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&mprove", Abc_CommandAbc9MultiProve, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&splitprove", Abc_CommandAbc9SplitProve, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&splitsat", Abc_CommandAbc9SplitSat, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&bmc", Abc_CommandAbc9Bmc, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&bmcs", Abc_CommandAbc9SBmc, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&chainbmc", Abc_CommandAbc9ChainBmc, 0 );
@ -11017,6 +11019,7 @@ usage:
***********************************************************************/
int Abc_CommandSop( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern void Abc_NtkFaninSort( Abc_Ntk_t * pNtk );
Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
int c, fCubeSort = 1, fMode = -1, nCubeLimit = 1000000;
@ -11072,6 +11075,8 @@ int Abc_CommandSop( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Converting to SOP has failed.\n" );
return 0;
}
if ( !fCubeSort )
Abc_NtkFaninSort( pNtk );
return 0;
usage:
@ -13365,6 +13370,7 @@ int Abc_CommandGen( Abc_Frame_t * pAbc, int argc, char ** argv )
int fFpga;
int fOneHot;
int fRandom;
int fGraph;
int fVerbose;
char * FileName;
char Command[1000];
@ -13376,6 +13382,7 @@ int Abc_CommandGen( Abc_Frame_t * pAbc, int argc, char ** argv )
extern void Abc_GenFpga( char * pFileName, int nLutSize, int nLuts, int nVars );
extern void Abc_GenOneHot( char * pFileName, int nVars );
extern void Abc_GenRandom( char * pFileName, int nPis );
extern void Abc_GenGraph( char * pFileName, int nPis );
extern void Abc_GenAdderTree( char * pFileName, int nArgs, int nBits );
// set defaults
@ -13390,9 +13397,10 @@ int Abc_CommandGen( Abc_Frame_t * pAbc, int argc, char ** argv )
fFpga = 0;
fOneHot = 0;
fRandom = 0;
fGraph = 0;
fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "NAKLatsembfnrvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "NAKLatsembfnrgvh" ) ) != EOF )
{
switch ( c )
{
@ -13467,6 +13475,9 @@ int Abc_CommandGen( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'r':
fRandom ^= 1;
break;
case 'g':
fGraph ^= 1;
break;
case 'v':
fVerbose ^= 1;
break;
@ -13506,6 +13517,8 @@ int Abc_CommandGen( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_GenOneHot( FileName, nVars );
else if ( fRandom )
Abc_GenRandom( FileName, nVars );
else if ( fGraph )
Abc_GenGraph( FileName, nVars );
else if ( fAdderTree )
{
printf( "Generating adder tree with %d arguments and %d bits.\n", nArgs, nVars );
@ -13525,7 +13538,7 @@ int Abc_CommandGen( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
Abc_Print( -2, "usage: gen [-NAKL num] [-atsembfnrvh] <file>\n" );
Abc_Print( -2, "usage: gen [-NAKL num] [-atsembfnrgvh] <file>\n" );
Abc_Print( -2, "\t generates simple circuits\n" );
Abc_Print( -2, "\t-N num : the number of variables [default = %d]\n", nVars );
Abc_Print( -2, "\t-A num : the number of agruments (for adder tree) [default = %d]\n", nArgs );
@ -13538,6 +13551,7 @@ usage:
Abc_Print( -2, "\t-m : generate a multiplier [default = %s]\n", fMulti? "yes": "no" );
Abc_Print( -2, "\t-b : generate a signed Booth multiplier [default = %s]\n", fBooth? "yes": "no" );
Abc_Print( -2, "\t-f : generate a LUT FPGA structure [default = %s]\n", fFpga? "yes": "no" );
Abc_Print( -2, "\t-g : generate a graph structure [default = %s]\n", fGraph? "yes": "no" );
Abc_Print( -2, "\t-n : generate one-hotness conditions [default = %s]\n", fOneHot? "yes": "no" );
Abc_Print( -2, "\t-r : generate random single-output function [default = %s]\n", fRandom? "yes": "no" );
Abc_Print( -2, "\t-v : prints verbose information [default = %s]\n", fVerbose? "yes": "no" );
@ -45032,17 +45046,21 @@ usage:
int Abc_CommandAbc9Compare( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern void Gia_Iso4TestTwo( Gia_Man_t * pGia0, Gia_Man_t * pGia1 );
extern void Gia_ManComparePrint( Gia_Man_t * p, Gia_Man_t * q );
Gia_Man_t * pGia0, * pGia1;
char ** pArgvNew; int nArgcNew;
int c, fVerbose = 0;
int c, fFunc = 0, fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "fvh" ) ) != EOF )
{
switch ( c )
{
case 'f':
fFunc ^= 1;
break;
case 'v':
fVerbose ^= 1;
break;
break;
case 'h':
goto usage;
default:
@ -45063,14 +45081,18 @@ int Abc_CommandAbc9Compare( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Abc_CommandAbc9Compare(): Reading input files did not work.\n" );
return 1;
}
Gia_Iso4TestTwo( pGia0, pGia1 );
if ( fFunc )
Gia_ManComparePrint( pGia0, pGia1 );
else
Gia_Iso4TestTwo( pGia0, pGia1 );
Gia_ManStop( pGia0 );
Gia_ManStop( pGia1 );
return 0;
usage:
Abc_Print( -2, "usage: &compare <file1> <file2> [-vh]\n" );
Abc_Print( -2, "usage: &compare <file1> <file2> [-fvh]\n" );
Abc_Print( -2, "\t compared two AIGs for structural similarity\n" );
Abc_Print( -2, "\t-f : toggle functional comparison [default = %s]\n", fFunc? "yes": "no" );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
@ -46062,6 +46084,163 @@ usage:
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandAbc9SplitSat( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern void Cnf_SplitSat( char * pFileName, int iVarBeg, int iVarEnd, int nLits, int Value, int TimeOut, int nProcs, int nIters, int Seed, int fPrepro, int fVerbose );
int c, iVarBeg = 0, iVarEnd = ABC_INFINITY, nLits = 10, Value = 2, TimeOut = 5, nProcs = 1, nIters = 1, Seed = 0, fPrepro = 0, fVerbose = 0; char * pFileName = NULL;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "BENVTPISpvh" ) ) != EOF )
{
switch ( c )
{
case 'B':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-B\" should be followed by a positive integer.\n" );
goto usage;
}
iVarBeg = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( iVarBeg < 0 )
goto usage;
break;
case 'E':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-E\" should be followed by a positive integer.\n" );
goto usage;
}
iVarEnd = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( iVarEnd < 0 )
goto usage;
break;
case 'N':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-N\" should be followed by a positive integer.\n" );
goto usage;
}
nLits = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nLits < 0 )
goto usage;
break;
case 'V':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-V\" should be followed by a positive integer.\n" );
goto usage;
}
Value = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( Value < 0 || Value > 2 )
goto usage;
break;
case 'T':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-T\" should be followed by a positive integer.\n" );
goto usage;
}
TimeOut = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( TimeOut < 0 )
goto usage;
break;
case 'P':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-P\" should be followed by a positive integer.\n" );
goto usage;
}
nProcs = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nProcs <= 0 )
goto usage;
break;
case 'I':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-I\" should be followed by an integer.\n" );
goto usage;
}
nIters = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nIters < 0 )
goto usage;
break;
case 'S':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-S\" should be followed by an integer.\n" );
goto usage;
}
Seed = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( Seed < 0 )
goto usage;
break;
case 'p':
fPrepro ^= 1;
break;
case 'v':
fVerbose ^= 1;
break;
case 'h':
goto usage;
default:
goto usage;
}
}
// get the file name
if ( argc != globalUtilOptind + 1 )
{
Abc_Print( -1, "Abc_CommandAbc9SplitSat(): CNF file names should be given on the command line.\n" );
return 1;
}
{
FILE * pFile;
pFileName = argv[globalUtilOptind];
pFile = fopen( pFileName, "r" );
if ( pFile == NULL )
{
Abc_Print( -1, "Cannot open file \"%s\" with the input test patterns.\n", pFileName );
return 0;
}
fclose( pFile );
}
Cnf_SplitSat( pFileName, iVarBeg, iVarEnd, nLits, Value, TimeOut, nProcs, nIters, Seed, fPrepro, fVerbose );
return 0;
usage:
Abc_Print( -2, "usage: &splitsat [-BENVTPIS num] [-pvh]\n" );
Abc_Print( -2, "\t solves CNF-based SAT problem by randomized case-splitting\n" );
Abc_Print( -2, "\t-B num : the first CNF variable to use for splitting [default = %d]\n", iVarBeg );
Abc_Print( -2, "\t-E num : the last CNF variable to use for splitting [default = %d]\n", iVarEnd );
Abc_Print( -2, "\t-N num : the number of CNF variables to use for splitting [default = %d]\n", nLits );
Abc_Print( -2, "\t-V num : the variable values to use (0, 1, or 2 for \"any\") [default = %d]\n", Value );
Abc_Print( -2, "\t-T num : the runtime limit in seconds per subproblem [default = %d]\n", TimeOut );
Abc_Print( -2, "\t-P num : the number of concurrent processes [default = %d]\n", nProcs );
Abc_Print( -2, "\t-I num : the max number of iterations (0 = infinity) [default = %d]\n", nIters );
Abc_Print( -2, "\t-S num : the random seed used to generate cofactors [default = %d]\n", Seed );
Abc_Print( -2, "\t-p : toggle using SatELIte (http://minisat.se/SatELite.html) [default = %s]\n", fPrepro? "yes": "no" );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
}
/**Function*************************************************************
Synopsis []
@ -49418,10 +49597,10 @@ usage:
***********************************************************************/
int Abc_CommandAbc9StochSyn( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern void Gia_ManStochSyn( int nMaxSize, int nIters, int TimeOut, int Seed, int fVerbose, char * pScript );
int c, nMaxSize = 1000, nIters = 10, TimeOut = 0, Seed = 0, fVerbose = 0; char * pScript;
extern void Gia_ManStochSyn( int nMaxSize, int nIters, int TimeOut, int Seed, int fVerbose, char * pScript, int nProcs );
int c, nMaxSize = 1000, nIters = 10, TimeOut = 0, Seed = 0, nProcs = 1, fVerbose = 0; char * pScript;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "NITSvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "NITSPvh" ) ) != EOF )
{
switch ( c )
{
@ -49469,6 +49648,17 @@ int Abc_CommandAbc9StochSyn( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( Seed < 0 )
goto usage;
break;
case 'P':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-P\" should be followed by an integer.\n" );
goto usage;
}
nProcs = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nProcs < 0 )
goto usage;
break;
case 'v':
fVerbose ^= 1;
break;
@ -49489,17 +49679,18 @@ int Abc_CommandAbc9StochSyn( Abc_Frame_t * pAbc, int argc, char ** argv )
goto usage;
}
pScript = Abc_UtilStrsav( argv[globalUtilOptind] );
Gia_ManStochSyn( nMaxSize, nIters, TimeOut, Seed, fVerbose, pScript );
Gia_ManStochSyn( nMaxSize, nIters, TimeOut, Seed, fVerbose, pScript, nProcs );
ABC_FREE( pScript );
return 0;
usage:
Abc_Print( -2, "usage: &stochsyn [-NITS <num>] [-tvh] <script>\n" );
Abc_Print( -2, "usage: &stochsyn [-NITSP <num>] [-tvh] <script>\n" );
Abc_Print( -2, "\t performs stochastic synthesis\n" );
Abc_Print( -2, "\t-N <num> : the max partition size (in AIG nodes or LUTs) [default = %d]\n", nMaxSize );
Abc_Print( -2, "\t-I <num> : the number of iterations [default = %d]\n", nIters );
Abc_Print( -2, "\t-T <num> : the timeout in seconds (0 = no timeout) [default = %d]\n", TimeOut );
Abc_Print( -2, "\t-S <num> : user-specified random seed (0 <= num <= 100) [default = %d]\n", Seed );
Abc_Print( -2, "\t-P <num> : the number of concurrent processes (1 <= num <= 100) [default = %d]\n", nProcs );
Abc_Print( -2, "\t-v : toggle printing optimization summary [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
Abc_Print( -2, "\t<script> : synthesis script to use for each partition\n");

8
src/base/abci/abcDsd.c
View File

@ -175,11 +175,11 @@ void Abc_NtkDsdConstruct( Dsd_Manager_t * pManDsd, Abc_Ntk_t * pNtk, Abc_Ntk_t *
// save the CI nodes in the DSD nodes
Abc_AigConst1(pNtk)->pCopy = pNodeNew = Abc_NtkCreateNodeConst1(pNtkNew);
Dsd_NodeSetMark( Dsd_ManagerReadConst1(pManDsd), (int)(ABC_PTRINT_T)pNodeNew );
Dsd_NodeSetMark( Dsd_ManagerReadConst1(pManDsd), (word)(ABC_PTRINT_T)pNodeNew );
Abc_NtkForEachCi( pNtk, pNode, i )
{
pNodeDsd = Dsd_ManagerReadInput( pManDsd, i );
Dsd_NodeSetMark( pNodeDsd, (int)(ABC_PTRINT_T)pNode->pCopy );
Dsd_NodeSetMark( pNodeDsd, (word)(ABC_PTRINT_T)pNode->pCopy );
}
// collect DSD nodes in DFS order (leaves and const1 are not collected)
@ -298,7 +298,7 @@ printf( "\n" );
}
}
pNodeNew->pData = bLocal;
Dsd_NodeSetMark( pNodeDsd, (int)(ABC_PTRINT_T)pNodeNew );
Dsd_NodeSetMark( pNodeDsd, (word)(ABC_PTRINT_T)pNodeNew );
return pNodeNew;
}
@ -417,7 +417,7 @@ void Abc_NodeDecompDsdAndMux( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes, Dsd_Manager
Abc_ObjForEachFanin( pNode, pFanin, i )
{
pFaninDsd = Dsd_ManagerReadInput( pManDsd, i );
Dsd_NodeSetMark( pFaninDsd, (int)(ABC_PTRINT_T)pFanin );
Dsd_NodeSetMark( pFaninDsd, (word)(ABC_PTRINT_T)pFanin );
}
// construct the intermediate nodes

64
src/base/abci/abcGen.c
View File

@ -1140,6 +1140,70 @@ void Abc_GenBooth( char * pFileName, int nVars )
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_GenGraph( char * pFileName, int nPis )
{
FILE * pFile;
int i, a, b, w, nDigitsIn, nWords = Abc_TruthWordNum( nPis*(nPis-1)/2 );
unsigned * pTruth = ABC_CALLOC( unsigned, nWords );
unsigned char M[10][10] = {{0}}, C[100][2] = {{0}}, nVars = 0;
assert( nPis <= 8 );
for ( a = 0; a < nPis; a++ )
for ( b = a+1; b < nPis; b++ )
C[nVars][0] = a, C[nVars][1] = b, nVars++;
for ( i = 0; i < (1<<nVars); i++ )
{
int fChanges = 1;
for ( w = 0; w < nVars; w++ )
M[C[w][0]][C[w][1]] = M[C[w][1]][C[w][0]] = (i >> w) & 1;
while ( fChanges && !M[0][1] ) {
fChanges = 0;
for ( a = 0; a < nPis; a++ )
for ( b = 0; b < nPis; b++ )
if ( M[a][b] )
for ( w = 0; w < nPis; w++ )
if ( M[b][w] && !M[a][w] )
M[a][w] = 1, fChanges = 1;
}
if ( M[0][1] )
Abc_InfoSetBit(pTruth, i);
}
pFile = fopen( pFileName, "w" );
fprintf( pFile, "# Function with %d inputs generated by ABC on %s\n", nVars, Extra_TimeStamp() );
fprintf( pFile, ".model fun%d\n", nVars );
fprintf( pFile, ".inputs" );
nDigitsIn = Abc_Base10Log( nVars );
for ( i = 0; i < nVars; i++ )
fprintf( pFile, " i%0*d", nDigitsIn, i );
fprintf( pFile, "\n" );
fprintf( pFile, ".outputs f\n" );
fprintf( pFile, ".names" );
nDigitsIn = Abc_Base10Log( nVars );
for ( b = nVars-1; b >= 0; b-- )
fprintf( pFile, " i%0*d", nDigitsIn, b );
fprintf( pFile, " f\n" );
for ( i = 0; i < (1<<nVars); i++ )
if ( Abc_InfoHasBit(pTruth, i) )
{
for ( b = nVars-1; b >= 0; b-- )
fprintf( pFile, "%d", (i>>b)&1 );
fprintf( pFile, " 1\n" );
}
fprintf( pFile, ".end\n" );
fprintf( pFile, "\n" );
fclose( pFile );
ABC_FREE( pTruth );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///

4
src/bdd/dsd/dsd.h
View File

@ -92,8 +92,8 @@ extern DdNode * Dsd_NodeReadSupp( Dsd_Node_t * p );
extern Dsd_Node_t ** Dsd_NodeReadDecs( Dsd_Node_t * p );
extern Dsd_Node_t * Dsd_NodeReadDec ( Dsd_Node_t * p, int i );
extern int Dsd_NodeReadDecsNum( Dsd_Node_t * p );
extern int Dsd_NodeReadMark( Dsd_Node_t * p );
extern void Dsd_NodeSetMark( Dsd_Node_t * p, int Mark );
extern word Dsd_NodeReadMark( Dsd_Node_t * p );
extern void Dsd_NodeSetMark( Dsd_Node_t * p, word Mark );
extern DdManager * Dsd_ManagerReadDd( Dsd_Manager_t * pMan );
extern Dsd_Node_t * Dsd_ManagerReadRoot( Dsd_Manager_t * pMan, int i );
extern Dsd_Node_t * Dsd_ManagerReadInput( Dsd_Manager_t * pMan, int i );

4
src/bdd/dsd/dsdApi.c
View File

@ -56,7 +56,7 @@ DdNode * Dsd_NodeReadSupp( Dsd_Node_t * p ) { return p->S; }
Dsd_Node_t ** Dsd_NodeReadDecs( Dsd_Node_t * p ) { return p->pDecs; }
Dsd_Node_t * Dsd_NodeReadDec ( Dsd_Node_t * p, int i ) { return p->pDecs[i]; }
int Dsd_NodeReadDecsNum( Dsd_Node_t * p ) { return p->nDecs; }
int Dsd_NodeReadMark( Dsd_Node_t * p ) { return p->Mark; }
word Dsd_NodeReadMark( Dsd_Node_t * p ) { return p->Mark; }
/**Function*************************************************************
@ -74,7 +74,7 @@ int Dsd_NodeReadMark( Dsd_Node_t * p ) { return p->Mark; }
SeeAlso []
***********************************************************************/
void Dsd_NodeSetMark( Dsd_Node_t * p, int Mark ){ p->Mark = Mark; }
void Dsd_NodeSetMark( Dsd_Node_t * p, word Mark ){ p->Mark = Mark; }
/**Function*************************************************************

2
src/bdd/dsd/dsdInt.h
View File

@ -57,7 +57,7 @@ struct Dsd_Node_t_
DdNode * G; // function of the node
DdNode * S; // support of this function
Dsd_Node_t ** pDecs; // pointer to structures for formal inputs
int Mark; // the mark used by CASE 4 of disjoint decomposition
word Mark; // the mark used by CASE 4 of disjoint decomposition
short nDecs; // the number of formal inputs
short nVisits; // the counter of visits
};

22
src/misc/util/abc_global.h
View File

@ -325,8 +325,8 @@ static inline int Abc_Var2Lit4( int Var, int Att ) { assert(!(Att >>
static inline int Abc_Lit2Var4( int Lit ) { assert(Lit >= 0); return Lit >> 4; }
static inline int Abc_Lit2Att4( int Lit ) { assert(Lit >= 0); return Lit & 15; }
// time counting
typedef ABC_INT64_T abctime;
// counting wall time
static inline abctime Abc_Clock()
{
#if defined(__APPLE__) && defined(__MACH__)
@ -334,6 +334,25 @@ static inline abctime Abc_Clock()
#else
#define APPLE_MACH 0
#endif
#if (defined(LIN) || defined(LIN64)) && !APPLE_MACH && !defined(__MINGW32__)
struct timespec ts;
if ( clock_gettime(CLOCK_MONOTONIC, &ts) < 0 )
return (abctime)-1;
abctime res = ((abctime) ts.tv_sec) * CLOCKS_PER_SEC;
res += (((abctime) ts.tv_nsec) * CLOCKS_PER_SEC) / 1000000000;
return res;
#else
return (abctime) clock();
#endif
}
// counting thread time
static inline abctime Abc_ThreadClock()
{
#if defined(__APPLE__) && defined(__MACH__)
#define APPLE_MACH (__APPLE__ & __MACH__)
#else
#define APPLE_MACH 0
#endif
#if (defined(LIN) || defined(LIN64)) && !APPLE_MACH && !defined(__MINGW32__)
struct timespec ts;
if ( clock_gettime(CLOCK_THREAD_CPUTIME_ID, &ts) < 0 )
@ -346,7 +365,6 @@ static inline abctime Abc_Clock()
#endif
}
// misc printing procedures
enum Abc_VerbLevel
{

2
src/proof/cec/cecSplit.c
View File

@ -705,7 +705,7 @@ finish:
// wait till threads finish
for ( i = 0; i < nProcs; i++ )
if ( ThData[i].fWorking )
i = 0;
i = -1;
// stop threads
for ( i = 0; i < nProcs; i++ )
{

16
src/sat/bmc/bmcMaj.c
View File

@ -1637,22 +1637,6 @@ Vec_Int_t * Exa4_ManSolve( char * pFileNameIn, char * pFileNameOut, int TimeOut,
char * pKissat = "kissat";
#endif
char Command[1000], * pCommand = (char *)&Command;
{
FILE * pFile = fopen( pKissat, "rb" );
if ( pFile == NULL )
{
printf( "Cannot find the Kissat binary \"%s\".\n", pKissat );
pKissat = "./kissat";
pFile = fopen( pKissat, "rb" );
if ( pFile == NULL )
{
printf( "Cannot find the Kissat binary \"%s\".\n", pKissat );
return NULL;
}
fclose( pFile );
}
fclose( pFile );
}
if ( TimeOut )
sprintf( pCommand, "%s --time=%d %s %s > %s", pKissat, TimeOut, fVerboseSolver ? "": "-q", pFileNameIn, pFileNameOut );
else

2
src/sat/cnf/cnf.h
View File

@ -154,6 +154,8 @@ extern void Cnf_ManStop( Cnf_Man_t * p );
extern Vec_Int_t * Cnf_DataCollectPiSatNums( Cnf_Dat_t * pCnf, Aig_Man_t * p );
extern Cnf_Dat_t * Cnf_DataAlloc( Aig_Man_t * pAig, int nVars, int nClauses, int nLiterals );
extern Cnf_Dat_t * Cnf_DataDup( Cnf_Dat_t * p );
extern Cnf_Dat_t * Cnf_DataDupCof( Cnf_Dat_t * p, int Lit );
extern Cnf_Dat_t * Cnf_DataDupCofArray( Cnf_Dat_t * p, Vec_Int_t * vLits );
extern void Cnf_DataFree( Cnf_Dat_t * p );
extern void Cnf_DataLift( Cnf_Dat_t * p, int nVarsPlus );
extern void Cnf_DataCollectFlipLits( Cnf_Dat_t * p, int iFlipVar, Vec_Int_t * vFlips );

49
src/sat/cnf/cnfMan.c
View File

@ -103,10 +103,8 @@ void Cnf_ManStop( Cnf_Man_t * p )
***********************************************************************/
Vec_Int_t * Cnf_DataCollectPiSatNums( Cnf_Dat_t * pCnf, Aig_Man_t * p )
{
Vec_Int_t * vCiIds;
Aig_Obj_t * pObj;
int i;
vCiIds = Vec_IntAlloc( Aig_ManCiNum(p) );
Aig_Obj_t * pObj; int i;
Vec_Int_t * vCiIds = Vec_IntAlloc( Aig_ManCiNum(p) );
Aig_ManForEachCi( p, pObj, i )
Vec_IntPush( vCiIds, pCnf->pVarNums[pObj->Id] );
return vCiIds;
@ -126,9 +124,7 @@ Vec_Int_t * Cnf_DataCollectPiSatNums( Cnf_Dat_t * pCnf, Aig_Man_t * p )
Cnf_Dat_t * Cnf_DataAlloc( Aig_Man_t * pAig, int nVars, int nClauses, int nLiterals )
{
Cnf_Dat_t * pCnf;
int i;
pCnf = ABC_ALLOC( Cnf_Dat_t, 1 );
memset( pCnf, 0, sizeof(Cnf_Dat_t) );
pCnf = ABC_CALLOC( Cnf_Dat_t, 1 );
pCnf->pMan = pAig;
pCnf->nVars = nVars;
pCnf->nClauses = nClauses;
@ -136,10 +132,8 @@ Cnf_Dat_t * Cnf_DataAlloc( Aig_Man_t * pAig, int nVars, int nClauses, int nLiter
pCnf->pClauses = ABC_ALLOC( int *, nClauses + 1 );
pCnf->pClauses[0] = ABC_ALLOC( int, nLiterals );
pCnf->pClauses[nClauses] = pCnf->pClauses[0] + nLiterals;
pCnf->pVarNums = ABC_ALLOC( int, Aig_ManObjNumMax(pAig) );
// memset( pCnf->pVarNums, 0xff, sizeof(int) * Aig_ManObjNumMax(pAig) );
for ( i = 0; i < Aig_ManObjNumMax(pAig); i++ )
pCnf->pVarNums[i] = -1;
if ( pCnf->pVarNums )
pCnf->pVarNums = ABC_FALLOC( int, Aig_ManObjNumMax(pAig) );
return pCnf;
}
@ -160,11 +154,44 @@ Cnf_Dat_t * Cnf_DataDup( Cnf_Dat_t * p )
int i;
pCnf = Cnf_DataAlloc( p->pMan, p->nVars, p->nClauses, p->nLiterals );
memcpy( pCnf->pClauses[0], p->pClauses[0], sizeof(int) * p->nLiterals );
if ( p->pVarNums )
memcpy( pCnf->pVarNums, p->pVarNums, sizeof(int) * Aig_ManObjNumMax(p->pMan) );
for ( i = 1; i < p->nClauses; i++ )
pCnf->pClauses[i] = pCnf->pClauses[0] + (p->pClauses[i] - p->pClauses[0]);
return pCnf;
}
Cnf_Dat_t * Cnf_DataDupCof( Cnf_Dat_t * p, int Lit )
{
Cnf_Dat_t * pCnf;
int i;
pCnf = Cnf_DataAlloc( p->pMan, p->nVars, p->nClauses+1, p->nLiterals+1 );
memcpy( pCnf->pClauses[0], p->pClauses[0], sizeof(int) * p->nLiterals );
if ( pCnf->pVarNums )
memcpy( pCnf->pVarNums, p->pVarNums, sizeof(int) * Aig_ManObjNumMax(p->pMan) );
for ( i = 1; i < p->nClauses; i++ )
pCnf->pClauses[i] = pCnf->pClauses[0] + (p->pClauses[i] - p->pClauses[0]);
pCnf->pClauses[p->nClauses] = pCnf->pClauses[0] + p->nLiterals;
pCnf->pClauses[p->nClauses][0] = Lit;
assert( pCnf->pClauses[p->nClauses+1] == pCnf->pClauses[0] + p->nLiterals+1 );
return pCnf;
}
Cnf_Dat_t * Cnf_DataDupCofArray( Cnf_Dat_t * p, Vec_Int_t * vLits )
{
Cnf_Dat_t * pCnf;
int i, iLit;
pCnf = Cnf_DataAlloc( p->pMan, p->nVars, p->nClauses+Vec_IntSize(vLits), p->nLiterals+Vec_IntSize(vLits) );
memcpy( pCnf->pClauses[0], p->pClauses[0], sizeof(int) * p->nLiterals );
if ( pCnf->pVarNums )
memcpy( pCnf->pVarNums, p->pVarNums, sizeof(int) * Aig_ManObjNumMax(p->pMan) );
for ( i = 1; i < p->nClauses; i++ )
pCnf->pClauses[i] = pCnf->pClauses[0] + (p->pClauses[i] - p->pClauses[0]);
Vec_IntForEachEntry( vLits, iLit, i ) {
pCnf->pClauses[p->nClauses+i] = pCnf->pClauses[0] + p->nLiterals+i;
pCnf->pClauses[p->nClauses+i][0] = iLit;
}
assert( pCnf->pClauses[p->nClauses+Vec_IntSize(vLits)] == pCnf->pClauses[0] + p->nLiterals+Vec_IntSize(vLits) );
return pCnf;
}
/**Function*************************************************************

747
src/sat/cnf/cnfUtil.c
View File

@ -9,7 +9,7 @@
Synopsis []
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - April 28, 2007.]
@ -23,55 +23,253 @@
ABC_NAMESPACE_IMPL_START
#ifdef ABC_USE_PTHREADS
#ifdef _WIN32
#include "../lib/pthread.h"
#else
#include <pthread.h>
#include <unistd.h>
#endif
#endif
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
extern Vec_Int_t *Exa4_ManParse(char *pFileName);
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Computes area, references, and nodes used in the mapping.]
Synopsis [Solving problems using one core.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Aig_ManScanMapping_rec( Cnf_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vMapped )
Vec_Int_t *Cnf_RunSolverOnce(int Id, int Rand, int TimeOut, int fVerbose)
{
Aig_Obj_t * pLeaf;
Dar_Cut_t * pCutBest;
int aArea, i;
if ( pObj->nRefs++ || Aig_ObjIsCi(pObj) || Aig_ObjIsConst1(pObj) )
return 0;
assert( Aig_ObjIsAnd(pObj) );
// collect the node first to derive pre-order
if ( vMapped )
Vec_PtrPush( vMapped, pObj );
// visit the transitive fanin of the selected cut
if ( pObj->fMarkB )
int fVerboseSolver = 0;
Vec_Int_t *vRes = NULL;
abctime clkTotal = Abc_Clock();
char FileNameIn[100], FileNameOut[100];
sprintf(FileNameIn, "%02d.cnf", Id);
sprintf(FileNameOut, "%02d.txt", Id);
#ifdef _WIN32
char *pKissat = "kissat.exe";
#else
char *pKissat = "kissat";
#endif
char Command[1000], *pCommand = (char *)&Command;
if (TimeOut)
sprintf(pCommand, "%s --seed=%d --time=%d %s %s > %s", pKissat, Rand, TimeOut, fVerboseSolver ? "" : "-q", FileNameIn, FileNameOut);
else
sprintf(pCommand, "%s --seed=%d %s %s > %s", pKissat, Rand, fVerboseSolver ? "" : "-q", FileNameIn, FileNameOut);
//printf( "Thread command: %s\n", pCommand);
FILE * pFile = fopen(FileNameIn, "rb");
if ( pFile != NULL ) {
fclose( pFile );
if (system(pCommand) == -1) {
fprintf(stdout, "Command \"%s\" did not succeed.\n", pCommand);
return 0;
}
vRes = Exa4_ManParse(FileNameOut); // FileNameOut is removed here
}
if (fVerbose) {
double SolvingTime = ((double)(Abc_Clock() - clkTotal))/((double)CLOCKS_PER_SEC);
if (vRes)
printf("Problem %2d has a solution. ", Id);
else if (vRes == NULL && (TimeOut == 0 || SolvingTime < (double)TimeOut))
printf("Problem %2d has no solution. ", Id);
else if (vRes == NULL)
printf("Problem %2d has no solution or timed out after %d sec. ", Id, TimeOut);
Abc_PrintTime(1, "Solving time", Abc_Clock() - clkTotal );
}
else if (vRes) {
printf("Problem %2d has a solution. ", Id);
Abc_PrintTime(1, "Solving time", Abc_Clock() - clkTotal );
printf("(Currently waiting for %d sec for other threads to finish.)\n", TimeOut);
}
return vRes;
}
Vec_Int_t * Cnf_RunSolverArray(int nProcs, int TimeOut, int fVerbose)
{
Vec_Int_t *vRes = NULL; int i;
for ( i = 0; i < nProcs; i++ )
if ((vRes = Cnf_RunSolverOnce(i, 0, TimeOut, fVerbose)))
break;
return vRes;
}
/**Function*************************************************************
Synopsis [Solving problems using many cores.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
#ifndef ABC_USE_PTHREADS
Vec_Int_t *Cnf_RunSolver(int nProcs, int TimeOut, int fVerbose)
{
return Cnf_RunSolverArray(nProcs, TimeOut, fVerbose);
}
#else // pthreads are used
#define PAR_THR_MAX 100
typedef struct Cnf_ThData_t_
{
Vec_Int_t *vRes;
int Index;
int Rand;
int nTimeOut;
int fWorking;
int fVerbose;
} Cnf_ThData_t;
void *Cnf_WorkerThread(void *pArg)
{
Cnf_ThData_t *pThData = (Cnf_ThData_t *)pArg;
volatile int *pPlace = &pThData->fWorking;
while (1)
{
Vec_Ptr_t * vSuper = Vec_PtrAlloc( 100 );
Aig_ObjCollectSuper( pObj, vSuper );
while (*pPlace == 0)
;
assert(pThData->fWorking);
if (pThData->Index == -1)
{
pthread_exit(NULL);
assert(0);
return NULL;
}
pThData->vRes = Cnf_RunSolverOnce(pThData->Index, pThData->Rand, pThData->nTimeOut, pThData->fVerbose);
pThData->fWorking = 0;
}
assert(0);
return NULL;
}
Vec_Int_t *Cnf_RunSolver(int nProcs, int TimeOut, int fVerbose)
{
Vec_Int_t *vRes = NULL;
Cnf_ThData_t ThData[PAR_THR_MAX];
pthread_t WorkerThread[PAR_THR_MAX];
int i, k, status;
if (fVerbose)
printf("Running concurrent solving with %d processes.\n", nProcs);
fflush(stdout);
if (nProcs < 2)
return Cnf_RunSolverArray(nProcs, TimeOut, fVerbose);
// subtract manager thread
// nProcs--;
assert(nProcs >= 1 && nProcs <= PAR_THR_MAX);
// start threads
for (i = 0; i < nProcs; i++)
{
ThData[i].vRes = NULL;
ThData[i].Index = -1;
ThData[i].Rand = Abc_Random(0) % 0x1000000;
ThData[i].nTimeOut = TimeOut;
ThData[i].fWorking = 0;
ThData[i].fVerbose = fVerbose;
status = pthread_create(WorkerThread + i, NULL, Cnf_WorkerThread, (void *)(ThData + i));
assert(status == 0);
}
// look at the threads
for (k = 0; k < nProcs;)
{
for (i = 0; i < nProcs; i++)
{
if (ThData[i].fWorking)
continue;
if (ThData[i].vRes)
{
k = nProcs;
break;
}
ThData[i].Index = k++;
ThData[i].fWorking = 1;
break;
}
}
// wait till threads finish
for (i = 0; i < nProcs; i++)
if (ThData[i].fWorking)
i = -1;
// stop threads
for (i = 0; i < nProcs; i++)
{
assert(!ThData[i].fWorking);
if (ThData[i].vRes && vRes == NULL)
{
vRes = ThData[i].vRes;
ThData[i].vRes = NULL;
}
Vec_IntFreeP(&ThData[i].vRes);
// stop
ThData[i].Index = -1;
ThData[i].fWorking = 1;
}
return vRes;
}
#endif // pthreads are used
/**Function*************************************************************
Synopsis [Computes area, references, and nodes used in the mapping.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Aig_ManScanMapping_rec(Cnf_Man_t *p, Aig_Obj_t *pObj, Vec_Ptr_t *vMapped)
{
Aig_Obj_t *pLeaf;
Dar_Cut_t *pCutBest;
int aArea, i;
if (pObj->nRefs++ || Aig_ObjIsCi(pObj) || Aig_ObjIsConst1(pObj))
return 0;
assert(Aig_ObjIsAnd(pObj));
// collect the node first to derive pre-order
if (vMapped)
Vec_PtrPush(vMapped, pObj);
// visit the transitive fanin of the selected cut
if (pObj->fMarkB)
{
Vec_Ptr_t *vSuper = Vec_PtrAlloc(100);
Aig_ObjCollectSuper(pObj, vSuper);
aArea = Vec_PtrSize(vSuper) + 1;
Vec_PtrForEachEntry( Aig_Obj_t *, vSuper, pLeaf, i )
aArea += Aig_ManScanMapping_rec( p, Aig_Regular(pLeaf), vMapped );
Vec_PtrFree( vSuper );
Vec_PtrForEachEntry(Aig_Obj_t *, vSuper, pLeaf, i)
aArea += Aig_ManScanMapping_rec(p, Aig_Regular(pLeaf), vMapped);
Vec_PtrFree(vSuper);
////////////////////////////
pObj->fMarkB = 1;
}
else
{
pCutBest = Dar_ObjBestCut( pObj );
aArea = Cnf_CutSopCost( p, pCutBest );
Dar_CutForEachLeaf( p->pManAig, pCutBest, pLeaf, i )
aArea += Aig_ManScanMapping_rec( p, pLeaf, vMapped );
pCutBest = Dar_ObjBestCut(pObj);
aArea = Cnf_CutSopCost(p, pCutBest);
Dar_CutForEachLeaf(p->pManAig, pCutBest, pLeaf, i)
aArea += Aig_ManScanMapping_rec(p, pLeaf, vMapped);
}
return aArea;
}
@ -81,28 +279,28 @@ int Aig_ManScanMapping_rec( Cnf_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vMapped
Synopsis [Computes area, references, and nodes used in the mapping.]
Description [Collects the nodes in reverse topological order.]
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Ptr_t * Aig_ManScanMapping( Cnf_Man_t * p, int fCollect )
Vec_Ptr_t *Aig_ManScanMapping(Cnf_Man_t *p, int fCollect)
{
Vec_Ptr_t * vMapped = NULL;
Aig_Obj_t * pObj;
Vec_Ptr_t *vMapped = NULL;
Aig_Obj_t *pObj;
int i;
// clean all references
Aig_ManForEachObj( p->pManAig, pObj, i )
Aig_ManForEachObj(p->pManAig, pObj, i)
pObj->nRefs = 0;
// allocate the array
if ( fCollect )
vMapped = Vec_PtrAlloc( 1000 );
if (fCollect)
vMapped = Vec_PtrAlloc(1000);
// collect nodes reachable from POs in the DFS order through the best cuts
p->aArea = 0;
Aig_ManForEachCo( p->pManAig, pObj, i )
p->aArea += Aig_ManScanMapping_rec( p, Aig_ObjFanin0(pObj), vMapped );
// printf( "Variables = %6d. Clauses = %8d.\n", vMapped? Vec_PtrSize(vMapped) + Aig_ManCiNum(p->pManAig) + 1 : 0, p->aArea + 2 );
Aig_ManForEachCo(p->pManAig, pObj, i)
p->aArea += Aig_ManScanMapping_rec(p, Aig_ObjFanin0(pObj), vMapped);
// printf( "Variables = %6d. Clauses = %8d.\n", vMapped? Vec_PtrSize(vMapped) + Aig_ManCiNum(p->pManAig) + 1 : 0, p->aArea + 2 );
return vMapped;
}
@ -111,48 +309,48 @@ Vec_Ptr_t * Aig_ManScanMapping( Cnf_Man_t * p, int fCollect )
Synopsis [Computes area, references, and nodes used in the mapping.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Cnf_ManScanMapping_rec( Cnf_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vMapped, int fPreorder )
int Cnf_ManScanMapping_rec(Cnf_Man_t *p, Aig_Obj_t *pObj, Vec_Ptr_t *vMapped, int fPreorder)
{
Aig_Obj_t * pLeaf;
Cnf_Cut_t * pCutBest;
Aig_Obj_t *pLeaf;
Cnf_Cut_t *pCutBest;
int aArea, i;
if ( pObj->nRefs++ || Aig_ObjIsCi(pObj) || Aig_ObjIsConst1(pObj) )
if (pObj->nRefs++ || Aig_ObjIsCi(pObj) || Aig_ObjIsConst1(pObj))
return 0;
assert( Aig_ObjIsAnd(pObj) );
assert( pObj->pData != NULL );
assert(Aig_ObjIsAnd(pObj));
assert(pObj->pData != NULL);
// add the node to the mapping
if ( vMapped && fPreorder )
Vec_PtrPush( vMapped, pObj );
if (vMapped && fPreorder)
Vec_PtrPush(vMapped, pObj);
// visit the transitive fanin of the selected cut
if ( pObj->fMarkB )
if (pObj->fMarkB)
{
Vec_Ptr_t * vSuper = Vec_PtrAlloc( 100 );
Aig_ObjCollectSuper( pObj, vSuper );
Vec_Ptr_t *vSuper = Vec_PtrAlloc(100);
Aig_ObjCollectSuper(pObj, vSuper);
aArea = Vec_PtrSize(vSuper) + 1;
Vec_PtrForEachEntry( Aig_Obj_t *, vSuper, pLeaf, i )
aArea += Cnf_ManScanMapping_rec( p, Aig_Regular(pLeaf), vMapped, fPreorder );
Vec_PtrFree( vSuper );
Vec_PtrForEachEntry(Aig_Obj_t *, vSuper, pLeaf, i)
aArea += Cnf_ManScanMapping_rec(p, Aig_Regular(pLeaf), vMapped, fPreorder);
Vec_PtrFree(vSuper);
////////////////////////////
pObj->fMarkB = 1;
}
else
{
pCutBest = (Cnf_Cut_t *)pObj->pData;
// assert( pCutBest->nFanins > 0 );
assert( pCutBest->Cost < 127 );
// assert( pCutBest->nFanins > 0 );
assert(pCutBest->Cost < 127);
aArea = pCutBest->Cost;
Cnf_CutForEachLeaf( p->pManAig, pCutBest, pLeaf, i )
aArea += Cnf_ManScanMapping_rec( p, pLeaf, vMapped, fPreorder );
Cnf_CutForEachLeaf(p->pManAig, pCutBest, pLeaf, i)
aArea += Cnf_ManScanMapping_rec(p, pLeaf, vMapped, fPreorder);
}
// add the node to the mapping
if ( vMapped && !fPreorder )
Vec_PtrPush( vMapped, pObj );
if (vMapped && !fPreorder)
Vec_PtrPush(vMapped, pObj);
return aArea;
}
@ -161,28 +359,28 @@ int Cnf_ManScanMapping_rec( Cnf_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vMapped
Synopsis [Computes area, references, and nodes used in the mapping.]
Description [Collects the nodes in reverse topological order.]
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Ptr_t * Cnf_ManScanMapping( Cnf_Man_t * p, int fCollect, int fPreorder )
Vec_Ptr_t *Cnf_ManScanMapping(Cnf_Man_t *p, int fCollect, int fPreorder)
{
Vec_Ptr_t * vMapped = NULL;
Aig_Obj_t * pObj;
Vec_Ptr_t *vMapped = NULL;
Aig_Obj_t *pObj;
int i;
// clean all references
Aig_ManForEachObj( p->pManAig, pObj, i )
Aig_ManForEachObj(p->pManAig, pObj, i)
pObj->nRefs = 0;
// allocate the array
if ( fCollect )
vMapped = Vec_PtrAlloc( 1000 );
if (fCollect)
vMapped = Vec_PtrAlloc(1000);
// collect nodes reachable from POs in the DFS order through the best cuts
p->aArea = 0;
Aig_ManForEachCo( p->pManAig, pObj, i )
p->aArea += Cnf_ManScanMapping_rec( p, Aig_ObjFanin0(pObj), vMapped, fPreorder );
// printf( "Variables = %6d. Clauses = %8d.\n", vMapped? Vec_PtrSize(vMapped) + Aig_ManCiNum(p->pManAig) + 1 : 0, p->aArea + 2 );
Aig_ManForEachCo(p->pManAig, pObj, i)
p->aArea += Cnf_ManScanMapping_rec(p, Aig_ObjFanin0(pObj), vMapped, fPreorder);
// printf( "Variables = %6d. Clauses = %8d.\n", vMapped? Vec_PtrSize(vMapped) + Aig_ManCiNum(p->pManAig) + 1 : 0, p->aArea + 2 );
return vMapped;
}
@ -191,20 +389,20 @@ Vec_Ptr_t * Cnf_ManScanMapping( Cnf_Man_t * p, int fCollect, int fPreorder )
Synopsis [Returns the array of CI IDs.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Cnf_DataCollectCiSatNums( Cnf_Dat_t * pCnf, Aig_Man_t * p )
Vec_Int_t *Cnf_DataCollectCiSatNums(Cnf_Dat_t *pCnf, Aig_Man_t *p)
{
Vec_Int_t * vCiIds;
Aig_Obj_t * pObj;
Vec_Int_t *vCiIds;
Aig_Obj_t *pObj;
int i;
vCiIds = Vec_IntAlloc( Aig_ManCiNum(p) );
Aig_ManForEachCi( p, pObj, i )
Vec_IntPush( vCiIds, pCnf->pVarNums[pObj->Id] );
vCiIds = Vec_IntAlloc(Aig_ManCiNum(p));
Aig_ManForEachCi(p, pObj, i)
Vec_IntPush(vCiIds, pCnf->pVarNums[pObj->Id]);
return vCiIds;
}
@ -213,20 +411,20 @@ Vec_Int_t * Cnf_DataCollectCiSatNums( Cnf_Dat_t * pCnf, Aig_Man_t * p )
Synopsis [Returns the array of CI IDs.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Cnf_DataCollectCoSatNums( Cnf_Dat_t * pCnf, Aig_Man_t * p )
Vec_Int_t *Cnf_DataCollectCoSatNums(Cnf_Dat_t *pCnf, Aig_Man_t *p)
{
Vec_Int_t * vCoIds;
Aig_Obj_t * pObj;
Vec_Int_t *vCoIds;
Aig_Obj_t *pObj;
int i;
vCoIds = Vec_IntAlloc( Aig_ManCoNum(p) );
Aig_ManForEachCo( p, pObj, i )
Vec_IntPush( vCoIds, pCnf->pVarNums[pObj->Id] );
vCoIds = Vec_IntAlloc(Aig_ManCoNum(p));
Aig_ManForEachCo(p, pObj, i)
Vec_IntPush(vCoIds, pCnf->pVarNums[pObj->Id]);
return vCoIds;
}
@ -235,58 +433,58 @@ Vec_Int_t * Cnf_DataCollectCoSatNums( Cnf_Dat_t * pCnf, Aig_Man_t * p )
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
unsigned char * Cnf_DataDeriveLitPolarities( Cnf_Dat_t * p )
unsigned char *Cnf_DataDeriveLitPolarities(Cnf_Dat_t *p)
{
int i, c, iClaBeg, iClaEnd, * pLit;
unsigned * pPols0 = ABC_CALLOC( unsigned, Aig_ManObjNumMax(p->pMan) );
unsigned * pPols1 = ABC_CALLOC( unsigned, Aig_ManObjNumMax(p->pMan) );
unsigned char * pPres = ABC_CALLOC( unsigned char, p->nClauses );
for ( i = 0; i < Aig_ManObjNumMax(p->pMan); i++ )
int i, c, iClaBeg, iClaEnd, *pLit;
unsigned *pPols0 = ABC_CALLOC(unsigned, Aig_ManObjNumMax(p->pMan));
unsigned *pPols1 = ABC_CALLOC(unsigned, Aig_ManObjNumMax(p->pMan));
unsigned char *pPres = ABC_CALLOC(unsigned char, p->nClauses);
for (i = 0; i < Aig_ManObjNumMax(p->pMan); i++)
{
if ( p->pObj2Count[i] == 0 )
if (p->pObj2Count[i] == 0)
continue;
iClaBeg = p->pObj2Clause[i];
iClaEnd = p->pObj2Clause[i] + p->pObj2Count[i];
// go through the negative polarity clauses
for ( c = iClaBeg; c < iClaEnd; c++ )
for ( pLit = p->pClauses[c]+1; pLit < p->pClauses[c+1]; pLit++ )
if ( Abc_LitIsCompl(p->pClauses[c][0]) )
pPols0[Abc_Lit2Var(*pLit)] |= (unsigned)(2 - Abc_LitIsCompl(*pLit)); // taking the opposite (!) -- not the case
for (c = iClaBeg; c < iClaEnd; c++)
for (pLit = p->pClauses[c] + 1; pLit < p->pClauses[c + 1]; pLit++)
if (Abc_LitIsCompl(p->pClauses[c][0]))
pPols0[Abc_Lit2Var(*pLit)] |= (unsigned)(2 - Abc_LitIsCompl(*pLit)); // taking the opposite (!) -- not the case
else
pPols1[Abc_Lit2Var(*pLit)] |= (unsigned)(2 - Abc_LitIsCompl(*pLit)); // taking the opposite (!) -- not the case
pPols1[Abc_Lit2Var(*pLit)] |= (unsigned)(2 - Abc_LitIsCompl(*pLit)); // taking the opposite (!) -- not the case
// record these clauses
for ( c = iClaBeg; c < iClaEnd; c++ )
for ( pLit = p->pClauses[c]+1; pLit < p->pClauses[c+1]; pLit++ )
if ( Abc_LitIsCompl(p->pClauses[c][0]) )
pPres[c] = (unsigned char)( (unsigned)pPres[c] | (pPols0[Abc_Lit2Var(*pLit)] << (2*(pLit-p->pClauses[c]-1))) );
for (c = iClaBeg; c < iClaEnd; c++)
for (pLit = p->pClauses[c] + 1; pLit < p->pClauses[c + 1]; pLit++)
if (Abc_LitIsCompl(p->pClauses[c][0]))
pPres[c] = (unsigned char)((unsigned)pPres[c] | (pPols0[Abc_Lit2Var(*pLit)] << (2 * (pLit - p->pClauses[c] - 1))));
else
pPres[c] = (unsigned char)( (unsigned)pPres[c] | (pPols1[Abc_Lit2Var(*pLit)] << (2*(pLit-p->pClauses[c]-1))) );
pPres[c] = (unsigned char)((unsigned)pPres[c] | (pPols1[Abc_Lit2Var(*pLit)] << (2 * (pLit - p->pClauses[c] - 1))));
// clean negative polarity
for ( c = iClaBeg; c < iClaEnd; c++ )
for ( pLit = p->pClauses[c]+1; pLit < p->pClauses[c+1]; pLit++ )
for (c = iClaBeg; c < iClaEnd; c++)
for (pLit = p->pClauses[c] + 1; pLit < p->pClauses[c + 1]; pLit++)
pPols0[Abc_Lit2Var(*pLit)] = pPols1[Abc_Lit2Var(*pLit)] = 0;
}
ABC_FREE( pPols0 );
ABC_FREE( pPols1 );
/*
// for ( c = 0; c < p->nClauses; c++ )
for ( c = 0; c < 100; c++ )
{
printf( "Clause %6d : ", c );
for ( i = 0; i < 4; i++ )
printf( "%d ", ((unsigned)pPres[c] >> (2*i)) & 3 );
printf( " " );
for ( pLit = p->pClauses[c]; pLit < p->pClauses[c+1]; pLit++ )
printf( "%6d ", *pLit );
printf( "\n" );
}
*/
ABC_FREE(pPols0);
ABC_FREE(pPols1);
/*
// for ( c = 0; c < p->nClauses; c++ )
for ( c = 0; c < 100; c++ )
{
printf( "Clause %6d : ", c );
for ( i = 0; i < 4; i++ )
printf( "%d ", ((unsigned)pPres[c] >> (2*i)) & 3 );
printf( " " );
for ( pLit = p->pClauses[c]; pLit < p->pClauses[c+1]; pLit++ )
printf( "%6d ", *pLit );
printf( "\n" );
}
*/
return pPres;
}
@ -295,96 +493,96 @@ unsigned char * Cnf_DataDeriveLitPolarities( Cnf_Dat_t * p )
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Cnf_Dat_t * Cnf_DataReadFromFile( char * pFileName )
Cnf_Dat_t *Cnf_DataReadFromFile(char *pFileName)
{
int MaxLine = 1000000;
int Var, Lit, nVars = -1, nClas = -1, i, Entry, iLine = 0;
Cnf_Dat_t * pCnf = NULL;
Vec_Int_t * vClas = NULL;
Vec_Int_t * vLits = NULL;
char * pBuffer, * pToken;
FILE * pFile = fopen( pFileName, "rb" );
if ( pFile == NULL )
Cnf_Dat_t *pCnf = NULL;
Vec_Int_t *vClas = NULL;
Vec_Int_t *vLits = NULL;
char *pBuffer, *pToken;
FILE *pFile = fopen(pFileName, "rb");
if (pFile == NULL)
{
printf( "Cannot open file \"%s\" for writing.\n", pFileName );
printf("Cannot open file \"%s\" for writing.\n", pFileName);
return NULL;
}
pBuffer = ABC_ALLOC( char, MaxLine );
while ( fgets(pBuffer, MaxLine, pFile) != NULL )
pBuffer = ABC_ALLOC(char, MaxLine);
while (fgets(pBuffer, MaxLine, pFile) != NULL)
{
iLine++;
if ( pBuffer[0] == 'c' )
if (pBuffer[0] == 'c')
continue;
if ( pBuffer[0] == 'p' )
if (pBuffer[0] == 'p')
{
pToken = strtok( pBuffer+1, " \t" );
if ( strcmp(pToken, "cnf") )
pToken = strtok(pBuffer + 1, " \t");
if (strcmp(pToken, "cnf"))
{
printf( "Incorrect input file.\n" );
printf("Incorrect input file.\n");
goto finish;
}
pToken = strtok( NULL, " \t" );
nVars = atoi( pToken );
pToken = strtok( NULL, " \t" );
nClas = atoi( pToken );
if ( nVars <= 0 || nClas <= 0 )
pToken = strtok(NULL, " \t");
nVars = atoi(pToken);
pToken = strtok(NULL, " \t");
nClas = atoi(pToken);
if (nVars <= 0 || nClas <= 0)
{
printf( "Incorrect parameters.\n" );
printf("Incorrect parameters.\n");
goto finish;
}
// temp storage
vClas = Vec_IntAlloc( nClas+1 );
vLits = Vec_IntAlloc( nClas*8 );
vClas = Vec_IntAlloc(nClas + 1);
vLits = Vec_IntAlloc(nClas * 8);
continue;
}
pToken = strtok( pBuffer, " \t\r\n" );
if ( pToken == NULL )
pToken = strtok(pBuffer, " \t\r\n");
if (pToken == NULL)
continue;
Vec_IntPush( vClas, Vec_IntSize(vLits) );
while ( pToken )
Vec_IntPush(vClas, Vec_IntSize(vLits));
while (pToken)
{
Var = atoi( pToken );
if ( Var == 0 )
Var = atoi(pToken);
if (Var == 0)
break;
Lit = (Var > 0) ? Abc_Var2Lit(Var-1, 0) : Abc_Var2Lit(-Var-1, 1);
if ( Lit >= 2*nVars )
Lit = (Var > 0) ? Abc_Var2Lit(Var - 1, 0) : Abc_Var2Lit(-Var - 1, 1);
if (Lit >= 2 * nVars)
{
printf( "Literal %d is out-of-bound for %d variables.\n", Lit, nVars );
printf("Literal %d is out-of-bound for %d variables.\n", Lit, nVars);
goto finish;
}
Vec_IntPush( vLits, Lit );
pToken = strtok( NULL, " \t\r\n" );
Vec_IntPush(vLits, Lit);
pToken = strtok(NULL, " \t\r\n");
}
if ( Var != 0 )
if (Var != 0)
{
printf( "There is no zero-terminator in line %d.\n", iLine );
printf("There is no zero-terminator in line %d.\n", iLine);
goto finish;
}
}
// finalize
if ( Vec_IntSize(vClas) != nClas )
printf( "Warning! The number of clauses (%d) is different from declaration (%d).\n", Vec_IntSize(vClas), nClas );
Vec_IntPush( vClas, Vec_IntSize(vLits) );
if (Vec_IntSize(vClas) != nClas)
printf("Warning! The number of clauses (%d) is different from declaration (%d).\n", Vec_IntSize(vClas), nClas);
Vec_IntPush(vClas, Vec_IntSize(vLits));
// create
pCnf = ABC_CALLOC( Cnf_Dat_t, 1 );
pCnf->nVars = nVars;
pCnf->nClauses = Vec_IntSize(vClas)-1;
pCnf = ABC_CALLOC(Cnf_Dat_t, 1);
pCnf->nVars = nVars;
pCnf->nClauses = Vec_IntSize(vClas) - 1;
pCnf->nLiterals = Vec_IntSize(vLits);
pCnf->pClauses = ABC_ALLOC( int *, Vec_IntSize(vClas) );
pCnf->pClauses = ABC_ALLOC(int *, Vec_IntSize(vClas));
pCnf->pClauses[0] = Vec_IntReleaseArray(vLits);
Vec_IntForEachEntry( vClas, Entry, i )
Vec_IntForEachEntry(vClas, Entry, i)
pCnf->pClauses[i] = pCnf->pClauses[0] + Entry;
finish:
fclose( pFile );
Vec_IntFreeP( &vClas );
Vec_IntFreeP( &vLits );
ABC_FREE( pBuffer );
fclose(pFile);
Vec_IntFreeP(&vClas);
Vec_IntFreeP(&vLits);
ABC_FREE(pBuffer);
return pCnf;
}
@ -393,87 +591,224 @@ finish:
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Cnf_DataSolveFromFile( char * pFileName, int nConfLimit, int nLearnedStart, int nLearnedDelta, int nLearnedPerce, int fVerbose, int fShowPattern, int ** ppModel, int nPis )
int Cnf_DataSolveFromFile(char *pFileName, int nConfLimit, int nLearnedStart, int nLearnedDelta, int nLearnedPerce, int fVerbose, int fShowPattern, int **ppModel, int nPis)
{
abctime clk = Abc_Clock();
Cnf_Dat_t * pCnf = Cnf_DataReadFromFile( pFileName );
sat_solver * pSat;
Cnf_Dat_t *pCnf = Cnf_DataReadFromFile(pFileName);
sat_solver *pSat;
int i, status, RetValue = -1;
if ( pCnf == NULL )
if (pCnf == NULL)
return -1;
if ( fVerbose )
if (fVerbose)
{
printf( "CNF stats: Vars = %6d. Clauses = %7d. Literals = %8d. ", pCnf->nVars, pCnf->nClauses, pCnf->nLiterals );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
printf("CNF stats: Vars = %6d. Clauses = %7d. Literals = %8d. ", pCnf->nVars, pCnf->nClauses, pCnf->nLiterals);
Abc_PrintTime(1, "Time", Abc_Clock() - clk);
}
// convert into SAT solver
pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
if ( pSat == NULL )
pSat = (sat_solver *)Cnf_DataWriteIntoSolver(pCnf, 1, 0);
if (pSat == NULL)
{
printf( "The problem is trivially UNSAT.\n" );
Cnf_DataFree( pCnf );
printf("The problem is trivially UNSAT.\n");
Cnf_DataFree(pCnf);
return 1;
}
if ( nLearnedStart )
if (nLearnedStart)
pSat->nLearntStart = pSat->nLearntMax = nLearnedStart;
if ( nLearnedDelta )
if (nLearnedDelta)
pSat->nLearntDelta = nLearnedDelta;
if ( nLearnedPerce )
if (nLearnedPerce)
pSat->nLearntRatio = nLearnedPerce;
if ( fVerbose )
if (fVerbose)
pSat->fVerbose = fVerbose;
//sat_solver_start_cardinality( pSat, 100 );
// sat_solver_start_cardinality( pSat, 100 );
// solve the miter
status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)nConfLimit, 0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
if ( status == l_Undef )
status = sat_solver_solve(pSat, NULL, NULL, (ABC_INT64_T)nConfLimit, 0, (ABC_INT64_T)0, (ABC_INT64_T)0);
if (status == l_Undef)
RetValue = -1;
else if ( status == l_True )
else if (status == l_True)
RetValue = 0;
else if ( status == l_False )
else if (status == l_False)
RetValue = 1;
else
assert( 0 );
if ( fVerbose )
Sat_SolverPrintStats( stdout, pSat );
if ( RetValue == -1 )
Abc_Print( 1, "UNDECIDED " );
else if ( RetValue == 0 )
Abc_Print( 1, "SATISFIABLE " );
assert(0);
if (fVerbose)
Sat_SolverPrintStats(stdout, pSat);
if (RetValue == -1)
Abc_Print(1, "UNDECIDED ");
else if (RetValue == 0)
Abc_Print(1, "SATISFIABLE ");
else
Abc_Print( 1, "UNSATISFIABLE " );
//Abc_Print( -1, "\n" );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
Abc_Print(1, "UNSATISFIABLE ");
// Abc_Print( -1, "\n" );
Abc_PrintTime(1, "Time", Abc_Clock() - clk);
// derive SAT assignment
if ( RetValue == 0 && nPis > 0 )
if (RetValue == 0 && nPis > 0)
{
*ppModel = ABC_ALLOC( int, nPis );
for ( i = 0; i < nPis; i++ )
(*ppModel)[i] = sat_solver_var_value( pSat, pCnf->nVars - nPis + i );
*ppModel = ABC_ALLOC(int, nPis);
for (i = 0; i < nPis; i++)
(*ppModel)[i] = sat_solver_var_value(pSat, pCnf->nVars - nPis + i);
}
if ( RetValue == 0 && fShowPattern )
if (RetValue == 0 && fShowPattern)
{
for ( i = 0; i < pCnf->nVars; i++ )
printf( "%d", sat_solver_var_value(pSat,i) );
printf( "\n" );
for (i = 0; i < pCnf->nVars; i++)
printf("%d", sat_solver_var_value(pSat, i));
printf("\n");
}
Cnf_DataFree( pCnf );
sat_solver_delete( pSat );
Cnf_DataFree(pCnf);
sat_solver_delete(pSat);
return RetValue;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Cnf_DataBestVar(Cnf_Dat_t *p, int *pSkip)
{
int *pNums = ABC_CALLOC(int, p->nVars);
int i, *pLit, NumMax = -1, iVarMax = -1;
for (i = 0; i < p->nClauses; i++)
for (pLit = p->pClauses[i]; pLit < p->pClauses[i + 1]; pLit++)
pNums[Abc_Lit2Var(*pLit)]++;
for (i = 0; i < p->nVars; i++)
if ((!pSkip || !pSkip[i]) && NumMax < pNums[i])
NumMax = pNums[i], iVarMax = i;
ABC_FREE(pNums);
return iVarMax;
}
void Cnf_Experiment1()
{
Cnf_Dat_t *pTemp, *p = Cnf_DataReadFromFile("../166b.cnf");
int i, *pSkip = ABC_CALLOC(int, p->nVars);
for (i = 0; i < 100; i++)
{
int iVar = Cnf_DataBestVar(p, pSkip);
char FileName[100];
sprintf(FileName, "cnf/%03d.cnf", i);
Cnf_DataWriteIntoFile(p, FileName, 0, NULL, NULL);
printf("Dumped file \"%s\".\n", FileName);
p = Cnf_DataDupCof(pTemp = p, Abc_Var2Lit(iVar, 0));
Cnf_DataFree(pTemp);
pSkip[iVar] = 1;
}
Cnf_DataFree(p);
ABC_FREE(pSkip);
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t *Cnf_GenRandLits(int iVarBeg, int iVarEnd, int nLits, int Value, int Rand, int fVerbose)
{
Vec_Int_t *vLits = Vec_IntAlloc(nLits);
assert(iVarBeg < iVarEnd && nLits < iVarEnd - iVarBeg);
while (Vec_IntSize(vLits) < nLits)
{
int iVar = iVarBeg + (Abc_Random(0) ^ Rand) % (iVarEnd - iVarBeg);
assert(iVar >= iVarBeg && iVar < iVarEnd);
if (Vec_IntFind(vLits, Abc_Var2Lit(iVar, 0)) == -1 && Vec_IntFind(vLits, Abc_Var2Lit(iVar, 1)) == -1)
{
if (Value == 0)
Vec_IntPush(vLits, Abc_Var2Lit(iVar, 1));
else if (Value == 1)
Vec_IntPush(vLits, Abc_Var2Lit(iVar, 0));
else
Vec_IntPush(vLits, Abc_Var2Lit(iVar, Abc_Random(0) & 1));
}
}
Vec_IntSort(vLits, 0);
if ( fVerbose )
Vec_IntPrint(vLits);
fflush(stdout);
return vLits;
}
void Cnf_SplitCnfFile(char * pFileName, int nParts, int iVarBeg, int iVarEnd, int nLits, int Value, int Rand, int fPrepro, int fVerbose)
{
Cnf_Dat_t *p = Cnf_DataReadFromFile(pFileName); int k;
if (iVarEnd == ABC_INFINITY)
iVarEnd = p->nVars;
for (k = 0; k < nParts; k++)
{
Vec_Int_t *vLits = Cnf_GenRandLits(iVarBeg, iVarEnd, nLits, Value, Rand, fVerbose);
Cnf_Dat_t *pCnf = Cnf_DataDupCofArray(p, vLits);
char FileName[100]; sprintf(FileName, "%02d.cnf", k);
if ( fPrepro ) {
char Command[1000];
sprintf(Command, "satelite --verbosity=0 -pre temp.cnf %s", FileName);
Cnf_DataWriteIntoFile(pCnf, "temp.cnf", 0, NULL, NULL);
if (system(Command) == -1) {
fprintf(stdout, "Command \"%s\" did not succeed. Preprocessing skipped.\n", Command);
Cnf_DataWriteIntoFile(pCnf, FileName, 0, NULL, NULL);
}
unlink("temp.cnf");
}
else
Cnf_DataWriteIntoFile(pCnf, FileName, 0, NULL, NULL);
Cnf_DataFree(pCnf);
Vec_IntFree(vLits);
}
Cnf_DataFree(p);
}
void Cnf_SplitCnfCleanup(int nParts)
{
char FileName[100]; int k;
for (k = 0; k < nParts; k++) {
sprintf(FileName, "%02d.cnf", k);
unlink(FileName);
}
}
void Cnf_SplitSat(char *pFileName, int iVarBeg, int iVarEnd, int nLits, int Value, int TimeOut, int nProcs, int nIters, int Seed, int fPrepro, int fVerbose)
{
abctime clk = Abc_Clock();
Vec_Int_t *vSol = NULL;
int i, Rand = 0;
if ( nIters == 0 )
nIters = ABC_INFINITY;
Abc_Random(1);
for ( i = 0; i < Seed; i++ )
Abc_Random(0);
Rand = Abc_Random(0);
for (i = 0; i < nIters && !vSol; i++)
{
abctime clk2 = Abc_Clock();
Cnf_SplitCnfFile(pFileName, nProcs, iVarBeg, iVarEnd, nLits, Value, Rand, fPrepro, fVerbose);
vSol = Cnf_RunSolver(nProcs, TimeOut, fVerbose);
Cnf_SplitCnfCleanup(nProcs);
if (fVerbose) {
printf( "Finished iteration %d. ", i);
Abc_PrintTime(0, "Time", Abc_Clock() - clk2);
}
}
printf("%solution is found. ", vSol ? "S" : "No s");
Abc_PrintTime(0, "Total time", Abc_Clock() - clk);
Vec_IntFreeP(&vSol);
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END