diff options
Diffstat (limited to 'src/aig')
-rw-r--r-- | src/aig/gia/gia.h | 1 | ||||
-rw-r--r-- | src/aig/gia/giaJf.c | 32 | ||||
-rw-r--r-- | src/aig/gia/giaMan.c | 2 |
3 files changed, 19 insertions, 16 deletions
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index 8d953273..1d170102 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -1097,6 +1097,7 @@ extern Gia_Man_t * Gia_ManPerformMapping( Gia_Man_t * p, void * pIfPars, /*=== giaJf.c ===========================================================*/ extern void Jf_ManSetDefaultPars( Jf_Par_t * pPars ); extern Gia_Man_t * Jf_ManPerformMapping( Gia_Man_t * pGia, Jf_Par_t * pPars ); +extern Gia_Man_t * Jf_ManDeriveCnf( Gia_Man_t * p ); /*=== giaIso.c ===========================================================*/ extern Gia_Man_t * Gia_ManIsoCanonicize( Gia_Man_t * p, int fVerbose ); extern Gia_Man_t * Gia_ManIsoReduce( Gia_Man_t * p, Vec_Ptr_t ** pvPosEquivs, Vec_Ptr_t ** pvPiPerms, int fEstimate, int fDualOut, int fVerbose, int fVeryVerbose ); diff --git a/src/aig/gia/giaJf.c b/src/aig/gia/giaJf.c index 9ab27c7c..46aa5d3f 100644 --- a/src/aig/gia/giaJf.c +++ b/src/aig/gia/giaJf.c @@ -212,7 +212,6 @@ Cnf_Dat_t * Jf_ManCreateCnf( Gia_Man_t * p, Vec_Int_t * vLits, Vec_Int_t * vClas iOut = Abc_Lit2Var(pCnf->pClauses[i][0]); if ( pCnf->pObj2Clause[iOut] == -1 ) { -// printf( "\n" ); pCnf->pObj2Clause[iOut] = i; pCnf->pObj2Count[iOut] = 1; } @@ -221,7 +220,6 @@ Cnf_Dat_t * Jf_ManCreateCnf( Gia_Man_t * p, Vec_Int_t * vLits, Vec_Int_t * vClas assert( pCnf->pObj2Count[iOut] > 0 ); pCnf->pObj2Count[iOut]++; } -//printf( "%d ", iOut ); } return pCnf; } @@ -1455,8 +1453,6 @@ Gia_Man_t * Jf_ManDeriveMappingGia( Jf_Man_t * p ) { vLits = Vec_IntAlloc( 1000 ); vClas = Vec_IntAlloc( 1000 ); - Vec_IntPush( vClas, Vec_IntSize(vLits) ); - Vec_IntPush( vLits, 1 ); } // create new manager pNew = Gia_ManStart( Gia_ManObjNum(p->pGia) ); @@ -1499,10 +1495,10 @@ Gia_Man_t * Jf_ManDeriveMappingGia( Jf_Man_t * p ) Vec_IntPush( vLeaves, Abc_Lit2LitL(Vec_IntArray(vCopies), iLit) ); // create GIA iLit = Kit_TruthToGia( pNew, (unsigned *)pTruth, Vec_IntSize(vLeaves), vCover, vLeaves, 0 ); - iLit = Abc_LitNotCond( iLit, Jf_CutFuncCompl(pCut) ); - Vec_IntWriteEntry( vCopies, i, iLit ); if ( p->pPars->fGenCnf ) Jf_ManGenCnf( uTruth, iLit, vLeaves, vLits, vClas, vCover ); + iLit = Abc_LitNotCond( iLit, Jf_CutFuncCompl(pCut) ); + Vec_IntWriteEntry( vCopies, i, iLit ); // create mapping Vec_IntSetEntry( vMapping, Abc_Lit2Var(iLit), Vec_IntSize(vMapping2) ); Vec_IntPush( vMapping2, Vec_IntSize(vLeaves) ); @@ -1541,7 +1537,11 @@ Gia_Man_t * Jf_ManDeriveMappingGia( Jf_Man_t * p ) Gia_ManSetRegNum( pNew, Gia_ManRegNum(p->pGia) ); // derive CNF if ( p->pPars->fGenCnf ) + { + Vec_IntPush( vClas, Vec_IntSize(vLits) ); + Vec_IntPush( vLits, 1 ); pNew->pData = Jf_ManCreateCnf( pNew, vLits, vClas ); + } Vec_IntFreeP( &vLits ); Vec_IntFreeP( &vClas ); return pNew; @@ -1749,23 +1749,25 @@ Gia_Man_t * Jf_ManPerformMapping( Gia_Man_t * pGia, Jf_Par_t * pPars ) Jf_ManFree( p ); return pNew; } -Cnf_Dat_t * Jf_ManDeriveCnf( Gia_Man_t * p ) +Gia_Man_t * Jf_ManDeriveCnf( Gia_Man_t * p ) { - Cnf_Dat_t * pCnf; - Gia_Man_t * pNew; Jf_Par_t Pars, * pPars = &Pars; Jf_ManSetDefaultPars( pPars ); pPars->fGenCnf = 1; - pNew = Jf_ManPerformMapping( p, pPars ); - pCnf = (Cnf_Dat_t *)pNew->pData; pNew->pData = NULL; -// Gia_ManStop( pNew ); - return pCnf; + return Jf_ManPerformMapping( p, pPars ); } void Jf_ManTestCnf( Gia_Man_t * p ) { - Cnf_Dat_t * pCnf = Jf_ManDeriveCnf( p ); + Gia_Man_t * pNew; + Cnf_Dat_t * pCnf; + int i; +// Cnf_Dat_t * pCnf = Cnf_DeriveGia( p ); + pNew = Jf_ManDeriveCnf( p ); + pCnf = (Cnf_Dat_t *)pNew->pData; pNew->pData = NULL; Cnf_DataWriteIntoFile( pCnf, "test.cnf", 0, NULL, NULL ); - Gia_ManStop( (Gia_Man_t *)pCnf->pMan ); + for ( i = 0; i < pCnf->nVars; i++ ) + printf( "%d : %d %d\n", i, pCnf->pObj2Count[i], pCnf->pObj2Clause[i] ); + Gia_ManStop( pNew ); Cnf_DataFree(pCnf); } diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c index eb728cd0..71becf0b 100644 --- a/src/aig/gia/giaMan.c +++ b/src/aig/gia/giaMan.c @@ -368,7 +368,7 @@ void Gia_ManPrintStats( Gia_Man_t * p, Gps_Par_t * pPars ) if ( p->pSibls ) Gia_ManPrintChoiceStats( p ); if ( Gia_ManHasMapping(p) ) - Gia_ManPrintMappingStats( p, pPars->fDumpFile ); + Gia_ManPrintMappingStats( p, pPars && pPars->fDumpFile ); if ( pPars && pPars->fNpn && Gia_ManHasMapping(p) && Gia_ManLutSizeMax(p) <= 4 ) Gia_ManPrintNpnClasses( p ); if ( p->vPacking ) |