diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2017-01-14 16:11:59 +0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2017-01-14 16:11:59 +0700 |
| commit | 79701f8b4603596095d3d04a13018c8e9598f7a0 (patch) | |
| tree | a8bf60919f71452cc9f59106a7d7f5191b49489c /src/aig/gia/giaEquiv.c | |
| parent | 6d606b51ab084c96d92848be789397700bb3591f (diff) | |
| download | abc-79701f8b4603596095d3d04a13018c8e9598f7a0.tar.gz abc-79701f8b4603596095d3d04a13018c8e9598f7a0.tar.bz2 abc-79701f8b4603596095d3d04a13018c8e9598f7a0.zip | |
Updates to arithmetic verification.
Diffstat (limited to 'src/aig/gia/giaEquiv.c')
| -rw-r--r-- | src/aig/gia/giaEquiv.c | 27 |
1 files changed, 26 insertions, 1 deletions
diff --git a/src/aig/gia/giaEquiv.c b/src/aig/gia/giaEquiv.c index 584be4cd..1b0bce07 100644 --- a/src/aig/gia/giaEquiv.c +++ b/src/aig/gia/giaEquiv.c @@ -129,7 +129,7 @@ Gia_Man_t * Gia_ManOrigIdsReduce( Gia_Man_t * p, Vec_Int_t * vPairs ) } Gia_ManHashStop( pNew ); Gia_ManForEachCo( p, pObj, i ) - Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); Vec_IntFree( vMap ); // compute equivalences assert( !p->pReprs && !p->pNexts ); @@ -171,6 +171,31 @@ Gia_Man_t * Gia_ManOrigIdsReduceTest( Gia_Man_t * p, Vec_Int_t * vPairs ) /**Function************************************************************* + Synopsis [Compute equivalence classes of nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Gia_ManComputeGiaEquivs( Gia_Man_t * pGia, int nConfs, int fVerbose ) +{ + Gia_Man_t * pTemp; + Cec_ParFra_t ParsFra, * pPars = &ParsFra; + Cec_ManFraSetDefaultParams( pPars ); + pPars->fUseOrigIds = 1; + pPars->fSatSweeping = 1; + pPars->nBTLimit = nConfs; + pPars->fVerbose = fVerbose; + pTemp = Cec_ManSatSweeping( pGia, pPars, 0 ); + Gia_ManStop( pTemp ); + return Gia_ManOrigIdsReduce( pGia, pGia->vIdsEquiv ); +} + +/**Function************************************************************* + Synopsis [Returns 1 if AIG is not in the required topo order.] Description [] |