1 /**CFile****************************************************************
2
3 FileName [dchInt.h]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [Choice computation for tech-mapping.]
8
9 Synopsis [External declarations.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - June 29, 2008.]
16
17 Revision [$Id: dchInt.h,v 1.00 2008/07/29 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #ifndef ABC__aig__dch__dchInt_h
22 #define ABC__aig__dch__dchInt_h
23
24
25 ////////////////////////////////////////////////////////////////////////
26 /// INCLUDES ///
27 ////////////////////////////////////////////////////////////////////////
28
29 #include "aig/aig/aig.h"
30 #include "sat/bsat/satSolver.h"
31 #include "dch.h"
32
33 ////////////////////////////////////////////////////////////////////////
34 /// PARAMETERS ///
35 ////////////////////////////////////////////////////////////////////////
36
37
38
39 ABC_NAMESPACE_HEADER_START
40
41
42 ////////////////////////////////////////////////////////////////////////
43 /// BASIC TYPES ///
44 ////////////////////////////////////////////////////////////////////////
45
46 // equivalence classes
47 typedef struct Dch_Cla_t_ Dch_Cla_t;
48
49 // choicing manager
50 typedef struct Dch_Man_t_ Dch_Man_t;
51 struct Dch_Man_t_
52 {
53 // parameters
54 Dch_Pars_t * pPars; // choicing parameters
55 // AIGs used in the package
56 // Vec_Ptr_t * vAigs; // user-given AIGs
57 Aig_Man_t * pAigTotal; // intermediate AIG
58 Aig_Man_t * pAigFraig; // final AIG
59 // equivalence classes
60 Dch_Cla_t * ppClasses; // equivalence classes of nodes
61 Aig_Obj_t ** pReprsProved; // equivalences proved
62 // SAT solving
63 sat_solver * pSat; // recyclable SAT solver
64 int nSatVars; // the counter of SAT variables
65 int * pSatVars; // mapping of each node into its SAT var
66 Vec_Ptr_t * vUsedNodes; // nodes whose SAT vars are assigned
67 int nRecycles; // the number of times SAT solver was recycled
68 int nCallsSince; // the number of calls since the last recycle
69 Vec_Ptr_t * vFanins; // fanins of the CNF node
70 Vec_Ptr_t * vSimRoots; // the roots of cand const 1 nodes to simulate
71 Vec_Ptr_t * vSimClasses; // the roots of cand equiv classes to simulate
72 // solver cone size
73 int nConeThis;
74 int nConeMax;
75 // SAT calls statistics
76 int nSatCalls; // the number of SAT calls
77 int nSatProof; // the number of proofs
78 int nSatFailsReal; // the number of timeouts
79 int nSatCallsUnsat; // the number of unsat SAT calls
80 int nSatCallsSat; // the number of sat SAT calls
81 // choice node statistics
82 int nLits; // the number of lits in the cand equiv classes
83 int nReprs; // the number of proved equivalent pairs
84 int nEquivs; // the number of final equivalences
85 int nChoices; // the number of final choice nodes
86 // runtime stats
87 abctime timeSimInit; // simulation and class computation
88 abctime timeSimSat; // simulation of the counter-examples
89 abctime timeSat; // solving SAT
90 abctime timeSatSat; // sat
91 abctime timeSatUnsat; // unsat
92 abctime timeSatUndec; // undecided
93 abctime timeChoice; // choice computation
94 abctime timeOther; // other runtime
95 abctime timeTotal; // total runtime
96 };
97
98 ////////////////////////////////////////////////////////////////////////
99 /// MACRO DEFINITIONS ///
100 ////////////////////////////////////////////////////////////////////////
101
Dch_ObjSatNum(Dch_Man_t * p,Aig_Obj_t * pObj)102 static inline int Dch_ObjSatNum( Dch_Man_t * p, Aig_Obj_t * pObj ) { return p->pSatVars[pObj->Id]; }
Dch_ObjSetSatNum(Dch_Man_t * p,Aig_Obj_t * pObj,int Num)103 static inline void Dch_ObjSetSatNum( Dch_Man_t * p, Aig_Obj_t * pObj, int Num ) { p->pSatVars[pObj->Id] = Num; }
104
Dch_ObjFraig(Aig_Obj_t * pObj)105 static inline Aig_Obj_t * Dch_ObjFraig( Aig_Obj_t * pObj ) { return (Aig_Obj_t *)pObj->pData; }
Dch_ObjSetFraig(Aig_Obj_t * pObj,Aig_Obj_t * pNode)106 static inline void Dch_ObjSetFraig( Aig_Obj_t * pObj, Aig_Obj_t * pNode ) { pObj->pData = pNode; }
107
Dch_ObjIsConst1Cand(Aig_Man_t * pAig,Aig_Obj_t * pObj)108 static inline int Dch_ObjIsConst1Cand( Aig_Man_t * pAig, Aig_Obj_t * pObj )
109 {
110 return Aig_ObjRepr(pAig, pObj) == Aig_ManConst1(pAig);
111 }
Dch_ObjSetConst1Cand(Aig_Man_t * pAig,Aig_Obj_t * pObj)112 static inline void Dch_ObjSetConst1Cand( Aig_Man_t * pAig, Aig_Obj_t * pObj )
113 {
114 assert( !Dch_ObjIsConst1Cand( pAig, pObj ) );
115 Aig_ObjSetRepr( pAig, pObj, Aig_ManConst1(pAig) );
116 }
117
118 ////////////////////////////////////////////////////////////////////////
119 /// FUNCTION DECLARATIONS ///
120 ////////////////////////////////////////////////////////////////////////
121
122 /*=== dchAig.c ===================================================*/
123 /*=== dchChoice.c ===================================================*/
124 extern int Dch_DeriveChoiceCountReprs( Aig_Man_t * pAig );
125 extern int Dch_DeriveChoiceCountEquivs( Aig_Man_t * pAig );
126 extern Aig_Man_t * Dch_DeriveChoiceAig( Aig_Man_t * pAig, int fSkipRedSupps );
127 /*=== dchClass.c =================================================*/
128 extern Dch_Cla_t * Dch_ClassesStart( Aig_Man_t * pAig );
129 extern void Dch_ClassesSetData( Dch_Cla_t * p, void * pManData,
130 unsigned (*pFuncNodeHash)(void *,Aig_Obj_t *),
131 int (*pFuncNodeIsConst)(void *,Aig_Obj_t *),
132 int (*pFuncNodesAreEqual)(void *,Aig_Obj_t *, Aig_Obj_t *) );
133 extern void Dch_ClassesStop( Dch_Cla_t * p );
134 extern int Dch_ClassesLitNum( Dch_Cla_t * p );
135 extern Aig_Obj_t ** Dch_ClassesReadClass( Dch_Cla_t * p, Aig_Obj_t * pRepr, int * pnSize );
136 extern void Dch_ClassesPrint( Dch_Cla_t * p, int fVeryVerbose );
137 extern void Dch_ClassesPrepare( Dch_Cla_t * p, int fLatchCorr, int nMaxLevs );
138 extern int Dch_ClassesRefine( Dch_Cla_t * p );
139 extern int Dch_ClassesRefineOneClass( Dch_Cla_t * p, Aig_Obj_t * pRepr, int fRecursive );
140 extern void Dch_ClassesCollectOneClass( Dch_Cla_t * p, Aig_Obj_t * pRepr, Vec_Ptr_t * vRoots );
141 extern void Dch_ClassesCollectConst1Group( Dch_Cla_t * p, Aig_Obj_t * pObj, int nNodes, Vec_Ptr_t * vRoots );
142 extern int Dch_ClassesRefineConst1Group( Dch_Cla_t * p, Vec_Ptr_t * vRoots, int fRecursive );
143 /*=== dchCnf.c ===================================================*/
144 extern void Dch_CnfNodeAddToSolver( Dch_Man_t * p, Aig_Obj_t * pObj );
145 /*=== dchMan.c ===================================================*/
146 extern Dch_Man_t * Dch_ManCreate( Aig_Man_t * pAig, Dch_Pars_t * pPars );
147 extern void Dch_ManStop( Dch_Man_t * p );
148 extern void Dch_ManSatSolverRecycle( Dch_Man_t * p );
149 /*=== dchSat.c ===================================================*/
150 extern int Dch_NodesAreEquiv( Dch_Man_t * p, Aig_Obj_t * pObj1, Aig_Obj_t * pObj2 );
151 /*=== dchSim.c ===================================================*/
152 extern Dch_Cla_t * Dch_CreateCandEquivClasses( Aig_Man_t * pAig, int nWords, int fVerbose );
153 /*=== dchSimSat.c ===================================================*/
154 extern void Dch_ManResimulateCex( Dch_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr );
155 extern void Dch_ManResimulateCex2( Dch_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr );
156 /*=== dchSweep.c ===================================================*/
157 extern void Dch_ManSweep( Dch_Man_t * p );
158
159
160
161 ABC_NAMESPACE_HEADER_END
162
163
164
165 #endif
166
167 ////////////////////////////////////////////////////////////////////////
168 /// END OF FILE ///
169 ////////////////////////////////////////////////////////////////////////
170
171