diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2014-06-04 17:45:15 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2014-06-04 17:45:15 -0700 |
| commit | c05aa7a8d2a78061bed22a4fd0be5cb88a4abadf (patch) | |
| tree | 2e0b450e9cd854ccf95f55f88f029ca7f1da36bc /src/proof/cec | |
| parent | 4875dfcb9b6a0c8d69e9a10221ed9472fb3231a0 (diff) | |
| download | abc-c05aa7a8d2a78061bed22a4fd0be5cb88a4abadf.tar.gz abc-c05aa7a8d2a78061bed22a4fd0be5cb88a4abadf.tar.bz2 abc-c05aa7a8d2a78061bed22a4fd0be5cb88a4abadf.zip | |
Adding CEC command &splitprove.
Diffstat (limited to 'src/proof/cec')
| -rw-r--r-- | src/proof/cec/cecSplit.c | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/proof/cec/cecSplit.c b/src/proof/cec/cecSplit.c index 078eed50..62b8f1a4 100644 --- a/src/proof/cec/cecSplit.c +++ b/src/proof/cec/cecSplit.c @@ -426,7 +426,7 @@ int Cec_GiaSplitTest2( Gia_Man_t * p, int nProcs, int nTimeOut, int nIterMax, in // get the last AIG Gia_Man_t * pLast = (Gia_Man_t *)Vec_PtrPop( vStack ); // determine cofactoring variable - int Depth = pLast->vCofVars ? Vec_IntSize(pLast->vCofVars) : 0; + int Depth = 1 + (pLast->vCofVars ? Vec_IntSize(pLast->vCofVars) : 0); int iVar = Gia_SplitCofVar( pLast, LookAhead ); // cofactor Gia_Man_t * pPart = Gia_ManDupCofactor( pLast, iVar, 0 ); @@ -441,7 +441,7 @@ int Cec_GiaSplitTest2( Gia_Man_t * p, int nProcs, int nTimeOut, int nIterMax, in status = Cnf_GiaSolveOne( pPart, pCnf, nTimeOut, &nSatVars, &nSatConfs ); Cnf_DataFree( pCnf ); if ( status == 1 ) - Progress += 1.0 / pow(2, Depth + 1); + Progress += 1.0 / pow(2, Depth); if ( fVerbose ) Cec_GiaSplitPrint( nIter, Depth, nSatVars, nSatConfs, status, Progress, Abc_Clock() - clkTotal ); if ( status == 0 ) // SAT @@ -468,7 +468,7 @@ int Cec_GiaSplitTest2( Gia_Man_t * p, int nProcs, int nTimeOut, int nIterMax, in status = Cnf_GiaSolveOne( pPart, pCnf, nTimeOut, &nSatVars, &nSatConfs ); Cnf_DataFree( pCnf ); if ( status == 1 ) - Progress += 1.0 / pow(2, Depth + 1); + Progress += 1.0 / pow(2, Depth); if ( fVerbose ) Cec_GiaSplitPrint( nIter, Depth, nSatVars, nSatConfs, status, Progress, Abc_Clock() - clkTotal ); if ( status == 0 ) // SAT @@ -568,7 +568,7 @@ int Cec_GiaSplitTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nIterMax, int pCnf = Cec_GiaDeriveGiaRemapped( p ); status = Cnf_GiaSolveOne( p, pCnf, nTimeOut, &nSatVars, &nSatConfs ); Cnf_DataFree( pCnf ); - if ( fVerbose ) + if ( fVerbose && status != -1 ) Cec_GiaSplitPrint( 0, 0, nSatVars, nSatConfs, status, Progress, Abc_Clock() - clkTotal ); if ( status == 0 ) { |