diff options
| -rw-r--r-- | src/base/abci/abc.c | 26 | ||||
| -rw-r--r-- | src/proof/cec/cecSplit.c | 13 |
2 files changed, 26 insertions, 13 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index d4dede6d..017e931a 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -32876,10 +32876,10 @@ usage: ***********************************************************************/ int Abc_CommandAbc9SplitProve( Abc_Frame_t * pAbc, int argc, char ** argv ) { - extern Gia_Man_t * Cec_GiaSplitTest( Gia_Man_t * p, int nTimeOut, int fVerbose ); - int c, nTimeOut = 1, fVerbose = 0; + extern Gia_Man_t * Cec_GiaSplitTest( Gia_Man_t * p, int nTimeOut, int nIterMax, int fVerbose ); + int c, nTimeOut = 1, nIterMax = 0, fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "Tvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "TIvh" ) ) != EOF ) { switch ( c ) { @@ -32894,6 +32894,17 @@ int Abc_CommandAbc9SplitProve( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( nTimeOut <= 0 ) goto usage; break; + case 'I': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-I\" should be followed by an integer.\n" ); + goto usage; + } + nIterMax = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nIterMax < 0 ) + goto usage; + break; case 'v': fVerbose ^= 1; break; @@ -32913,14 +32924,15 @@ int Abc_CommandAbc9SplitProve( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "Abc_CommandAbc9SplitProve(): The problem is sequential.\n" ); return 1; } - Cec_GiaSplitTest( pAbc->pGia, nTimeOut, fVerbose ); + Cec_GiaSplitTest( pAbc->pGia, nTimeOut, nIterMax, fVerbose ); return 0; usage: - Abc_Print( -2, "usage: &splitprove [-T num] [-vh]\n" ); + Abc_Print( -2, "usage: &splitprove [-TI num] [-vh]\n" ); Abc_Print( -2, "\t proves CEC problem by case-splitting\n" ); - Abc_Print( -2, "\t-T num : runtime limit in seconds per subproblem [default = %d]\n", nTimeOut ); - Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); + 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-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); return 1; } 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; } |