abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
llbInt.h
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [llbInt.h]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [BDD-based reachability.]
8 
9  Synopsis [External declarations.]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - May 8, 2010.]
16 
17  Revision [$Id: llbInt.h,v 1.00 2010/05/08 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #ifndef ABC__aig__llb__llbInt_h
22 #define ABC__aig__llb__llbInt_h
23 
24 
25 ////////////////////////////////////////////////////////////////////////
26 /// INCLUDES ///
27 ////////////////////////////////////////////////////////////////////////
28 
29 #include <stdio.h>
30 #include "aig/aig/aig.h"
31 #include "aig/saig/saig.h"
32 #include "proof/ssw/ssw.h"
33 #include "misc/extra/extraBdd.h"
34 #include "llb.h"
35 
36 ////////////////////////////////////////////////////////////////////////
37 /// PARAMETERS ///
38 ////////////////////////////////////////////////////////////////////////
39 
41 
42 ////////////////////////////////////////////////////////////////////////
43 /// BASIC TYPES ///
44 ////////////////////////////////////////////////////////////////////////
45 
46 typedef struct Llb_Man_t_ Llb_Man_t;
47 typedef struct Llb_Mtr_t_ Llb_Mtr_t;
48 typedef struct Llb_Grp_t_ Llb_Grp_t;
49 
50 struct Llb_Man_t_
51 {
52  Gia_ParLlb_t * pPars; // parameters
53  Aig_Man_t * pAigGlo; // initial AIG manager (owned by the caller)
54  Aig_Man_t * pAig; // derived AIG manager (created in this package)
55  DdManager * dd; // BDD manager
56  DdManager * ddG; // BDD manager
57  DdManager * ddR; // BDD manager
58  Vec_Int_t * vObj2Var; // mapping AIG ObjId into BDD var index
59  Vec_Int_t * vVar2Obj; // mapping BDD var index into AIG ObjId
60  Vec_Ptr_t * vGroups; // group Id into group pointer
61  Llb_Mtr_t * pMatrix; // dependency matrix
62  // image computation
63  Vec_Ptr_t * vRings; // onion rings
64  Vec_Int_t * vVarBegs; // the first group where the var appears
65  Vec_Int_t * vVarEnds; // the last group where the var appears
66  // variable mapping
67  Vec_Int_t * vNs2Glo; // next state variables into global variables
68  Vec_Int_t * vCs2Glo; // next state variables into global variables
69  Vec_Int_t * vGlo2Cs; // global variables into current state variables
70  Vec_Int_t * vGlo2Ns; // global variables into current state variables
71  // flow computation
72 // Vec_Int_t * vMem;
73 // Vec_Ptr_t * vTops;
74 // Vec_Ptr_t * vBots;
75 // Vec_Ptr_t * vCuts;
76 };
77 
78 struct Llb_Mtr_t_
79 {
80  int nPis; // number of primary inputs
81  int nFfs; // number of flip-flops
82  int nRows; // number of rows
83  int nCols; // number of columns
84  int * pColSums; // sum of values in a column
85  Llb_Grp_t ** pColGrps; // group structure for each col
86  int * pRowSums; // sum of values in a row
87  char ** pMatrix; // dependency matrix
88  Llb_Man_t * pMan; // manager
89  // partial product
90  char * pProdVars; // variables in the partial product
91  int * pProdNums; // var counts in the remaining partitions
92 };
93 
94 struct Llb_Grp_t_
95 {
96  int Id; // group ID
97  Vec_Ptr_t * vIns; // input AIG objs
98  Vec_Ptr_t * vOuts; // output AIG objs
99  Vec_Ptr_t * vNodes; // internal AIG objs
100  Llb_Man_t * pMan; // manager
101  Llb_Grp_t * pPrev; // previous group
102  Llb_Grp_t * pNext; // next group
103 };
104 
105 ////////////////////////////////////////////////////////////////////////
106 /// MACRO DEFINITIONS ///
107 ////////////////////////////////////////////////////////////////////////
108 
109 static inline int Llb_ObjBddVar( Vec_Int_t * vOrder, Aig_Obj_t * pObj ) { return Vec_IntEntry(vOrder, Aig_ObjId(pObj)); }
110 
111 ////////////////////////////////////////////////////////////////////////
112 /// FUNCTION DECLARATIONS ///
113 ////////////////////////////////////////////////////////////////////////
114 
115 /*=== llbConstr.c ======================================================*/
117 extern void Llb_ManPrintEntries( Aig_Man_t * p, Vec_Int_t * vCands );
118 /*=== llbCore.c ======================================================*/
119 extern int Llb_ManModelCheckAig( Aig_Man_t * pAigGlo, Gia_ParLlb_t * pPars, Vec_Int_t * vHints, DdManager ** pddGlo );
120 /*=== llbCluster.c ======================================================*/
121 extern void Llb_ManCluster( Llb_Mtr_t * p );
122 /*=== llbDump.c ======================================================*/
123 extern void Llb_ManDumpReached( DdManager * ddG, DdNode * bReached, char * pModel, char * pFileName );
124 /*=== llbFlow.c ======================================================*/
125 extern Vec_Ptr_t * Llb_ManFlow( Aig_Man_t * p, Vec_Ptr_t * vSources, int * pnFlow );
126 /*=== llbHint.c ======================================================*/
128 extern int Llb_ManModelCheckAigWithHints( Aig_Man_t * pAigGlo, Gia_ParLlb_t * pPars );
129 /*=== llbMan.c =======================================================*/
130 extern void Llb_ManPrepareVarMap( Llb_Man_t * p );
131 extern Llb_Man_t * Llb_ManStart( Aig_Man_t * pAigGlo, Aig_Man_t * pAig, Gia_ParLlb_t * pPars );
132 extern void Llb_ManStop( Llb_Man_t * p );
133 /*=== llbMatrix.c ====================================================*/
134 extern void Llb_MtrVerifyMatrix( Llb_Mtr_t * p );
135 extern Llb_Mtr_t * Llb_MtrCreate( Llb_Man_t * p );
136 extern void Llb_MtrFree( Llb_Mtr_t * p );
137 extern void Llb_MtrPrint( Llb_Mtr_t * p, int fOrder );
138 extern void Llb_MtrPrintMatrixStats( Llb_Mtr_t * p );
139 /*=== llbPart.c ======================================================*/
140 extern Llb_Grp_t * Llb_ManGroupAlloc( Llb_Man_t * pMan );
141 extern void Llb_ManGroupStop( Llb_Grp_t * p );
142 extern void Llb_ManPrepareGroups( Llb_Man_t * pMan );
143 extern Llb_Grp_t * Llb_ManGroupsCombine( Llb_Grp_t * p1, Llb_Grp_t * p2 );
144 extern Llb_Grp_t * Llb_ManGroupCreateFromCuts( Llb_Man_t * pMan, Vec_Int_t * vCut1, Vec_Int_t * vCut2 );
145 extern void Llb_ManPrepareVarLimits( Llb_Man_t * p );
146 /*=== llbPivot.c =====================================================*/
147 extern int Llb_ManTracePaths( Aig_Man_t * p, Aig_Obj_t * pPivot );
148 extern Vec_Int_t * Llb_ManMarkPivotNodes( Aig_Man_t * p, int fUseInternal );
149 /*=== llbReach.c =====================================================*/
150 extern int Llb_ManReachability( Llb_Man_t * p, Vec_Int_t * vHints, DdManager ** pddGlo );
151 /*=== llbSched.c =====================================================*/
152 extern void Llb_MtrSchedule( Llb_Mtr_t * p );
153 
154 /*=== llb2Bad.c ======================================================*/
155 extern DdNode * Llb_BddComputeBad( Aig_Man_t * pInit, DdManager * dd, abctime TimeOut );
156 extern DdNode * Llb_BddQuantifyPis( Aig_Man_t * pInit, DdManager * dd, DdNode * bFunc );
157 /*=== llb2Core.c ======================================================*/
158 extern DdNode * Llb_CoreComputeCube( DdManager * dd, Vec_Int_t * vVars, int fUseVarIndex, char * pValues );
159 extern int Llb_CoreExperiment( Aig_Man_t * pInit, Aig_Man_t * pAig, Gia_ParLlb_t * pPars, Vec_Ptr_t * vResult, abctime TimeTarget );
160 /*=== llb2Driver.c ======================================================*/
162 extern Vec_Int_t * Llb_DriverCollectNs( Aig_Man_t * pAig, Vec_Int_t * vDriRefs );
163 extern Vec_Int_t * Llb_DriverCollectCs( Aig_Man_t * pAig );
164 extern DdNode * Llb_DriverPhaseCube( Aig_Man_t * pAig, Vec_Int_t * vDriRefs, DdManager * dd );
165 extern DdManager * Llb_DriverLastPartition( Aig_Man_t * p, Vec_Int_t * vVarsNs, abctime TimeTarget );
166 /*=== llb2Image.c ======================================================*/
167 extern Vec_Ptr_t * Llb_ImgSupports( Aig_Man_t * p, Vec_Ptr_t * vDdMans, Vec_Int_t * vStart, Vec_Int_t * vStop, int fAddPis, int fVerbose );
168 extern void Llb_ImgSchedule( Vec_Ptr_t * vSupps, Vec_Ptr_t ** pvQuant0, Vec_Ptr_t ** pvQuant1, int fVerbose );
169 extern DdManager * Llb_ImgPartition( Aig_Man_t * p, Vec_Ptr_t * vLower, Vec_Ptr_t * vUpper, abctime TimeTarget );
170 extern void Llb_ImgQuantifyFirst( Aig_Man_t * pAig, Vec_Ptr_t * vDdMans, Vec_Ptr_t * vQuant0, int fVerbose );
171 extern void Llb_ImgQuantifyReset( Vec_Ptr_t * vDdMans );
172 extern DdNode * Llb_ImgComputeImage( Aig_Man_t * pAig, Vec_Ptr_t * vDdMans, DdManager * dd, DdNode * bInit,
173  Vec_Ptr_t * vQuant0, Vec_Ptr_t * vQuant1, Vec_Int_t * vDriRefs,
174  abctime TimeTarget, int fBackward, int fReorder, int fVerbose );
175 
176 extern DdManager * Llb_NonlinImageStart( Aig_Man_t * pAig, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vRoots, int * pVars2Q, int * pOrder, int fFirst, abctime TimeTarget );
177 extern DdNode * Llb_NonlinImageCompute( DdNode * bCurrent, int fReorder, int fDrop, int fVerbose, int * pOrder );
178 extern void Llb_NonlinImageQuit();
179 
180 /*=== llb3Image.c =======================================================*/
181 extern DdNode * Llb_NonlinImage( Aig_Man_t * pAig, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vRoots, int * pVars2Q,
182  DdManager * dd, DdNode * bCurrent, int fReorder, int fVerbose, int * pOrder );
183 /*=== llb3Nonlin.c ======================================================*/
184 extern DdNode * Llb_NonlinComputeInitState( Aig_Man_t * pAig, DdManager * dd );
185 
186 
187 /*=== llb4Cex.c =======================================================*/
188 extern Abc_Cex_t * Llb4_Nonlin4TransformCex( Aig_Man_t * pAig, Vec_Ptr_t * vStates, int iCexPo, int fVerbose );
189 /*=== llb4Cluster.c =======================================================*/
190 //extern void Llb_Nonlin4Cluster( Aig_Man_t * pAig, DdManager ** pdd, Vec_Int_t ** pvOrder, Vec_Ptr_t ** pvGroups, int nBddMax, int fVerbose );
191 /*=== llb4Image.c =======================================================*/
192 extern DdNode * Llb_Nonlin4Image( DdManager * dd, Vec_Ptr_t * vParts, DdNode * bCurrent, Vec_Int_t * vVars2Q );
193 extern Vec_Ptr_t * Llb_Nonlin4Group( DdManager * dd, Vec_Ptr_t * vParts, Vec_Int_t * vVars2Q, int nSizeMax );
194 /*=== llb4Map.c =========================================================*/
195 //extern Vec_Int_t * Llb_AigMap( Aig_Man_t * pAig, int nLutSize, int nLutMin );
196 /*=== llb4Nonlin.c ======================================================*/
197 //extern int Llb_Nonlin4CoreReach( Aig_Man_t * pAig, Gia_ParLlb_t * pPars );
198 /*=== llb4Sweep.c ======================================================*/
199 extern void Llb4_Nonlin4Sweep( Aig_Man_t * pAig, int nSweepMax, int nClusterMax, DdManager ** pdd, Vec_Int_t ** pvOrder, Vec_Ptr_t ** pvGroups, int fVerbose );
200 
201 
203 
204 
205 
206 #endif
207 
208 ////////////////////////////////////////////////////////////////////////
209 /// END OF FILE ///
210 ////////////////////////////////////////////////////////////////////////
211 
DdNode * Llb_CoreComputeCube(DdManager *dd, Vec_Int_t *vVars, int fUseVarIndex, char *pValues)
FUNCTION DEFINITIONS ///.
Definition: llb2Core.c:68
DdNode * Llb_NonlinComputeInitState(Aig_Man_t *pAig, DdManager *dd)
Definition: llb3Nonlin.c:214
Vec_Int_t * vCs2Glo
Definition: llbInt.h:68
void Llb_ManPrepareGroups(Llb_Man_t *pMan)
Definition: llb1Group.c:356
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
Vec_Int_t * vVarBegs
Definition: llbInt.h:64
Llb_Man_t * pMan
Definition: llbInt.h:88
Llb_Man_t * pMan
Definition: llbInt.h:100
DdManager * dd
Definition: llbInt.h:55
Llb_Grp_t * pPrev
Definition: llbInt.h:101
Definition: cudd.h:278
Aig_Man_t * pAig
Definition: llbInt.h:54
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition: aig.h:50
static Llb_Mgr_t * p
Definition: llb3Image.c:950
void Llb_MtrPrint(Llb_Mtr_t *p, int fOrder)
Definition: llb1Matrix.c:206
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
int * pProdNums
Definition: llbInt.h:91
Vec_Int_t * vGlo2Cs
Definition: llbInt.h:69
Vec_Ptr_t * vRings
Definition: llbInt.h:63
Vec_Ptr_t * vNodes
Definition: llbInt.h:99
void Llb_ManPrepareVarLimits(Llb_Man_t *p)
Definition: llb1Man.c:88
DdNode * Llb_ImgComputeImage(Aig_Man_t *pAig, Vec_Ptr_t *vDdMans, DdManager *dd, DdNode *bInit, Vec_Ptr_t *vQuant0, Vec_Ptr_t *vQuant1, Vec_Int_t *vDriRefs, abctime TimeTarget, int fBackward, int fReorder, int fVerbose)
Definition: llb2Image.c:364
Vec_Int_t * Llb_ManDeriveConstraints(Aig_Man_t *p)
FUNCTION DECLARATIONS ///.
Definition: llb1Constr.c:267
Vec_Ptr_t * Llb_Nonlin4Group(DdManager *dd, Vec_Ptr_t *vParts, Vec_Int_t *vVars2Q, int nSizeMax)
Definition: llb4Image.c:806
void Llb_ManDumpReached(DdManager *ddG, DdNode *bReached, char *pModel, char *pFileName)
Definition: llb2Dump.c:63
typedefABC_NAMESPACE_HEADER_START struct Gia_ParLlb_t_ Gia_ParLlb_t
INCLUDES ///.
Definition: llb.h:41
void Llb_ManGroupStop(Llb_Grp_t *p)
Definition: llb1Group.c:68
DdManager * Llb_NonlinImageStart(Aig_Man_t *pAig, Vec_Ptr_t *vLeaves, Vec_Ptr_t *vRoots, int *pVars2Q, int *pOrder, int fFirst, abctime TimeTarget)
Definition: llb3Image.c:963
int * pRowSums
Definition: llbInt.h:86
void Llb_NonlinImageQuit()
Definition: llb3Image.c:1075
void Llb_ManStop(Llb_Man_t *p)
Definition: llb1Man.c:130
Vec_Int_t * Llb_DriverCollectNs(Aig_Man_t *pAig, Vec_Int_t *vDriRefs)
Definition: llb2Driver.c:78
DdManager * ddR
Definition: llbInt.h:57
Vec_Ptr_t * vGroups
Definition: llbInt.h:60
Vec_Int_t * Llb_DriverCountRefs(Aig_Man_t *p)
DECLARATIONS ///.
Definition: llb2Driver.c:56
void Llb_ManPrintEntries(Aig_Man_t *p, Vec_Int_t *vCands)
Definition: llb1Constr.c:64
DdManager * Llb_ImgPartition(Aig_Man_t *p, Vec_Ptr_t *vLower, Vec_Ptr_t *vUpper, abctime TimeTarget)
Definition: llb2Image.c:183
int Llb_ManTracePaths(Aig_Man_t *p, Aig_Obj_t *pPivot)
Definition: llb1Pivot.c:81
DdNode * Llb_NonlinImageCompute(DdNode *bCurrent, int fReorder, int fDrop, int fVerbose, int *pOrder)
Definition: llb3Image.c:999
Llb_Mtr_t * pMatrix
Definition: llbInt.h:61
DdManager * Llb_DriverLastPartition(Aig_Man_t *p, Vec_Int_t *vVarsNs, abctime TimeTarget)
Definition: llb2Driver.c:163
DdNode * Llb_NonlinImage(Aig_Man_t *pAig, Vec_Ptr_t *vLeaves, Vec_Ptr_t *vRoots, int *pVars2Q, DdManager *dd, DdNode *bCurrent, int fReorder, int fVerbose, int *pOrder)
Definition: llb3Image.c:884
int nPis
Definition: llbInt.h:80
int Llb_ManReachabilityWithHints(Llb_Man_t *p)
DdNode * Llb_DriverPhaseCube(Aig_Man_t *pAig, Vec_Int_t *vDriRefs, DdManager *dd)
Definition: llb2Driver.c:128
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
Llb_Grp_t * Llb_ManGroupAlloc(Llb_Man_t *pMan)
DECLARATIONS ///.
Definition: llb1Group.c:45
char ** pMatrix
Definition: llbInt.h:87
Gia_ParLlb_t * pPars
Definition: llbInt.h:52
Definition: aig.h:69
#define ABC_NAMESPACE_HEADER_START
NAMESPACES ///.
Definition: abc_global.h:105
void Llb_ImgQuantifyReset(Vec_Ptr_t *vDdMans)
Definition: llb2Image.c:340
Vec_Int_t * vNs2Glo
Definition: llbInt.h:67
int nCols
Definition: llbInt.h:83
Llb_Grp_t * Llb_ManGroupsCombine(Llb_Grp_t *p1, Llb_Grp_t *p2)
Definition: llb1Group.c:251
Vec_Ptr_t * Llb_ImgSupports(Aig_Man_t *p, Vec_Ptr_t *vDdMans, Vec_Int_t *vStart, Vec_Int_t *vStop, int fAddPis, int fVerbose)
FUNCTION DEFINITIONS ///.
Definition: llb2Image.c:48
#define ABC_NAMESPACE_HEADER_END
Definition: abc_global.h:106
void Llb4_Nonlin4Sweep(Aig_Man_t *pAig, int nSweepMax, int nClusterMax, DdManager **pdd, Vec_Int_t **pvOrder, Vec_Ptr_t **pvGroups, int fVerbose)
Definition: llb4Sweep.c:520
Vec_Int_t * Llb_ManMarkPivotNodes(Aig_Man_t *p, int fUseInternal)
Definition: llb1Pivot.c:220
void Llb_ImgQuantifyFirst(Aig_Man_t *pAig, Vec_Ptr_t *vDdMans, Vec_Ptr_t *vQuant0, int fVerbose)
Definition: llb2Image.c:288
DdManager * ddG
Definition: llbInt.h:56
static int Llb_ObjBddVar(Vec_Int_t *vOrder, Aig_Obj_t *pObj)
MACRO DEFINITIONS ///.
Definition: llbInt.h:109
int Llb_ManModelCheckAigWithHints(Aig_Man_t *pAigGlo, Gia_ParLlb_t *pPars)
Definition: llb1Hint.c:162
int nFfs
Definition: llbInt.h:81
Vec_Int_t * vObj2Var
Definition: llbInt.h:58
int Llb_CoreExperiment(Aig_Man_t *pInit, Aig_Man_t *pAig, Gia_ParLlb_t *pPars, Vec_Ptr_t *vResult, abctime TimeTarget)
Definition: llb2Core.c:694
DdNode * Llb_Nonlin4Image(DdManager *dd, Vec_Ptr_t *vParts, DdNode *bCurrent, Vec_Int_t *vVars2Q)
Definition: llb4Image.c:752
void Llb_MtrVerifyMatrix(Llb_Mtr_t *p)
Definition: llb1Matrix.c:115
Vec_Int_t * vGlo2Ns
Definition: llbInt.h:70
void Llb_MtrSchedule(Llb_Mtr_t *p)
Definition: llb1Sched.c:222
Llb_Man_t * Llb_ManStart(Aig_Man_t *pAigGlo, Aig_Man_t *pAig, Gia_ParLlb_t *pPars)
Definition: llb1Man.c:193
Llb_Grp_t * Llb_ManGroupCreateFromCuts(Llb_Man_t *pMan, Vec_Int_t *vCut1, Vec_Int_t *vCut2)
Definition: llb1Group.c:312
int Llb_ManReachability(Llb_Man_t *p, Vec_Int_t *vHints, DdManager **pddGlo)
Definition: llb1Reach.c:582
Abc_Cex_t * Llb4_Nonlin4TransformCex(Aig_Man_t *pAig, Vec_Ptr_t *vStates, int iCexPo, int fVerbose)
DECLARATIONS ///.
Definition: llb4Cex.c:47
Aig_Man_t * pAigGlo
Definition: llbInt.h:53
int Llb_ManModelCheckAig(Aig_Man_t *pAigGlo, Gia_ParLlb_t *pPars, Vec_Int_t *vHints, DdManager **pddGlo)
Definition: llb1Core.c:112
Vec_Int_t * vVarEnds
Definition: llbInt.h:65
Vec_Ptr_t * Llb_ManFlow(Aig_Man_t *p, Vec_Ptr_t *vSources, int *pnFlow)
Definition: llb2Flow.c:762
static int Aig_ObjId(Aig_Obj_t *pObj)
Definition: aig.h:286
DdNode * Llb_BddQuantifyPis(Aig_Man_t *pInit, DdManager *dd, DdNode *bFunc)
Definition: llb2Bad.c:109
int Id
Definition: llbInt.h:96
void Llb_ImgSchedule(Vec_Ptr_t *vSupps, Vec_Ptr_t **pvQuant0, Vec_Ptr_t **pvQuant1, int fVerbose)
Definition: llb2Image.c:122
typedefABC_NAMESPACE_HEADER_START struct Abc_Cex_t_ Abc_Cex_t
INCLUDES ///.
Definition: utilCex.h:39
Vec_Int_t * vVar2Obj
Definition: llbInt.h:59
Vec_Int_t * Llb_DriverCollectCs(Aig_Man_t *pAig)
Definition: llb2Driver.c:106
Llb_Grp_t * pNext
Definition: llbInt.h:102
Llb_Mtr_t * Llb_MtrCreate(Llb_Man_t *p)
Definition: llb1Matrix.c:410
int nRows
Definition: llbInt.h:82
char * pProdVars
Definition: llbInt.h:90
ABC_INT64_T abctime
Definition: abc_global.h:278
int * pColSums
Definition: llbInt.h:84
Llb_Grp_t ** pColGrps
Definition: llbInt.h:85
typedefABC_NAMESPACE_HEADER_START struct Llb_Man_t_ Llb_Man_t
INCLUDES ///.
Definition: llbInt.h:46
Vec_Ptr_t * vOuts
Definition: llbInt.h:98
void Llb_MtrFree(Llb_Mtr_t *p)
Definition: llb1Matrix.c:321
Vec_Ptr_t * vIns
Definition: llbInt.h:97
void Llb_MtrPrintMatrixStats(Llb_Mtr_t *p)
Definition: llb1Matrix.c:236
DdNode * Llb_BddComputeBad(Aig_Man_t *pInit, DdManager *dd, abctime TimeOut)
DECLARATIONS ///.
Definition: llb2Bad.c:45
void Llb_ManPrepareVarMap(Llb_Man_t *p)
DECLARATIONS ///.
Definition: llb1Man.c:45
void Llb_ManCluster(Llb_Mtr_t *p)
Definition: llb1Cluster.c:324