diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2011-03-08 20:05:09 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2011-03-08 20:05:09 -0800 |
| commit | 937979d9dd0153519ae29297db7a3f753d5a2dbd (patch) | |
| tree | 0532297b69315ced6f08619de108d1eada4c3d72 /src/aig/int/intInt.h | |
| parent | eabc42a2d8cab80f93b73bb3cb2289adbcd1dcfc (diff) | |
| download | abc-937979d9dd0153519ae29297db7a3f753d5a2dbd.tar.gz abc-937979d9dd0153519ae29297db7a3f753d5a2dbd.tar.bz2 abc-937979d9dd0153519ae29297db7a3f753d5a2dbd.zip | |
Improvements to the interpolation command 'int'; change of default switch -t.
Diffstat (limited to 'src/aig/int/intInt.h')
| -rw-r--r-- | src/aig/int/intInt.h | 54 |
1 files changed, 31 insertions, 23 deletions
diff --git a/src/aig/int/intInt.h b/src/aig/int/intInt.h index 72079a49..d5e8ed00 100644 --- a/src/aig/int/intInt.h +++ b/src/aig/int/intInt.h @@ -79,6 +79,9 @@ struct Inter_Man_t_ int timeTotal; }; +// containment checking manager +typedef struct Inter_Check_t_ Inter_Check_t; + //////////////////////////////////////////////////////////////////////// /// MACRO DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -87,38 +90,43 @@ struct Inter_Man_t_ /// FUNCTION DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -/*=== intContain.c ==========================================================*/ -extern int Inter_ManCheckContainment( Aig_Man_t * pNew, Aig_Man_t * pOld ); -extern int Inter_ManCheckEquivalence( Aig_Man_t * pNew, Aig_Man_t * pOld ); -extern int Inter_ManCheckInductiveContainment( Aig_Man_t * pTrans, Aig_Man_t * pInter, int nSteps, int fBackward ); +/*=== intCheck.c ============================================================*/ +extern Inter_Check_t * Inter_CheckStart( Aig_Man_t * pTrans, int nFramesK ); +extern void Inter_CheckStop( Inter_Check_t * p ); +extern int Inter_CheckPerform( Inter_Check_t * p, Cnf_Dat_t * pCnf ); + +/*=== intContain.c ============================================================*/ +extern int Inter_ManCheckContainment( Aig_Man_t * pNew, Aig_Man_t * pOld ); +extern int Inter_ManCheckEquivalence( Aig_Man_t * pNew, Aig_Man_t * pOld ); +extern int Inter_ManCheckInductiveContainment( Aig_Man_t * pTrans, Aig_Man_t * pInter, int nSteps, int fBackward ); -/*=== intCtrex.c ==========================================================*/ -extern void * Inter_ManGetCounterExample( Aig_Man_t * pAig, int nFrames, int fVerbose ); +/*=== intCtrex.c ============================================================*/ +extern void * Inter_ManGetCounterExample( Aig_Man_t * pAig, int nFrames, int fVerbose ); -/*=== intDup.c ==========================================================*/ -extern Aig_Man_t * Inter_ManStartInitState( int nRegs ); -extern Aig_Man_t * Inter_ManStartDuplicated( Aig_Man_t * p ); -extern Aig_Man_t * Inter_ManStartOneOutput( Aig_Man_t * p, int fAddFirstPo ); +/*=== intDup.c ============================================================*/ +extern Aig_Man_t * Inter_ManStartInitState( int nRegs ); +extern Aig_Man_t * Inter_ManStartDuplicated( Aig_Man_t * p ); +extern Aig_Man_t * Inter_ManStartOneOutput( Aig_Man_t * p, int fAddFirstPo ); -/*=== intFrames.c ==========================================================*/ -extern Aig_Man_t * Inter_ManFramesInter( Aig_Man_t * pAig, int nFrames, int fAddRegOuts ); +/*=== intFrames.c ============================================================*/ +extern Aig_Man_t * Inter_ManFramesInter( Aig_Man_t * pAig, int nFrames, int fAddRegOuts ); -/*=== intMan.c ==========================================================*/ -extern Inter_Man_t * Inter_ManCreate( Aig_Man_t * pAig, Inter_ManParams_t * pPars ); -extern void Inter_ManClean( Inter_Man_t * p ); -extern void Inter_ManStop( Inter_Man_t * p ); +/*=== intMan.c ============================================================*/ +extern Inter_Man_t * Inter_ManCreate( Aig_Man_t * pAig, Inter_ManParams_t * pPars ); +extern void Inter_ManClean( Inter_Man_t * p ); +extern void Inter_ManStop( Inter_Man_t * p ); -/*=== intM114.c ==========================================================*/ -extern int Inter_ManPerformOneStep( Inter_Man_t * p, int fUseBias, int fUseBackward ); +/*=== intM114.c ============================================================*/ +extern int Inter_ManPerformOneStep( Inter_Man_t * p, int fUseBias, int fUseBackward ); -/*=== intM114p.c ==========================================================*/ +/*=== intM114p.c ============================================================*/ #ifdef ABC_USE_LIBRARIES -extern int Inter_ManPerformOneStepM114p( Inter_Man_t * p, int fUsePudlak, int fUseOther ); +extern int Inter_ManPerformOneStepM114p( Inter_Man_t * p, int fUsePudlak, int fUseOther ); #endif -/*=== intUtil.c ==========================================================*/ -extern int Inter_ManCheckInitialState( Aig_Man_t * p ); -extern int Inter_ManCheckAllStates( Aig_Man_t * p ); +/*=== intUtil.c ============================================================*/ +extern int Inter_ManCheckInitialState( Aig_Man_t * p ); +extern int Inter_ManCheckAllStates( Aig_Man_t * p ); |