diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2013-04-28 01:25:29 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2013-04-28 01:25:29 -0700 |
| commit | b09926e8e26de8df20a3973a3c9a1c63b06952cb (patch) | |
| tree | cd38678012538f93611262f680e00d7f12a83ba4 /src/base/abci/abc.c | |
| parent | 17a0d944b305cbadeb2bbbcdd7ef3c82b50c3c7a (diff) | |
| download | abc-b09926e8e26de8df20a3973a3c9a1c63b06952cb.tar.gz abc-b09926e8e26de8df20a3973a3c9a1c63b06952cb.tar.bz2 abc-b09926e8e26de8df20a3973a3c9a1c63b06952cb.zip | |
SAT sweeping under constraints.
Diffstat (limited to 'src/base/abci/abc.c')
| -rw-r--r-- | src/base/abci/abc.c | 14 |
1 files changed, 10 insertions, 4 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index b15b5b04..0eba452d 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -27148,7 +27148,7 @@ int Abc_CommandAbc9CFraig( Abc_Frame_t * pAbc, int argc, char ** argv ) Ssc_Pars_t Pars, * pPars = &Pars; Ssc_ManSetDefaultParams( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "WCvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "WCavh" ) ) != EOF ) { switch ( c ) { @@ -27174,6 +27174,9 @@ int Abc_CommandAbc9CFraig( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( pPars->nBTLimit < 0 ) goto usage; break; + case 'a': + pPars->fAppend ^= 1; + break; case 'v': pPars->fVerbose ^= 1; break; @@ -27191,12 +27194,13 @@ int Abc_CommandAbc9CFraig( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: &cfraig [-WC <num>] [-rmdwvh]\n" ); + Abc_Print( -2, "usage: &cfraig [-WC <num>] [-avh]\n" ); Abc_Print( -2, "\t performs combinational SAT sweeping under constraints\n" ); Abc_Print( -2, "\t which are present in the AIG or set manually using \"constr\"\n" ); Abc_Print( -2, "\t (constraints are listed as last POs and true when they are 0)\n" ); Abc_Print( -2, "\t-W num : the number of simulation words [default = %d]\n", pPars->nWords ); Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit ); + Abc_Print( -2, "\t-a : toggle appending constraints to the result [default = %s]\n", pPars->fAppend? "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"); return 1; @@ -31513,7 +31517,8 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv ) // extern void Unr_ManTest( Gia_Man_t * pGia ); // extern void Mig_ManTest( Gia_Man_t * pGia ); // extern int Gia_ManVerify( Gia_Man_t * pGia ); - extern Gia_Man_t * Gia_SweeperFraigTest( Gia_Man_t * p, int nWords, int nConfs, int fVerbose ); +// extern Gia_Man_t * Gia_SweeperFraigTest( Gia_Man_t * p, int nWords, int nConfs, int fVerbose ); + extern Gia_Man_t * Gia_ManOptimizeRing( Gia_Man_t * p ); Extra_UtilGetoptReset(); while ( ( c = Extra_UtilGetopt( argc, argv, "svh" ) ) != EOF ) @@ -31565,7 +31570,8 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv ) // Unr_ManTest( pAbc->pGia ); // Mig_ManTest( pAbc->pGia ); // Gia_ManVerifyWithBoxes( pAbc->pGia ); - pTemp = Gia_SweeperFraigTest( pAbc->pGia, 4, 1000, 0 ); +// pTemp = Gia_SweeperFraigTest( pAbc->pGia, 4, 1000, 0 ); + pTemp = Gia_ManOptimizeRing( pAbc->pGia ); Abc_FrameUpdateGia( pAbc, pTemp ); return 0; usage: |