1 /**CFile****************************************************************
2
3 FileName [absRef.h]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [Abstraction package.]
8
9 Synopsis [Refinement manager.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - June 20, 2005.]
16
17 Revision [$Id: absRef.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #ifndef ABC__proof_abs__AbsRef_h
22 #define ABC__proof_abs__AbsRef_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
41 ////////////////////////////////////////////////////////////////////////
42 /// MACRO DEFINITIONS ///
43 ////////////////////////////////////////////////////////////////////////
44
45 typedef struct Rnm_Obj_t_ Rnm_Obj_t; // refinement object
46 struct Rnm_Obj_t_
47 {
48 unsigned Value : 1; // binary value
49 unsigned fVisit : 1; // visited object
50 unsigned fVisitJ : 1; // justified visited object
51 unsigned fPPi : 1; // PPI object
52 unsigned Prio : 24; // priority (0 - highest)
53 };
54
55 typedef struct Rnm_Man_t_ Rnm_Man_t; // refinement manager
56 struct Rnm_Man_t_
57 {
58 // user data
59 Gia_Man_t * pGia; // working AIG manager (it is completely owned by this package)
60 Abc_Cex_t * pCex; // counter-example
61 Vec_Int_t * vMap; // mapping of CEX inputs into objects (PI + PPI, in any order)
62 int fPropFanout; // propagate fanouts
63 int fVerbose; // verbose flag
64 int nRefId; // refinement ID
65 // traversing data
66 Vec_Int_t * vObjs; // internal objects used in value propagation
67 // filtering of selected objects
68 Vec_Str_t * vCounts; // fanin counters
69 Vec_Int_t * vFanins; // fanins
70 /*
71 // SAT solver
72 sat_solver2 * pSat; // incremental SAT solver
73 Vec_Int_t * vSatVars; // SAT variables
74 Vec_Int_t * vSat2Ids; // mapping of SAT variables into object IDs
75 Vec_Int_t * vIsopMem; // memory for ISOP computation
76 */
77 // internal data
78 Rnm_Obj_t * pObjs; // refinement objects
79 int nObjs; // the number of used objects
80 int nObjsAlloc; // the number of allocated objects
81 int nObjsFrame; // the number of used objects in each frame
82 int nCalls; // total number of calls
83 int nRefines; // total refined objects
84 int nVisited; // visited during justification
85 // statistics
86 abctime timeFwd; // forward propagation
87 abctime timeBwd; // backward propagation
88 abctime timeVer; // ternary simulation
89 abctime timeTotal; // other time
90 };
91
92 // accessing the refinement object
Rnm_ManObj(Rnm_Man_t * p,Gia_Obj_t * pObj,int f)93 static inline Rnm_Obj_t * Rnm_ManObj( Rnm_Man_t * p, Gia_Obj_t * pObj, int f )
94 {
95 assert( Gia_ObjIsConst0(pObj) || pObj->Value );
96 assert( (int)pObj->Value < p->nObjsFrame );
97 assert( f >= 0 && f <= p->pCex->iFrame );
98 return p->pObjs + f * p->nObjsFrame + pObj->Value;
99 }
Rnm_ManSetRefId(Rnm_Man_t * p,int RefId)100 static inline void Rnm_ManSetRefId( Rnm_Man_t * p, int RefId ) { p->nRefId = RefId; }
101
Rnm_ObjCount(Rnm_Man_t * p,Gia_Obj_t * pObj)102 static inline int Rnm_ObjCount( Rnm_Man_t * p, Gia_Obj_t * pObj ) { return Vec_StrEntry( p->vCounts, Gia_ObjId(p->pGia, pObj) ); }
Rnm_ObjSetCount(Rnm_Man_t * p,Gia_Obj_t * pObj,int c)103 static inline void Rnm_ObjSetCount( Rnm_Man_t * p, Gia_Obj_t * pObj, int c ) { Vec_StrWriteEntry( p->vCounts, Gia_ObjId(p->pGia, pObj), (char)c ); }
Rnm_ObjAddToCount(Rnm_Man_t * p,Gia_Obj_t * pObj)104 static inline int Rnm_ObjAddToCount( Rnm_Man_t * p, Gia_Obj_t * pObj ) { int c = Rnm_ObjCount(p, pObj); if ( c < 16 ) Rnm_ObjSetCount(p, pObj, c+1); return c; }
105
Rnm_ObjIsJust(Rnm_Man_t * p,Gia_Obj_t * pObj)106 static inline int Rnm_ObjIsJust( Rnm_Man_t * p, Gia_Obj_t * pObj ) { return Gia_ObjIsConst0(pObj) || (pObj->Value && Rnm_ManObj(p, pObj, 0)->fVisitJ); }
107
108 ////////////////////////////////////////////////////////////////////////
109 /// FUNCTION DECLARATIONS ///
110 ////////////////////////////////////////////////////////////////////////
111
112 /*=== absRef.c ===========================================================*/
113 extern Rnm_Man_t * Rnm_ManStart( Gia_Man_t * pGia );
114 extern void Rnm_ManStop( Rnm_Man_t * p, int fProfile );
115 extern double Rnm_ManMemoryUsage( Rnm_Man_t * p );
116 extern Vec_Int_t * Rnm_ManRefine( Rnm_Man_t * p, Abc_Cex_t * pCex, Vec_Int_t * vMap, int fPropFanout, int fNewRefinement, int fVerbose );
117 /*=== absRefSelected.c ===========================================================*/
118 extern Vec_Int_t * Rnm_ManFilterSelected( Rnm_Man_t * p, Vec_Int_t * vOldPPis );
119 extern Vec_Int_t * Rnm_ManFilterSelectedNew( Rnm_Man_t * p, Vec_Int_t * vOldPPis );
120
121
122 ABC_NAMESPACE_HEADER_END
123
124 #endif
125
126 ////////////////////////////////////////////////////////////////////////
127 /// END OF FILE ///
128 ////////////////////////////////////////////////////////////////////////
129
130