diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2008-10-27 08:01:00 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2008-10-27 08:01:00 -0700 |
| commit | d80ee832f3883bf5b848db4ab31563c07fd08b59 (patch) | |
| tree | d19e8b6775ee149a091adef54657407c342b774d /src/aig/cnf | |
| parent | d2b735f794575ce0f10f01bba1255cf1dc3b8aaf (diff) | |
| download | abc-d80ee832f3883bf5b848db4ab31563c07fd08b59.tar.gz abc-d80ee832f3883bf5b848db4ab31563c07fd08b59.tar.bz2 abc-d80ee832f3883bf5b848db4ab31563c07fd08b59.zip | |
Version abc81027
Diffstat (limited to 'src/aig/cnf')
| -rw-r--r-- | src/aig/cnf/cnfMan.c | 7 | ||||
| -rw-r--r-- | src/aig/cnf/cnfWrite.c | 12 |
2 files changed, 14 insertions, 5 deletions
diff --git a/src/aig/cnf/cnfMan.c b/src/aig/cnf/cnfMan.c index 9059b9e5..7c24606c 100644 --- a/src/aig/cnf/cnfMan.c +++ b/src/aig/cnf/cnfMan.c @@ -122,6 +122,7 @@ Vec_Int_t * Cnf_DataCollectPiSatNums( Cnf_Dat_t * pCnf, Aig_Man_t * p ) Cnf_Dat_t * Cnf_DataAlloc( Aig_Man_t * pAig, int nVars, int nClauses, int nLiterals ) { Cnf_Dat_t * pCnf; + int i; pCnf = ALLOC( Cnf_Dat_t, 1 ); memset( pCnf, 0, sizeof(Cnf_Dat_t) ); pCnf->pMan = pAig; @@ -132,7 +133,9 @@ Cnf_Dat_t * Cnf_DataAlloc( Aig_Man_t * pAig, int nVars, int nClauses, int nLiter pCnf->pClauses[0] = ALLOC( int, nLiterals ); pCnf->pClauses[nClauses] = pCnf->pClauses[0] + nLiterals; pCnf->pVarNums = ALLOC( int, Aig_ManObjNumMax(pAig) ); - memset( pCnf->pVarNums, 0xff, sizeof(int) * Aig_ManObjNumMax(pAig) ); +// memset( pCnf->pVarNums, 0xff, sizeof(int) * Aig_ManObjNumMax(pAig) ); + for ( i = 0; i < Aig_ManObjNumMax(pAig); i++ ) + pCnf->pVarNums[i] = -1; return pCnf; } @@ -196,7 +199,7 @@ void Cnf_DataLift( Cnf_Dat_t * p, int nVarsPlus ) Aig_Obj_t * pObj; int v; Aig_ManForEachObj( p->pMan, pObj, v ) - if ( p->pVarNums[pObj->Id] ) + if ( p->pVarNums[pObj->Id] >= 0 ) p->pVarNums[pObj->Id] += nVarsPlus; for ( v = 0; v < p->nLiterals; v++ ) p->pClauses[0][v] += 2*nVarsPlus; diff --git a/src/aig/cnf/cnfWrite.c b/src/aig/cnf/cnfWrite.c index 3656aae3..860c7e3e 100644 --- a/src/aig/cnf/cnfWrite.c +++ b/src/aig/cnf/cnfWrite.c @@ -216,7 +216,9 @@ Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped, int nOutputs ) // create room for variable numbers pCnf->pVarNums = ALLOC( int, Aig_ManObjNumMax(p->pManAig) ); - memset( pCnf->pVarNums, 0xff, sizeof(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; // assign variables to the last (nOutputs) POs Number = 1; if ( nOutputs ) @@ -365,7 +367,9 @@ Cnf_Dat_t * Cnf_DeriveSimple( Aig_Man_t * p, int nOutputs ) // create room for variable numbers pCnf->pVarNums = ALLOC( int, Aig_ManObjNumMax(p) ); - memset( pCnf->pVarNums, 0xff, sizeof(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 ) @@ -485,7 +489,9 @@ Cnf_Dat_t * Cnf_DeriveSimpleForRetiming( Aig_Man_t * p ) // create room for variable numbers pCnf->pVarNums = ALLOC( int, Aig_ManObjNumMax(p) ); - memset( pCnf->pVarNums, 0xff, sizeof(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 ) |