luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Corner-case bug fixed in CNF generation.

This commit is contained in:
Alan Mishchenko 2017-12-28 13:26:08 -08:00
parent 680af1891b
commit feebac4156
1 changed files with 6 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
src/aig/gia/giaMf.c
View File

@ -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];