summaryrefslogtreecommitdiffstats
path: root/src/opt
diff options
context:
space:
mode:
Diffstat (limited to 'src/opt')
-rw-r--r--src/opt/fxu/fxu.c21
-rw-r--r--src/opt/fxu/fxu.h34
-rw-r--r--src/opt/fxu/fxuCreate.c32
-rw-r--r--src/opt/fxu/fxuInt.h8
-rw-r--r--src/opt/fxu/fxuMatrix.c20
-rw-r--r--src/opt/fxu/fxuUpdate.c29
-rw-r--r--src/opt/module.make1
7 files changed, 46 insertions, 99 deletions
diff --git a/src/opt/fxu/fxu.c b/src/opt/fxu/fxu.c
index 4b95b5a5..46f7ca1a 100644
--- a/src/opt/fxu/fxu.c
+++ b/src/opt/fxu/fxu.c
@@ -39,21 +39,14 @@ static int s_MemoryPeak;
Synopsis [Performs fast_extract on a set of covers.]
- Description [All the covers are given in the array p->ppCovers.
- The resulting covers are returned in the array p->ppCoversNew.
- The number of entries in both cover arrays is equal to the number
- of all values in the current nodes plus the max expected number
- of extracted nodes (p->nValuesCi + p->nValuesInt + p->nValuesExtMax).
- The first p->nValuesCi entries, corresponding to the CI nodes, are NULL.
- The next p->nValuesInt entries, corresponding to the int nodes, are covers
- from which the divisors are extracted. The last p->nValuesExtMax entries
- are reserved for the new covers to be extracted. The number of extracted
- covers is returned. This number does not exceed the given number (p->nNodesExt).
+ Description [All the covers are given in the array p->vSops.
+ The resulting covers are returned in the array p->vSopsNew.
+ The entries in these arrays correspond to objects in the network.
+ The entries corresponding to the PI and objects with trivial covers are NULL.
+ The number of extracted covers (not exceeding p->nNodesExt) is returned.
Two other things are important for the correct operation of this procedure:
- (1) The input covers should be SCC-free. (2) The literal array (pCover->pLits)
- is allocated in each cover. The i-th entry in the literal array of a cover
- is the number of the cover in the array p->ppCovers, which represents this
- literal (variable value) in the given cover.]
+ (1) The input covers do not have duplicated fanins and are SCC-free.
+ (2) The fanins array contains the numbers of the fanin objects.]
SideEffects []
diff --git a/src/opt/fxu/fxu.h b/src/opt/fxu/fxu.h
index 5bc1e75f..e9f63ea3 100644
--- a/src/opt/fxu/fxu.h
+++ b/src/opt/fxu/fxu.h
@@ -48,37 +48,8 @@ struct FxuDataStruct
bool fUse0; // set to 1 to have 0-weight also extracted
bool fUseCompl; // set to 1 to have complement taken into account
bool fVerbose; // set to 1 to have verbose output
- int nPairsMax; // the maximum number of cube pairs to consider
-/*
- // parameters of the network
- int fMvNetwork; // the network has some MV nodes
- // the information about nodes
- int nNodesCi; // the number of CI nodes of the network
- int nNodesInt; // the number of internal nodes of the network
- int nNodesOld; // the number of CI and int nodes
- int nNodesNew; // the number of added nodes
- int nNodesExt; // the max number of (binary) nodes to be added by FX
- int nNodesAlloc; // the total number of all nodes
- int * pNode2Value; // for each node, the number of its first value
- // the information about values
- int nValuesCi; // the total number of values of CI nodes
- int nValuesInt; // the total number of values of int nodes
- int nValuesOld; // the number of CI and int values
- int nValuesNew; // the number of values added nodes
- int nValuesExt; // the total number of values of the added nodes
- int nValuesAlloc; // the total number of all values of all nodes
- int * pValue2Node; // for each value, the number of its node
- // the information about covers
- Mvc_Cover_t ** ppCovers; // for each value, the corresponding cover
- Mvc_Cover_t ** ppCoversNew; // for each value, the corresponding cover after FX
- // the MVC manager
- Mvc_Manager_t * pManMvc;
-*/
- // statistics
- int nNodesOld; // the old number of nodes
int nNodesExt; // the number of divisors to extract
- int nNodesNew; // the number of divisors extracted
-
+ int nPairsMax; // the maximum number of cube pairs to consider
// the input information
Vec_Ptr_t * vSops; // the SOPs for each node in the network
Vec_Ptr_t * vFanins; // the fanins of each node in the network
@@ -87,6 +58,9 @@ struct FxuDataStruct
Vec_Ptr_t * vFaninsNew; // the fanins of each node in the network after extraction
// the SOP manager
Extra_MmFlex_t * pManSop;
+ // statistics
+ int nNodesOld; // the old number of nodes
+ int nNodesNew; // the number of divisors actually extracted
};
////////////////////////////////////////////////////////////////////////
diff --git a/src/opt/fxu/fxuCreate.c b/src/opt/fxu/fxuCreate.c
index 04b23fce..b061f53d 100644
--- a/src/opt/fxu/fxuCreate.c
+++ b/src/opt/fxu/fxuCreate.c
@@ -24,21 +24,21 @@
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
-extern int Fxu_PreprocessCubePairs( Fxu_Matrix * p, Vec_Ptr_t * vCovers, int nPairsTotal, int nPairsMax );
-
static void Fxu_CreateMatrixAddCube( Fxu_Matrix * p, Fxu_Cube * pCube, char * pSopCube, Vec_Fan_t * vFanins, int * pOrder );
static int Fxu_CreateMatrixLitCompare( int * ptrX, int * ptrY );
static void Fxu_CreateCoversNode( Fxu_Matrix * p, Fxu_Data_t * pData, int iNode, Fxu_Cube * pCubeFirst, Fxu_Cube * pCubeNext );
static Fxu_Cube * Fxu_CreateCoversFirstCube( Fxu_Matrix * p, Fxu_Data_t * pData, int iNode );
static Abc_Fan_t * s_pLits;
+extern int Fxu_PreprocessCubePairs( Fxu_Matrix * p, Vec_Ptr_t * vCovers, int nPairsTotal, int nPairsMax );
+
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
- Synopsis [Creates the sparse matrix from the array of Sop covers.]
+ Synopsis [Creates the sparse matrix from the array of SOPs.]
Description []
@@ -53,6 +53,7 @@ Fxu_Matrix * Fxu_CreateMatrix( Fxu_Data_t * pData )
Fxu_Var * pVar;
Fxu_Cube * pCubeFirst, * pCubeNew;
Fxu_Cube * pCube1, * pCube2;
+ Vec_Fan_t * vFanins;
char * pSopCover;
char * pSopCube;
int * pOrder, nBitsMax;
@@ -63,12 +64,11 @@ Fxu_Matrix * Fxu_CreateMatrix( Fxu_Data_t * pData )
int nCubes;
int iCube, iPair;
int nFanins;
- Vec_Fan_t * vFanins;
// collect all sorts of statistics
- nCubesTotal = 0;
- nPairsTotal = 0;
- nPairsStore = 0;
+ nCubesTotal = 0;
+ nPairsTotal = 0;
+ nPairsStore = 0;
nBitsMax = -1;
for ( i = 0; i < pData->nNodesOld; i++ )
if ( pSopCover = pData->vSops->pArray[i] )
@@ -158,12 +158,11 @@ Fxu_Matrix * Fxu_CreateMatrix( Fxu_Data_t * pData )
Abc_SopForEachCube( pSopCover, nFanins, pSopCube )
{
// create the cube
- pCubeNew = Fxu_MatrixAddCube( p, pVar, c );
+ pCubeNew = Fxu_MatrixAddCube( p, pVar, c++ );
Fxu_CreateMatrixAddCube( p, pCubeNew, pSopCube, vFanins, pOrder );
if ( pCubeFirst == NULL )
pCubeFirst = pCubeNew;
pCubeNew->pFirst = pCubeFirst;
- c++;
}
// set the first cube of this var
pVar->pFirst = pCubeFirst;
@@ -185,10 +184,7 @@ Fxu_Matrix * Fxu_CreateMatrix( Fxu_Data_t * pData )
// add the var pairs to the heap
Fxu_MatrixComputeSingles( p );
- // allocate temporary storage for pairs
- if ( pData->nPairsMax < 1000 )
- pData->nPairsMax = 1000;
- p->pPairsTemp = ALLOC( Fxu_Pair *, pData->nPairsMax * 10 + 100 );
+ // print stats
if ( pData->fVerbose )
{
double Density;
@@ -254,8 +250,8 @@ void Fxu_CreateMatrixAddCube( Fxu_Matrix * p, Fxu_Cube * pCube, char * pSopCube,
void Fxu_CreateCovers( Fxu_Matrix * p, Fxu_Data_t * pData )
{
Fxu_Cube * pCube, * pCubeFirst, * pCubeNext;
- int iNode, n;
char * pSopCover;
+ int iNode, n;
// get the first cube of the first internal node
pCubeFirst = Fxu_CreateCoversFirstCube( p, pData, 0 );
@@ -306,13 +302,11 @@ void Fxu_CreateCovers( Fxu_Matrix * p, Fxu_Data_t * pData )
void Fxu_CreateCoversNode( Fxu_Matrix * p, Fxu_Data_t * pData, int iNode, Fxu_Cube * pCubeFirst, Fxu_Cube * pCubeNext )
{
Vec_Int_t * vInputsNew;
- char * pSopCover;
- char * pSopCube;
+ char * pSopCover, * pSopCube;
Fxu_Var * pVar;
Fxu_Cube * pCube;
Fxu_Lit * pLit;
int iNum, nCubes, v;
- int fEmptyCube;
// collect positive polarity variable in the cubes between pCubeFirst and pCubeNext
Fxu_MatrixRingVarsStart( p );
@@ -362,7 +356,6 @@ void Fxu_CreateCoversNode( Fxu_Matrix * p, Fxu_Data_t * pData, int iNode, Fxu_Cu
// get hold of the SOP cube
pSopCube = pSopCover + nCubes * (vInputsNew->nSize + 3);
// insert literals
- fEmptyCube = 1;
for ( pLit = pCube->lLits.pHead; pLit; pLit = pLit->pHNext )
{
iNum = pLit->pVar->lLits.nItems; // hack - reuse lLits.nItems
@@ -371,14 +364,13 @@ void Fxu_CreateCoversNode( Fxu_Matrix * p, Fxu_Data_t * pData, int iNode, Fxu_Cu
pSopCube[iNum] = (pLit->pVar->iVar & 1)? '0' : '1'; // reverse CST
else
pSopCube[iNum] = (pLit->pVar->iVar & 1)? '1' : '0'; // no CST
- fEmptyCube = 0;
}
- assert( !fEmptyCube );
// count the cube
nCubes++;
}
assert( nCubes == Abc_SopGetCubeNum(pSopCover) );
+ // set the new cover and the array of fanins
pData->vSopsNew->pArray[iNode] = pSopCover;
pData->vFaninsNew->pArray[iNode] = vInputsNew;
}
diff --git a/src/opt/fxu/fxuInt.h b/src/opt/fxu/fxuInt.h
index 1f5a19b8..59b2df6d 100644
--- a/src/opt/fxu/fxuInt.h
+++ b/src/opt/fxu/fxuInt.h
@@ -25,6 +25,7 @@
#include "util.h"
#include "extra.h"
+#include "vec.h"
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
@@ -158,9 +159,6 @@ struct FxuHeapSingle
// sparse matrix
struct FxuMatrix // ~ 30 words
{
- // information about the network
-// int fMvNetwork; // set to 1 if the network has MV nodes
-// int * pValue2Node; // the mapping of values into nodes
// the cubes
Fxu_ListCube lCubes; // the double linked list of cubes
// the values (binary literals)
@@ -185,9 +183,7 @@ struct FxuMatrix // ~ 30 words
Fxu_Var * pOrderVars;
Fxu_Var ** ppTailVars;
// temporary storage for pairs
- Fxu_Pair ** pPairsTemp;
- int nPairsTemp;
-// int nPairsMax;
+ Vec_Ptr_t * vPairs;
// statistics
int nEntries; // the total number of entries in the sparse matrix
int nDivs1; // the single cube divisors taken
diff --git a/src/opt/fxu/fxuMatrix.c b/src/opt/fxu/fxuMatrix.c
index 0b732aef..503ba2f1 100644
--- a/src/opt/fxu/fxuMatrix.c
+++ b/src/opt/fxu/fxuMatrix.c
@@ -77,6 +77,7 @@ Fxu_Matrix * Fxu_MatrixAllocate()
#endif
p->pHeapDouble = Fxu_HeapDoubleStart();
p->pHeapSingle = Fxu_HeapSingleStart();
+ p->vPairs = Vec_PtrAlloc( 100 );
return p;
}
@@ -132,9 +133,10 @@ void Fxu_MatrixDelete( Fxu_Matrix * p )
Extra_MmFixedStop( p->pMemMan, 0 );
#endif
+ Vec_PtrFree( p->vPairs );
FREE( p->pppPairs );
FREE( p->ppPairs );
- FREE( p->pPairsTemp );
+// FREE( p->pPairsTemp );
FREE( p->pTable );
FREE( p->ppVars );
FREE( p );
@@ -305,20 +307,8 @@ void Fxu_MatrixAddDivisor( Fxu_Matrix * p, Fxu_Cube * pCube1, Fxu_Cube * pCube2
// canonicize the pair
Fxu_PairCanonicize( &pCube1, &pCube2 );
-
-/*
// compute the hash key
- if ( p->fMvNetwork )
-// if ( 0 )
- { // in case of MV network, if all the values in the cube-free divisor
- // belong to the same MV variable, this cube pair is not a divisor
- Key = Fxu_PairHashKeyMv( p, pCube1, pCube2, &nBase, &nLits1, &nLits2 );
- if ( Key == 0 )
- return;
- }
- else
-*/
- Key = Fxu_PairHashKey( p, pCube1, pCube2, &nBase, &nLits1, &nLits2 );
+ Key = Fxu_PairHashKey( p, pCube1, pCube2, &nBase, &nLits1, &nLits2 );
// create the cube pair
pPair = Fxu_PairAlloc( p, pCube1, pCube2 );
@@ -330,11 +320,13 @@ void Fxu_MatrixAddDivisor( Fxu_Matrix * p, Fxu_Cube * pCube1, Fxu_Cube * pCube2
fFound = 0;
Key %= p->nTableSize;
Fxu_TableForEachDouble( p, Key, pDiv )
+ {
if ( Fxu_PairCompare( pPair, pDiv->lPairs.pTail ) ) // they are equal
{
fFound = 1;
break;
}
+ }
if ( !fFound )
{ // create the new divisor
diff --git a/src/opt/fxu/fxuUpdate.c b/src/opt/fxu/fxuUpdate.c
index b781e0b1..4006bc76 100644
--- a/src/opt/fxu/fxuUpdate.c
+++ b/src/opt/fxu/fxuUpdate.c
@@ -287,10 +287,12 @@ void Fxu_UpdateDoublePairs( Fxu_Matrix * p, Fxu_Double * pDouble, Fxu_Var * pVar
// collect and sort the pairs
Fxu_UpdatePairsSort( p, pDouble );
- for ( i = 0; i < p->nPairsTemp; i++ )
+// for ( i = 0; i < p->nPairsTemp; i++ )
+ for ( i = 0; i < p->vPairs->nSize; i++ )
{
// get the pair
- pPair = p->pPairsTemp[i];
+// pPair = p->pPairsTemp[i];
+ pPair = p->vPairs->pArray[i];
// out of the two cubes, select the one which comes earlier
pCubeUse = Fxu_PairMinCube( pPair );
pCubeRem = Fxu_PairMaxCube( pPair );
@@ -312,7 +314,7 @@ void Fxu_UpdateDoublePairs( Fxu_Matrix * p, Fxu_Double * pDouble, Fxu_Var * pVar
// remove the pair
MEM_FREE_FXU( p, Fxu_Pair, 1, pPair );
}
- p->nPairsTemp = 0;
+ p->vPairs->nSize = 0;
}
/**Function*************************************************************
@@ -575,18 +577,17 @@ void Fxu_UpdateMatrixSingleClean( Fxu_Matrix * p, Fxu_Var * pVar1, Fxu_Var * pVa
void Fxu_UpdatePairsSort( Fxu_Matrix * p, Fxu_Double * pDouble )
{
Fxu_Pair * pPair;
- // order the pairs by the first cube to ensure that
- // new literals are added to the matrix from top to bottom
- // collect pairs into the array
- p->nPairsTemp = 0;
+ // order the pairs by the first cube to ensure that new literals are added
+ // to the matrix from top to bottom - collect pairs into the array
+ p->vPairs->nSize = 0;
Fxu_DoubleForEachPair( pDouble, pPair )
- p->pPairsTemp[ p->nPairsTemp++ ] = pPair;
- if ( p->nPairsTemp > 1 )
- { // sort
- qsort( (void *)p->pPairsTemp, p->nPairsTemp, sizeof(Fxu_Pair *),
- (int (*)(const void *, const void *)) Fxu_UpdatePairCompare );
- assert( Fxu_UpdatePairCompare( p->pPairsTemp, p->pPairsTemp + p->nPairsTemp - 1 ) < 0 );
- }
+ Vec_PtrPush( p->vPairs, pPair );
+ if ( p->vPairs->nSize < 2 )
+ return;
+ // sort
+ qsort( (void *)p->vPairs->pArray, p->vPairs->nSize, sizeof(Fxu_Pair *),
+ (int (*)(const void *, const void *)) Fxu_UpdatePairCompare );
+ assert( Fxu_UpdatePairCompare( (Fxu_Pair**)p->vPairs->pArray, (Fxu_Pair**)p->vPairs->pArray + p->vPairs->nSize - 1 ) < 0 );
}
/**Function*************************************************************
diff --git a/src/opt/module.make b/src/opt/module.make
deleted file mode 100644
index d6d908e7..00000000
--- a/src/opt/module.make
+++ /dev/null
@@ -1 +0,0 @@
-SRC +=
generated by cgit v1.2.3 (git 2.25.1) at 2025-04-02 05:24:03 +0000