diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2008-07-21 08:01:00 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2008-07-21 08:01:00 -0700 |
| commit | 2c96c8af36446d3b855e07d78975cfad50c2917c (patch) | |
| tree | 48ee5197e31ff733106efa4155d492029453b826 /src/aig/cnf | |
| parent | de978ced7b754706efaf18ae588e18eb05624faf (diff) | |
| download | abc-2c96c8af36446d3b855e07d78975cfad50c2917c.tar.gz abc-2c96c8af36446d3b855e07d78975cfad50c2917c.tar.bz2 abc-2c96c8af36446d3b855e07d78975cfad50c2917c.zip | |
Version abc80721
Diffstat (limited to 'src/aig/cnf')
| -rw-r--r-- | src/aig/cnf/cnf.h | 6 | ||||
| -rw-r--r-- | src/aig/cnf/cnfMan.c | 8 |
2 files changed, 11 insertions, 3 deletions
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++ ) { |