diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2012-07-09 19:24:39 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2012-07-09 19:24:39 -0700 |
commit | 637736827a770d32778c832802dd8c6ddee73073 (patch) | |
tree | 8edb5a7e81aa63b1ae82114ecbff801c61ed3934 /src/base | |
parent | 22dc4983740830d1b37a434f11af57c70e26ec7b (diff) | |
download | abc-637736827a770d32778c832802dd8c6ddee73073.tar.gz abc-637736827a770d32778c832802dd8c6ddee73073.tar.bz2 abc-637736827a770d32778c832802dd8c6ddee73073.zip |
Adding several command-line arguments to 'dsat'.
Diffstat (limited to 'src/base')
-rw-r--r-- | src/base/abci/abc.c | 54 | ||||
-rw-r--r-- | src/base/abci/abcDar.c | 6 | ||||
-rw-r--r-- | src/base/abci/abcIvy.c | 4 | ||||
-rw-r--r-- | src/base/abci/abcQbf.c | 4 |
4 files changed, 55 insertions, 13 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 9d06104d..daf265e8 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -17692,7 +17692,7 @@ int Abc_CommandDCec( Abc_Frame_t * pAbc, int argc, char ** argv ) int fPartition; int fMiter; - extern int Abc_NtkDSat( Abc_Ntk_t * pNtk, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fAlignPol, int fAndOuts, int fNewSolver, int fVerbose ); + extern int Abc_NtkDSat( Abc_Ntk_t * pNtk, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int nStartLearned, int nDeltaLearned, int nRatioLearned, int fAlignPol, int fAndOuts, int fNewSolver, int fVerbose ); extern int Abc_NtkDarCec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int fPartition, int fVerbose ); pNtk = Abc_FrameReadNtk(pAbc); @@ -17797,7 +17797,7 @@ int Abc_CommandDCec( Abc_Frame_t * pAbc, int argc, char ** argv ) // perform equivalence checking if ( fSat && fMiter ) - Abc_NtkDSat( pNtk1, nConfLimit, nInsLimit, 0, 0, 0, fVerbose ); + Abc_NtkDSat( pNtk1, nConfLimit, nInsLimit, 0, 0, 0, 0, 0, 0, fVerbose ); else Abc_NtkDarCec( pNtk1, pNtk2, nConfLimit, fPartition, fVerbose ); @@ -18943,10 +18943,13 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv ) int fNewSolver; int fVerbose; int nConfLimit; + int nStartLearned; + int nDeltaLearned; + int nRatioLearned; int nInsLimit; clock_t clk; - extern int Abc_NtkDSat( Abc_Ntk_t * pNtk, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fAlignPol, int fAndOuts, int fNewSolver, int fVerbose ); + extern int Abc_NtkDSat( Abc_Ntk_t * pNtk, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int nStartLearned, int nDeltaLearned, int nRatioLearned, int fAlignPol, int fAndOuts, int fNewSolver, int fVerbose ); // set defaults fAlignPol = 0; fAndOuts = 0; @@ -18954,8 +18957,11 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv ) fVerbose = 0; nConfLimit = 0; nInsLimit = 0; + nStartLearned = 0; + nDeltaLearned = 0; + nRatioLearned = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "CIpanvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "CISDRpanvh" ) ) != EOF ) { switch ( c ) { @@ -18981,6 +18987,39 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( nInsLimit < 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; + } + nStartLearned = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nStartLearned < 0 ) + goto usage; + break; + case 'D': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-D\" should be followed by an integer.\n" ); + goto usage; + } + nDeltaLearned = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nDeltaLearned < 0 ) + goto usage; + break; + case 'R': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-R\" should be followed by an integer.\n" ); + goto usage; + } + nRatioLearned = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nRatioLearned < 0 ) + goto usage; + break; case 'p': fAlignPol ^= 1; break; @@ -19024,7 +19063,7 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv ) } clk = clock(); - RetValue = Abc_NtkDSat( pNtk, (ABC_INT64_T)nConfLimit, (ABC_INT64_T)nInsLimit, fAlignPol, fAndOuts, fNewSolver, fVerbose ); + RetValue = Abc_NtkDSat( pNtk, (ABC_INT64_T)nConfLimit, (ABC_INT64_T)nInsLimit, nStartLearned, nDeltaLearned, nRatioLearned, fAlignPol, fAndOuts, fNewSolver, fVerbose ); // verify that the pattern is correct if ( RetValue == 0 && Abc_NtkPoNum(pNtk) == 1 ) { @@ -19046,11 +19085,14 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: dsat [-C num] [-I num] [-panvh]\n" ); + Abc_Print( -2, "usage: dsat [-CISDR num] [-panvh]\n" ); Abc_Print( -2, "\t solves the combinational miter using SAT solver MiniSat-1.14\n" ); Abc_Print( -2, "\t derives CNF from the current network and leave it unchanged\n" ); Abc_Print( -2, "\t-C num : limit on the number of conflicts [default = %d]\n", nConfLimit ); Abc_Print( -2, "\t-I num : limit on the number of inspections [default = %d]\n", nInsLimit ); + Abc_Print( -2, "\t-S num : starting value for learned clause removal [default = %d]\n", nStartLearned ); + Abc_Print( -2, "\t-D num : delta value for learned clause removal [default = %d]\n", nDeltaLearned ); + Abc_Print( -2, "\t-R num : ratio percentage for learned clause removal [default = %d]\n", nRatioLearned ); Abc_Print( -2, "\t-p : alighn polarity of SAT variables [default = %s]\n", fAlignPol? "yes": "no" ); Abc_Print( -2, "\t-a : toggle ANDing/ORing of miter outputs [default = %s]\n", fAndOuts? "ANDing": "ORing" ); Abc_Print( -2, "\t-n : toggle using new solver [default = %s]\n", fNewSolver? "yes": "no" ); diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c index 75df783f..82656d98 100644 --- a/src/base/abci/abcDar.c +++ b/src/base/abci/abcDar.c @@ -1403,7 +1403,7 @@ Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName, int fFastAlgo, SeeAlso [] ***********************************************************************/ -int Abc_NtkDSat( Abc_Ntk_t * pNtk, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fAlignPol, int fAndOuts, int fNewSolver, int fVerbose ) +int Abc_NtkDSat( Abc_Ntk_t * pNtk, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int nStartLearned, int nDeltaLearned, int nRatioLearned, int fAlignPol, int fAndOuts, int fNewSolver, int fVerbose ) { Aig_Man_t * pMan; int RetValue;//, clk = clock(); @@ -1411,7 +1411,7 @@ int Abc_NtkDSat( Abc_Ntk_t * pNtk, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit assert( Abc_NtkLatchNum(pNtk) == 0 ); // assert( Abc_NtkPoNum(pNtk) == 1 ); pMan = Abc_NtkToDar( pNtk, 0, 0 ); - RetValue = Fra_FraigSat( pMan, nConfLimit, nInsLimit, fAlignPol, fAndOuts, fNewSolver, fVerbose ); + RetValue = Fra_FraigSat( pMan, nConfLimit, nInsLimit, nStartLearned, nDeltaLearned, nRatioLearned, fAlignPol, fAndOuts, fNewSolver, fVerbose ); pNtk->pModel = (int *)pMan->pData, pMan->pData = NULL; Aig_ManStop( pMan ); return RetValue; @@ -2056,7 +2056,7 @@ int Abc_NtkDarBmcInter_int( Aig_Man_t * pMan, Inter_ManParams_t * pPars, Aig_Man if ( Aig_ManRegNum(pTemp) == 0 ) { pTemp->pSeqModel = NULL; - RetValue = Fra_FraigSat( pTemp, pPars->nBTLimit, 0, 0, 0, 0, 0 ); + RetValue = Fra_FraigSat( pTemp, pPars->nBTLimit, 0, 0, 0, 0, 0, 0, 0, 0 ); if ( pTemp->pData ) pTemp->pSeqModel = Abc_CexCreate( Aig_ManRegNum(pMan), Saig_ManPiNum(pMan), (int *)pTemp->pData, 0, i, 1 ); // pNtk->pModel = pTemp->pData, pTemp->pData = NULL; diff --git a/src/base/abci/abcIvy.c b/src/base/abci/abcIvy.c index 2d53a1ee..ae75e9fc 100644 --- a/src/base/abci/abcIvy.c +++ b/src/base/abci/abcIvy.c @@ -533,7 +533,7 @@ int Abc_NtkIvyProve( Abc_Ntk_t ** ppNtk, void * pPars ) // if SAT only, solve without iteration // RetValue = Abc_NtkMiterSat( pNtk, 2*(ABC_INT64_T)pParams->nMiteringLimitStart, (ABC_INT64_T)0, 0, NULL, NULL ); pMan2 = Abc_NtkToDar( pNtk, 0, 0 ); - RetValue = Fra_FraigSat( pMan2, (ABC_INT64_T)pParams->nMiteringLimitStart, (ABC_INT64_T)0, 1, 0, 0, 0 ); + RetValue = Fra_FraigSat( pMan2, (ABC_INT64_T)pParams->nMiteringLimitStart, (ABC_INT64_T)0, 0, 0, 0, 1, 0, 0, 0 ); pNtk->pModel = (int *)pMan2->pData, pMan2->pData = NULL; Aig_ManStop( pMan2 ); // pNtk->pModel = Aig_ManReleaseData( pMan2 ); @@ -583,7 +583,7 @@ int Abc_NtkIvyProve( Abc_Ntk_t ** ppNtk, void * pPars ) Ioa_WriteAiger( pMan2, pFileName, 0, 0 ); printf( "Intermediate reduced miter is written into file \"%s\".\n", pFileName ); } - RetValue = Fra_FraigSat( pMan2, pParams->nMiteringLimitLast, 0, 0, 0, 0, pParams->fVerbose ); + RetValue = Fra_FraigSat( pMan2, pParams->nMiteringLimitLast, 0, 0, 0, 0, 0, 0, 0, pParams->fVerbose ); pNtk->pModel = (int *)pMan2->pData, pMan2->pData = NULL; Aig_ManStop( pMan2 ); } diff --git a/src/base/abci/abcQbf.c b/src/base/abci/abcQbf.c index 0b53bc8a..a77ddf94 100644 --- a/src/base/abci/abcQbf.c +++ b/src/base/abci/abcQbf.c @@ -41,7 +41,7 @@ static void Abc_NtkVectorClearVars( Abc_Ntk_t * pNtk, Vec_Int_t * vPiValues, int static void Abc_NtkVectorPrintPars( Vec_Int_t * vPiValues, int nPars ); static void Abc_NtkVectorPrintVars( Abc_Ntk_t * pNtk, Vec_Int_t * vPiValues, int nPars ); -extern int Abc_NtkDSat( Abc_Ntk_t * pNtk, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fAlignPol, int fAndOuts, int fNewSolver, int fVerbose ); +extern int Abc_NtkDSat( Abc_Ntk_t * pNtk, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int nStartLearned, int nDeltaLearned, int nRatioLearned, int fAlignPol, int fAndOuts, int fNewSolver, int fVerbose ); //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// @@ -101,7 +101,7 @@ void Abc_NtkQbf( Abc_Ntk_t * pNtk, int nPars, int nItersMax, int fVerbose ) // solve the synthesis instance clkS = clock(); // RetValue = Abc_NtkMiterSat( pNtkSyn, 0, 0, 0, NULL, NULL ); - RetValue = Abc_NtkDSat( pNtkSyn, (ABC_INT64_T)0, (ABC_INT64_T)0, 1, 0, 0, 0 ); + RetValue = Abc_NtkDSat( pNtkSyn, (ABC_INT64_T)0, (ABC_INT64_T)0, 0, 0, 0, 1, 0, 0, 0 ); clkS = clock() - clkS; if ( RetValue == 0 ) Abc_NtkModelToVector( pNtkSyn, vPiValues ); |