summaryrefslogtreecommitdiffstats
path: root/src/opt/lpk
diff options
context:
space:
mode:
Diffstat (limited to 'src/opt/lpk')
-rw-r--r--src/opt/lpk/lpk.h1
-rw-r--r--src/opt/lpk/lpkCore.c258
-rw-r--r--src/opt/lpk/lpkCut.c14
-rw-r--r--src/opt/lpk/lpkInt.h6
-rw-r--r--src/opt/lpk/lpkMan.c2
-rw-r--r--src/opt/lpk/lpkMap.c194
-rw-r--r--src/opt/lpk/lpkMux.c163
-rw-r--r--src/opt/lpk/lpkSets.c55
8 files changed, 389 insertions, 304 deletions
diff --git a/src/opt/lpk/lpk.h b/src/opt/lpk/lpk.h
index 092b43e1..f1dcd528 100644
--- a/src/opt/lpk/lpk.h
+++ b/src/opt/lpk/lpk.h
@@ -47,6 +47,7 @@ struct Lpk_Par_t_
int nGrowthLevel; // (L) the maximum increase in the node level after resynthesis
int fSatur; // iterate till saturation
int fZeroCost; // accept zero-cost replacements
+ int fFirst; // use root node and first cut only
int fVerbose; // the verbosiness flag
int fVeryVerbose; // additional verbose info printout
// internal parameters
diff --git a/src/opt/lpk/lpkCore.c b/src/opt/lpk/lpkCore.c
index cbd971e3..aa0368a9 100644
--- a/src/opt/lpk/lpkCore.c
+++ b/src/opt/lpk/lpkCore.c
@@ -17,7 +17,7 @@
Revision [$Id: lpkCore.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
***********************************************************************/
-
+
#include "lpkInt.h"
////////////////////////////////////////////////////////////////////////
@@ -30,6 +30,54 @@
/**Function*************************************************************
+ Synopsis [Prepares the mapping manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Lpk_IfManStart( Lpk_Man_t * p )
+{
+ If_Par_t * pPars;
+ assert( p->pIfMan == NULL );
+ // set defaults
+ pPars = ALLOC( If_Par_t, 1 );
+ memset( pPars, 0, sizeof(If_Par_t) );
+ // user-controlable paramters
+ pPars->nLutSize = p->pPars->nLutSize;
+ pPars->nCutsMax = 16;
+ pPars->nFlowIters = 0; // 1
+ pPars->nAreaIters = 0; // 1
+ pPars->DelayTarget = -1;
+ pPars->fPreprocess = 0;
+ pPars->fArea = 1;
+ pPars->fFancy = 0;
+ pPars->fExpRed = 0; //
+ pPars->fLatchPaths = 0;
+ pPars->fSeqMap = 0;
+ pPars->fVerbose = 0;
+ // internal parameters
+ pPars->fTruth = 1;
+ pPars->fUsePerm = 0;
+ pPars->nLatches = 0;
+ pPars->pLutLib = NULL; // Abc_FrameReadLibLut();
+ pPars->pTimesArr = NULL;
+ pPars->pTimesArr = NULL;
+ pPars->fUseBdds = 0;
+ pPars->fUseSops = 0;
+ pPars->fUseCnfs = 0;
+ pPars->fUseMv = 0;
+ // start the mapping manager and set its parameters
+ p->pIfMan = If_ManStart( pPars );
+ If_ManSetupSetAll( p->pIfMan, 1000 );
+ p->pIfMan->pPars->pTimesArr = ALLOC( float, 32 );
+}
+
+/**Function*************************************************************
+
Synopsis [Returns 1 if at least one entry has changed.]
Description []
@@ -63,6 +111,112 @@ int Lpk_NodeHasChanged( Lpk_Man_t * p, int iNode )
/**Function*************************************************************
+ Synopsis [Prepares the mapping manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Lpk_ExploreCut( Lpk_Man_t * p, Lpk_Cut_t * pCut, Kit_DsdNtk_t * pNtk )
+{
+ extern Abc_Obj_t * Abc_NodeFromIf_rec( Abc_Ntk_t * pNtkNew, If_Man_t * pIfMan, If_Obj_t * pIfObj, Vec_Int_t * vCover );
+ Kit_DsdObj_t * pRoot;
+ If_Obj_t * pDriver, * ppLeaves[16];
+ Abc_Obj_t * pLeaf, * pObjNew;
+ int nGain, i, clk;
+// int nOldShared;
+
+ // check special cases
+ pRoot = Kit_DsdNtkRoot( pNtk );
+ if ( pRoot->Type == KIT_DSD_CONST1 )
+ {
+ if ( Kit_DsdLitIsCompl(pNtk->Root) )
+ pObjNew = Abc_NtkCreateNodeConst0( p->pNtk );
+ else
+ pObjNew = Abc_NtkCreateNodeConst1( p->pNtk );
+ Abc_NtkUpdate( p->pObj, pObjNew, p->vLevels );
+ p->nGainTotal += pCut->nNodes - pCut->nNodesDup;
+ return 1;
+ }
+ if ( pRoot->Type == KIT_DSD_VAR )
+ {
+ pObjNew = Abc_NtkObj( p->pNtk, pCut->pLeaves[ Kit_DsdLit2Var(pRoot->pFans[0]) ] );
+ if ( Kit_DsdLitIsCompl(pNtk->Root) ^ Kit_DsdLitIsCompl(pRoot->pFans[0]) )
+ pObjNew = Abc_NtkCreateNodeInv( p->pNtk, pObjNew );
+ Abc_NtkUpdate( p->pObj, pObjNew, p->vLevels );
+ p->nGainTotal += pCut->nNodes - pCut->nNodesDup;
+ return 1;
+ }
+ assert( pRoot->Type == KIT_DSD_AND || pRoot->Type == KIT_DSD_XOR || pRoot->Type == KIT_DSD_PRIME );
+
+ // start the mapping manager
+ if ( p->pIfMan == NULL )
+ Lpk_IfManStart( p );
+
+ // prepare the mapping manager
+ If_ManRestart( p->pIfMan );
+ // create the PI variables
+ for ( i = 0; i < p->pPars->nVarsMax; i++ )
+ ppLeaves[i] = If_ManCreateCi( p->pIfMan );
+ // set the arrival times
+ Lpk_CutForEachLeaf( p->pNtk, pCut, pLeaf, i )
+ p->pIfMan->pPars->pTimesArr[i] = (float)pLeaf->Level;
+ // prepare the PI cuts
+ If_ManSetupCiCutSets( p->pIfMan );
+ // create the internal nodes
+ p->fCalledOnce = 0;
+ p->nCalledSRed = 0;
+ pDriver = Lpk_MapTree_rec( p, pNtk, ppLeaves, pNtk->Root, NULL );
+ if ( pDriver == NULL )
+ return 0;
+ // create the PO node
+ If_ManCreateCo( p->pIfMan, If_Regular(pDriver) );
+
+ // perform mapping
+ p->pIfMan->pPars->fAreaOnly = 1;
+clk = clock();
+ If_ManPerformMappingComb( p->pIfMan );
+p->timeMap += clock() - clk;
+
+ // compute the gain in area
+ nGain = pCut->nNodes - pCut->nNodesDup - (int)p->pIfMan->AreaGlo;
+ if ( p->pPars->fVeryVerbose )
+ printf( " Mffc = %2d. Mapped = %2d. Gain = %3d. Depth increase = %d. SReds = %d.\n",
+ pCut->nNodes - pCut->nNodesDup, (int)p->pIfMan->AreaGlo, nGain, (int)p->pIfMan->RequiredGlo - (int)p->pObj->Level, p->nCalledSRed );
+
+ // quit if there is no gain
+ if ( !(nGain > 0 || (p->pPars->fZeroCost && nGain == 0)) )
+ return 0;
+
+ // quit if depth increases too much
+ if ( (int)p->pIfMan->RequiredGlo > Abc_ObjRequiredLevel(p->pObj) )
+ return 0;
+
+ // perform replacement
+ p->nGainTotal += nGain;
+ p->nChanges++;
+ if ( p->nCalledSRed )
+ p->nBenefited++;
+
+ // prepare the mapping manager
+ If_ManCleanNodeCopy( p->pIfMan );
+ If_ManCleanCutData( p->pIfMan );
+ // set the PIs of the cut
+ Lpk_CutForEachLeaf( p->pNtk, pCut, pLeaf, i )
+ If_ObjSetCopy( If_ManCi(p->pIfMan, i), pLeaf );
+ // get the area of mapping
+ pObjNew = Abc_NodeFromIf_rec( p->pNtk, p->pIfMan, If_Regular(pDriver), p->vCover );
+ pObjNew->pData = Hop_NotCond( pObjNew->pData, If_IsComplement(pDriver) );
+ // perform replacement
+ Abc_NtkUpdate( p->pObj, pObjNew, p->vLevels );
+ return 1;
+}
+
+/**Function*************************************************************
+
Synopsis [Performs resynthesis for one node.]
Description []
@@ -74,13 +228,13 @@ int Lpk_NodeHasChanged( Lpk_Man_t * p, int iNode )
***********************************************************************/
int Lpk_ResynthesizeNode( Lpk_Man_t * p )
{
+ static int Count = 0;
+ char * pFileName;
Kit_DsdNtk_t * pDsdNtk;
Lpk_Cut_t * pCut;
unsigned * pTruth;
void * pDsd = NULL;
- int i, RetValue, clk;
-
- Lpk_Cut_t * pCutMax;
+ int i, nSuppSize, RetValue, clk;
// compute the cuts
clk = clock();
@@ -91,17 +245,6 @@ p->timeCuts += clock() - clk;
}
p->timeCuts += clock() - clk;
- // find the max volume cut
- pCutMax = NULL;
- for ( i = 0; i < p->nEvals; i++ )
- {
- pCut = p->pCuts + p->pEvals[i];
- if ( pCutMax == NULL || pCutMax->nNodes < pCut->nNodes )
- pCutMax = pCut;
- }
- assert( pCutMax != NULL );
-
-
if ( p->pPars->fVeryVerbose )
printf( "Node %5d : Mffc size = %5d. Cuts = %5d.\n", p->pObj->Id, p->nMffc, p->nEvals );
// try the good cuts
@@ -111,20 +254,34 @@ p->timeCuts += clock() - clk;
{
// get the cut
pCut = p->pCuts + p->pEvals[i];
+ if ( p->pPars->fFirst && i == 1 )
+ break;
- if ( pCut != pCutMax )
- continue;
+ if ( p->pObj->Id == 8835 )
+ {
+ int x = 0;
+ }
// compute the truth table
clk = clock();
pTruth = Lpk_CutTruth( p, pCut );
+ nSuppSize = Extra_TruthSupportSize(pTruth, pCut->nLeaves);
p->timeTruth += clock() - clk;
-clk = clock();
- pDsdNtk = Kit_DsdDeriveNtk( pTruth, pCut->nLeaves, p->pPars->nLutSize );
-p->timeEval += clock() - clk;
+ pDsdNtk = Kit_DsdDecompose( pTruth, pCut->nLeaves );
+// Kit_DsdVerify( pDsdNtk, pTruth, pCut->nLeaves );
+ // skip 16-input non-DSD because ISOP will not work
+ if ( Kit_DsdNtkRoot(pDsdNtk)->nFans == 16 )
+ {
+ Kit_DsdNtkFree( pDsdNtk );
+ continue;
+ }
- if ( Kit_DsdNtkRoot(pDsdNtk)->nFans == 16 ) // skip 16-input non-DSD because ISOP will not work
+ // if DSD has nodes that require splitting to fit them into LUTs
+ // we can skip those cuts that cannot lead to improvement
+ // (a full DSD network requires V = Nmin * (K-1) + 1 for improvement)
+ if ( Kit_DsdNonDsdSizeMax(pDsdNtk) > p->pPars->nLutSize &&
+ nSuppSize >= ((int)pCut->nNodes - (int)pCut->nNodesDup - 1) * (p->pPars->nLutSize - 1) + 1 )
{
Kit_DsdNtkFree( pDsdNtk );
continue;
@@ -133,15 +290,18 @@ p->timeEval += clock() - clk;
if ( p->pPars->fVeryVerbose )
{
printf( " C%02d: L= %2d/%2d V= %2d/%d N= %d W= %4.2f ",
- i, pCut->nLeaves, Extra_TruthSupportSize(pTruth, pCut->nLeaves), pCut->nNodes, pCut->nNodesDup, pCut->nLuts, pCut->Weight );
+ i, pCut->nLeaves, nSuppSize, pCut->nNodes, pCut->nNodesDup, pCut->nLuts, pCut->Weight );
Kit_DsdPrint( stdout, pDsdNtk );
+// Kit_DsdPrintFromTruth( pTruth, pCut->nLeaves );
+ pFileName = Kit_TruthDumpToFile( pTruth, pCut->nLeaves, Count++ );
+ printf( "Saved truth table in file \"%s\".\n", pFileName );
}
// update the network
clk = clock();
- RetValue = Lpk_CutExplore( p, pCut, pDsdNtk );
+ RetValue = Lpk_ExploreCut( p, pCut, pDsdNtk );
+p->timeEval += clock() - clk;
Kit_DsdNtkFree( pDsdNtk );
-p->timeMap += clock() - clk;
if ( RetValue )
break;
}
@@ -187,16 +347,28 @@ int Lpk_Resynthesize( Abc_Ntk_t * pNtk, Lpk_Par_t * pPars )
pPars->nLutsMax, pPars->nLutSize, pPars->nLutsOver, pPars->nVarsShared, pPars->nVarsMax );
}
- // convert logic to AIGs
- Abc_NtkToAig( pNtk );
+
+ // convert into the AIG
+ if ( !Abc_NtkToAig(pNtk) )
+ {
+ fprintf( stdout, "Converting to BDD has failed.\n" );
+ return 0;
+ }
+ assert( Abc_NtkHasAig(pNtk) );
+
+ // set the number of levels
+ Abc_NtkLevel( pNtk );
+ Abc_NtkStartReverseLevels( pNtk, pPars->nGrowthLevel );
// start the manager
p = Lpk_ManStart( pPars );
p->pNtk = pNtk;
p->nNodesTotal = Abc_NtkNodeNum(pNtk);
- p->vLevels = Vec_VecStart( 3 * Abc_NtkLevel(pNtk) ); // computes levels of all nodes
+ p->vLevels = Vec_VecStart( pNtk->LevelMax );
if ( p->pPars->fSatur )
p->vVisited = Vec_VecStart( 0 );
+ if ( pPars->fVerbose )
+ p->nTotalNets = Abc_NtkGetTotalFanins(pNtk);
// iterate over the network
nNodesPrev = p->nNodesTotal;
@@ -213,8 +385,11 @@ int Lpk_Resynthesize( Abc_Ntk_t * pNtk, Lpk_Par_t * pPars )
Abc_NtkForEachNode( pNtk, pObj, i )
{
// skip all except the final node
-// if ( !Abc_ObjIsCo(Abc_ObjFanout0(pObj)) )
-// continue;
+ if ( pPars->fFirst )
+ {
+ if ( !Abc_ObjIsCo(Abc_ObjFanout0(pObj)) )
+ continue;
+ }
if ( i >= nNodes )
break;
@@ -227,8 +402,8 @@ int Lpk_Resynthesize( Abc_Ntk_t * pNtk, Lpk_Par_t * pPars )
p->pObj = pObj;
Lpk_ResynthesizeNode( p );
- if ( p->nChanges == 3 )
- break;
+// if ( p->nChanges == 3 )
+// break;
}
if ( !pPars->fVeryVerbose )
Extra_ProgressBarStop( pProgress );
@@ -241,19 +416,30 @@ int Lpk_Resynthesize( Abc_Ntk_t * pNtk, Lpk_Par_t * pPars )
if ( !p->pPars->fSatur )
break;
- break;
+ if ( pPars->fFirst )
+ break;
}
+ Abc_NtkStopReverseLevels( pNtk );
if ( pPars->fVerbose )
{
- printf( "N = %5d (%3d) Cut = %5d (%4d) Change = %5d Gain = %5d (%5.2f %%) Iter = %2d\n",
- p->nNodesTotal, p->nNodesOver, p->nCutsTotal, p->nCutsUseful, p->nChanges, p->nGainTotal, 100.0 * p->nGainTotal / p->nNodesTotal, Iter );
- printf( "Non_DSD blocks: " );
+ p->nTotalNets2 = Abc_NtkGetTotalFanins(pNtk);
+ printf( "Reduction in nodes = %5d. (%.2f %%) ",
+ p->nGainTotal, 100.0 * p->nGainTotal / p->nNodesTotal );
+ printf( "Reduction in edges = %5d. (%.2f %%) ",
+ p->nTotalNets-p->nTotalNets2, 100.0*(p->nTotalNets-p->nTotalNets2)/p->nTotalNets );
+ printf( "\n" );
+
+ printf( "Nodes = %5d (%3d) Cuts = %5d (%4d) Changes = %5d Iter = %2d Benefit = %d.\n",
+ p->nNodesTotal, p->nNodesOver, p->nCutsTotal, p->nCutsUseful, p->nChanges, Iter, p->nBenefited );
+ printf( "Non-DSD:" );
for ( i = 3; i <= pPars->nVarsMax; i++ )
if ( p->nBlocks[i] )
- printf( "%d=%d ", i, p->nBlocks[i] );
+ printf( " %d=%d", i, p->nBlocks[i] );
printf( "\n" );
+
p->timeTotal = clock() - clk;
+ p->timeEval = p->timeEval - p->timeMap;
p->timeOther = p->timeTotal - p->timeCuts - p->timeTruth - p->timeEval - p->timeMap;
PRTP( "Cuts ", p->timeCuts, p->timeTotal );
PRTP( "Truth ", p->timeTruth, p->timeTotal );
diff --git a/src/opt/lpk/lpkCut.c b/src/opt/lpk/lpkCut.c
index 251ec829..12dae15b 100644
--- a/src/opt/lpk/lpkCut.c
+++ b/src/opt/lpk/lpkCut.c
@@ -545,11 +545,11 @@ int Lpk_NodeCuts( Lpk_Man_t * p )
pCut = p->pCuts + i;
if ( pCut->nLeaves < 2 )
continue;
- // compute the number of LUTs neede to implement this cut
+ // compute the minimum number of LUTs needed to implement this cut
// V = N * (K-1) + 1 ~~~~~ N = Ceiling[(V-1)/(K-1)] = (V-1)/(K-1) + [(V-1)%(K-1) > 0]
pCut->nLuts = (pCut->nLeaves-1)/(p->pPars->nLutSize-1) + ( (pCut->nLeaves-1)%(p->pPars->nLutSize-1) > 0 );
pCut->Weight = (float)1.0 * (pCut->nNodes - pCut->nNodesDup) / pCut->nLuts; //p->pPars->nLutsMax;
- if ( pCut->Weight <= 1.0 )
+ if ( pCut->Weight <= 1.001 )
continue;
pCut->fHasDsd = Lpk_NodeCutsCheckDsd( p, pCut );
if ( pCut->fHasDsd )
@@ -566,7 +566,7 @@ int Lpk_NodeCuts( Lpk_Man_t * p )
{
pCut = p->pCuts + p->pEvals[i];
pCut2 = p->pCuts + p->pEvals[i+1];
- if ( pCut->Weight >= pCut2->Weight )
+ if ( pCut->Weight >= pCut2->Weight - 0.001 )
continue;
Temp = p->pEvals[i];
p->pEvals[i] = p->pEvals[i+1];
@@ -574,6 +574,14 @@ int Lpk_NodeCuts( Lpk_Man_t * p )
fChanges = 1;
}
} while ( fChanges );
+/*
+ for ( i = 0; i < p->nEvals; i++ )
+ {
+ pCut = p->pCuts + p->pEvals[i];
+ printf( "Cut %3d : W = %5.2f.\n", i, pCut->Weight );
+ }
+ printf( "\n" );
+*/
return 1;
}
diff --git a/src/opt/lpk/lpkInt.h b/src/opt/lpk/lpkInt.h
index fe442302..683e7b92 100644
--- a/src/opt/lpk/lpkInt.h
+++ b/src/opt/lpk/lpkInt.h
@@ -87,6 +87,7 @@ struct Lpk_Man_t_
// temporary variables
int fCofactoring; // working in the cofactoring mode
int fCalledOnce; // limits the depth of MUX cofactoring
+ int nCalledSRed; // the number of called to SRed
int pRefs[LPK_SIZE_MAX]; // fanin reference counters
int pCands[LPK_SIZE_MAX]; // internal nodes pointing only to the leaves
// truth table representation
@@ -94,6 +95,7 @@ struct Lpk_Man_t_
Vec_Ptr_t * vTtNodes; // storage for temporary truth tables of the nodes
// variable sets
Vec_Int_t * vSets[8];
+ Kit_DsdMan_t * pDsdMan;
// statistics
int nNodesTotal; // total number of nodes
int nNodesOver; // nodes with cuts over the limit
@@ -101,6 +103,9 @@ struct Lpk_Man_t_
int nCutsUseful; // useful cuts
int nGainTotal; // the gain in LUTs
int nChanges; // the number of changed nodes
+ int nBenefited; // the number of gainful that benefited from decomposition
+ int nTotalNets;
+ int nTotalNets2;
// counter of non-DSD blocks
int nBlocks[17];
// rutime
@@ -138,7 +143,6 @@ extern int Lpk_NodeCuts( Lpk_Man_t * p );
extern Lpk_Man_t * Lpk_ManStart( Lpk_Par_t * pPars );
extern void Lpk_ManStop( Lpk_Man_t * p );
/*=== lpkMap.c =========================================================*/
-extern int Lpk_CutExplore( Lpk_Man_t * p, Lpk_Cut_t * pCut, Kit_DsdNtk_t * pNtk );
extern If_Obj_t * Lpk_MapPrime( Lpk_Man_t * p, unsigned * pTruth, int nVars, If_Obj_t ** ppLeaves );
extern If_Obj_t * Lpk_MapTree_rec( Lpk_Man_t * p, Kit_DsdNtk_t * pNtk, If_Obj_t ** ppLeaves, int iLit, If_Obj_t * pResult );
/*=== lpkMulti.c =======================================================*/
diff --git a/src/opt/lpk/lpkMan.c b/src/opt/lpk/lpkMan.c
index da8b0e3a..5dd54450 100644
--- a/src/opt/lpk/lpkMan.c
+++ b/src/opt/lpk/lpkMan.c
@@ -54,6 +54,7 @@ Lpk_Man_t * Lpk_ManStart( Lpk_Par_t * pPars )
p->vCover = Vec_IntAlloc( 1 << 12 );
for ( i = 0; i < 8; i++ )
p->vSets[i] = Vec_IntAlloc(100);
+ p->pDsdMan = Kit_DsdManAlloc( pPars->nVarsMax );
return p;
}
@@ -71,6 +72,7 @@ Lpk_Man_t * Lpk_ManStart( Lpk_Par_t * pPars )
void Lpk_ManStop( Lpk_Man_t * p )
{
int i;
+ Kit_DsdManFree( p->pDsdMan );
for ( i = 0; i < 8; i++ )
Vec_IntFree(p->vSets[i]);
if ( p->pIfMan )
diff --git a/src/opt/lpk/lpkMap.c b/src/opt/lpk/lpkMap.c
index c647fdf7..698aeea1 100644
--- a/src/opt/lpk/lpkMap.c
+++ b/src/opt/lpk/lpkMap.c
@@ -24,62 +24,12 @@
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
-extern void Res_UpdateNetworkLevel( Abc_Obj_t * pObjNew, Vec_Vec_t * vLevels );
-
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
- Synopsis [Prepares the mapping manager.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Lpk_IfManStart( Lpk_Man_t * p )
-{
- If_Par_t * pPars;
- assert( p->pIfMan == NULL );
- // set defaults
- pPars = ALLOC( If_Par_t, 1 );
- memset( pPars, 0, sizeof(If_Par_t) );
- // user-controlable paramters
- pPars->nLutSize = p->pPars->nLutSize;
- pPars->nCutsMax = 16;
- pPars->nFlowIters = 0; // 1
- pPars->nAreaIters = 0; // 1
- pPars->DelayTarget = -1;
- pPars->fPreprocess = 0;
- pPars->fArea = 1;
- pPars->fFancy = 0;
- pPars->fExpRed = 0; //
- pPars->fLatchPaths = 0;
- pPars->fSeqMap = 0;
- pPars->fVerbose = 0;
- // internal parameters
- pPars->fTruth = 0;
- pPars->fUsePerm = 0;
- pPars->nLatches = 0;
- pPars->pLutLib = NULL; // Abc_FrameReadLibLut();
- pPars->pTimesArr = NULL;
- pPars->pTimesArr = NULL;
- pPars->fUseBdds = 0;
- pPars->fUseSops = 0;
- pPars->fUseCnfs = 0;
- pPars->fUseMv = 0;
- // start the mapping manager and set its parameters
- p->pIfMan = If_ManStart( pPars );
- If_ManSetupSetAll( p->pIfMan, 1000 );
- p->pIfMan->pPars->pTimesArr = ALLOC( float, 32 );
-}
-
-/**Function*************************************************************
-
Synopsis [Transforms the decomposition graph into the AIG.]
Description []
@@ -154,122 +104,10 @@ If_Obj_t * Lpk_MapPrime( Lpk_Man_t * p, unsigned * pTruth, int nVars, If_Obj_t *
SeeAlso []
***********************************************************************/
-int Lpk_CutExplore( Lpk_Man_t * p, Lpk_Cut_t * pCut, Kit_DsdNtk_t * pNtk )
-{
- extern Abc_Obj_t * Abc_NodeFromIf_rec( Abc_Ntk_t * pNtkNew, If_Man_t * pIfMan, If_Obj_t * pIfObj, Vec_Int_t * vCover );
- Kit_DsdObj_t * pRoot;
- If_Obj_t * pDriver, * ppLeaves[16];
- Abc_Obj_t * pLeaf, * pObjNew;
- int nGain, i;
-// int nOldShared;
-
- // check special cases
- pRoot = Kit_DsdNtkRoot( pNtk );
- if ( pRoot->Type == KIT_DSD_CONST1 )
- {
- if ( Kit_DsdLitIsCompl(pNtk->Root) )
- pObjNew = Abc_NtkCreateNodeConst0( p->pNtk );
- else
- pObjNew = Abc_NtkCreateNodeConst1( p->pNtk );
-
- // perform replacement
- pObjNew->Level = p->pObj->Level;
- Abc_ObjReplace( p->pObj, pObjNew );
- Res_UpdateNetworkLevel( pObjNew, p->vLevels );
- p->nGainTotal += pCut->nNodes - pCut->nNodesDup;
- return 1;
- }
- if ( pRoot->Type == KIT_DSD_VAR )
- {
- pObjNew = Abc_NtkObj( p->pNtk, pCut->pLeaves[ Kit_DsdLit2Var(pRoot->pFans[0]) ] );
- if ( Kit_DsdLitIsCompl(pNtk->Root) ^ Kit_DsdLitIsCompl(pRoot->pFans[0]) )
- pObjNew = Abc_NtkCreateNodeInv( p->pNtk, pObjNew );
-
- // perform replacement
- pObjNew->Level = p->pObj->Level;
- Abc_ObjReplace( p->pObj, pObjNew );
- Res_UpdateNetworkLevel( pObjNew, p->vLevels );
- p->nGainTotal += pCut->nNodes - pCut->nNodesDup;
- return 1;
- }
- assert( pRoot->Type == KIT_DSD_AND || pRoot->Type == KIT_DSD_XOR || pRoot->Type == KIT_DSD_PRIME );
-
- // start the mapping manager
- if ( p->pIfMan == NULL )
- Lpk_IfManStart( p );
-
- // prepare the mapping manager
- If_ManRestart( p->pIfMan );
- // create the PI variables
- for ( i = 0; i < p->pPars->nVarsMax; i++ )
- ppLeaves[i] = If_ManCreateCi( p->pIfMan );
- // set the arrival times
- Lpk_CutForEachLeaf( p->pNtk, pCut, pLeaf, i )
- p->pIfMan->pPars->pTimesArr[i] = (float)pLeaf->Level;
- // prepare the PI cuts
- If_ManSetupCiCutSets( p->pIfMan );
- // create the internal nodes
- p->fCalledOnce = 0;
- pDriver = Lpk_MapTree_rec( p, pNtk, ppLeaves, pNtk->Root, NULL );
- if ( pDriver == NULL )
- return 0;
- // create the PO node
- If_ManCreateCo( p->pIfMan, If_Regular(pDriver) );
-
- // perform mapping
- p->pIfMan->pPars->fAreaOnly = 1;
- If_ManPerformMappingComb( p->pIfMan );
-
- // compute the gain in area
- nGain = pCut->nNodes - pCut->nNodesDup - (int)p->pIfMan->AreaGlo;
- if ( p->pPars->fVeryVerbose )
- printf( " Mffc = %2d. Mapped = %2d. Gain = %3d. Depth increase = %d.\n",
- pCut->nNodes - pCut->nNodesDup, (int)p->pIfMan->AreaGlo, nGain, (int)p->pIfMan->RequiredGlo - (int)p->pObj->Level );
-
- // quit if there is no gain
- if ( !(nGain > 0 || (p->pPars->fZeroCost && nGain == 0)) )
- return 0;
-
- // quit if depth increases too much
- if ( (int)p->pIfMan->RequiredGlo - (int)p->pObj->Level > p->pPars->nGrowthLevel )
- return 0;
-
- // perform replacement
- p->nGainTotal += nGain;
- p->nChanges++;
-
- // prepare the mapping manager
- If_ManCleanNodeCopy( p->pIfMan );
- If_ManCleanCutData( p->pIfMan );
- // set the PIs of the cut
- Lpk_CutForEachLeaf( p->pNtk, pCut, pLeaf, i )
- If_ObjSetCopy( If_ManCi(p->pIfMan, i), pLeaf );
- // get the area of mapping
- pObjNew = Abc_NodeFromIf_rec( p->pNtk, p->pIfMan, If_Regular(pDriver), p->vCover );
- pObjNew->pData = Hop_NotCond( pObjNew->pData, If_IsComplement(pDriver) );
-
- // perform replacement
- pObjNew->Level = p->pObj->Level;
- Abc_ObjReplace( p->pObj, pObjNew );
- Res_UpdateNetworkLevel( pObjNew, p->vLevels );
- return 1;
-}
-
-/**Function*************************************************************
-
- Synopsis [Prepares the mapping manager.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
If_Obj_t * Lpk_MapTree_rec( Lpk_Man_t * p, Kit_DsdNtk_t * pNtk, If_Obj_t ** ppLeaves, int iLit, If_Obj_t * pResult )
{
Kit_DsdObj_t * pObj;
- If_Obj_t * pObjNew, * pFansNew[16];
+ If_Obj_t * pObjNew = NULL, * pObjNew2 = NULL, * pFansNew[16];
unsigned i, iLitFanin;
assert( iLit >= 0 );
@@ -325,20 +163,38 @@ If_Obj_t * Lpk_MapTree_rec( Lpk_Man_t * p, Kit_DsdNtk_t * pNtk, If_Obj_t ** ppLe
if ( pFansNew[i] == NULL )
return NULL;
}
-/*
+/*
if ( !p->fCofactoring && p->pPars->nVarsShared > 0 && (int)pObj->nFans > p->pPars->nLutSize )
{
pObjNew = Lpk_MapTreeMulti( p, Kit_DsdObjTruth(pObj), pObj->nFans, pFansNew );
return If_NotCond( pObjNew, Kit_DsdLitIsCompl(iLit) );
}
*/
+/*
+ if ( (int)pObj->nFans > p->pPars->nLutSize )
+ {
+ pObjNew2 = Lpk_MapTreeMux_rec( p, Kit_DsdObjTruth(pObj), pObj->nFans, pFansNew );
+// if ( pObjNew2 )
+// return If_NotCond( pObjNew2, Kit_DsdLitIsCompl(iLit) );
+ }
+*/
// find best cofactoring variable
- if ( pObj->nFans > 3 && !p->fCalledOnce )
-// pObjNew = Lpk_MapTreeMux_rec( p, Kit_DsdObjTruth(pObj), pObj->nFans, pFansNew );
- pObjNew = Lpk_MapSuppRedDec_rec( p, Kit_DsdObjTruth(pObj), pObj->nFans, pFansNew );
- else
- pObjNew = Lpk_MapPrime( p, Kit_DsdObjTruth(pObj), pObj->nFans, pFansNew );
+ if ( p->pPars->nVarsShared > 0 && (int)pObj->nFans > p->pPars->nLutSize )
+ {
+ pObjNew2 = Lpk_MapSuppRedDec_rec( p, Kit_DsdObjTruth(pObj), pObj->nFans, pFansNew );
+ if ( pObjNew2 )
+ return If_NotCond( pObjNew2, Kit_DsdLitIsCompl(iLit) );
+ }
+
+ pObjNew = Lpk_MapPrime( p, Kit_DsdObjTruth(pObj), pObj->nFans, pFansNew );
+
+ // add choice
+ if ( pObjNew && pObjNew2 )
+ {
+ If_ObjSetChoice( If_Regular(pObjNew), If_Regular(pObjNew2) );
+ If_ManCreateChoice( p->pIfMan, If_Regular(pObjNew) );
+ }
return If_NotCond( pObjNew, Kit_DsdLitIsCompl(iLit) );
}
diff --git a/src/opt/lpk/lpkMux.c b/src/opt/lpk/lpkMux.c
index d9e013f0..7928f77e 100644
--- a/src/opt/lpk/lpkMux.c
+++ b/src/opt/lpk/lpkMux.c
@@ -39,18 +39,12 @@
SeeAlso []
***********************************************************************/
-int Lpk_MapTreeBestVar( Lpk_Man_t * p, unsigned * pTruth, int nVars )
+int Lpk_MapTreeBestCofVar( Lpk_Man_t * p, unsigned * pTruth, int nVars, unsigned * pCof0, unsigned * pCof1 )
{
-// Kit_DsdNtk_t * ppNtks[2], * pTemp;
- unsigned * pCof0 = Vec_PtrEntry( p->vTtNodes, 0 );
- unsigned * pCof1 = Vec_PtrEntry( p->vTtNodes, 1 );
int i, iBestVar, nSuppSizeCur0, nSuppSizeCur1, nSuppSizeCur, nSuppSizeMin;
-// int nPrimeSizeCur0, nPrimeSizeCur1, nPrimeSizeCur, nPrimeSizeMin;
-
// iterate through variables
iBestVar = -1;
- nSuppSizeMin = ABC_INFINITY;
-// nPrimeSizeMin = ABC_INFINITY;
+ nSuppSizeMin = KIT_INFINITY;
for ( i = 0; i < nVars; i++ )
{
// cofactor the functiona and get support sizes
@@ -59,44 +53,22 @@ int Lpk_MapTreeBestVar( Lpk_Man_t * p, unsigned * pTruth, int nVars )
nSuppSizeCur0 = Kit_TruthSupportSize( pCof0, nVars );
nSuppSizeCur1 = Kit_TruthSupportSize( pCof1, nVars );
nSuppSizeCur = nSuppSizeCur0 + nSuppSizeCur1;
-/*
- // check the size of the largest prime components
- ppNtks[0] = Kit_DsdDecompose( pCof0, nVars );
- ppNtks[1] = Kit_DsdDecompose( pCof1, nVars );
- // compute the largest non-decomp block
- nPrimeSizeCur0 = Kit_DsdNonDsdSizeMax(ppNtks[0]);
- nPrimeSizeCur1 = Kit_DsdNonDsdSizeMax(ppNtks[1]);
- nPrimeSizeCur = KIT_MAX( nPrimeSizeCur0, nPrimeSizeCur1 );
-
- printf( "Evaluating variable %c:\n", 'a'+i );
-// Kit_DsdPrintExpanded( ppNtks[0] );
-// Kit_DsdPrintExpanded( ppNtks[1] );
-
- ppNtks[0] = Kit_DsdExpand( pTemp = ppNtks[0] );
- Kit_DsdNtkFree( pTemp );
-
- ppNtks[1] = Kit_DsdExpand( pTemp = ppNtks[1] );
- Kit_DsdNtkFree( pTemp );
-
- Kit_DsdPrint( stdout, ppNtks[0] );
- Kit_DsdPrint( stdout, ppNtks[1] );
-
-// Lpk_DsdEvalSets( p, ppNtks[0], ppNtks[1] );
-
- // free the networks
- Kit_DsdNtkFree( ppNtks[0] );
- Kit_DsdNtkFree( ppNtks[1] );
-*/
+ // skip cofactoring that goes above the limit
+ if ( nSuppSizeCur0 > p->pPars->nLutSize || nSuppSizeCur1 > p->pPars->nLutSize )
+ continue;
// compare this variable with other variables
- if ( nSuppSizeMin > nSuppSizeCur ) //|| (nSuppSizeMin == nSuppSizeCur && nPrimeSizeMin > nPrimeSizeCur ) )
+ if ( nSuppSizeMin > nSuppSizeCur )
{
nSuppSizeMin = nSuppSizeCur;
-// nPrimeSizeMin = nPrimeSizeCur;
iBestVar = i;
}
}
- printf( "\n" );
- assert( iBestVar != -1 );
+ // cofactor w.r.t. this variable
+ if ( iBestVar != -1 )
+ {
+ Kit_TruthCofactor0New( pCof0, pTruth, nVars, iBestVar );
+ Kit_TruthCofactor1New( pCof1, pTruth, nVars, iBestVar );
+ }
return iBestVar;
}
@@ -113,18 +85,17 @@ int Lpk_MapTreeBestVar( Lpk_Man_t * p, unsigned * pTruth, int nVars )
***********************************************************************/
If_Obj_t * Lpk_MapTreeMux_rec( Lpk_Man_t * p, unsigned * pTruth, int nVars, If_Obj_t ** ppLeaves )
{
- If_Obj_t * pObj0, * pObj1;
- Kit_DsdNtk_t * ppNtks[2];
unsigned * pCof0 = Vec_PtrEntry( p->vTtNodes, 0 );
unsigned * pCof1 = Vec_PtrEntry( p->vTtNodes, 1 );
+ If_Obj_t * pObj0, * pObj1;
+ Kit_DsdNtk_t * ppNtks[2];
int iBestVar;
assert( nVars > 3 );
p->fCalledOnce = 1;
-
// cofactor w.r.t. the best variable
- iBestVar = Lpk_MapTreeBestVar( p, pTruth, nVars );
- Kit_TruthCofactor0New( pCof0, pTruth, nVars, iBestVar );
- Kit_TruthCofactor1New( pCof1, pTruth, nVars, iBestVar );
+ iBestVar = Lpk_MapTreeBestCofVar( p, pTruth, nVars, pCof0, pCof1 );
+ if ( iBestVar == -1 )
+ return NULL;
// decompose the functions
ppNtks[0] = Kit_DsdDecompose( pCof0, nVars );
ppNtks[1] = Kit_DsdDecompose( pCof1, nVars );
@@ -158,7 +129,7 @@ If_Obj_t * Lpk_MapTreeMux_rec( Lpk_Man_t * p, unsigned * pTruth, int nVars, If_O
***********************************************************************/
If_Obj_t * Lpk_MapSuppRedDec_rec( Lpk_Man_t * p, unsigned * pTruth, int nVars, If_Obj_t ** ppLeaves )
{
- Kit_DsdNtk_t * pNtkDec, * pNtkComp;
+ Kit_DsdNtk_t * pNtkDec, * pNtkComp, * ppNtks[2], * pTemp;
If_Obj_t * pObjNew;
unsigned * pCof0 = Vec_PtrEntry( p->vTtNodes, 0 );
unsigned * pCof1 = Vec_PtrEntry( p->vTtNodes, 1 );
@@ -172,80 +143,96 @@ If_Obj_t * Lpk_MapSuppRedDec_rec( Lpk_Man_t * p, unsigned * pTruth, int nVars, I
unsigned * pCo0 = Vec_PtrEntry( p->vTtNodes, 9 );
unsigned * pCo1 = Vec_PtrEntry( p->vTtNodes, 10 );
unsigned * pCo = Vec_PtrEntry( p->vTtNodes, 11 );
- int TrueMint0, TrueMint1;
+ int TrueMint0, TrueMint1, FalseMint0, FalseMint1;
int uSubsets, uSubset0, uSubset1, iVar, iVarReused, i;
// determine if supp-red decomposition exists
uSubsets = Lpk_MapSuppRedDecSelect( p, pTruth, nVars, &iVar, &iVarReused );
if ( uSubsets == 0 )
return NULL;
+ p->nCalledSRed++;
- // get the bound sets
- uSubset0 = uSubsets & 0xFFFF;
- uSubset1 = uSubsets >> 16;
// get the cofactors
Kit_TruthCofactor0New( pCof0, pTruth, nVars, iVar );
Kit_TruthCofactor1New( pCof1, pTruth, nVars, iVar );
- // find any true assignments of the cofactors
- TrueMint0 = Kit_TruthFindFirstBit( pCof0, nVars );
- TrueMint1 = Kit_TruthFindFirstBit( pCof1, nVars );
+
+ // get the bound sets
+ uSubset0 = uSubsets & 0xFFFF;
+ uSubset1 = uSubsets >> 16;
+
+ // compute the decomposed functions
+ ppNtks[0] = Kit_DsdDecompose( pCof0, nVars );
+ ppNtks[1] = Kit_DsdDecompose( pCof1, nVars );
+ ppNtks[0] = Kit_DsdExpand( pTemp = ppNtks[0] ); Kit_DsdNtkFree( pTemp );
+ ppNtks[1] = Kit_DsdExpand( pTemp = ppNtks[1] ); Kit_DsdNtkFree( pTemp );
+ Kit_DsdTruthPartial( p->pDsdMan, ppNtks[0], pDec0, uSubset0 );
+ Kit_DsdTruthPartial( p->pDsdMan, ppNtks[1], pDec1, uSubset1 );
+ Kit_DsdNtkFree( ppNtks[0] );
+ Kit_DsdNtkFree( ppNtks[1] );
+//Kit_DsdPrintFromTruth( pDec0, nVars );
+//Kit_DsdPrintFromTruth( pDec1, nVars );
+ // get the decomposed function
+ Kit_TruthMuxVar( pDec, pDec0, pDec1, nVars, iVar );
+
+ // find any true assignments of the decomposed functions
+ TrueMint0 = Kit_TruthFindFirstBit( pDec0, nVars );
+ TrueMint1 = Kit_TruthFindFirstBit( pDec1, nVars );
assert( TrueMint0 >= 0 && TrueMint1 >= 0 );
+ // find any false assignments of the decomposed functions
+ FalseMint0 = Kit_TruthFindFirstZero( pDec0, nVars );
+ FalseMint1 = Kit_TruthFindFirstZero( pDec1, nVars );
+ assert( FalseMint0 >= 0 && FalseMint1 >= 0 );
+
// cofactor the cofactors according to these minterms
- Kit_TruthCopy( pDec0, pCof0, nVars );
- Kit_TruthCopy( pDec1, pCof1, nVars );
+ Kit_TruthCopy( pCo00, pCof0, nVars );
+ Kit_TruthCopy( pCo01, pCof0, nVars );
for ( i = 0; i < nVars; i++ )
- if ( !(uSubset0 & (1 << i)) )
+ if ( uSubset0 & (1 << i) )
{
+ if ( FalseMint0 & (1 << i) )
+ Kit_TruthCofactor1( pCo00, nVars, i );
+ else
+ Kit_TruthCofactor0( pCo00, nVars, i );
if ( TrueMint0 & (1 << i) )
- Kit_TruthCofactor1( pDec0, nVars, i );
+ Kit_TruthCofactor1( pCo01, nVars, i );
else
- Kit_TruthCofactor0( pDec0, nVars, i );
+ Kit_TruthCofactor0( pCo01, nVars, i );
}
+ Kit_TruthCopy( pCo10, pCof1, nVars );
+ Kit_TruthCopy( pCo11, pCof1, nVars );
for ( i = 0; i < nVars; i++ )
- if ( !(uSubset1 & (1 << i)) )
+ if ( uSubset1 & (1 << i) )
{
+ if ( FalseMint1 & (1 << i) )
+ Kit_TruthCofactor1( pCo10, nVars, i );
+ else
+ Kit_TruthCofactor0( pCo10, nVars, i );
if ( TrueMint1 & (1 << i) )
- Kit_TruthCofactor1( pDec1, nVars, i );
+ Kit_TruthCofactor1( pCo11, nVars, i );
else
- Kit_TruthCofactor0( pDec1, nVars, i );
+ Kit_TruthCofactor0( pCo11, nVars, i );
}
- // get the decomposed function
- Kit_TruthMuxVar( pDec, pDec0, pDec1, nVars, iVar );
- // derive the remainders
- Kit_TruthAndPhase( pCo00, pCof0, pDec0, nVars, 0, 1 );
- Kit_TruthAndPhase( pCo01, pCof0, pDec0, nVars, 0, 0 );
- Kit_TruthAndPhase( pCo10, pCof1, pDec1, nVars, 0, 1 );
- Kit_TruthAndPhase( pCo11, pCof1, pDec1, nVars, 0, 0 );
- // quantify bound set variables
- for ( i = 0; i < nVars; i++ )
- if ( uSubset0 & (1 << i) )
- {
- Kit_TruthExist( pCo00, nVars, i );
- Kit_TruthExist( pCo01, nVars, i );
- }
- for ( i = 0; i < nVars; i++ )
- if ( uSubset1 & (1 << i) )
- {
- Kit_TruthExist( pCo10, nVars, i );
- Kit_TruthExist( pCo11, nVars, i );
- }
// derive the functions by composing them with the new variable (iVarReused)
Kit_TruthMuxVar( pCo0, pCo00, pCo01, nVars, iVarReused );
Kit_TruthMuxVar( pCo1, pCo10, pCo11, nVars, iVarReused );
+//Kit_DsdPrintFromTruth( pCo0, nVars );
+//Kit_DsdPrintFromTruth( pCo1, nVars );
// derive the composition function
Kit_TruthMuxVar( pCo , pCo0 , pCo1 , nVars, iVar );
// process the decomposed function
pNtkDec = Kit_DsdDecompose( pDec, nVars );
- Kit_DsdPrint( stdout, pNtkDec );
- ppLeaves[iVarReused] = Lpk_MapTree_rec( p, pNtkDec, ppLeaves, pNtkDec->Root, NULL );
- Kit_DsdNtkFree( pNtkDec );
-
- // process the composition function
pNtkComp = Kit_DsdDecompose( pCo, nVars );
- Kit_DsdPrint( stdout, pNtkComp );
+//Kit_DsdPrint( stdout, pNtkDec );
+//Kit_DsdPrint( stdout, pNtkComp );
+//printf( "cofactored variable %c\n", 'a' + iVar );
+//printf( "reused variable %c\n", 'a' + iVarReused );
+
+ ppLeaves[iVarReused] = Lpk_MapTree_rec( p, pNtkDec, ppLeaves, pNtkDec->Root, NULL );
pObjNew = Lpk_MapTree_rec( p, pNtkComp, ppLeaves, pNtkComp->Root, NULL );
+
+ Kit_DsdNtkFree( pNtkDec );
Kit_DsdNtkFree( pNtkComp );
return pObjNew;
}
diff --git a/src/opt/lpk/lpkSets.c b/src/opt/lpk/lpkSets.c
index 721705cb..d0d56a86 100644
--- a/src/opt/lpk/lpkSets.c
+++ b/src/opt/lpk/lpkSets.c
@@ -104,7 +104,8 @@ unsigned Lpk_ComputeSets_rec( Kit_DsdNtk_t * p, int iLit, Vec_Int_t * vSets )
***********************************************************************/
unsigned Lpk_ComputeSets( Kit_DsdNtk_t * p, Vec_Int_t * vSets )
{
- unsigned uSupport, Entry, i;
+ unsigned uSupport, Entry;
+ int Number, i;
assert( p->nVars <= 16 );
Vec_IntClear( vSets );
Vec_IntPush( vSets, 0 );
@@ -120,8 +121,11 @@ unsigned Lpk_ComputeSets( Kit_DsdNtk_t * p, Vec_Int_t * vSets )
assert( (uSupport & 0xFFFF0000) == 0 );
Vec_IntPush( vSets, uSupport );
// set the remaining variables
- Vec_IntForEachEntry( vSets, Entry, i )
+ Vec_IntForEachEntry( vSets, Number, i )
+ {
+ Entry = Number;
Vec_IntWriteEntry( vSets, i, Entry | ((uSupport & ~Entry) << 16) );
+ }
return uSupport;
}
@@ -157,10 +161,14 @@ void Lpk_PrintSetOne( int uSupport )
***********************************************************************/
void Lpk_PrintSets( Vec_Int_t * vSets )
{
- unsigned uSupport, i;
+ unsigned uSupport;
+ int Number, i;
printf( "Subsets(%d): ", Vec_IntSize(vSets) );
- Vec_IntForEachEntry( vSets, uSupport, i )
+ Vec_IntForEachEntry( vSets, Number, i )
+ {
+ uSupport = Number;
Lpk_PrintSetOne( uSupport );
+ }
printf( "\n" );
}
@@ -237,7 +245,7 @@ void Lpk_ComposeSets( Vec_Int_t * vSets0, Vec_Int_t * vSets1, int nVars, int iCo
}
}
- // check if there are non-overlapping
+ // find the minimum overlap
nMinOver = 1000;
for ( s = 0; s < nUsed; s++ )
if ( nMinOver > Over[Used[s]] )
@@ -267,7 +275,7 @@ void Lpk_ComposeSets( Vec_Int_t * vSets0, Vec_Int_t * vSets1, int nVars, int iCo
// get the number of overlapping vars
pEntry->Over = Kit_WordCountOnes( Entry & (Entry >> 16) );
// get the support reduction
- pEntry->SRed = pEntry->Size - 1 - pEntry->Over;
+ pEntry->SRed = pEntry->Size - 1 - pEntry->Over;
assert( pEntry->SRed > 0 );
}
}
@@ -318,13 +326,21 @@ unsigned Lpk_MapSuppRedDecSelect( Lpk_Man_t * p, unsigned * pTruth, int nVars, i
Vec_Int_t * vSets1 = p->vSets[1];
unsigned * pCof0 = Vec_PtrEntry( p->vTtNodes, 0 );
unsigned * pCof1 = Vec_PtrEntry( p->vTtNodes, 1 );
- int nSets, i, SizeMax;
+ int nSets, i, SizeMax;//, SRedMax;
unsigned Entry;
+ int fVerbose = p->pPars->fVeryVerbose;
+// int fVerbose = 0;
// collect decomposable subsets for each pair of cofactors
+ if ( fVerbose )
+ {
+ printf( "\nExploring support-reducing bound-sets of function:\n" );
+ Kit_DsdPrintFromTruth( pTruth, nVars );
+ }
nSets = 0;
for ( i = 0; i < nVars; i++ )
{
+ if ( fVerbose )
printf( "Evaluating variable %c:\n", 'a'+i );
// evaluate the cofactor pair
Kit_TruthCofactor0New( pCof0, pTruth, nVars, i );
@@ -334,13 +350,17 @@ unsigned Lpk_MapSuppRedDecSelect( Lpk_Man_t * p, unsigned * pTruth, int nVars, i
ppNtks[1] = Kit_DsdDecompose( pCof1, nVars );
ppNtks[0] = Kit_DsdExpand( pTemp = ppNtks[0] ); Kit_DsdNtkFree( pTemp );
ppNtks[1] = Kit_DsdExpand( pTemp = ppNtks[1] ); Kit_DsdNtkFree( pTemp );
+ if ( fVerbose )
Kit_DsdPrint( stdout, ppNtks[0] );
+ if ( fVerbose )
Kit_DsdPrint( stdout, ppNtks[1] );
// compute subsets
Lpk_ComputeSets( ppNtks[0], vSets0 );
Lpk_ComputeSets( ppNtks[1], vSets1 );
// print subsets
+ if ( fVerbose )
Lpk_PrintSets( vSets0 );
+ if ( fVerbose )
Lpk_PrintSets( vSets1 );
// free the networks
Kit_DsdNtkFree( ppNtks[0] );
@@ -350,7 +370,9 @@ unsigned Lpk_MapSuppRedDecSelect( Lpk_Man_t * p, unsigned * pTruth, int nVars, i
}
// print the results
+ if ( fVerbose )
printf( "\n" );
+ if ( fVerbose )
for ( i = 0; i < nSets; i++ )
Lpk_MapSuppPrintSet( pStore + i, i );
@@ -368,14 +390,33 @@ unsigned Lpk_MapSuppRedDecSelect( Lpk_Man_t * p, unsigned * pTruth, int nVars, i
SizeMax = pSet->Size;
}
}
+/*
+ // if the best is not choosen, select the one with largest reduction
+ SRedMax = 0;
+ if ( pSetBest == NULL )
+ {
+ for ( i = 0; i < nSets; i++ )
+ {
+ pSet = pStore + i;
+ if ( SRedMax < pSet->SRed )
+ {
+ pSetBest = pSet;
+ SRedMax = pSet->SRed;
+ }
+ }
+ }
+*/
if ( pSetBest == NULL )
{
+ if ( fVerbose )
printf( "Could not select a subset.\n" );
return 0;
}
else
{
+ if ( fVerbose )
printf( "Selected the following subset:\n" );
+ if ( fVerbose )
Lpk_MapSuppPrintSet( pSetBest, pSetBest - pStore );
}
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-15 01:56:31 +0000