diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2015-10-07 17:35:36 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2015-10-07 17:35:36 -0700 |
commit | a2692b70fb1d05029486f784bf364cea83cb6b47 (patch) | |
tree | c3e2dfe2fa7e6c360942ef43c4d08c176f99c17a /src/base/abci | |
parent | b19d09f04c37ceea2f2ed7abfb9881e09ea59c60 (diff) | |
download | abc-a2692b70fb1d05029486f784bf364cea83cb6b47.tar.gz abc-a2692b70fb1d05029486f784bf364cea83cb6b47.tar.bz2 abc-a2692b70fb1d05029486f784bf364cea83cb6b47.zip |
New switch 'satclp -r' to reverse variable order.
Diffstat (limited to 'src/base/abci')
-rw-r--r-- | src/base/abci/abc.c | 17 | ||||
-rw-r--r-- | src/base/abci/abcCollapse.c | 18 |
2 files changed, 20 insertions, 15 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index f2b436f8..8e7e418c 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -3103,12 +3103,13 @@ int Abc_CommandSatClp( Abc_Frame_t * pAbc, int argc, char ** argv ) int nCubeLim = 1000; int nBTLimit = 1000000; int fCanon = 0; + int fReverse = 0; int fVerbose = 0; int c; // set defaults Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "CLcvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "CLcrvh" ) ) != EOF ) { switch ( c ) { @@ -3137,6 +3138,9 @@ int Abc_CommandSatClp( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'c': fCanon ^= 1; break; + case 'r': + fReverse ^= 1; + break; case 'v': fVerbose ^= 1; break; @@ -3161,11 +3165,11 @@ int Abc_CommandSatClp( Abc_Frame_t * pAbc, int argc, char ** argv ) // get the new network if ( Abc_NtkIsStrash(pNtk) ) - pNtkRes = Abc_NtkCollapseSat( pNtk, nCubeLim, nBTLimit, fCanon, fVerbose ); + pNtkRes = Abc_NtkCollapseSat( pNtk, nCubeLim, nBTLimit, fCanon, fReverse, fVerbose ); else { pNtk = Abc_NtkStrash( pNtk, 0, 0, 0 ); - pNtkRes = Abc_NtkCollapseSat( pNtk, nCubeLim, nBTLimit, fCanon, fVerbose ); + pNtkRes = Abc_NtkCollapseSat( pNtk, nCubeLim, nBTLimit, fCanon, fReverse, fVerbose ); Abc_NtkDelete( pNtk ); } if ( pNtkRes == NULL ) @@ -3178,11 +3182,12 @@ int Abc_CommandSatClp( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: satclp [-CL num] [-cvh]\n" ); + Abc_Print( -2, "usage: satclp [-CL num] [-crvh]\n" ); Abc_Print( -2, "\t performs SAT based collapsing\n" ); Abc_Print( -2, "\t-C num : the limit on the SOP size of one output [default = %d]\n", nCubeLim ); Abc_Print( -2, "\t-L num : the limit on the number of conflicts in one SAT call [default = %d]\n", nBTLimit ); Abc_Print( -2, "\t-c : toggles using canonical ISOP computation [default = %s]\n", fCanon? "yes": "no" ); + Abc_Print( -2, "\t-r : toggles using reverse veriable ordering [default = %s]\n", fReverse? "yes": "no" ); Abc_Print( -2, "\t-v : toggles printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); return 1; @@ -37807,7 +37812,7 @@ usage: ***********************************************************************/ int Abc_CommandAbc9SatClp( Abc_Frame_t * pAbc, int argc, char ** argv ) { - extern Vec_Str_t * Bmc_CollapseOne( Gia_Man_t * p, int nCubeLim, int nBTLimit, int fCanon, int fVerbose ); + extern Vec_Str_t * Bmc_CollapseOne( Gia_Man_t * p, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose ); int nCubeLim = 1000; int nBTLimit = 1000000; int fCanon = 0; @@ -37859,7 +37864,7 @@ int Abc_CommandAbc9SatClp( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "Abc_CommandAbc9SatClp(): There is no AIG.\n" ); return 0; } - vSop = Bmc_CollapseOne( pAbc->pGia, nCubeLim, nBTLimit, fCanon, fVerbose ); + vSop = Bmc_CollapseOne( pAbc->pGia, nCubeLim, nBTLimit, fCanon, 0, fVerbose ); Vec_StrFree( vSop ); return 0; diff --git a/src/base/abci/abcCollapse.c b/src/base/abci/abcCollapse.c index c1a93dcf..b78a1206 100644 --- a/src/base/abci/abcCollapse.c +++ b/src/base/abci/abcCollapse.c @@ -290,16 +290,16 @@ Gia_Man_t * Abc_NtkClpOneGia( Abc_Ntk_t * pNtk, int iCo, Vec_Int_t * vSupp ) Gia_ManStop( pTemp ); return pNew; } -Vec_Str_t * Abc_NtkClpOne( Abc_Ntk_t * pNtk, int iCo, int nCubeLim, int nBTLimit, int fVerbose, int fCanon, Vec_Int_t ** pvSupp ) +Vec_Str_t * Abc_NtkClpOne( Abc_Ntk_t * pNtk, int iCo, int nCubeLim, int nBTLimit, int fVerbose, int fCanon, int fReverse, Vec_Int_t ** pvSupp ) { extern Vec_Int_t * Abc_NtkNodeSupportInt( Abc_Ntk_t * pNtk, int iCo ); - extern Vec_Str_t * Bmc_CollapseOne( Gia_Man_t * p, int nCubeLim, int nBTLimit, int fCanon, int fVerbose ); + extern Vec_Str_t * Bmc_CollapseOne( Gia_Man_t * p, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose ); Vec_Int_t * vSupp = Abc_NtkNodeSupportInt( pNtk, iCo ); Gia_Man_t * pGia = Abc_NtkClpOneGia( pNtk, iCo, vSupp ); Vec_Str_t * vSop; if ( fVerbose ) printf( "Output %d:\n", iCo ); - vSop = Bmc_CollapseOne( pGia, nCubeLim, nBTLimit, fCanon, fVerbose ); + vSop = Bmc_CollapseOne( pGia, nCubeLim, nBTLimit, fCanon, fReverse, fVerbose ); Gia_ManStop( pGia ); *pvSupp = vSupp; if ( vSop == NULL ) @@ -320,14 +320,14 @@ Vec_Str_t * Abc_NtkClpOne( Abc_Ntk_t * pNtk, int iCo, int nCubeLim, int nBTLimit SeeAlso [] ***********************************************************************/ -Abc_Obj_t * Abc_NtkFromSopsOne( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, int iCo, int nCubeLim, int nBTLimit, int fCanon, int fVerbose ) +Abc_Obj_t * Abc_NtkFromSopsOne( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, int iCo, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose ) { Abc_Obj_t * pNodeNew; Vec_Int_t * vSupp; Vec_Str_t * vSop; int i, iCi; // compute SOP of the node - vSop = Abc_NtkClpOne( pNtk, iCo, nCubeLim, nBTLimit, fVerbose, fCanon, &vSupp ); + vSop = Abc_NtkClpOne( pNtk, iCo, nCubeLim, nBTLimit, fVerbose, fCanon, fReverse, &vSupp ); if ( vSop == NULL ) return NULL; // create a new node @@ -341,7 +341,7 @@ Abc_Obj_t * Abc_NtkFromSopsOne( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, int iCo, Vec_StrFree( vSop ); return pNodeNew; } -Abc_Ntk_t * Abc_NtkFromSops( Abc_Ntk_t * pNtk, int nCubeLim, int nBTLimit, int fCanon, int fVerbose ) +Abc_Ntk_t * Abc_NtkFromSops( Abc_Ntk_t * pNtk, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose ) { ProgressBar * pProgress; Abc_Ntk_t * pNtkNew; @@ -381,7 +381,7 @@ Abc_Ntk_t * Abc_NtkFromSops( Abc_Ntk_t * pNtk, int nCubeLim, int nBTLimit, int f Abc_ObjAddFanin( pNode->pCopy, pNodeNew ); continue; } - pNodeNew = Abc_NtkFromSopsOne( pNtkNew, pNtk, i, nCubeLim, nBTLimit, fCanon, fVerbose ); + pNodeNew = Abc_NtkFromSopsOne( pNtkNew, pNtk, i, nCubeLim, nBTLimit, fCanon, fReverse, fVerbose ); if ( pNodeNew == NULL ) { Abc_NtkDelete( pNtkNew ); @@ -394,12 +394,12 @@ Abc_Ntk_t * Abc_NtkFromSops( Abc_Ntk_t * pNtk, int nCubeLim, int nBTLimit, int f Extra_ProgressBarStop( pProgress ); return pNtkNew; } -Abc_Ntk_t * Abc_NtkCollapseSat( Abc_Ntk_t * pNtk, int nCubeLim, int nBTLimit, int fCanon, int fVerbose ) +Abc_Ntk_t * Abc_NtkCollapseSat( Abc_Ntk_t * pNtk, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose ) { Abc_Ntk_t * pNtkNew; assert( Abc_NtkIsStrash(pNtk) ); // create the new network - pNtkNew = Abc_NtkFromSops( pNtk, nCubeLim, nBTLimit, fCanon, fVerbose ); + pNtkNew = Abc_NtkFromSops( pNtk, nCubeLim, nBTLimit, fCanon, fReverse, fVerbose ); if ( pNtkNew == NULL ) return NULL; if ( pNtk->pExdc ) |