diff options
Diffstat (limited to 'src/base/abci')
-rw-r--r-- | src/base/abci/abc.c | 85 |
1 files changed, 73 insertions, 12 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 5c66958f..b8b5f5c4 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -2447,13 +2447,16 @@ usage: ***********************************************************************/ int Abc_CommandPrintStatus( Abc_Frame_t * pAbc, int argc, char ** argv ) { - int c; + int c, fShort = 1; // set defaults Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "sh" ) ) != EOF ) { switch ( c ) { + case 's': + fShort ^= 1; + break; case 'h': goto usage; default: @@ -2492,16 +2495,26 @@ int Abc_CommandPrintStatus( Abc_Frame_t * pAbc, int argc, char ** argv ) } if ( pAbc->vStatuses ) { - int i, Entry; - Vec_IntForEachEntry( pAbc->vStatuses, Entry, i ) - printf( "%d=%d ", i, Entry ); + if ( fShort ) + { + printf( "Status array contains %d SAT, %d UNSAT, and %d UNDEC entries (out of %d).", + Vec_IntCountEntry(pAbc->vStatuses, 0), Vec_IntCountEntry(pAbc->vStatuses, 1), + Vec_IntCountEntry(pAbc->vStatuses, -1), Vec_IntSize(pAbc->vStatuses) ); + } + else + { + int i, Entry; + Vec_IntForEachEntry( pAbc->vStatuses, Entry, i ) + printf( "%d=%d ", i, Entry ); + } printf( "\n" ); } return 0; usage: - Abc_Print( -2, "usage: print_status [-h]\n" ); + Abc_Print( -2, "usage: print_status [-sh]\n" ); Abc_Print( -2, "\t prints verification status\n" ); + Abc_Print( -2, "\t-s : toggle using short print-out [default = %s]\n", fShort? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); return 1; } @@ -32333,18 +32346,61 @@ usage: ***********************************************************************/ int Abc_CommandAbc9MultiProve( Abc_Frame_t * pAbc, int argc, char ** argv ) { - extern int Gia_ManMultiProve( Gia_Man_t * p, int fVerbose ); + extern int Gia_ManMultiProve( Gia_Man_t * p, int TimeOutGlo, int TimeOutLoc, int TimeOutInc, int fUseSyn, int fVerbose, int fVeryVerbose ); Vec_Int_t * vStatuses; - char * pCommLine = NULL; + int TimeOutGlo = 30; + int TimeOutLoc = 2; + int TimeOutInc = 2; + int fUseSyn = 0; int c, fVerbose = 0; + int fVeryVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "TLMsvwh" ) ) != EOF ) { switch ( c ) { + case 'T': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-T\" should be followed by an integer.\n" ); + goto usage; + } + TimeOutGlo = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( TimeOutGlo < 0 ) + goto usage; + break; + case 'L': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-L\" should be followed by an integer.\n" ); + goto usage; + } + TimeOutLoc = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( TimeOutLoc <= 0 ) + goto usage; + break; + case 'M': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-M\" should be followed by an integer.\n" ); + goto usage; + } + TimeOutInc = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( TimeOutInc <= 0 ) + goto usage; + break; + case 's': + fUseSyn ^= 1; + break; case 'v': fVerbose ^= 1; break; + case 'w': + fVeryVerbose ^= 1; + break; case 'h': goto usage; default: @@ -32356,16 +32412,21 @@ int Abc_CommandAbc9MultiProve( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "Abc_CommandAbc9PoPart(): There is no AIG.\n" ); return 1; } - pAbc->Status = Gia_ManMultiProve( pAbc->pGia, fVerbose ); + pAbc->Status = Gia_ManMultiProve( pAbc->pGia, TimeOutGlo, TimeOutLoc, TimeOutInc, fUseSyn, fVerbose, fVeryVerbose ); vStatuses = Abc_FrameDeriveStatusArray( pAbc->pGia->vSeqModelVec ); Abc_FrameReplacePoStatuses( pAbc, &vStatuses ); Abc_FrameReplaceCexVec( pAbc, &pAbc->pGia->vSeqModelVec ); return 0; usage: - Abc_Print( -2, "usage: &mprove [-vh]\n" ); + Abc_Print( -2, "usage: &mprove [-TLM num] [-svwh]\n" ); Abc_Print( -2, "\t proves multi-output testcase by applying several engines\n" ); - Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-T num : approximate global runtime limit in seconds [default = %d]\n", TimeOutGlo ); + Abc_Print( -2, "\t-L num : approximate local runtime limit in seconds [default = %d]\n", TimeOutLoc ); + Abc_Print( -2, "\t-M num : approximate multiple of the local runtime limit [default = %d]\n", TimeOutInc ); + Abc_Print( -2, "\t-s : toggle using combinational synthesis [default = %s]\n", fUseSyn? "yes": "no" ); + Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-w : toggle printing additional verbose information [default = %s]\n", fVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); return 1; } |