diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2013-10-31 13:07:43 -0400 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2013-10-31 13:07:43 -0400 |
| commit | f620a857d36343b2e475e3b60537fa56fee4d65c (patch) | |
| tree | ec4c7d4ee92a132a67bdd4125a1356254edae88e /src/aig | |
| parent | a457bfe1e580f646f1e02a1a1a00cde1e157353d (diff) | |
| download | abc-f620a857d36343b2e475e3b60537fa56fee4d65c.tar.gz abc-f620a857d36343b2e475e3b60537fa56fee4d65c.tar.bz2 abc-f620a857d36343b2e475e3b60537fa56fee4d65c.zip | |
Specialized induction check.
Diffstat (limited to 'src/aig')
| -rw-r--r-- | src/aig/gia/gia.h | 3 | ||||
| -rw-r--r-- | src/aig/gia/giaJf.c | 10 |
2 files changed, 9 insertions, 4 deletions
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index 7d5d6dde..416ec8a0 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -253,6 +253,7 @@ struct Jf_Par_t_ int fCutMin; int fFuncDsd; int fGenCnf; + int fCnfObjIds; int fPureAig; int fVerbose; int fVeryVerbose; @@ -1097,7 +1098,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 ); +extern Gia_Man_t * Jf_ManDeriveCnf( Gia_Man_t * p, int fCnfObjIds ); /*=== 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 5f30b524..8ba81c4c 100644 --- a/src/aig/gia/giaJf.c +++ b/src/aig/gia/giaJf.c @@ -1540,7 +1540,10 @@ Gia_Man_t * Jf_ManDeriveMappingGia( Jf_Man_t * p ) // derive CNF if ( p->pPars->fGenCnf ) { - pNew->pData = Jf_ManCreateCnf( pNew, vLits, vClas ); + if ( p->pPars->fCnfObjIds ) + pNew->pData = Jf_ManCreateCnf( pNew, vLits, vClas ); + else + pNew->pData = Jf_ManCreateCnfRemap( pNew, vLits, vClas ); } Vec_IntFreeP( &vLits ); Vec_IntFreeP( &vClas ); @@ -1749,11 +1752,12 @@ Gia_Man_t * Jf_ManPerformMapping( Gia_Man_t * pGia, Jf_Par_t * pPars ) Jf_ManFree( p ); return pNew; } -Gia_Man_t * Jf_ManDeriveCnf( Gia_Man_t * p ) +Gia_Man_t * Jf_ManDeriveCnf( Gia_Man_t * p, int fCnfObjIds ) { Jf_Par_t Pars, * pPars = &Pars; Jf_ManSetDefaultPars( pPars ); pPars->fGenCnf = 1; + pPars->fCnfObjIds = fCnfObjIds; return Jf_ManPerformMapping( p, pPars ); } void Jf_ManTestCnf( Gia_Man_t * p ) @@ -1762,7 +1766,7 @@ void Jf_ManTestCnf( Gia_Man_t * p ) Cnf_Dat_t * pCnf; int i; // Cnf_Dat_t * pCnf = Cnf_DeriveGia( p ); - pNew = Jf_ManDeriveCnf( p ); + pNew = Jf_ManDeriveCnf( p, 1 ); pCnf = (Cnf_Dat_t *)pNew->pData; pNew->pData = NULL; Cnf_DataWriteIntoFile( pCnf, "test.cnf", 0, NULL, NULL ); for ( i = 0; i < pCnf->nVars; i++ ) |