| /**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; | |
| int SC0_Lit0, | |
| SC0_Lit1, | |
| SC1_Lit0, | |
| SC1_Lit1; | |
| int Cube0Size, | |
| Cube1Size; | |
| Vec_IntClear( pFxchMan->vCubeFree ); | |
| 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 ) | |
| { | |
| int RetValue; | |
| SC0_Lit1 = Fxch_ManGetLit( pFxchMan, pSubCube0->iCube, pSubCube0->iLit1 ); | |
| SC1_Lit1 = Fxch_ManGetLit( pFxchMan, pSubCube1->iCube, pSubCube1->iLit1 ); | |
| if ( SC0_Lit0 < SC1_Lit0 ) | |
| { | |
| 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 ) ); | |
| } | |
| else | |
| { | |
| Vec_IntPush( pFxchMan->vCubeFree, Abc_Var2Lit( SC1_Lit0, 0 ) ); | |
| Vec_IntPush( pFxchMan->vCubeFree, Abc_Var2Lit( SC0_Lit0, 1 ) ); | |
| Vec_IntPush( pFxchMan->vCubeFree, Abc_Var2Lit( SC1_Lit1, 0 ) ); | |
| Vec_IntPush( pFxchMan->vCubeFree, Abc_Var2Lit( SC0_Lit1, 1 ) ); | |
| } | |
| 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 ) ); | |
| } | |
| 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 ) ) | |
| { | |
| 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 ) ); | |
| } | |
| 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 /// | |
| //////////////////////////////////////////////////////////////////////// | |
| ABC_NAMESPACE_IMPL_END |