From 2078b3945b8b7743ebda76494c5daffa46cacf46 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Tue, 18 Mar 2025 07:55:28 -0700 Subject: [PATCH] Adding support for the random seed to the recent experiments. --- src/aig/gia/giaSatLut.c | 23 ++++++++++++++--------- src/base/abci/abc.c | 40 ++++++++++++++++++++++++++++++---------- src/opt/rar/rewire_map.c | 4 ++-- src/sat/bmc/bmcMaj.c | 4 ++-- 4 files changed, 48 insertions(+), 23 deletions(-) diff --git a/src/aig/gia/giaSatLut.c b/src/aig/gia/giaSatLut.c index ee63d77ad..df92030b9 100644 --- a/src/aig/gia/giaSatLut.c +++ b/src/aig/gia/giaSatLut.c @@ -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 ); diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 0da06dba9..0e898d63c 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -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] \n" ); + Abc_Print( -2, "usage: &exmap [-NBRCT num] [-mfvh] \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" ); diff --git a/src/opt/rar/rewire_map.c b/src/opt/rar/rewire_map.c index 47621de71..b63da077b 100644 --- a/src/opt/rar/rewire_map.c +++ b/src/opt/rar/rewire_map.c @@ -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; } diff --git a/src/sat/bmc/bmcMaj.c b/src/sat/bmc/bmcMaj.c index 998215ae9..ca11102bf 100644 --- a/src/sat/bmc/bmcMaj.c +++ b/src/sat/bmc/bmcMaj.c @@ -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 );