From dc92f89278b17ad61407234a9159ffabc9c81e9e Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sat, 14 Mar 2015 03:13:05 +0700 Subject: Adding silent mode to &splitprove. --- src/base/abci/abc.c | 14 +++++++++----- src/proof/cec/cecSplit.c | 31 +++++++++++++++++-------------- src/sat/bmc/bmcFault.c | 8 +++++++- 3 files changed, 33 insertions(+), 20 deletions(-) diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index e28e5e7d..0aaee0f3 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -35609,10 +35609,10 @@ usage: ***********************************************************************/ int Abc_CommandAbc9SplitProve( Abc_Frame_t * pAbc, int argc, char ** argv ) { - extern int Cec_GiaSplitTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nIterMax, int LookAhead, int fVerbose, int fVeryVerbose ); - int c, nProcs = 1, nTimeOut = 10, nIterMax = 0, LookAhead = 1, fVerbose = 0, fVeryVerbose = 0; + extern int Cec_GiaSplitTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nIterMax, int LookAhead, int fVerbose, int fVeryVerbose, int fSilent ); + int c, nProcs = 1, nTimeOut = 10, nIterMax = 0, LookAhead = 1, fVerbose = 0, fVeryVerbose = 0, fSilent = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "PTILvwh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "PTILsvwh" ) ) != EOF ) { switch ( c ) { @@ -35663,6 +35663,9 @@ int Abc_CommandAbc9SplitProve( Abc_Frame_t * pAbc, int argc, char ** argv ) goto usage; } break; + case 's': + fSilent ^= 1; + break; case 'v': fVerbose ^= 1; break; @@ -35685,17 +35688,18 @@ int Abc_CommandAbc9SplitProve( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "Abc_CommandAbc9SplitProve(): The problem is sequential.\n" ); return 1; } - pAbc->Status = Cec_GiaSplitTest( pAbc->pGia, nProcs, nTimeOut, nIterMax, LookAhead, fVerbose, fVeryVerbose ); + pAbc->Status = Cec_GiaSplitTest( pAbc->pGia, nProcs, nTimeOut, nIterMax, LookAhead, fVerbose, fVeryVerbose, fSilent ); pAbc->pCex = pAbc->pGia->pCexComb; pAbc->pGia->pCexComb = NULL; return 0; usage: - Abc_Print( -2, "usage: &splitprove [-PTIL num] [-vwh]\n" ); + Abc_Print( -2, "usage: &splitprove [-PTIL num] [-svwh]\n" ); Abc_Print( -2, "\t proves CEC problem by case-splitting\n" ); Abc_Print( -2, "\t-P num : the number of concurrent processes [default = %d]\n", nProcs ); Abc_Print( -2, "\t-T num : runtime limit in seconds per subproblem [default = %d]\n", nTimeOut ); Abc_Print( -2, "\t-I num : the max number of iterations (0 = infinity) [default = %d]\n", nIterMax ); Abc_Print( -2, "\t-L num : maximum look-ahead during cofactoring [default = %d]\n", LookAhead ); + Abc_Print( -2, "\t-s : enable silent computation (no reporting) [default = %s]\n", fSilent? "yes": "no" ); Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); Abc_Print( -2, "\t-w : toggle printing more verbose information [default = %s]\n", fVeryVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); diff --git a/src/proof/cec/cecSplit.c b/src/proof/cec/cecSplit.c index 0984c234..ef6dea93 100644 --- a/src/proof/cec/cecSplit.c +++ b/src/proof/cec/cecSplit.c @@ -46,7 +46,7 @@ ABC_NAMESPACE_IMPL_START #ifndef ABC_USE_PTHREADS -int Cec_GiaSplitTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nIterMax, int LookAhead, int fVerbose, int fVeryVerbose ) { return -1; } +int Cec_GiaSplitTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nIterMax, int LookAhead, int fVerbose, int fVeryVerbose, int fSilent ) { return -1; } #else // pthreads are used @@ -564,7 +564,7 @@ void * Cec_GiaSplitWorkerThread( void * pArg ) assert( 0 ); return NULL; } -int Cec_GiaSplitTestInt( Gia_Man_t * p, int nProcs, int nTimeOut, int nIterMax, int LookAhead, int fVerbose, int fVeryVerbose ) +int Cec_GiaSplitTestInt( Gia_Man_t * p, int nProcs, int nTimeOut, int nIterMax, int LookAhead, int fVerbose, int fVeryVerbose, int fSilent ) { abctime clkTotal = Abc_Clock(); Par_ThData_t ThData[PAR_THR_MAX]; @@ -715,19 +715,22 @@ finish: } // finish Cec_GiaSplitClean( vStack ); - if ( RetValue == 0 ) - printf( "Problem is SAT " ); - else if ( RetValue == 1 ) - printf( "Problem is UNSAT " ); - else if ( RetValue == -1 ) - printf( "Problem is UNDECIDED " ); - else assert( 0 ); - printf( "after %d case-splits. ", nIter ); - Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal ); - fflush( stdout ); + if ( !fSilent ) + { + if ( RetValue == 0 ) + printf( "Problem is SAT " ); + else if ( RetValue == 1 ) + printf( "Problem is UNSAT " ); + else if ( RetValue == -1 ) + printf( "Problem is UNDECIDED " ); + else assert( 0 ); + printf( "after %d case-splits. ", nIter ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal ); + fflush( stdout ); + } return RetValue; } -int Cec_GiaSplitTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nIterMax, int LookAhead, int fVerbose, int fVeryVerbose ) +int Cec_GiaSplitTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nIterMax, int LookAhead, int fVerbose, int fVeryVerbose, int fSilent ) { Abc_Cex_t * pCex = NULL; Gia_Man_t * pOne; @@ -739,7 +742,7 @@ int Cec_GiaSplitTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nIterMax, int pOne = Gia_ManDupOutputGroup( p, i, i+1 ); if ( fVerbose ) printf( "\nSolving output %d:\n", i ); - RetValue1 = Cec_GiaSplitTestInt( pOne, nProcs, nTimeOut, nIterMax, LookAhead, fVerbose, fVeryVerbose ); + RetValue1 = Cec_GiaSplitTestInt( pOne, nProcs, nTimeOut, nIterMax, LookAhead, fVerbose, fVeryVerbose, fSilent ); Gia_ManStop( pOne ); // collect the result if ( RetValue1 == 0 && RetValue == -1 ) diff --git a/src/sat/bmc/bmcFault.c b/src/sat/bmc/bmcFault.c index 7a2a57fb..4912d82c 100644 --- a/src/sat/bmc/bmcFault.c +++ b/src/sat/bmc/bmcFault.c @@ -674,12 +674,18 @@ void Gia_ManPrintResults( Gia_Man_t * p, sat_solver * pSat, int nIter, abctime c ***********************************************************************/ int Gia_ManFaultAddOne( Gia_Man_t * pM, Cnf_Dat_t * pCnf, sat_solver * pSat, Vec_Int_t * vLits, int nFuncVars ) { - Gia_Man_t * pC; + Gia_Man_t * pC;//, * pTemp; Cnf_Dat_t * pCnf2; Gia_Obj_t * pObj; int i, Lit; // derive the cofactor pC = Gia_ManFaultCofactor( pM, vLits ); + // try synthesis +// printf( "\n" ); +// Gia_ManPrintStats( pC, NULL ); +// pC = Gia_ManAigSyn2( pTemp = pC, 0, 1, 0, 100, 0, 0, 0 ); +// Gia_ManStop( pTemp ); +// Gia_ManPrintStats( pC, NULL ); //Gia_AigerWrite( pC, "fftest_cof.aig", 0, 0 ); //printf( "Dumped cofactor circuit into file \"%s\".\n", "fftest_cof.aig" ); // derive new CNF -- cgit v1.2.3