summaryrefslogtreecommitdiffstats
path: root/src/aig/cnf
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2008-10-27 08:01:00 -0700
committerAlan Mishchenko <alanmi@berkeley.edu>2008-10-27 08:01:00 -0700
commitd80ee832f3883bf5b848db4ab31563c07fd08b59 (patch)
treed19e8b6775ee149a091adef54657407c342b774d /src/aig/cnf
parentd2b735f794575ce0f10f01bba1255cf1dc3b8aaf (diff)
downloadabc-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.c7
-rw-r--r--src/aig/cnf/cnfWrite.c12
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 )