61 int * pOrder, nBitsMax;
75 for ( i = 0; i < pData->nNodesOld; i++ )
76 if ( (pSopCover = (
char *)pData->vSops->pArray[i]) )
80 assert( nFanins > 1 && nCubes > 0 );
82 nCubesTotal += nCubes;
83 nPairsTotal += nCubes * (nCubes - 1) / 2;
84 nPairsStore += nCubes * nCubes;
85 if ( nBitsMax < nFanins )
90 printf(
"The current network does not have SOPs to perform extraction.\n" );
94 if ( nPairsStore > 50000000 )
96 printf(
"The problem is too large to be solved by \"fxu\" (%d cubes and %d cube pairs)\n", nCubesTotal, nPairsStore );
103 p->ppVars =
ABC_ALLOC(
Fxu_Var *, 2 * (pData->nNodesOld + pData->nNodesExt) );
104 for ( i = 0; i < 2 * pData->nNodesOld; i++ )
113 for ( i = 0; i < pData->nNodesOld; i++ )
114 if ( (pSopCover = (
char *)pData->vSops->pArray[i]) )
119 pVar = p->ppVars[2*i+1];
124 pVar->
ppPairs = p->pppPairs + iCube;
125 pVar->
ppPairs[0] = p->ppPairs + iPair;
126 for ( v = 1; v < nCubes; v++ )
131 iPair += nCubes * nCubes;
133 assert( iCube == nCubesTotal );
134 assert( iPair == nPairsStore );
140 for ( i = 0; i < pData->nNodesOld; i++ )
141 if ( (pSopCover = (
char *)pData->vSops->pArray[i]) )
144 pVar = p->ppVars[2*i+1];
148 vFanins = (
Vec_Int_t *)pData->vFanins->pArray[i];
152 for ( v = 0; v < nFanins; v++ )
165 if ( pCubeFirst == NULL )
166 pCubeFirst = pCubeNew;
167 pCubeNew->
pFirst = pCubeFirst;
170 pVar->
pFirst = pCubeFirst;
172 if ( nPairsTotal <= pData->nPairsMax )
174 for ( pCube1 = pCubeFirst; pCube1; pCube1 = pCube1->
pNext )
175 for ( pCube2 = pCube1? pCube1->
pNext: NULL; pCube2; pCube2 = pCube2->
pNext )
185 if ( nPairsTotal > 10000000 )
187 printf(
"The total number of cube pairs of the network is more than 10,000,000.\n" );
188 printf(
"Command \"fx\" takes a long time to run in such cases. It is suggested\n" );
189 printf(
"that the user changes the network by reducing the size of logic node and\n" );
190 printf(
"consequently the number of cube pairs to be processed by this command.\n" );
191 printf(
"It can be achieved as follows: \"st; if -K <num>\" or \"st; renode -s -K <num>\"\n" );
192 printf(
"as a proprocessing step, while selecting <num> as approapriate.\n" );
195 if ( nPairsTotal > pData->nPairsMax )
201 if ( p->lVars.nItems > 1000000 )
203 printf(
"The total number of variables is more than 1,000,000.\n" );
204 printf(
"Command \"fx\" takes a long time to run in such cases. It is suggested\n" );
205 printf(
"that the user changes the network by reducing the size of logic node and\n" );
206 printf(
"consequently the number of cube pairs to be processed by this command.\n" );
207 printf(
"It can be achieved as follows: \"st; if -K <num>\" or \"st; renode -s -K <num>\"\n" );
208 printf(
"as a proprocessing step, while selecting <num> as approapriate.\n" );
217 if ( pData->fVerbose )
220 Density = ((double)p->nEntries) / p->lVars.nItems / p->lCubes.nItems;
221 fprintf( stdout,
"Matrix: [vars x cubes] = [%d x %d] ",
222 p->lVars.nItems, p->lCubes.nItems );
223 fprintf( stdout,
"Lits = %d Density = %.5f%%\n",
224 p->nEntries, Density );
225 fprintf( stdout,
"1-cube divs = %6d. (Total = %6d) ", p->lSingles.nItems, p->nSingleTotal );
226 fprintf( stdout,
"2-cube divs = %6d. (Total = %6d)", p->nDivsTotal, nPairsTotal );
227 fprintf( stdout,
"\n" );
252 Value = pSopCube[pOrder[i]];
255 pVar = p->ppVars[ 2 * vFanins->pArray[pOrder[i]] + 1 ];
258 else if ( Value ==
'1' )
260 pVar = p->ppVars[ 2 * vFanins->pArray[pOrder[i]] ];
280 Fxu_Cube * pCube, * pCubeFirst, * pCubeNext;
288 for ( n = 0; n < pData->nNodesOld; n++ )
289 if ( (pSopCover = (
char *)pData->vSops->pArray[n]) )
296 for ( pCube = pCubeFirst; pCube != pCubeNext; pCube = pCube->
pNext )
299 if ( pCube != pCubeNext )
302 pCubeFirst = pCubeNext;
306 for ( n = 0; n < pData->nNodesNew; n++ )
309 iNode = pData->nNodesOld + n;
315 pCubeFirst = pCubeNext;
333 char * pSopCover, * pSopCube;
341 for ( pCube = pCubeFirst; pCube != pCubeNext; pCube = pCube->
pNext )
344 pVar = p->ppVars[ 2 * (pLit->
pVar->
iVar/2) + 1 ];
345 if ( pVar->
pOrder == NULL )
360 for ( v = 0; v < vInputsNew->nSize; v++ )
362 p->ppVars[ 2 * vInputsNew->pArray[v] + 0 ]->lLits.nItems = v;
363 p->ppVars[ 2 * vInputsNew->pArray[v] + 1 ]->lLits.nItems = v;
368 for ( pCube = pCubeFirst; pCube != pCubeNext; pCube = pCube->
pNext )
373 pSopCover =
Abc_SopStart( pData->pManSop, nCubes, vInputsNew->nSize );
375 if ( iNode < pData->nNodesOld &&
Abc_SopGetPhase( (
char *)pData->vSops->pArray[iNode] ) == 0 )
380 for ( pCube = pCubeFirst; pCube != pCubeNext; pCube = pCube->
pNext )
385 pSopCube = pSopCover + nCubes * (vInputsNew->nSize + 3);
390 assert( iNum < vInputsNew->nSize );
391 if ( pLit->
pVar->
iVar / 2 < pData->nNodesOld )
392 pSopCube[iNum] = (pLit->
pVar->
iVar & 1)?
'0' :
'1';
394 pSopCube[iNum] = (pLit->
pVar->
iVar & 1)?
'1' :
'0';
402 pData->vSopsNew->pArray[iNode] = pSopCover;
403 pData->vFaninsNew->pArray[iNode] = vInputsNew;
421 for ( v = iVar; v < pData->nNodesOld + pData->nNodesNew; v++ )
422 if ( p->ppVars[ 2*v + 1 ]->pFirst )
423 return p->ppVars[ 2*v + 1 ]->
pFirst;
ABC_DLL char * Abc_SopStart(Mem_Flex_t *pMan, int nCubes, int nVars)
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Fxu_Matrix * Fxu_MatrixAllocate()
DECLARATIONS ///.
static ABC_NAMESPACE_IMPL_START void Fxu_CreateMatrixAddCube(Fxu_Matrix *p, Fxu_Cube *pCube, char *pSopCube, Vec_Int_t *vFanins, int *pOrder)
DECLARATIONS ///.
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
void Fxu_MatrixAddDivisor(Fxu_Matrix *p, Fxu_Cube *pCube1, Fxu_Cube *pCube2)
#define Abc_SopForEachCube(pSop, nFanins, pCube)
ABC_DLL int Abc_SopGetCubeNum(char *pSop)
typedefABC_NAMESPACE_HEADER_START struct FxuDataStruct Fxu_Data_t
INCLUDES ///.
#define Fxu_MatrixForEachVarInRing(Matrix, Var)
#define ABC_ALLOC(type, num)
#define Abc_CubeForEachVar(pCube, Value, i)
static Fxu_Cube * Fxu_CreateCoversFirstCube(Fxu_Matrix *p, Fxu_Data_t *pData, int iNode)
static void Vec_IntSort(Vec_Int_t *p, int fReverse)
void Fxu_MatrixComputeSingles(Fxu_Matrix *p, int fUse0, int nSingleMax)
FUNCTION DEFINITIONS ///.
void Fxu_MatrixAddLiteral(Fxu_Matrix *p, Fxu_Cube *pCube, Fxu_Var *pVar)
#define Fxu_MatrixRingVarsStart(Matrix)
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
#define ABC_NAMESPACE_IMPL_END
Fxu_Cube * Fxu_MatrixAddCube(Fxu_Matrix *p, Fxu_Var *pVar, int iCube)
void Fxu_MatrixRingVarsUnmark(Fxu_Matrix *p)
static void Vec_IntPush(Vec_Int_t *p, int Entry)
#define Fxu_MatrixRingVarsAdd(Matrix, Var)
#define ABC_NAMESPACE_IMPL_START
ABC_DLL void Abc_SopComplement(char *pSop)
void Fxu_CreateCovers(Fxu_Matrix *p, Fxu_Data_t *pData)
ABC_DLL int Abc_SopGetVarNum(char *pSop)
#define Fxu_MatrixRingVarsStop(Matrix)
typedefABC_NAMESPACE_HEADER_START struct FxuMatrix Fxu_Matrix
INCLUDES ///.
Fxu_Matrix * Fxu_CreateMatrix(Fxu_Data_t *pData)
FUNCTION DEFINITIONS ///.
int Fxu_PreprocessCubePairs(Fxu_Matrix *p, Vec_Ptr_t *vCovers, int nPairsTotal, int nPairsMax)
FUNCTION DEFINITIONS ///.
Fxu_Var * Fxu_MatrixAddVar(Fxu_Matrix *p)
static int Fxu_CreateMatrixLitCompare(int *ptrX, int *ptrY)
ABC_DLL int Abc_SopGetPhase(char *pSop)
static void Fxu_CreateCoversNode(Fxu_Matrix *p, Fxu_Data_t *pData, int iNode, Fxu_Cube *pCubeFirst, Fxu_Cube *pCubeNext)