clean up

4 files changed, 8 insertions, 49 deletions

diff --git a/src/base/wlc/wlc.h b/src/base/wlc/wlc.h
index 9cb34bf3..686d9f00 100644
--- a/src/base/wlc/wlc.h
+++ b/src/base/wlc/wlc.h
@@ -170,27 +170,12 @@ struct Wlc_Par_t_
     int                    nBitsFlop;          // flop bit-width
     int                    nIterMax;           // the max number of iterations
     int                    fXorOutput;         // XOR outputs of word-level miter
-    int                    fVerbose;           // verbose output
-    int                    fPdrVerbose;        // verbose output
-};
-
-
-typedef struct WlcPdr_Par_t_ WlcPdr_Par_t;
-struct WlcPdr_Par_t_
-{
-    int                    nBitsAdd;           // adder bit-width
-    int                    nBitsMul;           // multiplier bit-widht 
-    int                    nBitsMux;           // MUX bit-width
-    int                    nBitsFlop;          // flop bit-width
-    int                    nIterMax;           // the max number of iterations
-    int                    fXorOutput;         // XOR outputs of word-level miter
     int                    fCheckClauses;      // Check clauses in the reloaded trace                    
     int                    fPushClauses;       // Push clauses in the reloaded trace                    
     int                    fVerbose;           // verbose output
     int                    fPdrVerbose;        // verbose output
 };
 
-
 static inline int          Wlc_NtkObjNum( Wlc_Ntk_t * p )                           { return p->iObj - 1;                                                      }
 static inline int          Wlc_NtkObjNumMax( Wlc_Ntk_t * p )                        { return p->iObj;                                                          }
 static inline int          Wlc_NtkPiNum( Wlc_Ntk_t * p )                            { return Vec_IntSize(&p->vPis);                                            }
@@ -294,7 +279,7 @@ static inline Wlc_Obj_t *  Wlc_ObjCo2PoFo( Wlc_Ntk_t * p, int iCoId )
 
 /*=== wlcAbs.c ========================================================*/
 extern int            Wlc_NtkAbsCore( Wlc_Ntk_t * p, Wlc_Par_t * pPars );
-extern int            Wlc_NtkPdrAbs( Wlc_Ntk_t * p, WlcPdr_Par_t * pPars );
+extern int            Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars );
 /*=== wlcAbs2.c ========================================================*/
 extern int            Wlc_NtkAbsCore2( Wlc_Ntk_t * p, Wlc_Par_t * pPars );
 /*=== wlcBlast.c ========================================================*/
@@ -303,7 +288,6 @@ extern Gia_Man_t *    Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int i
 extern void           Wlc_SetNtk( Abc_Frame_t * pAbc, Wlc_Ntk_t * pNtk );
 /*=== wlcNtk.c ========================================================*/
 extern void           Wlc_ManSetDefaultParams( Wlc_Par_t * pPars );
-extern void           WlcPdr_ManSetDefaultParams( WlcPdr_Par_t * pPars );
 extern char *         Wlc_ObjTypeName( Wlc_Obj_t * p );
 extern Wlc_Ntk_t *    Wlc_NtkAlloc( char * pName, int nObjsAlloc );
 extern int            Wlc_ObjAlloc( Wlc_Ntk_t * p, int Type, int Signed, int End, int Beg );
diff --git a/src/base/wlc/wlcAbs.c b/src/base/wlc/wlcAbs.c
index fbaa1b8a..1e5df918 100644
--- a/src/base/wlc/wlcAbs.c
+++ b/src/base/wlc/wlcAbs.c
@@ -40,33 +40,6 @@ extern int           IPdr_ManSolveInt( Pdr_Man_t * p, int fCheckClauses, int fPu
 
 /**Function*************************************************************
 
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-
-void WlcPdr_ManSetDefaultParams( WlcPdr_Par_t * pPars )
-{
-    memset( pPars, 0, sizeof(WlcPdr_Par_t) );
-    pPars->nBitsAdd    = ABC_INFINITY;   // adder bit-width
-    pPars->nBitsMul    = ABC_INFINITY;   // multiplier bit-width 
-    pPars->nBitsMux    = ABC_INFINITY;   // MUX bit-width
-    pPars->nBitsFlop   = ABC_INFINITY;   // flop bit-width
-    pPars->nIterMax    =         1000;   // the max number of iterations
-    pPars->fXorOutput  =            1;   // XOR outputs of word-level miter
-    pPars->fCheckClauses =          1;   // Check clauses in the reloaded trace                    
-    pPars->fPushClauses =           0;   // Push clauses in the reloaded trace                    
-    pPars->fVerbose    =            0;   // verbose output
-    pPars->fPdrVerbose =            0;   // show verbose PDR output
-}
-
-/**Function*************************************************************
-
   Synopsis    [Mark operators that meet the abstraction criteria.]
 
   Description [This procedure returns the array of objects (vLeaves) that 
@@ -78,7 +51,7 @@ void WlcPdr_ManSetDefaultParams( WlcPdr_Par_t * pPars )
   SeeAlso     []
 
 ***********************************************************************/
-static Vec_Bit_t * Wlc_NtkAbsMarkOpers( Wlc_Ntk_t * p, WlcPdr_Par_t * pPars, Vec_Bit_t * vUnmark, int fVerbose )
+static Vec_Bit_t * Wlc_NtkAbsMarkOpers( Wlc_Ntk_t * p, Wlc_Par_t * pPars, Vec_Bit_t * vUnmark, int fVerbose )
 {
     Vec_Bit_t * vLeaves = Vec_BitStart( Wlc_NtkObjNumMax(p) );
     Wlc_Obj_t * pObj; int i, Count[4] = {0};
@@ -199,7 +172,7 @@ static void Wlc_NtkAbsMarkNodes( Wlc_Ntk_t * p, Vec_Bit_t * vLeaves, Vec_Int_t *
   SeeAlso     []
 
 ***********************************************************************/
-static Wlc_Ntk_t * Wlc_NtkAbs( Wlc_Ntk_t * p, WlcPdr_Par_t * pPars, Vec_Bit_t * vUnmark, Vec_Int_t ** pvPisNew, int fVerbose )
+static Wlc_Ntk_t * Wlc_NtkAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars, Vec_Bit_t * vUnmark, Vec_Int_t ** pvPisNew, int fVerbose )
 {
     Wlc_Ntk_t * pNtkNew = NULL;
     Vec_Int_t * vPisOld = Vec_IntAlloc( 100 );
@@ -337,7 +310,7 @@ static int Wlc_NtkRemoveFromAbstraction( Wlc_Ntk_t * p, Vec_Int_t * vRefine, Vec
   SeeAlso     []
 
 ***********************************************************************/
-int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, WlcPdr_Par_t * pPars )
+int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars )
 {
     abctime clk = Abc_Clock();
     abctime pdrClk;
diff --git a/src/base/wlc/wlcCom.c b/src/base/wlc/wlcCom.c
index 7801abc6..df736e70 100644
--- a/src/base/wlc/wlcCom.c
+++ b/src/base/wlc/wlcCom.c
@@ -458,9 +458,9 @@ usage:
 int Abc_CommandPdrAbs( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc);
-    WlcPdr_Par_t Pars, * pPars = &Pars;
+    Wlc_Par_t Pars, * pPars = &Pars;
     int c;
-    WlcPdr_ManSetDefaultParams( pPars );
+    Wlc_ManSetDefaultParams( pPars );
     Extra_UtilGetoptReset();
     while ( ( c = Extra_UtilGetopt( argc, argv, "AMXFIcpxvwh" ) ) != EOF )
     {
diff --git a/src/base/wlc/wlcNtk.c b/src/base/wlc/wlcNtk.c
index e6ab0739..c8fc15a7 100644
--- a/src/base/wlc/wlcNtk.c
+++ b/src/base/wlc/wlcNtk.c
@@ -114,6 +114,8 @@ void Wlc_ManSetDefaultParams( Wlc_Par_t * pPars )
     pPars->nBitsFlop   = ABC_INFINITY;   // flop bit-width
     pPars->nIterMax    =         1000;   // the max number of iterations
     pPars->fXorOutput  =            1;   // XOR outputs of word-level miter
+    pPars->fCheckClauses =          1;   // Check clauses in the reloaded trace                    
+    pPars->fPushClauses =           0;   // Push clauses in the reloaded trace                    
     pPars->fVerbose    =            0;   // verbose output`
     pPars->fPdrVerbose =            0;   // show verbose PDR output
 }