diff options
author | Bruno Schmitt <bruno@oschmitt.com> | 2016-05-11 19:41:31 -0300 |
---|---|---|
committer | Bruno Schmitt <bruno@oschmitt.com> | 2016-05-11 19:41:31 -0300 |
commit | 3cf495c83197f838580a6efd25e9d5a68e871fa6 (patch) | |
tree | 5e0dfd49da6764d829f9e43a0f6dbc746bb92007 /src/opt/fxch/FxchDiv.c | |
parent | 8745fa8163d94ffd90590cc052eb39bd5a866bff (diff) | |
download | abc-3cf495c83197f838580a6efd25e9d5a68e871fa6.tar.gz abc-3cf495c83197f838580a6efd25e9d5a68e871fa6.tar.bz2 abc-3cf495c83197f838580a6efd25e9d5a68e871fa6.zip |
Add a new module which implements the fast extract with cube hashing (fxch) algorithm.
Removes old partial implementation of this algorithm from the "pla" module.
Diffstat (limited to 'src/opt/fxch/FxchDiv.c')
-rw-r--r-- | src/opt/fxch/FxchDiv.c | 582 |
1 files changed, 582 insertions, 0 deletions
diff --git a/src/opt/fxch/FxchDiv.c b/src/opt/fxch/FxchDiv.c new file mode 100644 index 00000000..072198ef --- /dev/null +++ b/src/opt/fxch/FxchDiv.c @@ -0,0 +1,582 @@ +/**CFile**************************************************************************************************************** + + FileName [ FxchDiv.c ] + + PackageName [ Fast eXtract with Cube Hashing (FXCH) ] + + Synopsis [ Divisor handling functions ] + + Author [ Bruno Schmitt - boschmitt at inf.ufrgs.br ] + + Affiliation [ UFRGS ] + + Date [ Ver. 1.0. Started - March 6, 2016. ] + + Revision [] + +***********************************************************************************************************************/ + +#include "Fxch.h" + +ABC_NAMESPACE_IMPL_START + +//////////////////////////////////////////////////////////////////////////////////////////////////////////////////////// +// FUNCTION DEFINITIONS +//////////////////////////////////////////////////////////////////////////////////////////////////////////////////////// +static inline int Fxch_DivNormalize( Vec_Int_t* vCubeFree ) +{ + int * L = Vec_IntArray(vCubeFree); + int RetValue = 0, LitA0 = -1, LitB0 = -1, LitA1 = -1, LitB1 = -1; + assert( Vec_IntSize(vCubeFree) == 4 ); + if ( Abc_LitIsCompl(L[0]) != Abc_LitIsCompl(L[1]) && (L[0] >> 2) == (L[1] >> 2) ) // diff cubes, same vars + { + if ( Abc_LitIsCompl(L[2]) == Abc_LitIsCompl(L[3]) ) + return -1; + LitA0 = Abc_Lit2Var(L[0]), LitB0 = Abc_Lit2Var(L[1]); + if ( Abc_LitIsCompl(L[0]) == Abc_LitIsCompl(L[2]) ) + { + assert( Abc_LitIsCompl(L[1]) == Abc_LitIsCompl(L[3]) ); + LitA1 = Abc_Lit2Var(L[2]), LitB1 = Abc_Lit2Var(L[3]); + } + else + { + assert( Abc_LitIsCompl(L[0]) == Abc_LitIsCompl(L[3]) ); + assert( Abc_LitIsCompl(L[1]) == Abc_LitIsCompl(L[2]) ); + LitA1 = Abc_Lit2Var(L[3]), LitB1 = Abc_Lit2Var(L[2]); + } + } + else if ( Abc_LitIsCompl(L[1]) != Abc_LitIsCompl(L[2]) && (L[1] >> 2) == (L[2] >> 2) ) + { + if ( Abc_LitIsCompl(L[0]) == Abc_LitIsCompl(L[3]) ) + return -1; + LitA0 = Abc_Lit2Var(L[1]), LitB0 = Abc_Lit2Var(L[2]); + if ( Abc_LitIsCompl(L[1]) == Abc_LitIsCompl(L[0]) ) + LitA1 = Abc_Lit2Var(L[0]), LitB1 = Abc_Lit2Var(L[3]); + else + LitA1 = Abc_Lit2Var(L[3]), LitB1 = Abc_Lit2Var(L[0]); + } + else if ( Abc_LitIsCompl(L[2]) != Abc_LitIsCompl(L[3]) && (L[2] >> 2) == (L[3] >> 2) ) + { + if ( Abc_LitIsCompl(L[0]) == Abc_LitIsCompl(L[1]) ) + return -1; + LitA0 = Abc_Lit2Var(L[2]), LitB0 = Abc_Lit2Var(L[3]); + if ( Abc_LitIsCompl(L[2]) == Abc_LitIsCompl(L[0]) ) + LitA1 = Abc_Lit2Var(L[0]), LitB1 = Abc_Lit2Var(L[1]); + else + LitA1 = Abc_Lit2Var(L[1]), LitB1 = Abc_Lit2Var(L[0]); + } + else + return -1; + assert( LitA0 == Abc_LitNot(LitB0) ); + if ( Abc_LitIsCompl(LitA0) ) + { + ABC_SWAP( int, LitA0, LitB0 ); + ABC_SWAP( int, LitA1, LitB1 ); + } + assert( !Abc_LitIsCompl(LitA0) ); + if ( Abc_LitIsCompl(LitA1) ) + { + LitA1 = Abc_LitNot(LitA1); + LitB1 = Abc_LitNot(LitB1); + RetValue = 1; + } + assert( !Abc_LitIsCompl(LitA1) ); + // arrange literals in such as a way that + // - the first two literals are control literals from different cubes + // - the third literal is non-complented data input + // - the forth literal is possibly complemented data input + L[0] = Abc_Var2Lit( LitA0, 0 ); + L[1] = Abc_Var2Lit( LitB0, 1 ); + L[2] = Abc_Var2Lit( LitA1, 0 ); + L[3] = Abc_Var2Lit( LitB1, 1 ); + return RetValue; +} + +/**Function************************************************************* + + Synopsis [ Creates a Divisor. ] + + Description [ This functions receive as input two sub-cubes and creates + a divisor using their information. The divisor is stored + in vCubeFree vector of the pFxchMan structure. + + It returns the base value, which is the number of elements + that the cubes pair used to generate the devisor have in + common. ] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fxch_DivCreate( Fxch_Man_t* pFxchMan, + Fxch_SubCube_t* pSubCube0, + Fxch_SubCube_t* pSubCube1 ) +{ + int Base = 0; + + Vec_IntClear( pFxchMan->vCubeFree ); + + int SC0_Lit0, + SC0_Lit1, + SC1_Lit0, + SC1_Lit1; + + SC0_Lit0 = Fxch_ManGetLit( pFxchMan, pSubCube0->iCube, pSubCube0->iLit0 ); + SC0_Lit1 = 0; + SC1_Lit0 = Fxch_ManGetLit( pFxchMan, pSubCube1->iCube, pSubCube1->iLit0 ); + SC1_Lit1 = 0; + + if ( pSubCube0->iLit1 == 0 && pSubCube1->iLit1 == 0 ) + { + Vec_IntPush( pFxchMan->vCubeFree, SC0_Lit0 ); + Vec_IntPush( pFxchMan->vCubeFree, SC1_Lit0 ); + } + else if ( pSubCube0->iLit1 > 0 && pSubCube1->iLit1 > 0 ) + { + SC0_Lit1 = Fxch_ManGetLit( pFxchMan, pSubCube0->iCube, pSubCube0->iLit1 ); + SC1_Lit1 = Fxch_ManGetLit( pFxchMan, pSubCube1->iCube, pSubCube1->iLit1 ); + + Vec_IntPush( pFxchMan->vCubeFree, Abc_Var2Lit( SC0_Lit0, 0 ) ); + Vec_IntPush( pFxchMan->vCubeFree, Abc_Var2Lit( SC1_Lit0, 1 ) ); + Vec_IntPush( pFxchMan->vCubeFree, Abc_Var2Lit( SC0_Lit1, 0 ) ); + Vec_IntPush( pFxchMan->vCubeFree, Abc_Var2Lit( SC1_Lit1, 1 ) ); + + int RetValue = Fxch_DivNormalize( pFxchMan->vCubeFree ); + if ( RetValue == -1 ) + return -1; + } + else + { + if ( pSubCube0->iLit1 > 0 ) + { + SC0_Lit1 = Fxch_ManGetLit( pFxchMan, pSubCube0->iCube, pSubCube0->iLit1 ); + + Vec_IntPush( pFxchMan->vCubeFree, SC1_Lit0 ); + if ( SC0_Lit0 == Abc_LitNot( SC1_Lit0 ) ) + Vec_IntPush( pFxchMan->vCubeFree, SC0_Lit1 ); + else if ( SC0_Lit1 == Abc_LitNot( SC1_Lit0 ) ) + Vec_IntPush( pFxchMan->vCubeFree, SC0_Lit0 ); + } + else + { + SC1_Lit1 = Fxch_ManGetLit( pFxchMan, pSubCube1->iCube, pSubCube1->iLit1 ); + + Vec_IntPush( pFxchMan->vCubeFree, SC0_Lit0 ); + if ( SC1_Lit0 == Abc_LitNot( SC0_Lit0 ) ) + Vec_IntPush( pFxchMan->vCubeFree, SC1_Lit1 ); + else if ( SC1_Lit1 == Abc_LitNot( SC0_Lit0 ) ) + Vec_IntPush( pFxchMan->vCubeFree, SC1_Lit0 ); + } + } + + if ( Vec_IntSize( pFxchMan->vCubeFree ) == 0 ) + return -1; + + if ( Vec_IntSize ( pFxchMan->vCubeFree ) == 2 ) + { + Vec_IntSort( pFxchMan->vCubeFree, 0 ); + + Vec_IntWriteEntry( pFxchMan->vCubeFree, 0, Abc_Var2Lit( Vec_IntEntry( pFxchMan->vCubeFree, 0 ), 0 ) ); + Vec_IntWriteEntry( pFxchMan->vCubeFree, 1, Abc_Var2Lit( Vec_IntEntry( pFxchMan->vCubeFree, 1 ), 1 ) ); + } + + int Cube0Size = Vec_IntSize( Fxch_ManGetCube( pFxchMan, pSubCube0->iCube ) ), + Cube1Size = Vec_IntSize( Fxch_ManGetCube( pFxchMan, pSubCube1->iCube ) ); + if ( Vec_IntSize( pFxchMan->vCubeFree ) % 2 == 0 ) + { + Base = Abc_MinInt( Cube0Size, Cube1Size ) + -( Vec_IntSize( pFxchMan->vCubeFree ) / 2) - 1; /* 1 or 2 Lits, 1 SOP NodeID */ + } + else + return -1; + + return Base; +} + +/**Function************************************************************* + + Synopsis [ Add a divisor to the divisors hash table. ] + + Description [ This functions will try to add the divisor store in + vCubeFree to the divisor hash table. If the divisor + is already present in the hash table it will just + increment its weight, otherwise it will add the divisor + and asign an initial weight. ] + + SideEffects [ If the fUpdate option is set, the function will also + update the divisor priority queue. ] + + SeeAlso [] + +***********************************************************************/ +int Fxch_DivAdd( Fxch_Man_t* pFxchMan, + int fUpdate, + int fSingleCube, + int fBase ) +{ + int iDiv = Hsh_VecManAdd( pFxchMan->pDivHash, pFxchMan->vCubeFree ); + + /* Verify if the divisor already exist */ + if ( iDiv == Vec_FltSize( pFxchMan->vDivWeights ) ) + { + if ( pFxchMan->SMode == 0 ) + Vec_WecPushLevel( pFxchMan->vDivCubePairs ); + + /* Assign initial weight */ + if ( fSingleCube ) + { + Vec_FltPush( pFxchMan->vDivWeights, + -Vec_IntSize( pFxchMan->vCubeFree ) + 0.9 + -0.001 * Fxch_ManComputeLevelDiv( pFxchMan, pFxchMan->vCubeFree ) ); + } + else + { + Vec_FltPush( pFxchMan->vDivWeights, + -Vec_IntSize( pFxchMan->vCubeFree ) + 0.9 + -0.0009 * Fxch_ManComputeLevelDiv( pFxchMan, pFxchMan->vCubeFree ) ); + } + + } + + /* Increment weight */ + if ( fSingleCube ) + Vec_FltAddToEntry( pFxchMan->vDivWeights, iDiv, 1 ); + else + Vec_FltAddToEntry( pFxchMan->vDivWeights, iDiv, fBase + Vec_IntSize( pFxchMan->vCubeFree ) - 1 ); + + assert( iDiv < Vec_FltSize( pFxchMan->vDivWeights ) ); + + if ( fUpdate ) + if ( pFxchMan->vDivPrio ) + { + if ( Vec_QueIsMember( pFxchMan->vDivPrio, iDiv ) ) + Vec_QueUpdate( pFxchMan->vDivPrio, iDiv ); + else + Vec_QuePush( pFxchMan->vDivPrio, iDiv ); + } + + return iDiv; +} + +/**Function************************************************************* + + Synopsis [ Removes a divisor to the divisors hash table. ] + + Description [ This function don't effectively removes a divisor from + the hash table (the hash table implementation don't + support such operation). It only assures its existence + and decrement its weight. ] + + SideEffects [ If the fUpdate option is set, the function will also + update the divisor priority queue. ] + + SeeAlso [] + +***********************************************************************/ +int Fxch_DivRemove( Fxch_Man_t* pFxchMan, + int fUpdate, + int fSingleCube, + int fBase ) +{ + int iDiv = Hsh_VecManAdd( pFxchMan->pDivHash, pFxchMan->vCubeFree ); + + assert( iDiv < Vec_FltSize( pFxchMan->vDivWeights ) ); + + /* Decrement weight */ + if ( fSingleCube ) + Vec_FltAddToEntry( pFxchMan->vDivWeights, iDiv, -1 ); + else + Vec_FltAddToEntry( pFxchMan->vDivWeights, iDiv, -( fBase + Vec_IntSize( pFxchMan->vCubeFree ) - 1 ) ); + + if ( fUpdate ) + if ( pFxchMan->vDivPrio ) + { + if ( Vec_QueIsMember( pFxchMan->vDivPrio, iDiv ) ) + Vec_QueUpdate( pFxchMan->vDivPrio, iDiv ); + } + + return iDiv; +} + +/**Function************************************************************* + + Synopsis [ Separete the cubes in present in a divisor ] + + Description [ In this implementation *all* stored divsors are composed + of two cubes. + + In order to save space and to be able to use the Vec_Int_t + hash table both cubes are stored in the same vector - using + a little hack to differentiate which literal belongs to each + cube. + + This function separetes the two cubes in their own vectors + so that they can be added to the cover. + + *Note* that this also applies to single cube + divisors beacuse of the DeMorgan Law: ab = ( a! + !b )! ] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fxch_DivSepareteCubes( Vec_Int_t* vDiv, + Vec_Int_t* vCube0, + Vec_Int_t* vCube1 ) +{ + int* pArray; + int i, + Lit; + + Vec_IntForEachEntry( vDiv, Lit, i ) + if ( Abc_LitIsCompl(Lit) ) + Vec_IntPush( vCube1, Abc_Lit2Var( Lit ) ); + else + Vec_IntPush( vCube0, Abc_Lit2Var( Lit ) ); + + if ( ( Vec_IntSize( vDiv ) == 4 ) && ( Vec_IntSize( vCube0 ) == 3 ) ) + { + assert( Vec_IntSize( vCube1 ) == 3 ); + + pArray = Vec_IntArray( vCube0 ); + if ( pArray[1] > pArray[2] ) + ABC_SWAP( int, pArray[1], pArray[2] ); + + pArray = Vec_IntArray( vCube1 ); + if ( pArray[1] > pArray[2] ) + ABC_SWAP( int, pArray[1], pArray[2] ); + } +} + +/**Function************************************************************* + + Synopsis [ Removes the literals present in the divisor from their + original cubes. ] + + Description [ This function returns the numeber of removed literals + which should be equal to the size of the divisor. ] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fxch_DivRemoveLits( Vec_Int_t* vCube0, + Vec_Int_t* vCube1, + Vec_Int_t* vDiv, + int *fCompl ) +{ + int i, + Lit, + CountP = 0, + CountN = 0, + Count = 0, + ret = 0; + + Vec_IntForEachEntry( vDiv, Lit, i ) + if ( Abc_LitIsCompl( Abc_Lit2Var( Lit ) ) ) + CountN += Vec_IntRemove1( vCube0, Abc_Lit2Var( Lit ) ); + else + CountP += Vec_IntRemove1( vCube0, Abc_Lit2Var( Lit ) ); + + Vec_IntForEachEntry( vDiv, Lit, i ) + Count += Vec_IntRemove1( vCube1, Abc_Lit2Var( Lit ) ); + + if ( Vec_IntSize( vDiv ) == 2 ) + Vec_IntForEachEntry( vDiv, Lit, i ) + { + Vec_IntRemove1( vCube0, Abc_LitNot( Abc_Lit2Var( Lit ) ) ); + Vec_IntRemove1( vCube1, Abc_LitNot( Abc_Lit2Var( Lit ) ) ); + } + + ret = Count + CountP + CountN; + + if ( Vec_IntSize( vDiv ) == 4 ) + { + int Lit0 = Abc_Lit2Var( Vec_IntEntry( vDiv, 0 ) ), + Lit1 = Abc_Lit2Var( Vec_IntEntry( vDiv, 1 ) ), + Lit2 = Abc_Lit2Var( Vec_IntEntry( vDiv, 2 ) ), + Lit3 = Abc_Lit2Var( Vec_IntEntry( vDiv, 3 ) ); + + if ( Lit0 == Abc_LitNot( Lit1 ) && Lit2 == Abc_LitNot( Lit3 ) && CountN == 1 ) + *fCompl = 1; + + if ( Lit0 == Abc_LitNot( Lit1 ) && ret == 2 ) + { + *fCompl = 1; + + Vec_IntForEachEntry( vDiv, Lit, i ) + ret += Vec_IntRemove1( vCube0, ( Abc_Lit2Var( Lit ) ^ (fCompl && i > 1) ) ); + + Vec_IntForEachEntry( vDiv, Lit, i ) + ret += Vec_IntRemove1( vCube1, ( Abc_Lit2Var( Lit ) ^ (fCompl && i > 1) ) ); + } + } + + return ret; +} + +/**Function************************************************************* + + Synopsis [ Print the divisor identified by iDiv. ] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fxch_DivPrint( Fxch_Man_t* pFxchMan, + int iDiv ) +{ + Vec_Int_t* vDiv = Hsh_VecReadEntry( pFxchMan->pDivHash, iDiv ); + int i, + Lit; + + printf( "Div %7d : ", iDiv ); + printf( "Weight %12.5f ", Vec_FltEntry( pFxchMan->vDivWeights, iDiv ) ); + + Vec_IntForEachEntry( vDiv, Lit, i ) + if ( !Abc_LitIsCompl( Lit ) ) + printf( "%d(1)", Abc_Lit2Var( Lit ) ); + + printf( " + " ); + + Vec_IntForEachEntry( vDiv, Lit, i ) + if ( Abc_LitIsCompl( Lit ) ) + printf( "%d(2)", Abc_Lit2Var( Lit ) ); + + printf( " Lits =%7d ", pFxchMan->nLits ); + printf( "Divs =%8d \n", Hsh_VecSize( pFxchMan->pDivHash ) ); +} + +/* XXX: The following functions were adapted from "fx" to be used by the Saving Memory mode */ +void Fxch_DivFindPivots( Vec_Int_t* vDiv, + int* pLit0, + int* pLit1 ) +{ + int i, + Lit; + * pLit0 = -1; + * pLit1 = -1; + + Vec_IntForEachEntry( vDiv, Lit, i ) + { + if ( Abc_LitIsCompl( Lit ) ) + { + if ( *pLit1 == -1 ) + *pLit1 = Abc_Lit2Var( Lit ); + } + else + { + if ( *pLit0 == -1 ) + *pLit0 = Abc_Lit2Var( Lit ); + } + if ( *pLit0 >= 0 && *pLit1 >= 0 ) + return; + } +} + +int Fxch_DivFind( Vec_Int_t* vCube0, + Vec_Int_t* vCube1, + Vec_Int_t* vCubeFree ) +{ + int Counter = 0, + fAttr0 = 0, + fAttr1 = 1; + int* pBeg1 = vCube0->pArray + 1, + * pBeg2 = vCube1->pArray + 1, + * pEnd1 = vCube0->pArray + vCube0->nSize, + * pEnd2 = vCube1->pArray + vCube1->nSize; + + Vec_IntClear( vCubeFree ); + + while ( pBeg1 < pEnd1 && pBeg2 < pEnd2 ) + { + if ( *pBeg1 == *pBeg2 ) + { + pBeg1++; + pBeg2++; + Counter++; + } + else if ( *pBeg1 < *pBeg2 ) + Vec_IntPush( vCubeFree, Abc_Var2Lit( *pBeg1++, fAttr0 ) ); + else + { + if ( Vec_IntSize( vCubeFree ) == 0 ) + fAttr0 = 1, fAttr1 = 0; + Vec_IntPush( vCubeFree, Abc_Var2Lit( *pBeg2++, fAttr1) ); + } + } + while ( pBeg1 < pEnd1 ) + Vec_IntPush( vCubeFree, Abc_Var2Lit( *pBeg1++, fAttr0 ) ); + while ( pBeg2 < pEnd2 ) + Vec_IntPush( vCubeFree, Abc_Var2Lit( *pBeg2++, fAttr1 ) ); + + assert( !Abc_LitIsCompl( Vec_IntEntry(vCubeFree, 0) ) ); + return Counter; +} + +void Fxch_DivFindCubePairs( Fxch_Man_t* pFxchMan, + Vec_Int_t* vCubes_Lit0, + Vec_Int_t* vCubes_Lit1 ) +{ + int* pBeg1 = vCubes_Lit0->pArray + 1, + * pBeg2 = vCubes_Lit1->pArray + 1, + * pEnd1 = vCubes_Lit0->pArray + vCubes_Lit0->nSize, + * pEnd2 = vCubes_Lit1->pArray + vCubes_Lit1->nSize; + + Vec_IntClear( pFxchMan->vPairs ); + + while ( pBeg1 < pEnd1 && pBeg2 < pEnd2 ) + { + int CubeId1 = Fxch_ManGetLit( pFxchMan, *pBeg1, 0 ), + CubeId2 = Fxch_ManGetLit( pFxchMan, *pBeg2, 0 ), + i, k; + + if ( CubeId1 == CubeId2 ) + { + for ( i = 1; pBeg1+i < pEnd1; i++ ) + if ( CubeId1 != Fxch_ManGetLit( pFxchMan, pBeg1[i], 0) ) + break; + + for ( k = 1; pBeg2+k < pEnd2; k++ ) + if ( CubeId1 != Fxch_ManGetLit( pFxchMan, pBeg2[k], 0) ) + break; + + for ( int i_ = 0; i_ < i; i_++ ) + for ( int k_ = 0; k_ < k; k_++ ) + { + if ( pBeg1[i_] == pBeg2[k_] ) + continue; + Fxch_DivFind( Vec_WecEntry( pFxchMan->vCubes, pBeg1[i_] ), + Vec_WecEntry( pFxchMan->vCubes, pBeg2[k_] ), + pFxchMan->vCubeFree ); + + if ( Vec_IntSize( pFxchMan->vCubeFree ) == 4 ) + Fxch_DivNormalize( pFxchMan->vCubeFree ); + + if ( !Vec_IntEqual( pFxchMan->vDiv, pFxchMan->vCubeFree ) ) + continue; + + Vec_IntPush( pFxchMan->vPairs, pBeg1[i_] ); + Vec_IntPush( pFxchMan->vPairs, pBeg2[k_] ); + } + pBeg1 += i; + pBeg2 += k; + } + else if ( CubeId1 < CubeId2 ) + pBeg1++; + else + pBeg2++; + } +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + +ABC_NAMESPACE_IMPL_END |