From e5636522bffa347c951b93b5285bef6e51607f4d Mon Sep 17 00:00:00 2001 From: Mathias Soeken Date: Thu, 25 Aug 2016 10:56:59 +0200 Subject: BMS fixes and start gates parameter. --- src/base/abc/abc.h | 2 +- src/base/abci/abc.c | 24 ++++++++++++++++++------ src/base/abci/abcExact.c | 34 +++++++++++++++------------------- 3 files changed, 34 insertions(+), 26 deletions(-) (limited to 'src') diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h index e752fb71..6c0d96d1 100644 --- a/src/base/abc/abc.h +++ b/src/base/abc/abc.h @@ -646,7 +646,7 @@ extern ABC_DLL Vec_Ptr_t * Abc_AigGetLevelizedOrder( Abc_Ntk_t * pNtk, in extern ABC_DLL int Abc_ExactInputNum(); extern ABC_DLL int Abc_ExactIsRunning(); extern ABC_DLL Abc_Obj_t * Abc_ExactBuildNode( word * pTruth, int nVars, int * pArrTimeProfile, Abc_Obj_t ** pFanins, Abc_Ntk_t * pNtk ); -extern ABC_DLL Abc_Ntk_t * Abc_NtkFindExact( word * pTruth, int nVars, int nFunc, int nMaxDepth, int * pArrivalTimes, int nBTLimit, int fVerbose ); +extern ABC_DLL Abc_Ntk_t * Abc_NtkFindExact( word * pTruth, int nVars, int nFunc, int nMaxDepth, int * pArrivalTimes, int nBTLimit, int nStartGates, int fVerbose ); /*=== abcFanio.c ==========================================================*/ extern ABC_DLL void Abc_ObjAddFanin( Abc_Obj_t * pObj, Abc_Obj_t * pFanin ); extern ABC_DLL void Abc_ObjDeleteFanin( Abc_Obj_t * pObj, Abc_Obj_t * pFanin ); diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 9e45a7da..97d6b157 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -7291,9 +7291,9 @@ usage: ***********************************************************************/ int Abc_CommandExact( Abc_Frame_t * pAbc, int argc, char ** argv ) { - extern Gia_Man_t * Gia_ManFindExact( word * pTruth, int nVars, int nFunc, int nMaxDepth, int * pArrivalTimes, int nBTLimit, int fVerbose ); + extern Gia_Man_t * Gia_ManFindExact( word * pTruth, int nVars, int nFunc, int nMaxDepth, int * pArrivalTimes, int nBTLimit, int nStartGates, int fVerbose ); - int c, nMaxDepth = -1, fMakeAIG = 0, fTest = 0, fVerbose = 0, nVars = 0, nVarsTmp, nFunc = 0, nBTLimit = 100; + int c, nMaxDepth = -1, fMakeAIG = 0, fTest = 0, fVerbose = 0, nVars = 0, nVarsTmp, nFunc = 0, nStartGates = 1, nBTLimit = 100; char * p1, * p2; word pTruth[64]; int pArrTimeProfile[8], fHasArrTimeProfile = 0; @@ -7301,7 +7301,7 @@ int Abc_CommandExact( Abc_Frame_t * pAbc, int argc, char ** argv ) Gia_Man_t * pGiaRes; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "DACatvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "DASCatvh" ) ) != EOF ) { switch ( c ) { @@ -7341,6 +7341,17 @@ int Abc_CommandExact( Abc_Frame_t * pAbc, int argc, char ** argv ) ++p2; } break; + case 'S': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-S\" should be followed by an integer.\n" ); + goto usage; + } + nStartGates = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nStartGates < 1 ) + goto usage; + break; case 'C': if ( globalUtilOptind >= argc ) { @@ -7406,7 +7417,7 @@ int Abc_CommandExact( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( fMakeAIG ) { - pGiaRes = Gia_ManFindExact( pTruth, nVars, nFunc, nMaxDepth, fHasArrTimeProfile ? pArrTimeProfile : NULL, nBTLimit, fVerbose ); + pGiaRes = Gia_ManFindExact( pTruth, nVars, nFunc, nMaxDepth, fHasArrTimeProfile ? pArrTimeProfile : NULL, nBTLimit, nStartGates - 1, fVerbose ); if ( pGiaRes ) Abc_FrameUpdateGia( pAbc, pGiaRes ); else @@ -7414,7 +7425,7 @@ int Abc_CommandExact( Abc_Frame_t * pAbc, int argc, char ** argv ) } else { - pNtkRes = Abc_NtkFindExact( pTruth, nVars, nFunc, nMaxDepth, fHasArrTimeProfile ? pArrTimeProfile : NULL, nBTLimit, fVerbose ); + pNtkRes = Abc_NtkFindExact( pTruth, nVars, nFunc, nMaxDepth, fHasArrTimeProfile ? pArrTimeProfile : NULL, nBTLimit, nStartGates - 1, fVerbose ); if ( pNtkRes ) { Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); @@ -7426,10 +7437,11 @@ int Abc_CommandExact( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: exact [-D ] [-atvh] ...\n" ); + Abc_Print( -2, "usage: exact [-DSC ] [-A ] [-atvh] ...\n" ); Abc_Print( -2, "\t finds optimum networks using SAT-based exact synthesis for hex truth tables ...\n" ); Abc_Print( -2, "\t-D : constrain maximum depth (if too low, algorithm may not terminate)\n" ); Abc_Print( -2, "\t-A : input arrival times (comma separated list)\n" ); + Abc_Print( -2, "\t-S : number of start gates in search [default = %s]\n", nStartGates ); Abc_Print( -2, "\t-C : the limit on the number of conflicts [default = %d]\n", nBTLimit ); Abc_Print( -2, "\t-a : toggle create AIG [default = %s]\n", fMakeAIG ? "yes" : "no" ); Abc_Print( -2, "\t-t : run test suite\n" ); diff --git a/src/base/abci/abcExact.c b/src/base/abci/abcExact.c index 770afb0a..f5e7d713 100644 --- a/src/base/abci/abcExact.c +++ b/src/base/abci/abcExact.c @@ -966,17 +966,11 @@ static int Ses_ManCreateClauses( Ses_Man_t * pSes ) { pLits[0] = Abc_Var2Lit( Ses_ManOutputVar( pSes, 0, i ), 1 ); if ( !sat_solver_addclause( pSes->pSat, pLits, pLits + 1 ) ) - { - Vec_IntFree( vLits ); return 0; - } } pLits[0] = Abc_Var2Lit( Ses_ManOutputVar( pSes, 0, pSes->nGates - 1 ), 0 ); if ( !sat_solver_addclause( pSes->pSat, pLits, pLits + 1 ) ) - { - Vec_IntFree( vLits ); return 0; - } vLits = Vec_IntAlloc( 0u ); } @@ -1744,7 +1738,7 @@ static int Ses_ManFindMinimumSize( Ses_Man_t * pSes ) pSes->fHitResLimit = 0; /* do the arrival times allow for a network? */ - if ( pSes->nMaxDepth != -1 && !Ses_CheckDepthConsistency( pSes ) ) + if ( pSes->nMaxDepth != -1 && pSes->pArrTimeProfile && !Ses_CheckDepthConsistency( pSes ) ) return 0; //Ses_ManStoreDepthAndArrivalTimes( pSes ); @@ -1818,7 +1812,7 @@ static int Ses_ManFindMinimumSize( Ses_Man_t * pSes ) SeeAlso [] ***********************************************************************/ -Abc_Ntk_t * Abc_NtkFindExact( word * pTruth, int nVars, int nFunc, int nMaxDepth, int * pArrTimeProfile, int nBTLimit, int fVerbose ) +Abc_Ntk_t * Abc_NtkFindExact( word * pTruth, int nVars, int nFunc, int nMaxDepth, int * pArrTimeProfile, int nBTLimit, int nStartGates, int fVerbose ) { Ses_Man_t * pSes; char * pSol; @@ -1831,6 +1825,7 @@ Abc_Ntk_t * Abc_NtkFindExact( word * pTruth, int nVars, int nFunc, int nMaxDepth timeStart = Abc_Clock(); pSes = Ses_ManAlloc( pTruth, nVars, nFunc, nMaxDepth, pArrTimeProfile, 0, nBTLimit, fVerbose ); + pSes->nStartGates = nStartGates; if ( fVerbose ) Ses_ManPrintFuncs( pSes ); @@ -1852,7 +1847,7 @@ Abc_Ntk_t * Abc_NtkFindExact( word * pTruth, int nVars, int nFunc, int nMaxDepth return pNtk; } -Gia_Man_t * Gia_ManFindExact( word * pTruth, int nVars, int nFunc, int nMaxDepth, int * pArrTimeProfile, int nBTLimit, int fVerbose ) +Gia_Man_t * Gia_ManFindExact( word * pTruth, int nVars, int nFunc, int nMaxDepth, int * pArrTimeProfile, int nBTLimit, int nStartGates, int fVerbose ) { Ses_Man_t * pSes; char * pSol; @@ -1865,6 +1860,7 @@ Gia_Man_t * Gia_ManFindExact( word * pTruth, int nVars, int nFunc, int nMaxDepth timeStart = Abc_Clock(); pSes = Ses_ManAlloc( pTruth, nVars, nFunc, nMaxDepth, pArrTimeProfile, 1, nBTLimit, fVerbose ); + pSes->nStartGates = nStartGates; pSes->fVeryVerbose = 1; pSes->fExtractVerbose = 1; pSes->fSatVerbose = 1; @@ -1920,30 +1916,30 @@ void Abc_ExactTestSingleOutput( int fVerbose ) pNtk = Abc_NtkFromTruthTable( pTruth, 4 ); - pNtk2 = Abc_NtkFindExact( pTruth, 4, 1, -1, NULL, 0, fVerbose ); + pNtk2 = Abc_NtkFindExact( pTruth, 4, 1, -1, NULL, 0, 0, fVerbose ); Abc_NtkShortNames( pNtk2 ); Abc_NtkCecSat( pNtk, pNtk2, 10000, 0 ); assert( pNtk2 ); assert( Abc_NtkNodeNum( pNtk2 ) == 6 ); Abc_NtkDelete( pNtk2 ); - pNtk3 = Abc_NtkFindExact( pTruth, 4, 1, 3, NULL, 0, fVerbose ); + pNtk3 = Abc_NtkFindExact( pTruth, 4, 1, 3, NULL, 0, 0, fVerbose ); Abc_NtkShortNames( pNtk3 ); Abc_NtkCecSat( pNtk, pNtk3, 10000, 0 ); assert( pNtk3 ); assert( Abc_NtkLevel( pNtk3 ) <= 3 ); Abc_NtkDelete( pNtk3 ); - pNtk4 = Abc_NtkFindExact( pTruth, 4, 1, 9, pArrTimeProfile, 50000, fVerbose ); + pNtk4 = Abc_NtkFindExact( pTruth, 4, 1, 9, pArrTimeProfile, 50000, 0, fVerbose ); Abc_NtkShortNames( pNtk4 ); Abc_NtkCecSat( pNtk, pNtk4, 10000, 0 ); assert( pNtk4 ); assert( Abc_NtkLevel( pNtk4 ) <= 9 ); Abc_NtkDelete( pNtk4 ); - assert( !Abc_NtkFindExact( pTruth, 4, 1, 2, NULL, 50000, fVerbose ) ); + assert( !Abc_NtkFindExact( pTruth, 4, 1, 2, NULL, 50000, 0, fVerbose ) ); - assert( !Abc_NtkFindExact( pTruth, 4, 1, 8, pArrTimeProfile, 50000, fVerbose ) ); + assert( !Abc_NtkFindExact( pTruth, 4, 1, 8, pArrTimeProfile, 50000, 0, fVerbose ) ); Abc_NtkDelete( pNtk ); } @@ -1962,27 +1958,27 @@ void Abc_ExactTestSingleOutputAIG( int fVerbose ) Abc_NtkToAig( pNtk ); pGia = Abc_NtkAigToGia( pNtk, 1 ); - pGia2 = Gia_ManFindExact( pTruth, 4, 1, -1, NULL, 0, fVerbose ); + pGia2 = Gia_ManFindExact( pTruth, 4, 1, -1, NULL, 0, 0, fVerbose ); pMiter = Gia_ManMiter( pGia, pGia2, 0, 1, 0, 0, 1 ); assert( pMiter ); Cec_ManVerify( pMiter, pPars ); Gia_ManStop( pMiter ); - pGia3 = Gia_ManFindExact( pTruth, 4, 1, 3, NULL, 0, fVerbose ); + pGia3 = Gia_ManFindExact( pTruth, 4, 1, 3, NULL, 0, 0, fVerbose ); pMiter = Gia_ManMiter( pGia, pGia3, 0, 1, 0, 0, 1 ); assert( pMiter ); Cec_ManVerify( pMiter, pPars ); Gia_ManStop( pMiter ); - pGia4 = Gia_ManFindExact( pTruth, 4, 1, 9, pArrTimeProfile, 50000, fVerbose ); + pGia4 = Gia_ManFindExact( pTruth, 4, 1, 9, pArrTimeProfile, 50000, 0, fVerbose ); pMiter = Gia_ManMiter( pGia, pGia4, 0, 1, 0, 0, 1 ); assert( pMiter ); Cec_ManVerify( pMiter, pPars ); Gia_ManStop( pMiter ); - assert( !Gia_ManFindExact( pTruth, 4, 1, 2, NULL, 50000, fVerbose ) ); + assert( !Gia_ManFindExact( pTruth, 4, 1, 2, NULL, 50000, 0, fVerbose ) ); - assert( !Gia_ManFindExact( pTruth, 4, 1, 8, pArrTimeProfile, 50000, fVerbose ) ); + assert( !Gia_ManFindExact( pTruth, 4, 1, 8, pArrTimeProfile, 50000, 0, fVerbose ) ); Gia_ManStop( pGia ); Gia_ManStop( pGia2 ); -- cgit v1.2.3