From 14b7a520a14eba14aeb8ae63f692e23add5c660f Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 15 May 2015 22:36:11 -0700 Subject: Bug fix in 'dsd_tune' when processing cells with 0-input LUTs. --- src/map/if/ifTune.c | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) (limited to 'src/map/if/ifTune.c') 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; } -- cgit v1.2.3