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

Adding support for the random seed to the recent experiments.

This commit is contained in:
Alan Mishchenko 2025-03-18 07:55:28 -07:00
parent 30c952ed22
commit 2078b3945b
4 changed files with 48 additions and 23 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

23
src/aig/gia/giaSatLut.c
View File

@ -1234,7 +1234,7 @@ void Gia_ManLutSat( Gia_Man_t * pGia, int LutSize, int nNumber, int nImproves, i
SeeAlso []
***********************************************************************/
Vec_Int_t * Gia_RunKadical( char * pFileNameIn, char * pFileNameOut, int nBTLimit, int TimeOut, int fVerbose, int * pStatus )
Vec_Int_t * Gia_RunKadical( char * pFileNameIn, char * pFileNameOut, int Seed, int nBTLimit, int TimeOut, int fVerbose, int * pStatus )
{
extern Vec_Int_t * Exa4_ManParse( char *pFileName );
int fVerboseSolver = 0;
@ -1244,19 +1244,24 @@ Vec_Int_t * Gia_RunKadical( char * pFileNameIn, char * pFileNameOut, int nBTLimi
char * pKadical = "kadical.exe";
#else
char * pKadical = "./kadical";
FILE * pFile = fopen( pKadical, "rb" );
if ( pFile == NULL )
pKadical += 2;
else
fclose( pFile );
#endif
char Command[1000], * pCommand = (char *)&Command;
if ( nBTLimit ) {
if ( TimeOut )
sprintf( pCommand, "%s -c %d -t %d %s %s > %s", pKadical, nBTLimit, TimeOut, fVerboseSolver ? "": "-q", pFileNameIn, pFileNameOut );
sprintf( pCommand, "%s --seed=%d -c %d -t %d %s %s > %s", pKadical, Seed, nBTLimit, TimeOut, fVerboseSolver ? "": "-q", pFileNameIn, pFileNameOut );
else
sprintf( pCommand, "%s -c %d %s %s > %s", pKadical, nBTLimit, fVerboseSolver ? "": "-q", pFileNameIn, pFileNameOut );
sprintf( pCommand, "%s --seed=%d -c %d %s %s > %s", pKadical, Seed, nBTLimit, fVerboseSolver ? "": "-q", pFileNameIn, pFileNameOut );
}
else {
if ( TimeOut )
sprintf( pCommand, "%s -t %d %s %s > %s", pKadical, TimeOut, fVerboseSolver ? "": "-q", pFileNameIn, pFileNameOut );
sprintf( pCommand, "%s --seed=%d -t %d %s %s > %s", pKadical, Seed, TimeOut, fVerboseSolver ? "": "-q", pFileNameIn, pFileNameOut );
else
sprintf( pCommand, "%s %s %s > %s", pKadical, fVerboseSolver ? "": "-q", pFileNameIn, pFileNameOut );
sprintf( pCommand, "%s --seed=%d %s %s > %s", pKadical, Seed, fVerboseSolver ? "": "-q", pFileNameIn, pFileNameOut );
}
#ifdef __wasm
if ( 1 )
@ -1564,7 +1569,7 @@ int Gia_ManDumpCnf2( Vec_Str_t * vStr, int nVars, int argc, char ** argv, abctim
fclose( pFile );
return 1;
}
int Gia_ManSimpleMapping( Gia_Man_t * p, int nBound, int nBTLimit, int nTimeout, int fVerbose, int fKeepFile, int argc, char ** argv )
int Gia_ManSimpleMapping( Gia_Man_t * p, int nBound, int Seed, int nBTLimit, int nTimeout, int fVerbose, int fKeepFile, int argc, char ** argv )
{
abctime clkStart = Abc_Clock();
srand(time(NULL));
@ -1582,7 +1587,7 @@ int Gia_ManSimpleMapping( Gia_Man_t * p, int nBound, int nBTLimit, int nTimeout,
if ( fVerbose )
printf( "SAT variables = %d. SAT clauses = %d. Cardinality bound = %d. Conflict limit = %d. Timeout = %d.\n",
nVars, Vec_StrCountEntry(vStr, '\n'), nBound, nBTLimit, nTimeout );
Vec_Int_t * vRes = Gia_RunKadical( pFileNameI, pFileNameO, nBTLimit, nTimeout, fVerbose, &Status );
Vec_Int_t * vRes = Gia_RunKadical( pFileNameI, pFileNameO, Seed, nBTLimit, nTimeout, fVerbose, &Status );
unlink( pFileNameI );
//unlink( pFileNameO );
if ( fKeepFile ) Gia_ManDumpCnf2( vStr, nVars, argc, argv, Abc_Clock() - clkStart, Status );
@ -2000,7 +2005,7 @@ word Gia_ManGetTruth( Gia_Man_t * p )
return Const[Gia_ObjFaninC0(pObj)] ^ pFuncs[Gia_ObjFaninId0p(p, pObj)];
}
Gia_Man_t * Gia_ManKSatMapping( word Truth, int nIns, int nNodes, int nBound, int fMultiLevel, int nBTLimit, int nTimeout, int fVerbose, int fKeepFile, int argc, char ** argv )
Gia_Man_t * Gia_ManKSatMapping( word Truth, int nIns, int nNodes, int nBound, int Seed, int fMultiLevel, int nBTLimit, int nTimeout, int fVerbose, int fKeepFile, int argc, char ** argv )
{
abctime clkStart = Abc_Clock();
Gia_Man_t * pNew = NULL;
@ -2017,7 +2022,7 @@ Gia_Man_t * Gia_ManKSatMapping( word Truth, int nIns, int nNodes, int nBound, in
if ( fVerbose )
printf( "Vars = %d. Nodes = %d. Cardinality bound = %d. SAT vars = %d. SAT clauses = %d. Conflict limit = %d. Timeout = %d.\n",
nIns, nNodes, nBound, nVars, Vec_StrCountEntry(vStr, '\n'), nBTLimit, nTimeout );
Vec_Int_t * vRes = Gia_RunKadical( pFileNameI, pFileNameO, nBTLimit, nTimeout, 1, &Status );
Vec_Int_t * vRes = Gia_RunKadical( pFileNameI, pFileNameO, Seed, nBTLimit, nTimeout, 1, &Status );
unlink( pFileNameI );
//unlink( pFileNameO );
if ( fKeepFile ) Gia_ManDumpCnf2( vStr, nVars, argc, argv, Abc_Clock() - clkStart, Status );

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

@ -44458,10 +44458,10 @@ usage:
int Abc_CommandAbc9Simap( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern void Mio_IntallSimpleLibrary();
extern int Gia_ManSimpleMapping( Gia_Man_t * p, int nBound, int nBTLimit, int nTimeout, int fVerbose, int fKeepFile, int argc, char ** argv );
int c, nBTLimit = 0, nBound = 0, nTimeout = 0, fKeepFile = 0, fVerbose = 0;
extern int Gia_ManSimpleMapping( Gia_Man_t * p, int nBound, int Seed, int nBTLimit, int nTimeout, int fVerbose, int fKeepFile, int argc, char ** argv );
int c, Seed = 0, nBTLimit = 0, nBound = 0, nTimeout = 0, fKeepFile = 0, fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "BCTfvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "BRCTfvh" ) ) != EOF )
{
switch ( c )
{
@ -44479,6 +44479,15 @@ int Abc_CommandAbc9Simap( Abc_Frame_t * pAbc, int argc, char ** argv )
goto usage;
}
break;
case 'R':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-R\" should be followed by an integer.\n" );
goto usage;
}
Seed = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
break;
case 'C':
if ( globalUtilOptind >= argc )
{
@ -44519,14 +44528,15 @@ int Abc_CommandAbc9Simap( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
}
Mio_IntallSimpleLibrary();
if ( !Gia_ManSimpleMapping( pAbc->pGia, nBound, nBTLimit, nTimeout, fVerbose, fKeepFile, argc, argv ) )
if ( !Gia_ManSimpleMapping( pAbc->pGia, nBound, Seed, nBTLimit, nTimeout, fVerbose, fKeepFile, argc, argv ) )
printf( "Simple mapping has failed.\n" );
return 0;
usage:
Abc_Print( -2, "usage: &simap [-BCT num] [-fvh]\n" );
Abc_Print( -2, "usage: &simap [-BRCT num] [-fvh]\n" );
Abc_Print( -2, "\t performs simple mapping of the AIG\n" );
Abc_Print( -2, "\t-B num : the bound on the solution size [default = %d]\n", nBound );
Abc_Print( -2, "\t-R num : random number generator seed [default = %d]\n", Seed );
Abc_Print( -2, "\t-C num : the conflict limit [default = %d]\n", nBTLimit );
Abc_Print( -2, "\t-T num : runtime limit in seconds [default = %d]\n", nTimeout );
Abc_Print( -2, "\t-f : toggles keeping the intermediate CNF file [default = %s]\n", fKeepFile? "yes": "no" );
@ -44549,11 +44559,11 @@ usage:
int Abc_CommandAbc9Exmap( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern void Mio_IntallSimpleLibrary2();
extern Gia_Man_t * Gia_ManKSatMapping( word Truth, int nIns, int nNodes, int nBound, int fMultiLevel, int nBTLimit, int nTimeout, int fVerbose, int fKeepFile, int argc, char ** argv );
extern Gia_Man_t * Gia_ManKSatMapping( word Truth, int nIns, int nNodes, int nBound, int Seed, int fMultiLevel, int nBTLimit, int nTimeout, int fVerbose, int fKeepFile, int argc, char ** argv );
Gia_Man_t * pTemp = NULL; char * pTruth = NULL; word Truth = 0;
int c, nVars = 0, nNodes = 0, nVars2, nBTLimit = 0, nBound = 0, fMultiLevel = 0, nTimeout = 0, fKeepFile = 0, fVerbose = 0;
int c, nVars = 0, nNodes = 0, nVars2, Seed = 0, nBTLimit = 0, nBound = 0, fMultiLevel = 0, nTimeout = 0, fKeepFile = 0, fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "NBCTmfvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "NBRCTmfvh" ) ) != EOF )
{
switch ( c )
{
@ -44585,6 +44595,15 @@ int Abc_CommandAbc9Exmap( Abc_Frame_t * pAbc, int argc, char ** argv )
goto usage;
}
break;
case 'R':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-R\" should be followed by an integer.\n" );
goto usage;
}
Seed = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
break;
case 'C':
if ( globalUtilOptind >= argc )
{
@ -44646,7 +44665,7 @@ int Abc_CommandAbc9Exmap( Abc_Frame_t * pAbc, int argc, char ** argv )
}
nVars2 = Abc_TtReadHex( &Truth, pTruth );
assert( nVars2 == nVars );
pTemp = Gia_ManKSatMapping( Truth, nVars, nNodes, nBound, fMultiLevel, nBTLimit, nTimeout, fVerbose, fKeepFile, argc, argv );
pTemp = Gia_ManKSatMapping( Truth, nVars, nNodes, nBound, Seed, fMultiLevel, nBTLimit, nTimeout, fVerbose, fKeepFile, argc, argv );
if ( pTemp ) {
//Mio_IntallSimpleLibrary2();
Abc_FrameUpdateGia( pAbc, pTemp );
@ -44654,10 +44673,11 @@ int Abc_CommandAbc9Exmap( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
Abc_Print( -2, "usage: &exmap [-NBCT num] [-mfvh] <truth>\n" );
Abc_Print( -2, "usage: &exmap [-NBRCT num] [-mfvh] <truth>\n" );
Abc_Print( -2, "\t performs simple mapping of the truth table\n" );
Abc_Print( -2, "\t-N num : the number of nodes [default = %d]\n", nNodes );
Abc_Print( -2, "\t-B num : the bound on the solution size [default = %d]\n", nBound );
Abc_Print( -2, "\t-R num : random number generator seed [default = %d]\n", Seed );
Abc_Print( -2, "\t-C num : the conflict limit [default = %d]\n", nBTLimit );
Abc_Print( -2, "\t-T num : runtime limit in seconds [default = %d]\n", nTimeout );
Abc_Print( -2, "\t-m : toggles using multi-level primitives [default = %s]\n", fMultiLevel? "yes": "no" );

4
src/opt/rar/rewire_map.c
View File

@ -33,7 +33,7 @@ extern void Nf_ManSetDefaultPars( Jf_Par_t * pPars );
extern Gia_Man_t * Nf_ManPerformMapping( Gia_Man_t * pGia, Jf_Par_t * pPars );
extern Abc_Ntk_t * Abc_NtkFromMappedGia( Gia_Man_t * p, int fFindEnables, int fUseBuffs );
extern Abc_Ntk_t * Abc_NtkFromCellMappedGia( Gia_Man_t * p, int fUseBuffs );
extern int Gia_ManSimpleMapping( Gia_Man_t * p, int nBound, int nBTLimit, int nTimeout, int fVerbose, int fKeepFile, int argc, char ** argv );
extern int Gia_ManSimpleMapping( Gia_Man_t * p, int nBound, int Seed, int nBTLimit, int nTimeout, int fVerbose, int fKeepFile, int argc, char ** argv );
Abc_Ntk_t *Gia_ManRewirePut(Gia_Man_t *pGia) {
Aig_Man_t *pMan = Gia_ManToAig(pGia, 0);
@ -67,7 +67,7 @@ Abc_Ntk_t *Gia_ManRewireMapNf(Gia_Man_t *pGia) {
}
Abc_Ntk_t *Gia_ManRewireMapSimap(Gia_Man_t *pGia, int nBound, int nBTLimit, int nTimeout) {
if (!Gia_ManSimpleMapping(pGia, nBound, nBTLimit, nTimeout, 0, 0, 0, NULL)) {
if (!Gia_ManSimpleMapping(pGia, nBound, 0, nBTLimit, nTimeout, 0, 0, 0, NULL)) {
// Abc_Print(-1, "Mapping has failed.\n");
return NULL;
}

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

@ -2280,7 +2280,7 @@ Mini_Aig_t * Exa4_ManMiniAig( Exa4_Man_t * p, Vec_Int_t * vValues, int fFancy )
***********************************************************************/
Mini_Aig_t * Exa4_ManGenTest( Vec_Wrd_t * vSimsIn, Vec_Wrd_t * vSimsOut, int nIns, int nDivs, int nOuts, int nNodes, int TimeOut, int fOnlyAnd, int fFancy, int fOrderNodes, int fUniqFans, int fVerbose, int fCard )
{
extern Vec_Int_t * Gia_RunKadical( char * pFileNameIn, char * pFileNameOut, int nBTLimit, int TimeOut, int fVerbose, int * pStatus );
extern Vec_Int_t * Gia_RunKadical( char * pFileNameIn, char * pFileNameOut, int Seed, int nBTLimit, int TimeOut, int fVerbose, int * pStatus );
Mini_Aig_t * pMini = NULL;
abctime clkTotal = Abc_Clock();
Vec_Int_t * vValues = NULL;
@ -2296,7 +2296,7 @@ Mini_Aig_t * Exa4_ManGenTest( Vec_Wrd_t * vSimsIn, Vec_Wrd_t * vSimsOut, int nIn
if ( fVerbose )
printf( "CNF with %d variables and %d clauses was dumped into file \"%s\".\n", p->nCnfVars, p->nCnfClauses, pFileNameIn );
if ( fCard )
vValues = Gia_RunKadical( pFileNameIn, pFileNameOut, 0, TimeOut, fVerbose, &Status );
vValues = Gia_RunKadical( pFileNameIn, pFileNameOut, 0, 0, TimeOut, fVerbose, &Status );
else
vValues = Exa4_ManSolve( pFileNameIn, pFileNameOut, TimeOut, fVerbose );
if ( vValues ) pMini = Exa4_ManMiniAig( p, vValues, fFancy );