diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2015-10-28 13:44:29 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2015-10-28 13:44:29 -0700 |
commit | 9521d1345b364eeb99498dfc0df329375d0ea669 (patch) | |
tree | 96e06e42241796b3493bfa91061f235959037bea /src/proof/abs | |
parent | fe0487dab6b013ddb6d4e5216b5bd26cf85fd2bb (diff) | |
download | abc-9521d1345b364eeb99498dfc0df329375d0ea669.tar.gz abc-9521d1345b364eeb99498dfc0df329375d0ea669.tar.bz2 abc-9521d1345b364eeb99498dfc0df329375d0ea669.zip |
Improvements to 'satclp'.
Diffstat (limited to 'src/proof/abs')
-rw-r--r-- | src/proof/abs/absRpm.c | 81 |
1 files changed, 81 insertions, 0 deletions
diff --git a/src/proof/abs/absRpm.c b/src/proof/abs/absRpm.c index ef5747c1..edcbe7ed 100644 --- a/src/proof/abs/absRpm.c +++ b/src/proof/abs/absRpm.c @@ -19,6 +19,7 @@ ***********************************************************************/ #include "abs.h" +#include "misc/vec/vecWec.h" ABC_NAMESPACE_IMPL_START @@ -106,6 +107,86 @@ void Gia_ManComputeDoms( Gia_Man_t * p ) Gia_ManAddDom( p, Gia_ObjFanin1(pObj), i ); } } + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Wec_t * Gia_ManCreateSupps( Gia_Man_t * p, int fVerbose ) +{ + abctime clk = Abc_Clock(); + Gia_Obj_t * pObj; int i, Id; + Vec_Wec_t * vSupps = Vec_WecStart( Gia_ManObjNum(p) ); + Gia_ManForEachCiId( p, Id, i ) + Vec_IntPush( Vec_WecEntry(vSupps, Id), i ); + Gia_ManForEachAnd( p, pObj, Id ) + Vec_IntTwoMerge2( Vec_WecEntry(vSupps, Gia_ObjFaninId0(pObj, Id)), + Vec_WecEntry(vSupps, Gia_ObjFaninId1(pObj, Id)), + Vec_WecEntry(vSupps, Id) ); +// Gia_ManForEachCo( p, pObj, i ) +// Vec_IntAppend( Vec_WecEntry(vSupps, Gia_ObjId(p, pObj)), Vec_WecEntry(vSupps, Gia_ObjFaninId0p(p, pObj)) ); + if ( fVerbose ) + Abc_PrintTime( 1, "Support computation", Abc_Clock() - clk ); + return vSupps; +} +void Gia_ManDomTest( Gia_Man_t * p ) +{ + Vec_Int_t * vDoms = Vec_IntAlloc( 100 ); + Vec_Int_t * vSupp = Vec_IntAlloc( 100 ); + Vec_Wec_t * vSupps = Gia_ManCreateSupps( p, 1 ); + Vec_Wec_t * vDomeds = Vec_WecStart( Gia_ManObjNum(p) ); + Gia_Obj_t * pObj, * pDom; int i, Id, nMffcSize; + Gia_ManCreateRefs( p ); + Gia_ManComputeDoms( p ); + Gia_ManForEachCi( p, pObj, i ) + { + if ( Gia_ObjDom(p, pObj) == -1 ) + continue; + for ( pDom = Gia_ManObj(p, Gia_ObjDom(p, pObj)); Gia_ObjIsAnd(pDom); pDom = Gia_ManObj(p, Gia_ObjDom(p, pDom)) ) + Vec_IntPush( Vec_WecEntry(vDomeds, Gia_ObjId(p, pDom)), i ); + } + Gia_ManForEachAnd( p, pObj, i ) + if ( Vec_IntEqual(Vec_WecEntry(vSupps, i), Vec_WecEntry(vDomeds, i)) ) + Vec_IntPush( vDoms, i ); + Vec_WecFree( vSupps ); + Vec_WecFree( vDomeds ); + + // check MFFC sizes + Vec_IntForEachEntry( vDoms, Id, i ) + Gia_ObjRefInc( p, Gia_ManObj(p, Id) ); + Vec_IntForEachEntry( vDoms, Id, i ) + { + nMffcSize = Gia_NodeMffcSizeSupp( p, Gia_ManObj(p, Id), vSupp ); + printf( "%d(%d:%d) ", Id, Vec_IntSize(vSupp), nMffcSize ); + } + printf( "\n" ); + Vec_IntForEachEntry( vDoms, Id, i ) + Gia_ObjRefDec( p, Gia_ManObj(p, Id) ); + +// Vec_IntPrint( vDoms ); + Vec_IntFree( vDoms ); + Vec_IntFree( vSupp ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ void Gia_ManTestDoms2( Gia_Man_t * p ) { Vec_Int_t * vNodes; |