diff options
Diffstat (limited to 'src/proof/abs/absRef2.h')
-rw-r--r-- | src/proof/abs/absRef2.h | 67 |
1 files changed, 67 insertions, 0 deletions
diff --git a/src/proof/abs/absRef2.h b/src/proof/abs/absRef2.h new file mode 100644 index 00000000..df7774c0 --- /dev/null +++ b/src/proof/abs/absRef2.h @@ -0,0 +1,67 @@ +/**CFile**************************************************************** + + FileName [absRef2.h] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Abstraction package.] + + Synopsis [Refinement manager.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: absRef2.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#ifndef ABC__proof_abs__AbsRef2_h +#define ABC__proof_abs__AbsRef2_h + + +//////////////////////////////////////////////////////////////////////// +/// INCLUDES /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// PARAMETERS /// +//////////////////////////////////////////////////////////////////////// + +ABC_NAMESPACE_HEADER_START + + +//////////////////////////////////////////////////////////////////////// +/// BASIC TYPES /// +//////////////////////////////////////////////////////////////////////// + +typedef struct Rf2_Man_t_ Rf2_Man_t; // refinement manager + +//////////////////////////////////////////////////////////////////////// +/// MACRO DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +/*=== giaAbsRef.c ===========================================================*/ +extern Rf2_Man_t * Rf2_ManStart( Gia_Man_t * pGia ); +extern void Rf2_ManStop( Rf2_Man_t * p, int fProfile ); +extern double Rf2_ManMemoryUsage( Rf2_Man_t * p ); +extern Vec_Int_t * Rf2_ManRefine( Rf2_Man_t * p, Abc_Cex_t * pCex, Vec_Int_t * vMap, int fPropFanout, int fVerbose ); + + + +ABC_NAMESPACE_HEADER_END + + + +#endif + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + |