diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2016-05-11 11:07:34 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2016-05-11 11:07:34 -0700 |
| commit | 6e8efec57d5ef07ca33a3cefc3c1e6c3f7c70856 (patch) | |
| tree | a932d3800b3dcd220173982289f5bc0c01613a4c /src/proof/acec/acecUtil.c | |
| parent | c89f987dc7aeea7efa4506503446fd22a1cfd7d3 (diff) | |
| download | abc-6e8efec57d5ef07ca33a3cefc3c1e6c3f7c70856.tar.gz abc-6e8efec57d5ef07ca33a3cefc3c1e6c3f7c70856.tar.bz2 abc-6e8efec57d5ef07ca33a3cefc3c1e6c3f7c70856.zip | |
Experiments with CEC for arithmetic circuits.
Diffstat (limited to 'src/proof/acec/acecUtil.c')
| -rw-r--r-- | src/proof/acec/acecUtil.c | 16 |
1 files changed, 14 insertions, 2 deletions
diff --git a/src/proof/acec/acecUtil.c b/src/proof/acec/acecUtil.c index 26087f92..191856cf 100644 --- a/src/proof/acec/acecUtil.c +++ b/src/proof/acec/acecUtil.c @@ -48,11 +48,23 @@ void Gia_PolynCollectXors_rec( Gia_Man_t * pGia, int iObj, Vec_Int_t * vXors ) if ( Gia_ObjIsTravIdCurrent(pGia, pObj) ) return; Gia_ObjSetTravIdCurrent(pGia, pObj); - if ( !Gia_ObjIsAnd(pObj) || !Gia_ObjIsXor(pObj) ) + if ( !Gia_ObjIsAnd(pObj) || !Gia_ObjIsXor(pObj) || Gia_ObjRefNum(pGia, pObj) > 1 ) return; - Vec_IntPush( vXors, iObj ); Gia_PolynCollectXors_rec( pGia, Gia_ObjFaninId0(pObj, iObj), vXors ); Gia_PolynCollectXors_rec( pGia, Gia_ObjFaninId1(pObj, iObj), vXors ); + Vec_IntPushUnique( vXors, iObj ); +} +Vec_Int_t * Gia_PolynCollectLastXor( Gia_Man_t * pGia, int fVerbose ) +{ + Vec_Int_t * vXors = Vec_IntAlloc( 100 ); + Gia_Obj_t * pObj = Gia_ManCo( pGia, Gia_ManCoNum(pGia)-1 ); + ABC_FREE( pGia->pRefs ); + Gia_ManCreateRefs( pGia ); + Gia_ManIncrementTravId( pGia ); + Gia_PolynCollectXors_rec( pGia, Gia_ObjFaninId0p(pGia, pObj), vXors ); + Vec_IntReverseOrder( vXors ); + ABC_FREE( pGia->pRefs ); + return vXors; } void Gia_PolynAnalyzeXors( Gia_Man_t * pGia, int fVerbose ) { |