From 6274498e0131d650f039c49ee0ed3d3afa6bf766 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 19 Jan 2018 14:03:24 -0800 Subject: Updates to exact synthesis commands. --- src/base/abci/abc.c | 30 +++++++++-- src/sat/bmc/bmc.h | 2 + src/sat/bmc/bmcMaj.c | 146 ++++++++++++++++++++++++++++++++++++++++++-------- src/sat/bmc/bmcMaj3.c | 86 +++++++++++++++++++++++++---- 4 files changed, 226 insertions(+), 38 deletions(-) diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 3467008a..2259d3ff 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -8299,7 +8299,7 @@ int Abc_CommandLutExact( Abc_Frame_t * pAbc, int argc, char ** argv ) Bmc_EsPar_t Pars, * pPars = &Pars; Bmc_EsParSetDefault( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "INKaogvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "INKiaogvh" ) ) != EOF ) { switch ( c ) { @@ -8336,6 +8336,9 @@ int Abc_CommandLutExact( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( pPars->nLutSize < 0 ) goto usage; break; + case 'i': + pPars->fUseIncr ^= 1; + break; case 'a': pPars->fOnlyAnd ^= 1; break; @@ -8388,11 +8391,12 @@ int Abc_CommandLutExact( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: lutexact [-INK ] [-aogvh] \n" ); + Abc_Print( -2, "usage: lutexact [-INK ] [-iaogvh] \n" ); Abc_Print( -2, "\t exact synthesis of I-input function using N K-input gates\n" ); 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-i : toggle using incremental solving [default = %s]\n", pPars->fUseIncr ? "yes" : "no" ); 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" ); @@ -8420,7 +8424,7 @@ int Abc_CommandAllExact( Abc_Frame_t * pAbc, int argc, char ** argv ) Bmc_EsPar_t Pars, * pPars = &Pars; Bmc_EsParSetDefault( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "MINKaoegvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "MINKiaoegvh" ) ) != EOF ) { switch ( c ) { @@ -8468,6 +8472,9 @@ int Abc_CommandAllExact( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( pPars->nLutSize < 0 ) goto usage; break; + case 'i': + pPars->fUseIncr ^= 1; + break; case 'a': pPars->fOnlyAnd ^= 1; break; @@ -8499,6 +8506,7 @@ int Abc_CommandAllExact( Abc_Frame_t * pAbc, int argc, char ** argv ) pPars->nVars = pPars->nMajSupp; pPars->nLutSize = 3; pPars->fMajority = 1; + pPars->fUseIncr = 1; if ( pPars->nNodes == 0 ) { if ( pPars->nMajSupp == 5 ) @@ -8549,16 +8557,30 @@ int Abc_CommandAllExact( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "Node size should not be more than 6 inputs.\n" ); return 1; } + if ( !pPars->fUseIncr ) + { + if ( pPars->fMajority ) + { + Abc_Print( -1, "Cannot synthesize majority in the non-incremental mode (use \'-i\').\n" ); + return 1; + } + if ( pPars->nLutSize > 3 ) + { + Abc_Print( -1, "Cannot synthesize LUT4 and larger in non-incremental mode (use \'-i\').\n" ); + return 1; + } + } Zyx_ManExactSynthesis( pPars ); return 0; usage: - Abc_Print( -2, "usage: allexact [-MIKN ] [-aoevh] \n" ); + Abc_Print( -2, "usage: allexact [-MIKN ] [-iaoevh] \n" ); Abc_Print( -2, "\t exact synthesis of I-input function using N K-input gates\n" ); Abc_Print( -2, "\t-M : the majority support size (overrides -I and -K) [default = %d]\n", pPars->nMajSupp ); Abc_Print( -2, "\t-I : the number of input variables [default = %d]\n", pPars->nVars ); Abc_Print( -2, "\t-K : the number of node fanins [default = %d]\n", pPars->nLutSize ); Abc_Print( -2, "\t-N : the number of K-input nodes [default = %d]\n", pPars->nNodes ); + Abc_Print( -2, "\t-i : toggle using incremental solving [default = %s]\n", pPars->fUseIncr ? "yes" : "no" ); 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 node ordering by fanins [default = %s]\n", pPars->fOrderNodes ? "yes" : "no" ); Abc_Print( -2, "\t-e : toggle enumerating all solutions [default = %s]\n", pPars->fEnumSols ? "yes" : "no" ); diff --git a/src/sat/bmc/bmc.h b/src/sat/bmc/bmc.h index 752bab5b..1d5180f3 100644 --- a/src/sat/bmc/bmc.h +++ b/src/sat/bmc/bmc.h @@ -52,6 +52,7 @@ struct Bmc_EsPar_t_ int nLutSize; int nMajSupp; int fMajority; + int fUseIncr; int fOnlyAnd; int fGlucose; int fOrderNodes; @@ -69,6 +70,7 @@ static inline void Bmc_EsParSetDefault( Bmc_EsPar_t * pPars ) pPars->nLutSize = 2; pPars->nMajSupp = 0; pPars->fMajority = 0; + pPars->fUseIncr = 0; pPars->fOnlyAnd = 0; pPars->fGlucose = 0; pPars->fOrderNodes = 0; diff --git a/src/sat/bmc/bmcMaj.c b/src/sat/bmc/bmcMaj.c index 92ff06ee..efa8d857 100644 --- a/src/sat/bmc/bmcMaj.c +++ b/src/sat/bmc/bmcMaj.c @@ -799,14 +799,41 @@ struct Exa3_Man_t_ int iVar; // the next available SAT variable word * pTruth; // truth table Vec_Wrd_t * vInfo; // nVars + nNodes + 1 + Vec_Bit_t * vUsed2; // bit masks + Vec_Bit_t * vUsed3; // bit masks int VarMarks[MAJ_NOBJS][6][MAJ_NOBJS]; // variable marks int VarVals[MAJ_NOBJS]; // values of the first nVars variables Vec_Wec_t * vOutLits; // output vars bmcg_sat_solver * pSat; // SAT solver + int nUsed[2]; }; static inline word * Exa3_ManTruth( Exa3_Man_t * p, int v ) { return Vec_WrdEntryP( p->vInfo, p->nWords * v ); } +static inline int Exa3_ManIsUsed2( Exa3_Man_t * p, int m, int n, int i, int j ) +{ + int Pos = ((m * p->pPars->nNodes + n - p->pPars->nVars) * p->nObjs + i) * p->nObjs + j; + p->nUsed[0]++; + assert( i < n && j < n && i < j ); + if ( Vec_BitEntry(p->vUsed2, Pos) ) + return 1; + p->nUsed[1]++; + Vec_BitWriteEntry( p->vUsed2, Pos, 1 ); + return 0; +} + +static inline int Exa3_ManIsUsed3( Exa3_Man_t * p, int m, int n, int i, int j, int k ) +{ + int Pos = (((m * p->pPars->nNodes + n - p->pPars->nVars) * p->nObjs + i) * p->nObjs + j) * p->nObjs + k; + p->nUsed[0]++; + assert( i < n && j < n && k < n && i < j && j < k ); + if ( Vec_BitEntry(p->vUsed3, Pos) ) + return 1; + p->nUsed[1]++; + Vec_BitWriteEntry( p->vUsed3, Pos, 1 ); + return 0; +} + /**Function************************************************************* @@ -882,6 +909,10 @@ static Exa3_Man_t * Exa3_ManAlloc( Bmc_EsPar_t * pPars, word * pTruth ) p->vOutLits = Vec_WecStart( p->nObjs ); p->iVar = Exa3_ManMarkup( p ); p->vInfo = Exa3_ManTruthTables( p ); + if ( p->pPars->nLutSize == 2 ) + p->vUsed2 = Vec_BitStart( (1 << p->pPars->nVars) * p->pPars->nNodes * p->nObjs * p->nObjs ); + else if ( p->pPars->nLutSize == 3 ) + p->vUsed3 = Vec_BitStart( (1 << p->pPars->nVars) * p->pPars->nNodes * p->nObjs * p->nObjs * p->nObjs ); p->pSat = bmcg_sat_solver_start(); bmcg_sat_solver_set_nvars( p->pSat, p->iVar ); return p; @@ -890,6 +921,8 @@ static void Exa3_ManFree( Exa3_Man_t * p ) { bmcg_sat_solver_stop( p->pSat ); Vec_WrdFree( p->vInfo ); + Vec_BitFreeP( &p->vUsed2 ); + Vec_BitFreeP( &p->vUsed3 ); Vec_WecFree( p->vOutLits ); ABC_FREE( p ); } @@ -1041,18 +1074,21 @@ static int Exa3_ManAddCnfStart( Exa3_Man_t * p, int fOnlyAnd ) return 0; } } -#ifdef USE_NODE_ORDER +//#ifdef USE_NODE_ORDER // node ordering - for ( j = p->nVars; j < i; j++ ) - for ( n = 0; n < p->nObjs; n++ ) if ( p->VarMarks[i][0][n] ) - for ( m = n+1; m < p->nObjs; m++ ) if ( p->VarMarks[j][0][m] ) + if ( p->pPars->fUseIncr ) { - pLits2[0] = Abc_Var2Lit( p->VarMarks[i][0][n], 1 ); - pLits2[1] = Abc_Var2Lit( p->VarMarks[j][0][m], 1 ); - if ( !bmcg_sat_solver_addclause( p->pSat, pLits2, 2 ) ) - return 0; + for ( j = p->nVars; j < i; j++ ) + for ( n = 0; n < p->nObjs; n++ ) if ( p->VarMarks[i][0][n] ) + for ( m = n+1; m < p->nObjs; m++ ) if ( p->VarMarks[j][0][m] ) + { + pLits2[0] = Abc_Var2Lit( p->VarMarks[i][0][n], 1 ); + pLits2[1] = Abc_Var2Lit( p->VarMarks[j][0][m], 1 ); + if ( !bmcg_sat_solver_addclause( p->pSat, pLits2, 2 ) ) + return 0; + } } -#endif +//#endif if ( p->nLutSize != 2 ) continue; // two-input functions @@ -1123,7 +1159,7 @@ static int Exa3_ManAddCnf( Exa3_Man_t * p, int iMint ) continue; for ( k = 0; k <= p->LutMask; k++ ) { - int pLits[8], nLits = 0; + int pLits[16], nLits = 0; if ( k == 0 && n == 1 ) continue; //pLits[nLits++] = Abc_Var2Lit( iBaseSatVarI + 0, (k&1) ); @@ -1142,6 +1178,69 @@ static int Exa3_ManAddCnf( Exa3_Man_t * p, int iMint ) p->iVar += (p->nLutSize+1)*p->nNodes; return 1; } + +static int Exa3_ManAddCnf2( Exa3_Man_t * p, int iMint ) +{ + int iBaseSatVar = p->iVar + p->nNodes*iMint; + // save minterm values + int i, k, n, j, Value = Abc_TtGetBit(p->pTruth, iMint); + for ( i = 0; i < p->nVars; i++ ) + p->VarVals[i] = (iMint >> i) & 1; + //printf( "Adding clauses for minterm %d with value %d.\n", iMint, Value ); + for ( i = p->nVars; i < p->nObjs; i++ ) + { +// int iBaseSatVarI = p->iVar + (p->nLutSize+1)*(i - p->nVars); + int iVarStart = 1 + p->LutMask*(i - p->nVars); + // collect fanin variables + int pFanins[16]; + for ( j = 0; j < p->nLutSize; j++ ) + pFanins[j] = Exa3_ManFindFanin(p, i, j); + // check cache + if ( p->pPars->nLutSize == 2 && Exa3_ManIsUsed2(p, iMint, i, pFanins[1], pFanins[0]) ) + continue; + if ( p->pPars->nLutSize == 3 && Exa3_ManIsUsed3(p, iMint, i, pFanins[2], pFanins[1], pFanins[0]) ) + continue; + // node functionality + for ( n = 0; n < 2; n++ ) + { + if ( i == p->nObjs - 1 && n == Value ) + continue; + for ( k = 0; k <= p->LutMask; k++ ) + { + int pLits[16], nLits = 0; + if ( k == 0 && n == 1 ) + continue; + for ( j = 0; j < p->nLutSize; j++ ) + { +// pLits[nLits++] = Abc_Var2Lit( iBaseSatVar + j, (k >> j) & 1 ); + pLits[nLits++] = Abc_Var2Lit( p->VarMarks[i][j][pFanins[j]], 1 ); + if ( pFanins[j] >= p->nVars ) + pLits[nLits++] = Abc_Var2Lit( iBaseSatVar + pFanins[j] - p->nVars, (k >> j) & 1 ); + else if ( p->VarVals[pFanins[j]] != ((k >> j) & 1) ) + break; + } + if ( j < p->nLutSize ) + continue; +// if ( i != p->nObjs - 1 ) pLits[nLits++] = Abc_Var2Lit( iBaseSatVar + j, !n ); + if ( i != p->nObjs - 1 ) pLits[nLits++] = Abc_Var2Lit( iBaseSatVar + i - p->nVars, !n ); + if ( k > 0 ) pLits[nLits++] = Abc_Var2Lit( iVarStart + k-1, n ); + assert( nLits <= 2*p->nLutSize+2 ); + if ( !bmcg_sat_solver_addclause( p->pSat, pLits, nLits ) ) + return 0; + } + } + } + return 1; +} +void Exa3_ManPrint( Exa3_Man_t * p, int i, int iMint, abctime clk ) +{ + printf( "Iter%6d : ", i ); + Extra_PrintBinary( stdout, (unsigned *)&iMint, p->nVars ); + printf( " Var =%5d ", bmcg_sat_solver_varnum(p->pSat) ); + printf( "Cla =%6d ", bmcg_sat_solver_clausenum(p->pSat) ); + printf( "Conf =%9d ", bmcg_sat_solver_conflictnum(p->pSat) ); + Abc_PrintTime( 1, "Time", clk ); +} void Exa3_ManExactSynthesis( Bmc_EsPar_t * pPars ) { int i, status, iMint = 1; @@ -1155,30 +1254,31 @@ void Exa3_ManExactSynthesis( Bmc_EsPar_t * pPars ) 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 ); + if ( pPars->fUseIncr ) + { + bmcg_sat_solver_set_nvars( p->pSat, p->iVar + p->nNodes*(1 << p->nVars) ); + status = bmcg_sat_solver_solve( p->pSat, NULL, 0 ); + assert( status == GLUCOSE_SAT ); + } for ( i = 0; iMint != -1; i++ ) { abctime clk = Abc_Clock(); - if ( !Exa3_ManAddCnf( p, iMint ) ) + if ( pPars->fUseIncr ? !Exa3_ManAddCnf2( p, iMint ) : !Exa3_ManAddCnf( p, iMint ) ) break; status = bmcg_sat_solver_solve( p->pSat, NULL, 0 ); - if ( pPars->fVerbose ) - { - printf( "Iter %3d : ", i ); - Extra_PrintBinary( stdout, (unsigned *)&iMint, p->nVars ); - printf( " Var =%5d ", p->iVar ); - printf( "Cla =%6d ", bmcg_sat_solver_clausenum(p->pSat) ); - printf( "Conf =%9d ", bmcg_sat_solver_conflictnum(p->pSat) ); - Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); - } + if ( pPars->fVerbose && (!pPars->fUseIncr || i % 100 == 0) ) + Exa3_ManPrint( p, i, iMint, Abc_Clock() - clkTotal ); if ( status == GLUCOSE_UNSAT ) - { - printf( "The problem has no solution.\n" ); break; - } iMint = Exa3_ManEval( p ); } + if ( pPars->fVerbose ) + Exa3_ManPrint( p, i, iMint, Abc_Clock() - clkTotal ); if ( iMint == -1 ) Exa3_ManPrintSolution( p, fCompl ); + else + printf( "The problem has no solution.\n" ); + printf( "Added = %d. Tried = %d. ", p->nUsed[1], p->nUsed[0] ); Exa3_ManFree( p ); Abc_PrintTime( 1, "Total runtime", Abc_Clock() - clkTotal ); } diff --git a/src/sat/bmc/bmcMaj3.c b/src/sat/bmc/bmcMaj3.c index f4949af5..2a3bca07 100644 --- a/src/sat/bmc/bmcMaj3.c +++ b/src/sat/bmc/bmcMaj3.c @@ -575,9 +575,11 @@ struct Zyx_Man_t_ static inline word * Zyx_ManTruth( Zyx_Man_t * p, int v ) { return Vec_WrdEntryP( p->vInfo, p->nWords * v ); } -static inline int Zyx_FuncVar( Zyx_Man_t * p, int i, int m ) { return (p->LutMask + 1) * (i - p->pPars->nVars) + m; } -static inline int Zyx_TopoVar( Zyx_Man_t * p, int i, int f ) { return p->TopoBase + p->nObjs * (i - p->pPars->nVars) + f; } -static inline int Zyx_MintVar( Zyx_Man_t * p, int m, int i ) { return p->MintBase + p->nObjs * m + i; } +static inline int Zyx_FuncVar( Zyx_Man_t * p, int i, int m ) { return (p->LutMask + 1) * (i - p->pPars->nVars) + m; } +static inline int Zyx_TopoVar( Zyx_Man_t * p, int i, int f ) { return p->TopoBase + p->nObjs * (i - p->pPars->nVars) + f; } +static inline int Zyx_MintVar( Zyx_Man_t * p, int m, int i ) { return p->MintBase + p->nObjs * m + i; } + +//static inline int Zyx_MintVar2( Zyx_Man_t * p, int m, int i, int f ) { assert(i >= p->pPars->nVars); return p->MintBase + m * p->pPars->nNodes * (p->pPars->nLutSize + 1) + (i - p->pPars->nVars) * (p->pPars->nLutSize + 1) + f; } static inline int Zyx_ManIsUsed2( Zyx_Man_t * p, int m, int n, int i, int j ) { @@ -801,12 +803,15 @@ Zyx_Man_t * Zyx_ManAlloc( Bmc_EsPar_t * pPars, word * pTruth ) p->vVarValues = Vec_IntStartFull( p->MintBase + (1 << p->pPars->nVars) * p->nObjs ); p->vMidMints = Vec_IntAlloc( 1 << p->pPars->nVars ); p->vInfo = Zyx_ManTruthTables( p, pTruth ); - if ( p->pPars->nLutSize == 2 || p->pPars->fMajority ) - p->vUsed2 = Vec_BitStart( (1 << p->pPars->nVars) * p->pPars->nNodes * p->nObjs * p->nObjs ); - else if ( p->pPars->nLutSize == 3 ) - p->vUsed3 = Vec_BitStart( (1 << p->pPars->nVars) * p->pPars->nNodes * p->nObjs * p->nObjs * p->nObjs ); p->vPairs = Zyx_ManCreateSymVarPairs( p->pPars->fMajority ? Zyx_ManTruth(p, p->nObjs) : pTruth, p->pPars->nVars ); p->pSat = bmcg_sat_solver_start(); + if ( pPars->fUseIncr ) + { + if ( p->pPars->nLutSize == 2 || p->pPars->fMajority ) + p->vUsed2 = Vec_BitStart( (1 << p->pPars->nVars) * p->pPars->nNodes * p->nObjs * p->nObjs ); + else if ( p->pPars->nLutSize == 3 ) + p->vUsed3 = Vec_BitStart( (1 << p->pPars->nVars) * p->pPars->nNodes * p->nObjs * p->nObjs * p->nObjs ); + } bmcg_sat_solver_set_nvars( p->pSat, p->MintBase + (1 << p->pPars->nVars) * p->nObjs ); Zyx_ManSetupVars( p ); Zyx_ManAddCnfStart( p ); @@ -995,9 +1000,8 @@ int Zyx_ManAddCnfBlockSolution( Zyx_Man_t * p ) Vec_IntFree( vLits ); return 1; } -int Zyx_ManAddCnfLazyFunc( Zyx_Man_t * p, int iMint ) +int Zyx_ManAddCnfLazyFunc2( Zyx_Man_t * p, int iMint ) { - int Sets[3][2] = {{0, 1}, {0, 2}, {1, 2}}; int i, k, n, j, s; assert( !p->pPars->fMajority || p->pPars->nLutSize == 3 ); //printf( "Adding functionality clauses for minterm %d.\n", iMint ); @@ -1008,6 +1012,7 @@ int Zyx_ManAddCnfLazyFunc( Zyx_Man_t * p, int iMint ) assert( nFanins == p->pPars->nLutSize ); if ( p->pPars->fMajority ) { + int Sets[3][2] = {{0, 1}, {0, 2}, {1, 2}}; for ( k = 0; k < 3; k++ ) { if ( Zyx_ManIsUsed2(p, iMint, i, p->pFanins[i][Sets[k][0]], p->pFanins[i][Sets[k][1]]) ) @@ -1051,6 +1056,65 @@ int Zyx_ManAddCnfLazyFunc( Zyx_Man_t * p, int iMint ) return 1; } +int Zyx_ManAddCnfLazyFunc( Zyx_Man_t * p, int iMint ) +{ + int i, k, n, j, s, t, u; + //printf( "Adding clauses for minterm %d with value %d.\n", iMint, Value ); + assert( !p->pPars->fMajority && p->pPars->nLutSize < 4 ); + p->Counts[iMint]++; + if ( p->pPars->nLutSize == 2 ) + { + for ( i = p->pPars->nVars; i < p->nObjs; i++ ) + for ( s = 0; s < i; s++ ) + for ( t = s+1; t < i; t++ ) + { + p->pFanins[i][0] = s; + p->pFanins[i][1] = t; + for ( k = 0; k <= p->LutMask; k++ ) + for ( n = 0; n < 2; n++ ) + { + p->nLits[0] = 0; + p->pLits[0][p->nLits[0]++] = Abc_Var2Lit( Zyx_FuncVar(p, i, k), n ); + for ( j = 0; j < p->pPars->nLutSize; j++ ) + { + p->pLits[0][p->nLits[0]++] = Abc_Var2Lit( Zyx_TopoVar(p, i, p->pFanins[i][j]), 1 ); + p->pLits[0][p->nLits[0]++] = Abc_Var2Lit( Zyx_MintVar(p, iMint, p->pFanins[i][j]), (k >> j) & 1 ); + } + p->pLits[0][p->nLits[0]++] = Abc_Var2Lit( Zyx_MintVar(p, iMint, i), !n ); + if ( !bmcg_sat_solver_addclause( p->pSat, p->pLits[0], p->nLits[0] ) ) + return 0; + } + } + } + else if ( p->pPars->nLutSize == 3 ) + { + for ( i = p->pPars->nVars; i < p->nObjs; i++ ) + for ( s = 0; s < i; s++ ) + for ( t = s+1; t < i; t++ ) + for ( u = t+1; u < i; u++ ) + { + p->pFanins[i][0] = s; + p->pFanins[i][1] = t; + p->pFanins[i][2] = u; + for ( k = 0; k <= p->LutMask; k++ ) + for ( n = 0; n < 2; n++ ) + { + p->nLits[0] = 0; + p->pLits[0][p->nLits[0]++] = Abc_Var2Lit( Zyx_FuncVar(p, i, k), n ); + for ( j = 0; j < p->pPars->nLutSize; j++ ) + { + p->pLits[0][p->nLits[0]++] = Abc_Var2Lit( Zyx_TopoVar(p, i, p->pFanins[i][j]), 1 ); + p->pLits[0][p->nLits[0]++] = Abc_Var2Lit( Zyx_MintVar(p, iMint, p->pFanins[i][j]), (k >> j) & 1 ); + } + p->pLits[0][p->nLits[0]++] = Abc_Var2Lit( Zyx_MintVar(p, iMint, i), !n ); + if ( !bmcg_sat_solver_addclause( p->pSat, p->pLits[0], p->nLits[0] ) ) + return 0; + } + } + } + return 1; +} + /**Function************************************************************* Synopsis [] @@ -1251,14 +1315,14 @@ void Zyx_ManExactSynthesis( Bmc_EsPar_t * pPars ) else break; } - if ( !Zyx_ManAddCnfLazyFunc(p, iMint) ) + if ( pPars->fUseIncr ? !Zyx_ManAddCnfLazyFunc2(p, iMint) : !Zyx_ManAddCnfLazyFunc(p, iMint) ) { printf( "Became UNSAT after adding constraints for minterm %d\n", iMint ); status = GLUCOSE_UNSAT; break; } status = bmcg_sat_solver_solve( p->pSat, NULL, 0 ); - if ( pPars->fVerbose && Iter % 100 == 0 ) + if ( pPars->fVerbose && (!pPars->fUseIncr || Iter % 100 == 0) ) { Zyx_ManPrint( p, Iter, iMint, nLazyAll, Abc_Clock() - clk ); clk = Abc_Clock(); -- cgit v1.2.3