diff options
Diffstat (limited to 'src/base/wlc/wlc.h')
-rw-r--r-- | src/base/wlc/wlc.h | 24 |
1 files changed, 24 insertions, 0 deletions
diff --git a/src/base/wlc/wlc.h b/src/base/wlc/wlc.h index 53936cc9..5d4f374e 100644 --- a/src/base/wlc/wlc.h +++ b/src/base/wlc/wlc.h @@ -180,10 +180,34 @@ struct Wlc_Par_t_ int fCheckCombUnsat; // Check if ABS becomes comb. unsat int fAbs2; // Use UFAR style createAbs int fProofUsePPI; // Use PPI values in PBR + int fUseBmc3; // Run BMC3 in parallel int fVerbose; // verbose output int fPdrVerbose; // verbose output }; +typedef struct Wla_Man_t_ Wla_Man_t; +struct Wla_Man_t_ +{ + Wlc_Ntk_t * p; + Wlc_Par_t * pPars; + Vec_Vec_t * vClauses; + Vec_Int_t * vBlacks; + Abc_Cex_t * pCex; + Gia_Man_t * pGia; + Vec_Bit_t * vUnmark; + void * pPdrPars; + void * pThread; + + int nIters; + int nTotalCla; + int nDisj; + int nNDisj; + + abctime tPdr; + abctime tCbr; + abctime tPbr; +}; + 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); } |