/**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_ManCoNum( p->pManAig ) + 3 * nOutputs; nClauses = 1 + Aig_ManCoNum( 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_ManCoNum( 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_ManCoNum(p->pManAig) ); Aig_ManForEachCo( 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_ManForEachCi( 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_ManCoNum(p->pManAig) ); Aig_ManForEachCo( 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_ManForEachCi( 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_ManForEachCo( p->pManAig, pObj, i ) { OutVar = pCnf->pVarNums[ Aig_ObjFanin0(pObj)->Id ]; if ( i < Aig_ManCoNum(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_ManCoNum( p->pManAig ); nClauses = 1 + 2 * Aig_ManCoNum( 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_ManForEachCi( 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_ManForEachCo( 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_ManCoNum( p ) + 3 * nOutputs; nClauses = 1 + 3 * Aig_ManNodeNum(p) + Aig_ManCoNum( 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_ManForEachCo( 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_ManForEachCi( 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_ManForEachCo( p, pObj, i ) { OutVar = pCnf->pVarNums[ Aig_ObjFanin0(pObj)->Id ]; if ( i < Aig_ManCoNum(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_ManCoNum(p); nClauses = 1 + 3 * Aig_ManNodeNum(p) + 3 * Aig_ManCoNum(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_ManForEachCo( 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_ManForEachCi( 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_ManForEachCo( 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