diff options
| author | Yen-Sheng Ho <ysho@berkeley.edu> | 2017-03-16 13:33:14 -0700 |
|---|---|---|
| committer | Yen-Sheng Ho <ysho@berkeley.edu> | 2017-03-16 13:33:14 -0700 |
| commit | b9971b2348cd8940cf74db7b3d6e0c7146db6af2 (patch) | |
| tree | ef01da60c798e3f3d883ae1bb5e7210df2031451 /src/base/wlc | |
| parent | 6bf50cbb8660616bfc4de4715f55e439465c2603 (diff) | |
| download | abc-b9971b2348cd8940cf74db7b3d6e0c7146db6af2.tar.gz abc-b9971b2348cd8940cf74db7b3d6e0c7146db6af2.tar.bz2 abc-b9971b2348cd8940cf74db7b3d6e0c7146db6af2.zip | |
added another function for printing wlc
Diffstat (limited to 'src/base/wlc')
| -rw-r--r-- | src/base/wlc/wlcAbs.c | 31 |
1 files changed, 31 insertions, 0 deletions
diff --git a/src/base/wlc/wlcAbs.c b/src/base/wlc/wlcAbs.c index ebe4cbe1..23e60b0d 100644 --- a/src/base/wlc/wlcAbs.c +++ b/src/base/wlc/wlcAbs.c @@ -54,6 +54,35 @@ int IntPairPtrCompare ( Int_Pair_t ** a, Int_Pair_t ** b ) /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// +void Wlc_NtkPrintNtk( Wlc_Ntk_t * p ) +{ + int i; + Wlc_Obj_t * pObj; + + Abc_Print( 1, "PIs:"); + Wlc_NtkForEachPi( p, pObj, i ) + Abc_Print( 1, " %s", Wlc_ObjName(p, Wlc_ObjId(p, pObj)) ); + Abc_Print( 1, "\n\n"); + + Abc_Print( 1, "POs:"); + Wlc_NtkForEachPo( p, pObj, i ) + Abc_Print( 1, " %s", Wlc_ObjName(p, Wlc_ObjId(p, pObj)) ); + Abc_Print( 1, "\n\n"); + + Abc_Print( 1, "FO(Fi)s:"); + Wlc_NtkForEachCi( p, pObj, i ) + if ( !Wlc_ObjIsPi( pObj ) ) + Abc_Print( 1, " %s(%s)", Wlc_ObjName(p, Wlc_ObjId(p, pObj)), Wlc_ObjName(p, Wlc_ObjId(p, Wlc_ObjFo2Fi(p, pObj))) ); + Abc_Print( 1, "\n\n"); + + Abc_Print( 1, "Objs:\n"); + Wlc_NtkForEachObj( p, pObj, i ) + { + if ( !Wlc_ObjIsCi(pObj) ) + Wlc_NtkPrintNode( p, pObj ) ; + } +} + void Wlc_NtkAbsGetSupp_rec( Wlc_Ntk_t * p, Wlc_Obj_t * pObj, Vec_Bit_t * vCiMarks, Vec_Int_t * vSuppRefs, Vec_Int_t * vSuppList ) { int i, iFanin, iObj; @@ -107,6 +136,7 @@ void Wlc_NtkAbsAnalyzeRefine( Wlc_Ntk_t * p, Vec_Int_t * vBlacks, Vec_Bit_t * vU vSuppList = Vec_IntAlloc( Wlc_NtkCiNum(p) + Vec_IntSize(vBlacks) ); vSuppRefs = Vec_IntAlloc( Wlc_NtkObjNumMax( p ) ); + Vec_IntFill( vSuppRefs, Wlc_NtkObjNumMax( p ), 0 ); Wlc_NtkForEachCi( p, pObj, i ) @@ -1177,6 +1207,7 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars ) pPdrPars->nRestLimit = 500; // reset queue or proof-obligations when it gets larger than this } + // perform refinement iterations for ( nIters = 1; nIters < pPars->nIterMax; nIters++ ) { |