diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2014-06-23 14:04:40 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2014-06-23 14:04:40 -0700 |
| commit | e19d21a09b1854a35b5a0b44e43b3dd307a7f9a0 (patch) | |
| tree | 89a3d76f339f97f049c75aa97b91530a10979e8d /src/aig/gia/giaMf.c | |
| parent | 938ffa5a7dede96fcd3c9d1dc59eb9bdfa5ebe11 (diff) | |
| download | abc-e19d21a09b1854a35b5a0b44e43b3dd307a7f9a0.tar.gz abc-e19d21a09b1854a35b5a0b44e43b3dd307a7f9a0.tar.bz2 abc-e19d21a09b1854a35b5a0b44e43b3dd307a7f9a0.zip | |
Improvements to CNF generation.
Diffstat (limited to 'src/aig/gia/giaMf.c')
| -rw-r--r-- | src/aig/gia/giaMf.c | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/src/aig/gia/giaMf.c b/src/aig/gia/giaMf.c index 89958e4c..043d4fa7 100644 --- a/src/aig/gia/giaMf.c +++ b/src/aig/gia/giaMf.c @@ -339,7 +339,6 @@ Cnf_Dat_t * Mf_ManDeriveCnf( Mf_Man_t * p, int fCnfObjIds, int fAddOrCla ) // create CNF IDs if ( fCnfObjIds ) { - int iVar = 1; iVar += 1 + Gia_ManCiNum(p->pGia) + Gia_ManCoNum(p->pGia); Gia_ManForEachCoId( p->pGia, Id, i ) Vec_IntWriteEntry( vCnfIds, Id, Id ); @@ -353,7 +352,6 @@ Cnf_Dat_t * Mf_ManDeriveCnf( Mf_Man_t * p, int fCnfObjIds, int fAddOrCla ) } else { - int iVar = 1; Gia_ManForEachCoId( p->pGia, Id, i ) Vec_IntWriteEntry( vCnfIds, Id, iVar++ ); Gia_ManForEachAndReverseId( p->pGia, Id ) @@ -479,7 +477,7 @@ Cnf_Dat_t * Mf_ManDeriveCnf( Mf_Man_t * p, int fCnfObjIds, int fAddOrCla ) static inline int Mf_CutComputeTruth6( Mf_Man_t * p, Mf_Cut_t * pCut0, Mf_Cut_t * pCut1, int fCompl0, int fCompl1, Mf_Cut_t * pCutR, int fIsXor ) { // extern int Mf_ManTruthCanonicize( word * t, int nVars ); - int nOldSupp = pCutR->nLeaves, nCubes = 0, truthId, fCompl; word t; + int nOldSupp = pCutR->nLeaves, truthId, fCompl; word t; word t0 = *Vec_MemReadEntry(p->vTtMem, Abc_Lit2Var(pCut0->iFunc)); word t1 = *Vec_MemReadEntry(p->vTtMem, Abc_Lit2Var(pCut1->iFunc)); if ( Abc_LitIsCompl(pCut0->iFunc) ^ fCompl0 ) t0 = ~t0; @@ -531,7 +529,7 @@ static inline int Mf_CutComputeTruth( Mf_Man_t * p, Mf_Cut_t * pCut0, Mf_Cut_t * } static inline int Mf_CutComputeTruthMux6( Mf_Man_t * p, Mf_Cut_t * pCut0, Mf_Cut_t * pCut1, Mf_Cut_t * pCutC, int fCompl0, int fCompl1, int fComplC, Mf_Cut_t * pCutR ) { - int nOldSupp = pCutR->nLeaves, nCubes = 0, truthId, fCompl; word t; + int nOldSupp = pCutR->nLeaves, truthId, fCompl; word t; word t0 = *Vec_MemReadEntry(p->vTtMem, Abc_Lit2Var(pCut0->iFunc)); word t1 = *Vec_MemReadEntry(p->vTtMem, Abc_Lit2Var(pCut1->iFunc)); word tC = *Vec_MemReadEntry(p->vTtMem, Abc_Lit2Var(pCutC->iFunc)); |