luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Adding CEC command &splitprove.

This commit is contained in:
Alan Mishchenko 2014-06-04 11:33:49 -07:00
parent d527f03a27
commit d2c3971de0
1 changed files with 42 additions and 9 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

51
src/proof/cec/cecSplit.c
View File

@ -148,7 +148,7 @@ void Cec_GiaSplitExplore( Gia_Man_t * p )
/**Function************************************************************* /**Function*************************************************************
Synopsis [Permute primary inputs.] Synopsis [Find cofactoring variable.]
Description [] Description []
@ -193,6 +193,41 @@ Gia_Man_t * Gia_PermuteSpecial( Gia_Man_t * p )
return pNew; return pNew;
} }
/**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************************************************************* /**Function*************************************************************
Synopsis [] Synopsis []
@ -295,10 +330,10 @@ void Cec_GiaSplitPrint( int nIter, int Depth, int nVars, int nConfs, int fSatUns
{ {
printf( "%6d : ", nIter ); printf( "%6d : ", nIter );
printf( "Depth =%3d ", Depth ); printf( "Depth =%3d ", Depth );
printf( "SatVar =%10d ", nVars ); printf( "SatVar =%7d ", nVars );
printf( "SatConf =%7d ", nConfs ); printf( "SatConf =%7d ", nConfs );
printf( "%s ", fSatUnsat ? "UNSAT " : "UNDECIDED" ); printf( "%s ", fSatUnsat ? "UNSAT " : "UNDECIDED" );
printf( "Progress = %.10f ", Prog ); printf( "Progress = %.10f ", Prog );
Abc_PrintTime( 1, "Time", clk ); Abc_PrintTime( 1, "Time", clk );
//ABC_PRTr( "Time", Abc_Clock()-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 // get the last AIG
pLast = (Gia_Man_t *)Vec_PtrPop( vStack ); pLast = (Gia_Man_t *)Vec_PtrPop( vStack );
// determine cofactoring variable // determine cofactoring variable
iVar = Gia_SplitCofVar( pLast );
Depth = Vec_IntSize(pLast->vCofVars); Depth = Vec_IntSize(pLast->vCofVars);
iVar = Gia_SplitCofVar2( pLast );
// cofactor // cofactor
pPart0 = Gia_ManDupCofactor( pLast, iVar, 0 ); pPart0 = Gia_ManDupCofactor( pLast, iVar, 0 );
// create variable // create variable
@ -371,8 +406,6 @@ int Cec_GiaSplitTest( Gia_Man_t * p, int nTimeOut, int fVerbose )
fSatUnsat = (fSatUnsat == Vec_PtrSize(vStack)); fSatUnsat = (fSatUnsat == Vec_PtrSize(vStack));
if ( fSatUnsat ) if ( fSatUnsat )
Progress += 1.0 / pow(2, Depth + 1); Progress += 1.0 / pow(2, Depth + 1);
else
Cec_GiaSplitPrintRefs( pPart0 );
if ( fVerbose ) if ( fVerbose )
Cec_GiaSplitPrint( nIter, Depth, nSatVars, nSatConfs, fSatUnsat, Progress, Abc_Clock() - clk ); Cec_GiaSplitPrint( nIter, Depth, nSatVars, nSatConfs, fSatUnsat, Progress, Abc_Clock() - clk );
// cofactor // cofactor
@ -395,8 +428,8 @@ int Cec_GiaSplitTest( Gia_Man_t * p, int nTimeOut, int fVerbose )
Progress += 1.0 / pow(2, Depth + 1); Progress += 1.0 / pow(2, Depth + 1);
if ( fVerbose ) if ( fVerbose )
Cec_GiaSplitPrint( nIter, Depth, nSatVars, nSatConfs, fSatUnsat, Progress, Abc_Clock() - clk ); Cec_GiaSplitPrint( nIter, Depth, nSatVars, nSatConfs, fSatUnsat, Progress, Abc_Clock() - clk );
// if ( Vec_PtrSize(vStack) > 5 ) if ( Vec_PtrSize(vStack) > 3 )
// break; break;
} }
if ( Vec_PtrSize(vStack) == 0 ) if ( Vec_PtrSize(vStack) == 0 )
RetValue = 1; RetValue = 1;