diff options
| author | Bruno Schmitt <bruno@oschmitt.com> | 2016-06-17 17:24:58 -0300 |
|---|---|---|
| committer | Bruno Schmitt <bruno@oschmitt.com> | 2016-06-17 17:24:58 -0300 |
| commit | 85428a60ccea5de48d4507501e420efb082f3201 (patch) | |
| tree | 50dbf6a972dc8965aed4cc2e995ed743e8acaa99 /src/opt/fxch/FxchDiv.c | |
| parent | 3c3a770a17e7f8ef81f3e3add81b3f96299f32c1 (diff) | |
| download | abc-85428a60ccea5de48d4507501e420efb082f3201.tar.gz abc-85428a60ccea5de48d4507501e420efb082f3201.tar.bz2 abc-85428a60ccea5de48d4507501e420efb082f3201.zip | |
Enables FXCH to handle Distance-1 cubes (D1C) and Single Cube Containment (SCC) as by product of extraction.
D1C: Whenever they appear a constant divisor (x! + x) will be created and handle as any other divisor.
SCC: Will be taken care of as soon as they appear.
Diffstat (limited to 'src/opt/fxch/FxchDiv.c')
| -rw-r--r-- | src/opt/fxch/FxchDiv.c | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/src/opt/fxch/FxchDiv.c b/src/opt/fxch/FxchDiv.c index 68fd569d..18c8bbfb 100644 --- a/src/opt/fxch/FxchDiv.c +++ b/src/opt/fxch/FxchDiv.c @@ -457,6 +457,17 @@ void Fxch_DivPrint( Fxch_Man_t* pFxchMan, printf( "Divs =%8d \n", Hsh_VecSize( pFxchMan->pDivHash ) ); } +int Fxch_DivIsNotConstant1( Vec_Int_t* vDiv ) +{ + int Lit0 = Abc_Lit2Var( Vec_IntEntry( vDiv, 0 ) ), + Lit1 = Abc_Lit2Var( Vec_IntEntry( vDiv, 1 ) ); + + if ( ( Vec_IntSize( vDiv ) == 2 ) && ( Lit0 == Abc_LitNot( Lit1 ) ) ) + return 0; + + return 1; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// |