diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2018-01-27 13:05:37 -0800 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2018-01-27 13:05:37 -0800 |
commit | 5158acb113586d17895cc32e8d71e12c06705eb5 (patch) | |
tree | ec035afddd4cb5f2392e41680cfa7ba6f95e7329 /src/base/abci/abc.c | |
parent | e4cd0d60f1d2ecf8563c22b51519f3da0125d3be (diff) | |
download | abc-5158acb113586d17895cc32e8d71e12c06705eb5.tar.gz abc-5158acb113586d17895cc32e8d71e12c06705eb5.tar.bz2 abc-5158acb113586d17895cc32e8d71e12c06705eb5.zip |
Experiments with circuit-based SAT.
Diffstat (limited to 'src/base/abci/abc.c')
-rw-r--r-- | src/base/abci/abc.c | 19 |
1 files changed, 15 insertions, 4 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 0c2b72ec..67854f1a 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -33640,13 +33640,14 @@ usage: ***********************************************************************/ int Abc_CommandAbc9Sat( Abc_Frame_t * pAbc, int argc, char ** argv ) { + extern Vec_Int_t * Cbs2_ManSolveMiterNc( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvStatus, int fVerbose ); Cec_ParSat_t ParsSat, * pPars = &ParsSat; Gia_Man_t * pTemp; int c; - int fCSat = 0; + int fNewSolver = 0, fCSat = 0; Cec_ManSatSetDefaultParams( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "CSNnmtcvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "CSNanmtcvh" ) ) != EOF ) { switch ( c ) { @@ -33683,6 +33684,9 @@ int Abc_CommandAbc9Sat( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( pPars->nCallsRecycle < 0 ) goto usage; break; + case 'a': + fNewSolver ^= 1; + break; case 'n': pPars->fNonChrono ^= 1; break; @@ -33711,7 +33715,9 @@ int Abc_CommandAbc9Sat( Abc_Frame_t * pAbc, int argc, char ** argv ) { Vec_Int_t * vCounters; Vec_Str_t * vStatus; - if ( pPars->fLearnCls ) + if ( fNewSolver ) + vCounters = Cbs2_ManSolveMiterNc( pAbc->pGia, pPars->nBTLimit, &vStatus, pPars->fVerbose ); + else if ( pPars->fLearnCls ) vCounters = Tas_ManSolveMiterNc( pAbc->pGia, pPars->nBTLimit, &vStatus, pPars->fVerbose ); else if ( pPars->fNonChrono ) vCounters = Cbs_ManSolveMiterNc( pAbc->pGia, pPars->nBTLimit, &vStatus, pPars->fVerbose ); @@ -33728,11 +33734,12 @@ int Abc_CommandAbc9Sat( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: &sat [-CSN <num>] [-nmctvh]\n" ); + Abc_Print( -2, "usage: &sat [-CSN <num>] [-anmctvh]\n" ); Abc_Print( -2, "\t performs SAT solving for the combinational outputs\n" ); Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit ); Abc_Print( -2, "\t-S num : the min number of variables to recycle the solver [default = %d]\n", pPars->nSatVarMax ); Abc_Print( -2, "\t-N num : the min number of calls to recycle the solver [default = %d]\n", pPars->nCallsRecycle ); + Abc_Print( -2, "\t-a : toggle using new solver [default = %s]\n", fNewSolver? "yes": "no" ); Abc_Print( -2, "\t-n : toggle using non-chronological backtracking [default = %s]\n", pPars->fNonChrono? "yes": "no" ); Abc_Print( -2, "\t-m : toggle miter vs. any circuit [default = %s]\n", pPars->fCheckMiter? "miter": "circuit" ); Abc_Print( -2, "\t-c : toggle using circuit-based SAT solver [default = %s]\n", fCSat? "yes": "no" ); @@ -44856,6 +44863,7 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv ) // Gia_ParTest( pAbc->pGia, nWords, nProcs ); // Gia_StoComputeCuts( pAbc->pGia ); // printf( "\nThis command is currently disabled.\n\n" ); +/* { char Buffer[10]; extern void Gia_DumpLutSizeDistrib( Gia_Man_t * p, char * pFileName ); @@ -44863,6 +44871,9 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( pAbc->pGia ) Gia_DumpLutSizeDistrib( pAbc->pGia, Buffer ); } +*/ +// pTemp = Slv_ManToAig( pAbc->pGia ); +// Abc_FrameUpdateGia( pAbc, pTemp ); return 0; usage: Abc_Print( -2, "usage: &test [-FW num] [-svh]\n" ); |