diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2015-05-15 22:36:11 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2015-05-15 22:36:11 -0700 |
| commit | 14b7a520a14eba14aeb8ae63f692e23add5c660f (patch) | |
| tree | 061147c2f98676be89dc43aecc61bd02f4c5910b /src | |
| parent | 37b6b5f1f8a46d6f233a352b8874352fc5097dbe (diff) | |
| download | abc-14b7a520a14eba14aeb8ae63f692e23add5c660f.tar.gz abc-14b7a520a14eba14aeb8ae63f692e23add5c660f.tar.bz2 abc-14b7a520a14eba14aeb8ae63f692e23add5c660f.zip | |
Bug fix in 'dsd_tune' when processing cells with 0-input LUTs.
Diffstat (limited to 'src')
| -rw-r--r-- | src/map/if/ifTune.c | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/src/map/if/ifTune.c b/src/map/if/ifTune.c index d4e336ed..7fe7a4bb 100644 --- a/src/map/if/ifTune.c +++ b/src/map/if/ifTune.c @@ -1111,9 +1111,10 @@ int Ifn_NtkAddClauses( Ifn_Ntk_t * p, int * pValues, sat_solver * pSat ) int i, f, v, nLits, pLits[IFN_INS+2], pLits2[IFN_INS+2]; // assign new variables int nSatVars = sat_solver_nvars(pSat); - for ( i = 0; i < p->nObjs-1; i++ ) +// for ( i = 0; i < p->nObjs-1; i++ ) + for ( i = 0; i < p->nObjs; i++ ) p->Nodes[i].Var = nSatVars++; - p->Nodes[p->nObjs-1].Var = 0xFFFF; + //p->Nodes[p->nObjs-1].Var = 0xFFFF; sat_solver_setnvars( pSat, nSatVars ); // verify variable values for ( i = 0; i < p->nVars; i++ ) @@ -1237,6 +1238,10 @@ int Ifn_NtkAddClauses( Ifn_Ntk_t * p, int * pValues, sat_solver * pSat ) else assert( 0 ); //printf( "\n" ); } + // add last clause (not needed if the root node is IFN_DSD_PRIME) + pLits[0] = Abc_Var2Lit( p->Nodes[p->nObjs-1].Var, pValues[p->nObjs-1]==0 ); + if ( !Ifn_AddClause( pSat, pLits, pLits + 1 ) ) + return 0; return 1; } |