abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
absRefJ.h
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [absRef2.h]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [Abstraction package.]
8 
9  Synopsis [Refinement manager to compute all justifying subsets.]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - June 20, 2005.]
16 
17  Revision [$Id: absRef2.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #ifndef ABC__proof_abs__AbsRef2_h
22 #define ABC__proof_abs__AbsRef2_h
23 
24 
25 ////////////////////////////////////////////////////////////////////////
26 /// INCLUDES ///
27 ////////////////////////////////////////////////////////////////////////
28 
29 ////////////////////////////////////////////////////////////////////////
30 /// PARAMETERS ///
31 ////////////////////////////////////////////////////////////////////////
32 
33 ABC_NAMESPACE_HEADER_START
34 
35 
36 ////////////////////////////////////////////////////////////////////////
37 /// BASIC TYPES ///
38 ////////////////////////////////////////////////////////////////////////
39 
40 typedef struct Rf2_Man_t_ Rf2_Man_t; // refinement manager
41 
42 ////////////////////////////////////////////////////////////////////////
43 /// MACRO DEFINITIONS ///
44 ////////////////////////////////////////////////////////////////////////
45 
46 ////////////////////////////////////////////////////////////////////////
47 /// FUNCTION DECLARATIONS ///
48 ////////////////////////////////////////////////////////////////////////
49 
50 /*=== giaAbsRef.c ===========================================================*/
51 extern Rf2_Man_t * Rf2_ManStart( Gia_Man_t * pGia );
52 extern void Rf2_ManStop( Rf2_Man_t * p, int fProfile );
53 extern double Rf2_ManMemoryUsage( Rf2_Man_t * p );
54 extern Vec_Int_t * Rf2_ManRefine( Rf2_Man_t * p, Abc_Cex_t * pCex, Vec_Int_t * vMap, int fPropFanout, int fVerbose );
55 
56 
57 
58 ABC_NAMESPACE_HEADER_END
59 
60 
61 
62 #endif
63 
64 ////////////////////////////////////////////////////////////////////////
65 /// END OF FILE ///
66 ////////////////////////////////////////////////////////////////////////
67 
Rf2_ManRefine
Vec_Int_t * Rf2_ManRefine(Rf2_Man_t *p, Abc_Cex_t *pCex, Vec_Int_t *vMap, int fPropFanout, int fVerbose)
Definition: absRefJ.c:863
Rf2_Man_t_::fPropFanout
int fPropFanout
Definition: absRefJ.c:90
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
Rf2_Man_t_::pCex
Abc_Cex_t * pCex
Definition: absRefJ.c:88
Rf2_ManMemoryUsage
double Rf2_ManMemoryUsage(Rf2_Man_t *p)
Definition: absRefJ.c:249
Rf2_ManStart
Rf2_Man_t * Rf2_ManStart(Gia_Man_t *pGia)
MACRO DEFINITIONS ///.
Definition: absRefJ.c:211
Rf2_Man_t_
Definition: absRefJ.c:84
Rf2_Man_t_::pGia
Gia_Man_t * pGia
Definition: absRefJ.c:87
ABC_NAMESPACE_HEADER_START
#define ABC_NAMESPACE_HEADER_START
NAMESPACES ///.
Definition: abc_global.h:105
Rf2_ManStop
void Rf2_ManStop(Rf2_Man_t *p, int fProfile)
Definition: absRefJ.c:225
ABC_NAMESPACE_HEADER_END
#define ABC_NAMESPACE_HEADER_END
Definition: abc_global.h:106
Rf2_Man_t_::vMap
Vec_Int_t * vMap
Definition: absRefJ.c:89
Rf2_Man_t_::fVerbose
int fVerbose
Definition: absRefJ.c:91
Gia_Man_t_
Definition: gia.h:95
Rf2_Man_t
typedefABC_NAMESPACE_HEADER_START struct Rf2_Man_t_ Rf2_Man_t
INCLUDES ///.
Definition: absRefJ.h:40
Abc_Cex_t
typedefABC_NAMESPACE_HEADER_START struct Abc_Cex_t_ Abc_Cex_t
INCLUDES ///.
Definition: utilCex.h:39