diff options
| author | Yen-Sheng Ho <ysho@berkeley.edu> | 2017-03-02 17:31:30 -0800 |
|---|---|---|
| committer | Yen-Sheng Ho <ysho@berkeley.edu> | 2017-03-02 17:31:30 -0800 |
| commit | 7eac1f576673d8f6c394e41dd90c568ff92046d9 (patch) | |
| tree | 7c5b498f4abd34c2abb95a2b46950a0a3e73c75b /src/base | |
| parent | 18b47dfbd5c9f70511c00bef411e454615620365 (diff) | |
| download | abc-7eac1f576673d8f6c394e41dd90c568ff92046d9.tar.gz abc-7eac1f576673d8f6c394e41dd90c568ff92046d9.tar.bz2 abc-7eac1f576673d8f6c394e41dd90c568ff92046d9.zip | |
added experimental codes
Diffstat (limited to 'src/base')
| -rw-r--r-- | src/base/wlc/wlcAbs.c | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/base/wlc/wlcAbs.c b/src/base/wlc/wlcAbs.c index 776770de..6de8a4fe 100644 --- a/src/base/wlc/wlcAbs.c +++ b/src/base/wlc/wlcAbs.c @@ -34,6 +34,8 @@ extern Vec_Vec_t * IPdr_ManSaveClauses( Pdr_Man_t * p, int fDropLast ); extern int IPdr_ManRestore( Pdr_Man_t * p, Vec_Vec_t * vClauses, Vec_Int_t * vMap ); extern int IPdr_ManSolveInt( Pdr_Man_t * p, int fCheckClauses, int fPushClauses ); extern int IPdr_ManCheckCombUnsat( Pdr_Man_t * p ); +extern int IPdr_ManReduceClauses( Pdr_Man_t * p, Vec_Vec_t * vClauses ); +extern void IPdr_ManPrintClauses( Vec_Vec_t * vClauses, int kStart, int nRegs ); typedef struct Int_Pair_t_ Int_Pair_t; struct Int_Pair_t_ |