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

Adding CEC command &splitprove.

This commit is contained in:
Alan Mishchenko 2014-06-04 11:40:37 -07:00
parent d2c3971de0
commit 97bd9d8f1b
2 changed files with 26 additions and 13 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

26
src/base/abci/abc.c
View File

@ -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;
}

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

@ -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;
}