diff options
author | Yen-Sheng Ho <ysho@berkeley.edu> | 2017-02-25 18:32:43 -0800 |
---|---|---|
committer | Yen-Sheng Ho <ysho@berkeley.edu> | 2017-02-25 18:32:43 -0800 |
commit | a8f6e5c60a0ffb23ebb6c1ae2a1a6f27514dc0e2 (patch) | |
tree | b8f4e94b1323d46abb888a58177602f6cc0514eb /src/base/wlc/wlc.h | |
parent | a7bc919b6921fe0a2a0fc152929bc01f6e31b820 (diff) | |
download | abc-a8f6e5c60a0ffb23ebb6c1ae2a1a6f27514dc0e2.tar.gz abc-a8f6e5c60a0ffb23ebb6c1ae2a1a6f27514dc0e2.tar.bz2 abc-a8f6e5c60a0ffb23ebb6c1ae2a1a6f27514dc0e2.zip |
added an option -b to %pdra
Diffstat (limited to 'src/base/wlc/wlc.h')
-rw-r--r-- | src/base/wlc/wlc.h | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/base/wlc/wlc.h b/src/base/wlc/wlc.h index cb84a70d..71273f98 100644 --- a/src/base/wlc/wlc.h +++ b/src/base/wlc/wlc.h @@ -174,6 +174,7 @@ struct Wlc_Par_t_ int fPushClauses; // Push clauses in the reloaded trace int fMFFC; // Refine the entire MFFC of a PPI int fPdra; // Use pdr -nct + int fProofRefine; // Use proof-based refinement int fVerbose; // verbose output int fPdrVerbose; // verbose output }; @@ -311,6 +312,7 @@ extern void Wlc_NtkTransferNames( Wlc_Ntk_t * pNew, Wlc_Ntk_t * p ); extern char * Wlc_NtkNewName( Wlc_Ntk_t * p, int iCoId, int fSeq ); extern Wlc_Ntk_t * Wlc_NtkDupDfs( Wlc_Ntk_t * p, int fMarked, int fSeq ); extern Wlc_Ntk_t * Wlc_NtkDupDfsAbs( Wlc_Ntk_t * p, Vec_Int_t * vPisOld, Vec_Int_t * vPisNew, Vec_Int_t * vFlops ); +extern Wlc_Ntk_t * Wlc_NtkDupDfsSimple( Wlc_Ntk_t * p ); extern void Wlc_NtkCleanMarks( Wlc_Ntk_t * p ); extern void Wlc_NtkMarkCone( Wlc_Ntk_t * p, int iCoId, int Range, int fSeq, int fAllPis ); extern void Wlc_NtkProfileCones( Wlc_Ntk_t * p ); |