diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2014-06-04 12:00:37 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2014-06-04 12:00:37 -0700 |
| commit | f2818ddb83cb405724233c62ae577cb9c78096a9 (patch) | |
| tree | 462123b8d8e4cb89ec58a76582e65f8e0efca17d /src/proof/cec/cecSplit.c | |
| parent | 97bd9d8f1b1755422f65b288ee42a1d4ccb8b777 (diff) | |
| download | abc-f2818ddb83cb405724233c62ae577cb9c78096a9.tar.gz abc-f2818ddb83cb405724233c62ae577cb9c78096a9.tar.bz2 abc-f2818ddb83cb405724233c62ae577cb9c78096a9.zip | |
Adding CEC command &splitprove.
Diffstat (limited to 'src/proof/cec/cecSplit.c')
| -rw-r--r-- | src/proof/cec/cecSplit.c | 15 |
1 files changed, 11 insertions, 4 deletions
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 |