diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2014-06-04 11:33:49 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2014-06-04 11:33:49 -0700 |
| commit | d2c3971de071e0ac074f29bbfb35bac67cbe81fa (patch) | |
| tree | 81d38b498ee42289d1bd1e7a990d48eee5cb270f | |
| parent | d527f03a2789e2fc2d66bb055f4e880ca864b27d (diff) | |
| download | abc-d2c3971de071e0ac074f29bbfb35bac67cbe81fa.tar.gz abc-d2c3971de071e0ac074f29bbfb35bac67cbe81fa.tar.bz2 abc-d2c3971de071e0ac074f29bbfb35bac67cbe81fa.zip | |
Adding CEC command &splitprove.
| -rw-r--r-- | src/proof/cec/cecSplit.c | 51 |
1 files changed, 42 insertions, 9 deletions
diff --git a/src/proof/cec/cecSplit.c b/src/proof/cec/cecSplit.c index 6dedbe0f..7b33efc6 100644 --- a/src/proof/cec/cecSplit.c +++ b/src/proof/cec/cecSplit.c @@ -148,7 +148,7 @@ void Cec_GiaSplitExplore( Gia_Man_t * p ) /**Function************************************************************* - Synopsis [Permute primary inputs.] + Synopsis [Find cofactoring variable.] Description [] @@ -195,6 +195,41 @@ Gia_Man_t * Gia_PermuteSpecial( Gia_Man_t * p ) /**Function************************************************************* + Synopsis [Find cofactoring variable.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_SplitCofVar2( Gia_Man_t * p ) +{ + Gia_Man_t * pPart; + int * pOrder = Gia_PermuteSpecialOrder( p ); + int Cost0, Cost1, CostBest = ABC_INFINITY; + int i, iBest = -1, LookAhead = 10; + for ( i = 0; i < LookAhead; i++ ) + { + pPart = Gia_ManDupCofactor( p, pOrder[i], 0 ); + Cost0 = Gia_ManAndNum(pPart); + Gia_ManStop( pPart ); + + pPart = Gia_ManDupCofactor( p, pOrder[i], 1 ); + Cost1 = Gia_ManAndNum(pPart); + Gia_ManStop( pPart ); + + if ( CostBest > Cost0 + Cost1 ) + CostBest = Cost0 + Cost1, iBest = pOrder[i]; + } + ABC_FREE( pOrder ); + assert( iBest >= 0 ); + return iBest; +} + +/**Function************************************************************* + Synopsis [] Description [] @@ -295,10 +330,10 @@ void Cec_GiaSplitPrint( int nIter, int Depth, int nVars, int nConfs, int fSatUns { printf( "%6d : ", nIter ); printf( "Depth =%3d ", Depth ); - printf( "SatVar =%10d ", nVars ); + printf( "SatVar =%7d ", nVars ); printf( "SatConf =%7d ", nConfs ); - printf( "%s ", fSatUnsat ? "UNSAT " : "UNDECIDED" ); - printf( "Progress = %.10f ", Prog ); + printf( "%s ", fSatUnsat ? "UNSAT " : "UNDECIDED" ); + printf( "Progress = %.10f ", Prog ); Abc_PrintTime( 1, "Time", clk ); //ABC_PRTr( "Time", Abc_Clock()-clk ); } @@ -351,8 +386,8 @@ int Cec_GiaSplitTest( Gia_Man_t * p, int nTimeOut, int fVerbose ) // get the last AIG pLast = (Gia_Man_t *)Vec_PtrPop( vStack ); // determine cofactoring variable - iVar = Gia_SplitCofVar( pLast ); Depth = Vec_IntSize(pLast->vCofVars); + iVar = Gia_SplitCofVar2( pLast ); // cofactor pPart0 = Gia_ManDupCofactor( pLast, iVar, 0 ); // create variable @@ -371,8 +406,6 @@ int Cec_GiaSplitTest( Gia_Man_t * p, int nTimeOut, int fVerbose ) fSatUnsat = (fSatUnsat == Vec_PtrSize(vStack)); if ( fSatUnsat ) Progress += 1.0 / pow(2, Depth + 1); - else - Cec_GiaSplitPrintRefs( pPart0 ); if ( fVerbose ) Cec_GiaSplitPrint( nIter, Depth, nSatVars, nSatConfs, fSatUnsat, Progress, Abc_Clock() - clk ); // cofactor @@ -395,8 +428,8 @@ 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) > 5 ) -// break; + if ( Vec_PtrSize(vStack) > 3 ) + break; } if ( Vec_PtrSize(vStack) == 0 ) RetValue = 1; |