diff options
Diffstat (limited to 'src/sat')
| -rw-r--r-- | src/sat/cnf/cnf.h | 2 | ||||
| -rw-r--r-- | src/sat/cnf/cnfMan.c | 1 | ||||
| -rw-r--r-- | src/sat/cnf/cnfUtil.c | 60 |
3 files changed, 63 insertions, 0 deletions
diff --git a/src/sat/cnf/cnf.h b/src/sat/cnf/cnf.h index e5079a46..ba41ef4e 100644 --- a/src/sat/cnf/cnf.h +++ b/src/sat/cnf/cnf.h @@ -63,6 +63,7 @@ struct Cnf_Dat_t_ int * pVarNums; // the number of CNF variable for each node ID (-1 if unused) int * pObj2Clause; // the mapping of objects into clauses int * pObj2Count; // the mapping of objects into clause number + unsigned char * pClaPols; // polarity of input literals in each clause Vec_Int_t * vMapping; // mapping of internal nodes }; @@ -176,6 +177,7 @@ extern Vec_Ptr_t * Aig_ManScanMapping( Cnf_Man_t * p, int fCollect ); extern Vec_Ptr_t * Cnf_ManScanMapping( Cnf_Man_t * p, int fCollect, int fPreorder ); extern Vec_Int_t * Cnf_DataCollectCiSatNums( Cnf_Dat_t * pCnf, Aig_Man_t * p ); extern Vec_Int_t * Cnf_DataCollectCoSatNums( Cnf_Dat_t * pCnf, Aig_Man_t * p ); +extern unsigned char * Cnf_DataDeriveLitPolarities( Cnf_Dat_t * p ); /*=== cnfWrite.c ========================================================*/ extern Vec_Int_t * Cnf_ManWriteCnfMapping( Cnf_Man_t * p, Vec_Ptr_t * vMapped ); extern void Cnf_SopConvertToVector( char * pSop, int nCubes, Vec_Int_t * vCover ); diff --git a/src/sat/cnf/cnfMan.c b/src/sat/cnf/cnfMan.c index 2aa5df6f..8a155f78 100644 --- a/src/sat/cnf/cnfMan.c +++ b/src/sat/cnf/cnfMan.c @@ -182,6 +182,7 @@ void Cnf_DataFree( Cnf_Dat_t * p ) if ( p == NULL ) return; Vec_IntFreeP( &p->vMapping ); + ABC_FREE( p->pClaPols ); ABC_FREE( p->pObj2Clause ); ABC_FREE( p->pObj2Count ); ABC_FREE( p->pClauses[0] ); diff --git a/src/sat/cnf/cnfUtil.c b/src/sat/cnf/cnfUtil.c index e3828863..98b494b3 100644 --- a/src/sat/cnf/cnfUtil.c +++ b/src/sat/cnf/cnfUtil.c @@ -229,6 +229,66 @@ Vec_Int_t * Cnf_DataCollectCoSatNums( Cnf_Dat_t * pCnf, Aig_Man_t * p ) return vCoIds; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +unsigned char * Cnf_DataDeriveLitPolarities( Cnf_Dat_t * p ) +{ + int i, c, iClaBeg, iClaEnd, * pLit; + unsigned * pPols0 = ABC_CALLOC( unsigned, Aig_ManObjNumMax(p->pMan) ); + unsigned * pPols1 = ABC_CALLOC( unsigned, Aig_ManObjNumMax(p->pMan) ); + unsigned char * pPres = ABC_CALLOC( unsigned char, p->nClauses ); + for ( i = 0; i < Aig_ManObjNumMax(p->pMan); i++ ) + { + if ( p->pObj2Count[i] == 0 ) + continue; + iClaBeg = p->pObj2Clause[i]; + iClaEnd = p->pObj2Clause[i] + p->pObj2Count[i]; + // go through the negative polarity clauses + for ( c = iClaBeg; c < iClaEnd; c++ ) + for ( pLit = p->pClauses[c]+1; pLit < p->pClauses[c+1]; pLit++ ) + if ( Abc_LitIsCompl(p->pClauses[c][0]) ) + pPols0[Abc_Lit2Var(*pLit)] |= (unsigned)(2 - Abc_LitIsCompl(*pLit)); // taking the opposite (!) -- not the case + else + pPols1[Abc_Lit2Var(*pLit)] |= (unsigned)(2 - Abc_LitIsCompl(*pLit)); // taking the opposite (!) -- not the case + // record these clauses + for ( c = iClaBeg; c < iClaEnd; c++ ) + for ( pLit = p->pClauses[c]+1; pLit < p->pClauses[c+1]; pLit++ ) + if ( Abc_LitIsCompl(p->pClauses[c][0]) ) + pPres[c] = (unsigned char)( (unsigned)pPres[c] | (pPols0[Abc_Lit2Var(*pLit)] << (2*(pLit-p->pClauses[c]-1))) ); + else + pPres[c] = (unsigned char)( (unsigned)pPres[c] | (pPols1[Abc_Lit2Var(*pLit)] << (2*(pLit-p->pClauses[c]-1))) ); + // clean negative polarity + for ( c = iClaBeg; c < iClaEnd; c++ ) + for ( pLit = p->pClauses[c]+1; pLit < p->pClauses[c+1]; pLit++ ) + pPols0[Abc_Lit2Var(*pLit)] = pPols1[Abc_Lit2Var(*pLit)] = 0; + } + ABC_FREE( pPols0 ); + ABC_FREE( pPols1 ); +/* +// for ( c = 0; c < p->nClauses; c++ ) + for ( c = 0; c < 100; c++ ) + { + printf( "Clause %6d : ", c ); + for ( i = 0; i < 4; i++ ) + printf( "%d ", ((unsigned)pPres[c] >> (2*i)) & 3 ); + printf( " " ); + for ( pLit = p->pClauses[c]; pLit < p->pClauses[c+1]; pLit++ ) + printf( "%6d ", *pLit ); + printf( "\n" ); + } +*/ + return pPres; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// |