diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2014-06-04 11:40:37 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2014-06-04 11:40:37 -0700 |
| commit | 97bd9d8f1b1755422f65b288ee42a1d4ccb8b777 (patch) | |
| tree | c3ec6511d478279ecfbb3be4f875f2a8855f572e /src/proof/cec | |
| parent | d2c3971de071e0ac074f29bbfb35bac67cbe81fa (diff) | |
| download | abc-97bd9d8f1b1755422f65b288ee42a1d4ccb8b777.tar.gz abc-97bd9d8f1b1755422f65b288ee42a1d4ccb8b777.tar.bz2 abc-97bd9d8f1b1755422f65b288ee42a1d4ccb8b777.zip | |
Adding CEC command &splitprove.
Diffstat (limited to 'src/proof/cec')
| -rw-r--r-- | src/proof/cec/cecSplit.c | 13 |
1 files changed, 7 insertions, 6 deletions
diff --git a/src/proof/cec/cecSplit.c b/src/proof/cec/cecSplit.c index 7b33efc6..7ba3d51e 100644 --- a/src/proof/cec/cecSplit.c +++ b/src/proof/cec/cecSplit.c @@ -331,7 +331,7 @@ void Cec_GiaSplitPrint( int nIter, int Depth, int nVars, int nConfs, int fSatUns printf( "%6d : ", nIter ); printf( "Depth =%3d ", Depth ); printf( "SatVar =%7d ", nVars ); - printf( "SatConf =%7d ", nConfs ); + printf( "SatConf =%7d ", nConfs ); printf( "%s ", fSatUnsat ? "UNSAT " : "UNDECIDED" ); printf( "Progress = %.10f ", Prog ); Abc_PrintTime( 1, "Time", clk ); @@ -359,7 +359,7 @@ void Cec_GiaSplitPrintRefs( Gia_Man_t * p ) SeeAlso [] ***********************************************************************/ -int Cec_GiaSplitTest( Gia_Man_t * p, int nTimeOut, int fVerbose ) +int Cec_GiaSplitTest( Gia_Man_t * p, int nTimeOut, int nIterMax, int fVerbose ) { abctime clk, clkTotal = Abc_Clock(); Gia_Man_t * pPart0, * pPart1, * pLast; @@ -428,7 +428,7 @@ int Cec_GiaSplitTest( Gia_Man_t * p, int nTimeOut, int fVerbose ) Progress += 1.0 / pow(2, Depth + 1); if ( fVerbose ) Cec_GiaSplitPrint( nIter, Depth, nSatVars, nSatConfs, fSatUnsat, Progress, Abc_Clock() - clk ); - if ( Vec_PtrSize(vStack) > 3 ) + if ( nIterMax && Vec_PtrSize(vStack) >= nIterMax ) break; } if ( Vec_PtrSize(vStack) == 0 ) @@ -436,12 +436,13 @@ int Cec_GiaSplitTest( Gia_Man_t * p, int nTimeOut, int fVerbose ) } Cec_GiaSplitClean( vStack ); if ( RetValue == 0 ) - printf( "Problem is SAT " ); + printf( "Problem is SAT " ); else if ( RetValue == 1 ) - printf( "Problem is UNSAT " ); + printf( "Problem is UNSAT " ); else if ( RetValue == -1 ) - printf( "Problem is UNDECIDED " ); + printf( "Problem is UNDECIDED " ); else assert( 0 ); + printf( "after %d case-splits. ", nIter ); Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal ); return RetValue; } |