Skip to content

A
abc
Commit 7a78e303 by Alan Mishchenko
Options

New fast extract.

parent a1ceb761
Showing with 332 additions and 260 deletions
src/base/abc/abcUtil.c
......@@ -2684,6 +2684,53 @@ int Abc_NtkIsTopo( Abc_Ntk_t * pNtk )
return (int)(Counter == 0);
}
/**Function*************************************************************
Synopsis [Reroders fanins of the network.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_NtkOrderFanins( Abc_Ntk_t * pNtk )
{
Vec_Int_t * vOrder;
Abc_Obj_t * pNode;
char * pSop, * pSopNew;
char * pCube, * pCubeNew;
int nVars, i, v, * pOrder;
assert( Abc_NtkIsSopLogic(pNtk) );
vOrder = Vec_IntAlloc( 100 );
Abc_NtkForEachNode( pNtk, pNode, i )
{
pSop = (char *)pNode->pData;
nVars = Abc_SopGetVarNum(pSop);
assert( nVars == Abc_ObjFaninNum(pNode) );
Vec_IntClear( vOrder );
for ( v = 0; v < nVars; v++ )
Vec_IntPush( vOrder, v );
pOrder = Vec_IntArray(vOrder);
Vec_IntSelectSortCost( pOrder, nVars, &pNode->vFanins );
pSopNew = pCubeNew = Abc_SopStart( (Mem_Flex_t *)pNtk->pManFunc, Abc_SopGetCubeNum(pSop), nVars );
Abc_SopForEachCube( pSop, nVars, pCube )
{
for ( v = 0; v < nVars; v++ )
if ( pCube[pOrder[v]] == '0' )
pCubeNew[v] = '0';
else if ( pCube[pOrder[v]] == '1' )
pCubeNew[v] = '1';
pCubeNew += nVars + 3;
}
pNode->pData = pSopNew;
Vec_IntSort( &pNode->vFanins, 0 );
// Vec_IntPrint( vOrder );
}
Vec_IntFree( vOrder );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
......
src/base/abci/abc.c
......@@ -3530,7 +3530,7 @@ int Abc_CommandFastExtract( Abc_Frame_t * pAbc, int argc, char ** argv )
extern int Abc_NtkFxPerform( Abc_Ntk_t * pNtk, int fVerbose );
Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
Fxu_Data_t Params, * p = &Params;
int c, fNewAlgo = 0;
int c, fNewAlgo = 1;
// set the defaults
Abc_NtkSetDefaultParams( p );
Extra_UtilGetoptReset();
......
src/base/abci/abcFx.c
......@@ -29,62 +29,49 @@ ABC_NAMESPACE_IMPL_START
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
extern int Fx_FastExtract( Vec_Wec_t * vCubes, int nVars, int fVerbose );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
typedef struct Fx_Man_t_ Fx_Man_t;
struct Fx_Man_t_
{
// user's data
Vec_Wec_t * vCubes; // cube -> lit
// internal data
Vec_Wec_t * vLits; // lit -> cube
Vec_Int_t * vCounts; // literal counts (currently unused)
Hsh_VecMan_t * pHash; // hash table of divisors
Vec_Flt_t * vWeights; // divisor weights
Vec_Que_t * vPrio; // priority queue
Vec_Int_t * vVarCube; // mapping var into its first cube
// temporary arrays used for updating data-structure after one extraction
Vec_Int_t * vCubesS; // single cubes for the given divisor
Vec_Int_t * vCubesD; // cube pairs for the given divisor
Vec_Int_t * vCompls; // complements of cube pairs
Vec_Int_t * vCubeFree; // cube-free divisor
Vec_Int_t * vDiv; // divisor
// statistics
clock_t timeStart; // starting time
int nVars; // original problem variables
int nLits; // the number of SOP literals
int nDivs; // the number of extracted divisors
int nPairsS; // number of lit pairs
int nPairsD; // number of cube pairs
int nDivsS; // single cube divisors
int nDivMux[3]; // 0 = mux, 1 = compl mux, 2 = no mux
};
Synopsis [Reroders fanins of the network.]
static inline int Fx_ManGetFirstVarCube( Fx_Man_t * p, Vec_Int_t * vCube ) { return Vec_IntEntry( p->vVarCube, Vec_IntEntry(vCube, 0) ); }
Description []
SideEffects []
#define Fx_ManForEachCubeVec( vVec, vCubes, vCube, i ) \
for ( i = 0; (i < Vec_IntSize(vVec)) && ((vCube) = Vec_WecEntry(vCubes, Vec_IntEntry(vVec, i))); i++ )
SeeAlso []
static int Fx_FastExtract( Vec_Wec_t * vCubes, int nVars, int fVerbose );
***********************************************************************/
void Abc_NtkOrderFanins( Abc_Ntk_t * pNtk )
{
Vec_Int_t * vOrder;
Abc_Obj_t * pNode;
char * pSop, * pSopNew;
char * pCube, * pCubeNew;
int nVars, i, v, * pOrder;
assert( Abc_NtkIsSopLogic(pNtk) );
vOrder = Vec_IntAlloc( 100 );
Abc_NtkForEachNode( pNtk, pNode, i )
{
pSop = (char *)pNode->pData;
nVars = Abc_SopGetVarNum(pSop);
assert( nVars == Abc_ObjFaninNum(pNode) );
Vec_IntClear( vOrder );
for ( v = 0; v < nVars; v++ )
Vec_IntPush( vOrder, v );
pOrder = Vec_IntArray(vOrder);
Vec_IntSelectSortCost( pOrder, nVars, &pNode->vFanins );
pSopNew = pCubeNew = Abc_SopStart( (Mem_Flex_t *)pNtk->pManFunc, Abc_SopGetCubeNum(pSop), nVars );
Abc_SopForEachCube( pSop, nVars, pCube )
{
for ( v = 0; v < nVars; v++ )
if ( pCube[pOrder[v]] == '0' )
pCubeNew[v] = '0';
else if ( pCube[pOrder[v]] == '1' )
pCubeNew[v] = '1';
pCubeNew += nVars + 3;
}
pNode->pData = pSopNew;
Vec_IntSort( &pNode->vFanins, 0 );
// Vec_IntPrint( vOrder );
}
Vec_IntFree( vOrder );
}
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Extracts SOP information.]
Synopsis [Retrieves SOP information for fast_extract.]
Description []
......@@ -93,7 +80,7 @@ void Abc_NtkOrderFanins( Abc_Ntk_t * pNtk )
SeeAlso []
***********************************************************************/
Vec_Wec_t * Abc_NtkFxExtract( Abc_Ntk_t * pNtk )
Vec_Wec_t * Abc_NtkFxRetrieve( Abc_Ntk_t * pNtk )
{
Vec_Wec_t * vCubes;
Vec_Int_t * vCube;
......@@ -107,8 +94,7 @@ Vec_Wec_t * Abc_NtkFxExtract( Abc_Ntk_t * pNtk )
pSop = (char *)pNode->pData;
nVars = Abc_SopGetVarNum(pSop);
assert( nVars == Abc_ObjFaninNum(pNode) );
if ( nVars < 2 )
continue;
// if ( nVars < 2 ) continue;
Abc_SopForEachCube( pSop, nVars, pCube )
{
vCube = Vec_WecPushLevel( vCubes );
......@@ -128,7 +114,7 @@ Vec_Wec_t * Abc_NtkFxExtract( Abc_Ntk_t * pNtk )
/**Function*************************************************************
Synopsis [Inserts SOP information.]
Synopsis [Inserts SOP information after fast_extract.]
Description []
......@@ -155,14 +141,12 @@ void Abc_NtkFxInsert( Abc_Ntk_t * pNtk, Vec_Wec_t * vCubes )
// find the largest index
Vec_WecForEachLevel( vCubes, vCube, i )
iNodeMax = Abc_MaxInt( iNodeMax, Vec_IntEntry(vCube, 0) );
// quit if nothing new
/*
// quit if nothing changes
if ( iNodeMax < Abc_NtkObjNumMax(pNtk) )
{
printf( "The network is unchanged by fast extract.\n" );
return;
}
*/
// create new nodes
for ( i = Abc_NtkObjNumMax(pNtk); i <= iNodeMax; i++ )
{
......@@ -183,11 +167,7 @@ void Abc_NtkFxInsert( Abc_Ntk_t * pNtk, Vec_Wec_t * vCubes )
vPres = Vec_IntStartFull( Abc_NtkObjNumMax(pNtk) );
Abc_NtkForEachNode( pNtk, pNode, i )
{
if ( Vec_IntEntry(vCount, i) == 0 )
{
assert( Abc_ObjFaninNum(pNode) < 2 );
continue;
}
// if ( Vec_IntEntry(vCount, i) == 0 ) continue;
Abc_ObjRemoveFanins( pNode );
// create fanins
assert( Vec_IntEntry(vCount, i) > 0 );
......@@ -219,6 +199,7 @@ void Abc_NtkFxInsert( Abc_Ntk_t * pNtk, Vec_Wec_t * vCubes )
}
pCube += Abc_ObjFaninNum(pNode) + 3;
}
// complement SOP if the original one was complemented
if ( pNode->pData && Abc_SopIsComplement((char *)pNode->pData) )
Abc_SopComplement( pSop );
pNode->pData = pSop;
......@@ -279,7 +260,7 @@ int Abc_NtkFxPerform( Abc_Ntk_t * pNtk, int fVerbose )
Abc_NtkCleanup( pNtk, 0 );
// Abc_NtkOrderFanins( pNtk );
// collect information about the covers
vCubes = Abc_NtkFxExtract( pNtk );
vCubes = Abc_NtkFxRetrieve( pNtk );
// call the fast extract procedure
if ( Fx_FastExtract( vCubes, Abc_NtkObjNumMax(pNtk), fVerbose ) > 0 )
{
......@@ -298,43 +279,9 @@ int Abc_NtkFxPerform( Abc_Ntk_t * pNtk, int fVerbose )
typedef struct Fx_Man_t_ Fx_Man_t;
struct Fx_Man_t_
{
Vec_Wec_t * vCubes; // cube -> lit (user data)
Vec_Wec_t * vLits; // lit -> cube
Vec_Int_t * vCounts; // literal counts
Hsh_VecMan_t * pHash; // divisors
Vec_Flt_t * vWeights; // divisor weights
Vec_Que_t * vPrio; // priority queue
Vec_Int_t * vVarCube; // mapping var into its first cube
// temporary arrays used for updating
Vec_Int_t * vCubesS; // single cube divisors
Vec_Int_t * vCubesD; // double cube divisors
Vec_Int_t * vPart0; // cubes of given literal
Vec_Int_t * vPart1; // cubes of given literal
Vec_Int_t * vFree; // cube-free divisor
Vec_Int_t * vCube; // one cube
Vec_Int_t * vDiv; // divisor
// statistics
int nVars; // original problem variables
int nLits; // the number of SOP literals
int nPairsS; // number of lit pairs
int nPairsD; // number of cube pairs
int nDivsS; // single cube divisors
};
static inline int Fx_ManGetFirstVarCube( Fx_Man_t * p, Vec_Int_t * vCube ) { return Vec_IntEntry( p->vVarCube, Vec_IntEntry(vCube, 0) ); }
#define Fx_ManForEachCubeVec( vVec, vCubes, vCube, i ) \
for ( i = 0; (i < Vec_IntSize(vVec)) && ((vCube) = Vec_WecEntry(vCubes, Vec_IntEntry(vVec, i))); i++ )
#define Fx_ManForEachPairVec( vVec, vCubes, vCube1, vCube2, i ) \
for ( i = 0; (i+1 < Vec_IntSize(vVec)) && ((vCube) = Vec_WecEntry(vCubes, Vec_IntEntry(vVec, i))) && ((vCube2) = Vec_WecEntry(vCubes, Vec_IntEntry(vVec, i+1))); i += 2 )
/**Function*************************************************************
Synopsis [Create literals.]
Synopsis [Starting the manager.]
Description []
......@@ -343,60 +290,40 @@ static inline int Fx_ManGetFirstVarCube( Fx_Man_t * p, Vec_Int_t * vCube ) { ret
SeeAlso []
***********************************************************************/
int Fx_ManDivCanonicize( Vec_Int_t * vFree ) // return 1 if complemented
Fx_Man_t * Fx_ManStart( Vec_Wec_t * vCubes )
{
int * A = Vec_IntArray(vFree);
int C[4] = { Abc_Lit2Var(A[0]), Abc_Lit2Var(A[1]), Abc_Lit2Var(A[2]), Abc_Lit2Var(A[3]) };
int L[4] = { Abc_Lit2Var(A[0]), Abc_Lit2Var(A[1]), Abc_Lit2Var(A[2]), Abc_Lit2Var(A[3]) };
int V[4] = { Abc_Lit2Var(L[0]), Abc_Lit2Var(L[1]), Abc_Lit2Var(L[2]), Abc_Lit2Var(L[3]) };
assert( Vec_IntSize(vFree) == 4 );
if ( V[0] == V[1] && V[2] == V[3] ) // 2,2,2
{
assert( !Abc_LitIsCompl(L[0]) );
assert( Abc_LitIsCompl(L[1]) );
if ( !Abc_LitIsCompl(L[2]) )
{
C[2] ^= 2;
C[3] ^= 2;
return 1;
}
return 0;
}
if ( V[0] == V[1] )
{
assert( V[0] != V[2] && V[0] != V[3] );
if ( Abc_LitIsCompl(L[0]) == Abc_LitIsCompl(L[2]) && Abc_LitIsCompl(L[1]) == Abc_LitIsCompl(L[3]) ) // 2,2,3
{
if ( Abc_LitIsCompl(Abc_Lit2Var(L[0])) == Abc_LitIsCompl(Abc_Lit2Var(L[2])) )
{
L[2] = Abc_LitNot(L[2]);
L[3] = Abc_LitNot(L[3]);
return 1;
}
return 0;
}
}
if ( V[0] == V[2] )
{
}
if ( V[0] == V[3] )
{
}
if ( V[1] == V[2] )
{
}
if ( V[1] == V[3] )
{
}
if ( V[2] == V[3] )
{
}
return 0;
Fx_Man_t * p;
p = ABC_CALLOC( Fx_Man_t, 1 );
p->vCubes = vCubes;
// temporary data
p->vCubesS = Vec_IntAlloc( 100 );
p->vCubesD = Vec_IntAlloc( 100 );
p->vCompls = Vec_IntAlloc( 100 );
p->vCubeFree = Vec_IntAlloc( 100 );
p->vDiv = Vec_IntAlloc( 100 );
return p;
}
void Fx_ManStop( Fx_Man_t * p )
{
// Vec_WecFree( p->vCubes );
Vec_WecFree( p->vLits );
Vec_IntFree( p->vCounts );
Hsh_VecManStop( p->pHash );
Vec_FltFree( p->vWeights );
Vec_QueFree( p->vPrio );
Vec_IntFree( p->vVarCube );
// temporary data
Vec_IntFree( p->vCubesS );
Vec_IntFree( p->vCubesD );
Vec_IntFree( p->vCompls );
Vec_IntFree( p->vCubeFree );
Vec_IntFree( p->vDiv );
ABC_FREE( p );
}
/**Function*************************************************************
Synopsis []
Synopsis [Printing procedures.]
Description []
......@@ -406,7 +333,7 @@ int Fx_ManDivCanonicize( Vec_Int_t * vFree ) // return 1 if complemented
***********************************************************************/
static inline char Fx_PrintDivLit( int Lit ) { return (Abc_LitIsCompl(Lit) ? 'A' : 'a') + Abc_Lit2Var(Lit); }
static inline void Fx_PrintDivOne( Vec_Int_t * vDiv )
static inline void Fx_PrintDivOneReal( Vec_Int_t * vDiv )
{
int i, Lit;
Vec_IntForEachEntry( vDiv, Lit, i )
......@@ -417,12 +344,40 @@ static inline void Fx_PrintDivOne( Vec_Int_t * vDiv )
if ( Abc_LitIsCompl(Lit) )
printf( "%c", Fx_PrintDivLit(Abc_Lit2Var(Lit)) );
}
static inline void Fx_PrintDivOne( Vec_Int_t * vDiv )
{
int i, Lit;
Vec_IntForEachEntry( vDiv, Lit, i )
if ( !Abc_LitIsCompl(Lit) )
printf( "%c", Fx_PrintDivLit( Abc_Var2Lit(i, Abc_LitIsCompl(Lit)) ) );
printf( " + " );
Vec_IntForEachEntry( vDiv, Lit, i )
if ( Abc_LitIsCompl(Lit) )
printf( "%c", Fx_PrintDivLit( Abc_Var2Lit(i, Abc_LitIsCompl(Lit)) ) );
}
static inline void Fx_PrintDivArray( Vec_Int_t * vDiv )
{
int i, Lit;
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) );
}
static inline void Fx_PrintDiv( Fx_Man_t * p, int iDiv )
{
printf( "Div %6d : ", iDiv );
printf( "Cost %4d ", (int)Vec_FltEntry(p->vWeights, iDiv) );
int i;
printf( "%4d : ", p->nDivs );
printf( "Div %7d : ", iDiv );
printf( "Weight %5d ", (int)Vec_FltEntry(p->vWeights, iDiv) );
Fx_PrintDivOne( Hsh_VecReadEntry(p->pHash, iDiv) );
printf( "\n" );
for ( i = Vec_IntSize(Hsh_VecReadEntry(p->pHash, iDiv)) + 3; i < 20; i++ )
printf( " " );
printf( "Lits =%7d ", p->nLits );
printf( "Divs =%8d ", Hsh_VecSize(p->pHash) );
Abc_PrintTime( 1, "Time", clock() - p->timeStart );
}
static void Fx_PrintDivisors( Fx_Man_t * p )
{
......@@ -469,20 +424,103 @@ static void Fx_PrintMatrix( Fx_Man_t * p )
}
static void Fx_PrintStats( Fx_Man_t * p, clock_t clk )
{
printf( "Cubes =%6d ", Vec_WecSizeUsed(p->vCubes) );
printf( "Lits =%6d ", Vec_WecSizeUsed(p->vLits) );
printf( "Divs =%6d ", Hsh_VecSize(p->pHash) );
printf( "Divs+ =%6d ", Vec_QueSize(p->vPrio) );
printf( "DivsS =%6d ", p->nDivsS );
printf( "PairS =%6d ", p->nPairsS );
printf( "PairD =%6d ", p->nPairsD );
printf( "Cubes =%7d ", Vec_WecSizeUsed(p->vCubes) );
printf( "Lits =%7d ", Vec_WecSizeUsed(p->vLits) );
printf( "Divs =%7d ", Hsh_VecSize(p->pHash) );
printf( "Divs+ =%7d ", Vec_QueSize(p->vPrio) );
printf( "Compl =%6d ", p->nDivMux[1] );
// printf( "DivsS =%6d ", p->nDivsS );
// printf( "PairS =%6d ", p->nPairsS );
// printf( "PairD =%6d ", p->nPairsD );
Abc_PrintTime( 1, "Time", clk );
// printf( "\n" );
}
/**Function*************************************************************
Synopsis []
Synopsis [Returns 1 if the divisor should be complemented.]
Description [Normalizes the divisor by putting, first, positive control
literal first and, second, positive data1 literal. As the result,
a MUX divisor is (ab + !ac) and an XOR divisor is (ab + !a!b).]
SideEffects []
SeeAlso []
***********************************************************************/
static int Fx_ManDivNormalize( Vec_Int_t * vCubeFree ) // return 1 if complemented
{
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 [Find a cube-free divisor of the two cubes.]
Description []
......@@ -491,39 +529,39 @@ static void Fx_PrintStats( Fx_Man_t * p, clock_t clk )
SeeAlso []
***********************************************************************/
int Fx_ManDivFindCubeFree( Vec_Int_t * vArr1, Vec_Int_t * vArr2, Vec_Int_t * vFree )
int Fx_ManDivFindCubeFree( Vec_Int_t * vArr1, Vec_Int_t * vArr2, Vec_Int_t * vCubeFree )
{
int * pBeg1 = vArr1->pArray + 1;
int * pBeg2 = vArr2->pArray + 1;
int * pBeg1 = vArr1->pArray + 1; // skip variable ID
int * pBeg2 = vArr2->pArray + 1; // skip variable ID
int * pEnd1 = vArr1->pArray + vArr1->nSize;
int * pEnd2 = vArr2->pArray + vArr2->nSize;
int Counter = 0, fAttr0 = 0, fAttr1 = 1;
Vec_IntClear( vFree );
Vec_IntClear( vCubeFree );
while ( pBeg1 < pEnd1 && pBeg2 < pEnd2 )
{
if ( *pBeg1 == *pBeg2 )
pBeg1++, pBeg2++, Counter++;
else if ( *pBeg1 < *pBeg2 )
Vec_IntPush( vFree, Abc_Var2Lit(*pBeg1++, fAttr0) );
Vec_IntPush( vCubeFree, Abc_Var2Lit(*pBeg1++, fAttr0) );
else
{
if ( Vec_IntSize(vFree) == 0 )
if ( Vec_IntSize(vCubeFree) == 0 )
fAttr0 = 1, fAttr1 = 0;
Vec_IntPush( vFree, Abc_Var2Lit(*pBeg2++, fAttr1) );
Vec_IntPush( vCubeFree, Abc_Var2Lit(*pBeg2++, fAttr1) );
}
}
while ( pBeg1 < pEnd1 )
Vec_IntPush( vFree, Abc_Var2Lit(*pBeg1++, fAttr0) );
Vec_IntPush( vCubeFree, Abc_Var2Lit(*pBeg1++, fAttr0) );
while ( pBeg2 < pEnd2 )
Vec_IntPush( vFree, Abc_Var2Lit(*pBeg2++, fAttr1) );
assert( Vec_IntSize(vFree) > 1 ); // the cover is not SCC-free
assert( !Abc_LitIsCompl(Vec_IntEntry(vFree, 0)) );
Vec_IntPush( vCubeFree, Abc_Var2Lit(*pBeg2++, fAttr1) );
assert( Vec_IntSize(vCubeFree) > 1 ); // the cover is not SCC-free
assert( !Abc_LitIsCompl(Vec_IntEntry(vCubeFree, 0)) );
return Counter;
}
/**Function*************************************************************
Synopsis []
Synopsis [Procedures operating on a two-cube divisor.]
Description []
......@@ -553,16 +591,17 @@ static inline void Fx_ManDivFindPivots( Vec_Int_t * vDiv, int * pLit0, int * pLi
return;
}
}
static inline int Fx_ManDivRemoveLits( Vec_Int_t * vCube, Vec_Int_t * vDiv )
static inline int Fx_ManDivRemoveLits( Vec_Int_t * vCube, Vec_Int_t * vDiv, int fCompl )
{
int i, Lit, Count = 0;
assert( !fCompl || Vec_IntSize(vDiv) == 4 );
Vec_IntForEachEntry( vDiv, Lit, i )
Count += Vec_IntRemove1( vCube, Abc_Lit2Var(Lit) );
Count += Vec_IntRemove1( vCube, Abc_Lit2Var(Lit) ^ (fCompl && i > 1) ); // the last two lits can be complemented
return Count;
}
static inline void Fx_ManDivAddLits( Vec_Int_t * vCube, Vec_Int_t * vCube2, Vec_Int_t * vDiv )
{
int i, Lit;
int i, Lit, * pArray;
// Vec_IntClear( vCube );
// Vec_IntClear( vCube2 );
Vec_IntForEachEntry( vDiv, Lit, i )
......@@ -570,11 +609,21 @@ static inline void Fx_ManDivAddLits( Vec_Int_t * vCube, Vec_Int_t * vCube2, Vec_
Vec_IntPush( vCube2, Abc_Lit2Var(Lit) );
else
Vec_IntPush( vCube, Abc_Lit2Var(Lit) );
if ( Vec_IntSize(vDiv) == 4 && Vec_IntSize(vCube) == 3 )
{
assert( Vec_IntSize(vCube2) == 3 );
pArray = Vec_IntArray(vCube);
if ( pArray[1] > pArray[2] )
ABC_SWAP( int, pArray[1], pArray[2] );
pArray = Vec_IntArray(vCube2);
if ( pArray[1] > pArray[2] )
ABC_SWAP( int, pArray[1], pArray[2] );
}
}
/**Function*************************************************************
Synopsis []
Synopsis [Setting up the data-structure.]
Description []
......@@ -628,10 +677,10 @@ int Fx_ManCubeSingleCubeDivisors( Fx_Man_t * p, Vec_Int_t * vPivot, int fRemove,
Vec_IntForEachEntryStart( vPivot, Lit2, n, k+1 )
{
assert( Lit < Lit2 );
Vec_IntClear( p->vFree );
Vec_IntPush( p->vFree, Abc_Var2Lit(Abc_LitNot(Lit), 0) );
Vec_IntPush( p->vFree, Abc_Var2Lit(Abc_LitNot(Lit2), 1) );
iDiv = Hsh_VecManAdd( p->pHash, p->vFree );
Vec_IntClear( p->vCubeFree );
Vec_IntPush( p->vCubeFree, Abc_Var2Lit(Abc_LitNot(Lit), 0) );
Vec_IntPush( p->vCubeFree, Abc_Var2Lit(Abc_LitNot(Lit2), 1) );
iDiv = Hsh_VecManAdd( p->pHash, p->vCubeFree );
if ( !fRemove )
{
if ( Vec_FltSize(p->vWeights) == iDiv )
......@@ -671,33 +720,30 @@ void Fx_ManCubeDoubleCubeDivisors( Fx_Man_t * p, int iFirst, Vec_Int_t * vPivot,
continue;
if ( Vec_IntEntry(vCube, 0) != Vec_IntEntry(vPivot, 0) )
break;
Base = Fx_ManDivFindCubeFree( vCube, vPivot, p->vFree );
/*
if ( fUpdate )
{
printf( "Cubes %2d %2d : ", Vec_WecLevelId(p->vCubes, vCube), Vec_WecLevelId(p->vCubes, vPivot) );
if ( fRemove )
printf( "Rem " );
Base = Fx_ManDivFindCubeFree( vCube, vPivot, p->vCubeFree );
if ( Vec_IntSize(p->vCubeFree) == 4 )
{
int Value = Fx_ManDivNormalize( p->vCubeFree );
if ( Value == 0 )
p->nDivMux[0]++;
else if ( Value == 1 )
p->nDivMux[1]++;
else
printf( "Add " );
Fx_PrintDivOne( p->vFree ); printf( "\n" );
p->nDivMux[2]++;
}
*/
// if ( Vec_IntSize(p->vFree) == 4 )
// Fx_ManDivCanonicize( p->vFree );
iDiv = Hsh_VecManAdd( p->pHash, p->vFree );
iDiv = Hsh_VecManAdd( p->pHash, p->vCubeFree );
if ( !fRemove )
{
if ( iDiv == Vec_FltSize(p->vWeights) )
Vec_FltPush(p->vWeights, -Vec_IntSize(p->vFree));
Vec_FltPush(p->vWeights, -Vec_IntSize(p->vCubeFree));
assert( iDiv < Vec_FltSize(p->vWeights) );
Vec_FltAddToEntry( p->vWeights, iDiv, Base + Vec_IntSize(p->vFree) - 1 );
Vec_FltAddToEntry( p->vWeights, iDiv, Base + Vec_IntSize(p->vCubeFree) - 1 );
p->nPairsD++;
}
else
{
assert( iDiv < Vec_FltSize(p->vWeights) );
Vec_FltAddToEntry( p->vWeights, iDiv, -(Base + Vec_IntSize(p->vFree) - 1) );
Vec_FltAddToEntry( p->vWeights, iDiv, -(Base + Vec_IntSize(p->vCubeFree) - 1) );
p->nPairsD--;
}
if ( fUpdate )
......@@ -736,7 +782,7 @@ void Fx_ManCreateDivisors( Fx_Man_t * p )
/**Function*************************************************************
Synopsis []
Synopsis [Compress the cubes by removing unused ones.]
Description []
......@@ -745,44 +791,19 @@ void Fx_ManCreateDivisors( Fx_Man_t * p )
SeeAlso []
***********************************************************************/
Fx_Man_t * Fx_ManStart( Vec_Wec_t * vCubes )
{
Fx_Man_t * p;
p = ABC_CALLOC( Fx_Man_t, 1 );
p->vCubes = vCubes;
// temporary data
p->vCubesS = Vec_IntAlloc( 100 );
p->vCubesD = Vec_IntAlloc( 100 );
p->vPart0 = Vec_IntAlloc( 100 );
p->vPart1 = Vec_IntAlloc( 100 );
p->vFree = Vec_IntAlloc( 100 );
p->vCube = Vec_IntAlloc( 100 );
p->vDiv = Vec_IntAlloc( 100 );
return p;
}
void Fx_ManStop( Fx_Man_t * p )
static inline void Fx_ManCompressCubes( Vec_Wec_t * vCubes, Vec_Int_t * vLit2Cube )
{
// Vec_WecFree( p->vCubes );
Vec_WecFree( p->vLits );
Vec_IntFree( p->vCounts );
Hsh_VecManStop( p->pHash );
Vec_FltFree( p->vWeights );
Vec_QueFree( p->vPrio );
Vec_IntFree( p->vVarCube );
// temporary data
Vec_IntFree( p->vCubesS );
Vec_IntFree( p->vCubesD );
Vec_IntFree( p->vPart0 );
Vec_IntFree( p->vPart1 );
Vec_IntFree( p->vFree );
Vec_IntFree( p->vCube );
Vec_IntFree( p->vDiv );
ABC_FREE( p );
int i, CubeId, k = 0;
Vec_IntForEachEntry( vLit2Cube, CubeId, i )
if ( Vec_IntSize(Vec_WecEntry(vCubes, CubeId)) > 0 )
Vec_IntWriteEntry( vLit2Cube, k++, CubeId );
Vec_IntShrink( vLit2Cube, k );
}
/**Function*************************************************************
Synopsis []
Synopsis [Find command cube pairs.]
Description []
......@@ -791,27 +812,20 @@ void Fx_ManStop( Fx_Man_t * p )
SeeAlso []
***********************************************************************/
static inline void Fx_ManCompressCubes( Vec_Wec_t * vCubes, Vec_Int_t * vLit2Cube )
{
int i, CubeId, k = 0;
Vec_IntForEachEntry( vLit2Cube, CubeId, i )
if ( Vec_IntSize(Vec_WecEntry(vCubes, CubeId)) > 0 )
Vec_IntWriteEntry( vLit2Cube, k++, CubeId );
Vec_IntShrink( vLit2Cube, k );
}
static inline int Fx_ManGetCubeVar( Vec_Wec_t * vCubes, int iCube ) { return Vec_IntEntry( Vec_WecEntry(vCubes, iCube), 0 ); }
void Fx_ManFindCommonPairs( Vec_Wec_t * vCubes, Vec_Int_t * vPart0, Vec_Int_t * vPart1, Vec_Int_t * vPairs, Vec_Int_t * vDiv, Vec_Int_t * vFree )
static inline int Fx_ManGetCubeVar( Vec_Wec_t * vCubes, int iCube ) { return Vec_IntEntry( Vec_WecEntry(vCubes, iCube), 0 ); }
void Fx_ManFindCommonPairs( Vec_Wec_t * vCubes, Vec_Int_t * vPart0, Vec_Int_t * vPart1, Vec_Int_t * vPairs, Vec_Int_t * vCompls, Vec_Int_t * vDiv, Vec_Int_t * vCubeFree )
{
int * pBeg1 = vPart0->pArray;
int * pBeg2 = vPart1->pArray;
int * pEnd1 = vPart0->pArray + vPart0->nSize;
int * pEnd2 = vPart1->pArray + vPart1->nSize;
int i, k, i_, k_;
int i, k, i_, k_, fCompl, CubeId1, CubeId2;
Vec_IntClear( vPairs );
Vec_IntClear( vCompls );
while ( pBeg1 < pEnd1 && pBeg2 < pEnd2 )
{
int CubeId1 = Fx_ManGetCubeVar(vCubes, *pBeg1);
int CubeId2 = Fx_ManGetCubeVar(vCubes, *pBeg2);
CubeId1 = Fx_ManGetCubeVar(vCubes, *pBeg1);
CubeId2 = Fx_ManGetCubeVar(vCubes, *pBeg2);
if ( CubeId1 == CubeId2 )
{
for ( i = 1; pBeg1+i < pEnd1; i++ )
......@@ -825,11 +839,13 @@ void Fx_ManFindCommonPairs( Vec_Wec_t * vCubes, Vec_Int_t * vPart0, Vec_Int_t *
{
if ( pBeg1[i_] == pBeg2[k_] )
continue;
Fx_ManDivFindCubeFree( Vec_WecEntry(vCubes, pBeg1[i_]), Vec_WecEntry(vCubes, pBeg2[k_]), vFree );
if ( !Vec_IntEqual( vDiv, vFree ) )
Fx_ManDivFindCubeFree( Vec_WecEntry(vCubes, pBeg1[i_]), Vec_WecEntry(vCubes, pBeg2[k_]), vCubeFree );
fCompl = (Vec_IntSize(vCubeFree) == 4 && Fx_ManDivNormalize(vCubeFree) == 1);
if ( !Vec_IntEqual( vDiv, vCubeFree ) )
continue;
Vec_IntPush( vPairs, pBeg1[i_] );
Vec_IntPush( vPairs, pBeg2[k_] );
Vec_IntPush( vCompls, fCompl );
}
pBeg1 += i;
pBeg2 += k;
......@@ -843,7 +859,7 @@ void Fx_ManFindCommonPairs( Vec_Wec_t * vCubes, Vec_Int_t * vPart0, Vec_Int_t *
/**Function*************************************************************
Synopsis [Updates the data-structure when divisor is selected.]
Synopsis [Updates the data-structure when one divisor is selected.]
Description []
......@@ -857,11 +873,12 @@ void Fx_ManUpdate( Fx_Man_t * p, int iDiv )
Vec_Int_t * vCube, * vCube2, * vLitP, * vLitN;
Vec_Int_t * vDiv = p->vDiv;
int nLitsNew = p->nLits - (int)Vec_FltEntry(p->vWeights, iDiv);
int i, k, Lit0, Lit1, iVarNew, RetValue;
// get the divisor
int i, k, Lit0, Lit1, iVarNew, fComplAny, RetValue;
// get the divisor and select pivot variables
p->nDivs++;
Vec_IntClear( vDiv );
Vec_IntAppend( vDiv, Hsh_VecReadEntry(p->pHash, iDiv) );
// select pivot variables
Fx_ManDivFindPivots( vDiv, &Lit0, &Lit1 );
assert( Lit0 >= 0 && Lit1 >= 0 );
......@@ -873,13 +890,11 @@ void Fx_ManUpdate( Fx_Man_t * p, int iDiv )
Fx_ManCompressCubes( p->vCubes, Vec_WecEntry(p->vLits, Abc_LitNot(Lit1)) );
Vec_IntTwoRemoveCommon( Vec_WecEntry(p->vLits, Abc_LitNot(Lit0)), Vec_WecEntry(p->vLits, Abc_LitNot(Lit1)), p->vCubesS );
}
//Vec_IntPrint( p->vCubesS );
// collect double-cube-divisor cube pairs
Fx_ManCompressCubes( p->vCubes, Vec_WecEntry(p->vLits, Lit0) );
Fx_ManCompressCubes( p->vCubes, Vec_WecEntry(p->vLits, Lit1) );
Fx_ManFindCommonPairs( p->vCubes, Vec_WecEntry(p->vLits, Lit0), Vec_WecEntry(p->vLits, Lit1), p->vCubesD, vDiv, p->vFree );
//Vec_IntPrint( p->vCubesD );
Fx_ManFindCommonPairs( p->vCubes, Vec_WecEntry(p->vLits, Lit0), Vec_WecEntry(p->vLits, Lit1), p->vCubesD, p->vCompls, vDiv, p->vCubeFree );
// subtract cost of single-cube divisors
Fx_ManForEachCubeVec( p->vCubesS, p->vCubes, vCube, i )
......@@ -937,18 +952,24 @@ void Fx_ManUpdate( Fx_Man_t * p, int iDiv )
}
// create updated double-cube divisor cube pairs
k = 0;
fComplAny = 0;
assert( Vec_IntSize(p->vCubesD) % 2 == 0 );
Fx_ManForEachPairVec( p->vCubesD, p->vCubes, vCube, vCube2, i )
assert( Vec_IntSize(p->vCubesD) == 2 * Vec_IntSize(p->vCompls) );
for ( i = 0; i < Vec_IntSize(p->vCubesD); i += 2 )
{
RetValue = Fx_ManDivRemoveLits( vCube, vDiv ); // cube 2*i
RetValue += Fx_ManDivRemoveLits( vCube2, vDiv ); // cube 2*i+1
int fCompl = Vec_IntEntry(p->vCompls, i/2);
fComplAny |= fCompl;
vCube = Vec_WecEntry( p->vCubes, Vec_IntEntry(p->vCubesD, i) );
vCube2 = Vec_WecEntry( p->vCubes, Vec_IntEntry(p->vCubesD, i+1) );
RetValue = Fx_ManDivRemoveLits( vCube, vDiv, fCompl ); // cube 2*i
RetValue += Fx_ManDivRemoveLits( vCube2, vDiv, fCompl ); // cube 2*i+1
assert( RetValue == Vec_IntSize(vDiv) );
if ( Vec_IntSize(vDiv) == 2 )
if ( Vec_IntSize(vDiv) == 2 || fCompl )
{
Vec_IntPush( vCube, Abc_Var2Lit(iVarNew, 1) );
Vec_IntPush( vLitN, Vec_WecLevelId(p->vCubes, vCube) );
}
else
else
{
Vec_IntPush( vCube, Abc_Var2Lit(iVarNew, 0) );
Vec_IntPush( vLitP, Vec_WecLevelId(p->vCubes, vCube) );
......@@ -997,9 +1018,14 @@ void Fx_ManUpdate( Fx_Man_t * p, int iDiv )
// remove these cubes from the lit array of the divisor
Vec_IntForEachEntry( vDiv, Lit0, i )
{
Vec_IntTwoRemove( Vec_WecEntry(p->vLits, Abc_Lit2Var(Lit0)), p->vCubesD );
assert( p->nLits == nLitsNew ); // new SOP lits == old SOP lits - divisor weight
if ( fComplAny && i > 1 ) // the last two lits are possibly complemented
Vec_IntTwoRemove( Vec_WecEntry(p->vLits, Abc_LitNot(Abc_Lit2Var(Lit0))), p->vCubesD );
}
// check predicted improvement: (new SOP lits == old SOP lits - divisor weight)
assert( p->nLits == nLitsNew );
}
/**Function*************************************************************
......@@ -1029,6 +1055,7 @@ int Fx_FastExtract( Vec_Wec_t * vCubes, int nVars, int fVerbose )
if ( fVerbose )
Fx_PrintStats( p, clock() - clk );
// perform extraction
p->timeStart = clock();
while ( Vec_QueTopCost(p->vPrio) > 0.0 )
{
int iDiv = Vec_QuePop(p->vPrio);
......@@ -1037,8 +1064,6 @@ int Fx_FastExtract( Vec_Wec_t * vCubes, int nVars, int fVerbose )
Fx_ManUpdate( p, iDiv );
if ( fVeryVerbose )
Fx_PrintMatrix( p );
if ( fVerbose )
Fx_PrintStats( p, clock() - clk );
}
Fx_ManStop( p );
// return the result
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment