diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2017-12-28 13:26:08 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2017-12-28 13:26:08 -0800 |
| commit | feebac4156f8d2314e664aa9ac5d33157c3df5b8 (patch) | |
| tree | dada9e46560d7597c3d630dfc712c4bfcb82b213 | |
| parent | 680af1891b76db8942c72dd1156cd949e4beca7f (diff) | |
| download | abc-feebac4156f8d2314e664aa9ac5d33157c3df5b8.tar.gz abc-feebac4156f8d2314e664aa9ac5d33157c3df5b8.tar.bz2 abc-feebac4156f8d2314e664aa9ac5d33157c3df5b8.zip | |
Corner-case bug fixed in CNF generation.
| -rw-r--r-- | src/aig/gia/giaMf.c | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/src/aig/gia/giaMf.c b/src/aig/gia/giaMf.c index 7d5e14c1..7ec14f9a 100644 --- a/src/aig/gia/giaMf.c +++ b/src/aig/gia/giaMf.c @@ -420,8 +420,13 @@ Cnf_Dat_t * Mf_ManDeriveCnf( Mf_Man_t * p, int fCnfObjIds, int fAddOrCla ) continue; pCut = Mf_ObjCutBest( p, Id ); iFunc = Abc_Lit2Var( Mf_CutFunc(pCut) ); - //Dau_DsdPrintFromTruth( Vec_MemReadEntry(p->vTtMem, iFunc), 3 ); fComplLast = Abc_LitIsCompl( Mf_CutFunc(pCut) ); + if ( iFunc == 0 ) // constant cut + { + pCnf->pClauses[iCla++] = pCnf->pClauses[0] + iLit; + pCnf->pClauses[0][iLit++] = Abc_Var2Lit(pCnfIds[Id], !fComplLast); + continue; + } for ( k = 0; k < Mf_CutSize(pCut); k++ ) pFanins[k] = pCnfIds[pCut[k+1]]; pFanins[k++] = pCnfIds[Id]; |