diff options
Diffstat (limited to 'src/base/abci/abc.c')
-rw-r--r-- | src/base/abci/abc.c | 18 |
1 files changed, 12 insertions, 6 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 32ed17eb..ac0f26dd 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -17038,7 +17038,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 fVerbose ); + 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_NtkDarCec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int fPartition, int fVerbose ); pNtk = Abc_FrameReadNtk(pAbc); @@ -17143,7 +17143,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, fVerbose ); + Abc_NtkDSat( pNtk1, nConfLimit, nInsLimit, 0, 0, 0, fVerbose ); else Abc_NtkDarCec( pNtk1, pNtk2, nConfLimit, fPartition, fVerbose ); @@ -18250,20 +18250,22 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv ) int RetValue; int fAlignPol; int fAndOuts; + int fNewSolver; int fVerbose; int nConfLimit; int nInsLimit; int clk; - extern int Abc_NtkDSat( Abc_Ntk_t * pNtk, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fAlignPol, int fAndOuts, int fVerbose ); + extern int Abc_NtkDSat( Abc_Ntk_t * pNtk, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fAlignPol, int fAndOuts, int fNewSolver, int fVerbose ); // set defaults fAlignPol = 0; fAndOuts = 0; + fNewSolver = 0; fVerbose = 0; nConfLimit = 100000; nInsLimit = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "CIpavh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "CIpanvh" ) ) != EOF ) { switch ( c ) { @@ -18295,6 +18297,9 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'a': fAndOuts ^= 1; break; + case 'n': + fNewSolver ^= 1; + break; case 'v': fVerbose ^= 1; break; @@ -18329,7 +18334,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, fVerbose ); + RetValue = Abc_NtkDSat( pNtk, (ABC_INT64_T)nConfLimit, (ABC_INT64_T)nInsLimit, fAlignPol, fAndOuts, fNewSolver, fVerbose ); // verify that the pattern is correct if ( RetValue == 0 && Abc_NtkPoNum(pNtk) == 1 ) { @@ -18351,13 +18356,14 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: dsat [-C num] [-I num] [-pavh]\n" ); + Abc_Print( -2, "usage: dsat [-C num] [-I 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-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" ); Abc_Print( -2, "\t-v : prints verbose information [default = %s]\n", fVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); return 1; |