diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2007-07-26 08:01:00 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2007-07-26 08:01:00 -0700 |
commit | 054e2cd3a8ab4ada55db4def2d6ce7d309341e07 (patch) | |
tree | a951eeeafa90dc555cb6442151761190e0b5af6a /src/aig/cnf/cnfWrite.c | |
parent | 64dc240b904adafee78e2a66a1fc31b717f8985f (diff) | |
download | abc-054e2cd3a8ab4ada55db4def2d6ce7d309341e07.tar.gz abc-054e2cd3a8ab4ada55db4def2d6ce7d309341e07.tar.bz2 abc-054e2cd3a8ab4ada55db4def2d6ce7d309341e07.zip |
Version abc70726
Diffstat (limited to 'src/aig/cnf/cnfWrite.c')
-rw-r--r-- | src/aig/cnf/cnfWrite.c | 85 |
1 files changed, 24 insertions, 61 deletions
diff --git a/src/aig/cnf/cnfWrite.c b/src/aig/cnf/cnfWrite.c index 22c4240a..41a00732 100644 --- a/src/aig/cnf/cnfWrite.c +++ b/src/aig/cnf/cnfWrite.c @@ -127,42 +127,15 @@ int Cnf_IsopCountLiterals( Vec_Int_t * vIsop, int nVars ) SeeAlso [] ***********************************************************************/ -int Cnf_SopWriteCube( char Cube, int * pVars, int fCompl, int * pLiterals ) -{ - int nLits = 4, b; - for ( b = 0; b < 4; b++ ) - { - if ( Cube % 3 == 0 ) - *pLiterals++ = 2 * pVars[b] + !fCompl; - else if ( Cube % 3 == 1 ) - *pLiterals++ = 2 * pVars[b] + fCompl; - else - nLits--; - Cube = Cube / 3; - } - return nLits; -} - -/**Function************************************************************* - - Synopsis [Writes the cube and returns the number of literals in it.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Cnf_IsopWriteCube( int Cube, int nVars, int * pVars, int fCompl, int * pLiterals ) +int Cnf_IsopWriteCube( int Cube, int nVars, int * pVars, int * pLiterals ) { int nLits = nVars, b; for ( b = 0; b < nVars; b++ ) { - if ( (Cube & 3) == 1 ) - *pLiterals++ = 2 * pVars[b] + !fCompl; - else if ( (Cube & 3) == 2 ) - *pLiterals++ = 2 * pVars[b] + fCompl; + if ( (Cube & 3) == 1 ) // value 0 --> write positive literal + *pLiterals++ = 2 * pVars[b]; + else if ( (Cube & 3) == 2 ) // value 1 --> write negative literal + *pLiterals++ = 2 * pVars[b] + 1; else nLits--; Cube >>= 2; @@ -186,9 +159,10 @@ Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped ) Aig_Obj_t * pObj; Cnf_Dat_t * pCnf; Cnf_Cut_t * pCut; + Vec_Int_t * vCover, * vSopTemp; int OutVar, pVars[32], * pLits, ** pClas; unsigned uTruth; - int i, k, nLiterals, nClauses, nCubes, Cube, Number; + int i, k, nLiterals, nClauses, Cube, Number; // count the number of literals and clauses nLiterals = 1 + Aig_ManPoNum( p->pManAig ); @@ -249,6 +223,7 @@ Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped ) pCnf->nVars = Number; // assign the clauses + vSopTemp = Vec_IntAlloc( 1 << 16 ); pLits = pCnf->pClauses[0]; pClas = pCnf->pClauses; Vec_PtrForEachEntry( vMapped, pObj, i ) @@ -267,48 +242,36 @@ Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped ) if ( pCut->nFanins < 5 ) { uTruth = 0xFFFF & *Cnf_CutTruth(pCut); - nCubes = p->pSopSizes[uTruth]; - for ( k = 0; k < nCubes; k++ ) - { - *pClas++ = pLits; - *pLits++ = 2 * OutVar + 1; - pLits += Cnf_SopWriteCube( p->pSops[uTruth][k], pVars, 0, pLits ); - } + Cnf_SopConvertToVector( p->pSops[uTruth], p->pSopSizes[uTruth], vSopTemp ); + vCover = vSopTemp; } else + vCover = pCut->vIsop[1]; + Vec_IntForEachEntry( vCover, Cube, k ) { - Vec_IntForEachEntry( pCut->vIsop[1], Cube, k ) - { - *pClas++ = pLits; - *pLits++ = 2 * OutVar + 1; - pLits += Cnf_IsopWriteCube( Cube, pCut->nFanins, pVars, 0, pLits ); - } + *pClas++ = pLits; + *pLits++ = 2 * OutVar; + pLits += Cnf_IsopWriteCube( Cube, pCut->nFanins, pVars, pLits ); } // negative polarity of the cut if ( pCut->nFanins < 5 ) { uTruth = 0xFFFF & ~*Cnf_CutTruth(pCut); - nCubes = p->pSopSizes[uTruth]; - for ( k = 0; k < nCubes; k++ ) - { - *pClas++ = pLits; - *pLits++ = 2 * OutVar; - pLits += Cnf_SopWriteCube( p->pSops[uTruth][k], pVars, 1, pLits ); - } + Cnf_SopConvertToVector( p->pSops[uTruth], p->pSopSizes[uTruth], vSopTemp ); + vCover = vSopTemp; } else + vCover = pCut->vIsop[0]; + Vec_IntForEachEntry( vCover, Cube, k ) { - Vec_IntForEachEntry( pCut->vIsop[0], Cube, k ) - { - *pClas++ = pLits; - *pLits++ = 2 * OutVar; - pLits += Cnf_IsopWriteCube( Cube, pCut->nFanins, pVars, 1, pLits ); - } + *pClas++ = pLits; + *pLits++ = 2 * OutVar + 1; + pLits += Cnf_IsopWriteCube( Cube, pCut->nFanins, pVars, pLits ); } -//printf( "%d ", pClas-pCnf->pClauses ); } - + Vec_IntFree( vSopTemp ); + // write the constant literal OutVar = pCnf->pVarNums[ Aig_ManConst1(p->pManAig)->Id ]; assert( OutVar <= Aig_ManObjIdMax(p->pManAig) ); |