diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2013-10-27 14:16:29 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2013-10-27 14:16:29 -0700 |
commit | a7867378ac835c7775f6fae0749943d773e83498 (patch) | |
tree | 2a5caba1e5d1660b24cee21dd06b6224666d5d91 /src/aig | |
parent | b39e09bb734e32aefd52ebf4a4096abdaf71585c (diff) | |
download | abc-a7867378ac835c7775f6fae0749943d773e83498.tar.gz abc-a7867378ac835c7775f6fae0749943d773e83498.tar.bz2 abc-a7867378ac835c7775f6fae0749943d773e83498.zip |
New BMC engine.
Diffstat (limited to 'src/aig')
-rw-r--r-- | src/aig/gia/giaJf.c | 48 |
1 files changed, 45 insertions, 3 deletions
diff --git a/src/aig/gia/giaJf.c b/src/aig/gia/giaJf.c index 414d4f63..9ab27c7c 100644 --- a/src/aig/gia/giaJf.c +++ b/src/aig/gia/giaJf.c @@ -159,7 +159,7 @@ void Jf_ManGenCnf( word uTruth, int iLitOut, Vec_Int_t * vLeaves, Vec_Int_t * vL } } } -Cnf_Dat_t * Jf_ManCreateCnf( Gia_Man_t * p, Vec_Int_t * vLits, Vec_Int_t * vClas ) +Cnf_Dat_t * Jf_ManCreateCnfRemap( Gia_Man_t * p, Vec_Int_t * vLits, Vec_Int_t * vClas ) { Cnf_Dat_t * pCnf; Gia_Obj_t * pObj; @@ -189,6 +189,42 @@ Cnf_Dat_t * Jf_ManCreateCnf( Gia_Man_t * p, Vec_Int_t * vLits, Vec_Int_t * vClas pCnf->pVarNums = pMap; return pCnf; } +Cnf_Dat_t * Jf_ManCreateCnf( Gia_Man_t * p, Vec_Int_t * vLits, Vec_Int_t * vClas ) +{ + Cnf_Dat_t * pCnf; + int i, Entry, iOut; + // generate CNF + pCnf = ABC_CALLOC( Cnf_Dat_t, 1 ); + pCnf->pMan = (Aig_Man_t *)p; + pCnf->nVars = Gia_ManObjNum(p); + pCnf->nLiterals = Vec_IntSize(vLits); + pCnf->nClauses = Vec_IntSize(vClas); + pCnf->pClauses = ABC_ALLOC( int *, pCnf->nClauses+1 ); + pCnf->pClauses[0] = Vec_IntReleaseArray(vLits); + Vec_IntForEachEntry( vClas, Entry, i ) + pCnf->pClauses[i] = pCnf->pClauses[0] + Entry; + pCnf->pClauses[i] = pCnf->pClauses[0] + pCnf->nLiterals; + // create mapping of objects into their clauses + pCnf->pObj2Clause = ABC_FALLOC( int, Gia_ManObjNum(p) ); + pCnf->pObj2Count = ABC_FALLOC( int, Gia_ManObjNum(p) ); + for ( i = 0; i < pCnf->nClauses; i++ ) + { + iOut = Abc_Lit2Var(pCnf->pClauses[i][0]); + if ( pCnf->pObj2Clause[iOut] == -1 ) + { +// printf( "\n" ); + pCnf->pObj2Clause[iOut] = i; + pCnf->pObj2Count[iOut] = 1; + } + else + { + assert( pCnf->pObj2Count[iOut] > 0 ); + pCnf->pObj2Count[iOut]++; + } +//printf( "%d ", iOut ); + } + return pCnf; +} /**Function************************************************************* @@ -1713,7 +1749,7 @@ Gia_Man_t * Jf_ManPerformMapping( Gia_Man_t * pGia, Jf_Par_t * pPars ) Jf_ManFree( p ); return pNew; } -void Jf_ManTestCnf( Gia_Man_t * p ) +Cnf_Dat_t * Jf_ManDeriveCnf( Gia_Man_t * p ) { Cnf_Dat_t * pCnf; Gia_Man_t * pNew; @@ -1722,8 +1758,14 @@ void Jf_ManTestCnf( Gia_Man_t * p ) pPars->fGenCnf = 1; pNew = Jf_ManPerformMapping( p, pPars ); pCnf = (Cnf_Dat_t *)pNew->pData; pNew->pData = NULL; - Gia_ManStop( pNew ); +// Gia_ManStop( pNew ); + return pCnf; +} +void Jf_ManTestCnf( Gia_Man_t * p ) +{ + Cnf_Dat_t * pCnf = Jf_ManDeriveCnf( p ); Cnf_DataWriteIntoFile( pCnf, "test.cnf", 0, NULL, NULL ); + Gia_ManStop( (Gia_Man_t *)pCnf->pMan ); Cnf_DataFree(pCnf); } |