diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2013-03-27 12:51:57 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2013-03-27 12:51:57 -0700 |
| commit | 272089221a530f61bceee07378cb747c88471b70 (patch) | |
| tree | 163bdb928740d3999775c04d9d0aadd348b2be82 | |
| parent | e64cad10e2f9417247cb7f212d9bc434902bd154 (diff) | |
| download | abc-272089221a530f61bceee07378cb747c88471b70.tar.gz abc-272089221a530f61bceee07378cb747c88471b70.tar.bz2 abc-272089221a530f61bceee07378cb747c88471b70.zip | |
Removing hard-coded limit on the number of solving iterations in command 'qbf'.
| -rw-r--r-- | src/base/abci/abc.c | 6 | ||||
| -rw-r--r-- | src/base/abci/abcQbf.c | 6 |
2 files changed, 6 insertions, 6 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 69ab229f..cd77c98d 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -11564,9 +11564,9 @@ int Abc_CommandQbf( Abc_Frame_t * pAbc, int argc, char ** argv ) extern void Abc_NtkQbf( Abc_Ntk_t * pNtk, int nPars, int nIters, int fVerbose ); // set defaults - nPars = -1; - nIters = -1; - fVerbose = 1; + nPars = -1; + nIters = 500; + fVerbose = 1; Extra_UtilGetoptReset(); while ( ( c = Extra_UtilGetopt( argc, argv, "PIvh" ) ) != EOF ) { diff --git a/src/base/abci/abcQbf.c b/src/base/abci/abcQbf.c index 86755433..abbcc172 100644 --- a/src/base/abci/abcQbf.c +++ b/src/base/abci/abcQbf.c @@ -65,7 +65,7 @@ void Abc_NtkQbf( Abc_Ntk_t * pNtk, int nPars, int nItersMax, int fVerbose ) Abc_Ntk_t * pNtkVer, * pNtkSyn, * pNtkSyn2, * pNtkTemp; Vec_Int_t * vPiValues; clock_t clkTotal = clock(), clkS, clkV; - int nIters, nIterMax = 500, nInputs, RetValue, fFound = 0; + int nIters, nInputs, RetValue, fFound = 0; assert( Abc_NtkIsStrash(pNtk) ); assert( Abc_NtkIsComb(pNtk) ); @@ -96,7 +96,7 @@ void Abc_NtkQbf( Abc_Ntk_t * pNtk, int nPars, int nItersMax, int fVerbose ) } // iteratively solve - for ( nIters = 0; nIters < nIterMax; nIters++ ) + for ( nIters = 0; nIters < nItersMax; nIters++ ) { // solve the synthesis instance clkS = clock(); @@ -170,7 +170,7 @@ clkV = clock() - clkV; printf( "\n" ); printf( "Solved after %d interations. ", nIters ); } - else if ( nIters == nIterMax ) + else if ( nIters == nItersMax ) printf( "Unsolved after %d interations. ", nIters ); else if ( nIters == nItersMax ) printf( "Quit after %d interatios. ", nItersMax ); |