luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Adding silent mode to &splitprove.

This commit is contained in:
Alan Mishchenko 2015-03-14 13:22:02 +07:00
parent dc92f89278
commit e89fe16b91
1 changed files with 19 additions and 12 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

11
src/proof/cec/cecSplit.c
View File

@ -403,7 +403,7 @@ void Cec_GiaSplitPrintRefs( Gia_Man_t * p )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
int Cec_GiaSplitTest2( Gia_Man_t * p, int nProcs, int nTimeOut, int nIterMax, int LookAhead, int fVerbose, int fVeryVerbose ) int Cec_GiaSplitTest2( Gia_Man_t * p, int nProcs, int nTimeOut, int nIterMax, int LookAhead, int fVerbose, int fVeryVerbose, int fSilent )
{ {
abctime clkTotal = Abc_Clock(); abctime clkTotal = Abc_Clock();
Vec_Ptr_t * vStack; Vec_Ptr_t * vStack;
@ -419,11 +419,13 @@ int Cec_GiaSplitTest2( Gia_Man_t * p, int nProcs, int nTimeOut, int nIterMax, in
Cec_GiaSplitPrint( 0, 0, nSatVars, nSatConfs, status, Progress, Abc_Clock() - clkTotal ); Cec_GiaSplitPrint( 0, 0, nSatVars, nSatConfs, status, Progress, Abc_Clock() - clkTotal );
if ( status == 0 ) if ( status == 0 )
{ {
if ( !fSilent )
printf( "The problem is SAT without cofactoring.\n" ); printf( "The problem is SAT without cofactoring.\n" );
return 0; return 0;
} }
if ( status == 1 ) if ( status == 1 )
{ {
if ( !fSilent )
printf( "The problem is UNSAT without cofactoring.\n" ); printf( "The problem is UNSAT without cofactoring.\n" );
return 1; return 1;
} }
@ -508,6 +510,8 @@ int Cec_GiaSplitTest2( Gia_Man_t * p, int nProcs, int nTimeOut, int nIterMax, in
RetValue = 1; RetValue = 1;
// finish // finish
Cec_GiaSplitClean( vStack ); Cec_GiaSplitClean( vStack );
if ( !fSilent )
{
if ( RetValue == 0 ) if ( RetValue == 0 )
printf( "Problem is SAT " ); printf( "Problem is SAT " );
else if ( RetValue == 1 ) else if ( RetValue == 1 )
@ -518,6 +522,7 @@ int Cec_GiaSplitTest2( Gia_Man_t * p, int nProcs, int nTimeOut, int nIterMax, in
printf( "after %d case-splits. ", nIter ); printf( "after %d case-splits. ", nIter );
Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal ); Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal );
fflush( stdout ); fflush( stdout );
}
return RetValue; return RetValue;
} }
@ -581,7 +586,7 @@ int Cec_GiaSplitTestInt( Gia_Man_t * p, int nProcs, int nTimeOut, int nIterMax,
printf( "Processes = %d TimeOut = %d sec MaxIter = %d LookAhead = %d Verbose = %d.\n", nProcs, nTimeOut, nIterMax, LookAhead, fVerbose ); printf( "Processes = %d TimeOut = %d sec MaxIter = %d LookAhead = %d Verbose = %d.\n", nProcs, nTimeOut, nIterMax, LookAhead, fVerbose );
fflush( stdout ); fflush( stdout );
if ( nProcs == 1 ) if ( nProcs == 1 )
return Cec_GiaSplitTest2( p, nProcs, nTimeOut, nIterMax, LookAhead, fVerbose, fVeryVerbose ); return Cec_GiaSplitTest2( p, nProcs, nTimeOut, nIterMax, LookAhead, fVerbose, fVeryVerbose, fSilent );
// subtract manager thread // subtract manager thread
nProcs--; nProcs--;
assert( nProcs >= 1 && nProcs <= PAR_THR_MAX ); assert( nProcs >= 1 && nProcs <= PAR_THR_MAX );
@ -593,11 +598,13 @@ int Cec_GiaSplitTestInt( Gia_Man_t * p, int nProcs, int nTimeOut, int nIterMax,
Cec_GiaSplitPrint( 0, 0, nSatVars, nSatConfs, status, Progress, Abc_Clock() - clkTotal ); Cec_GiaSplitPrint( 0, 0, nSatVars, nSatConfs, status, Progress, Abc_Clock() - clkTotal );
if ( status == 0 ) if ( status == 0 )
{ {
if ( !fSilent )
printf( "The problem is SAT without cofactoring.\n" ); printf( "The problem is SAT without cofactoring.\n" );
return 0; return 0;
} }
if ( status == 1 ) if ( status == 1 )
{ {
if ( !fSilent )
printf( "The problem is UNSAT without cofactoring.\n" ); printf( "The problem is UNSAT without cofactoring.\n" );
return 1; return 1;
} }