diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2012-01-21 04:30:10 -0800 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2012-01-21 04:30:10 -0800 |
commit | 8014f25f6db719fa62336f997963532a14c568f6 (patch) | |
tree | c691ee91a3a2d452a2bd24ac89a8c717beaa7af7 /src/aig/int/intInt.h | |
parent | c44cc5de9429e6b4f1c05045fcf43c9cb96437b5 (diff) | |
download | abc-8014f25f6db719fa62336f997963532a14c568f6.tar.gz abc-8014f25f6db719fa62336f997963532a14c568f6.tar.bz2 abc-8014f25f6db719fa62336f997963532a14c568f6.zip |
Major restructuring of the code.
Diffstat (limited to 'src/aig/int/intInt.h')
-rw-r--r-- | src/aig/int/intInt.h | 142 |
1 files changed, 0 insertions, 142 deletions
diff --git a/src/aig/int/intInt.h b/src/aig/int/intInt.h deleted file mode 100644 index 66ff9578..00000000 --- a/src/aig/int/intInt.h +++ /dev/null @@ -1,142 +0,0 @@ -/**CFile**************************************************************** - - FileName [intInt.h] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [Interpolation engine.] - - Synopsis [Internal declarations.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - June 24, 2008.] - - Revision [$Id: intInt.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#ifndef __INT_INT_H__ -#define __INT_INT_H__ - - -//////////////////////////////////////////////////////////////////////// -/// INCLUDES /// -//////////////////////////////////////////////////////////////////////// - -#include "saig.h" -#include "cnf.h" -#include "satSolver.h" -#include "satStore.h" -#include "int.h" - -//////////////////////////////////////////////////////////////////////// -/// PARAMETERS /// -//////////////////////////////////////////////////////////////////////// - - - -ABC_NAMESPACE_HEADER_START - - -//////////////////////////////////////////////////////////////////////// -/// BASIC TYPES /// -//////////////////////////////////////////////////////////////////////// - -// interpolation manager -typedef struct Inter_Man_t_ Inter_Man_t; -struct Inter_Man_t_ -{ - // AIG manager - Aig_Man_t * pAig; // the original AIG manager - Aig_Man_t * pAigTrans; // the transformed original AIG manager - Cnf_Dat_t * pCnfAig; // CNF for the original manager - // interpolant - Aig_Man_t * pInter; // the current interpolant - Cnf_Dat_t * pCnfInter; // CNF for the current interplant - // timeframes - Aig_Man_t * pFrames; // the timeframes - Cnf_Dat_t * pCnfFrames; // CNF for the timeframes - // other data - Vec_Int_t * vVarsAB; // the variables participating in - // temporary place for the new interpolant - Aig_Man_t * pInterNew; - Vec_Ptr_t * vInters; - // parameters - int nFrames; // the number of timeframes - int nConfCur; // the current number of conflicts - int nConfLimit; // the limit on the number of conflicts - int fVerbose; // the verbosiness flag - // runtime - int timeRwr; - int timeCnf; - int timeSat; - int timeInt; - int timeEqu; - int timeOther; - int timeTotal; -}; - -// containment checking manager -typedef struct Inter_Check_t_ Inter_Check_t; - -//////////////////////////////////////////////////////////////////////// -/// MACRO DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -/*=== 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, int nTimeNewOut ); - -/*=== 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 ); - -/*=== 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 ); - -/*=== 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, int fProved ); - -/*=== intM114.c ============================================================*/ -extern int Inter_ManPerformOneStep( Inter_Man_t * p, int fUseBias, int fUseBackward, int nTimeNewOut ); - -/*=== intM114p.c ============================================================*/ -#ifdef ABC_USE_LIBRARIES -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 ); - - - -ABC_NAMESPACE_HEADER_END - - - -#endif - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - |