From c7b65a15d386ed1ad89707e20dcc2d31237c8e60 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 6 Dec 2017 15:09:11 -0800 Subject: Adding parameter structure to 'twoexact' and 'lutexact'. --- src/base/abci/abc.c | 130 +++++++++++++++++++++++++++----------------------- src/sat/bmc/bmc.h | 30 +++++++++++- src/sat/bmc/bmcMaj.c | 74 +++++++++++++--------------- src/sat/bmc/bmcMaj2.c | 74 +++++++++++++--------------- 4 files changed, 165 insertions(+), 143 deletions(-) (limited to 'src') diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index f4bbaf16..c925fa42 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -8177,11 +8177,13 @@ usage: ***********************************************************************/ int Abc_CommandTwoExact( Abc_Frame_t * pAbc, int argc, char ** argv ) { - extern void Exa_ManExactSynthesis( char * pTtStr, int nVars, int nNodes, int fOnlyAnd, int fVerbose ); - extern void Exa_ManExactSynthesis2( char * pTtStr, int nVars, int nNodes, int fOnlyAnd, int fVerbose ); - int c, nVars = 4, nNodes = 3, fGlucose = 0, fOnlyAnd = 0, fVerbose = 1; char * pTtStr = NULL; + extern void Exa_ManExactSynthesis( Bmc_EsPar_t * pPars ); + extern void Exa_ManExactSynthesis2( Bmc_EsPar_t * pPars ); + int c; + Bmc_EsPar_t Pars, * pPars = &Pars; + Bmc_EsParSetDefault( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "INagvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "INaogvh" ) ) != EOF ) { switch ( c ) { @@ -8191,9 +8193,9 @@ int Abc_CommandTwoExact( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "Command line switch \"-I\" should be followed by an integer.\n" ); goto usage; } - nVars = atoi(argv[globalUtilOptind]); + pPars->nVars = atoi(argv[globalUtilOptind]); globalUtilOptind++; - if ( nVars < 0 ) + if ( pPars->nVars < 0 ) goto usage; break; case 'N': @@ -8202,19 +8204,22 @@ int Abc_CommandTwoExact( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "Command line switch \"-N\" should be followed by an integer.\n" ); goto usage; } - nNodes = atoi(argv[globalUtilOptind]); + pPars->nNodes = atoi(argv[globalUtilOptind]); globalUtilOptind++; - if ( nNodes < 0 ) + if ( pPars->nNodes < 0 ) goto usage; break; case 'a': - fOnlyAnd ^= 1; + pPars->fOnlyAnd ^= 1; + break; + case 'o': + pPars->fFewerVars ^= 1; break; case 'g': - fGlucose ^= 1; + pPars->fGlucose ^= 1; break; case 'v': - fVerbose ^= 1; + pPars->fVerbose ^= 1; break; case 'h': goto usage; @@ -8223,41 +8228,42 @@ int Abc_CommandTwoExact( Abc_Frame_t * pAbc, int argc, char ** argv ) } } if ( argc == globalUtilOptind + 1 ) - pTtStr = argv[globalUtilOptind]; - if ( pTtStr == NULL ) + pPars->pTtStr = argv[globalUtilOptind]; + if ( pPars->pTtStr == NULL ) { Abc_Print( -1, "Truth table should be given on the command line.\n" ); return 1; } - if ( (1 << (nVars-2)) != (int)strlen(pTtStr) ) + if ( (1 << (pPars->nVars-2)) != (int)strlen(pPars->pTtStr) ) { - Abc_Print( -1, "Truth table is expected to have %d hex digits (instead of %d).\n", (1 << (nVars-2)), strlen(pTtStr) ); + Abc_Print( -1, "Truth table is expected to have %d hex digits (instead of %d).\n", (1 << (pPars->nVars-2)), strlen(pPars->pTtStr) ); return 1; } - if ( nVars > nNodes * (2 - 1) + 1 ) + if ( pPars->nVars > pPars->nNodes * (2 - 1) + 1 ) { - Abc_Print( -1, "Function with %d variales cannot be implemented with %d two-input gates.\n", nVars, nNodes ); + Abc_Print( -1, "Function with %d variales cannot be implemented with %d two-input gates.\n", pPars->nVars, pPars->nNodes ); return 1; } - if ( nVars > 10 ) + if ( pPars->nVars > 10 ) { Abc_Print( -1, "Function should not have more than 10 inputs.\n" ); return 1; } - if ( fGlucose ) - Exa_ManExactSynthesis( pTtStr, nVars, nNodes, fOnlyAnd, fVerbose ); + if ( pPars->fGlucose ) + Exa_ManExactSynthesis( pPars ); else - Exa_ManExactSynthesis2( pTtStr, nVars, nNodes, fOnlyAnd, fVerbose ); + Exa_ManExactSynthesis2( pPars ); return 0; usage: - Abc_Print( -2, "usage: twoexact [-IN ] [-agvh] \n" ); + Abc_Print( -2, "usage: twoexact [-IN ] [-aogvh] \n" ); Abc_Print( -2, "\t exact synthesis of multi-input function using two-input gates\n" ); - Abc_Print( -2, "\t-I : the number of input variables [default = %d]\n", nVars ); - Abc_Print( -2, "\t-N : the number of MAJ3 nodes [default = %d]\n", nNodes ); - Abc_Print( -2, "\t-a : toggle using only AND-gates (without XOR-gates) [default = %s]\n", fOnlyAnd ? "yes" : "no" ); - Abc_Print( -2, "\t-g : toggle using Glucose 3.0 by Gilles Audemard and Laurent Simon [default = %s]\n", fGlucose ? "yes" : "no" ); - Abc_Print( -2, "\t-v : toggle verbose printout [default = %s]\n", fVerbose ? "yes" : "no" ); + Abc_Print( -2, "\t-I : the number of input variables [default = %d]\n", pPars->nVars ); + Abc_Print( -2, "\t-N : the number of MAJ3 nodes [default = %d]\n", pPars->nNodes ); + Abc_Print( -2, "\t-a : toggle using only AND-gates (without XOR-gates) [default = %s]\n", pPars->fOnlyAnd ? "yes" : "no" ); + Abc_Print( -2, "\t-o : toggle using additional optimizations [default = %s]\n", pPars->fFewerVars ? "yes" : "no" ); + Abc_Print( -2, "\t-g : toggle using Glucose 3.0 by Gilles Audemard and Laurent Simon [default = %s]\n", pPars->fGlucose ? "yes" : "no" ); + Abc_Print( -2, "\t-v : toggle verbose printout [default = %s]\n", pPars->fVerbose ? "yes" : "no" ); Abc_Print( -2, "\t-h : print the command usage\n" ); Abc_Print( -2, "\t : truth table in hex notation\n" ); Abc_Print( -2, "\t \n" ); @@ -8283,11 +8289,13 @@ usage: ***********************************************************************/ int Abc_CommandLutExact( Abc_Frame_t * pAbc, int argc, char ** argv ) { - extern void Exa3_ManExactSynthesis( char * pTtStr, int nVars, int nNodes, int nLutSize, int fOnlyAnd, int fVerbose ); - extern void Exa3_ManExactSynthesis2( char * pTtStr, int nVars, int nNodes, int nLutSize, int fOnlyAnd, int fVerbose ); - int c, nVars = 5, nNodes = 5, nLutSize = 3, fGlucose = 0, fOnlyAnd = 0, fVerbose = 1; char * pTtStr = NULL; + extern void Exa3_ManExactSynthesis( Bmc_EsPar_t * pPars ); + extern void Exa3_ManExactSynthesis2( Bmc_EsPar_t * pPars ); + int c; + Bmc_EsPar_t Pars, * pPars = &Pars; + Bmc_EsParSetDefault( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "INKagvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "INKaogvh" ) ) != EOF ) { switch ( c ) { @@ -8297,9 +8305,9 @@ int Abc_CommandLutExact( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "Command line switch \"-I\" should be followed by an integer.\n" ); goto usage; } - nVars = atoi(argv[globalUtilOptind]); + pPars->nVars = atoi(argv[globalUtilOptind]); globalUtilOptind++; - if ( nVars < 0 ) + if ( pPars->nVars < 0 ) goto usage; break; case 'N': @@ -8308,30 +8316,33 @@ int Abc_CommandLutExact( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "Command line switch \"-N\" should be followed by an integer.\n" ); goto usage; } - nNodes = atoi(argv[globalUtilOptind]); + pPars->nNodes = atoi(argv[globalUtilOptind]); globalUtilOptind++; - if ( nNodes < 0 ) + if ( pPars->nNodes < 0 ) goto usage; break; - case 'K': + case 'K': if ( globalUtilOptind >= argc ) { Abc_Print( -1, "Command line switch \"-K\" should be followed by an integer.\n" ); goto usage; } - nLutSize = atoi(argv[globalUtilOptind]); + pPars->nLutSize = atoi(argv[globalUtilOptind]); globalUtilOptind++; - if ( nLutSize < 0 ) + if ( pPars->nLutSize < 0 ) goto usage; break; case 'a': - fOnlyAnd ^= 1; + pPars->fOnlyAnd ^= 1; + break; + case 'o': + pPars->fFewerVars ^= 1; break; case 'g': - fGlucose ^= 1; + pPars->fGlucose ^= 1; break; case 'v': - fVerbose ^= 1; + pPars->fVerbose ^= 1; break; case 'h': goto usage; @@ -8340,47 +8351,48 @@ int Abc_CommandLutExact( Abc_Frame_t * pAbc, int argc, char ** argv ) } } if ( argc == globalUtilOptind + 1 ) - pTtStr = argv[globalUtilOptind]; - if ( pTtStr == NULL ) + pPars->pTtStr = argv[globalUtilOptind]; + if ( pPars->pTtStr == NULL ) { Abc_Print( -1, "Truth table should be given on the command line.\n" ); return 1; } - if ( (1 << (nVars-2)) != (int)strlen(pTtStr) ) + if ( (1 << (pPars->nVars-2)) != (int)strlen(pPars->pTtStr) ) { - Abc_Print( -1, "Truth table is expected to have %d hex digits (instead of %d).\n", (1 << (nVars-2)), strlen(pTtStr) ); + Abc_Print( -1, "Truth table is expected to have %d hex digits (instead of %d).\n", (1 << (pPars->nVars-2)), strlen(pPars->pTtStr) ); return 1; } - if ( nVars > nNodes * (nLutSize - 1) + 1 ) + if ( pPars->nVars > pPars->nNodes * (pPars->nLutSize - 1) + 1 ) { - Abc_Print( -1, "Function with %d variales cannot be implemented with %d %d-input LUTs.\n", nVars, nNodes, nLutSize ); + Abc_Print( -1, "Function with %d variales cannot be implemented with %d %d-input LUTs.\n", pPars->nVars, pPars->nNodes, pPars->nLutSize ); return 1; } - if ( nVars > 10 ) + if ( pPars->nVars > 10 ) { Abc_Print( -1, "Function should not have more than 10 inputs.\n" ); return 1; } - if ( nLutSize > 6 ) + if ( pPars->nLutSize > 6 ) { Abc_Print( -1, "Node size should not be more than 6 inputs.\n" ); return 1; } - if ( fGlucose ) - Exa3_ManExactSynthesis( pTtStr, nVars, nNodes, nLutSize, fOnlyAnd, fVerbose ); + if ( pPars->fGlucose ) + Exa3_ManExactSynthesis( pPars ); else - Exa3_ManExactSynthesis2( pTtStr, nVars, nNodes, nLutSize, fOnlyAnd, fVerbose ); + Exa3_ManExactSynthesis2( pPars ); return 0; usage: - Abc_Print( -2, "usage: lutexact [-INK ] [-agvh] \n" ); + Abc_Print( -2, "usage: lutexact [-INK ] [-aogvh] \n" ); Abc_Print( -2, "\t exact synthesis of multi-input function using two-input gates\n" ); - Abc_Print( -2, "\t-I : the number of input variables [default = %d]\n", nVars ); - Abc_Print( -2, "\t-N : the number of K-input nodes [default = %d]\n", nNodes ); - Abc_Print( -2, "\t-K : the number of node fanins [default = %d]\n", nLutSize ); - Abc_Print( -2, "\t-a : toggle using only AND-gates when K = 2 [default = %s]\n", fOnlyAnd ? "yes" : "no" ); - Abc_Print( -2, "\t-g : toggle using Glucose 3.0 by Gilles Audemard and Laurent Simon [default = %s]\n", fGlucose ? "yes" : "no" ); - Abc_Print( -2, "\t-v : toggle verbose printout [default = %s]\n", fVerbose ? "yes" : "no" ); + Abc_Print( -2, "\t-I : the number of input variables [default = %d]\n", pPars->nVars ); + Abc_Print( -2, "\t-N : the number of K-input nodes [default = %d]\n", pPars->nNodes ); + Abc_Print( -2, "\t-K : the number of node fanins [default = %d]\n", pPars->nLutSize ); + Abc_Print( -2, "\t-a : toggle using only AND-gates when K = 2 [default = %s]\n", pPars->fOnlyAnd ? "yes" : "no" ); + Abc_Print( -2, "\t-o : toggle using additional optimizations [default = %s]\n", pPars->fFewerVars ? "yes" : "no" ); + Abc_Print( -2, "\t-g : toggle using Glucose 3.0 by Gilles Audemard and Laurent Simon [default = %s]\n", pPars->fGlucose ? "yes" : "no" ); + Abc_Print( -2, "\t-v : toggle verbose printout [default = %s]\n", pPars->fVerbose ? "yes" : "no" ); Abc_Print( -2, "\t-h : print the command usage\n" ); Abc_Print( -2, "\t : truth table in hex notation\n" ); return 1; diff --git a/src/sat/bmc/bmc.h b/src/sat/bmc/bmc.h index 51f207e6..5b914741 100644 --- a/src/sat/bmc/bmc.h +++ b/src/sat/bmc/bmc.h @@ -36,13 +36,39 @@ ABC_NAMESPACE_HEADER_START //#define USE_NODE_ORDER 1 -//#define USE_FIRST_SPECIAL 1 -//#define USE_LESS_VARS 1 //////////////////////////////////////////////////////////////////////// /// BASIC TYPES /// //////////////////////////////////////////////////////////////////////// + +// exact synthesis parameters + +typedef struct Bmc_EsPar_t_ Bmc_EsPar_t; +struct Bmc_EsPar_t_ +{ + int nVars; + int nNodes; + int nLutSize; + int fGlucose; + int fOnlyAnd; + int fFewerVars; + int fVerbose; + char * pTtStr; +}; + +static inline void Bmc_EsParSetDefault( Bmc_EsPar_t * pPars ) +{ + pPars->nVars = 5; // when first GC happens (4096) (degree of 2) + pPars->nNodes = 4; // when each next GC happens (5) + pPars->nLutSize = 3; // log difference compared to unique table + pPars->fGlucose = 0; // minimum gain when reodering is not performed + pPars->fOnlyAnd = 0; // minimum gain when reodering is not performed + pPars->fFewerVars = 0; // minimum gain when reodering is not performed + pPars->fVerbose = 1; // verbose output +} + + // unrolling manager typedef struct Unr_Man_t_ Unr_Man_t; diff --git a/src/sat/bmc/bmcMaj.c b/src/sat/bmc/bmcMaj.c index 4700b1d4..67dcb26c 100644 --- a/src/sat/bmc/bmcMaj.c +++ b/src/sat/bmc/bmcMaj.c @@ -392,6 +392,7 @@ int Maj_ManExactSynthesis( int nVars, int nNodes, int fUseConst, int fUseLine, i typedef struct Exa_Man_t_ Exa_Man_t; struct Exa_Man_t_ { + Bmc_EsPar_t * pPars; // parameters int nVars; // inputs int nNodes; // internal nodes int nObjs; // total objects (nVars inputs + nNodes internal nodes) @@ -438,20 +439,14 @@ int Exa_ManMarkup( Exa_Man_t * p ) { for ( k = 0; k < 2; k++ ) { -#ifdef USE_FIRST_SPECIAL - if ( i == p->nObjs - 1 && k == 0 ) + if ( p->pPars->fFewerVars && i == p->nObjs - 1 && k == 0 ) { j = p->nObjs - 2; Vec_WecPush( p->vOutLits, j, Abc_Var2Lit(p->iVar, 0) ); p->VarMarks[i][k][j] = p->iVar++; continue; } -#endif -#ifdef USE_LESS_VARS - for ( j = 1 - k; j < i - k; j++ ) -#else - for ( j = 0; j < i - k; j++ ) -#endif + for ( j = p->pPars->fFewerVars ? 1 - k : 0; j < i - k; j++ ) { Vec_WecPush( p->vOutLits, j, Abc_Var2Lit(p->iVar, 0) ); p->VarMarks[i][k][j] = p->iVar++; @@ -473,13 +468,14 @@ int Exa_ManMarkup( Exa_Man_t * p ) } return p->iVar; } -Exa_Man_t * Exa_ManAlloc( int nVars, int nNodes, word * pTruth ) +Exa_Man_t * Exa_ManAlloc( Bmc_EsPar_t * pPars, word * pTruth ) { Exa_Man_t * p = ABC_CALLOC( Exa_Man_t, 1 ); - p->nVars = nVars; - p->nNodes = nNodes; - p->nObjs = nVars + nNodes; - p->nWords = Abc_TtWordNum(nVars); + p->pPars = pPars; + p->nVars = pPars->nVars; + p->nNodes = pPars->nNodes; + p->nObjs = pPars->nVars + pPars->nNodes; + p->nWords = Abc_TtWordNum(pPars->nVars); p->pTruth = pTruth; p->vOutLits = Vec_WecStart( p->nObjs ); p->iVar = Exa_ManMarkup( p ); @@ -729,16 +725,16 @@ int Exa_ManAddCnf( Exa_Man_t * p, int iMint ) p->iVar += 3*p->nNodes; return 1; } -void Exa_ManExactSynthesis( char * pTtStr, int nVars, int nNodes, int fOnlyAnd, int fVerbose ) +void Exa_ManExactSynthesis( Bmc_EsPar_t * pPars ) { int i, status, iMint = 1; abctime clkTotal = Abc_Clock(); Exa_Man_t * p; int fCompl = 0; - word pTruth[16]; Abc_TtReadHex( pTruth, pTtStr ); - assert( nVars <= 10 ); - p = Exa_ManAlloc( nVars, nNodes, pTruth ); + word pTruth[16]; Abc_TtReadHex( pTruth, pPars->pTtStr ); + assert( pPars->nVars <= 10 ); + p = Exa_ManAlloc( pPars, pTruth ); if ( pTruth[0] & 1 ) { fCompl = 1; Abc_TtNot( pTruth, p->nWords ); } - status = Exa_ManAddCnfStart( p, fOnlyAnd ); + status = Exa_ManAddCnfStart( p, pPars->fOnlyAnd ); assert( status ); printf( "Running exact synthesis for %d-input function with %d two-input gates...\n", p->nVars, p->nNodes ); for ( i = 0; iMint != -1; i++ ) @@ -747,7 +743,7 @@ void Exa_ManExactSynthesis( char * pTtStr, int nVars, int nNodes, int fOnlyAnd, if ( !Exa_ManAddCnf( p, iMint ) ) break; status = bmcg_sat_solver_solve( p->pSat, NULL, 0 ); - if ( fVerbose ) + if ( pPars->fVerbose ) { printf( "Iter %3d : ", i ); Extra_PrintBinary( stdout, (unsigned *)&iMint, p->nVars ); @@ -775,6 +771,7 @@ void Exa_ManExactSynthesis( char * pTtStr, int nVars, int nNodes, int fOnlyAnd, typedef struct Exa3_Man_t_ Exa3_Man_t; struct Exa3_Man_t_ { + Bmc_EsPar_t * pPars; // parameters int nVars; // inputs int nNodes; // internal nodes int nLutSize; // lut size @@ -823,20 +820,14 @@ static int Exa3_ManMarkup( Exa3_Man_t * p ) { for ( k = 0; k < p->nLutSize; k++ ) { -#ifdef USE_FIRST_SPECIAL - if ( i == p->nObjs - 1 && k == 0 ) + if ( p->pPars->fFewerVars && i == p->nObjs - 1 && k == 0 ) { j = p->nObjs - 2; Vec_WecPush( p->vOutLits, j, Abc_Var2Lit(p->iVar, 0) ); p->VarMarks[i][k][j] = p->iVar++; continue; } -#endif -#ifdef USE_LESS_VARS - for ( j = p->nLutSize - 1 - k; j < i - k; j++ ) -#else - for ( j = 0; j < i - k; j++ ) -#endif + for ( j = p->pPars->fFewerVars ? p->nLutSize - 1 - k : 0; j < i - k; j++ ) { Vec_WecPush( p->vOutLits, j, Abc_Var2Lit(p->iVar, 0) ); p->VarMarks[i][k][j] = p->iVar++; @@ -859,15 +850,16 @@ static int Exa3_ManMarkup( Exa3_Man_t * p ) } return p->iVar; } -static Exa3_Man_t * Exa3_ManAlloc( int nVars, int nNodes, int nLutSize, word * pTruth ) +static Exa3_Man_t * Exa3_ManAlloc( Bmc_EsPar_t * pPars, word * pTruth ) { Exa3_Man_t * p = ABC_CALLOC( Exa3_Man_t, 1 ); - p->nVars = nVars; - p->nNodes = nNodes; - p->nLutSize = nLutSize; - p->LutMask = (1 << nLutSize) - 1; - p->nObjs = nVars + nNodes; - p->nWords = Abc_TtWordNum(nVars); + p->pPars = pPars; + p->nVars = pPars->nVars; + p->nNodes = pPars->nNodes; + p->nLutSize = pPars->nLutSize; + p->LutMask = (1 << pPars->nLutSize) - 1; + p->nObjs = pPars->nVars + pPars->nNodes; + p->nWords = Abc_TtWordNum(pPars->nVars); p->pTruth = pTruth; p->vOutLits = Vec_WecStart( p->nObjs ); p->iVar = Exa3_ManMarkup( p ); @@ -1132,17 +1124,17 @@ static int Exa3_ManAddCnf( Exa3_Man_t * p, int iMint ) p->iVar += (p->nLutSize+1)*p->nNodes; return 1; } -void Exa3_ManExactSynthesis( char * pTtStr, int nVars, int nNodes, int nLutSize, int fOnlyAnd, int fVerbose ) +void Exa3_ManExactSynthesis( Bmc_EsPar_t * pPars ) { int i, status, iMint = 1; abctime clkTotal = Abc_Clock(); Exa3_Man_t * p; int fCompl = 0; - word pTruth[16]; Abc_TtReadHex( pTruth, pTtStr ); - assert( nVars <= 10 ); - assert( nLutSize <= 6 ); - p = Exa3_ManAlloc( nVars, nNodes, nLutSize, pTruth ); + word pTruth[16]; Abc_TtReadHex( pTruth, pPars->pTtStr ); + assert( pPars->nVars <= 10 ); + assert( pPars->nLutSize <= 6 ); + p = Exa3_ManAlloc( pPars, pTruth ); if ( pTruth[0] & 1 ) { fCompl = 1; Abc_TtNot( pTruth, p->nWords ); } - status = Exa3_ManAddCnfStart( p, fOnlyAnd ); + status = Exa3_ManAddCnfStart( p, pPars->fOnlyAnd ); assert( status ); printf( "Running exact synthesis for %d-input function with %d %d-input LUTs...\n", p->nVars, p->nNodes, p->nLutSize ); for ( i = 0; iMint != -1; i++ ) @@ -1151,7 +1143,7 @@ void Exa3_ManExactSynthesis( char * pTtStr, int nVars, int nNodes, int nLutSize, if ( !Exa3_ManAddCnf( p, iMint ) ) break; status = bmcg_sat_solver_solve( p->pSat, NULL, 0 ); - if ( fVerbose ) + if ( pPars->fVerbose ) { printf( "Iter %3d : ", i ); Extra_PrintBinary( stdout, (unsigned *)&iMint, p->nVars ); diff --git a/src/sat/bmc/bmcMaj2.c b/src/sat/bmc/bmcMaj2.c index a3c1027a..b0827b09 100644 --- a/src/sat/bmc/bmcMaj2.c +++ b/src/sat/bmc/bmcMaj2.c @@ -498,6 +498,7 @@ int Maj_ManExactSynthesisTest() typedef struct Exa_Man_t_ Exa_Man_t; struct Exa_Man_t_ { + Bmc_EsPar_t * pPars; // parameters int nVars; // inputs int nNodes; // internal nodes int nObjs; // total objects (nVars inputs + nNodes internal nodes) @@ -544,20 +545,14 @@ static int Exa_ManMarkup( Exa_Man_t * p ) { for ( k = 0; k < 2; k++ ) { -#ifdef USE_FIRST_SPECIAL - if ( i == p->nObjs - 1 && k == 0 ) + if ( p->pPars->fFewerVars && i == p->nObjs - 1 && k == 0 ) { j = p->nObjs - 2; Vec_WecPush( p->vOutLits, j, Abc_Var2Lit(p->iVar, 0) ); p->VarMarks[i][k][j] = p->iVar++; continue; } -#endif -#ifdef USE_LESS_VARS - for ( j = 1 - k; j < i - k; j++ ) -#else - for ( j = 0; j < i - k; j++ ) -#endif + for ( j = p->pPars->fFewerVars ? 1 - k : 0; j < i - k; j++ ) { Vec_WecPush( p->vOutLits, j, Abc_Var2Lit(p->iVar, 0) ); p->VarMarks[i][k][j] = p->iVar++; @@ -579,13 +574,14 @@ static int Exa_ManMarkup( Exa_Man_t * p ) } return p->iVar; } -static Exa_Man_t * Exa_ManAlloc( int nVars, int nNodes, word * pTruth ) +static Exa_Man_t * Exa_ManAlloc( Bmc_EsPar_t * pPars, word * pTruth ) { Exa_Man_t * p = ABC_CALLOC( Exa_Man_t, 1 ); - p->nVars = nVars; - p->nNodes = nNodes; - p->nObjs = nVars + nNodes; - p->nWords = Abc_TtWordNum(nVars); + p->pPars = pPars; + p->nVars = pPars->nVars; + p->nNodes = pPars->nNodes; + p->nObjs = pPars->nVars + pPars->nNodes; + p->nWords = Abc_TtWordNum(pPars->nVars); p->pTruth = pTruth; p->vOutLits = Vec_WecStart( p->nObjs ); p->iVar = Exa_ManMarkup( p ); @@ -835,16 +831,16 @@ static int Exa_ManAddCnf( Exa_Man_t * p, int iMint ) p->iVar += 3*p->nNodes; return 1; } -void Exa_ManExactSynthesis2( char * pTtStr, int nVars, int nNodes, int fOnlyAnd, int fVerbose ) +void Exa_ManExactSynthesis2( Bmc_EsPar_t * pPars ) { int i, status, iMint = 1; abctime clkTotal = Abc_Clock(); Exa_Man_t * p; int fCompl = 0; - word pTruth[16]; Abc_TtReadHex( pTruth, pTtStr ); - assert( nVars <= 10 ); - p = Exa_ManAlloc( nVars, nNodes, pTruth ); + word pTruth[16]; Abc_TtReadHex( pTruth, pPars->pTtStr ); + assert( pPars->nVars <= 10 ); + p = Exa_ManAlloc( pPars, pTruth ); if ( pTruth[0] & 1 ) { fCompl = 1; Abc_TtNot( pTruth, p->nWords ); } - status = Exa_ManAddCnfStart( p, fOnlyAnd ); + status = Exa_ManAddCnfStart( p, pPars->fOnlyAnd ); assert( status ); printf( "Running exact synthesis for %d-input function with %d two-input gates...\n", p->nVars, p->nNodes ); for ( i = 0; iMint != -1; i++ ) @@ -853,7 +849,7 @@ void Exa_ManExactSynthesis2( char * pTtStr, int nVars, int nNodes, int fOnlyAnd, if ( !Exa_ManAddCnf( p, iMint ) ) break; status = sat_solver_solve( p->pSat, NULL, NULL, 0, 0, 0, 0 ); - if ( fVerbose ) + if ( pPars->fVerbose ) { printf( "Iter %3d : ", i ); Extra_PrintBinary( stdout, (unsigned *)&iMint, p->nVars ); @@ -883,6 +879,7 @@ void Exa_ManExactSynthesis2( char * pTtStr, int nVars, int nNodes, int fOnlyAnd, typedef struct Exa3_Man_t_ Exa3_Man_t; struct Exa3_Man_t_ { + Bmc_EsPar_t * pPars; // parameters int nVars; // inputs int nNodes; // internal nodes int nLutSize; // lut size @@ -931,20 +928,14 @@ static int Exa3_ManMarkup( Exa3_Man_t * p ) { for ( k = 0; k < p->nLutSize; k++ ) { -#ifdef USE_FIRST_SPECIAL - if ( i == p->nObjs - 1 && k == 0 ) + if ( p->pPars->fFewerVars && i == p->nObjs - 1 && k == 0 ) { j = p->nObjs - 2; Vec_WecPush( p->vOutLits, j, Abc_Var2Lit(p->iVar, 0) ); p->VarMarks[i][k][j] = p->iVar++; continue; } -#endif -#ifdef USE_LESS_VARS - for ( j = p->nLutSize - 1 - k; j < i - k; j++ ) -#else - for ( j = 0; j < i - k; j++ ) -#endif + for ( j = p->pPars->fFewerVars ? p->nLutSize - 1 - k : 0; j < i - k; j++ ) { Vec_WecPush( p->vOutLits, j, Abc_Var2Lit(p->iVar, 0) ); p->VarMarks[i][k][j] = p->iVar++; @@ -1016,15 +1007,16 @@ static void Exa3_ManInitPolarity( Exa3_Man_t * p ) //intf( "\n" ); } } -static Exa3_Man_t * Exa3_ManAlloc( int nVars, int nNodes, int nLutSize, word * pTruth ) +static Exa3_Man_t * Exa3_ManAlloc( Bmc_EsPar_t * pPars, word * pTruth ) { Exa3_Man_t * p = ABC_CALLOC( Exa3_Man_t, 1 ); - p->nVars = nVars; - p->nNodes = nNodes; - p->nLutSize = nLutSize; - p->LutMask = (1 << nLutSize) - 1; - p->nObjs = nVars + nNodes; - p->nWords = Abc_TtWordNum(nVars); + p->pPars = pPars; + p->nVars = pPars->nVars; + p->nNodes = pPars->nNodes; + p->nLutSize = pPars->nLutSize; + p->LutMask = (1 << pPars->nLutSize) - 1; + p->nObjs = pPars->nVars + pPars->nNodes; + p->nWords = Abc_TtWordNum(pPars->nVars); p->pTruth = pTruth; p->vOutLits = Vec_WecStart( p->nObjs ); p->iVar = Exa3_ManMarkup( p ); @@ -1300,17 +1292,17 @@ static int Exa3_ManAddCnf( Exa3_Man_t * p, int iMint ) p->iVar += (p->nLutSize+1)*p->nNodes; return 1; } -void Exa3_ManExactSynthesis2( char * pTtStr, int nVars, int nNodes, int nLutSize, int fOnlyAnd, int fVerbose ) +void Exa3_ManExactSynthesis2( Bmc_EsPar_t * pPars ) { int i, status, iMint = 1; abctime clkTotal = Abc_Clock(); Exa3_Man_t * p; int fCompl = 0; - word pTruth[16]; Abc_TtReadHex( pTruth, pTtStr ); - assert( nVars <= 10 ); - assert( nLutSize <= 6 ); - p = Exa3_ManAlloc( nVars, nNodes, nLutSize, pTruth ); + word pTruth[16]; Abc_TtReadHex( pTruth, pPars->pTtStr ); + assert( pPars->nVars <= 10 ); + assert( pPars->nLutSize <= 6 ); + p = Exa3_ManAlloc( pPars, pTruth ); if ( pTruth[0] & 1 ) { fCompl = 1; Abc_TtNot( pTruth, p->nWords ); } - status = Exa3_ManAddCnfStart( p, fOnlyAnd ); + status = Exa3_ManAddCnfStart( p, pPars->fOnlyAnd ); assert( status ); printf( "Running exact synthesis for %d-input function with %d %d-input LUTs...\n", p->nVars, p->nNodes, p->nLutSize ); for ( i = 0; iMint != -1; i++ ) @@ -1319,7 +1311,7 @@ void Exa3_ManExactSynthesis2( char * pTtStr, int nVars, int nNodes, int nLutSize if ( !Exa3_ManAddCnf( p, iMint ) ) break; status = sat_solver_solve( p->pSat, NULL, NULL, 0, 0, 0, 0 ); - if ( fVerbose ) + if ( pPars->fVerbose ) { printf( "Iter %3d : ", i ); Extra_PrintBinary( stdout, (unsigned *)&iMint, p->nVars ); -- cgit v1.2.3