abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
cecCore.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [cecCore.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [Combinational equivalence checking.]
8 
9  Synopsis [Core procedures.]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - June 20, 2005.]
16 
17  Revision [$Id: cecCore.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "cecInt.h"
22 
23 ABC_NAMESPACE_IMPL_START
24 
25 
26 ////////////////////////////////////////////////////////////////////////
27 /// DECLARATIONS ///
28 ////////////////////////////////////////////////////////////////////////
29 
30 ////////////////////////////////////////////////////////////////////////
31 /// FUNCTION DEFINITIONS ///
32 ////////////////////////////////////////////////////////////////////////
33 
34 /**Function*************************************************************
35 
36  Synopsis [This procedure sets default parameters.]
37 
38  Description []
39 
40  SideEffects []
41 
42  SeeAlso []
43 
44 ***********************************************************************/
45 void Cec_ManSatSetDefaultParams( Cec_ParSat_t * p )
46 {
47  memset( p, 0, sizeof(Cec_ParSat_t) );
48  p->nBTLimit = 100; // conflict limit at a node
49  p->nSatVarMax = 2000; // the max number of SAT variables
50  p->nCallsRecycle = 200; // calls to perform before recycling SAT solver
51  p->fNonChrono = 0; // use non-chronological backtracling (for circuit SAT only)
52  p->fPolarFlip = 1; // flops polarity of variables
53  p->fCheckMiter = 0; // the circuit is the miter
54 // p->fFirstStop = 0; // stop on the first sat output
55  p->fLearnCls = 0; // perform clause learning
56  p->fVerbose = 0; // verbose stats
57 }
58 
59 /**Function************ *************************************************
60 
61  Synopsis [This procedure sets default parameters.]
62 
63  Description []
64 
65  SideEffects []
66 
67  SeeAlso []
68 
69 ***********************************************************************/
70 void Cec_ManSimSetDefaultParams( Cec_ParSim_t * p )
71 {
72  memset( p, 0, sizeof(Cec_ParSim_t) );
73  p->nWords = 31; // the number of simulation words
74  p->nFrames = 100; // the number of simulation frames
75  p->nRounds = 20; // the max number of simulation rounds
76  p->nNonRefines = 3; // the max number of rounds without refinement
77  p->TimeLimit = 0; // the runtime limit in seconds
78  p->fCheckMiter = 0; // the circuit is the miter
79 // p->fFirstStop = 0; // stop on the first sat output
80  p->fDualOut = 0; // miter with separate outputs
81  p->fConstCorr = 0; // consider only constants
82  p->fSeqSimulate = 0; // performs sequential simulation
83  p->fVeryVerbose = 0; // verbose stats
84  p->fVerbose = 0; // verbose stats
85 }
86 
87 /**Function************ *************************************************
88 
89  Synopsis [This procedure sets default parameters.]
90 
91  Description []
92 
93  SideEffects []
94 
95  SeeAlso []
96 
97 ***********************************************************************/
98 void Cec_ManSmfSetDefaultParams( Cec_ParSmf_t * p )
99 {
100  memset( p, 0, sizeof(Cec_ParSmf_t) );
101  p->nWords = 31; // the number of simulation words
102  p->nRounds = 200; // the number of simulation rounds
103  p->nFrames = 200; // the max number of time frames
104  p->nNonRefines = 3; // the max number of rounds without refinement
105  p->nMinOutputs = 0; // the min outputs to accumulate
106  p->nBTLimit = 100; // conflict limit at a node
107  p->TimeLimit = 0; // the runtime limit in seconds
108  p->fDualOut = 0; // miter with separate outputs
109  p->fCheckMiter = 0; // the circuit is the miter
110 // p->fFirstStop = 0; // stop on the first sat output
111  p->fVerbose = 0; // verbose stats
112 }
113 
114 /**Function************ *************************************************
115 
116  Synopsis [This procedure sets default parameters.]
117 
118  Description []
119 
120  SideEffects []
121 
122  SeeAlso []
123 
124 ***********************************************************************/
125 void Cec_ManFraSetDefaultParams( Cec_ParFra_t * p )
126 {
127  memset( p, 0, sizeof(Cec_ParFra_t) );
128  p->nWords = 15; // the number of simulation words
129  p->nRounds = 15; // the number of simulation rounds
130  p->TimeLimit = 0; // the runtime limit in seconds
131  p->nItersMax = 10; // the maximum number of iterations of SAT sweeping
132  p->nBTLimit = 100; // conflict limit at a node
133  p->nLevelMax = 0; // restriction on the level of nodes to be swept
134  p->nDepthMax = 1; // the depth in terms of steps of speculative reduction
135  p->fRewriting = 0; // enables AIG rewriting
136  p->fCheckMiter = 0; // the circuit is the miter
137 // p->fFirstStop = 0; // stop on the first sat output
138  p->fDualOut = 0; // miter with separate outputs
139  p->fColorDiff = 0; // miter with separate outputs
140  p->fSatSweeping = 0; // enable SAT sweeping
141  p->fVeryVerbose = 0; // verbose stats
142  p->fVerbose = 0; // verbose stats
143  p->iOutFail = -1; // the failed output
144 }
145 
146 /**Function*************************************************************
147 
148  Synopsis [This procedure sets default parameters.]
149 
150  Description []
151 
152  SideEffects []
153 
154  SeeAlso []
155 
156 ***********************************************************************/
157 void Cec_ManCecSetDefaultParams( Cec_ParCec_t * p )
158 {
159  memset( p, 0, sizeof(Cec_ParCec_t) );
160  p->nBTLimit = 1000; // conflict limit at a node
161  p->TimeLimit = 0; // the runtime limit in seconds
162 // p->fFirstStop = 0; // stop on the first sat output
163  p->fUseSmartCnf = 0; // use smart CNF computation
164  p->fRewriting = 0; // enables AIG rewriting
165  p->fVeryVerbose = 0; // verbose stats
166  p->fVerbose = 0; // verbose stats
167  p->iOutFail = -1; // the number of failed output
168 }
169 
170 /**Function*************************************************************
171 
172  Synopsis [This procedure sets default parameters.]
173 
174  Description []
175 
176  SideEffects []
177 
178  SeeAlso []
179 
180 ***********************************************************************/
181 void Cec_ManCorSetDefaultParams( Cec_ParCor_t * p )
182 {
183  memset( p, 0, sizeof(Cec_ParCor_t) );
184  p->nWords = 15; // the number of simulation words
185  p->nRounds = 15; // the number of simulation rounds
186  p->nFrames = 1; // the number of time frames
187  p->nBTLimit = 100; // conflict limit at a node
188  p->nLevelMax = -1; // (scorr only) the max number of levels
189  p->nStepsMax = -1; // (scorr only) the max number of induction steps
190  p->fLatchCorr = 0; // consider only latch outputs
191  p->fConstCorr = 0; // consider only constants
192  p->fUseRings = 1; // combine classes into rings
193  p->fUseCSat = 1; // use circuit-based solver
194 // p->fFirstStop = 0; // stop on the first sat output
195  p->fUseSmartCnf = 0; // use smart CNF computation
196  p->fVeryVerbose = 0; // verbose stats
197  p->fVerbose = 0; // verbose stats
198 }
199 
200 /**Function*************************************************************
201 
202  Synopsis [This procedure sets default parameters.]
203 
204  Description []
205 
206  SideEffects []
207 
208  SeeAlso []
209 
210 ***********************************************************************/
211 void Cec_ManChcSetDefaultParams( Cec_ParChc_t * p )
212 {
213  memset( p, 0, sizeof(Cec_ParChc_t) );
214  p->nWords = 15; // the number of simulation words
215  p->nRounds = 15; // the number of simulation rounds
216  p->nBTLimit = 1000; // conflict limit at a node
217  p->fUseRings = 1; // use rings
218  p->fUseCSat = 0; // use circuit-based solver
219  p->fVeryVerbose = 0; // verbose stats
220  p->fVerbose = 0; // verbose stats
221 }
222 
223 /**Function*************************************************************
224 
225  Synopsis [Core procedure for SAT sweeping.]
226 
227  Description []
228 
229  SideEffects []
230 
231  SeeAlso []
232 
233 ***********************************************************************/
234 Gia_Man_t * Cec_ManSatSolving( Gia_Man_t * pAig, Cec_ParSat_t * pPars )
235 {
236  Gia_Man_t * pNew;
237  Cec_ManPat_t * pPat;
238  pPat = Cec_ManPatStart();
239  Cec_ManSatSolve( pPat, pAig, pPars );
240 // pNew = Gia_ManDupDfsSkip( pAig );
241  pNew = Gia_ManDup( pAig );
242  Cec_ManPatStop( pPat );
243  return pNew;
244 }
245 
246 /**Function*************************************************************
247 
248  Synopsis [Core procedure for simulation.]
249 
250  Description [Returns 1 if refinement has happened.]
251 
252  SideEffects []
253 
254  SeeAlso []
255 
256 ***********************************************************************/
257 int Cec_ManSimulationOne( Gia_Man_t * pAig, Cec_ParSim_t * pPars )
258 {
259  Cec_ManSim_t * pSim;
260  int RetValue = 0;
261  abctime clkTotal = Abc_Clock();
262  pSim = Cec_ManSimStart( pAig, pPars );
263  if ( (pAig->pReprs == NULL && (RetValue = Cec_ManSimClassesPrepare( pSim, -1 ))) ||
264  (RetValue == 0 && (RetValue = Cec_ManSimClassesRefine( pSim ))) )
265  Abc_Print( 1, "The number of failed outputs of the miter = %6d. (Words = %4d. Frames = %4d.)\n",
266  pSim->nOuts, pPars->nWords, pPars->nFrames );
267  if ( pPars->fVerbose )
268  Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal );
269  Cec_ManSimStop( pSim );
270  return RetValue;
271 }
272 
273 /**Function*************************************************************
274 
275  Synopsis [Core procedure for simulation.]
276 
277  Description []
278 
279  SideEffects []
280 
281  SeeAlso []
282 
283 ***********************************************************************/
284 void Cec_ManSimulation( Gia_Man_t * pAig, Cec_ParSim_t * pPars )
285 {
286  int r, nLitsOld, nLitsNew, nCountNoRef = 0, fStop = 0;
287  Gia_ManRandom( 1 );
288  if ( pPars->fSeqSimulate )
289  Abc_Print( 1, "Performing rounds of random simulation of %d frames with %d words.\n",
290  pPars->nRounds, pPars->nFrames, pPars->nWords );
291  nLitsOld = Gia_ManEquivCountLits( pAig );
292  for ( r = 0; r < pPars->nRounds; r++ )
293  {
294  if ( Cec_ManSimulationOne( pAig, pPars ) )
295  {
296  fStop = 1;
297  break;
298  }
299  // decide when to stop
300  nLitsNew = Gia_ManEquivCountLits( pAig );
301  if ( nLitsOld == 0 || nLitsOld > nLitsNew )
302  {
303  nLitsOld = nLitsNew;
304  nCountNoRef = 0;
305  }
306  else if ( ++nCountNoRef == pPars->nNonRefines )
307  {
308  r++;
309  break;
310  }
311  assert( nLitsOld == nLitsNew );
312  }
313 // if ( pPars->fVerbose )
314  if ( r == pPars->nRounds || fStop )
315  Abc_Print( 1, "Random simulation is stopped after %d rounds.\n", r );
316  else
317  Abc_Print( 1, "Random simulation saturated after %d rounds.\n", r );
318  if ( pPars->fCheckMiter )
319  {
320  int nNonConsts = Cec_ManCountNonConstOutputs( pAig );
321  if ( nNonConsts )
322  Abc_Print( 1, "The number of POs that are not const-0 candidates = %d.\n", nNonConsts );
323  }
324 }
325 
326 /**Function*************************************************************
327 
328  Synopsis [Core procedure for SAT sweeping.]
329 
330  Description []
331 
332  SideEffects []
333 
334  SeeAlso []
335 
336 ***********************************************************************/
337 Gia_Man_t * Cec_ManSatSweeping( Gia_Man_t * pAig, Cec_ParFra_t * pPars )
338 {
339  int fOutputResult = 0;
340  Cec_ParSat_t ParsSat, * pParsSat = &ParsSat;
341  Cec_ParSim_t ParsSim, * pParsSim = &ParsSim;
342  Gia_Man_t * pIni, * pSrm, * pTemp;
343  Cec_ManFra_t * p;
344  Cec_ManSim_t * pSim;
345  Cec_ManPat_t * pPat;
346  int i, fTimeOut = 0, nMatches = 0;
347  abctime clk, clk2, clkTotal = Abc_Clock();
348 
349  // duplicate AIG and transfer equivalence classes
350  Gia_ManRandom( 1 );
351  pIni = Gia_ManDup(pAig);
352  pIni->pReprs = pAig->pReprs; pAig->pReprs = NULL;
353  pIni->pNexts = pAig->pNexts; pAig->pNexts = NULL;
354 
355  // prepare the managers
356  // SAT sweeping
357  p = Cec_ManFraStart( pIni, pPars );
358  if ( pPars->fDualOut )
359  pPars->fColorDiff = 1;
360  // simulation
361  Cec_ManSimSetDefaultParams( pParsSim );
362  pParsSim->nWords = pPars->nWords;
363  pParsSim->nFrames = pPars->nRounds;
364  pParsSim->fCheckMiter = pPars->fCheckMiter;
365  pParsSim->fDualOut = pPars->fDualOut;
366  pParsSim->fVerbose = pPars->fVerbose;
367  pSim = Cec_ManSimStart( p->pAig, pParsSim );
368  // SAT solving
369  Cec_ManSatSetDefaultParams( pParsSat );
370  pParsSat->nBTLimit = pPars->nBTLimit;
371  pParsSat->fVerbose = pPars->fVeryVerbose;
372  // simulation patterns
373  pPat = Cec_ManPatStart();
374  pPat->fVerbose = pPars->fVeryVerbose;
375 
376  // start equivalence classes
377 clk = Abc_Clock();
378  if ( p->pAig->pReprs == NULL )
379  {
380  if ( Cec_ManSimClassesPrepare(pSim, -1) || Cec_ManSimClassesRefine(pSim) )
381  {
382  Gia_ManStop( p->pAig );
383  p->pAig = NULL;
384  goto finalize;
385  }
386  }
387 p->timeSim += Abc_Clock() - clk;
388  // perform solving
389  for ( i = 1; i <= pPars->nItersMax; i++ )
390  {
391  clk2 = Abc_Clock();
392  nMatches = 0;
393  if ( pPars->fDualOut )
394  {
395  nMatches = Gia_ManEquivSetColors( p->pAig, pPars->fVeryVerbose );
396 // p->pAig->pIso = Cec_ManDetectIsomorphism( p->pAig );
397 // Gia_ManEquivTransform( p->pAig, 1 );
398  }
399  pSrm = Cec_ManFraSpecReduction( p );
400 
401 // Gia_AigerWrite( pSrm, "gia_srm.aig", 0, 0 );
402 
403  if ( pPars->fVeryVerbose )
404  Gia_ManPrintStats( pSrm, NULL );
405  if ( Gia_ManCoNum(pSrm) == 0 )
406  {
407  Gia_ManStop( pSrm );
408  if ( p->pPars->fVerbose )
409  Abc_Print( 1, "Considered all available candidate equivalences.\n" );
410  if ( pPars->fDualOut && Gia_ManAndNum(p->pAig) > 0 )
411  {
412  if ( pPars->fColorDiff )
413  {
414  if ( p->pPars->fVerbose )
415  Abc_Print( 1, "Switching into reduced mode.\n" );
416  pPars->fColorDiff = 0;
417  }
418  else
419  {
420  if ( p->pPars->fVerbose )
421  Abc_Print( 1, "Switching into normal mode.\n" );
422  pPars->fDualOut = 0;
423  }
424  continue;
425  }
426  break;
427  }
428 clk = Abc_Clock();
429  if ( pPars->fRunCSat )
430  Cec_ManSatSolveCSat( pPat, pSrm, pParsSat );
431  else
432  Cec_ManSatSolve( pPat, pSrm, pParsSat );
433 p->timeSat += Abc_Clock() - clk;
434  if ( Cec_ManFraClassesUpdate( p, pSim, pPat, pSrm ) )
435  {
436  Gia_ManStop( pSrm );
437  Gia_ManStop( p->pAig );
438  p->pAig = NULL;
439  goto finalize;
440  }
441  Gia_ManStop( pSrm );
442 
443  // update the manager
444  pSim->pAig = p->pAig = Gia_ManEquivReduceAndRemap( pTemp = p->pAig, 0, pParsSim->fDualOut );
445  if ( p->pAig == NULL )
446  {
447  p->pAig = pTemp;
448  break;
449  }
450  Gia_ManStop( pTemp );
451  if ( p->pPars->fVerbose )
452  {
453  Abc_Print( 1, "%3d : P =%7d. D =%7d. F =%6d. M = %7d. And =%8d. ",
454  i, p->nAllProved, p->nAllDisproved, p->nAllFailed, nMatches, Gia_ManAndNum(p->pAig) );
455  Abc_PrintTime( 1, "Time", Abc_Clock() - clk2 );
456  }
457  if ( Gia_ManAndNum(p->pAig) == 0 )
458  {
459  if ( p->pPars->fVerbose )
460  Abc_Print( 1, "Network after reduction is empty.\n" );
461  break;
462  }
463  // check resource limits
464  if ( p->pPars->TimeLimit && (Abc_Clock() - clkTotal)/CLOCKS_PER_SEC >= p->pPars->TimeLimit )
465  {
466  fTimeOut = 1;
467  break;
468  }
469 // if ( p->nAllFailed && !p->nAllProved && !p->nAllDisproved )
470  if ( p->nAllFailed > p->nAllProved + p->nAllDisproved )
471  {
472  if ( pParsSat->nBTLimit >= 10001 )
473  break;
474  if ( pPars->fSatSweeping )
475  {
476  if ( p->pPars->fVerbose )
477  Abc_Print( 1, "Exceeded the limit on the number of conflicts (%d).\n", pParsSat->nBTLimit );
478  break;
479  }
480  pParsSat->nBTLimit *= 10;
481  if ( p->pPars->fVerbose )
482  {
483  if ( p->pPars->fVerbose )
484  Abc_Print( 1, "Increasing conflict limit to %d.\n", pParsSat->nBTLimit );
485  if ( fOutputResult )
486  {
487  Gia_AigerWrite( p->pAig, "gia_cec_temp.aig", 0, 0 );
488  Abc_Print( 1,"The result is written into file \"%s\".\n", "gia_cec_temp.aig" );
489  }
490  }
491  }
492  if ( pPars->fDualOut && pPars->fColorDiff && (Gia_ManAndNum(p->pAig) < 100000 || p->nAllProved + p->nAllDisproved < 10) )
493  {
494  if ( p->pPars->fVerbose )
495  Abc_Print( 1, "Switching into reduced mode.\n" );
496  pPars->fColorDiff = 0;
497  }
498 // if ( pPars->fDualOut && Gia_ManAndNum(p->pAig) < 20000 )
499  else if ( pPars->fDualOut && (Gia_ManAndNum(p->pAig) < 20000 || p->nAllProved + p->nAllDisproved < 10) )
500  {
501  if ( p->pPars->fVerbose )
502  Abc_Print( 1, "Switching into normal mode.\n" );
503  pPars->fColorDiff = 0;
504  pPars->fDualOut = 0;
505  }
506  }
507 finalize:
508  if ( p->pPars->fVerbose && p->pAig )
509  {
510  Abc_Print( 1, "NBeg = %d. NEnd = %d. (Gain = %6.2f %%). RBeg = %d. REnd = %d. (Gain = %6.2f %%).\n",
511  Gia_ManAndNum(pAig), Gia_ManAndNum(p->pAig),
512  100.0*(Gia_ManAndNum(pAig)-Gia_ManAndNum(p->pAig))/(Gia_ManAndNum(pAig)?Gia_ManAndNum(pAig):1),
513  Gia_ManRegNum(pAig), Gia_ManRegNum(p->pAig),
514  100.0*(Gia_ManRegNum(pAig)-Gia_ManRegNum(p->pAig))/(Gia_ManRegNum(pAig)?Gia_ManRegNum(pAig):1) );
515  Abc_PrintTimeP( 1, "Sim ", p->timeSim, Abc_Clock() - (int)clkTotal );
516  Abc_PrintTimeP( 1, "Sat ", p->timeSat-pPat->timeTotalSave, Abc_Clock() - (int)clkTotal );
517  Abc_PrintTimeP( 1, "Pat ", p->timePat+pPat->timeTotalSave, Abc_Clock() - (int)clkTotal );
518  Abc_PrintTime( 1, "Time", (int)(Abc_Clock() - clkTotal) );
519  }
520 
521  pTemp = p->pAig; p->pAig = NULL;
522  if ( pTemp == NULL && pSim->iOut >= 0 )
523  {
524  Abc_Print( 1, "Disproved at least one output of the miter (zero-based number %d).\n", pSim->iOut );
525  pPars->iOutFail = pSim->iOut;
526  }
527  else if ( pSim->pCexes )
528  Abc_Print( 1, "Disproved %d outputs of the miter.\n", pSim->nOuts );
529  if ( fTimeOut )
530  Abc_Print( 1, "Timed out after %d seconds.\n", (int)((double)Abc_Clock() - clkTotal)/CLOCKS_PER_SEC );
531 
532  pAig->pCexComb = pSim->pCexComb; pSim->pCexComb = NULL;
533  Cec_ManSimStop( pSim );
534  Cec_ManPatStop( pPat );
535  Cec_ManFraStop( p );
536  return pTemp;
537 }
538 
539 
540 ////////////////////////////////////////////////////////////////////////
541 /// END OF FILE ///
542 ////////////////////////////////////////////////////////////////////////
543 
544 
545 ABC_NAMESPACE_IMPL_END
546 
memset
char * memset()
Cec_ManSim_t_::pCexComb
Abc_Cex_t * pCexComb
Definition: cecInt.h:133
Cec_ParCor_t_::nRounds
int nRounds
Definition: cec.h:136
Cec_ParSim_t_::fVerbose
int fVerbose
Definition: cec.h:73
Cec_ParSmf_t_::nFrames
int nFrames
Definition: cec.h:82
Gia_ManEquivCountLits
int Gia_ManEquivCountLits(Gia_Man_t *p)
Definition: giaEquiv.c:253
Cec_ParChc_t_::fUseCSat
int fUseCSat
Definition: cec.h:166
Cec_ParSim_t_::TimeLimit
int TimeLimit
Definition: cec.h:65
Cec_ManSimClassesPrepare
int Cec_ManSimClassesPrepare(Cec_ManSim_t *p, int LevelMax)
Definition: cecClass.c:851
Cec_ParSim_t_::fVeryVerbose
int fVeryVerbose
Definition: cec.h:72
Gia_ManDup
Gia_Man_t * Gia_ManDup(Gia_Man_t *p)
Definition: giaDup.c:552
Gia_ManStop
void Gia_ManStop(Gia_Man_t *p)
Definition: giaMan.c:77
Gia_ManEquivReduceAndRemap
Gia_Man_t * Gia_ManEquivReduceAndRemap(Gia_Man_t *p, int fSeq, int fMiterPairs)
Definition: giaEquiv.c:638
Gia_ManPrintStats
void Gia_ManPrintStats(Gia_Man_t *p, Gps_Par_t *pPars)
Definition: giaMan.c:389
Gia_Man_t_::pNexts
int * pNexts
Definition: gia.h:122
Cec_ParCor_t_::fUseCSat
int fUseCSat
Definition: cec.h:146
Cec_ParSim_t_::fSeqSimulate
int fSeqSimulate
Definition: cec.h:69
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Cec_ParCor_t_
Definition: cec.h:133
Cec_ParCec_t_::nBTLimit
int nBTLimit
Definition: cec.h:120
Cec_ParCor_t_::fVeryVerbose
int fVeryVerbose
Definition: cec.h:151
Cec_ManFra_t_::timeSim
abctime timeSim
Definition: cecInt.h:157
Cec_ParCec_t_::fUseSmartCnf
int fUseSmartCnf
Definition: cec.h:123
Cec_ParSmf_t_::nRounds
int nRounds
Definition: cec.h:81
Cec_ParCor_t_::fUseRings
int fUseRings
Definition: cec.h:144
Cec_ManFraClassesUpdate
int Cec_ManFraClassesUpdate(Cec_ManFra_t *p, Cec_ManSim_t *pSim, Cec_ManPat_t *pPat, Gia_Man_t *pNew)
Definition: cecSweep.c:188
Cec_ManSatSolve
void Cec_ManSatSolve(Cec_ManPat_t *pPat, Gia_Man_t *pAig, Cec_ParSat_t *pPars)
Definition: cecSolve.c:676
Cec_ManSim_t_
Definition: cecInt.h:112
Cec_ParFra_t_::TimeLimit
int TimeLimit
Definition: cec.h:101
Cec_ParCor_t_::fConstCorr
int fConstCorr
Definition: cec.h:143
Cec_ManSatSolving
Gia_Man_t * Cec_ManSatSolving(Gia_Man_t *pAig, Cec_ParSat_t *pPars)
Definition: cecCore.c:234
Gia_Man_t_::pCexComb
Abc_Cex_t * pCexComb
Definition: gia.h:135
Cec_ParCec_t_::fVeryVerbose
int fVeryVerbose
Definition: cec.h:126
Cec_ManSimStop
void Cec_ManSimStop(Cec_ManSim_t *p)
Definition: cecMan.c:232
Cec_ManFra_t_::nAllFailed
int nAllFailed
Definition: cecInt.h:155
Cec_ManSim_t_::pAig
Gia_Man_t * pAig
Definition: cecInt.h:115
Cec_ParChc_t_::fUseRings
int fUseRings
Definition: cec.h:165
Cec_ManSimulation
void Cec_ManSimulation(Gia_Man_t *pAig, Cec_ParSim_t *pPars)
Definition: cecCore.c:284
Abc_Clock
static abctime Abc_Clock()
Definition: abc_global.h:279
Abc_PrintTimeP
static void Abc_PrintTimeP(int level, const char *pStr, abctime time, abctime Time)
Definition: abc_global.h:372
Cec_ManSatSolveCSat
void Cec_ManSatSolveCSat(Cec_ManPat_t *pPat, Gia_Man_t *pAig, Cec_ParSat_t *pPars)
Definition: cecSolve.c:765
Cec_ManCorSetDefaultParams
void Cec_ManCorSetDefaultParams(Cec_ParCor_t *p)
Definition: cecCore.c:181
Cec_ParFra_t_::fRunCSat
int fRunCSat
Definition: cec.h:110
Cec_ManFra_t_
Definition: cecInt.h:146
Cec_ParFra_t_
Definition: cec.h:95
Cec_ParSim_t_::fCheckMiter
int fCheckMiter
Definition: cec.h:67
Cec_ManFra_t_::timeSat
abctime timeSat
Definition: cecInt.h:159
Cec_ParCor_t_::fLatchCorr
int fLatchCorr
Definition: cec.h:142
Cec_ParCor_t_::fVerbose
int fVerbose
Definition: cec.h:152
Cec_ParFra_t_::fVerbose
int fVerbose
Definition: cec.h:112
Cec_ManSimStart
Cec_ManSim_t * Cec_ManSimStart(Gia_Man_t *pAig, Cec_ParSim_t *pPars)
Definition: cecMan.c:198
Gia_ManRandom
unsigned Gia_ManRandom(int fReset)
FUNCTION DEFINITIONS ///.
Definition: giaUtil.c:49
Cec_ManFraSetDefaultParams
void Cec_ManFraSetDefaultParams(Cec_ParFra_t *p)
Definition: cecCore.c:125
Cec_ManSatSetDefaultParams
ABC_NAMESPACE_IMPL_START void Cec_ManSatSetDefaultParams(Cec_ParSat_t *p)
DECLARATIONS ///.
Definition: cecCore.c:45
Cec_ParChc_t_::nRounds
int nRounds
Definition: cec.h:163
Cec_ParChc_t_::nWords
int nWords
Definition: cec.h:162
Abc_PrintTime
static void Abc_PrintTime(int level, const char *pStr, abctime time)
Definition: abc_global.h:367
Cec_ManChcSetDefaultParams
void Cec_ManChcSetDefaultParams(Cec_ParChc_t *p)
Definition: cecCore.c:211
Gia_ManAndNum
static int Gia_ManAndNum(Gia_Man_t *p)
Definition: gia.h:389
Cec_ManFra_t_::nAllDisproved
int nAllDisproved
Definition: cecInt.h:154
Cec_ParChc_t_::nBTLimit
int nBTLimit
Definition: cec.h:164
Cec_ParSmf_t_
Definition: cec.h:78
Cec_ParFra_t_::fDualOut
int fDualOut
Definition: cec.h:107
Cec_ParSim_t_::fConstCorr
int fConstCorr
Definition: cec.h:71
Cec_ParCec_t_::fRewriting
int fRewriting
Definition: cec.h:124
Cec_ParChc_t_
Definition: cec.h:160
Cec_ManSimSetDefaultParams
void Cec_ManSimSetDefaultParams(Cec_ParSim_t *p)
Definition: cecCore.c:70
Cec_ParFra_t_::fColorDiff
int fColorDiff
Definition: cec.h:108
Cec_ParCor_t_::nFrames
int nFrames
Definition: cec.h:137
Cec_ManSatSweeping
Gia_Man_t * Cec_ManSatSweeping(Gia_Man_t *pAig, Cec_ParFra_t *pPars)
Definition: cecCore.c:337
Cec_ParSmf_t_::nBTLimit
int nBTLimit
Definition: cec.h:85
Cec_ManPat_t
typedefABC_NAMESPACE_HEADER_START struct Cec_ManPat_t_ Cec_ManPat_t
INCLUDES ///.
Definition: cecInt.h:48
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
Cec_ParCor_t_::nLevelMax
int nLevelMax
Definition: cec.h:140
Cec_ParCec_t_::TimeLimit
int TimeLimit
Definition: cec.h:121
Cec_ManSim_t_::pCexes
void ** pCexes
Definition: cecInt.h:130
Abc_Print
static void Abc_Print(int level, const char *format,...)
Definition: abc_global.h:313
Gia_AigerWrite
void Gia_AigerWrite(Gia_Man_t *p, char *pFileName, int fWriteSymbols, int fCompact)
Definition: giaAiger.c:1024
Cec_ParCec_t_
Definition: cec.h:118
Cec_ManCountNonConstOutputs
int Cec_ManCountNonConstOutputs(Gia_Man_t *pAig)
Definition: cecSeq.c:272
Cec_ParFra_t_::nWords
int nWords
Definition: cec.h:97
Cec_ParSmf_t_::fVerbose
int fVerbose
Definition: cec.h:90
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
Cec_ParCor_t_::nWords
int nWords
Definition: cec.h:135
Cec_ManSmfSetDefaultParams
void Cec_ManSmfSetDefaultParams(Cec_ParSmf_t *p)
Definition: cecCore.c:98
Cec_ParCec_t_::iOutFail
int iOutFail
Definition: cec.h:128
Cec_ManSimClassesRefine
int Cec_ManSimClassesRefine(Cec_ManSim_t *p)
Definition: cecClass.c:908
Cec_ManSimulationOne
int Cec_ManSimulationOne(Gia_Man_t *pAig, Cec_ParSim_t *pPars)
Definition: cecCore.c:257
Cec_ParSmf_t_::fCheckMiter
int fCheckMiter
Definition: cec.h:88
Cec_ParFra_t_::nRounds
int nRounds
Definition: cec.h:98
Cec_ParSmf_t_::TimeLimit
int TimeLimit
Definition: cec.h:86
Cec_ParCor_t_::fUseSmartCnf
int fUseSmartCnf
Definition: cec.h:148
Cec_ManFraSpecReduction
Gia_Man_t * Cec_ManFraSpecReduction(Cec_ManFra_t *p)
DECLARATIONS ///.
Definition: cecSweep.c:45
Cec_ParSmf_t_::nWords
int nWords
Definition: cec.h:80
Cec_ParSim_t_::nFrames
int nFrames
Definition: cec.h:62
Cec_ParFra_t_::nBTLimit
int nBTLimit
Definition: cec.h:100
Cec_ManFraStop
void Cec_ManFraStop(Cec_ManFra_t *p)
Definition: cecMan.c:284
Cec_ParFra_t_::nItersMax
int nItersMax
Definition: cec.h:99
Cec_ParCor_t_::nBTLimit
int nBTLimit
Definition: cec.h:139
Gia_Man_t_
Definition: gia.h:95
Cec_ParFra_t_::fCheckMiter
int fCheckMiter
Definition: cec.h:105
Cec_ParSmf_t_::fDualOut
int fDualOut
Definition: cec.h:87
Cec_ParFra_t_::nDepthMax
int nDepthMax
Definition: cec.h:103
Cec_ParFra_t_::nLevelMax
int nLevelMax
Definition: cec.h:102
Cec_ManFra_t_::pAig
Gia_Man_t * pAig
Definition: cecInt.h:149
Cec_ManSim_t_::iOut
int iOut
Definition: cecInt.h:131
Cec_ManCecSetDefaultParams
void Cec_ManCecSetDefaultParams(Cec_ParCec_t *p)
Definition: cecCore.c:157
Cec_ParCec_t_::fVerbose
int fVerbose
Definition: cec.h:127
Cec_ParSim_t_::nNonRefines
int nNonRefines
Definition: cec.h:64
Cec_ParSim_t_::fDualOut
int fDualOut
Definition: cec.h:66
Cec_ManFraStart
Cec_ManFra_t * Cec_ManFraStart(Gia_Man_t *pAig, Cec_ParFra_t *pPars)
Definition: cecMan.c:262
Cec_ParSat_t
typedefABC_NAMESPACE_HEADER_START struct Cec_ParSat_t_ Cec_ParSat_t
INCLUDES ///.
Definition: cec.h:43
Gia_Man_t_::pReprs
Gia_Rpr_t * pReprs
Definition: gia.h:121
Cec_ParSmf_t_::nMinOutputs
int nMinOutputs
Definition: cec.h:84
assert
#define assert(ex)
Definition: util_old.h:213
Cec_ParSim_t_::nRounds
int nRounds
Definition: cec.h:63
Cec_ParSim_t_
Definition: cec.h:59
Gia_ManEquivSetColors
int Gia_ManEquivSetColors(Gia_Man_t *p, int fVerbose)
Definition: giaEquiv.c:692
Cec_ParSmf_t_::nNonRefines
int nNonRefines
Definition: cec.h:83
Cec_ManFra_t_::timePat
abctime timePat
Definition: cecInt.h:158
Cec_ParSim_t_::nWords
int nWords
Definition: cec.h:61
Cec_ParCor_t_::nStepsMax
int nStepsMax
Definition: cec.h:141
Cec_ParFra_t_::fSatSweeping
int fSatSweeping
Definition: cec.h:109
Cec_ManSim_t_::nOuts
int nOuts
Definition: cecInt.h:132
abctime
ABC_INT64_T abctime
Definition: abc_global.h:278
Cec_ManFra_t_::nAllProved
int nAllProved
Definition: cecInt.h:153
Cec_ParChc_t_::fVeryVerbose
int fVeryVerbose
Definition: cec.h:167
Cec_ManPatStop
void Cec_ManPatStop(Cec_ManPat_t *p)
Definition: cecMan.c:177
Cec_ParChc_t_::fVerbose
int fVerbose
Definition: cec.h:168
Cec_ParFra_t_::fRewriting
int fRewriting
Definition: cec.h:104
Cec_ParFra_t_::fVeryVerbose
int fVeryVerbose
Definition: cec.h:111
Gia_ManCoNum
static int Gia_ManCoNum(Gia_Man_t *p)
Definition: gia.h:384
Cec_ParFra_t_::iOutFail
int iOutFail
Definition: cec.h:113
Cec_ManFra_t_::pPars
Cec_ParFra_t * pPars
Definition: cecInt.h:150
Cec_ManPatStart
Cec_ManPat_t * Cec_ManPatStart()
Definition: cecMan.c:129
Gia_ManRegNum
static int Gia_ManRegNum(Gia_Man_t *p)
Definition: gia.h:387