From 2c96c8af36446d3b855e07d78975cfad50c2917c Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Mon, 21 Jul 2008 08:01:00 -0700 Subject: Version abc80721 --- src/aig/cnf/cnf.h | 6 +++++- src/aig/cnf/cnfMan.c | 8 ++++++-- 2 files changed, 11 insertions(+), 3 deletions(-) (limited to 'src/aig/cnf') diff --git a/src/aig/cnf/cnf.h b/src/aig/cnf/cnf.h index f4f782df..c9c5bce3 100644 --- a/src/aig/cnf/cnf.h +++ b/src/aig/cnf/cnf.h @@ -108,6 +108,10 @@ static inline void Cnf_ObjSetBestCut( Aig_Obj_t * pObj, Cnf_Cut_t * pCut /// ITERATORS /// //////////////////////////////////////////////////////////////////////// +// iterator over the clauses +#define Cnf_CnfForClause( p, pBeg, pEnd, i ) \ + for ( i = 0; i < p->nClauses && (pBeg = p->pClauses[i]) && (pEnd = p->pClauses[i+1]); i++ ) + // iterator over leaves of the cut #define Cnf_CutForEachLeaf( p, pCut, pLeaf, i ) \ for ( i = 0; (i < (int)(pCut)->nFanins) && ((pLeaf) = Aig_ManObj(p, (pCut)->pFanins[i])); i++ ) @@ -142,7 +146,7 @@ extern void Cnf_DataWriteIntoFile( Cnf_Dat_t * p, char * pFileName, i extern void * Cnf_DataWriteIntoSolver( Cnf_Dat_t * p, int nFrames, int fInit ); extern int Cnf_DataWriteOrClause( void * pSat, Cnf_Dat_t * pCnf ); extern int Cnf_DataWriteAndClauses( void * p, Cnf_Dat_t * pCnf ); -extern void Cnf_DataTranformPolarity( Cnf_Dat_t * pCnf ); +extern void Cnf_DataTranformPolarity( Cnf_Dat_t * pCnf, int fTransformPos ); /*=== cnfMap.c ========================================================*/ extern void Cnf_DeriveMapping( Cnf_Man_t * p ); extern int Cnf_ManMapForCnf( Cnf_Man_t * p ); diff --git a/src/aig/cnf/cnfMan.c b/src/aig/cnf/cnfMan.c index 1e650a05..9059b9e5 100644 --- a/src/aig/cnf/cnfMan.c +++ b/src/aig/cnf/cnfMan.c @@ -470,7 +470,7 @@ int Cnf_DataWriteAndClauses( void * p, Cnf_Dat_t * pCnf ) SeeAlso [] ***********************************************************************/ -void Cnf_DataTranformPolarity( Cnf_Dat_t * pCnf ) +void Cnf_DataTranformPolarity( Cnf_Dat_t * pCnf, int fTransformPos ) { Aig_Obj_t * pObj; int * pVarToPol; @@ -478,8 +478,12 @@ void Cnf_DataTranformPolarity( Cnf_Dat_t * pCnf ) // create map from the variable number to its polarity pVarToPol = CALLOC( int, pCnf->nVars ); Aig_ManForEachObj( pCnf->pMan, pObj, i ) - if ( !Aig_ObjIsPo(pObj) && pCnf->pVarNums[pObj->Id] >= 0 ) + { + if ( !fTransformPos && Aig_ObjIsPo(pObj) ) + continue; + if ( pCnf->pVarNums[pObj->Id] >= 0 ) pVarToPol[ pCnf->pVarNums[pObj->Id] ] = pObj->fPhase; + } // transform literals for ( i = 0; i < pCnf->nLiterals; i++ ) { -- cgit v1.2.3