diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/base/abci/abc.c | 8 | ||||
| -rw-r--r-- | src/base/abci/abcExact.c | 8 |
2 files changed, 8 insertions, 8 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 9bb1c09a..953a6c6a 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -7295,7 +7295,7 @@ int Abc_CommandExact( Abc_Frame_t * pAbc, int argc, char ** argv ) { extern Gia_Man_t * Gia_ManFindExact( word * pTruth, int nVars, int nFunc, int nMaxDepth, int * pArrivalTimes, int nBTLimit, int nStartGates, int fVerbose ); - int c, nMaxDepth = -1, fMakeAIG = 0, fTest = 0, fVerbose = 0, nVars = 0, nVarsTmp, nFunc = 0, nStartGates = 1, nBTLimit = 100; + int c, nMaxDepth = -1, fMakeAIG = 0, fTest = 0, fVerbose = 0, nVars = 0, nVarsTmp, nFunc = 0, nStartGates = 1, nBTLimit = 400000; char * p1, * p2; word pTruth[64]; int pArrTimeProfile[8], fHasArrTimeProfile = 0; @@ -7423,7 +7423,7 @@ int Abc_CommandExact( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( pGiaRes ) Abc_FrameUpdateGia( pAbc, pGiaRes ); else - Abc_Print( 0, "Could not find AIG within given resource constraints.\n" ); + Abc_Print( 0, "Could not find AIG within given resource constraints, retry with different value for -C.\n" ); } else { @@ -7434,7 +7434,7 @@ int Abc_CommandExact( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_FrameClearVerifStatus( pAbc ); } else - Abc_Print( 0, "Could not find network within given resource constraints.\n" ); + Abc_Print( 0, "Could not find network within given resource constraints, retry with different value for -C.\n" ); } return 0; @@ -7444,7 +7444,7 @@ usage: Abc_Print( -2, "\t-D <num> : constrain maximum depth (if too low, algorithm may not terminate)\n" ); Abc_Print( -2, "\t-A <list> : input arrival times (comma separated list)\n" ); Abc_Print( -2, "\t-S <num> : number of start gates in search [default = %s]\n", nStartGates ); - Abc_Print( -2, "\t-C <num> : the limit on the number of conflicts [default = %d]\n", nBTLimit ); + Abc_Print( -2, "\t-C <num> : the limit on the number of conflicts; turn off with 0 [default = %d]\n", nBTLimit ); Abc_Print( -2, "\t-a : toggle create AIG [default = %s]\n", fMakeAIG ? "yes" : "no" ); Abc_Print( -2, "\t-t : run test suite\n" ); Abc_Print( -2, "\t-v : toggle verbose printout [default = %s]\n", fVerbose ? "yes" : "no" ); diff --git a/src/base/abci/abcExact.c b/src/base/abci/abcExact.c index 090b2d69..8052f982 100644 --- a/src/base/abci/abcExact.c +++ b/src/base/abci/abcExact.c @@ -2314,7 +2314,7 @@ static char * Ses_ManFindMinimumSizeTopDown( Ses_Man_t * pSes, int nMinGates ) static char * Ses_ManFindMinimumSize( Ses_Man_t * pSes ) { - char * pSol; + char * pSol = NULL; /* do the arrival times allow for a network? */ if ( pSes->nMaxDepth != -1 && pSes->pArrTimeProfile ) @@ -2326,7 +2326,7 @@ static char * Ses_ManFindMinimumSize( Ses_Man_t * pSes ) pSol = Ses_ManFindMinimumSizeBottomUp( pSes ); - if ( !pSol && pSes->fHitResLimit && pSes->nGates != pSes->nMaxGates ) + if ( !pSol && pSes->nMaxDepth != -1 && pSes->fHitResLimit && pSes->nGates != pSes->nMaxGates ) return Ses_ManFindMinimumSizeTopDown( pSes, pSes->nGates + 1 ); else return pSol; @@ -2360,8 +2360,8 @@ Abc_Ntk_t * Abc_NtkFindExact( word * pTruth, int nVars, int nFunc, int nMaxDepth pSes = Ses_ManAlloc( pTruth, nVars, nFunc, nMaxDepth, pArrTimeProfile, 0, nBTLimit, fVerbose ); pSes->nStartGates = nStartGates; - pSes->fReasonVerbose = 1; - pSes->fSatVerbose = 1; + pSes->fReasonVerbose = 0; + pSes->fSatVerbose = 0; if ( fVerbose ) Ses_ManPrintFuncs( pSes ); |