From adcc398bc38c91fa4cc8849aca9eb69c6fb61d21 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 26 Jun 2022 19:45:03 -0700 Subject: Dumping equivalences after SAT sweeping. --- src/base/abci/abc.c | 20 +++++++++++++++----- 1 file changed, 15 insertions(+), 5 deletions(-) (limited to 'src/base') diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index f1c8cc7f..33a8315c 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -37195,13 +37195,14 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv ) extern Gia_Man_t * Cec2_ManSimulateTest( Gia_Man_t * p, Cec_ParFra_t * pPars ); extern Gia_Man_t * Cec3_ManSimulateTest( Gia_Man_t * p, Cec_ParFra_t * pPars ); extern Gia_Man_t * Cec4_ManSimulateTest( Gia_Man_t * p, Cec_ParFra_t * pPars ); + extern void Cec4_ManSimulateTest5( Gia_Man_t * p, int nConfs, int fVerbose ); extern Gia_Man_t * Cec5_ManSimulateTest( Gia_Man_t * p, Cec_ParFra_t * pPars, int fCbs, int approxLim, int subBatchSz, int adaRecycle ); Cec_ParFra_t ParsFra, * pPars = &ParsFra; Gia_Man_t * pTemp; - int c, fUseAlgo = 0, fUseAlgoG = 0, fUseAlgoX = 0, fUseAlgoY = 0; + int c, fUseAlgo = 0, fUseAlgoG = 0, fUseAlgoX = 0, fUseAlgoY = 0, fUseSave = 0; int fCbs = 1, approxLim = 600, subBatchSz = 1, adaRecycle = 500; Cec4_ManSetParams( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "JWRILDCNPrmdckngxywvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "JWRILDCNPrmdckngxyswvh" ) ) != EOF ) { switch ( c ) { @@ -37331,6 +37332,9 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'y': fUseAlgoY ^= 1; break; + case 's': + fUseSave ^= 1; + break; case 'w': pPars->fVeryVerbose ^= 1; break; @@ -37346,7 +37350,12 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "Abc_CommandAbc9Fraig(): There is no AIG.\n" ); return 1; } - if ( fUseAlgo ) + if ( fUseSave ) + { + Cec4_ManSimulateTest5( pAbc->pGia, pPars->nBTLimit, pPars->fVerbose ); + return 0; + } + else if ( fUseAlgo ) pTemp = Cec2_ManSimulateTest( pAbc->pGia, pPars ); else if ( fUseAlgoG ) pTemp = Cec3_ManSimulateTest( pAbc->pGia, pPars ); @@ -37354,7 +37363,7 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv ) pTemp = Cec4_ManSimulateTest( pAbc->pGia, pPars ); else if ( fUseAlgoY ) pTemp = Cec5_ManSimulateTest( pAbc->pGia, pPars, fCbs, approxLim, subBatchSz, adaRecycle ); - else + else pTemp = Cec_ManSatSweeping( pAbc->pGia, pPars, 0 ); if ( pAbc->pGia->pCexSeq != NULL ) { @@ -37366,7 +37375,7 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: &fraig [-JWRILDCNP ] [-rmdckngxywvh]\n" ); + Abc_Print( -2, "usage: &fraig [-JWRILDCNP ] [-rmdckngxyswvh]\n" ); Abc_Print( -2, "\t performs combinational SAT sweeping\n" ); Abc_Print( -2, "\t-J num : the solver type [default = %d]\n", pPars->jType ); Abc_Print( -2, "\t-W num : the number of simulation words [default = %d]\n", pPars->nWords ); @@ -37386,6 +37395,7 @@ usage: Abc_Print( -2, "\t-g : toggle using another new implementation [default = %s]\n", fUseAlgoG? "yes": "no" ); Abc_Print( -2, "\t-x : toggle using another new implementation [default = %s]\n", fUseAlgoX? "yes": "no" ); Abc_Print( -2, "\t-y : toggle using another new implementation [default = %s]\n", fUseAlgoY? "yes": "no" ); + Abc_Print( -2, "\t-s : toggle dumping equivalences into a file [default = %s]\n", fUseSave? "yes": "no" ); Abc_Print( -2, "\t-w : toggle printing even more verbose information [default = %s]\n", pPars->fVeryVerbose? "yes": "no" ); Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); -- cgit v1.2.3