diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2014-06-07 13:14:23 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2014-06-07 13:14:23 -0700 |
| commit | 3c6def2915664328df40b939e48941e6a2fcb475 (patch) | |
| tree | 6920d9a6ce3cd14c5acbb4ab048a31789d2d0625 /src/proof | |
| parent | 2d38fc16082607666fe60a72197872196c7bcc2a (diff) | |
| download | abc-3c6def2915664328df40b939e48941e6a2fcb475.tar.gz abc-3c6def2915664328df40b939e48941e6a2fcb475.tar.bz2 abc-3c6def2915664328df40b939e48941e6a2fcb475.zip | |
Adding print-out to &splitprove to see impact of cof variable on AIG size.
Diffstat (limited to 'src/proof')
| -rw-r--r-- | src/proof/cec/cecSplit.c | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/src/proof/cec/cecSplit.c b/src/proof/cec/cecSplit.c index eef0fc77..5279570e 100644 --- a/src/proof/cec/cecSplit.c +++ b/src/proof/cec/cecSplit.c @@ -397,7 +397,7 @@ void Cec_GiaSplitPrintRefs( Gia_Man_t * p ) SeeAlso [] ***********************************************************************/ -int Cec_GiaSplitTest2( Gia_Man_t * p, int nProcs, int nTimeOut, int nIterMax, int LookAhead, int fVerbose ) +int Cec_GiaSplitTest2( Gia_Man_t * p, int nProcs, int nTimeOut, int nIterMax, int LookAhead, int fVerbose, int fVeryVerbose ) { abctime clkTotal = Abc_Clock(); Vec_Ptr_t * vStack; @@ -438,7 +438,7 @@ int Cec_GiaSplitTest2( Gia_Man_t * p, int nProcs, int nTimeOut, int nIterMax, in if ( pLast->vCofVars == NULL ) pLast->vCofVars = Vec_IntAlloc( 100 ); // print results - if ( fVerbose ) + if ( fVeryVerbose ) { // Cec_GiaSplitPrintRefs( pLast ); printf( "Var = %5d. Fanouts = %5d. Cost = %8d. AndBefore = %6d. AndAfter = %6d.\n", @@ -558,7 +558,7 @@ void * Cec_GiaSplitWorkerThread( void * pArg ) assert( 0 ); return NULL; } -int Cec_GiaSplitTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nIterMax, int LookAhead, int fVerbose ) +int Cec_GiaSplitTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nIterMax, int LookAhead, int fVerbose, int fVeryVerbose ) { abctime clkTotal = Abc_Clock(); Par_ThData_t ThData[PAR_THR_MAX]; @@ -575,7 +575,7 @@ int Cec_GiaSplitTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nIterMax, int printf( "Processes = %d TimeOut = %d sec MaxIter = %d LookAhead = %d Verbose = %d.\n", nProcs, nTimeOut, nIterMax, LookAhead, fVerbose ); fflush( stdout ); if ( nProcs == 1 ) - return Cec_GiaSplitTest2( p, nProcs, nTimeOut, nIterMax, LookAhead, fVerbose ); + return Cec_GiaSplitTest2( p, nProcs, nTimeOut, nIterMax, LookAhead, fVerbose, fVeryVerbose ); // subtract manager thread nProcs--; assert( nProcs >= 1 && nProcs <= PAR_THR_MAX ); @@ -650,7 +650,7 @@ int Cec_GiaSplitTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nIterMax, int Vec_IntPush( pPart->vCofVars, Abc_Var2Lit(iVar, 1) ); Vec_PtrPush( vStack, pPart ); // print results - if ( fVerbose ) + if ( fVeryVerbose ) { // Cec_GiaSplitPrintRefs( pLast ); printf( "Var = %5d. Fanouts = %5d. Cost = %8d. AndBefore = %6d. AndAfter = %6d.\n", |