ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
fra.h
Go to the documentation of this file.
1
20
21#ifndef ABC__aig__fra__fra_h
22#define ABC__aig__fra__fra_h
23
24
28
29#include <stdio.h>
30#include <stdlib.h>
31#include <string.h>
32#include <assert.h>
33
34#include "misc/vec/vec.h"
35#include "aig/aig/aig.h"
36#include "opt/dar/dar.h"
37#include "sat/bsat/satSolver.h"
38#include "aig/ioa/ioa.h"
39
43
44
45
46ABC_NAMESPACE_HEADER_START
47
48
52
53typedef struct Fra_Par_t_ Fra_Par_t;
54typedef struct Fra_Ssw_t_ Fra_Ssw_t;
55typedef struct Fra_Sec_t_ Fra_Sec_t;
56typedef struct Fra_Man_t_ Fra_Man_t;
57typedef struct Fra_Cla_t_ Fra_Cla_t;
58typedef struct Fra_Sml_t_ Fra_Sml_t;
59typedef struct Fra_Bmc_t_ Fra_Bmc_t;
60
61// FRAIG parameters
62struct Fra_Par_t_
63{
64 int nSimWords; // the number of words in the simulation info
65 double dSimSatur; // the ratio of refined classes when saturation is reached
66 int fPatScores; // enables simulation pattern scoring
67 int MaxScore; // max score after which resimulation is used
68 double dActConeRatio; // the ratio of cone to be bumped
69 double dActConeBumpMax; // the largest bump in activity
70 int fChoicing; // enables choicing
71 int fSpeculate; // use speculative reduction
72 int fProve; // prove the miter outputs
73 int fVerbose; // verbose output
74 int fDoSparse; // skip sparse functions
75 int fConeBias; // bias variables in the cone (good for unsat runs)
76 int nBTLimitNode; // conflict limit at a node
77 int nBTLimitMiter; // conflict limit at an output
78 int nLevelMax; // the max level to consider seriously
79 int nFramesP; // the number of timeframes to in the prefix
80 int nFramesK; // the number of timeframes to unroll
81 int nMaxImps; // the maximum number of implications to consider
82 int nMaxLevs; // the maximum number of levels to consider
83 int fRewrite; // use rewriting for constraint reduction
84 int fLatchCorr; // computes latch correspondence only
85 int fUseImps; // use implications
86 int fUse1Hot; // use one-hotness conditions
87 int fWriteImps; // record implications
88 int fDontShowBar; // does not show progressbar during fraiging
89};
90
91// seq SAT sweeping parameters
92struct Fra_Ssw_t_
93{
94 int nPartSize; // size of the partition
95 int nOverSize; // size of the overlap between partitions
96 int nFramesP; // number of frames in the prefix
97 int nFramesK; // number of frames for induction (1=simple)
98 int nMaxImps; // max implications to consider
99 int nMaxLevs; // max levels to consider
100 int nMinDomSize; // min clock domain considered for optimization
101 int fUseImps; // use implications
102 int fRewrite; // enable rewriting of the specualatively reduced model
103 int fFraiging; // enable comb SAT sweeping as preprocessing
104 int fLatchCorr; // perform register correspondence
105 int fWriteImps; // write implications into a file
106 int fUse1Hot; // use one-hotness constraints
107 int fVerbose; // enable verbose output
108 int fSilent; // disable any output
109 int nIters; // the number of iterations performed
110 float TimeLimit; // the runtime budget for this call
111};
112
113// SEC parametesr
114struct Fra_Sec_t_
115{
116 int fTryComb; // try CEC call as a preprocessing step
117 int fTryBmc; // try BMC call as a preprocessing step
118 int nFramesMax; // the max number of frames used for induction
119 int nBTLimit; // the conflict limit at a node
120 int nBTLimitGlobal; // the global conflict limit
121 int nBTLimitInter; // the conflict limit for interpolation
122 int nBddVarsMax; // the state space limit for BDD reachability
123 int nBddMax; // the max number of BDD nodes
124 int nBddIterMax; // the limit on the number of BDD iterations
125 int nPdrTimeout; // the timeout for PDR in the end
126 int fPhaseAbstract; // enables phase abstraction
127 int fRetimeFirst; // enables most-forward retiming at the beginning
128 int fRetimeRegs; // enables min-register retiming at the beginning
129 int fFraiging; // enables fraiging at the beginning
130 int fInduction; // enable the use of induction
131 int fInterpolation; // enables interpolation
132 int fInterSeparate; // enables interpolation for each outputs separately
133 int fReachability; // enables BDD based reachability
134 int fReorderImage; // enables BDD reordering during image computation
135 int fStopOnFirstFail; // enables stopping after first output of a miter has failed to prove
136 int fUseNewProver; // the new prover
137 int fUsePdr; // the PDR
138 int fSilent; // disables all output
139 int fVerbose; // enables verbose reporting of statistics
140 int fVeryVerbose; // enables very verbose reporting
141 int TimeLimit; // enables the timeout
142 int fReadUnsolved; // inserts the unsolved model back
143 int nSMnumber; // the number of model written
144 // internal parameters
145 int fRecursive; // set to 1 when SEC is called recursively
146 int fReportSolution; // enables report solution in a special form
147};
148
149// FRAIG equivalence classes
150struct Fra_Cla_t_
151{
152 Aig_Man_t * pAig; // the original AIG manager
153 Aig_Obj_t ** pMemRepr; // pointers to representatives of each node
154 Vec_Ptr_t * vClasses; // equivalence classes
155 Vec_Ptr_t * vClasses1; // equivalence class of Const1 node
156 Vec_Ptr_t * vClassesTemp; // temporary storage for new classes
157 Aig_Obj_t ** pMemClasses; // memory allocated for equivalence classes
158 Aig_Obj_t ** pMemClassesFree; // memory allocated for equivalence classes to be used
159 Vec_Ptr_t * vClassOld; // old equivalence class after splitting
160 Vec_Ptr_t * vClassNew; // new equivalence class(es) after splitting
161 int nPairs; // the number of pairs of nodes
162 int fRefinement; // set to 1 when refinement has happened
163 Vec_Int_t * vImps; // implications
164 // procedures used for class refinement
165 int (*pFuncNodeHash) (Aig_Obj_t *, int); // returns has key of the node
166 int (*pFuncNodeIsConst) (Aig_Obj_t *); // returns 1 if the node is a constant
167 int (*pFuncNodesAreEqual)(Aig_Obj_t *, Aig_Obj_t *); // returns 1 if nodes are equal up to a complement
168};
169
170// simulation manager
171struct Fra_Sml_t_
172{
173 Aig_Man_t * pAig; // the original AIG manager
174 int nPref; // the number of times frames in the prefix
175 int nFrames; // the number of times frames
176 int nWordsFrame; // the number of words in each time frame
177 int nWordsTotal; // the total number of words at a node
178 int nWordsPref; // the number of word in the prefix
179 int fNonConstOut; // have seen a non-const-0 output during simulation
180 int nSimRounds; // statistics
181 int timeSim; // statistics
182 unsigned pData[0]; // simulation data for the nodes
183};
184
185// FRAIG manager
186struct Fra_Man_t_
187{
188 // high-level data
189 Fra_Par_t * pPars; // parameters governing fraiging
190 // AIG managers
191 Aig_Man_t * pManAig; // the starting AIG manager
192 Aig_Man_t * pManFraig; // the final AIG manager
193 // mapping AIG into FRAIG
194 int nFramesAll; // the number of timeframes used
195 Aig_Obj_t ** pMemFraig; // memory allocated for points to the fraig nodes
196 int nSizeAlloc; // allocated size of the arrays for timeframe nodes
197 // equivalence classes
198 Fra_Cla_t * pCla; // representation of (candidate) equivalent nodes
199 // simulation info
200 Fra_Sml_t * pSml; // simulation manager
201 // bounded model checking manager
202 Fra_Bmc_t * pBmc;
203 // counter example storage
204 int nPatWords; // the number of words in the counter example
205 unsigned * pPatWords; // the counter example
206 Vec_Int_t * vCex;
207 // one-hotness conditions
208 Vec_Int_t * vOneHots;
209 // satisfiability solving
210 sat_solver * pSat; // SAT solver
211 int nSatVars; // the number of variables currently used
212 Vec_Ptr_t * vPiVars; // the PIs of the cone used
213 ABC_INT64_T nBTLimitGlobal; // resource limit
214 ABC_INT64_T nInsLimitGlobal; // resource limit
215 Vec_Ptr_t ** pMemFanins; // the arrays of fanins for some FRAIG nodes
216 int * pMemSatNums; // the array of SAT numbers for some FRAIG nodes
217 int nMemAlloc; // allocated size of the arrays for FRAIG varnums and fanins
218 Vec_Ptr_t * vTimeouts; // the nodes, for which equivalence checking timed out
219 // statistics
220 int nSimRounds;
221 int nNodesMiter;
222 int nLitsBeg;
223 int nLitsEnd;
224 int nNodesBeg;
225 int nNodesEnd;
226 int nRegsBeg;
227 int nRegsEnd;
228 int nSatCalls;
229 int nSatCallsSat;
230 int nSatCallsUnsat;
231 int nSatProof;
232 int nSatFails;
233 int nSatFailsReal;
234 int nSpeculs;
235 int nChoices;
236 int nChoicesFake;
237 int nSatCallsRecent;
238 int nSatCallsSkipped;
239 // runtime
240 abctime timeSim;
241 abctime timeTrav;
242 abctime timeRwr;
243 abctime timeSat;
244 abctime timeSatUnsat;
245 abctime timeSatSat;
246 abctime timeSatFail;
247 abctime timeRef;
248 abctime timeTotal;
249 abctime time1;
250 abctime time2;
251};
252
256
257static inline unsigned * Fra_ObjSim( Fra_Sml_t * p, int Id ) { return p->pData + p->nWordsTotal * Id; }
258static inline unsigned Fra_ObjRandomSim() { return Aig_ManRandom(0); }
259
260static inline Aig_Obj_t * Fra_ObjFraig( Aig_Obj_t * pObj, int i ) { return ((Fra_Man_t *)pObj->pData)->pMemFraig[((Fra_Man_t *)pObj->pData)->nFramesAll*pObj->Id + i]; }
261static inline void Fra_ObjSetFraig( Aig_Obj_t * pObj, int i, Aig_Obj_t * pNode ) { ((Fra_Man_t *)pObj->pData)->pMemFraig[((Fra_Man_t *)pObj->pData)->nFramesAll*pObj->Id + i] = pNode; }
262
263static inline Vec_Ptr_t * Fra_ObjFaninVec( Aig_Obj_t * pObj ) { return ((Fra_Man_t *)pObj->pData)->pMemFanins[pObj->Id]; }
264static inline void Fra_ObjSetFaninVec( Aig_Obj_t * pObj, Vec_Ptr_t * vFanins ) { ((Fra_Man_t *)pObj->pData)->pMemFanins[pObj->Id] = vFanins; }
265
266static inline int Fra_ObjSatNum( Aig_Obj_t * pObj ) { return ((Fra_Man_t *)pObj->pData)->pMemSatNums[pObj->Id]; }
267static inline void Fra_ObjSetSatNum( Aig_Obj_t * pObj, int Num ) { ((Fra_Man_t *)pObj->pData)->pMemSatNums[pObj->Id] = Num; }
268
269static inline Aig_Obj_t * Fra_ClassObjRepr( Aig_Obj_t * pObj ) { return ((Fra_Man_t *)pObj->pData)->pCla->pMemRepr[pObj->Id]; }
270static inline void Fra_ClassObjSetRepr( Aig_Obj_t * pObj, Aig_Obj_t * pNode ) { ((Fra_Man_t *)pObj->pData)->pCla->pMemRepr[pObj->Id] = pNode; }
271
272static inline Aig_Obj_t * Fra_ObjChild0Fra( Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin0(pObj)? Aig_NotCond(Fra_ObjFraig(Aig_ObjFanin0(pObj),i), Aig_ObjFaninC0(pObj)) : NULL; }
273static inline Aig_Obj_t * Fra_ObjChild1Fra( Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? Aig_NotCond(Fra_ObjFraig(Aig_ObjFanin1(pObj),i), Aig_ObjFaninC1(pObj)) : NULL; }
274
275static inline int Fra_ImpLeft( int Imp ) { return Imp & 0xFFFF; }
276static inline int Fra_ImpRight( int Imp ) { return Imp >> 16; }
277static inline int Fra_ImpCreate( int Left, int Right ) { return (Right << 16) | Left; }
278
282
286
287/*=== fraCec.c ========================================================*/
288extern int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int nLearnedStart, int nLearnedDelta, int nLearnedPerce, int fFlipBits, int fAndOuts, int fNewSolver, int fVerbose );
289extern int Fra_FraigCec( Aig_Man_t ** ppAig, int nConfLimit, int fVerbose );
290extern int Fra_FraigCecPartitioned( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nConfLimit, int nPartSize, int fSmart, int fVerbose );
291/*=== fraClass.c ========================================================*/
292extern int Fra_BmcNodeIsConst( Aig_Obj_t * pObj );
293extern int Fra_BmcNodesAreEqual( Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 );
294extern void Fra_BmcStop( Fra_Bmc_t * p );
295extern void Fra_BmcPerform( Fra_Man_t * p, int nPref, int nDepth );
296extern void Fra_BmcPerformSimple( Aig_Man_t * pAig, int nFrames, int nBTLimit, int fRewrite, int fVerbose );
297/*=== fraClass.c ========================================================*/
298extern Fra_Cla_t * Fra_ClassesStart( Aig_Man_t * pAig );
299extern void Fra_ClassesStop( Fra_Cla_t * p );
300extern void Fra_ClassesCopyReprs( Fra_Cla_t * p, Vec_Ptr_t * vFailed );
301extern void Fra_ClassesPrint( Fra_Cla_t * p, int fVeryVerbose );
302extern void Fra_ClassesPrepare( Fra_Cla_t * p, int fLatchCorr, int nMaxLevs );
303extern int Fra_ClassesRefine( Fra_Cla_t * p );
304extern int Fra_ClassesRefine1( Fra_Cla_t * p, int fRefineNewClass, int * pSkipped );
305extern int Fra_ClassesCountLits( Fra_Cla_t * p );
306extern int Fra_ClassesCountPairs( Fra_Cla_t * p );
307extern void Fra_ClassesTest( Fra_Cla_t * p, int Id1, int Id2 );
308extern void Fra_ClassesLatchCorr( Fra_Man_t * p );
309extern void Fra_ClassesPostprocess( Fra_Cla_t * p );
310extern void Fra_ClassesSelectRepr( Fra_Cla_t * p );
311extern Aig_Man_t * Fra_ClassesDeriveAig( Fra_Cla_t * p, int nFramesK );
312/*=== fraCnf.c ========================================================*/
313extern void Fra_CnfNodeAddToSolver( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew );
314/*=== fraCore.c ========================================================*/
315extern void Fra_FraigSweep( Fra_Man_t * pManAig );
316extern int Fra_FraigMiterStatus( Aig_Man_t * p );
317extern int Fra_FraigMiterAssertedOutput( Aig_Man_t * p );
318extern Aig_Man_t * Fra_FraigPerform( Aig_Man_t * pManAig, Fra_Par_t * pPars );
319extern Aig_Man_t * Fra_FraigChoice( Aig_Man_t * pManAig, int nConfMax, int nLevelMax );
320extern Aig_Man_t * Fra_FraigEquivence( Aig_Man_t * pManAig, int nConfMax, int fProve );
321/*=== fraHot.c ========================================================*/
322extern Vec_Int_t * Fra_OneHotCompute( Fra_Man_t * p, Fra_Sml_t * pSim );
323extern void Fra_OneHotAssume( Fra_Man_t * p, Vec_Int_t * vOneHots );
324extern void Fra_OneHotCheck( Fra_Man_t * p, Vec_Int_t * vOneHots );
325extern int Fra_OneHotRefineUsingCex( Fra_Man_t * p, Vec_Int_t * vOneHots );
326extern int Fra_OneHotCount( Fra_Man_t * p, Vec_Int_t * vOneHots );
327extern void Fra_OneHotEstimateCoverage( Fra_Man_t * p, Vec_Int_t * vOneHots );
328extern Aig_Man_t * Fra_OneHotCreateExdc( Fra_Man_t * p, Vec_Int_t * vOneHots );
329extern void Fra_OneHotAddKnownConstraint( Fra_Man_t * p, Vec_Ptr_t * vOnehots );
330/*=== fraImp.c ========================================================*/
331extern Vec_Int_t * Fra_ImpDerive( Fra_Man_t * p, int nImpMaxLimit, int nImpUseLimit, int fLatchCorr );
332extern void Fra_ImpAddToSolver( Fra_Man_t * p, Vec_Int_t * vImps, int * pSatVarNums );
333extern int Fra_ImpCheckForNode( Fra_Man_t * p, Vec_Int_t * vImps, Aig_Obj_t * pNode, int Pos );
334extern int Fra_ImpRefineUsingCex( Fra_Man_t * p, Vec_Int_t * vImps );
335extern void Fra_ImpCompactArray( Vec_Int_t * vImps );
336extern double Fra_ImpComputeStateSpaceRatio( Fra_Man_t * p );
337extern int Fra_ImpVerifyUsingSimulation( Fra_Man_t * p );
338extern void Fra_ImpRecordInManager( Fra_Man_t * p, Aig_Man_t * pNew );
339/*=== fraInd.c ========================================================*/
340extern Aig_Man_t * Fra_FraigInduction( Aig_Man_t * p, Fra_Ssw_t * pPars );
341/*=== fraIndVer.c =====================================================*/
342extern int Fra_InvariantVerify( Aig_Man_t * p, int nFrames, Vec_Int_t * vClauses, Vec_Int_t * vLits );
343/*=== fraLcr.c ========================================================*/
344extern Aig_Man_t * Fra_FraigLatchCorrespondence( Aig_Man_t * pAig, int nFramesP, int nConfMax, int fProve, int fVerbose, int * pnIter, float TimeLimit );
345/*=== fraMan.c ========================================================*/
346extern void Fra_ParamsDefault( Fra_Par_t * pParams );
347extern void Fra_ParamsDefaultSeq( Fra_Par_t * pParams );
348extern Fra_Man_t * Fra_ManStart( Aig_Man_t * pManAig, Fra_Par_t * pParams );
349extern void Fra_ManClean( Fra_Man_t * p, int nNodesMax );
350extern Aig_Man_t * Fra_ManPrepareComb( Fra_Man_t * p );
351extern void Fra_ManFinalizeComb( Fra_Man_t * p );
352extern void Fra_ManStop( Fra_Man_t * p );
353extern void Fra_ManPrint( Fra_Man_t * p );
354/*=== fraSat.c ========================================================*/
355extern int Fra_NodesAreEquiv( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew );
356extern int Fra_NodesAreImp( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew, int fComplL, int fComplR );
357extern int Fra_NodesAreClause( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew, int fComplL, int fComplR );
358extern int Fra_NodeIsConst( Fra_Man_t * p, Aig_Obj_t * pNew );
359/*=== fraSec.c ========================================================*/
360extern void Fra_SecSetDefaultParams( Fra_Sec_t * p );
361extern int Fra_FraigSec( Aig_Man_t * p, Fra_Sec_t * pParSec, Aig_Man_t ** ppResult );
362/*=== fraSim.c ========================================================*/
363extern int Fra_SmlNodeHash( Aig_Obj_t * pObj, int nTableSize );
364extern int Fra_SmlNodeIsConst( Aig_Obj_t * pObj );
365extern int Fra_SmlNodesAreEqual( Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 );
366extern int Fra_SmlNodeNotEquWeight( Fra_Sml_t * p, int Left, int Right );
367extern int Fra_SmlNodeCountOnes( Fra_Sml_t * p, Aig_Obj_t * pObj );
368extern int Fra_SmlCheckOutput( Fra_Man_t * p );
369extern void Fra_SmlSavePattern( Fra_Man_t * p );
370extern void Fra_SmlSimulate( Fra_Man_t * p, int fInit );
371extern void Fra_SmlResimulate( Fra_Man_t * p );
372extern Fra_Sml_t * Fra_SmlStart( Aig_Man_t * pAig, int nPref, int nFrames, int nWordsFrame );
373extern void Fra_SmlStop( Fra_Sml_t * p );
374extern Fra_Sml_t * Fra_SmlSimulateComb( Aig_Man_t * pAig, int nWords, int fCheckMiter );
375extern Fra_Sml_t * Fra_SmlSimulateCombGiven( Aig_Man_t * pAig, char * pFileName, int fCheckMiter, int fVerbose );
376extern Fra_Sml_t * Fra_SmlSimulateSeq( Aig_Man_t * pAig, int nPref, int nFrames, int nWords, int fCheckMiter );
377extern Abc_Cex_t * Fra_SmlGetCounterExample( Fra_Sml_t * p );
378extern Abc_Cex_t * Fra_SmlCopyCounterExample( Aig_Man_t * pAig, Aig_Man_t * pFrames, int * pModel );
379
380ABC_NAMESPACE_HEADER_END
381
382
383
384#endif
385
389
nWords
int nWords
Definition abcNpn.c:127
abctime
ABC_INT64_T abctime
Definition abc_global.h:332
ABC_NAMESPACE_HEADER_END
#define ABC_NAMESPACE_HEADER_END
Definition abc_namespaces.h:51
ABC_NAMESPACE_HEADER_START
#define ABC_NAMESPACE_HEADER_START
NAMESPACES ///.
Definition abc_namespaces.h:50
Aig_Obj_t
struct Aig_Obj_t_ Aig_Obj_t
Definition aig.h:51
Aig_Man_t
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition aig.h:50
Aig_ManRandom
unsigned Aig_ManRandom(int fReset)
Definition aigUtil.c:1170
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
sat_solver
#define sat_solver
Definition cecSatG2.c:34
Pos
ush Pos
Definition deflate.h:88
p
Cube * p
Definition exorList.c:222
Fra_ClassesRefine1
int Fra_ClassesRefine1(Fra_Cla_t *p, int fRefineNewClass, int *pSkipped)
Definition fraClass.c:527
Fra_ClassesCopyReprs
void Fra_ClassesCopyReprs(Fra_Cla_t *p, Vec_Ptr_t *vFailed)
Definition fraClass.c:114
Fra_NodeIsConst
int Fra_NodeIsConst(Fra_Man_t *p, Aig_Obj_t *pNew)
Definition fraSat.c:425
Fra_ClassesStart
Fra_Cla_t * Fra_ClassesStart(Aig_Man_t *pAig)
FUNCTION DEFINITIONS ///.
Definition fraClass.c:60
Fra_FraigSweep
void Fra_FraigSweep(Fra_Man_t *pManAig)
Definition fraCore.c:310
Fra_ImpCheckForNode
int Fra_ImpCheckForNode(Fra_Man_t *p, Vec_Int_t *vImps, Aig_Obj_t *pNode, int Pos)
Definition fraImp.c:503
Fra_Bmc_t
struct Fra_Bmc_t_ Fra_Bmc_t
Definition fra.h:59
Fra_SmlNodeIsConst
int Fra_SmlNodeIsConst(Aig_Obj_t *pObj)
Definition fraSim.c:86
Fra_ClassesDeriveAig
Aig_Man_t * Fra_ClassesDeriveAig(Fra_Cla_t *p, int nFramesK)
Definition fraClass.c:796
Fra_Par_t
typedefABC_NAMESPACE_HEADER_START struct Fra_Par_t_ Fra_Par_t
INCLUDES ///.
Definition fra.h:53
Fra_ClassesTest
void Fra_ClassesTest(Fra_Cla_t *p, int Id1, int Id2)
Definition fraClass.c:590
Fra_ImpVerifyUsingSimulation
int Fra_ImpVerifyUsingSimulation(Fra_Man_t *p)
Definition fraImp.c:665
Fra_ClassesStop
void Fra_ClassesStop(Fra_Cla_t *p)
Definition fraClass.c:90
Fra_SmlSimulate
void Fra_SmlSimulate(Fra_Man_t *p, int fInit)
Definition fraSim.c:738
Fra_OneHotCompute
Vec_Int_t * Fra_OneHotCompute(Fra_Man_t *p, Fra_Sml_t *pSim)
Definition fraHot.c:134
Fra_NodesAreClause
int Fra_NodesAreClause(Fra_Man_t *p, Aig_Obj_t *pOld, Aig_Obj_t *pNew, int fComplL, int fComplR)
Definition fraSat.c:317
Fra_FraigCecPartitioned
int Fra_FraigCecPartitioned(Aig_Man_t *pMan1, Aig_Man_t *pMan2, int nConfLimit, int nPartSize, int fSmart, int fVerbose)
Definition fraCec.c:451
Fra_OneHotAssume
void Fra_OneHotAssume(Fra_Man_t *p, Vec_Int_t *vOneHots)
Definition fraHot.c:191
Fra_OneHotEstimateCoverage
void Fra_OneHotEstimateCoverage(Fra_Man_t *p, Vec_Int_t *vOneHots)
Definition fraHot.c:328
Fra_FraigEquivence
Aig_Man_t * Fra_FraigEquivence(Aig_Man_t *pManAig, int nConfMax, int fProve)
Definition fraCore.c:468
Fra_FraigLatchCorrespondence
Aig_Man_t * Fra_FraigLatchCorrespondence(Aig_Man_t *pAig, int nFramesP, int nConfMax, int fProve, int fVerbose, int *pnIter, float TimeLimit)
Definition fraLcr.c:531
Fra_FraigPerform
Aig_Man_t * Fra_FraigPerform(Aig_Man_t *pManAig, Fra_Par_t *pPars)
Definition fraCore.c:375
Fra_ImpCompactArray
void Fra_ImpCompactArray(Vec_Int_t *vImps)
Definition fraImp.c:607
Fra_SmlStop
void Fra_SmlStop(Fra_Sml_t *p)
Definition fraSim.c:839
Fra_ClassesPrepare
void Fra_ClassesPrepare(Fra_Cla_t *p, int fLatchCorr, int nMaxLevs)
Definition fraClass.c:276
Fra_ImpRecordInManager
void Fra_ImpRecordInManager(Fra_Man_t *p, Aig_Man_t *pNew)
Definition fraImp.c:705
Fra_Man_t
struct Fra_Man_t_ Fra_Man_t
Definition fra.h:56
Fra_SmlStart
Fra_Sml_t * Fra_SmlStart(Aig_Man_t *pAig, int nPref, int nFrames, int nWordsFrame)
Definition fraSim.c:813
Fra_OneHotCreateExdc
Aig_Man_t * Fra_OneHotCreateExdc(Fra_Man_t *p, Vec_Int_t *vOneHots)
Definition fraHot.c:398
Fra_FraigCec
int Fra_FraigCec(Aig_Man_t **ppAig, int nConfLimit, int fVerbose)
Definition fraCec.c:320
Fra_CnfNodeAddToSolver
void Fra_CnfNodeAddToSolver(Fra_Man_t *p, Aig_Obj_t *pOld, Aig_Obj_t *pNew)
Definition fraCnf.c:238
Fra_ImpDerive
Vec_Int_t * Fra_ImpDerive(Fra_Man_t *p, int nImpMaxLimit, int nImpUseLimit, int fLatchCorr)
Definition fraImp.c:321
Fra_SmlCheckOutput
int Fra_SmlCheckOutput(Fra_Man_t *p)
Definition fraSim.c:326
Fra_ManPrepareComb
Aig_Man_t * Fra_ManPrepareComb(Fra_Man_t *p)
Definition fraMan.c:176
Fra_FraigSat
int Fra_FraigSat(Aig_Man_t *pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int nLearnedStart, int nLearnedDelta, int nLearnedPerce, int fFlipBits, int fAndOuts, int fNewSolver, int fVerbose)
ITERATORS ///.
Definition fraCec.c:47
Fra_SmlNodeNotEquWeight
int Fra_SmlNodeNotEquWeight(Fra_Sml_t *p, int Left, int Right)
Definition fraSim.c:133
Fra_OneHotRefineUsingCex
int Fra_OneHotRefineUsingCex(Fra_Man_t *p, Vec_Int_t *vOneHots)
Definition fraHot.c:266
Fra_SecSetDefaultParams
void Fra_SecSetDefaultParams(Fra_Sec_t *p)
DECLARATIONS ///.
Definition fraSec.c:52
Fra_ManStop
void Fra_ManStop(Fra_Man_t *p)
Definition fraMan.c:240
Fra_Sec_t
struct Fra_Sec_t_ Fra_Sec_t
Definition fra.h:55
Fra_ClassesRefine
int Fra_ClassesRefine(Fra_Cla_t *p)
Definition fraClass.c:493
Fra_ClassesCountLits
int Fra_ClassesCountLits(Fra_Cla_t *p)
Definition fraClass.c:164
Fra_OneHotAddKnownConstraint
void Fra_OneHotAddKnownConstraint(Fra_Man_t *p, Vec_Ptr_t *vOnehots)
Definition fraHot.c:439
Fra_Sml_t
struct Fra_Sml_t_ Fra_Sml_t
Definition fra.h:58
Fra_SmlSimulateComb
Fra_Sml_t * Fra_SmlSimulateComb(Aig_Man_t *pAig, int nWords, int fCheckMiter)
Definition fraSim.c:856
Fra_ManStart
Fra_Man_t * Fra_ManStart(Aig_Man_t *pManAig, Fra_Par_t *pParams)
Definition fraMan.c:104
Fra_ImpAddToSolver
void Fra_ImpAddToSolver(Fra_Man_t *p, Vec_Int_t *vImps, int *pSatVarNums)
Definition fraImp.c:428
Fra_ClassesPostprocess
void Fra_ClassesPostprocess(Fra_Cla_t *p)
Definition fraClass.c:641
Fra_FraigChoice
Aig_Man_t * Fra_FraigChoice(Aig_Man_t *pManAig, int nConfMax, int nLevelMax)
Definition fraCore.c:442
Fra_SmlCopyCounterExample
Abc_Cex_t * Fra_SmlCopyCounterExample(Aig_Man_t *pAig, Aig_Man_t *pFrames, int *pModel)
Definition fraSim.c:1123
Fra_ClassesLatchCorr
void Fra_ClassesLatchCorr(Fra_Man_t *p)
Definition fraClass.c:615
Fra_BmcStop
void Fra_BmcStop(Fra_Bmc_t *p)
Definition fraBmc.c:216
Fra_ClassesSelectRepr
void Fra_ClassesSelectRepr(Fra_Cla_t *p)
Definition fraClass.c:706
Fra_NodesAreImp
int Fra_NodesAreImp(Fra_Man_t *p, Aig_Obj_t *pOld, Aig_Obj_t *pNew, int fComplL, int fComplR)
Definition fraSat.c:209
Fra_BmcNodeIsConst
int Fra_BmcNodeIsConst(Aig_Obj_t *pObj)
Definition fraBmc.c:103
Fra_SmlSimulateCombGiven
Fra_Sml_t * Fra_SmlSimulateCombGiven(Aig_Man_t *pAig, char *pFileName, int fCheckMiter, int fVerbose)
Definition fraSim.c:987
Fra_ClassesCountPairs
int Fra_ClassesCountPairs(Fra_Cla_t *p)
Definition fraClass.c:189
Fra_SmlNodesAreEqual
int Fra_SmlNodesAreEqual(Aig_Obj_t *pObj0, Aig_Obj_t *pObj1)
Definition fraSim.c:109
Fra_BmcNodesAreEqual
int Fra_BmcNodesAreEqual(Aig_Obj_t *pObj0, Aig_Obj_t *pObj1)
FUNCTION DEFINITIONS ///.
Definition fraBmc.c:72
Fra_SmlResimulate
void Fra_SmlResimulate(Fra_Man_t *p)
Definition fraSim.c:703
Fra_OneHotCheck
void Fra_OneHotCheck(Fra_Man_t *p, Vec_Int_t *vOneHots)
Definition fraHot.c:229
Fra_FraigMiterAssertedOutput
int Fra_FraigMiterAssertedOutput(Aig_Man_t *p)
Definition fraCore.c:125
Fra_ManFinalizeComb
void Fra_ManFinalizeComb(Fra_Man_t *p)
Definition fraMan.c:217
Fra_SmlNodeCountOnes
int Fra_SmlNodeCountOnes(Fra_Sml_t *p, Aig_Obj_t *pObj)
Definition fraSim.c:177
Fra_FraigMiterStatus
int Fra_FraigMiterStatus(Aig_Man_t *p)
DECLARATIONS ///.
Definition fraCore.c:62
Fra_Ssw_t
struct Fra_Ssw_t_ Fra_Ssw_t
Definition fra.h:54
Fra_SmlNodeHash
int Fra_SmlNodeHash(Aig_Obj_t *pObj, int nTableSize)
DECLARATIONS ///.
Definition fraSim.c:46
Fra_ClassesPrint
void Fra_ClassesPrint(Fra_Cla_t *p, int fVeryVerbose)
Definition fraClass.c:236
Fra_ImpRefineUsingCex
int Fra_ImpRefineUsingCex(Fra_Man_t *p, Vec_Int_t *vImps)
Definition fraImp.c:575
Fra_InvariantVerify
int Fra_InvariantVerify(Aig_Man_t *p, int nFrames, Vec_Int_t *vClauses, Vec_Int_t *vLits)
DECLARATIONS ///.
Definition fraIndVer.c:46
Fra_BmcPerformSimple
void Fra_BmcPerformSimple(Aig_Man_t *pAig, int nFrames, int nBTLimit, int fRewrite, int fVerbose)
Definition fraBmc.c:383
Fra_SmlSimulateSeq
Fra_Sml_t * Fra_SmlSimulateSeq(Aig_Man_t *pAig, int nPref, int nFrames, int nWords, int fCheckMiter)
Definition fraSim.c:1027
Fra_FraigInduction
Aig_Man_t * Fra_FraigInduction(Aig_Man_t *p, Fra_Ssw_t *pPars)
Definition fraInd.c:344
Fra_FraigSec
int Fra_FraigSec(Aig_Man_t *p, Fra_Sec_t *pParSec, Aig_Man_t **ppResult)
Definition fraSec.c:118
Fra_Cla_t
struct Fra_Cla_t_ Fra_Cla_t
Definition fra.h:57
Fra_ManClean
void Fra_ManClean(Fra_Man_t *p, int nNodesMax)
Definition fraMan.c:145
Fra_OneHotCount
int Fra_OneHotCount(Fra_Man_t *p, Vec_Int_t *vOneHots)
Definition fraHot.c:303
Fra_ManPrint
void Fra_ManPrint(Fra_Man_t *p)
Definition fraMan.c:278
Fra_ParamsDefault
void Fra_ParamsDefault(Fra_Par_t *pParams)
DECLARATIONS ///.
Definition fraMan.c:45
Fra_SmlGetCounterExample
Abc_Cex_t * Fra_SmlGetCounterExample(Fra_Sml_t *p)
Definition fraSim.c:1049
Fra_NodesAreEquiv
int Fra_NodesAreEquiv(Fra_Man_t *p, Aig_Obj_t *pOld, Aig_Obj_t *pNew)
FUNCTION DEFINITIONS ///.
Definition fraSat.c:48
Fra_BmcPerform
void Fra_BmcPerform(Fra_Man_t *p, int nPref, int nDepth)
Definition fraBmc.c:311
Fra_SmlSavePattern
void Fra_SmlSavePattern(Fra_Man_t *p)
Definition fraSim.c:241
Fra_ImpComputeStateSpaceRatio
double Fra_ImpComputeStateSpaceRatio(Fra_Man_t *p)
Definition fraImp.c:628
Fra_ParamsDefaultSeq
void Fra_ParamsDefaultSeq(Fra_Par_t *pParams)
Definition fraMan.c:75
Aig_Obj_t_::Id
int Id
Definition aig.h:85
Aig_Obj_t_::pData
void * pData
Definition aig.h:87
Fra_Bmc_t_
DECLARATIONS ///.
Definition fraBmc.c:32
Fra_Cla_t_
Definition fra.h:151
Fra_Cla_t_::fRefinement
int fRefinement
Definition fra.h:162
Fra_Cla_t_::vClassOld
Vec_Ptr_t * vClassOld
Definition fra.h:159
Fra_Cla_t_::pFuncNodeIsConst
int(* pFuncNodeIsConst)(Aig_Obj_t *)
Definition fra.h:166
Fra_Cla_t_::vClasses1
Vec_Ptr_t * vClasses1
Definition fra.h:155
Fra_Cla_t_::pFuncNodesAreEqual
int(* pFuncNodesAreEqual)(Aig_Obj_t *, Aig_Obj_t *)
Definition fra.h:167
Fra_Cla_t_::pAig
Aig_Man_t * pAig
Definition fra.h:152
Fra_Cla_t_::vImps
Vec_Int_t * vImps
Definition fra.h:163
Fra_Cla_t_::vClassesTemp
Vec_Ptr_t * vClassesTemp
Definition fra.h:156
Fra_Cla_t_::pFuncNodeHash
int(* pFuncNodeHash)(Aig_Obj_t *, int)
Definition fra.h:165
Fra_Cla_t_::vClassNew
Vec_Ptr_t * vClassNew
Definition fra.h:160
Fra_Cla_t_::nPairs
int nPairs
Definition fra.h:161
Fra_Cla_t_::pMemRepr
Aig_Obj_t ** pMemRepr
Definition fra.h:153
Fra_Cla_t_::pMemClassesFree
Aig_Obj_t ** pMemClassesFree
Definition fra.h:158
Fra_Cla_t_::vClasses
Vec_Ptr_t * vClasses
Definition fra.h:154
Fra_Cla_t_::pMemClasses
Aig_Obj_t ** pMemClasses
Definition fra.h:157
Fra_Man_t_
Definition fra.h:187
Fra_Man_t_::pManFraig
Aig_Man_t * pManFraig
Definition fra.h:192
Fra_Man_t_::nSpeculs
int nSpeculs
Definition fra.h:234
Fra_Man_t_::timeSim
abctime timeSim
Definition fra.h:240
Fra_Man_t_::time1
abctime time1
Definition fra.h:249
Fra_Man_t_::nSatCallsUnsat
int nSatCallsUnsat
Definition fra.h:230
Fra_Man_t_::timeSatUnsat
abctime timeSatUnsat
Definition fra.h:244
Fra_Man_t_::nRegsEnd
int nRegsEnd
Definition fra.h:227
Fra_Man_t_::nPatWords
int nPatWords
Definition fra.h:204
Fra_Man_t_::pManAig
Aig_Man_t * pManAig
Definition fra.h:191
Fra_Man_t_::timeTotal
abctime timeTotal
Definition fra.h:248
Fra_Man_t_::nSimRounds
int nSimRounds
Definition fra.h:220
Fra_Man_t_::nLitsEnd
int nLitsEnd
Definition fra.h:223
Fra_Man_t_::pCla
Fra_Cla_t * pCla
Definition fra.h:198
Fra_Man_t_::nSatCallsSat
int nSatCallsSat
Definition fra.h:229
Fra_Man_t_::nBTLimitGlobal
ABC_INT64_T nBTLimitGlobal
Definition fra.h:213
Fra_Man_t_::nSatFails
int nSatFails
Definition fra.h:232
Fra_Man_t_::nMemAlloc
int nMemAlloc
Definition fra.h:217
Fra_Man_t_::nSatCallsSkipped
int nSatCallsSkipped
Definition fra.h:238
Fra_Man_t_::nNodesBeg
int nNodesBeg
Definition fra.h:224
Fra_Man_t_::timeSat
abctime timeSat
Definition fra.h:243
Fra_Man_t_::nLitsBeg
int nLitsBeg
Definition fra.h:222
Fra_Man_t_::pMemFraig
Aig_Obj_t ** pMemFraig
Definition fra.h:195
Fra_Man_t_::nInsLimitGlobal
ABC_INT64_T nInsLimitGlobal
Definition fra.h:214
Fra_Man_t_::timeRwr
abctime timeRwr
Definition fra.h:242
Fra_Man_t_::vPiVars
Vec_Ptr_t * vPiVars
Definition fra.h:212
Fra_Man_t_::pMemSatNums
int * pMemSatNums
Definition fra.h:216
Fra_Man_t_::timeRef
abctime timeRef
Definition fra.h:247
Fra_Man_t_::vOneHots
Vec_Int_t * vOneHots
Definition fra.h:208
Fra_Man_t_::timeTrav
abctime timeTrav
Definition fra.h:241
Fra_Man_t_::nSatVars
int nSatVars
Definition fra.h:211
Fra_Man_t_::nRegsBeg
int nRegsBeg
Definition fra.h:226
Fra_Man_t_::pMemFanins
Vec_Ptr_t ** pMemFanins
Definition fra.h:215
Fra_Man_t_::nChoices
int nChoices
Definition fra.h:235
Fra_Man_t_::nSatCalls
int nSatCalls
Definition fra.h:228
Fra_Man_t_::pPars
Fra_Par_t * pPars
Definition fra.h:189
Fra_Man_t_::nNodesMiter
int nNodesMiter
Definition fra.h:221
Fra_Man_t_::pSat
sat_solver * pSat
Definition fra.h:210
Fra_Man_t_::time2
abctime time2
Definition fra.h:250
Fra_Man_t_::nSizeAlloc
int nSizeAlloc
Definition fra.h:196
Fra_Man_t_::nSatFailsReal
int nSatFailsReal
Definition fra.h:233
Fra_Man_t_::pPatWords
unsigned * pPatWords
Definition fra.h:205
Fra_Man_t_::vCex
Vec_Int_t * vCex
Definition fra.h:206
Fra_Man_t_::nChoicesFake
int nChoicesFake
Definition fra.h:236
Fra_Man_t_::vTimeouts
Vec_Ptr_t * vTimeouts
Definition fra.h:218
Fra_Man_t_::timeSatFail
abctime timeSatFail
Definition fra.h:246
Fra_Man_t_::nNodesEnd
int nNodesEnd
Definition fra.h:225
Fra_Man_t_::nSatProof
int nSatProof
Definition fra.h:231
Fra_Man_t_::timeSatSat
abctime timeSatSat
Definition fra.h:245
Fra_Man_t_::pBmc
Fra_Bmc_t * pBmc
Definition fra.h:202
Fra_Man_t_::pSml
Fra_Sml_t * pSml
Definition fra.h:200
Fra_Man_t_::nFramesAll
int nFramesAll
Definition fra.h:194
Fra_Man_t_::nSatCallsRecent
int nSatCallsRecent
Definition fra.h:237
Fra_Par_t_
Definition fra.h:63
Fra_Par_t_::fConeBias
int fConeBias
Definition fra.h:75
Fra_Par_t_::fPatScores
int fPatScores
Definition fra.h:66
Fra_Par_t_::nLevelMax
int nLevelMax
Definition fra.h:78
Fra_Par_t_::dActConeBumpMax
double dActConeBumpMax
Definition fra.h:69
Fra_Par_t_::nBTLimitMiter
int nBTLimitMiter
Definition fra.h:77
Fra_Par_t_::nMaxImps
int nMaxImps
Definition fra.h:81
Fra_Par_t_::fUse1Hot
int fUse1Hot
Definition fra.h:86
Fra_Par_t_::fRewrite
int fRewrite
Definition fra.h:83
Fra_Par_t_::MaxScore
int MaxScore
Definition fra.h:67
Fra_Par_t_::nBTLimitNode
int nBTLimitNode
Definition fra.h:76
Fra_Par_t_::dActConeRatio
double dActConeRatio
Definition fra.h:68
Fra_Par_t_::nSimWords
int nSimWords
Definition fra.h:64
Fra_Par_t_::nFramesK
int nFramesK
Definition fra.h:80
Fra_Par_t_::fWriteImps
int fWriteImps
Definition fra.h:87
Fra_Par_t_::fProve
int fProve
Definition fra.h:72
Fra_Par_t_::fUseImps
int fUseImps
Definition fra.h:85
Fra_Par_t_::dSimSatur
double dSimSatur
Definition fra.h:65
Fra_Par_t_::fDontShowBar
int fDontShowBar
Definition fra.h:88
Fra_Par_t_::fDoSparse
int fDoSparse
Definition fra.h:74
Fra_Par_t_::nFramesP
int nFramesP
Definition fra.h:79
Fra_Par_t_::fVerbose
int fVerbose
Definition fra.h:73
Fra_Par_t_::nMaxLevs
int nMaxLevs
Definition fra.h:82
Fra_Par_t_::fSpeculate
int fSpeculate
Definition fra.h:71
Fra_Par_t_::fLatchCorr
int fLatchCorr
Definition fra.h:84
Fra_Par_t_::fChoicing
int fChoicing
Definition fra.h:70
Fra_Sec_t_
Definition fra.h:115
Fra_Sec_t_::fStopOnFirstFail
int fStopOnFirstFail
Definition fra.h:135
Fra_Sec_t_::nPdrTimeout
int nPdrTimeout
Definition fra.h:125
Fra_Sec_t_::fFraiging
int fFraiging
Definition fra.h:129
Fra_Sec_t_::nBTLimit
int nBTLimit
Definition fra.h:119
Fra_Sec_t_::fVerbose
int fVerbose
Definition fra.h:139
Fra_Sec_t_::nBddIterMax
int nBddIterMax
Definition fra.h:124
Fra_Sec_t_::nBTLimitInter
int nBTLimitInter
Definition fra.h:121
Fra_Sec_t_::fRetimeRegs
int fRetimeRegs
Definition fra.h:128
Fra_Sec_t_::nBddMax
int nBddMax
Definition fra.h:123
Fra_Sec_t_::fVeryVerbose
int fVeryVerbose
Definition fra.h:140
Fra_Sec_t_::fTryBmc
int fTryBmc
Definition fra.h:117
Fra_Sec_t_::fUseNewProver
int fUseNewProver
Definition fra.h:136
Fra_Sec_t_::fReportSolution
int fReportSolution
Definition fra.h:146
Fra_Sec_t_::fRetimeFirst
int fRetimeFirst
Definition fra.h:127
Fra_Sec_t_::fInduction
int fInduction
Definition fra.h:130
Fra_Sec_t_::fPhaseAbstract
int fPhaseAbstract
Definition fra.h:126
Fra_Sec_t_::fInterpolation
int fInterpolation
Definition fra.h:131
Fra_Sec_t_::nSMnumber
int nSMnumber
Definition fra.h:143
Fra_Sec_t_::fReorderImage
int fReorderImage
Definition fra.h:134
Fra_Sec_t_::fReadUnsolved
int fReadUnsolved
Definition fra.h:142
Fra_Sec_t_::fInterSeparate
int fInterSeparate
Definition fra.h:132
Fra_Sec_t_::fTryComb
int fTryComb
Definition fra.h:116
Fra_Sec_t_::nFramesMax
int nFramesMax
Definition fra.h:118
Fra_Sec_t_::fRecursive
int fRecursive
Definition fra.h:145
Fra_Sec_t_::nBddVarsMax
int nBddVarsMax
Definition fra.h:122
Fra_Sec_t_::fReachability
int fReachability
Definition fra.h:133
Fra_Sec_t_::nBTLimitGlobal
int nBTLimitGlobal
Definition fra.h:120
Fra_Sec_t_::fUsePdr
int fUsePdr
Definition fra.h:137
Fra_Sec_t_::TimeLimit
int TimeLimit
Definition fra.h:141
Fra_Sec_t_::fSilent
int fSilent
Definition fra.h:138
Fra_Sml_t_
Definition fra.h:172
Fra_Sml_t_::nWordsPref
int nWordsPref
Definition fra.h:178
Fra_Sml_t_::pData
unsigned pData[0]
Definition fra.h:182
Fra_Sml_t_::fNonConstOut
int fNonConstOut
Definition fra.h:179
Fra_Sml_t_::nWordsFrame
int nWordsFrame
Definition fra.h:176
Fra_Sml_t_::nSimRounds
int nSimRounds
Definition fra.h:180
Fra_Sml_t_::pAig
Aig_Man_t * pAig
Definition fra.h:173
Fra_Sml_t_::timeSim
int timeSim
Definition fra.h:181
Fra_Sml_t_::nFrames
int nFrames
Definition fra.h:175
Fra_Sml_t_::nPref
int nPref
Definition fra.h:174
Fra_Sml_t_::nWordsTotal
int nWordsTotal
Definition fra.h:177
Fra_Ssw_t_
Definition fra.h:93
Fra_Ssw_t_::fRewrite
int fRewrite
Definition fra.h:102
Fra_Ssw_t_::fUse1Hot
int fUse1Hot
Definition fra.h:106
Fra_Ssw_t_::fSilent
int fSilent
Definition fra.h:108
Fra_Ssw_t_::nMinDomSize
int nMinDomSize
Definition fra.h:100
Fra_Ssw_t_::nPartSize
int nPartSize
Definition fra.h:94
Fra_Ssw_t_::nFramesP
int nFramesP
Definition fra.h:96
Fra_Ssw_t_::nIters
int nIters
Definition fra.h:109
Fra_Ssw_t_::nMaxImps
int nMaxImps
Definition fra.h:98
Fra_Ssw_t_::fLatchCorr
int fLatchCorr
Definition fra.h:104
Fra_Ssw_t_::TimeLimit
float TimeLimit
Definition fra.h:110
Fra_Ssw_t_::fUseImps
int fUseImps
Definition fra.h:101
Fra_Ssw_t_::fFraiging
int fFraiging
Definition fra.h:103
Fra_Ssw_t_::fVerbose
int fVerbose
Definition fra.h:107
Fra_Ssw_t_::fWriteImps
int fWriteImps
Definition fra.h:105
Fra_Ssw_t_::nOverSize
int nOverSize
Definition fra.h:95
Fra_Ssw_t_::nMaxLevs
int nMaxLevs
Definition fra.h:99
Fra_Ssw_t_::nFramesK
int nFramesK
Definition fra.h:97
Abc_Cex_t
typedefABC_NAMESPACE_HEADER_START struct Abc_Cex_t_ Abc_Cex_t
INCLUDES ///.
Definition utilCex.h:39
assert
#define assert(ex)
Definition util_old.h:213
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition vecPtr.h:42