summaryrefslogtreecommitdiffstats
path: root/src/opt
diff options
context:
space:
mode:
Diffstat (limited to 'src/opt')
-rw-r--r--src/opt/dec/dec.h2
-rw-r--r--src/opt/dec/decAbc.c6
-rw-r--r--src/opt/rwr/rwr.h9
-rw-r--r--src/opt/rwr/rwrDec.c3
-rw-r--r--src/opt/rwr/rwrEva.c6
-rw-r--r--src/opt/rwr/rwrMan.c25
-rw-r--r--src/opt/rwr/rwrPrint.c31
-rw-r--r--src/opt/sim/simSupp.c3
-rw-r--r--src/opt/sim/simSymSat.c4
9 files changed, 73 insertions, 16 deletions
diff --git a/src/opt/dec/dec.h b/src/opt/dec/dec.h
index 6ecc9678..783655fa 100644
--- a/src/opt/dec/dec.h
+++ b/src/opt/dec/dec.h
@@ -97,7 +97,7 @@ struct Dec_Man_t_
/*=== decAbc.c ========================================================*/
extern Abc_Obj_t * Dec_GraphToNetwork( Abc_Aig_t * pMan, Dec_Graph_t * pGraph );
extern int Dec_GraphToNetworkCount( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, int NodeMax, int LevelMax );
-extern void Dec_GraphUpdateNetwork( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, int nGain );
+extern void Dec_GraphUpdateNetwork( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, bool fUpdateLevel, int nGain );
/*=== decFactor.c ========================================================*/
extern Dec_Graph_t * Dec_Factor( char * pSop );
/*=== decMan.c ========================================================*/
diff --git a/src/opt/dec/decAbc.c b/src/opt/dec/decAbc.c
index 9931b136..62f90889 100644
--- a/src/opt/dec/decAbc.c
+++ b/src/opt/dec/decAbc.c
@@ -126,7 +126,7 @@ int Dec_GraphToNetworkCount( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, int NodeMa
else if ( Abc_ObjRegular(pAnd) == Abc_ObjRegular(pAnd1) )
LevelNew = (int)Abc_ObjRegular(pAnd1)->Level;
LevelOld = (int)Abc_ObjRegular(pAnd)->Level;
- assert( LevelNew == LevelOld );
+// assert( LevelNew == LevelOld );
}
if ( LevelNew > LevelMax )
return -1;
@@ -148,7 +148,7 @@ int Dec_GraphToNetworkCount( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, int NodeMa
SeeAlso []
***********************************************************************/
-void Dec_GraphUpdateNetwork( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, int nGain )
+void Dec_GraphUpdateNetwork( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, bool fUpdateLevel, int nGain )
{
Abc_Obj_t * pRootNew;
Abc_Ntk_t * pNtk = pRoot->pNtk;
@@ -157,7 +157,7 @@ void Dec_GraphUpdateNetwork( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, int nGain
// create the new structure of nodes
pRootNew = Dec_GraphToNetwork( pNtk->pManFunc, pGraph );
// remove the old nodes
- Abc_AigReplace( pNtk->pManFunc, pRoot, pRootNew );
+ Abc_AigReplace( pNtk->pManFunc, pRoot, pRootNew, fUpdateLevel );
// compare the gains
nNodesNew = Abc_NtkNodeNum(pNtk);
assert( nGain <= nNodesOld - nNodesNew );
diff --git a/src/opt/rwr/rwr.h b/src/opt/rwr/rwr.h
index 6d1a6c06..1467ce7a 100644
--- a/src/opt/rwr/rwr.h
+++ b/src/opt/rwr/rwr.h
@@ -49,6 +49,7 @@ struct Rwr_Man_t_
char * pPhases; // canonical phases
char * pPerms; // canonical permutations
unsigned char * pMap; // mapping of functions into class numbers
+ unsigned short * pMapInv; // mapping of classes into functions
char * pPractical; // practical NPN classes
char ** pPerms4; // four-var permutations
// node space
@@ -63,10 +64,11 @@ struct Rwr_Man_t_
int nClasses; // the number of NN classes
// the result of resynthesis
int fCompl; // indicates if the output of FF should be complemented
- void * pGraph; // the decomposition tree (temporary)
+ void * pGraph; // the decomposition tree (temporary)
Vec_Ptr_t * vFanins; // the fanins array (temporary)
Vec_Ptr_t * vFaninsCur; // the fanins array (temporary)
Vec_Int_t * vLevNums; // the array of levels (temporary)
+ Vec_Ptr_t * vNodesTemp; // the nodes in MFFC (temporary)
// node statistics
int nNodesConsidered;
int nNodesRewritten;
@@ -80,6 +82,8 @@ struct Rwr_Man_t_
int timeCut;
int timeRes;
int timeEval;
+ int timeMffc;
+ int timeUpdate;
int timeTotal;
};
@@ -114,7 +118,7 @@ static inline Rwr_Node_t * Rwr_NotCond( Rwr_Node_t * p, int c ) { return (Rwr_N
/*=== rwrDec.c ========================================================*/
extern void Rwr_ManPreprocess( Rwr_Man_t * p );
/*=== rwrEva.c ========================================================*/
-extern int Rwr_NodeRewrite( Rwr_Man_t * p, Cut_Man_t * pManCut, Abc_Obj_t * pNode, int fUseZeros );
+extern int Rwr_NodeRewrite( Rwr_Man_t * p, Cut_Man_t * pManCut, Abc_Obj_t * pNode, int fUpdateLevel, int fUseZeros );
/*=== rwrLib.c ========================================================*/
extern void Rwr_ManPrecompute( Rwr_Man_t * p );
extern Rwr_Node_t * Rwr_ManAddVar( Rwr_Man_t * p, unsigned uTruth, int fPrecompute );
@@ -128,6 +132,7 @@ extern void Rwr_ManPrintStats( Rwr_Man_t * p );
extern void * Rwr_ManReadDecs( Rwr_Man_t * p );
extern int Rwr_ManReadCompl( Rwr_Man_t * p );
extern void Rwr_ManAddTimeCuts( Rwr_Man_t * p, int Time );
+extern void Rwr_ManAddTimeUpdate( Rwr_Man_t * p, int Time );
extern void Rwr_ManAddTimeTotal( Rwr_Man_t * p, int Time );
/*=== rwrPrint.c ========================================================*/
extern void Rwr_ManPrint( Rwr_Man_t * p );
diff --git a/src/opt/rwr/rwrDec.c b/src/opt/rwr/rwrDec.c
index d072879d..a7f55a90 100644
--- a/src/opt/rwr/rwrDec.c
+++ b/src/opt/rwr/rwrDec.c
@@ -49,6 +49,8 @@ void Rwr_ManPreprocess( Rwr_Man_t * p )
Rwr_Node_t * pNode;
int i, k;
// put the nodes into the structure
+ p->pMapInv = ALLOC( unsigned short, 222 );
+ memset( p->pMapInv, 0, sizeof(unsigned short) * 222 );
p->vClasses = Vec_VecStart( 222 );
for ( i = 0; i < p->nFuncs; i++ )
{
@@ -60,6 +62,7 @@ void Rwr_ManPreprocess( Rwr_Man_t * p )
assert( pNode->uTruth == p->pTable[i]->uTruth );
assert( p->pMap[pNode->uTruth] >= 0 && p->pMap[pNode->uTruth] < 222 );
Vec_VecPush( p->vClasses, p->pMap[pNode->uTruth], pNode );
+ p->pMapInv[ p->pMap[pNode->uTruth] ] = p->puCanons[pNode->uTruth];
}
}
// compute decomposition forms for each node and verify them
diff --git a/src/opt/rwr/rwrEva.c b/src/opt/rwr/rwrEva.c
index c934dfd8..8a00cec8 100644
--- a/src/opt/rwr/rwrEva.c
+++ b/src/opt/rwr/rwrEva.c
@@ -49,7 +49,7 @@ static Dec_Graph_t * Rwr_CutEvaluate( Rwr_Man_t * p, Abc_Obj_t * pRoot, Cut_Cut_
SeeAlso []
***********************************************************************/
-int Rwr_NodeRewrite( Rwr_Man_t * p, Cut_Man_t * pManCut, Abc_Obj_t * pNode, int fUseZeros )
+int Rwr_NodeRewrite( Rwr_Man_t * p, Cut_Man_t * pManCut, Abc_Obj_t * pNode, int fUpdateLevel, int fUseZeros )
{
int fVeryVerbose = 0;
Dec_Graph_t * pGraph;
@@ -63,7 +63,7 @@ int Rwr_NodeRewrite( Rwr_Man_t * p, Cut_Man_t * pManCut, Abc_Obj_t * pNode, int
p->nNodesConsidered++;
// get the required times
- Required = Abc_NodeReadRequiredLevel( pNode );
+ Required = fUpdateLevel? Abc_NodeReadRequiredLevel(pNode) : ABC_INFINITY;
// get the node's cuts
clk = clock();
pCut = (Cut_Cut_t *)Abc_NodeGetCutsRecursive( pManCut, pNode );
@@ -98,6 +98,7 @@ clk = clock();
}
p->nCutsGood++;
+clk2 = clock();
// mark the fanin boundary
Vec_PtrForEachEntry( p->vFaninsCur, pFanin, i )
Abc_ObjRegular(pFanin)->vFanouts.nSize++;
@@ -107,6 +108,7 @@ clk = clock();
// unmark the fanin boundary
Vec_PtrForEachEntry( p->vFaninsCur, pFanin, i )
Abc_ObjRegular(pFanin)->vFanouts.nSize--;
+p->timeMffc += clock() - clk2;
// evaluate the cut
clk2 = clock();
diff --git a/src/opt/rwr/rwrMan.c b/src/opt/rwr/rwrMan.c
index a21dd520..bfeaa273 100644
--- a/src/opt/rwr/rwrMan.c
+++ b/src/opt/rwr/rwrMan.c
@@ -75,6 +75,7 @@ clk = clock();
p->vLevNums = Vec_IntAlloc( 50 );
p->vFanins = Vec_PtrAlloc( 50 );
p->vFaninsCur = Vec_PtrAlloc( 50 );
+ p->vNodesTemp = Vec_PtrAlloc( 50 );
if ( fPrecompute )
{ // precompute subgraphs
Rwr_ManPrecompute( p );
@@ -112,11 +113,13 @@ void Rwr_ManStop( Rwr_Man_t * p )
Dec_GraphFree( (Dec_Graph_t *)pNode->pNext );
}
if ( p->vClasses ) Vec_VecFree( p->vClasses );
+ Vec_PtrFree( p->vNodesTemp );
Vec_PtrFree( p->vForest );
Vec_IntFree( p->vLevNums );
Vec_PtrFree( p->vFanins );
Vec_PtrFree( p->vFaninsCur );
Extra_MmFixedStop( p->pMmNode, 0 );
+ FREE( p->pMapInv );
free( p->pTable );
free( p->pPractical );
free( p->pPerms4 );
@@ -151,14 +154,16 @@ void Rwr_ManPrintStats( Rwr_Man_t * p )
PRT( "Start ", p->timeStart );
PRT( "Cuts ", p->timeCut );
PRT( "Resynthesis ", p->timeRes );
+ PRT( " Mffc ", p->timeMffc );
PRT( " Eval ", p->timeEval );
+ PRT( "Update ", p->timeUpdate );
PRT( "TOTAL ", p->timeTotal );
/*
- printf( "The scores are : " );
+ printf( "The scores are:\n" );
for ( i = 0; i < 222; i++ )
if ( p->nScores[i] > 0 )
- printf( "%d=%d ", i, p->nScores[i] );
+ printf( "%3d = %8d canon = %5d\n", i, p->nScores[i], p->pMapInv[i] );
printf( "\n" );
*/
}
@@ -222,6 +227,22 @@ void Rwr_ManAddTimeCuts( Rwr_Man_t * p, int Time )
SeeAlso []
***********************************************************************/
+void Rwr_ManAddTimeUpdate( Rwr_Man_t * p, int Time )
+{
+ p->timeUpdate += Time;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Stops the resynthesis manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
void Rwr_ManAddTimeTotal( Rwr_Man_t * p, int Time )
{
p->timeTotal += Time;
diff --git a/src/opt/rwr/rwrPrint.c b/src/opt/rwr/rwrPrint.c
index 30c99f00..9011ce56 100644
--- a/src/opt/rwr/rwrPrint.c
+++ b/src/opt/rwr/rwrPrint.c
@@ -79,6 +79,33 @@ void Rwr_GetBushVolume( Rwr_Man_t * p, int Entry, int * pVolume, int * pnFuncs )
/**Function*************************************************************
+ Synopsis [Adds the node to the end of the list.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Rwr_GetBushSumOfVolumes( Rwr_Man_t * p, int Entry )
+{
+ Rwr_Node_t * pNode;
+ int Volume, VolumeTotal = 0;
+ for ( pNode = p->pTable[Entry]; pNode; pNode = pNode->pNext )
+ {
+ if ( pNode->uTruth != p->puCanons[pNode->uTruth] )
+ continue;
+ Volume = 0;
+ Rwr_ManIncTravId( p );
+ Rwr_Trav2_rec( p, pNode, &Volume );
+ VolumeTotal += Volume;
+ }
+ return VolumeTotal;
+}
+
+/**Function*************************************************************
+
Synopsis [Prints one rwr node.]
Description []
@@ -219,9 +246,9 @@ void Rwr_ManPrint( Rwr_Man_t * p )
continue;
if ( i != p->puCanons[i] )
continue;
- fprintf( pFile, "\nClass %3d. Func %6d. ", p->pMap[i], Counter++ );
+ fprintf( pFile, "\nClass %3d. Func %6d. ", p->pMap[i], Counter++ );
Rwr_GetBushVolume( p, i, &Volume, &nFuncs );
- fprintf( pFile, "Functions = %2d. Volume = %2d. ", nFuncs, Volume );
+ fprintf( pFile, "Roots = %3d. Vol = %3d. Sum = %3d. ", nFuncs, Volume, Rwr_GetBushSumOfVolumes(p, i) );
uTruth = i;
Extra_PrintBinary( pFile, &uTruth, 16 );
fprintf( pFile, "\n" );
diff --git a/src/opt/sim/simSupp.c b/src/opt/sim/simSupp.c
index 576e19cc..d805da72 100644
--- a/src/opt/sim/simSupp.c
+++ b/src/opt/sim/simSupp.c
@@ -35,8 +35,6 @@ static void Sim_UtilAssignFromFifo( Sim_Man_t * p );
static void Sim_SolveTargetsUsingSat( Sim_Man_t * p, int nCounters );
static int Sim_SolveSuppModelVerify( Abc_Ntk_t * pNtk, int * pModel, int Input, int Output );
-extern Fraig_Man_t * Abc_NtkToFraig( Abc_Ntk_t * pNtk, Fraig_Params_t * pParams, int fAllNodes );
-
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFITIONS ///
////////////////////////////////////////////////////////////////////////
@@ -469,6 +467,7 @@ void Sim_SolveTargetsUsingSat( Sim_Man_t * p, int Limit )
// transform the miter into a fraig
Fraig_ParamsSetDefault( &Params );
+ Params.nSeconds = ABC_INFINITY;
Params.fInternal = 1;
clk = clock();
pMan = Abc_NtkToFraig( pMiter, &Params, 0 );
diff --git a/src/opt/sim/simSymSat.c b/src/opt/sim/simSymSat.c
index db9917b3..a98d4b5e 100644
--- a/src/opt/sim/simSymSat.c
+++ b/src/opt/sim/simSymSat.c
@@ -26,8 +26,7 @@
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
-extern int Sim_SymmsSatProveOne( Sym_Man_t * p, int Out, int Var1, int Var2, unsigned * pPattern );
-extern Fraig_Man_t * Abc_NtkToFraig( Abc_Ntk_t * pNtk, Fraig_Params_t * pParams, int fAllNodes );
+static int Sim_SymmsSatProveOne( Sym_Man_t * p, int Out, int Var1, int Var2, unsigned * pPattern );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFITIONS ///
@@ -145,6 +144,7 @@ int Sim_SymmsSatProveOne( Sym_Man_t * p, int Out, int Var1, int Var2, unsigned *
Params.fInternal = 1;
Params.nPatsRand = 512;
Params.nPatsDyna = 512;
+ Params.nSeconds = ABC_INFINITY;
clk = clock();
pMan = Abc_NtkToFraig( pMiter, &Params, 0 );
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-15 21:36:04 +0000