From 31b2e8bebd9a531d4a1a6a807436615e0497c75e Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Mon, 6 Jun 2016 19:31:56 -0700 Subject: Switch 'fx -x' to use only canonical divisors in 'fx'. --- src/base/abci/abc.c | 12 ++++++++---- src/base/abci/abcFx.c | 14 ++++++++++---- 2 files changed, 18 insertions(+), 8 deletions(-) (limited to 'src/base') diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index befa1127..c55a46ed 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -3980,7 +3980,7 @@ usage: ***********************************************************************/ int Abc_CommandFastExtract( Abc_Frame_t * pAbc, int argc, char ** argv ) { - extern int Abc_NtkFxPerform( Abc_Ntk_t * pNtk, int nNewNodesMax, int nLitCountMax, int fVerbose, int fVeryVerbose ); + extern int Abc_NtkFxPerform( Abc_Ntk_t * pNtk, int nNewNodesMax, int nLitCountMax, int fCanonDivs, int fVerbose, int fVeryVerbose ); Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc); Fxu_Data_t Params, * p = &Params; int c, fNewAlgo = 1; @@ -3988,7 +3988,7 @@ int Abc_CommandFastExtract( Abc_Frame_t * pAbc, int argc, char ** argv ) // set the defaults Abc_NtkSetDefaultFxParams( p ); Extra_UtilGetoptReset(); - while ( (c = Extra_UtilGetopt(argc, argv, "SDNWMPsdzcnvwh")) != EOF ) + while ( (c = Extra_UtilGetopt(argc, argv, "SDNWMPsdzcnxvwh")) != EOF ) { switch (c) { @@ -4073,6 +4073,9 @@ int Abc_CommandFastExtract( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'n': fNewAlgo ^= 1; break; + case 'x': + p->fCanonDivs ^= 1; + break; case 'v': p->fVerbose ^= 1; break; @@ -4114,14 +4117,14 @@ int Abc_CommandFastExtract( Abc_Frame_t * pAbc, int argc, char ** argv ) // the nodes to be merged are linked into the special linked list if ( fNewAlgo ) - Abc_NtkFxPerform( pNtk, p->nNodesExt, p->LitCountMax, p->fVerbose, p->fVeryVerbose ); + Abc_NtkFxPerform( pNtk, p->nNodesExt, p->LitCountMax, p->fCanonDivs, p->fVerbose, p->fVeryVerbose ); else Abc_NtkFastExtract( pNtk, p ); Abc_NtkFxuFreeInfo( p ); return 0; usage: - Abc_Print( -2, "usage: fx [-SDNWMP ] [-sdzcnvwh]\n"); + Abc_Print( -2, "usage: fx [-SDNWMP ] [-sdzcnxvwh]\n"); Abc_Print( -2, "\t performs unate fast extract on the current network\n"); Abc_Print( -2, "\t-S : max number of single-cube divisors to consider [default = %d]\n", p->nSingleMax ); Abc_Print( -2, "\t-D : max number of double-cube divisors to consider [default = %d]\n", p->nPairsMax ); @@ -4134,6 +4137,7 @@ usage: Abc_Print( -2, "\t-z : use zero-weight divisors [default = %s]\n", p->fUse0? "yes": "no" ); Abc_Print( -2, "\t-c : use complement in the binary case [default = %s]\n", p->fUseCompl? "yes": "no" ); Abc_Print( -2, "\t-n : use new implementation of fast extract [default = %s]\n", fNewAlgo? "yes": "no" ); + Abc_Print( -2, "\t-x : use only canonical divisors (AND, XOR, MUX) [default = %s]\n", p->fCanonDivs? "yes": "no" ); Abc_Print( -2, "\t-v : print verbose information [default = %s]\n", p->fVerbose? "yes": "no" ); Abc_Print( -2, "\t-w : print additional information [default = %s]\n", p->fVeryVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); diff --git a/src/base/abci/abcFx.c b/src/base/abci/abcFx.c index 8208f68b..60f2e562 100644 --- a/src/base/abci/abcFx.c +++ b/src/base/abci/abcFx.c @@ -88,6 +88,7 @@ struct Fx_Man_t_ // user's data Vec_Wec_t * vCubes; // cube -> lit int LitCountMax;// max size of divisor to extract + int fCanonDivs; // use only AND/XOR/MUX // internal data Vec_Wec_t * vLits; // lit -> cube Vec_Int_t * vCounts; // literal counts (currently not used) @@ -300,9 +301,9 @@ int Abc_NtkFxCheck( Abc_Ntk_t * pNtk ) SeeAlso [] ***********************************************************************/ -int Abc_NtkFxPerform( Abc_Ntk_t * pNtk, int nNewNodesMax, int LitCountMax, int fVerbose, int fVeryVerbose ) +int Abc_NtkFxPerform( Abc_Ntk_t * pNtk, int nNewNodesMax, int LitCountMax, int fCanonDivs, int fVerbose, int fVeryVerbose ) { - extern int Fx_FastExtract( Vec_Wec_t * vCubes, int ObjIdMax, int nNewNodesMax, int LitCountMax, int fVerbose, int fVeryVerbose ); + extern int Fx_FastExtract( Vec_Wec_t * vCubes, int ObjIdMax, int nNewNodesMax, int LitCountMax, int fCanonDivs, int fVerbose, int fVeryVerbose ); Vec_Wec_t * vCubes; assert( Abc_NtkIsSopLogic(pNtk) ); // check unique fanins @@ -319,7 +320,7 @@ int Abc_NtkFxPerform( Abc_Ntk_t * pNtk, int nNewNodesMax, int LitCountMax, int f // collect information about the covers vCubes = Abc_NtkFxRetrieve( pNtk ); // call the fast extract procedure - if ( Fx_FastExtract( vCubes, Abc_NtkObjNumMax(pNtk), nNewNodesMax, LitCountMax, fVerbose, fVeryVerbose ) > 0 ) + if ( Fx_FastExtract( vCubes, Abc_NtkObjNumMax(pNtk), nNewNodesMax, LitCountMax, fCanonDivs, fVerbose, fVeryVerbose ) > 0 ) { // update the network Abc_NtkFxInsert( pNtk, vCubes ); @@ -841,9 +842,13 @@ void Fx_ManCubeDoubleCubeDivisors( Fx_Man_t * p, int iFirst, Vec_Int_t * vPivot, p->nDivMux[1]++; else p->nDivMux[2]++; + if ( p->fCanonDivs && Value < 0 ) + continue; } if ( p->LitCountMax && p->LitCountMax < Vec_IntSize(p->vCubeFree) ) continue; + if ( p->fCanonDivs && Vec_IntSize(p->vCubeFree) == 3 ) + continue; iDiv = Hsh_VecManAdd( p->pHash, p->vCubeFree ); if ( !fRemove ) { @@ -1167,7 +1172,7 @@ void Fx_ManUpdate( Fx_Man_t * p, int iDiv, int * fWarning ) SeeAlso [] ***********************************************************************/ -int Fx_FastExtract( Vec_Wec_t * vCubes, int ObjIdMax, int nNewNodesMax, int LitCountMax, int fVerbose, int fVeryVerbose ) +int Fx_FastExtract( Vec_Wec_t * vCubes, int ObjIdMax, int nNewNodesMax, int LitCountMax, int fCanonDivs, int fVerbose, int fVeryVerbose ) { int fVeryVeryVerbose = 0; int i, iDiv, fWarning = 0; @@ -1176,6 +1181,7 @@ int Fx_FastExtract( Vec_Wec_t * vCubes, int ObjIdMax, int nNewNodesMax, int LitC // initialize the data-structure p = Fx_ManStart( vCubes ); p->LitCountMax = LitCountMax; + p->fCanonDivs = fCanonDivs; Fx_ManCreateLiterals( p, ObjIdMax ); Fx_ManComputeLevel( p ); Fx_ManCreateDivisors( p ); -- cgit v1.2.3