From fefd8b901d89ad0d977db8896c12123cc747e3d7 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Mon, 30 Jul 2007 08:01:00 -0700 Subject: Version abc70730 --- src/aig/cnf/cnfWrite.c | 129 ++++++++++++++++++++++++++++++++++++++++++++++--- 1 file changed, 123 insertions(+), 6 deletions(-) (limited to 'src/aig/cnf/cnfWrite.c') diff --git a/src/aig/cnf/cnfWrite.c b/src/aig/cnf/cnfWrite.c index fa5be801..6faa08d2 100644 --- a/src/aig/cnf/cnfWrite.c +++ b/src/aig/cnf/cnfWrite.c @@ -217,11 +217,12 @@ Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped, int nOutputs ) pCnf->pVarNums = ALLOC( int, 1+Aig_ManObjIdMax(p->pManAig) ); memset( pCnf->pVarNums, 0xff, sizeof(int) * (1+Aig_ManObjIdMax(p->pManAig)) ); // assign variables to the last (nOutputs) POs - Number = 0; - for ( i = 0; i < nOutputs; i++ ) + Number = 1; + if ( nOutputs ) { - pObj = Aig_ManPo( p->pManAig, Aig_ManPoNum(p->pManAig) - nOutputs + i ); - pCnf->pVarNums[pObj->Id] = Number++; + 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( vMapped, pObj, i ) @@ -291,16 +292,15 @@ Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped, int nOutputs ) // write the output literals Aig_ManForEachPo( p->pManAig, pObj, i ) { + OutVar = pCnf->pVarNums[ Aig_ObjFanin0(pObj)->Id ]; if ( i < Aig_ManPoNum(p->pManAig) - nOutputs ) { - OutVar = pCnf->pVarNums[ Aig_ObjFanin0(pObj)->Id ]; *pClas++ = pLits; *pLits++ = 2 * OutVar + Aig_ObjFaninC0(pObj); } else { PoVar = pCnf->pVarNums[ pObj->Id ]; - OutVar = pCnf->pVarNums[ Aig_ObjFanin0(pObj)->Id ]; // first clause *pClas++ = pLits; *pLits++ = 2 * PoVar; @@ -319,6 +319,123 @@ Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped, int nOutputs ) } +/**Function************************************************************* + + Synopsis [Derives a simple CNF for the AIG.] + + 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_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 = ALLOC( Cnf_Dat_t, 1 ); + memset( pCnf, 0, sizeof(Cnf_Dat_t) ); + pCnf->nLiterals = nLiterals; + pCnf->nClauses = nClauses; + pCnf->pClauses = ALLOC( int *, nClauses + 1 ); + pCnf->pClauses[0] = ALLOC( int, nLiterals ); + pCnf->pClauses[nClauses] = pCnf->pClauses[0] + nLiterals; + + // create room for variable numbers + pCnf->pVarNums = ALLOC( int, 1+Aig_ManObjIdMax(p) ); + memset( pCnf->pVarNums, 0xff, sizeof(int) * (1+Aig_ManObjIdMax(p)) ); + // 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++; + } + // 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_ManObjIdMax(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; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// -- cgit v1.2.3