diff options
Diffstat (limited to 'src/aig/cnf/cnfWrite.c')
| -rw-r--r-- | src/aig/cnf/cnfWrite.c | 806 |
1 files changed, 0 insertions, 806 deletions
diff --git a/src/aig/cnf/cnfWrite.c b/src/aig/cnf/cnfWrite.c deleted file mode 100644 index 54c28967..00000000 --- a/src/aig/cnf/cnfWrite.c +++ /dev/null @@ -1,806 +0,0 @@ -/**CFile**************************************************************** - - FileName [cnfWrite.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [AIG-to-CNF conversion.] - - Synopsis [] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - April 28, 2007.] - - Revision [$Id: cnfWrite.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "cnf.h" - -ABC_NAMESPACE_IMPL_START - - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Derives CNF mapping.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Int_t * Cnf_ManWriteCnfMapping( Cnf_Man_t * p, Vec_Ptr_t * vMapped ) -{ - Vec_Int_t * vResult; - Aig_Obj_t * pObj; - Cnf_Cut_t * pCut; - int i, k, nOffset; - nOffset = Aig_ManObjNumMax(p->pManAig); - vResult = Vec_IntStart( nOffset ); - Vec_PtrForEachEntry( Aig_Obj_t *, vMapped, pObj, i ) - { - assert( Aig_ObjIsNode(pObj) ); - pCut = Cnf_ObjBestCut( pObj ); - assert( pCut->nFanins < 5 ); - Vec_IntWriteEntry( vResult, Aig_ObjId(pObj), nOffset ); - Vec_IntPush( vResult, *Cnf_CutTruth(pCut) ); - for ( k = 0; k < pCut->nFanins; k++ ) - Vec_IntPush( vResult, pCut->pFanins[k] ); - for ( ; k < 4; k++ ) - Vec_IntPush( vResult, -1 ); - nOffset += 5; - } - return vResult; -} - - - -/**Function************************************************************* - - Synopsis [Writes the cover into the array.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Cnf_SopConvertToVector( char * pSop, int nCubes, Vec_Int_t * vCover ) -{ - int Lits[4], Cube, iCube, i, b; - Vec_IntClear( vCover ); - for ( i = 0; i < nCubes; i++ ) - { - Cube = pSop[i]; - for ( b = 0; b < 4; b++ ) - { - if ( Cube % 3 == 0 ) - Lits[b] = 1; - else if ( Cube % 3 == 1 ) - Lits[b] = 2; - else - Lits[b] = 0; - Cube = Cube / 3; - } - iCube = 0; - for ( b = 0; b < 4; b++ ) - iCube = (iCube << 2) | Lits[b]; - Vec_IntPush( vCover, iCube ); - } -} - -/**Function************************************************************* - - Synopsis [Returns the number of literals in the SOP.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Cnf_SopCountLiterals( char * pSop, int nCubes ) -{ - int nLits = 0, Cube, i, b; - for ( i = 0; i < nCubes; i++ ) - { - Cube = pSop[i]; - for ( b = 0; b < 4; b++ ) - { - if ( Cube % 3 != 2 ) - nLits++; - Cube = Cube / 3; - } - } - return nLits; -} - -/**Function************************************************************* - - Synopsis [Returns the number of literals in the SOP.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Cnf_IsopCountLiterals( Vec_Int_t * vIsop, int nVars ) -{ - int nLits = 0, Cube, i, b; - Vec_IntForEachEntry( vIsop, Cube, i ) - { - for ( b = 0; b < nVars; b++ ) - { - if ( (Cube & 3) == 1 || (Cube & 3) == 2 ) - nLits++; - Cube >>= 2; - } - } - 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 * pLiterals ) -{ - int nLits = nVars, b; - for ( b = 0; b < nVars; b++ ) - { - 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; - } - return nLits; -} - -/**Function************************************************************* - - Synopsis [Derives CNF for the mapping.] - - Description [The last argument shows the number of last outputs - of the manager, which will not be converted into clauses but the - new variables for which will be introduced.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped, int nOutputs ) -{ - int fChangeVariableOrder = 0; // should be set to 0 to improve performance - Aig_Obj_t * pObj; - Cnf_Dat_t * pCnf; - Cnf_Cut_t * pCut; - Vec_Int_t * vCover, * vSopTemp; - int OutVar, PoVar, pVars[32], * pLits, ** pClas; - unsigned uTruth; - int i, k, nLiterals, nClauses, Cube, Number; - - // count the number of literals and clauses - nLiterals = 1 + Aig_ManPoNum( p->pManAig ) + 3 * nOutputs; - nClauses = 1 + Aig_ManPoNum( p->pManAig ) + nOutputs; - Vec_PtrForEachEntry( Aig_Obj_t *, vMapped, pObj, i ) - { - assert( Aig_ObjIsNode(pObj) ); - pCut = Cnf_ObjBestCut( pObj ); - - // positive polarity of the cut - if ( pCut->nFanins < 5 ) - { - uTruth = 0xFFFF & *Cnf_CutTruth(pCut); - nLiterals += Cnf_SopCountLiterals( p->pSops[uTruth], p->pSopSizes[uTruth] ) + p->pSopSizes[uTruth]; - assert( p->pSopSizes[uTruth] >= 0 ); - nClauses += p->pSopSizes[uTruth]; - } - else - { - nLiterals += Cnf_IsopCountLiterals( pCut->vIsop[1], pCut->nFanins ) + Vec_IntSize(pCut->vIsop[1]); - nClauses += Vec_IntSize(pCut->vIsop[1]); - } - // negative polarity of the cut - if ( pCut->nFanins < 5 ) - { - uTruth = 0xFFFF & ~*Cnf_CutTruth(pCut); - nLiterals += Cnf_SopCountLiterals( p->pSops[uTruth], p->pSopSizes[uTruth] ) + p->pSopSizes[uTruth]; - assert( p->pSopSizes[uTruth] >= 0 ); - nClauses += p->pSopSizes[uTruth]; - } - else - { - nLiterals += Cnf_IsopCountLiterals( pCut->vIsop[0], pCut->nFanins ) + Vec_IntSize(pCut->vIsop[0]); - nClauses += Vec_IntSize(pCut->vIsop[0]); - } -//printf( "%d ", nClauses-(1 + Aig_ManPoNum( p->pManAig )) ); - } -//printf( "\n" ); - - // allocate CNF - pCnf = ABC_CALLOC( Cnf_Dat_t, 1 ); - pCnf->pMan = p->pManAig; - pCnf->nLiterals = nLiterals; - pCnf->nClauses = nClauses; - pCnf->pClauses = ABC_ALLOC( int *, nClauses + 1 ); - pCnf->pClauses[0] = ABC_ALLOC( int, nLiterals ); - pCnf->pClauses[nClauses] = pCnf->pClauses[0] + nLiterals; - // create room for variable numbers - pCnf->pVarNums = ABC_ALLOC( int, Aig_ManObjNumMax(p->pManAig) ); -// memset( pCnf->pVarNums, 0xff, sizeof(int) * Aig_ManObjNumMax(p->pManAig) ); - for ( i = 0; i < Aig_ManObjNumMax(p->pManAig); i++ ) - pCnf->pVarNums[i] = -1; - - if ( !fChangeVariableOrder ) - { - // assign variables to the last (nOutputs) POs - Number = 1; - if ( nOutputs ) - { - if ( Aig_ManRegNum(p->pManAig) == 0 ) - { - assert( nOutputs == Aig_ManPoNum(p->pManAig) ); - Aig_ManForEachPo( p->pManAig, pObj, i ) - pCnf->pVarNums[pObj->Id] = Number++; - } - else - { - assert( nOutputs == Aig_ManRegNum(p->pManAig) ); - Aig_ManForEachLiSeq( p->pManAig, pObj, i ) - pCnf->pVarNums[pObj->Id] = Number++; - } - } - // assign variables to the internal nodes - Vec_PtrForEachEntry( Aig_Obj_t *, vMapped, pObj, i ) - pCnf->pVarNums[pObj->Id] = Number++; - // assign variables to the PIs and constant node - Aig_ManForEachPi( p->pManAig, pObj, i ) - pCnf->pVarNums[pObj->Id] = Number++; - pCnf->pVarNums[Aig_ManConst1(p->pManAig)->Id] = Number++; - pCnf->nVars = Number; - } - else - { - // assign variables to the last (nOutputs) POs - Number = Aig_ManObjNumMax(p->pManAig) + 1; - pCnf->nVars = Number + 1; - if ( nOutputs ) - { - if ( Aig_ManRegNum(p->pManAig) == 0 ) - { - assert( nOutputs == Aig_ManPoNum(p->pManAig) ); - Aig_ManForEachPo( p->pManAig, pObj, i ) - pCnf->pVarNums[pObj->Id] = Number--; - } - else - { - assert( nOutputs == Aig_ManRegNum(p->pManAig) ); - Aig_ManForEachLiSeq( p->pManAig, pObj, i ) - pCnf->pVarNums[pObj->Id] = Number--; - } - } - // assign variables to the internal nodes - Vec_PtrForEachEntry( Aig_Obj_t *, vMapped, pObj, i ) - pCnf->pVarNums[pObj->Id] = Number--; - // assign variables to the PIs and constant node - Aig_ManForEachPi( p->pManAig, pObj, i ) - pCnf->pVarNums[pObj->Id] = Number--; - pCnf->pVarNums[Aig_ManConst1(p->pManAig)->Id] = Number--; - assert( Number >= 0 ); - } - - // assign the clauses - vSopTemp = Vec_IntAlloc( 1 << 16 ); - pLits = pCnf->pClauses[0]; - pClas = pCnf->pClauses; - Vec_PtrForEachEntry( Aig_Obj_t *, vMapped, pObj, i ) - { - pCut = Cnf_ObjBestCut( pObj ); - - // save variables of this cut - OutVar = pCnf->pVarNums[ pObj->Id ]; - for ( k = 0; k < (int)pCut->nFanins; k++ ) - { - pVars[k] = pCnf->pVarNums[ pCut->pFanins[k] ]; - assert( pVars[k] <= Aig_ManObjNumMax(p->pManAig) ); - } - - // positive polarity of the cut - if ( pCut->nFanins < 5 ) - { - uTruth = 0xFFFF & *Cnf_CutTruth(pCut); - Cnf_SopConvertToVector( p->pSops[uTruth], p->pSopSizes[uTruth], vSopTemp ); - vCover = vSopTemp; - } - else - vCover = pCut->vIsop[1]; - Vec_IntForEachEntry( vCover, Cube, k ) - { - *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); - Cnf_SopConvertToVector( p->pSops[uTruth], p->pSopSizes[uTruth], vSopTemp ); - vCover = vSopTemp; - } - else - vCover = pCut->vIsop[0]; - Vec_IntForEachEntry( vCover, Cube, k ) - { - *pClas++ = pLits; - *pLits++ = 2 * OutVar + 1; - pLits += Cnf_IsopWriteCube( Cube, pCut->nFanins, pVars, pLits ); - } - } - Vec_IntFree( vSopTemp ); - - // write the constant literal - OutVar = pCnf->pVarNums[ Aig_ManConst1(p->pManAig)->Id ]; - assert( OutVar <= Aig_ManObjNumMax(p->pManAig) ); - *pClas++ = pLits; - *pLits++ = 2 * OutVar; - - // write the output literals - Aig_ManForEachPo( p->pManAig, pObj, i ) - { - OutVar = pCnf->pVarNums[ Aig_ObjFanin0(pObj)->Id ]; - if ( i < Aig_ManPoNum(p->pManAig) - nOutputs ) - { - *pClas++ = pLits; - *pLits++ = 2 * OutVar + Aig_ObjFaninC0(pObj); - } - else - { - PoVar = pCnf->pVarNums[ pObj->Id ]; - // first clause - *pClas++ = pLits; - *pLits++ = 2 * PoVar; - *pLits++ = 2 * OutVar + !Aig_ObjFaninC0(pObj); - // second clause - *pClas++ = pLits; - *pLits++ = 2 * PoVar + 1; - *pLits++ = 2 * OutVar + Aig_ObjFaninC0(pObj); - } - } - - // verify that the correct number of literals and clauses was written - assert( pLits - pCnf->pClauses[0] == nLiterals ); - assert( pClas - pCnf->pClauses == nClauses ); -//Cnf_DataPrint( pCnf, 1 ); - return pCnf; -} - - -/**Function************************************************************* - - Synopsis [Derives CNF for the mapping.] - - Description [Derives CNF with obj IDs as SAT vars and mapping of - objects into clauses (pObj2Clause and pObj2Count).] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Cnf_Dat_t * Cnf_ManWriteCnfOther( 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, PoVar, pVars[32], * pLits, ** pClas; - unsigned uTruth; - int i, k, nLiterals, nClauses, Cube; - - // count the number of literals and clauses - nLiterals = 1 + 4 * Aig_ManPoNum( p->pManAig ); - nClauses = 1 + 2 * Aig_ManPoNum( p->pManAig ); - Vec_PtrForEachEntry( Aig_Obj_t *, vMapped, pObj, i ) - { - assert( Aig_ObjIsNode(pObj) ); - pCut = Cnf_ObjBestCut( pObj ); - // positive polarity of the cut - if ( pCut->nFanins < 5 ) - { - uTruth = 0xFFFF & *Cnf_CutTruth(pCut); - nLiterals += Cnf_SopCountLiterals( p->pSops[uTruth], p->pSopSizes[uTruth] ) + p->pSopSizes[uTruth]; - assert( p->pSopSizes[uTruth] >= 0 ); - nClauses += p->pSopSizes[uTruth]; - } - else - { - nLiterals += Cnf_IsopCountLiterals( pCut->vIsop[1], pCut->nFanins ) + Vec_IntSize(pCut->vIsop[1]); - nClauses += Vec_IntSize(pCut->vIsop[1]); - } - // negative polarity of the cut - if ( pCut->nFanins < 5 ) - { - uTruth = 0xFFFF & ~*Cnf_CutTruth(pCut); - nLiterals += Cnf_SopCountLiterals( p->pSops[uTruth], p->pSopSizes[uTruth] ) + p->pSopSizes[uTruth]; - assert( p->pSopSizes[uTruth] >= 0 ); - nClauses += p->pSopSizes[uTruth]; - } - else - { - nLiterals += Cnf_IsopCountLiterals( pCut->vIsop[0], pCut->nFanins ) + Vec_IntSize(pCut->vIsop[0]); - nClauses += Vec_IntSize(pCut->vIsop[0]); - } - } - - // allocate CNF - pCnf = ABC_CALLOC( Cnf_Dat_t, 1 ); - pCnf->pMan = p->pManAig; - pCnf->nLiterals = nLiterals; - pCnf->nClauses = nClauses; - pCnf->pClauses = ABC_ALLOC( int *, nClauses + 1 ); - pCnf->pClauses[0] = ABC_ALLOC( int, nLiterals ); - pCnf->pClauses[nClauses] = pCnf->pClauses[0] + nLiterals; - // create room for variable numbers - pCnf->pObj2Clause = ABC_ALLOC( int, Aig_ManObjNumMax(p->pManAig) ); - pCnf->pObj2Count = ABC_ALLOC( int, Aig_ManObjNumMax(p->pManAig) ); - for ( i = 0; i < Aig_ManObjNumMax(p->pManAig); i++ ) - pCnf->pObj2Clause[i] = pCnf->pObj2Count[i] = -1; - pCnf->nVars = Aig_ManObjNumMax(p->pManAig); - - // clear the PI counters - Aig_ManForEachPi( p->pManAig, pObj, i ) - pCnf->pObj2Count[pObj->Id] = 0; - - // assign the clauses - vSopTemp = Vec_IntAlloc( 1 << 16 ); - pLits = pCnf->pClauses[0]; - pClas = pCnf->pClauses; - Vec_PtrForEachEntry( Aig_Obj_t *, vMapped, pObj, i ) - { - // remember the starting clause - pCnf->pObj2Clause[pObj->Id] = pClas - pCnf->pClauses; - pCnf->pObj2Count[pObj->Id] = 0; - - // get the best cut - pCut = Cnf_ObjBestCut( pObj ); - // save variables of this cut - OutVar = pObj->Id; - for ( k = 0; k < (int)pCut->nFanins; k++ ) - { - pVars[k] = pCut->pFanins[k]; - assert( pVars[k] <= Aig_ManObjNumMax(p->pManAig) ); - } - - // positive polarity of the cut - if ( pCut->nFanins < 5 ) - { - uTruth = 0xFFFF & *Cnf_CutTruth(pCut); - Cnf_SopConvertToVector( p->pSops[uTruth], p->pSopSizes[uTruth], vSopTemp ); - vCover = vSopTemp; - } - else - vCover = pCut->vIsop[1]; - Vec_IntForEachEntry( vCover, Cube, k ) - { - *pClas++ = pLits; - *pLits++ = 2 * OutVar; - pLits += Cnf_IsopWriteCube( Cube, pCut->nFanins, pVars, pLits ); - } - pCnf->pObj2Count[pObj->Id] += Vec_IntSize(vCover); - - // negative polarity of the cut - if ( pCut->nFanins < 5 ) - { - uTruth = 0xFFFF & ~*Cnf_CutTruth(pCut); - Cnf_SopConvertToVector( p->pSops[uTruth], p->pSopSizes[uTruth], vSopTemp ); - vCover = vSopTemp; - } - else - vCover = pCut->vIsop[0]; - Vec_IntForEachEntry( vCover, Cube, k ) - { - *pClas++ = pLits; - *pLits++ = 2 * OutVar + 1; - pLits += Cnf_IsopWriteCube( Cube, pCut->nFanins, pVars, pLits ); - } - pCnf->pObj2Count[pObj->Id] += Vec_IntSize(vCover); - } - Vec_IntFree( vSopTemp ); - - // write the output literals - Aig_ManForEachPo( p->pManAig, pObj, i ) - { - // remember the starting clause - pCnf->pObj2Clause[pObj->Id] = pClas - pCnf->pClauses; - pCnf->pObj2Count[pObj->Id] = 2; - // get variables - OutVar = Aig_ObjFanin0(pObj)->Id; - PoVar = pObj->Id; - // first clause - *pClas++ = pLits; - *pLits++ = 2 * PoVar; - *pLits++ = 2 * OutVar + !Aig_ObjFaninC0(pObj); - // second clause - *pClas++ = pLits; - *pLits++ = 2 * PoVar + 1; - *pLits++ = 2 * OutVar + Aig_ObjFaninC0(pObj); - } - - // remember the starting clause - pCnf->pObj2Clause[Aig_ManConst1(p->pManAig)->Id] = pClas - pCnf->pClauses; - pCnf->pObj2Count[Aig_ManConst1(p->pManAig)->Id] = 1; - // write the constant literal - OutVar = Aig_ManConst1(p->pManAig)->Id; - *pClas++ = pLits; - *pLits++ = 2 * OutVar; - - // verify that the correct number of literals and clauses was written - assert( pLits - pCnf->pClauses[0] == nLiterals ); - assert( pClas - pCnf->pClauses == nClauses ); -//Cnf_DataPrint( pCnf, 1 ); - return pCnf; -} - - -/**Function************************************************************* - - Synopsis [Derives a simple CNF for the AIG.] - - Description [The last argument lists the number of last outputs - of the manager, which will not be converted into clauses. - New variables will be introduced for these outputs.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Cnf_Dat_t * Cnf_DeriveSimple( Aig_Man_t * p, int nOutputs ) -{ - Aig_Obj_t * pObj; - Cnf_Dat_t * pCnf; - int OutVar, PoVar, pVars[32], * pLits, ** pClas; - int i, nLiterals, nClauses, Number; - - // count the number of literals and clauses - nLiterals = 1 + 7 * Aig_ManNodeNum(p) + Aig_ManPoNum( p ) + 3 * nOutputs; - nClauses = 1 + 3 * Aig_ManNodeNum(p) + Aig_ManPoNum( p ) + nOutputs; - - // allocate CNF - pCnf = ABC_ALLOC( Cnf_Dat_t, 1 ); - memset( pCnf, 0, sizeof(Cnf_Dat_t) ); - pCnf->pMan = p; - pCnf->nLiterals = nLiterals; - pCnf->nClauses = nClauses; - pCnf->pClauses = ABC_ALLOC( int *, nClauses + 1 ); - pCnf->pClauses[0] = ABC_ALLOC( int, nLiterals ); - pCnf->pClauses[nClauses] = pCnf->pClauses[0] + nLiterals; - - // create room for variable numbers - pCnf->pVarNums = ABC_ALLOC( int, Aig_ManObjNumMax(p) ); -// memset( pCnf->pVarNums, 0xff, sizeof(int) * Aig_ManObjNumMax(p) ); - for ( i = 0; i < Aig_ManObjNumMax(p); i++ ) - pCnf->pVarNums[i] = -1; - // assign variables to the last (nOutputs) POs - Number = 1; - if ( nOutputs ) - { -// assert( nOutputs == Aig_ManRegNum(p) ); -// Aig_ManForEachLiSeq( p, pObj, i ) -// pCnf->pVarNums[pObj->Id] = Number++; - Aig_ManForEachPo( p, pObj, i ) - pCnf->pVarNums[pObj->Id] = Number++; - } - // assign variables to the internal nodes - Aig_ManForEachNode( p, pObj, i ) - pCnf->pVarNums[pObj->Id] = Number++; - // assign variables to the PIs and constant node - Aig_ManForEachPi( p, pObj, i ) - pCnf->pVarNums[pObj->Id] = Number++; - pCnf->pVarNums[Aig_ManConst1(p)->Id] = Number++; - pCnf->nVars = Number; -/* - // print CNF numbers - printf( "SAT numbers of each node:\n" ); - Aig_ManForEachObj( p, pObj, i ) - printf( "%d=%d ", pObj->Id, pCnf->pVarNums[pObj->Id] ); - printf( "\n" ); -*/ - // assign the clauses - pLits = pCnf->pClauses[0]; - pClas = pCnf->pClauses; - Aig_ManForEachNode( p, pObj, i ) - { - OutVar = pCnf->pVarNums[ pObj->Id ]; - pVars[0] = pCnf->pVarNums[ Aig_ObjFanin0(pObj)->Id ]; - pVars[1] = pCnf->pVarNums[ Aig_ObjFanin1(pObj)->Id ]; - - // positive phase - *pClas++ = pLits; - *pLits++ = 2 * OutVar; - *pLits++ = 2 * pVars[0] + !Aig_ObjFaninC0(pObj); - *pLits++ = 2 * pVars[1] + !Aig_ObjFaninC1(pObj); - // negative phase - *pClas++ = pLits; - *pLits++ = 2 * OutVar + 1; - *pLits++ = 2 * pVars[0] + Aig_ObjFaninC0(pObj); - *pClas++ = pLits; - *pLits++ = 2 * OutVar + 1; - *pLits++ = 2 * pVars[1] + Aig_ObjFaninC1(pObj); - } - - // write the constant literal - OutVar = pCnf->pVarNums[ Aig_ManConst1(p)->Id ]; - assert( OutVar <= Aig_ManObjNumMax(p) ); - *pClas++ = pLits; - *pLits++ = 2 * OutVar; - - // write the output literals - Aig_ManForEachPo( p, pObj, i ) - { - OutVar = pCnf->pVarNums[ Aig_ObjFanin0(pObj)->Id ]; - if ( i < Aig_ManPoNum(p) - nOutputs ) - { - *pClas++ = pLits; - *pLits++ = 2 * OutVar + Aig_ObjFaninC0(pObj); - } - else - { - PoVar = pCnf->pVarNums[ pObj->Id ]; - // first clause - *pClas++ = pLits; - *pLits++ = 2 * PoVar; - *pLits++ = 2 * OutVar + !Aig_ObjFaninC0(pObj); - // second clause - *pClas++ = pLits; - *pLits++ = 2 * PoVar + 1; - *pLits++ = 2 * OutVar + Aig_ObjFaninC0(pObj); - } - } - - // verify that the correct number of literals and clauses was written - assert( pLits - pCnf->pClauses[0] == nLiterals ); - assert( pClas - pCnf->pClauses == nClauses ); - return pCnf; -} - -/**Function************************************************************* - - Synopsis [Derives a simple CNF for backward retiming computation.] - - Description [The last argument shows the number of last outputs - of the manager, which will not be converted into clauses. - New variables will be introduced for these outputs.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Cnf_Dat_t * Cnf_DeriveSimpleForRetiming( Aig_Man_t * p ) -{ - Aig_Obj_t * pObj; - Cnf_Dat_t * pCnf; - int OutVar, PoVar, pVars[32], * pLits, ** pClas; - int i, nLiterals, nClauses, Number; - - // count the number of literals and clauses - nLiterals = 1 + 7 * Aig_ManNodeNum(p) + 5 * Aig_ManPoNum(p); - nClauses = 1 + 3 * Aig_ManNodeNum(p) + 3 * Aig_ManPoNum(p); - - // allocate CNF - pCnf = ABC_ALLOC( Cnf_Dat_t, 1 ); - memset( pCnf, 0, sizeof(Cnf_Dat_t) ); - pCnf->pMan = p; - pCnf->nLiterals = nLiterals; - pCnf->nClauses = nClauses; - pCnf->pClauses = ABC_ALLOC( int *, nClauses + 1 ); - pCnf->pClauses[0] = ABC_ALLOC( int, nLiterals ); - pCnf->pClauses[nClauses] = pCnf->pClauses[0] + nLiterals; - - // create room for variable numbers - pCnf->pVarNums = ABC_ALLOC( int, Aig_ManObjNumMax(p) ); -// memset( pCnf->pVarNums, 0xff, sizeof(int) * Aig_ManObjNumMax(p) ); - for ( i = 0; i < Aig_ManObjNumMax(p); i++ ) - pCnf->pVarNums[i] = -1; - // assign variables to the last (nOutputs) POs - Number = 1; - Aig_ManForEachPo( p, pObj, i ) - pCnf->pVarNums[pObj->Id] = Number++; - // assign variables to the internal nodes - Aig_ManForEachNode( p, pObj, i ) - pCnf->pVarNums[pObj->Id] = Number++; - // assign variables to the PIs and constant node - Aig_ManForEachPi( p, pObj, i ) - pCnf->pVarNums[pObj->Id] = Number++; - pCnf->pVarNums[Aig_ManConst1(p)->Id] = Number++; - pCnf->nVars = Number; - // assign the clauses - pLits = pCnf->pClauses[0]; - pClas = pCnf->pClauses; - Aig_ManForEachNode( p, pObj, i ) - { - OutVar = pCnf->pVarNums[ pObj->Id ]; - pVars[0] = pCnf->pVarNums[ Aig_ObjFanin0(pObj)->Id ]; - pVars[1] = pCnf->pVarNums[ Aig_ObjFanin1(pObj)->Id ]; - - // positive phase - *pClas++ = pLits; - *pLits++ = 2 * OutVar; - *pLits++ = 2 * pVars[0] + !Aig_ObjFaninC0(pObj); - *pLits++ = 2 * pVars[1] + !Aig_ObjFaninC1(pObj); - // negative phase - *pClas++ = pLits; - *pLits++ = 2 * OutVar + 1; - *pLits++ = 2 * pVars[0] + Aig_ObjFaninC0(pObj); - *pClas++ = pLits; - *pLits++ = 2 * OutVar + 1; - *pLits++ = 2 * pVars[1] + Aig_ObjFaninC1(pObj); - } - - // write the constant literal - OutVar = pCnf->pVarNums[ Aig_ManConst1(p)->Id ]; - assert( OutVar <= Aig_ManObjNumMax(p) ); - *pClas++ = pLits; - *pLits++ = 2 * OutVar; - - // write the output literals - Aig_ManForEachPo( p, pObj, i ) - { - OutVar = pCnf->pVarNums[ Aig_ObjFanin0(pObj)->Id ]; - PoVar = pCnf->pVarNums[ pObj->Id ]; - // first clause - *pClas++ = pLits; - *pLits++ = 2 * PoVar; - *pLits++ = 2 * OutVar + !Aig_ObjFaninC0(pObj); - // second clause - *pClas++ = pLits; - *pLits++ = 2 * PoVar + 1; - *pLits++ = 2 * OutVar + Aig_ObjFaninC0(pObj); - // final clause (init-state is always 0 -> set the output to 0) - *pClas++ = pLits; - *pLits++ = 2 * PoVar + 1; - } - - // verify that the correct number of literals and clauses was written - assert( pLits - pCnf->pClauses[0] == nLiterals ); - assert( pClas - pCnf->pClauses == nClauses ); - return pCnf; -} - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - -ABC_NAMESPACE_IMPL_END - |