From 19510bd38e46fd913bf6dc29393938e50fd717ee Mon Sep 17 00:00:00 2001
From: Yen-Sheng Ho <ysho@berkeley.edu>
Date: Mon, 20 Feb 2017 11:07:12 -0800
Subject: added datastructure for %pdra options

---
 src/base/wlc/wlc.h    | 18 +++++++++++++++++-
 src/base/wlc/wlcAbs.c | 27 ++++++++++++++++++++++++++-
 src/base/wlc/wlcCom.c |  4 ++--
 3 files changed, 45 insertions(+), 4 deletions(-)

diff --git a/src/base/wlc/wlc.h b/src/base/wlc/wlc.h
index 9ca56917..cf8bdab4 100644
--- a/src/base/wlc/wlc.h
+++ b/src/base/wlc/wlc.h
@@ -174,6 +174,21 @@ struct Wlc_Par_t_
     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                    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);                                            }
@@ -277,7 +292,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, Wlc_Par_t * pPars );
+extern int            Wlc_NtkPdrAbs( Wlc_Ntk_t * p, WlcPdr_Par_t * pPars );
 /*=== wlcAbs2.c ========================================================*/
 extern int            Wlc_NtkAbsCore2( Wlc_Ntk_t * p, Wlc_Par_t * pPars );
 /*=== wlcBlast.c ========================================================*/
@@ -286,6 +301,7 @@ 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 902c060d..8fde7f56 100644
--- a/src/base/wlc/wlcAbs.c
+++ b/src/base/wlc/wlcAbs.c
@@ -38,6 +38,31 @@ extern int           IPdr_ManSolveInt( Pdr_Man_t * p );
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
+/**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->fVerbose    =            0;   // verbose output
+    pPars->fPdrVerbose =            0;   // show verbose PDR output
+}
+
 /**Function*************************************************************
 
   Synopsis    [Mark operators that meet the abstraction criteria.]
@@ -310,7 +335,7 @@ static int Wlc_NtkRemoveFromAbstraction( Wlc_Ntk_t * p, Vec_Int_t * vRefine, Vec
   SeeAlso     []
 
 ***********************************************************************/
-int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars )
+int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, WlcPdr_Par_t * pPars )
 {
     abctime clk = Abc_Clock();
     abctime pdrClk;
diff --git a/src/base/wlc/wlcCom.c b/src/base/wlc/wlcCom.c
index e980752b..d30b376e 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);
-    Wlc_Par_t Pars, * pPars = &Pars;
+    WlcPdr_Par_t Pars, * pPars = &Pars;
     int c;
-    Wlc_ManSetDefaultParams( pPars );
+    WlcPdr_ManSetDefaultParams( pPars );
     Extra_UtilGetoptReset();
     while ( ( c = Extra_UtilGetopt( argc, argv, "AMXFIxvwh" ) ) != EOF )
     {
-- 
cgit v1.2.3