Commit b9971b23 by Yen-Sheng Ho

added another function for printing wlc

parent 6bf50cbb
...@@ -54,6 +54,35 @@ int IntPairPtrCompare ( Int_Pair_t ** a, Int_Pair_t ** b ) ...@@ -54,6 +54,35 @@ int IntPairPtrCompare ( Int_Pair_t ** a, Int_Pair_t ** b )
/// FUNCTION DEFINITIONS /// /// 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 ) 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; int i, iFanin, iObj;
...@@ -107,6 +136,7 @@ void Wlc_NtkAbsAnalyzeRefine( Wlc_Ntk_t * p, Vec_Int_t * vBlacks, Vec_Bit_t * vU ...@@ -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) ); vSuppList = Vec_IntAlloc( Wlc_NtkCiNum(p) + Vec_IntSize(vBlacks) );
vSuppRefs = Vec_IntAlloc( Wlc_NtkObjNumMax( p ) ); vSuppRefs = Vec_IntAlloc( Wlc_NtkObjNumMax( p ) );
Vec_IntFill( vSuppRefs, Wlc_NtkObjNumMax( p ), 0 ); Vec_IntFill( vSuppRefs, Wlc_NtkObjNumMax( p ), 0 );
Wlc_NtkForEachCi( p, pObj, i ) Wlc_NtkForEachCi( p, pObj, i )
...@@ -1177,6 +1207,7 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars ) ...@@ -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 pPdrPars->nRestLimit = 500; // reset queue or proof-obligations when it gets larger than this
} }
// perform refinement iterations // perform refinement iterations
for ( nIters = 1; nIters < pPars->nIterMax; nIters++ ) for ( nIters = 1; nIters < pPars->nIterMax; nIters++ )
{ {
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment