From 9be1b076934b0410689c857cd71ef7d21a714b5f Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Thu, 6 Sep 2007 08:01:00 -0700 Subject: Version abc70906 --- src/aig/cnf/cnfWrite.c | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) (limited to 'src/aig/cnf/cnfWrite.c') diff --git a/src/aig/cnf/cnfWrite.c b/src/aig/cnf/cnfWrite.c index 6faa08d2..45a3efad 100644 --- a/src/aig/cnf/cnfWrite.c +++ b/src/aig/cnf/cnfWrite.c @@ -214,8 +214,8 @@ Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped, int nOutputs ) pCnf->pClauses[nClauses] = pCnf->pClauses[0] + nLiterals; // create room for variable numbers - pCnf->pVarNums = ALLOC( int, 1+Aig_ManObjIdMax(p->pManAig) ); - memset( pCnf->pVarNums, 0xff, sizeof(int) * (1+Aig_ManObjIdMax(p->pManAig)) ); + pCnf->pVarNums = ALLOC( int, Aig_ManObjNumMax(p->pManAig) ); + memset( pCnf->pVarNums, 0xff, sizeof(int) * Aig_ManObjNumMax(p->pManAig) ); // assign variables to the last (nOutputs) POs Number = 1; if ( nOutputs ) @@ -246,7 +246,7 @@ Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped, int nOutputs ) for ( k = 0; k < (int)pCut->nFanins; k++ ) { pVars[k] = pCnf->pVarNums[ pCut->pFanins[k] ]; - assert( pVars[k] <= Aig_ManObjIdMax(p->pManAig) ); + assert( pVars[k] <= Aig_ManObjNumMax(p->pManAig) ); } // positive polarity of the cut @@ -285,7 +285,7 @@ Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped, int nOutputs ) // write the constant literal OutVar = pCnf->pVarNums[ Aig_ManConst1(p->pManAig)->Id ]; - assert( OutVar <= Aig_ManObjIdMax(p->pManAig) ); + assert( OutVar <= Aig_ManObjNumMax(p->pManAig) ); *pClas++ = pLits; *pLits++ = 2 * OutVar; @@ -353,8 +353,8 @@ Cnf_Dat_t * Cnf_DeriveSimple( Aig_Man_t * p, int nOutputs ) 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)) ); + pCnf->pVarNums = ALLOC( int, Aig_ManObjNumMax(p) ); + memset( pCnf->pVarNums, 0xff, sizeof(int) * Aig_ManObjNumMax(p) ); // assign variables to the last (nOutputs) POs Number = 1; if ( nOutputs ) @@ -403,7 +403,7 @@ Cnf_Dat_t * Cnf_DeriveSimple( Aig_Man_t * p, int nOutputs ) // write the constant literal OutVar = pCnf->pVarNums[ Aig_ManConst1(p)->Id ]; - assert( OutVar <= Aig_ManObjIdMax(p) ); + assert( OutVar <= Aig_ManObjNumMax(p) ); *pClas++ = pLits; *pLits++ = 2 * OutVar; -- cgit v1.2.3