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 /src/base/abci/abcQbf.c | |
| 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'.
Diffstat (limited to 'src/base/abci/abcQbf.c')
| -rw-r--r-- | src/base/abci/abcQbf.c | 6 |
1 files changed, 3 insertions, 3 deletions
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 ); |