abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
fraigMan.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [fraigMan.c]
4 
5  PackageName [FRAIG: Functionally reduced AND-INV graphs.]
6 
7  Synopsis [Implementation of the FRAIG manager.]
8 
9  Author [Alan Mishchenko <alanmi@eecs.berkeley.edu>]
10 
11  Affiliation [UC Berkeley]
12 
13  Date [Ver. 2.0. Started - October 1, 2004]
14 
15  Revision [$Id: fraigMan.c,v 1.11 2005/07/08 01:01:31 alanmi Exp $]
16 
17 ***********************************************************************/
18 
19 #include "fraigInt.h"
20 
21 ABC_NAMESPACE_IMPL_START
22 
23 
24 ////////////////////////////////////////////////////////////////////////
25 /// DECLARATIONS ///
26 ////////////////////////////////////////////////////////////////////////
27 
28 abctime timeSelect;
29 abctime timeAssign;
30 
31 ////////////////////////////////////////////////////////////////////////
32 /// FUNCTION DEFINITIONS ///
33 ////////////////////////////////////////////////////////////////////////
34 
35 /**Function*************************************************************
36 
37  Synopsis [Sets the default parameters of the package.]
38 
39  Description [This set of parameters is tuned for equivalence checking.]
40 
41  SideEffects []
42 
43  SeeAlso []
44 
45 ***********************************************************************/
46 void Prove_ParamsSetDefault( Prove_Params_t * pParams )
47 {
48  // clean the parameter structure
49  memset( pParams, 0, sizeof(Prove_Params_t) );
50  // general parameters
51  pParams->fUseFraiging = 1; // enables fraiging
52  pParams->fUseRewriting = 1; // enables rewriting
53  pParams->fUseBdds = 0; // enables BDD construction when other methods fail
54  pParams->fVerbose = 0; // prints verbose stats
55  // iterations
56  pParams->nItersMax = 6; // the number of iterations
57  // mitering
58  pParams->nMiteringLimitStart = 5000; // starting mitering limit
59  pParams->nMiteringLimitMulti = 2.0; // multiplicative coefficient to increase the limit in each iteration
60  // rewriting (currently not used)
61  pParams->nRewritingLimitStart = 3; // the number of rewriting iterations
62  pParams->nRewritingLimitMulti = 1.0; // multiplicative coefficient to increase the limit in each iteration
63  // fraiging
64  pParams->nFraigingLimitStart = 2; // starting backtrack(conflict) limit
65  pParams->nFraigingLimitMulti = 8.0; // multiplicative coefficient to increase the limit in each iteration
66  // last-gasp BDD construction
67  pParams->nBddSizeLimit = 1000000; // the number of BDD nodes when construction is aborted
68  pParams->fBddReorder = 1; // enables dynamic BDD variable reordering
69  // last-gasp mitering
70 // pParams->nMiteringLimitLast = 1000000; // final mitering limit
71  pParams->nMiteringLimitLast = 0; // final mitering limit
72  // global SAT solver limits
73  pParams->nTotalBacktrackLimit = 0; // global limit on the number of backtracks
74  pParams->nTotalInspectLimit = 0; // global limit on the number of clause inspects
75 // pParams->nTotalInspectLimit = 100000000; // global limit on the number of clause inspects
76 }
77 
78 /**Function*************************************************************
79 
80  Synopsis [Prints out the current values of CEC engine parameters.]
81 
82  Description []
83 
84  SideEffects []
85 
86  SeeAlso []
87 
88 ***********************************************************************/
89 void Prove_ParamsPrint( Prove_Params_t * pParams )
90 {
91  printf( "CEC enging parameters:\n" );
92  printf( "Fraiging enabled: %s\n", pParams->fUseFraiging? "yes":"no" );
93  printf( "Rewriting enabled: %s\n", pParams->fUseRewriting? "yes":"no" );
94  printf( "BDD construction enabled: %s\n", pParams->fUseBdds? "yes":"no" );
95  printf( "Verbose output enabled: %s\n", pParams->fVerbose? "yes":"no" );
96  printf( "Solver iterations: %d\n", pParams->nItersMax );
97  printf( "Starting mitering limit: %d\n", pParams->nMiteringLimitStart );
98  printf( "Multiplicative coeficient for mitering: %.2f\n", pParams->nMiteringLimitMulti );
99  printf( "Starting number of rewriting iterations: %d\n", pParams->nRewritingLimitStart );
100  printf( "Multiplicative coeficient for rewriting: %.2f\n", pParams->nRewritingLimitMulti );
101  printf( "Starting number of conflicts in fraiging: %.2f\n", pParams->nFraigingLimitMulti );
102  printf( "Multiplicative coeficient for fraiging: %.2f\n", pParams->nRewritingLimitMulti );
103  printf( "BDD size limit for bailing out: %d\n", pParams->nBddSizeLimit );
104  printf( "BDD reordering enabled: %s\n", pParams->fBddReorder? "yes":"no" );
105  printf( "Last-gasp mitering limit: %d\n", pParams->nMiteringLimitLast );
106  printf( "Total conflict limit: %d\n", (int)pParams->nTotalBacktrackLimit );
107  printf( "Total inspection limit: %d\n", (int)pParams->nTotalInspectLimit );
108  printf( "Parameter dump complete.\n" );
109 }
110 
111 /**Function*************************************************************
112 
113  Synopsis [Sets the default parameters of the package.]
114 
115  Description [This set of parameters is tuned for equivalence checking.]
116 
117  SideEffects []
118 
119  SeeAlso []
120 
121 ***********************************************************************/
122 void Fraig_ParamsSetDefault( Fraig_Params_t * pParams )
123 {
124  memset( pParams, 0, sizeof(Fraig_Params_t) );
125  pParams->nPatsRand = FRAIG_PATTERNS_RANDOM; // the number of words of random simulation info
126  pParams->nPatsDyna = FRAIG_PATTERNS_DYNAMIC; // the number of words of dynamic simulation info
127  pParams->nBTLimit = 99; // the max number of backtracks to perform
128  pParams->nSeconds = 20; // the max number of seconds to solve the miter
129  pParams->fFuncRed = 1; // performs only one level hashing
130  pParams->fFeedBack = 1; // enables solver feedback
131  pParams->fDist1Pats = 1; // enables distance-1 patterns
132  pParams->fDoSparse = 0; // performs equiv tests for sparse functions
133  pParams->fChoicing = 0; // enables recording structural choices
134  pParams->fTryProve = 1; // tries to solve the final miter
135  pParams->fVerbose = 0; // the verbosiness flag
136  pParams->fVerboseP = 0; // the verbose flag for reporting the proof
137  pParams->fInternal = 0; // the flag indicates the internal run
138  pParams->nConfLimit = 0; // the limit on the number of conflicts
139  pParams->nInspLimit = 0; // the limit on the number of inspections
140 }
141 
142 /**Function*************************************************************
143 
144  Synopsis [Sets the default parameters of the package.]
145 
146  Description [This set of parameters is tuned for complete FRAIGing.]
147 
148  SideEffects []
149 
150  SeeAlso []
151 
152 ***********************************************************************/
153 void Fraig_ParamsSetDefaultFull( Fraig_Params_t * pParams )
154 {
155  memset( pParams, 0, sizeof(Fraig_Params_t) );
156  pParams->nPatsRand = FRAIG_PATTERNS_RANDOM; // the number of words of random simulation info
157  pParams->nPatsDyna = FRAIG_PATTERNS_DYNAMIC; // the number of words of dynamic simulation info
158  pParams->nBTLimit = -1; // the max number of backtracks to perform
159  pParams->nSeconds = 20; // the max number of seconds to solve the miter
160  pParams->fFuncRed = 1; // performs only one level hashing
161  pParams->fFeedBack = 1; // enables solver feedback
162  pParams->fDist1Pats = 1; // enables distance-1 patterns
163  pParams->fDoSparse = 1; // performs equiv tests for sparse functions
164  pParams->fChoicing = 0; // enables recording structural choices
165  pParams->fTryProve = 0; // tries to solve the final miter
166  pParams->fVerbose = 0; // the verbosiness flag
167  pParams->fVerboseP = 0; // the verbose flag for reporting the proof
168  pParams->fInternal = 0; // the flag indicates the internal run
169  pParams->nConfLimit = 0; // the limit on the number of conflicts
170  pParams->nInspLimit = 0; // the limit on the number of inspections
171 }
172 
173 /**Function*************************************************************
174 
175  Synopsis [Creates the new FRAIG manager.]
176 
177  Description []
178 
179  SideEffects []
180 
181  SeeAlso []
182 
183 ***********************************************************************/
184 Fraig_Man_t * Fraig_ManCreate( Fraig_Params_t * pParams )
185 {
186  Fraig_Params_t Params;
187  Fraig_Man_t * p;
188 
189  // set the random seed for simulation
190 // srand( 0xFEEDDEAF );
191 // srand( 0xDEADCAFE );
192  Aig_ManRandom( 1 );
193 
194  // set parameters for equivalence checking
195  if ( pParams == NULL )
196  Fraig_ParamsSetDefault( pParams = &Params );
197  // adjust the amount of simulation info
198  if ( pParams->nPatsRand < 128 )
199  pParams->nPatsRand = 128;
200  if ( pParams->nPatsRand > 32768 )
201  pParams->nPatsRand = 32768;
202  if ( pParams->nPatsDyna < 128 )
203  pParams->nPatsDyna = 128;
204  if ( pParams->nPatsDyna > 32768 )
205  pParams->nPatsDyna = 32768;
206  // if reduction is not performed, allocate minimum simulation info
207  if ( !pParams->fFuncRed )
208  pParams->nPatsRand = pParams->nPatsDyna = 128;
209 
210  // start the manager
211  p = ABC_ALLOC( Fraig_Man_t, 1 );
212  memset( p, 0, sizeof(Fraig_Man_t) );
213 
214  // set the default parameters
215  p->nWordsRand = FRAIG_NUM_WORDS( pParams->nPatsRand ); // the number of words of random simulation info
216  p->nWordsDyna = FRAIG_NUM_WORDS( pParams->nPatsDyna ); // the number of patterns for dynamic simulation info
217  p->nBTLimit = pParams->nBTLimit; // -1 means infinite backtrack limit
218  p->nSeconds = pParams->nSeconds; // the timeout for the final miter
219  p->fFuncRed = pParams->fFuncRed; // enables functional reduction (otherwise, only one-level hashing is performed)
220  p->fFeedBack = pParams->fFeedBack; // enables solver feedback (the use of counter-examples in simulation)
221  p->fDist1Pats = pParams->fDist1Pats; // enables solver feedback (the use of counter-examples in simulation)
222  p->fDoSparse = pParams->fDoSparse; // performs equivalence checking for sparse functions (whose sim-info is 0)
223  p->fChoicing = pParams->fChoicing; // disable accumulation of structural choices (keeps only the first choice)
224  p->fTryProve = pParams->fTryProve; // disable accumulation of structural choices (keeps only the first choice)
225  p->fVerbose = pParams->fVerbose; // disable verbose output
226  p->fVerboseP = pParams->fVerboseP; // disable verbose output
227  p->nInspLimit = pParams->nInspLimit; // the limit on the number of inspections
228 
229  // start memory managers
230  p->mmNodes = Fraig_MemFixedStart( sizeof(Fraig_Node_t) );
231  p->mmSims = Fraig_MemFixedStart( sizeof(unsigned) * (p->nWordsRand + p->nWordsDyna) );
232  // allocate node arrays
233  p->vInputs = Fraig_NodeVecAlloc( 1000 ); // the array of primary inputs
234  p->vOutputs = Fraig_NodeVecAlloc( 1000 ); // the array of primary outputs
235  p->vNodes = Fraig_NodeVecAlloc( 1000 ); // the array of internal nodes
236  // start the tables
237  p->pTableS = Fraig_HashTableCreate( 1000 ); // hashing by structure
238  p->pTableF = Fraig_HashTableCreate( 1000 ); // hashing by function
239  p->pTableF0 = Fraig_HashTableCreate( 1000 ); // hashing by function (for sparse functions)
240  // create the constant node
241  p->pConst1 = Fraig_NodeCreateConst( p );
242  // initialize SAT solver feedback data structures
243  Fraig_FeedBackInit( p );
244  // initialize other variables
245  p->vProj = Msat_IntVecAlloc( 10 );
246  p->nTravIds = 1;
247  p->nTravIds2 = 1;
248  return p;
249 }
250 
251 /**Function*************************************************************
252 
253  Synopsis [Deallocates the mapping manager.]
254 
255  Description []
256 
257  SideEffects []
258 
259  SeeAlso []
260 
261 ***********************************************************************/
262 void Fraig_ManFree( Fraig_Man_t * p )
263 {
264  int i;
265  if ( p->fVerbose )
266  {
267  if ( p->fChoicing ) Fraig_ManReportChoices( p );
268  Fraig_ManPrintStats( p );
269 // Fraig_TablePrintStatsS( p );
270 // Fraig_TablePrintStatsF( p );
271 // Fraig_TablePrintStatsF0( p );
272  }
273 
274  for ( i = 0; i < p->vNodes->nSize; i++ )
275  if ( p->vNodes->pArray[i]->vFanins )
276  {
277  Fraig_NodeVecFree( p->vNodes->pArray[i]->vFanins );
278  p->vNodes->pArray[i]->vFanins = NULL;
279  }
280 
281  if ( p->vInputs ) Fraig_NodeVecFree( p->vInputs );
282  if ( p->vNodes ) Fraig_NodeVecFree( p->vNodes );
283  if ( p->vOutputs ) Fraig_NodeVecFree( p->vOutputs );
284 
285  if ( p->pTableS ) Fraig_HashTableFree( p->pTableS );
286  if ( p->pTableF ) Fraig_HashTableFree( p->pTableF );
287  if ( p->pTableF0 ) Fraig_HashTableFree( p->pTableF0 );
288 
289  if ( p->pSat ) Msat_SolverFree( p->pSat );
290  if ( p->vProj ) Msat_IntVecFree( p->vProj );
291  if ( p->vCones ) Fraig_NodeVecFree( p->vCones );
292  if ( p->vPatsReal ) Msat_IntVecFree( p->vPatsReal );
293  if ( p->pModel ) ABC_FREE( p->pModel );
294 
295  Fraig_MemFixedStop( p->mmNodes, 0 );
296  Fraig_MemFixedStop( p->mmSims, 0 );
297 
298  if ( p->pSuppS )
299  {
300  ABC_FREE( p->pSuppS[0] );
301  ABC_FREE( p->pSuppS );
302  }
303  if ( p->pSuppF )
304  {
305  ABC_FREE( p->pSuppF[0] );
306  ABC_FREE( p->pSuppF );
307  }
308 
309  ABC_FREE( p->ppOutputNames );
310  ABC_FREE( p->ppInputNames );
311  ABC_FREE( p );
312 }
313 
314 /**Function*************************************************************
315 
316  Synopsis [Prepares the SAT solver to run on the two nodes.]
317 
318  Description []
319 
320  SideEffects []
321 
322  SeeAlso []
323 
324 ***********************************************************************/
325 void Fraig_ManCreateSolver( Fraig_Man_t * p )
326 {
327  extern abctime timeSelect;
328  extern abctime timeAssign;
329  assert( p->pSat == NULL );
330  // allocate data for SAT solving
331  p->pSat = Msat_SolverAlloc( 500, 1, 1, 1, 1, 0 );
332  p->vVarsInt = Msat_SolverReadConeVars( p->pSat );
333  p->vAdjacents = Msat_SolverReadAdjacents( p->pSat );
334  p->vVarsUsed = Msat_SolverReadVarsUsed( p->pSat );
335  timeSelect = 0;
336  timeAssign = 0;
337 }
338 
339 
340 /**Function*************************************************************
341 
342  Synopsis [Deallocates the mapping manager.]
343 
344  Description []
345 
346  SideEffects []
347 
348  SeeAlso []
349 
350 ***********************************************************************/
351 void Fraig_ManPrintStats( Fraig_Man_t * p )
352 {
353  double nMemory;
354  nMemory = ((double)(p->vInputs->nSize + p->vNodes->nSize) *
355  (sizeof(Fraig_Node_t) + sizeof(unsigned)*(p->nWordsRand + p->nWordsDyna) /*+ p->nSuppWords*sizeof(unsigned)*/))/(1<<20);
356  printf( "Words: Random = %d. Dynamic = %d. Used = %d. Memory = %0.2f MB.\n",
357  p->nWordsRand, p->nWordsDyna, p->iWordPerm, nMemory );
358  printf( "Proof = %d. Counter-example = %d. Fail = %d. FailReal = %d. Zero = %d.\n",
359  p->nSatProof, p->nSatCounter, p->nSatFails, p->nSatFailsReal, p->nSatZeros );
360  printf( "Nodes: Final = %d. Total = %d. Mux = %d. (Exor = %d.) ClaVars = %d.\n",
361  Fraig_CountNodes(p,0), p->vNodes->nSize, Fraig_ManCountMuxes(p), Fraig_ManCountExors(p), p->nVarsClauses );
362  if ( p->pSat ) Msat_SolverPrintStats( p->pSat );
363  Fraig_PrintTime( "AIG simulation ", p->timeSims );
364  Fraig_PrintTime( "AIG traversal ", p->timeTrav );
365  Fraig_PrintTime( "Solver feedback ", p->timeFeed );
366  Fraig_PrintTime( "SAT solving ", p->timeSat );
367  Fraig_PrintTime( "Network update ", p->timeToNet );
368  Fraig_PrintTime( "TOTAL RUNTIME ", p->timeTotal );
369  if ( p->time1 > 0 ) { Fraig_PrintTime( "time1", p->time1 ); }
370  if ( p->time2 > 0 ) { Fraig_PrintTime( "time2", p->time2 ); }
371  if ( p->time3 > 0 ) { Fraig_PrintTime( "time3", p->time3 ); }
372  if ( p->time4 > 0 ) { Fraig_PrintTime( "time4", p->time4 ); }
373 // ABC_PRT( "Selection ", timeSelect );
374 // ABC_PRT( "Assignment", timeAssign );
375  fflush( stdout );
376 }
377 
378 /**Function*************************************************************
379 
380  Synopsis [Allocates simulation information for all nodes.]
381 
382  Description []
383 
384  SideEffects []
385 
386  SeeAlso []
387 
388 ***********************************************************************/
389 Fraig_NodeVec_t * Fraig_UtilInfoAlloc( int nSize, int nWords, int fClean )
390 {
391  Fraig_NodeVec_t * vInfo;
392  unsigned * pUnsigned;
393  int i;
394  assert( nSize > 0 && nWords > 0 );
395  vInfo = Fraig_NodeVecAlloc( nSize );
396  pUnsigned = ABC_ALLOC( unsigned, nSize * nWords );
397  vInfo->pArray[0] = (Fraig_Node_t *)pUnsigned;
398  if ( fClean )
399  memset( pUnsigned, 0, sizeof(unsigned) * nSize * nWords );
400  for ( i = 1; i < nSize; i++ )
401  vInfo->pArray[i] = (Fraig_Node_t *)(((unsigned *)vInfo->pArray[i-1]) + nWords);
402  vInfo->nSize = nSize;
403  return vInfo;
404 }
405 
406 /**Function*************************************************************
407 
408  Synopsis [Returns simulation info of all nodes.]
409 
410  Description []
411 
412  SideEffects []
413 
414  SeeAlso []
415 
416 ***********************************************************************/
417 Fraig_NodeVec_t * Fraig_ManGetSimInfo( Fraig_Man_t * p )
418 {
419  Fraig_NodeVec_t * vInfo;
420  Fraig_Node_t * pNode;
421  unsigned * pUnsigned;
422  int nRandom, nDynamic;
423  int i, k, nWords;
424 
425  nRandom = Fraig_ManReadPatternNumRandom( p );
426  nDynamic = Fraig_ManReadPatternNumDynamic( p );
427  nWords = nRandom / 32 + nDynamic / 32;
428 
429  vInfo = Fraig_UtilInfoAlloc( p->vNodes->nSize, nWords, 0 );
430  for ( i = 0; i < p->vNodes->nSize; i++ )
431  {
432  pNode = p->vNodes->pArray[i];
433  assert( i == pNode->Num );
434  pUnsigned = (unsigned *)vInfo->pArray[i];
435  for ( k = 0; k < nRandom / 32; k++ )
436  pUnsigned[k] = pNode->puSimR[k];
437  for ( k = 0; k < nDynamic / 32; k++ )
438  pUnsigned[nRandom / 32 + k] = pNode->puSimD[k];
439  }
440  return vInfo;
441 }
442 
443 /**Function*************************************************************
444 
445  Synopsis [Returns 1 if A v B is always true based on the siminfo.]
446 
447  Description [A v B is always true iff A' * B' is always false.]
448 
449  SideEffects []
450 
451  SeeAlso []
452 
453 ***********************************************************************/
454 int Fraig_ManCheckClauseUsingSimInfo( Fraig_Man_t * p, Fraig_Node_t * pNode1, Fraig_Node_t * pNode2 )
455 {
456  int fCompl1, fCompl2, i;
457 
458  fCompl1 = 1 ^ Fraig_IsComplement(pNode1) ^ Fraig_Regular(pNode1)->fInv;
459  fCompl2 = 1 ^ Fraig_IsComplement(pNode2) ^ Fraig_Regular(pNode2)->fInv;
460 
461  pNode1 = Fraig_Regular(pNode1);
462  pNode2 = Fraig_Regular(pNode2);
463  assert( pNode1 != pNode2 );
464 
465  // check the simulation info
466  if ( fCompl1 && fCompl2 )
467  {
468  for ( i = 0; i < p->nWordsRand; i++ )
469  if ( ~pNode1->puSimR[i] & ~pNode2->puSimR[i] )
470  return 0;
471  for ( i = 0; i < p->iWordStart; i++ )
472  if ( ~pNode1->puSimD[i] & ~pNode2->puSimD[i] )
473  return 0;
474  return 1;
475  }
476  if ( !fCompl1 && fCompl2 )
477  {
478  for ( i = 0; i < p->nWordsRand; i++ )
479  if ( pNode1->puSimR[i] & ~pNode2->puSimR[i] )
480  return 0;
481  for ( i = 0; i < p->iWordStart; i++ )
482  if ( pNode1->puSimD[i] & ~pNode2->puSimD[i] )
483  return 0;
484  return 1;
485  }
486  if ( fCompl1 && !fCompl2 )
487  {
488  for ( i = 0; i < p->nWordsRand; i++ )
489  if ( ~pNode1->puSimR[i] & pNode2->puSimR[i] )
490  return 0;
491  for ( i = 0; i < p->iWordStart; i++ )
492  if ( ~pNode1->puSimD[i] & pNode2->puSimD[i] )
493  return 0;
494  return 1;
495  }
496 // if ( fCompl1 && fCompl2 )
497  {
498  for ( i = 0; i < p->nWordsRand; i++ )
499  if ( pNode1->puSimR[i] & pNode2->puSimR[i] )
500  return 0;
501  for ( i = 0; i < p->iWordStart; i++ )
502  if ( pNode1->puSimD[i] & pNode2->puSimD[i] )
503  return 0;
504  return 1;
505  }
506 }
507 
508 /**Function*************************************************************
509 
510  Synopsis [Adds clauses to the solver.]
511 
512  Description [This procedure is used to add external clauses to the solver.
513  The clauses are given by sets of nodes. Each node stands for one literal.
514  If the node is complemented, the literal is negated.]
515 
516  SideEffects []
517 
518  SeeAlso []
519 
520 ***********************************************************************/
521 void Fraig_ManAddClause( Fraig_Man_t * p, Fraig_Node_t ** ppNodes, int nNodes )
522 {
523  Fraig_Node_t * pNode;
524  int i, fComp, RetValue;
525  if ( p->pSat == NULL )
526  Fraig_ManCreateSolver( p );
527  // create four clauses
528  Msat_IntVecClear( p->vProj );
529  for ( i = 0; i < nNodes; i++ )
530  {
531  pNode = Fraig_Regular(ppNodes[i]);
532  fComp = Fraig_IsComplement(ppNodes[i]);
533  Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNode->Num, fComp) );
534 // printf( "%d(%d) ", pNode->Num, fComp );
535  }
536 // printf( "\n" );
537  RetValue = Msat_SolverAddClause( p->pSat, p->vProj );
538  assert( RetValue );
539 }
540 
541 ////////////////////////////////////////////////////////////////////////
542 /// END OF FILE ///
543 ////////////////////////////////////////////////////////////////////////
544 
545 ABC_NAMESPACE_IMPL_END
546 
memset
char * memset()
Fraig_ManFree
void Fraig_ManFree(Fraig_Man_t *p)
Definition: fraigMan.c:262
Prove_ParamsStruct_t_::nMiteringLimitStart
int nMiteringLimitStart
Definition: ivyFraig.c:119
Fraig_ManReadPatternNumRandom
int Fraig_ManReadPatternNumRandom(Fraig_Man_t *p)
Definition: fraigApi.c:65
Fraig_NodeCreateConst
Fraig_Node_t * Fraig_NodeCreateConst(Fraig_Man_t *p)
FUNCTION DEFINITIONS ///.
Definition: fraigNode.c:46
Fraig_ParamsStruct_t_::fInternal
int fInternal
Definition: fraig.h:62
Fraig_ParamsStruct_t_::nConfLimit
int nConfLimit
Definition: fraig.h:63
Fraig_CountNodes
int Fraig_CountNodes(Fraig_Man_t *pMan, int fEquiv)
Definition: fraigUtil.c:152
Msat_SolverReadVarsUsed
Msat_IntVec_t * Msat_SolverReadVarsUsed(Msat_Solver_t *p)
Definition: msatSolverApi.c:136
Fraig_Man_t
typedefABC_NAMESPACE_HEADER_START struct Fraig_ManStruct_t_ Fraig_Man_t
INCLUDES ///.
Definition: fraig.h:40
Prove_ParamsStruct_t_::fUseFraiging
int fUseFraiging
Definition: ivyFraig.c:112
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Fraig_ManAddClause
void Fraig_ManAddClause(Fraig_Man_t *p, Fraig_Node_t **ppNodes, int nNodes)
Definition: fraigMan.c:521
Msat_SolverAddClause
int Msat_SolverAddClause(Msat_Solver_t *p, Msat_IntVec_t *pLits)
Definition: msatSolverCore.c:65
Prove_ParamsStruct_t_::nMiteringLimitMulti
float nMiteringLimitMulti
Definition: ivyFraig.c:120
Msat_SolverFree
void Msat_SolverFree(Msat_Solver_t *p)
Definition: msatSolverApi.c:386
Msat_SolverReadConeVars
Msat_IntVec_t * Msat_SolverReadConeVars(Msat_Solver_t *p)
Definition: msatSolverApi.c:120
Fraig_ParamsStruct_t_::nInspLimit
ABC_INT64_T nInspLimit
Definition: fraig.h:64
Fraig_ParamsStruct_t_::fDoSparse
int fDoSparse
Definition: fraig.h:57
Msat_IntVecClear
void Msat_IntVecClear(Msat_IntVec_t *p)
Definition: msatVec.c:335
Prove_ParamsStruct_t_::fUseRewriting
int fUseRewriting
Definition: ivyFraig.c:113
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
Prove_ParamsStruct_t_::fUseBdds
int fUseBdds
Definition: ivyFraig.c:114
Aig_ManRandom
unsigned Aig_ManRandom(int fReset)
Definition: aigUtil.c:1157
Fraig_HashTableFree
void Fraig_HashTableFree(Fraig_HashTable_t *p)
Definition: fraigTable.c:70
Fraig_ParamsStruct_t_::fVerbose
int fVerbose
Definition: fraig.h:60
Fraig_NodeStruct_t_::puSimD
unsigned * puSimD
Definition: fraigInt.h:248
Fraig_ParamsStruct_t_
Definition: fraig.h:48
Fraig_UtilInfoAlloc
Fraig_NodeVec_t * Fraig_UtilInfoAlloc(int nSize, int nWords, int fClean)
Definition: fraigMan.c:389
Msat_SolverAlloc
Msat_Solver_t * Msat_SolverAlloc(int nVars, double dClaInc, double dClaDecay, double dVarInc, double dVarDecay, int fVerbose)
Definition: msatSolverApi.c:154
Fraig_ParamsStruct_t_::fFuncRed
int fFuncRed
Definition: fraig.h:54
nWords
int nWords
Definition: abcNpn.c:127
for
for(p=first;p->value< newval;p=p->next)
Fraig_ManCreateSolver
void Fraig_ManCreateSolver(Fraig_Man_t *p)
Definition: fraigMan.c:325
timeSelect
ABC_NAMESPACE_IMPL_START abctime timeSelect
DECLARATIONS ///.
Definition: fraigMan.c:28
FRAIG_PATTERNS_RANDOM
#define FRAIG_PATTERNS_RANDOM
Definition: fraigInt.h:58
Fraig_PrintTime
#define Fraig_PrintTime(a, t)
Definition: fraigInt.h:90
Msat_IntVecPush
void Msat_IntVecPush(Msat_IntVec_t *p, int Entry)
Definition: msatVec.c:351
Prove_ParamsStruct_t_::nMiteringLimitLast
int nMiteringLimitLast
Definition: ivyFraig.c:131
Fraig_NodeStruct_t_::puSimR
unsigned * puSimR
Definition: fraigInt.h:247
Fraig_ManReadPatternNumDynamic
int Fraig_ManReadPatternNumDynamic(Fraig_Man_t *p)
Definition: fraigApi.c:67
timeAssign
abctime timeAssign
Definition: fraigMan.c:29
Fraig_FeedBackInit
void Fraig_FeedBackInit(Fraig_Man_t *p)
FUNCTION DEFINITIONS ///.
Definition: fraigFeed.c:57
Fraig_ParamsStruct_t_::nPatsRand
int nPatsRand
Definition: fraig.h:50
Fraig_ManGetSimInfo
Fraig_NodeVec_t * Fraig_ManGetSimInfo(Fraig_Man_t *p)
Definition: fraigMan.c:417
Fraig_ParamsStruct_t_::fFeedBack
int fFeedBack
Definition: fraig.h:55
Prove_ParamsStruct_t_::fBddReorder
int fBddReorder
Definition: ivyFraig.c:129
Fraig_NodeVecFree
void Fraig_NodeVecFree(Fraig_NodeVec_t *p)
Definition: fraigVec.c:66
Fraig_ManCountMuxes
int Fraig_ManCountMuxes(Fraig_Man_t *pMan)
Definition: fraigUtil.c:763
Fraig_NodeVecAlloc
Fraig_NodeVec_t * Fraig_NodeVecAlloc(int nCap)
DECLARATIONS ///.
Definition: fraigVec.c:43
Fraig_NodeStruct_t_
Definition: fraigInt.h:207
Fraig_ManCheckClauseUsingSimInfo
int Fraig_ManCheckClauseUsingSimInfo(Fraig_Man_t *p, Fraig_Node_t *pNode1, Fraig_Node_t *pNode2)
Definition: fraigMan.c:454
Prove_ParamsStruct_t_::nRewritingLimitStart
int nRewritingLimitStart
Definition: ivyFraig.c:122
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
FRAIG_PATTERNS_DYNAMIC
#define FRAIG_PATTERNS_DYNAMIC
Definition: fraigInt.h:59
Prove_ParamsStruct_t_::nFraigingLimitStart
int nFraigingLimitStart
Definition: ivyFraig.c:125
Prove_ParamsStruct_t_::nTotalInspectLimit
ABC_INT64_T nTotalInspectLimit
Definition: ivyFraig.c:134
Fraig_ParamsStruct_t_::fTryProve
int fTryProve
Definition: fraig.h:59
Fraig_ManPrintStats
void Fraig_ManPrintStats(Fraig_Man_t *p)
Definition: fraigMan.c:351
FRAIG_NUM_WORDS
#define FRAIG_NUM_WORDS(n)
Definition: fraigInt.h:72
Prove_ParamsStruct_t_::nRewritingLimitMulti
float nRewritingLimitMulti
Definition: ivyFraig.c:123
Msat_IntVecAlloc
Msat_IntVec_t * Msat_IntVecAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: msatVec.c:48
Msat_IntVecFree
void Msat_IntVecFree(Msat_IntVec_t *p)
Definition: msatVec.c:160
Fraig_IsComplement
#define Fraig_IsComplement(p)
GLOBAL VARIABLES ///.
Definition: fraig.h:107
Fraig_HashTableCreate
Fraig_HashTable_t * Fraig_HashTableCreate(int nSize)
FUNCTION DEFINITIONS ///.
Definition: fraigTable.c:46
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
Fraig_ParamsStruct_t_::fChoicing
int fChoicing
Definition: fraig.h:58
Prove_ParamsStruct_t_::nBddSizeLimit
int nBddSizeLimit
Definition: ivyFraig.c:128
Prove_ParamsStruct_t_::nTotalBacktrackLimit
ABC_INT64_T nTotalBacktrackLimit
Definition: ivyFraig.c:133
Fraig_NodeStruct_t_::Num
int Num
Definition: fraigInt.h:210
Prove_ParamsStruct_t_::nItersMax
int nItersMax
Definition: ivyFraig.c:117
Fraig_Node_t
struct Fraig_NodeStruct_t_ Fraig_Node_t
Definition: fraig.h:41
Msat_SolverReadAdjacents
Msat_ClauseVec_t * Msat_SolverReadAdjacents(Msat_Solver_t *p)
Definition: msatSolverApi.c:104
Fraig_ParamsStruct_t_::fDist1Pats
int fDist1Pats
Definition: fraig.h:56
Prove_ParamsStruct_t_::fVerbose
int fVerbose
Definition: ivyFraig.c:115
Fraig_ManCreate
Fraig_Man_t * Fraig_ManCreate(Fraig_Params_t *pParams)
Definition: fraigMan.c:184
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
Fraig_NodeVecStruct_t_::pArray
Fraig_Node_t ** pArray
Definition: fraigInt.h:267
Fraig_Regular
#define Fraig_Regular(p)
Definition: fraig.h:108
Fraig_ManReportChoices
void Fraig_ManReportChoices(Fraig_Man_t *pMan)
Definition: fraigUtil.c:520
Prove_ParamsStruct_t_::nFraigingLimitMulti
float nFraigingLimitMulti
Definition: ivyFraig.c:126
Fraig_ParamsStruct_t_::fVerboseP
int fVerboseP
Definition: fraig.h:61
Fraig_MemFixedStop
void Fraig_MemFixedStop(Fraig_MemFixed_t *p, int fVerbose)
Definition: fraigMem.c:102
Fraig_ManCountExors
int Fraig_ManCountExors(Fraig_Man_t *pMan)
Definition: fraigUtil.c:742
Fraig_ParamsStruct_t_::nPatsDyna
int nPatsDyna
Definition: fraig.h:51
MSAT_VAR2LIT
#define MSAT_VAR2LIT(v, s)
Definition: msat.h:56
assert
#define assert(ex)
Definition: util_old.h:213
Fraig_ParamsSetDefaultFull
void Fraig_ParamsSetDefaultFull(Fraig_Params_t *pParams)
Definition: fraigMan.c:153
Fraig_NodeVecStruct_t_::nSize
int nSize
Definition: fraigInt.h:266
Fraig_ParamsStruct_t_::nBTLimit
int nBTLimit
Definition: fraig.h:52
Prove_ParamsPrint
void Prove_ParamsPrint(Prove_Params_t *pParams)
Definition: fraigMan.c:89
abctime
ABC_INT64_T abctime
Definition: abc_global.h:278
Fraig_MemFixedStart
Fraig_MemFixed_t * Fraig_MemFixedStart(int nEntrySize)
FUNCTION DEFINITIONS ///.
Definition: fraigMem.c:63
Msat_SolverPrintStats
void Msat_SolverPrintStats(Msat_Solver_t *p)
Definition: msatSolverCore.c:110
Fraig_ParamsSetDefault
void Fraig_ParamsSetDefault(Fraig_Params_t *pParams)
Definition: fraigMan.c:122
Fraig_ParamsStruct_t_::nSeconds
int nSeconds
Definition: fraig.h:53
Prove_ParamsSetDefault
void Prove_ParamsSetDefault(Prove_Params_t *pParams)
FUNCTION DEFINITIONS ///.
Definition: fraigMan.c:46
Prove_ParamsStruct_t_
Definition: ivyFraig.c:109
Fraig_NodeVecStruct_t_
Definition: fraigInt.h:263