diff options
| -rw-r--r-- | src/base/abci/abc.c | 25 | ||||
| -rw-r--r-- | src/proof/cec/cecSplit.c | 15 |
2 files changed, 31 insertions, 9 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 017e931a..7058de3e 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 nIterMax, int fVerbose ); - int c, nTimeOut = 1, nIterMax = 0, fVerbose = 0; + extern Gia_Man_t * Cec_GiaSplitTest( Gia_Man_t * p, int nTimeOut, int nIterMax, int LookAhead, int fVerbose ); + int c, nTimeOut = 1, nIterMax = 0, LookAhead = 1, fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "TIvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "TILvh" ) ) != EOF ) { switch ( c ) { @@ -32905,6 +32905,20 @@ int Abc_CommandAbc9SplitProve( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( nIterMax < 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; + } + LookAhead = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( LookAhead <= 0 || LookAhead > 100 ) + { + Abc_Print( -1, "Look-ahead value (\"-L <num>\") should be between 1 and 100.\n", LookAhead ); + goto usage; + } + break; case 'v': fVerbose ^= 1; break; @@ -32924,14 +32938,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, nIterMax, fVerbose ); + Cec_GiaSplitTest( pAbc->pGia, nTimeOut, nIterMax, LookAhead, fVerbose ); return 0; usage: - Abc_Print( -2, "usage: &splitprove [-TI num] [-vh]\n" ); + Abc_Print( -2, "usage: &splitprove [-TIL 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-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-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 7ba3d51e..e04d6224 100644 --- a/src/proof/cec/cecSplit.c +++ b/src/proof/cec/cecSplit.c @@ -204,12 +204,14 @@ Gia_Man_t * Gia_PermuteSpecial( Gia_Man_t * p ) SeeAlso [] ***********************************************************************/ -int Gia_SplitCofVar2( Gia_Man_t * p ) +int Gia_SplitCofVar2( Gia_Man_t * p, int LookAhead ) { + abctime clk = Abc_Clock(); Gia_Man_t * pPart; int * pOrder = Gia_PermuteSpecialOrder( p ); int Cost0, Cost1, CostBest = ABC_INFINITY; - int i, iBest = -1, LookAhead = 10; + int i, iBest = -1; + LookAhead = Abc_MinInt( LookAhead, Gia_ManPiNum(p) ); for ( i = 0; i < LookAhead; i++ ) { pPart = Gia_ManDupCofactor( p, pOrder[i], 0 ); @@ -222,9 +224,14 @@ int Gia_SplitCofVar2( Gia_Man_t * p ) if ( CostBest > Cost0 + Cost1 ) CostBest = Cost0 + Cost1, iBest = pOrder[i]; + +// printf( "%2d : Var = %4d Refs = %3d %6d %6d -> %6d\n", +// i, pOrder[i], Gia_ObjRefNum(p, Gia_ManPi(p, pOrder[i])), +// Cost0, Cost1, Cost0+Cost1 ); } ABC_FREE( pOrder ); assert( iBest >= 0 ); +// Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); return iBest; } @@ -359,7 +366,7 @@ void Cec_GiaSplitPrintRefs( Gia_Man_t * p ) SeeAlso [] ***********************************************************************/ -int Cec_GiaSplitTest( Gia_Man_t * p, int nTimeOut, int nIterMax, int fVerbose ) +int Cec_GiaSplitTest( Gia_Man_t * p, int nTimeOut, int nIterMax, int LookAhead, int fVerbose ) { abctime clk, clkTotal = Abc_Clock(); Gia_Man_t * pPart0, * pPart1, * pLast; @@ -387,7 +394,7 @@ int Cec_GiaSplitTest( Gia_Man_t * p, int nTimeOut, int nIterMax, int fVerbose ) pLast = (Gia_Man_t *)Vec_PtrPop( vStack ); // determine cofactoring variable Depth = Vec_IntSize(pLast->vCofVars); - iVar = Gia_SplitCofVar2( pLast ); + iVar = Gia_SplitCofVar2( pLast, LookAhead ); // cofactor pPart0 = Gia_ManDupCofactor( pLast, iVar, 0 ); // create variable |