abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
ivyFraig.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [ivyFraig.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [And-Inverter Graph package.]
8 
9  Synopsis [Functional reduction of AIGs]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - May 11, 2006.]
16 
17  Revision [$Id: ivyFraig.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include <math.h>
22 
23 #include "sat/bsat/satSolver.h"
24 #include "misc/extra/extra.h"
25 #include "ivy.h"
26 
27 ABC_NAMESPACE_IMPL_START
28 
29 ////////////////////////////////////////////////////////////////////////
30 /// DECLARATIONS ///
31 ////////////////////////////////////////////////////////////////////////
32 
33 typedef struct Ivy_FraigMan_t_ Ivy_FraigMan_t;
34 typedef struct Ivy_FraigSim_t_ Ivy_FraigSim_t;
35 typedef struct Ivy_FraigList_t_ Ivy_FraigList_t;
36 
37 struct Ivy_FraigList_t_
38 {
39  Ivy_Obj_t * pHead;
40  Ivy_Obj_t * pTail;
41  int nItems;
42 };
43 
44 struct Ivy_FraigSim_t_
45 {
46  int Type;
47  Ivy_FraigSim_t * pNext;
48  Ivy_FraigSim_t * pFanin0;
49  Ivy_FraigSim_t * pFanin1;
50  unsigned pData[0];
51 };
52 
53 struct Ivy_FraigMan_t_
54 {
55  // general info
56  Ivy_FraigParams_t * pParams; // various parameters
57  // temporary backtrack limits because "ABC_INT64_T" cannot be defined in Ivy_FraigParams_t ...
58  ABC_INT64_T nBTLimitGlobal; // global limit on the number of backtracks
59  ABC_INT64_T nInsLimitGlobal;// global limit on the number of clause inspects
60  // AIG manager
61  Ivy_Man_t * pManAig; // the starting AIG manager
62  Ivy_Man_t * pManFraig; // the final AIG manager
63  // simulation information
64  int nSimWords; // the number of words
65  char * pSimWords; // the simulation info
66  Ivy_FraigSim_t * pSimStart; // the list of simulation info for internal nodes
67  // counter example storage
68  int nPatWords; // the number of words in the counter example
69  unsigned * pPatWords; // the counter example
70  int * pPatScores; // the scores of each pattern
71  // equivalence classes
72  Ivy_FraigList_t lClasses; // equivalence classes
73  Ivy_FraigList_t lCand; // candidatates
74  int nPairs; // the number of pairs of nodes
75  // equivalence checking
76  sat_solver * pSat; // SAT solver
77  int nSatVars; // the number of variables currently used
78  Vec_Ptr_t * vPiVars; // the PIs of the cone used
79  // other
80  ProgressBar * pProgress;
81  // statistics
82  int nSimRounds;
83  int nNodesMiter;
84  int nClassesZero;
85  int nClassesBeg;
86  int nClassesEnd;
87  int nPairsBeg;
88  int nPairsEnd;
89  int nSatCalls;
90  int nSatCallsSat;
91  int nSatCallsUnsat;
92  int nSatProof;
93  int nSatFails;
94  int nSatFailsReal;
95  // runtime
96  abctime timeSim;
97  abctime timeTrav;
98  abctime timeSat;
99  abctime timeSatUnsat;
100  abctime timeSatSat;
101  abctime timeSatFail;
102  abctime timeRef;
103  abctime timeTotal;
104  abctime time1;
105  abctime time2;
106 };
107 
108 typedef struct Prove_ParamsStruct_t_ Prove_Params_t;
109 struct Prove_ParamsStruct_t_
110 {
111  // general parameters
112  int fUseFraiging; // enables fraiging
113  int fUseRewriting; // enables rewriting
114  int fUseBdds; // enables BDD construction when other methods fail
115  int fVerbose; // prints verbose stats
116  // iterations
117  int nItersMax; // the number of iterations
118  // mitering
119  int nMiteringLimitStart; // starting mitering limit
120  float nMiteringLimitMulti; // multiplicative coefficient to increase the limit in each iteration
121  // rewriting
122  int nRewritingLimitStart; // the number of rewriting iterations
123  float nRewritingLimitMulti; // multiplicative coefficient to increase the limit in each iteration
124  // fraiging
125  int nFraigingLimitStart; // starting backtrack(conflict) limit
126  float nFraigingLimitMulti; // multiplicative coefficient to increase the limit in each iteration
127  // last-gasp BDD construction
128  int nBddSizeLimit; // the number of BDD nodes when construction is aborted
129  int fBddReorder; // enables dynamic BDD variable reordering
130  // last-gasp mitering
131  int nMiteringLimitLast; // final mitering limit
132  // global SAT solver limits
133  ABC_INT64_T nTotalBacktrackLimit; // global limit on the number of backtracks
134  ABC_INT64_T nTotalInspectLimit; // global limit on the number of clause inspects
135  // global resources applied
136  ABC_INT64_T nTotalBacktracksMade; // the total number of backtracks made
137  ABC_INT64_T nTotalInspectsMade; // the total number of inspects made
138 };
139 
140 static inline Ivy_FraigSim_t * Ivy_ObjSim( Ivy_Obj_t * pObj ) { return (Ivy_FraigSim_t *)pObj->pFanout; }
141 static inline Ivy_Obj_t * Ivy_ObjClassNodeLast( Ivy_Obj_t * pObj ) { return pObj->pNextFan0; }
142 static inline Ivy_Obj_t * Ivy_ObjClassNodeRepr( Ivy_Obj_t * pObj ) { return pObj->pNextFan0; }
143 static inline Ivy_Obj_t * Ivy_ObjClassNodeNext( Ivy_Obj_t * pObj ) { return pObj->pNextFan1; }
144 static inline Ivy_Obj_t * Ivy_ObjNodeHashNext( Ivy_Obj_t * pObj ) { return pObj->pPrevFan0; }
145 static inline Ivy_Obj_t * Ivy_ObjEquivListNext( Ivy_Obj_t * pObj ) { return pObj->pPrevFan0; }
146 static inline Ivy_Obj_t * Ivy_ObjEquivListPrev( Ivy_Obj_t * pObj ) { return pObj->pPrevFan1; }
147 static inline Ivy_Obj_t * Ivy_ObjFraig( Ivy_Obj_t * pObj ) { return pObj->pEquiv; }
148 static inline int Ivy_ObjSatNum( Ivy_Obj_t * pObj ) { return (int)(ABC_PTRUINT_T)pObj->pNextFan0; }
149 static inline Vec_Ptr_t * Ivy_ObjFaninVec( Ivy_Obj_t * pObj ) { return (Vec_Ptr_t *)pObj->pNextFan1; }
150 
151 static inline void Ivy_ObjSetSim( Ivy_Obj_t * pObj, Ivy_FraigSim_t * pSim ) { pObj->pFanout = (Ivy_Obj_t *)pSim; }
152 static inline void Ivy_ObjSetClassNodeLast( Ivy_Obj_t * pObj, Ivy_Obj_t * pLast ) { pObj->pNextFan0 = pLast; }
153 static inline void Ivy_ObjSetClassNodeRepr( Ivy_Obj_t * pObj, Ivy_Obj_t * pRepr ) { pObj->pNextFan0 = pRepr; }
154 static inline void Ivy_ObjSetClassNodeNext( Ivy_Obj_t * pObj, Ivy_Obj_t * pNext ) { pObj->pNextFan1 = pNext; }
155 static inline void Ivy_ObjSetNodeHashNext( Ivy_Obj_t * pObj, Ivy_Obj_t * pNext ) { pObj->pPrevFan0 = pNext; }
156 static inline void Ivy_ObjSetEquivListNext( Ivy_Obj_t * pObj, Ivy_Obj_t * pNext ) { pObj->pPrevFan0 = pNext; }
157 static inline void Ivy_ObjSetEquivListPrev( Ivy_Obj_t * pObj, Ivy_Obj_t * pPrev ) { pObj->pPrevFan1 = pPrev; }
158 static inline void Ivy_ObjSetFraig( Ivy_Obj_t * pObj, Ivy_Obj_t * pNode ) { pObj->pEquiv = pNode; }
159 static inline void Ivy_ObjSetSatNum( Ivy_Obj_t * pObj, int Num ) { pObj->pNextFan0 = (Ivy_Obj_t *)(ABC_PTRUINT_T)Num; }
160 static inline void Ivy_ObjSetFaninVec( Ivy_Obj_t * pObj, Vec_Ptr_t * vFanins ) { pObj->pNextFan1 = (Ivy_Obj_t *)vFanins; }
161 
162 static inline unsigned Ivy_ObjRandomSim() { return (rand() << 24) ^ (rand() << 12) ^ rand(); }
163 
164 // iterate through equivalence classes
165 #define Ivy_FraigForEachEquivClass( pList, pEnt ) \
166  for ( pEnt = pList; \
167  pEnt; \
168  pEnt = Ivy_ObjEquivListNext(pEnt) )
169 #define Ivy_FraigForEachEquivClassSafe( pList, pEnt, pEnt2 ) \
170  for ( pEnt = pList, \
171  pEnt2 = pEnt? Ivy_ObjEquivListNext(pEnt): NULL; \
172  pEnt; \
173  pEnt = pEnt2, \
174  pEnt2 = pEnt? Ivy_ObjEquivListNext(pEnt): NULL )
175 // iterate through nodes in one class
176 #define Ivy_FraigForEachClassNode( pClass, pEnt ) \
177  for ( pEnt = pClass; \
178  pEnt; \
179  pEnt = Ivy_ObjClassNodeNext(pEnt) )
180 // iterate through nodes in the hash table
181 #define Ivy_FraigForEachBinNode( pBin, pEnt ) \
182  for ( pEnt = pBin; \
183  pEnt; \
184  pEnt = Ivy_ObjNodeHashNext(pEnt) )
185 
186 static Ivy_FraigMan_t * Ivy_FraigStart( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams );
187 static Ivy_FraigMan_t * Ivy_FraigStartSimple( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams );
188 static Ivy_Man_t * Ivy_FraigPerform_int( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams, ABC_INT64_T nBTLimitGlobal, ABC_INT64_T nInsLimitGlobal, ABC_INT64_T * pnSatConfs, ABC_INT64_T * pnSatInspects );
189 static void Ivy_FraigPrint( Ivy_FraigMan_t * p );
190 static void Ivy_FraigStop( Ivy_FraigMan_t * p );
191 static void Ivy_FraigSimulate( Ivy_FraigMan_t * p );
192 static void Ivy_FraigSweep( Ivy_FraigMan_t * p );
193 static Ivy_Obj_t * Ivy_FraigAnd( Ivy_FraigMan_t * p, Ivy_Obj_t * pObjOld );
194 static int Ivy_FraigNodesAreEquiv( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj0, Ivy_Obj_t * pObj1 );
195 static int Ivy_FraigNodeIsConst( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj );
196 static void Ivy_FraigNodeAddToSolver( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj0, Ivy_Obj_t * pObj1 );
197 static int Ivy_FraigSetActivityFactors( Ivy_FraigMan_t * p, Ivy_Obj_t * pOld, Ivy_Obj_t * pNew );
198 static void Ivy_FraigAddToPatScores( Ivy_FraigMan_t * p, Ivy_Obj_t * pClass, Ivy_Obj_t * pClassNew );
199 static int Ivy_FraigMiterStatus( Ivy_Man_t * pMan );
200 static void Ivy_FraigMiterProve( Ivy_FraigMan_t * p );
201 static void Ivy_FraigMiterPrint( Ivy_Man_t * pNtk, char * pString, abctime clk, int fVerbose );
202 static int * Ivy_FraigCreateModel( Ivy_FraigMan_t * p );
203 
204 static int Ivy_FraigNodesAreEquivBdd( Ivy_Obj_t * pObj1, Ivy_Obj_t * pObj2 );
205 static int Ivy_FraigCheckCone( Ivy_FraigMan_t * pGlo, Ivy_Man_t * p, Ivy_Obj_t * pObj1, Ivy_Obj_t * pObj2, int nConfLimit );
206 
207 static ABC_INT64_T s_nBTLimitGlobal = 0;
208 static ABC_INT64_T s_nInsLimitGlobal = 0;
209 
210 ////////////////////////////////////////////////////////////////////////
211 /// FUNCTION DEFINITIONS ///
212 ////////////////////////////////////////////////////////////////////////
213 
214 /**Function*************************************************************
215 
216  Synopsis [Sets the default solving parameters.]
217 
218  Description []
219 
220  SideEffects []
221 
222  SeeAlso []
223 
224 ***********************************************************************/
225 void Ivy_FraigParamsDefault( Ivy_FraigParams_t * pParams )
226 {
227  memset( pParams, 0, sizeof(Ivy_FraigParams_t) );
228  pParams->nSimWords = 32; // the number of words in the simulation info
229  pParams->dSimSatur = 0.005; // the ratio of refined classes when saturation is reached
230  pParams->fPatScores = 0; // enables simulation pattern scoring
231  pParams->MaxScore = 25; // max score after which resimulation is used
232  pParams->fDoSparse = 1; // skips sparse functions
233 // pParams->dActConeRatio = 0.05; // the ratio of cone to be bumped
234 // pParams->dActConeBumpMax = 5.0; // the largest bump of activity
235  pParams->dActConeRatio = 0.3; // the ratio of cone to be bumped
236  pParams->dActConeBumpMax = 10.0; // the largest bump of activity
237 
238  pParams->nBTLimitNode = 100; // conflict limit at a node
239  pParams->nBTLimitMiter = 500000; // conflict limit at an output
240 // pParams->nBTLimitGlobal = 0; // conflict limit global
241 // pParams->nInsLimitGlobal = 0; // inspection limit global
242 }
243 
244 /**Function*************************************************************
245 
246  Synopsis [Performs combinational equivalence checking for the miter.]
247 
248  Description []
249 
250  SideEffects []
251 
252  SeeAlso []
253 
254 ***********************************************************************/
255 int Ivy_FraigProve( Ivy_Man_t ** ppManAig, void * pPars )
256 {
257  Prove_Params_t * pParams = (Prove_Params_t *)pPars;
258  Ivy_FraigParams_t Params, * pIvyParams = &Params;
259  Ivy_Man_t * pManAig, * pManTemp;
260  int RetValue, nIter;
261  abctime clk;//, Counter;
262  ABC_INT64_T nSatConfs = 0, nSatInspects = 0;
263 
264  // start the network and parameters
265  pManAig = *ppManAig;
266  Ivy_FraigParamsDefault( pIvyParams );
267  pIvyParams->fVerbose = pParams->fVerbose;
268  pIvyParams->fProve = 1;
269 
270  if ( pParams->fVerbose )
271  {
272  printf( "RESOURCE LIMITS: Iterations = %d. Rewriting = %s. Fraiging = %s.\n",
273  pParams->nItersMax, pParams->fUseRewriting? "yes":"no", pParams->fUseFraiging? "yes":"no" );
274  printf( "Miter = %d (%3.1f). Rwr = %d (%3.1f). Fraig = %d (%3.1f). Last = %d.\n",
275  pParams->nMiteringLimitStart, pParams->nMiteringLimitMulti,
276  pParams->nRewritingLimitStart, pParams->nRewritingLimitMulti,
277  pParams->nFraigingLimitStart, pParams->nFraigingLimitMulti, pParams->nMiteringLimitLast );
278  }
279 
280  // if SAT only, solve without iteration
281  if ( !pParams->fUseRewriting && !pParams->fUseFraiging )
282  {
283  clk = Abc_Clock();
284  pIvyParams->nBTLimitMiter = pParams->nMiteringLimitLast / Ivy_ManPoNum(pManAig);
285  pManAig = Ivy_FraigMiter( pManTemp = pManAig, pIvyParams ); Ivy_ManStop( pManTemp );
286  RetValue = Ivy_FraigMiterStatus( pManAig );
287  Ivy_FraigMiterPrint( pManAig, "SAT solving", clk, pParams->fVerbose );
288  *ppManAig = pManAig;
289  return RetValue;
290  }
291 
292  if ( Ivy_ManNodeNum(pManAig) < 500 )
293  {
294  // run the first mitering
295  clk = Abc_Clock();
296  pIvyParams->nBTLimitMiter = pParams->nMiteringLimitStart / Ivy_ManPoNum(pManAig);
297  pManAig = Ivy_FraigMiter( pManTemp = pManAig, pIvyParams ); Ivy_ManStop( pManTemp );
298  RetValue = Ivy_FraigMiterStatus( pManAig );
299  Ivy_FraigMiterPrint( pManAig, "SAT solving", clk, pParams->fVerbose );
300  if ( RetValue >= 0 )
301  {
302  *ppManAig = pManAig;
303  return RetValue;
304  }
305  }
306 
307  // check the current resource limits
308  RetValue = -1;
309  for ( nIter = 0; nIter < pParams->nItersMax; nIter++ )
310  {
311  if ( pParams->fVerbose )
312  {
313  printf( "ITERATION %2d : Confs = %6d. FraigBTL = %3d. \n", nIter+1,
314  (int)(pParams->nMiteringLimitStart * pow(pParams->nMiteringLimitMulti,nIter)),
315  (int)(pParams->nFraigingLimitStart * pow(pParams->nFraigingLimitMulti,nIter)) );
316  fflush( stdout );
317  }
318 
319  // try rewriting
320  if ( pParams->fUseRewriting )
321  { // bug in Ivy_NodeFindCutsAll() when leaves are identical!
322 /*
323  clk = Abc_Clock();
324  Counter = (int)(pParams->nRewritingLimitStart * pow(pParams->nRewritingLimitMulti,nIter));
325  pManAig = Ivy_ManRwsat( pManAig, 0 );
326  RetValue = Ivy_FraigMiterStatus( pManAig );
327  Ivy_FraigMiterPrint( pManAig, "Rewriting ", clk, pParams->fVerbose );
328 */
329  }
330  if ( RetValue >= 0 )
331  break;
332 
333  // catch the situation when ref pattern detects the bug
334  RetValue = Ivy_FraigMiterStatus( pManAig );
335  if ( RetValue >= 0 )
336  break;
337 
338  // try fraiging followed by mitering
339  if ( pParams->fUseFraiging )
340  {
341  clk = Abc_Clock();
342  pIvyParams->nBTLimitNode = (int)(pParams->nFraigingLimitStart * pow(pParams->nFraigingLimitMulti,nIter));
343  pIvyParams->nBTLimitMiter = 1 + (int)(pParams->nMiteringLimitStart * pow(pParams->nMiteringLimitMulti,nIter)) / Ivy_ManPoNum(pManAig);
344  pManAig = Ivy_FraigPerform_int( pManTemp = pManAig, pIvyParams, pParams->nTotalBacktrackLimit, pParams->nTotalInspectLimit, &nSatConfs, &nSatInspects ); Ivy_ManStop( pManTemp );
345  RetValue = Ivy_FraigMiterStatus( pManAig );
346  Ivy_FraigMiterPrint( pManAig, "Fraiging ", clk, pParams->fVerbose );
347  }
348  if ( RetValue >= 0 )
349  break;
350 
351  // add to the number of backtracks and inspects
352  pParams->nTotalBacktracksMade += nSatConfs;
353  pParams->nTotalInspectsMade += nSatInspects;
354  // check if global resource limit is reached
355  if ( (pParams->nTotalBacktrackLimit && pParams->nTotalBacktracksMade >= pParams->nTotalBacktrackLimit) ||
356  (pParams->nTotalInspectLimit && pParams->nTotalInspectsMade >= pParams->nTotalInspectLimit) )
357  {
358  printf( "Reached global limit on conflicts/inspects. Quitting.\n" );
359  *ppManAig = pManAig;
360  return -1;
361  }
362  }
363 /*
364  if ( RetValue < 0 )
365  {
366  if ( pParams->fVerbose )
367  {
368  printf( "Attempting SAT with conflict limit %d ...\n", pParams->nMiteringLimitLast );
369  fflush( stdout );
370  }
371  clk = Abc_Clock();
372  pIvyParams->nBTLimitMiter = pParams->nMiteringLimitLast / Ivy_ManPoNum(pManAig);
373  if ( pParams->nTotalBacktrackLimit )
374  s_nBTLimitGlobal = pParams->nTotalBacktrackLimit - pParams->nTotalBacktracksMade;
375  if ( pParams->nTotalInspectLimit )
376  s_nInsLimitGlobal = pParams->nTotalInspectLimit - pParams->nTotalInspectsMade;
377  pManAig = Ivy_FraigMiter( pManTemp = pManAig, pIvyParams ); Ivy_ManStop( pManTemp );
378  s_nBTLimitGlobal = 0;
379  s_nInsLimitGlobal = 0;
380  RetValue = Ivy_FraigMiterStatus( pManAig );
381  Ivy_FraigMiterPrint( pManAig, "SAT solving", clk, pParams->fVerbose );
382  // make sure that the sover never returns "undecided" when infinite resource limits are set
383  if( RetValue == -1 && pParams->nTotalInspectLimit == 0 &&
384  pParams->nTotalBacktrackLimit == 0 )
385  {
386  extern void Prove_ParamsPrint( Prove_Params_t * pParams );
387  Prove_ParamsPrint( pParams );
388  printf("ERROR: ABC has returned \"undecided\" in spite of no limits...\n");
389  exit(1);
390  }
391  }
392 */
393  // assign the model if it was proved by rewriting (const 1 miter)
394  if ( RetValue == 0 && pManAig->pData == NULL )
395  {
396  pManAig->pData = ABC_ALLOC( int, Ivy_ManPiNum(pManAig) );
397  memset( pManAig->pData, 0, sizeof(int) * Ivy_ManPiNum(pManAig) );
398  }
399  *ppManAig = pManAig;
400  return RetValue;
401 }
402 
403 /**Function*************************************************************
404 
405  Synopsis [Performs fraiging of the AIG.]
406 
407  Description []
408 
409  SideEffects []
410 
411  SeeAlso []
412 
413 ***********************************************************************/
414 Ivy_Man_t * Ivy_FraigPerform_int( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams, ABC_INT64_T nBTLimitGlobal, ABC_INT64_T nInsLimitGlobal, ABC_INT64_T * pnSatConfs, ABC_INT64_T * pnSatInspects )
415 {
416  Ivy_FraigMan_t * p;
417  Ivy_Man_t * pManAigNew;
418  abctime clk;
419  if ( Ivy_ManNodeNum(pManAig) == 0 )
420  return Ivy_ManDup(pManAig);
421 clk = Abc_Clock();
422  assert( Ivy_ManLatchNum(pManAig) == 0 );
423  p = Ivy_FraigStart( pManAig, pParams );
424  // set global limits
425  p->nBTLimitGlobal = nBTLimitGlobal;
426  p->nInsLimitGlobal = nInsLimitGlobal;
427 
428  Ivy_FraigSimulate( p );
429  Ivy_FraigSweep( p );
430  pManAigNew = p->pManFraig;
431 p->timeTotal = Abc_Clock() - clk;
432  if ( pnSatConfs )
433  *pnSatConfs = p->pSat? p->pSat->stats.conflicts : 0;
434  if ( pnSatInspects )
435  *pnSatInspects = p->pSat? p->pSat->stats.inspects : 0;
436  Ivy_FraigStop( p );
437  return pManAigNew;
438 }
439 
440 /**Function*************************************************************
441 
442  Synopsis [Performs fraiging of the AIG.]
443 
444  Description []
445 
446  SideEffects []
447 
448  SeeAlso []
449 
450 ***********************************************************************/
451 Ivy_Man_t * Ivy_FraigPerform( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams )
452 {
453  Ivy_FraigMan_t * p;
454  Ivy_Man_t * pManAigNew;
455  abctime clk;
456  if ( Ivy_ManNodeNum(pManAig) == 0 )
457  return Ivy_ManDup(pManAig);
458 clk = Abc_Clock();
459  assert( Ivy_ManLatchNum(pManAig) == 0 );
460  p = Ivy_FraigStart( pManAig, pParams );
461  Ivy_FraigSimulate( p );
462  Ivy_FraigSweep( p );
463  pManAigNew = p->pManFraig;
464 p->timeTotal = Abc_Clock() - clk;
465  Ivy_FraigStop( p );
466  return pManAigNew;
467 }
468 
469 /**Function*************************************************************
470 
471  Synopsis [Applies brute-force SAT to the miter.]
472 
473  Description []
474 
475  SideEffects []
476 
477  SeeAlso []
478 
479 ***********************************************************************/
480 Ivy_Man_t * Ivy_FraigMiter( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams )
481 {
482  Ivy_FraigMan_t * p;
483  Ivy_Man_t * pManAigNew;
484  Ivy_Obj_t * pObj;
485  int i;
486  abctime clk;
487 clk = Abc_Clock();
488  assert( Ivy_ManLatchNum(pManAig) == 0 );
489  p = Ivy_FraigStartSimple( pManAig, pParams );
490  // set global limits
491  p->nBTLimitGlobal = s_nBTLimitGlobal;
492  p->nInsLimitGlobal = s_nInsLimitGlobal;
493  // duplicate internal nodes
494  Ivy_ManForEachNode( p->pManAig, pObj, i )
495  pObj->pEquiv = Ivy_And( p->pManFraig, Ivy_ObjChild0Equiv(pObj), Ivy_ObjChild1Equiv(pObj) );
496  // try to prove each output of the miter
497  Ivy_FraigMiterProve( p );
498  // add the POs
499  Ivy_ManForEachPo( p->pManAig, pObj, i )
500  Ivy_ObjCreatePo( p->pManFraig, Ivy_ObjChild0Equiv(pObj) );
501  // clean the new manager
502  Ivy_ManForEachObj( p->pManFraig, pObj, i )
503  {
504  if ( Ivy_ObjFaninVec(pObj) )
505  Vec_PtrFree( Ivy_ObjFaninVec(pObj) );
506  pObj->pNextFan0 = pObj->pNextFan1 = NULL;
507  }
508  // remove dangling nodes
509  Ivy_ManCleanup( p->pManFraig );
510  pManAigNew = p->pManFraig;
511 p->timeTotal = Abc_Clock() - clk;
512 
513 //printf( "Final nodes = %6d. ", Ivy_ManNodeNum(pManAigNew) );
514 //ABC_PRT( "Time", p->timeTotal );
515  Ivy_FraigStop( p );
516  return pManAigNew;
517 }
518 
519 /**Function*************************************************************
520 
521  Synopsis [Starts the fraiging manager without simulation info.]
522 
523  Description []
524 
525  SideEffects []
526 
527  SeeAlso []
528 
529 ***********************************************************************/
530 Ivy_FraigMan_t * Ivy_FraigStartSimple( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams )
531 {
532  Ivy_FraigMan_t * p;
533  // allocat the fraiging manager
534  p = ABC_ALLOC( Ivy_FraigMan_t, 1 );
535  memset( p, 0, sizeof(Ivy_FraigMan_t) );
536  p->pParams = pParams;
537  p->pManAig = pManAig;
538  p->pManFraig = Ivy_ManStartFrom( pManAig );
539  p->vPiVars = Vec_PtrAlloc( 100 );
540  return p;
541 }
542 
543 /**Function*************************************************************
544 
545  Synopsis [Starts the fraiging manager.]
546 
547  Description []
548 
549  SideEffects []
550 
551  SeeAlso []
552 
553 ***********************************************************************/
554 Ivy_FraigMan_t * Ivy_FraigStart( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams )
555 {
556  Ivy_FraigMan_t * p;
557  Ivy_FraigSim_t * pSims;
558  Ivy_Obj_t * pObj;
559  int i, k, EntrySize;
560  // clean the fanout representation
561  Ivy_ManForEachObj( pManAig, pObj, i )
562 // pObj->pEquiv = pObj->pFanout = pObj->pNextFan0 = pObj->pNextFan1 = pObj->pPrevFan0 = pObj->pPrevFan1 = NULL;
563  assert( !pObj->pEquiv && !pObj->pFanout );
564  // allocat the fraiging manager
565  p = ABC_ALLOC( Ivy_FraigMan_t, 1 );
566  memset( p, 0, sizeof(Ivy_FraigMan_t) );
567  p->pParams = pParams;
568  p->pManAig = pManAig;
569  p->pManFraig = Ivy_ManStartFrom( pManAig );
570  // allocate simulation info
571  p->nSimWords = pParams->nSimWords;
572 // p->pSimWords = ABC_ALLOC( unsigned, Ivy_ManObjNum(pManAig) * p->nSimWords );
573  EntrySize = sizeof(Ivy_FraigSim_t) + sizeof(unsigned) * p->nSimWords;
574  p->pSimWords = (char *)ABC_ALLOC( char, Ivy_ManObjNum(pManAig) * EntrySize );
575  memset( p->pSimWords, 0, EntrySize );
576  k = 0;
577  Ivy_ManForEachObj( pManAig, pObj, i )
578  {
579  pSims = (Ivy_FraigSim_t *)(p->pSimWords + EntrySize * k++);
580  pSims->pNext = NULL;
581  if ( Ivy_ObjIsNode(pObj) )
582  {
583  if ( p->pSimStart == NULL )
584  p->pSimStart = pSims;
585  else
586  ((Ivy_FraigSim_t *)(p->pSimWords + EntrySize * (k-2)))->pNext = pSims;
587  pSims->pFanin0 = Ivy_ObjSim( Ivy_ObjFanin0(pObj) );
588  pSims->pFanin1 = Ivy_ObjSim( Ivy_ObjFanin1(pObj) );
589  pSims->Type = (Ivy_ObjFaninPhase(Ivy_ObjChild0(pObj)) << 2) | (Ivy_ObjFaninPhase(Ivy_ObjChild1(pObj)) << 1) | pObj->fPhase;
590  }
591  else
592  {
593  pSims->pFanin0 = NULL;
594  pSims->pFanin1 = NULL;
595  pSims->Type = 0;
596  }
597  Ivy_ObjSetSim( pObj, pSims );
598  }
599  assert( k == Ivy_ManObjNum(pManAig) );
600  // allocate storage for sim pattern
601  p->nPatWords = Ivy_BitWordNum( Ivy_ManPiNum(pManAig) );
602  p->pPatWords = ABC_ALLOC( unsigned, p->nPatWords );
603  p->pPatScores = ABC_ALLOC( int, 32 * p->nSimWords );
604  p->vPiVars = Vec_PtrAlloc( 100 );
605  // set random number generator
606  srand( 0xABCABC );
607  return p;
608 }
609 
610 /**Function*************************************************************
611 
612  Synopsis [Stops the fraiging manager.]
613 
614  Description []
615 
616  SideEffects []
617 
618  SeeAlso []
619 
620 ***********************************************************************/
621 void Ivy_FraigStop( Ivy_FraigMan_t * p )
622 {
623  if ( p->pParams->fVerbose )
624  Ivy_FraigPrint( p );
625  if ( p->vPiVars ) Vec_PtrFree( p->vPiVars );
626  if ( p->pSat ) sat_solver_delete( p->pSat );
627  ABC_FREE( p->pPatScores );
628  ABC_FREE( p->pPatWords );
629  ABC_FREE( p->pSimWords );
630  ABC_FREE( p );
631 }
632 
633 /**Function*************************************************************
634 
635  Synopsis [Prints stats for the fraiging manager.]
636 
637  Description []
638 
639  SideEffects []
640 
641  SeeAlso []
642 
643 ***********************************************************************/
644 void Ivy_FraigPrint( Ivy_FraigMan_t * p )
645 {
646  double nMemory;
647  nMemory = (double)Ivy_ManObjNum(p->pManAig)*p->nSimWords*sizeof(unsigned)/(1<<20);
648  printf( "SimWords = %d. Rounds = %d. Mem = %0.2f MB. ", p->nSimWords, p->nSimRounds, nMemory );
649  printf( "Classes: Beg = %d. End = %d.\n", p->nClassesBeg, p->nClassesEnd );
650 // printf( "Limits: BTNode = %d. BTMiter = %d.\n", p->pParams->nBTLimitNode, p->pParams->nBTLimitMiter );
651  printf( "Proof = %d. Counter-example = %d. Fail = %d. FailReal = %d. Zero = %d.\n",
652  p->nSatProof, p->nSatCallsSat, p->nSatFails, p->nSatFailsReal, p->nClassesZero );
653  printf( "Final = %d. Miter = %d. Total = %d. Mux = %d. (Exor = %d.) SatVars = %d.\n",
654  Ivy_ManNodeNum(p->pManFraig), p->nNodesMiter, Ivy_ManNodeNum(p->pManAig), 0, 0, p->nSatVars );
655  if ( p->pSat ) Sat_SolverPrintStats( stdout, p->pSat );
656  ABC_PRT( "AIG simulation ", p->timeSim );
657  ABC_PRT( "AIG traversal ", p->timeTrav );
658  ABC_PRT( "SAT solving ", p->timeSat );
659  ABC_PRT( " Unsat ", p->timeSatUnsat );
660  ABC_PRT( " Sat ", p->timeSatSat );
661  ABC_PRT( " Fail ", p->timeSatFail );
662  ABC_PRT( "Class refining ", p->timeRef );
663  ABC_PRT( "TOTAL RUNTIME ", p->timeTotal );
664  if ( p->time1 ) { ABC_PRT( "time1 ", p->time1 ); }
665 }
666 
667 
668 
669 /**Function*************************************************************
670 
671  Synopsis [Assigns random patterns to the PI node.]
672 
673  Description []
674 
675  SideEffects []
676 
677  SeeAlso []
678 
679 ***********************************************************************/
680 void Ivy_NodeAssignRandom( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj )
681 {
682  Ivy_FraigSim_t * pSims;
683  int i;
684  assert( Ivy_ObjIsPi(pObj) );
685  pSims = Ivy_ObjSim(pObj);
686  for ( i = 0; i < p->nSimWords; i++ )
687  pSims->pData[i] = Ivy_ObjRandomSim();
688 }
689 
690 /**Function*************************************************************
691 
692  Synopsis [Assigns constant patterns to the PI node.]
693 
694  Description []
695 
696  SideEffects []
697 
698  SeeAlso []
699 
700 ***********************************************************************/
701 void Ivy_NodeAssignConst( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj, int fConst1 )
702 {
703  Ivy_FraigSim_t * pSims;
704  int i;
705  assert( Ivy_ObjIsPi(pObj) );
706  pSims = Ivy_ObjSim(pObj);
707  for ( i = 0; i < p->nSimWords; i++ )
708  pSims->pData[i] = fConst1? ~(unsigned)0 : 0;
709 }
710 
711 /**Function*************************************************************
712 
713  Synopsis [Assings random simulation info for the PIs.]
714 
715  Description []
716 
717  SideEffects []
718 
719  SeeAlso []
720 
721 ***********************************************************************/
722 void Ivy_FraigAssignRandom( Ivy_FraigMan_t * p )
723 {
724  Ivy_Obj_t * pObj;
725  int i;
726  Ivy_ManForEachPi( p->pManAig, pObj, i )
727  Ivy_NodeAssignRandom( p, pObj );
728 }
729 
730 /**Function*************************************************************
731 
732  Synopsis [Assings distance-1 simulation info for the PIs.]
733 
734  Description []
735 
736  SideEffects []
737 
738  SeeAlso []
739 
740 ***********************************************************************/
741 void Ivy_FraigAssignDist1( Ivy_FraigMan_t * p, unsigned * pPat )
742 {
743  Ivy_Obj_t * pObj;
744  int i, Limit;
745  Ivy_ManForEachPi( p->pManAig, pObj, i )
746  {
747  Ivy_NodeAssignConst( p, pObj, Ivy_InfoHasBit(pPat, i) );
748 // printf( "%d", Ivy_InfoHasBit(pPat, i) );
749  }
750 // printf( "\n" );
751 
752  Limit = IVY_MIN( Ivy_ManPiNum(p->pManAig), p->nSimWords * 32 - 1 );
753  for ( i = 0; i < Limit; i++ )
754  Ivy_InfoXorBit( Ivy_ObjSim( Ivy_ManPi(p->pManAig,i) )->pData, i+1 );
755 }
756 
757 /**Function*************************************************************
758 
759  Synopsis [Returns 1 if simulation info is composed of all zeros.]
760 
761  Description []
762 
763  SideEffects []
764 
765  SeeAlso []
766 
767 ***********************************************************************/
768 int Ivy_NodeHasZeroSim( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj )
769 {
770  Ivy_FraigSim_t * pSims;
771  int i;
772  pSims = Ivy_ObjSim(pObj);
773  for ( i = 0; i < p->nSimWords; i++ )
774  if ( pSims->pData[i] )
775  return 0;
776  return 1;
777 }
778 
779 /**Function*************************************************************
780 
781  Synopsis [Returns 1 if simulation info is composed of all zeros.]
782 
783  Description []
784 
785  SideEffects []
786 
787  SeeAlso []
788 
789 ***********************************************************************/
790 void Ivy_NodeComplementSim( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj )
791 {
792  Ivy_FraigSim_t * pSims;
793  int i;
794  pSims = Ivy_ObjSim(pObj);
795  for ( i = 0; i < p->nSimWords; i++ )
796  pSims->pData[i] = ~pSims->pData[i];
797 }
798 
799 /**Function*************************************************************
800 
801  Synopsis [Returns 1 if simulation infos are equal.]
802 
803  Description []
804 
805  SideEffects []
806 
807  SeeAlso []
808 
809 ***********************************************************************/
810 int Ivy_NodeCompareSims( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj0, Ivy_Obj_t * pObj1 )
811 {
812  Ivy_FraigSim_t * pSims0, * pSims1;
813  int i;
814  pSims0 = Ivy_ObjSim(pObj0);
815  pSims1 = Ivy_ObjSim(pObj1);
816  for ( i = 0; i < p->nSimWords; i++ )
817  if ( pSims0->pData[i] != pSims1->pData[i] )
818  return 0;
819  return 1;
820 }
821 
822 /**Function*************************************************************
823 
824  Synopsis [Simulates one node.]
825 
826  Description []
827 
828  SideEffects []
829 
830  SeeAlso []
831 
832 ***********************************************************************/
833 void Ivy_NodeSimulateSim( Ivy_FraigMan_t * p, Ivy_FraigSim_t * pSims )
834 {
835  unsigned * pData, * pData0, * pData1;
836  int i;
837  pData = pSims->pData;
838  pData0 = pSims->pFanin0->pData;
839  pData1 = pSims->pFanin1->pData;
840  switch( pSims->Type )
841  {
842  case 0:
843  for ( i = 0; i < p->nSimWords; i++ )
844  pData[i] = (pData0[i] & pData1[i]);
845  break;
846  case 1:
847  for ( i = 0; i < p->nSimWords; i++ )
848  pData[i] = ~(pData0[i] & pData1[i]);
849  break;
850  case 2:
851  for ( i = 0; i < p->nSimWords; i++ )
852  pData[i] = (pData0[i] & ~pData1[i]);
853  break;
854  case 3:
855  for ( i = 0; i < p->nSimWords; i++ )
856  pData[i] = (~pData0[i] | pData1[i]);
857  break;
858  case 4:
859  for ( i = 0; i < p->nSimWords; i++ )
860  pData[i] = (~pData0[i] & pData1[i]);
861  break;
862  case 5:
863  for ( i = 0; i < p->nSimWords; i++ )
864  pData[i] = (pData0[i] | ~pData1[i]);
865  break;
866  case 6:
867  for ( i = 0; i < p->nSimWords; i++ )
868  pData[i] = ~(pData0[i] | pData1[i]);
869  break;
870  case 7:
871  for ( i = 0; i < p->nSimWords; i++ )
872  pData[i] = (pData0[i] | pData1[i]);
873  break;
874  }
875 }
876 
877 /**Function*************************************************************
878 
879  Synopsis [Simulates one node.]
880 
881  Description []
882 
883  SideEffects []
884 
885  SeeAlso []
886 
887 ***********************************************************************/
888 void Ivy_NodeSimulate( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj )
889 {
890  Ivy_FraigSim_t * pSims, * pSims0, * pSims1;
891  int fCompl, fCompl0, fCompl1, i;
892  assert( !Ivy_IsComplement(pObj) );
893  // get hold of the simulation information
894  pSims = Ivy_ObjSim(pObj);
895  pSims0 = Ivy_ObjSim(Ivy_ObjFanin0(pObj));
896  pSims1 = Ivy_ObjSim(Ivy_ObjFanin1(pObj));
897  // get complemented attributes of the children using their random info
898  fCompl = pObj->fPhase;
899  fCompl0 = Ivy_ObjFaninPhase(Ivy_ObjChild0(pObj));
900  fCompl1 = Ivy_ObjFaninPhase(Ivy_ObjChild1(pObj));
901  // simulate
902  if ( fCompl0 && fCompl1 )
903  {
904  if ( fCompl )
905  for ( i = 0; i < p->nSimWords; i++ )
906  pSims->pData[i] = (pSims0->pData[i] | pSims1->pData[i]);
907  else
908  for ( i = 0; i < p->nSimWords; i++ )
909  pSims->pData[i] = ~(pSims0->pData[i] | pSims1->pData[i]);
910  }
911  else if ( fCompl0 && !fCompl1 )
912  {
913  if ( fCompl )
914  for ( i = 0; i < p->nSimWords; i++ )
915  pSims->pData[i] = (pSims0->pData[i] | ~pSims1->pData[i]);
916  else
917  for ( i = 0; i < p->nSimWords; i++ )
918  pSims->pData[i] = (~pSims0->pData[i] & pSims1->pData[i]);
919  }
920  else if ( !fCompl0 && fCompl1 )
921  {
922  if ( fCompl )
923  for ( i = 0; i < p->nSimWords; i++ )
924  pSims->pData[i] = (~pSims0->pData[i] | pSims1->pData[i]);
925  else
926  for ( i = 0; i < p->nSimWords; i++ )
927  pSims->pData[i] = (pSims0->pData[i] & ~pSims1->pData[i]);
928  }
929  else // if ( !fCompl0 && !fCompl1 )
930  {
931  if ( fCompl )
932  for ( i = 0; i < p->nSimWords; i++ )
933  pSims->pData[i] = ~(pSims0->pData[i] & pSims1->pData[i]);
934  else
935  for ( i = 0; i < p->nSimWords; i++ )
936  pSims->pData[i] = (pSims0->pData[i] & pSims1->pData[i]);
937  }
938 }
939 
940 /**Function*************************************************************
941 
942  Synopsis [Computes hash value using simulation info.]
943 
944  Description []
945 
946  SideEffects []
947 
948  SeeAlso []
949 
950 ***********************************************************************/
951 unsigned Ivy_NodeHash( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj )
952 {
953  static int s_FPrimes[128] = {
954  1009, 1049, 1093, 1151, 1201, 1249, 1297, 1361, 1427, 1459,
955  1499, 1559, 1607, 1657, 1709, 1759, 1823, 1877, 1933, 1997,
956  2039, 2089, 2141, 2213, 2269, 2311, 2371, 2411, 2467, 2543,
957  2609, 2663, 2699, 2741, 2797, 2851, 2909, 2969, 3037, 3089,
958  3169, 3221, 3299, 3331, 3389, 3461, 3517, 3557, 3613, 3671,
959  3719, 3779, 3847, 3907, 3943, 4013, 4073, 4129, 4201, 4243,
960  4289, 4363, 4441, 4493, 4549, 4621, 4663, 4729, 4793, 4871,
961  4933, 4973, 5021, 5087, 5153, 5227, 5281, 5351, 5417, 5471,
962  5519, 5573, 5651, 5693, 5749, 5821, 5861, 5923, 6011, 6073,
963  6131, 6199, 6257, 6301, 6353, 6397, 6481, 6563, 6619, 6689,
964  6737, 6803, 6863, 6917, 6977, 7027, 7109, 7187, 7237, 7309,
965  7393, 7477, 7523, 7561, 7607, 7681, 7727, 7817, 7877, 7933,
966  8011, 8039, 8059, 8081, 8093, 8111, 8123, 8147
967  };
968  Ivy_FraigSim_t * pSims;
969  unsigned uHash;
970  int i;
971  assert( p->nSimWords <= 128 );
972  uHash = 0;
973  pSims = Ivy_ObjSim(pObj);
974  for ( i = 0; i < p->nSimWords; i++ )
975  uHash ^= pSims->pData[i] * s_FPrimes[i];
976  return uHash;
977 }
978 
979 /**Function*************************************************************
980 
981  Synopsis [Simulates AIG manager.]
982 
983  Description [Assumes that the PI simulation info is attached.]
984 
985  SideEffects []
986 
987  SeeAlso []
988 
989 ***********************************************************************/
990 void Ivy_FraigSimulateOne( Ivy_FraigMan_t * p )
991 {
992  Ivy_Obj_t * pObj;
993  int i;
994  abctime clk;
995 clk = Abc_Clock();
996  Ivy_ManForEachNode( p->pManAig, pObj, i )
997  {
998  Ivy_NodeSimulate( p, pObj );
999 /*
1000  if ( Ivy_ObjFraig(pObj) == NULL )
1001  printf( "%3d --- -- %d : ", pObj->Id, pObj->fPhase );
1002  else
1003  printf( "%3d %3d %2d %d : ", pObj->Id, Ivy_Regular(Ivy_ObjFraig(pObj))->Id, Ivy_ObjSatNum(Ivy_Regular(Ivy_ObjFraig(pObj))), pObj->fPhase );
1004  Extra_PrintBinary( stdout, Ivy_ObjSim(pObj), 30 );
1005  printf( "\n" );
1006 */
1007  }
1008 p->timeSim += Abc_Clock() - clk;
1009 p->nSimRounds++;
1010 }
1011 
1012 /**Function*************************************************************
1013 
1014  Synopsis [Simulates AIG manager.]
1015 
1016  Description [Assumes that the PI simulation info is attached.]
1017 
1018  SideEffects []
1019 
1020  SeeAlso []
1021 
1022 ***********************************************************************/
1023 void Ivy_FraigSimulateOneSim( Ivy_FraigMan_t * p )
1024 {
1025  Ivy_FraigSim_t * pSims;
1026  abctime clk;
1027 clk = Abc_Clock();
1028  for ( pSims = p->pSimStart; pSims; pSims = pSims->pNext )
1029  Ivy_NodeSimulateSim( p, pSims );
1030 p->timeSim += Abc_Clock() - clk;
1031 p->nSimRounds++;
1032 }
1033 
1034 /**Function*************************************************************
1035 
1036  Synopsis [Adds one node to the equivalence class.]
1037 
1038  Description []
1039 
1040  SideEffects []
1041 
1042  SeeAlso []
1043 
1044 ***********************************************************************/
1045 void Ivy_NodeAddToClass( Ivy_Obj_t * pClass, Ivy_Obj_t * pObj )
1046 {
1047  if ( Ivy_ObjClassNodeNext(pClass) == NULL )
1048  Ivy_ObjSetClassNodeNext( pClass, pObj );
1049  else
1050  Ivy_ObjSetClassNodeNext( Ivy_ObjClassNodeLast(pClass), pObj );
1051  Ivy_ObjSetClassNodeLast( pClass, pObj );
1052  Ivy_ObjSetClassNodeRepr( pObj, pClass );
1053  Ivy_ObjSetClassNodeNext( pObj, NULL );
1054 }
1055 
1056 /**Function*************************************************************
1057 
1058  Synopsis [Adds equivalence class to the list of classes.]
1059 
1060  Description []
1061 
1062  SideEffects []
1063 
1064  SeeAlso []
1065 
1066 ***********************************************************************/
1067 void Ivy_FraigAddClass( Ivy_FraigList_t * pList, Ivy_Obj_t * pClass )
1068 {
1069  if ( pList->pHead == NULL )
1070  {
1071  pList->pHead = pClass;
1072  pList->pTail = pClass;
1073  Ivy_ObjSetEquivListPrev( pClass, NULL );
1074  Ivy_ObjSetEquivListNext( pClass, NULL );
1075  }
1076  else
1077  {
1078  Ivy_ObjSetEquivListNext( pList->pTail, pClass );
1079  Ivy_ObjSetEquivListPrev( pClass, pList->pTail );
1080  Ivy_ObjSetEquivListNext( pClass, NULL );
1081  pList->pTail = pClass;
1082  }
1083  pList->nItems++;
1084 }
1085 
1086 /**Function*************************************************************
1087 
1088  Synopsis [Updates the list of classes after base class has split.]
1089 
1090  Description []
1091 
1092  SideEffects []
1093 
1094  SeeAlso []
1095 
1096 ***********************************************************************/
1097 void Ivy_FraigInsertClass( Ivy_FraigList_t * pList, Ivy_Obj_t * pBase, Ivy_Obj_t * pClass )
1098 {
1099  Ivy_ObjSetEquivListPrev( pClass, pBase );
1100  Ivy_ObjSetEquivListNext( pClass, Ivy_ObjEquivListNext(pBase) );
1101  if ( Ivy_ObjEquivListNext(pBase) )
1102  Ivy_ObjSetEquivListPrev( Ivy_ObjEquivListNext(pBase), pClass );
1103  Ivy_ObjSetEquivListNext( pBase, pClass );
1104  if ( pList->pTail == pBase )
1105  pList->pTail = pClass;
1106  pList->nItems++;
1107 }
1108 
1109 /**Function*************************************************************
1110 
1111  Synopsis [Removes equivalence class from the list of classes.]
1112 
1113  Description []
1114 
1115  SideEffects []
1116 
1117  SeeAlso []
1118 
1119 ***********************************************************************/
1120 void Ivy_FraigRemoveClass( Ivy_FraigList_t * pList, Ivy_Obj_t * pClass )
1121 {
1122  if ( pList->pHead == pClass )
1123  pList->pHead = Ivy_ObjEquivListNext(pClass);
1124  if ( pList->pTail == pClass )
1125  pList->pTail = Ivy_ObjEquivListPrev(pClass);
1126  if ( Ivy_ObjEquivListPrev(pClass) )
1127  Ivy_ObjSetEquivListNext( Ivy_ObjEquivListPrev(pClass), Ivy_ObjEquivListNext(pClass) );
1128  if ( Ivy_ObjEquivListNext(pClass) )
1129  Ivy_ObjSetEquivListPrev( Ivy_ObjEquivListNext(pClass), Ivy_ObjEquivListPrev(pClass) );
1130  Ivy_ObjSetEquivListNext( pClass, NULL );
1131  Ivy_ObjSetEquivListPrev( pClass, NULL );
1132  pClass->fMarkA = 0;
1133  pList->nItems--;
1134 }
1135 
1136 /**Function*************************************************************
1137 
1138  Synopsis [Count the number of pairs.]
1139 
1140  Description []
1141 
1142  SideEffects []
1143 
1144  SeeAlso []
1145 
1146 ***********************************************************************/
1147 int Ivy_FraigCountPairsClasses( Ivy_FraigMan_t * p )
1148 {
1149  Ivy_Obj_t * pClass, * pNode;
1150  int nPairs = 0, nNodes;
1151  return nPairs;
1152 
1153  Ivy_FraigForEachEquivClass( p->lClasses.pHead, pClass )
1154  {
1155  nNodes = 0;
1156  Ivy_FraigForEachClassNode( pClass, pNode )
1157  nNodes++;
1158  nPairs += nNodes * (nNodes - 1) / 2;
1159  }
1160  return nPairs;
1161 }
1162 
1163 /**Function*************************************************************
1164 
1165  Synopsis [Creates initial simulation classes.]
1166 
1167  Description [Assumes that simulation info is assigned.]
1168 
1169  SideEffects []
1170 
1171  SeeAlso []
1172 
1173 ***********************************************************************/
1174 void Ivy_FraigCreateClasses( Ivy_FraigMan_t * p )
1175 {
1176  Ivy_Obj_t ** pTable;
1177  Ivy_Obj_t * pObj, * pConst1, * pBin, * pEntry;
1178  int i, nTableSize;
1179  unsigned Hash;
1180  pConst1 = Ivy_ManConst1(p->pManAig);
1181  // allocate the table
1182  nTableSize = Ivy_ManObjNum(p->pManAig) / 2 + 13;
1183  pTable = ABC_ALLOC( Ivy_Obj_t *, nTableSize );
1184  memset( pTable, 0, sizeof(Ivy_Obj_t *) * nTableSize );
1185  // collect nodes into the table
1186  Ivy_ManForEachObj( p->pManAig, pObj, i )
1187  {
1188  if ( !Ivy_ObjIsPi(pObj) && !Ivy_ObjIsNode(pObj) )
1189  continue;
1190  Hash = Ivy_NodeHash( p, pObj );
1191  if ( Hash == 0 && Ivy_NodeHasZeroSim( p, pObj ) )
1192  {
1193  Ivy_NodeAddToClass( pConst1, pObj );
1194  continue;
1195  }
1196  // add the node to the table
1197  pBin = pTable[Hash % nTableSize];
1198  Ivy_FraigForEachBinNode( pBin, pEntry )
1199  if ( Ivy_NodeCompareSims( p, pEntry, pObj ) )
1200  {
1201  Ivy_NodeAddToClass( pEntry, pObj );
1202  break;
1203  }
1204  // check if the entry was added
1205  if ( pEntry )
1206  continue;
1207  Ivy_ObjSetNodeHashNext( pObj, pBin );
1208  pTable[Hash % nTableSize] = pObj;
1209  }
1210  // collect non-trivial classes
1211  assert( p->lClasses.pHead == NULL );
1212  Ivy_ManForEachObj( p->pManAig, pObj, i )
1213  {
1214  if ( !Ivy_ObjIsConst1(pObj) && !Ivy_ObjIsPi(pObj) && !Ivy_ObjIsNode(pObj) )
1215  continue;
1216  Ivy_ObjSetNodeHashNext( pObj, NULL );
1217  if ( Ivy_ObjClassNodeRepr(pObj) == NULL )
1218  {
1219  assert( Ivy_ObjClassNodeNext(pObj) == NULL );
1220  continue;
1221  }
1222  // recognize the head of the class
1223  if ( Ivy_ObjClassNodeNext( Ivy_ObjClassNodeRepr(pObj) ) != NULL )
1224  continue;
1225  // clean the class representative and add it to the list
1226  Ivy_ObjSetClassNodeRepr( pObj, NULL );
1227  Ivy_FraigAddClass( &p->lClasses, pObj );
1228  }
1229  // free the table
1230  ABC_FREE( pTable );
1231 }
1232 
1233 /**Function*************************************************************
1234 
1235  Synopsis [Recursively refines the class after simulation.]
1236 
1237  Description [Returns 1 if the class has changed.]
1238 
1239  SideEffects []
1240 
1241  SeeAlso []
1242 
1243 ***********************************************************************/
1244 int Ivy_FraigRefineClass_rec( Ivy_FraigMan_t * p, Ivy_Obj_t * pClass )
1245 {
1246  Ivy_Obj_t * pClassNew, * pListOld, * pListNew, * pNode;
1247  int RetValue = 0;
1248  // check if there is refinement
1249  pListOld = pClass;
1250  Ivy_FraigForEachClassNode( Ivy_ObjClassNodeNext(pClass), pClassNew )
1251  {
1252  if ( !Ivy_NodeCompareSims(p, pClass, pClassNew) )
1253  {
1254  if ( p->pParams->fPatScores )
1255  Ivy_FraigAddToPatScores( p, pClass, pClassNew );
1256  break;
1257  }
1258  pListOld = pClassNew;
1259  }
1260  if ( pClassNew == NULL )
1261  return 0;
1262  // set representative of the new class
1263  Ivy_ObjSetClassNodeRepr( pClassNew, NULL );
1264  // start the new list
1265  pListNew = pClassNew;
1266  // go through the remaining nodes and sort them into two groups:
1267  // (1) matches of the old node; (2) non-matches of the old node
1268  Ivy_FraigForEachClassNode( Ivy_ObjClassNodeNext(pClassNew), pNode )
1269  if ( Ivy_NodeCompareSims( p, pClass, pNode ) )
1270  {
1271  Ivy_ObjSetClassNodeNext( pListOld, pNode );
1272  pListOld = pNode;
1273  }
1274  else
1275  {
1276  Ivy_ObjSetClassNodeNext( pListNew, pNode );
1277  Ivy_ObjSetClassNodeRepr( pNode, pClassNew );
1278  pListNew = pNode;
1279  }
1280  // finish both lists
1281  Ivy_ObjSetClassNodeNext( pListNew, NULL );
1282  Ivy_ObjSetClassNodeNext( pListOld, NULL );
1283  // update the list of classes
1284  Ivy_FraigInsertClass( &p->lClasses, pClass, pClassNew );
1285  // if the old class is trivial, remove it
1286  if ( Ivy_ObjClassNodeNext(pClass) == NULL )
1287  Ivy_FraigRemoveClass( &p->lClasses, pClass );
1288  // if the new class is trivial, remove it; otherwise, try to refine it
1289  if ( Ivy_ObjClassNodeNext(pClassNew) == NULL )
1290  Ivy_FraigRemoveClass( &p->lClasses, pClassNew );
1291  else
1292  RetValue = Ivy_FraigRefineClass_rec( p, pClassNew );
1293  return RetValue + 1;
1294 }
1295 
1296 /**Function*************************************************************
1297 
1298  Synopsis [Creates the counter-example from the successful pattern.]
1299 
1300  Description []
1301 
1302  SideEffects []
1303 
1304  SeeAlso []
1305 
1306 ***********************************************************************/
1307 void Ivy_FraigCheckOutputSimsSavePattern( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj )
1308 {
1309  Ivy_FraigSim_t * pSims;
1310  int i, k, BestPat, * pModel;
1311  // find the word of the pattern
1312  pSims = Ivy_ObjSim(pObj);
1313  for ( i = 0; i < p->nSimWords; i++ )
1314  if ( pSims->pData[i] )
1315  break;
1316  assert( i < p->nSimWords );
1317  // find the bit of the pattern
1318  for ( k = 0; k < 32; k++ )
1319  if ( pSims->pData[i] & (1 << k) )
1320  break;
1321  assert( k < 32 );
1322  // determine the best pattern
1323  BestPat = i * 32 + k;
1324  // fill in the counter-example data
1325  pModel = ABC_ALLOC( int, Ivy_ManPiNum(p->pManFraig) );
1326  Ivy_ManForEachPi( p->pManAig, pObj, i )
1327  {
1328  pModel[i] = Ivy_InfoHasBit(Ivy_ObjSim(pObj)->pData, BestPat);
1329 // printf( "%d", pModel[i] );
1330  }
1331 // printf( "\n" );
1332  // set the model
1333  assert( p->pManFraig->pData == NULL );
1334  p->pManFraig->pData = pModel;
1335  return;
1336 }
1337 
1338 /**Function*************************************************************
1339 
1340  Synopsis [Returns 1 if the one of the output is already non-constant 0.]
1341 
1342  Description []
1343 
1344  SideEffects []
1345 
1346  SeeAlso []
1347 
1348 ***********************************************************************/
1349 int Ivy_FraigCheckOutputSims( Ivy_FraigMan_t * p )
1350 {
1351  Ivy_Obj_t * pObj;
1352  int i;
1353  // make sure the reference simulation pattern does not detect the bug
1354 // pObj = Ivy_ManPo( p->pManAig, 0 );
1355  Ivy_ManForEachPo( p->pManAig, pObj, i )
1356  {
1357  assert( Ivy_ObjFanin0(pObj)->fPhase == (unsigned)Ivy_ObjFaninC0(pObj) ); // Ivy_ObjFaninPhase(Ivy_ObjChild0(pObj)) == 0
1358  // complement simulation info
1359 // if ( Ivy_ObjFanin0(pObj)->fPhase ^ Ivy_ObjFaninC0(pObj) ) // Ivy_ObjFaninPhase(Ivy_ObjChild0(pObj))
1360 // Ivy_NodeComplementSim( p, Ivy_ObjFanin0(pObj) );
1361  // check
1362  if ( !Ivy_NodeHasZeroSim( p, Ivy_ObjFanin0(pObj) ) )
1363  {
1364  // create the counter-example from this pattern
1365  Ivy_FraigCheckOutputSimsSavePattern( p, Ivy_ObjFanin0(pObj) );
1366  return 1;
1367  }
1368  // complement simulation info
1369 // if ( Ivy_ObjFanin0(pObj)->fPhase ^ Ivy_ObjFaninC0(pObj) )
1370 // Ivy_NodeComplementSim( p, Ivy_ObjFanin0(pObj) );
1371  }
1372  return 0;
1373 }
1374 
1375 /**Function*************************************************************
1376 
1377  Synopsis [Refines the classes after simulation.]
1378 
1379  Description [Assumes that simulation info is assigned. Returns the
1380  number of classes refined.]
1381 
1382  SideEffects [Large equivalence class of constant 0 may cause problems.]
1383 
1384  SeeAlso []
1385 
1386 ***********************************************************************/
1387 int Ivy_FraigRefineClasses( Ivy_FraigMan_t * p )
1388 {
1389  Ivy_Obj_t * pClass, * pClass2;
1390  int RetValue, Counter = 0;
1391  abctime clk;
1392  // check if some outputs already became non-constant
1393  // this is a special case when computation can be stopped!!!
1394  if ( p->pParams->fProve )
1395  Ivy_FraigCheckOutputSims( p );
1396  if ( p->pManFraig->pData )
1397  return 0;
1398  // refine the classed
1399 clk = Abc_Clock();
1400  Ivy_FraigForEachEquivClassSafe( p->lClasses.pHead, pClass, pClass2 )
1401  {
1402  if ( pClass->fMarkA )
1403  continue;
1404  RetValue = Ivy_FraigRefineClass_rec( p, pClass );
1405  Counter += ( RetValue > 0 );
1406 //if ( Ivy_ObjIsConst1(pClass) )
1407 //printf( "%d ", RetValue );
1408 //if ( Ivy_ObjIsConst1(pClass) )
1409 // p->time1 += Abc_Clock() - clk;
1410  }
1411 p->timeRef += Abc_Clock() - clk;
1412  return Counter;
1413 }
1414 
1415 /**Function*************************************************************
1416 
1417  Synopsis [Print the class.]
1418 
1419  Description []
1420 
1421  SideEffects []
1422 
1423  SeeAlso []
1424 
1425 ***********************************************************************/
1426 void Ivy_FraigPrintClass( Ivy_Obj_t * pClass )
1427 {
1428  Ivy_Obj_t * pObj;
1429  printf( "Class {" );
1430  Ivy_FraigForEachClassNode( pClass, pObj )
1431  printf( " %d(%d)%c", pObj->Id, pObj->Level, pObj->fPhase? '+' : '-' );
1432  printf( " }\n" );
1433 }
1434 
1435 /**Function*************************************************************
1436 
1437  Synopsis [Count the number of elements in the class.]
1438 
1439  Description []
1440 
1441  SideEffects []
1442 
1443  SeeAlso []
1444 
1445 ***********************************************************************/
1446 int Ivy_FraigCountClassNodes( Ivy_Obj_t * pClass )
1447 {
1448  Ivy_Obj_t * pObj;
1449  int Counter = 0;
1450  Ivy_FraigForEachClassNode( pClass, pObj )
1451  Counter++;
1452  return Counter;
1453 }
1454 
1455 /**Function*************************************************************
1456 
1457  Synopsis [Prints simulation classes.]
1458 
1459  Description []
1460 
1461  SideEffects []
1462 
1463  SeeAlso []
1464 
1465 ***********************************************************************/
1466 void Ivy_FraigPrintSimClasses( Ivy_FraigMan_t * p )
1467 {
1468  Ivy_Obj_t * pClass;
1469  Ivy_FraigForEachEquivClass( p->lClasses.pHead, pClass )
1470  {
1471 // Ivy_FraigPrintClass( pClass );
1472  printf( "%d ", Ivy_FraigCountClassNodes( pClass ) );
1473  }
1474 // printf( "\n" );
1475 }
1476 
1477 /**Function*************************************************************
1478 
1479  Synopsis [Generated const 0 pattern.]
1480 
1481  Description []
1482 
1483  SideEffects []
1484 
1485  SeeAlso []
1486 
1487 ***********************************************************************/
1488 void Ivy_FraigSavePattern0( Ivy_FraigMan_t * p )
1489 {
1490  memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords );
1491 }
1492 
1493 /**Function*************************************************************
1494 
1495  Synopsis [[Generated const 1 pattern.]
1496 
1497  Description []
1498 
1499  SideEffects []
1500 
1501  SeeAlso []
1502 
1503 ***********************************************************************/
1504 void Ivy_FraigSavePattern1( Ivy_FraigMan_t * p )
1505 {
1506  memset( p->pPatWords, 0xff, sizeof(unsigned) * p->nPatWords );
1507 }
1508 
1509 /**Function*************************************************************
1510 
1511  Synopsis [Generates the counter-example satisfying the miter.]
1512 
1513  Description []
1514 
1515  SideEffects []
1516 
1517  SeeAlso []
1518 
1519 ***********************************************************************/
1520 int * Ivy_FraigCreateModel( Ivy_FraigMan_t * p )
1521 {
1522  int * pModel;
1523  Ivy_Obj_t * pObj;
1524  int i;
1525  pModel = ABC_ALLOC( int, Ivy_ManPiNum(p->pManFraig) );
1526  Ivy_ManForEachPi( p->pManFraig, pObj, i )
1527 // pModel[i] = ( p->pSat->model.ptr[Ivy_ObjSatNum(pObj)] == l_True );
1528  pModel[i] = ( p->pSat->model[Ivy_ObjSatNum(pObj)] == l_True );
1529  return pModel;
1530 }
1531 
1532 /**Function*************************************************************
1533 
1534  Synopsis [Copy pattern from the solver into the internal storage.]
1535 
1536  Description []
1537 
1538  SideEffects []
1539 
1540  SeeAlso []
1541 
1542 ***********************************************************************/
1543 void Ivy_FraigSavePattern( Ivy_FraigMan_t * p )
1544 {
1545  Ivy_Obj_t * pObj;
1546  int i;
1547  memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords );
1548  Ivy_ManForEachPi( p->pManFraig, pObj, i )
1549 // Vec_PtrForEachEntry( Ivy_Obj_t *, p->vPiVars, pObj, i )
1550 // if ( p->pSat->model.ptr[Ivy_ObjSatNum(pObj)] == l_True )
1551  if ( p->pSat->model[Ivy_ObjSatNum(pObj)] == l_True )
1552  Ivy_InfoSetBit( p->pPatWords, i );
1553 // Ivy_InfoSetBit( p->pPatWords, pObj->Id - 1 );
1554 }
1555 
1556 /**Function*************************************************************
1557 
1558  Synopsis [Copy pattern from the solver into the internal storage.]
1559 
1560  Description []
1561 
1562  SideEffects []
1563 
1564  SeeAlso []
1565 
1566 ***********************************************************************/
1567 void Ivy_FraigSavePattern2( Ivy_FraigMan_t * p )
1568 {
1569  Ivy_Obj_t * pObj;
1570  int i;
1571  memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords );
1572 // Ivy_ManForEachPi( p->pManFraig, pObj, i )
1573  Vec_PtrForEachEntry( Ivy_Obj_t *, p->vPiVars, pObj, i )
1574 // if ( p->pSat->model.ptr[Ivy_ObjSatNum(pObj)] == l_True )
1575  if ( p->pSat->model[Ivy_ObjSatNum(pObj)] == l_True )
1576 // Ivy_InfoSetBit( p->pPatWords, i );
1577  Ivy_InfoSetBit( p->pPatWords, pObj->Id - 1 );
1578 }
1579 
1580 /**Function*************************************************************
1581 
1582  Synopsis [Copy pattern from the solver into the internal storage.]
1583 
1584  Description []
1585 
1586  SideEffects []
1587 
1588  SeeAlso []
1589 
1590 ***********************************************************************/
1591 void Ivy_FraigSavePattern3( Ivy_FraigMan_t * p )
1592 {
1593  Ivy_Obj_t * pObj;
1594  int i;
1595  for ( i = 0; i < p->nPatWords; i++ )
1596  p->pPatWords[i] = Ivy_ObjRandomSim();
1597  Vec_PtrForEachEntry( Ivy_Obj_t *, p->vPiVars, pObj, i )
1598 // if ( Ivy_InfoHasBit( p->pPatWords, pObj->Id - 1 ) ^ (p->pSat->model.ptr[Ivy_ObjSatNum(pObj)] == l_True) )
1599  if ( Ivy_InfoHasBit( p->pPatWords, pObj->Id - 1 ) ^ sat_solver_var_value(p->pSat, Ivy_ObjSatNum(pObj)) )
1600  Ivy_InfoXorBit( p->pPatWords, pObj->Id - 1 );
1601 }
1602 
1603 
1604 /**Function*************************************************************
1605 
1606  Synopsis [Performs simulation of the manager.]
1607 
1608  Description []
1609 
1610  SideEffects []
1611 
1612  SeeAlso []
1613 
1614 ***********************************************************************/
1615 void Ivy_FraigSimulate( Ivy_FraigMan_t * p )
1616 {
1617  int nChanges, nClasses;
1618  // start the classes
1619  Ivy_FraigAssignRandom( p );
1620  Ivy_FraigSimulateOne( p );
1621  Ivy_FraigCreateClasses( p );
1622 //printf( "Starting classes = %5d. Pairs = %6d.\n", p->lClasses.nItems, Ivy_FraigCountPairsClasses(p) );
1623  // refine classes by walking 0/1 patterns
1624  Ivy_FraigSavePattern0( p );
1625  Ivy_FraigAssignDist1( p, p->pPatWords );
1626  Ivy_FraigSimulateOne( p );
1627  nChanges = Ivy_FraigRefineClasses( p );
1628  if ( p->pManFraig->pData )
1629  return;
1630 //printf( "Refined classes = %5d. Changes = %4d. Pairs = %6d.\n", p->lClasses.nItems, nChanges, Ivy_FraigCountPairsClasses(p) );
1631  Ivy_FraigSavePattern1( p );
1632  Ivy_FraigAssignDist1( p, p->pPatWords );
1633  Ivy_FraigSimulateOne( p );
1634  nChanges = Ivy_FraigRefineClasses( p );
1635  if ( p->pManFraig->pData )
1636  return;
1637 //printf( "Refined classes = %5d. Changes = %4d. Pairs = %6d.\n", p->lClasses.nItems, nChanges, Ivy_FraigCountPairsClasses(p) );
1638  // refine classes by random simulation
1639  do {
1640  Ivy_FraigAssignRandom( p );
1641  Ivy_FraigSimulateOne( p );
1642  nClasses = p->lClasses.nItems;
1643  nChanges = Ivy_FraigRefineClasses( p );
1644  if ( p->pManFraig->pData )
1645  return;
1646 //printf( "Refined classes = %5d. Changes = %4d. Pairs = %6d.\n", p->lClasses.nItems, nChanges, Ivy_FraigCountPairsClasses(p) );
1647  } while ( (double)nChanges / nClasses > p->pParams->dSimSatur );
1648 // Ivy_FraigPrintSimClasses( p );
1649 }
1650 
1651 
1652 
1653 /**Function*************************************************************
1654 
1655  Synopsis [Cleans pattern scores.]
1656 
1657  Description []
1658 
1659  SideEffects []
1660 
1661  SeeAlso []
1662 
1663 ***********************************************************************/
1664 void Ivy_FraigCleanPatScores( Ivy_FraigMan_t * p )
1665 {
1666  int i, nLimit = p->nSimWords * 32;
1667  for ( i = 0; i < nLimit; i++ )
1668  p->pPatScores[i] = 0;
1669 }
1670 
1671 /**Function*************************************************************
1672 
1673  Synopsis [Adds to pattern scores.]
1674 
1675  Description []
1676 
1677  SideEffects []
1678 
1679  SeeAlso []
1680 
1681 ***********************************************************************/
1682 void Ivy_FraigAddToPatScores( Ivy_FraigMan_t * p, Ivy_Obj_t * pClass, Ivy_Obj_t * pClassNew )
1683 {
1684  Ivy_FraigSim_t * pSims0, * pSims1;
1685  unsigned uDiff;
1686  int i, w;
1687  // get hold of the simulation information
1688  pSims0 = Ivy_ObjSim(pClass);
1689  pSims1 = Ivy_ObjSim(pClassNew);
1690  // iterate through the differences and record the score
1691  for ( w = 0; w < p->nSimWords; w++ )
1692  {
1693  uDiff = pSims0->pData[w] ^ pSims1->pData[w];
1694  if ( uDiff == 0 )
1695  continue;
1696  for ( i = 0; i < 32; i++ )
1697  if ( uDiff & ( 1 << i ) )
1698  p->pPatScores[w*32+i]++;
1699  }
1700 }
1701 
1702 /**Function*************************************************************
1703 
1704  Synopsis [Selects the best pattern.]
1705 
1706  Description [Returns 1 if such pattern is found.]
1707 
1708  SideEffects []
1709 
1710  SeeAlso []
1711 
1712 ***********************************************************************/
1713 int Ivy_FraigSelectBestPat( Ivy_FraigMan_t * p )
1714 {
1715  Ivy_FraigSim_t * pSims;
1716  Ivy_Obj_t * pObj;
1717  int i, nLimit = p->nSimWords * 32, MaxScore = 0, BestPat = -1;
1718  for ( i = 1; i < nLimit; i++ )
1719  {
1720  if ( MaxScore < p->pPatScores[i] )
1721  {
1722  MaxScore = p->pPatScores[i];
1723  BestPat = i;
1724  }
1725  }
1726  if ( MaxScore == 0 )
1727  return 0;
1728 // if ( MaxScore > p->pParams->MaxScore )
1729 // printf( "Max score is %3d. ", MaxScore );
1730  // copy the best pattern into the selected pattern
1731  memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords );
1732  Ivy_ManForEachPi( p->pManAig, pObj, i )
1733  {
1734  pSims = Ivy_ObjSim(pObj);
1735  if ( Ivy_InfoHasBit(pSims->pData, BestPat) )
1736  Ivy_InfoSetBit(p->pPatWords, i);
1737  }
1738  return MaxScore;
1739 }
1740 
1741 /**Function*************************************************************
1742 
1743  Synopsis [Resimulates fraiging manager after finding a counter-example.]
1744 
1745  Description []
1746 
1747  SideEffects []
1748 
1749  SeeAlso []
1750 
1751 ***********************************************************************/
1752 void Ivy_FraigResimulate( Ivy_FraigMan_t * p )
1753 {
1754  int nChanges;
1755  Ivy_FraigAssignDist1( p, p->pPatWords );
1756  Ivy_FraigSimulateOne( p );
1757  if ( p->pParams->fPatScores )
1758  Ivy_FraigCleanPatScores( p );
1759  nChanges = Ivy_FraigRefineClasses( p );
1760  if ( p->pManFraig->pData )
1761  return;
1762  if ( nChanges < 1 )
1763  printf( "Error: A counter-example did not refine classes!\n" );
1764  assert( nChanges >= 1 );
1765 //printf( "Refined classes! = %5d. Changes = %4d.\n", p->lClasses.nItems, nChanges );
1766  if ( !p->pParams->fPatScores )
1767  return;
1768 
1769  // perform additional simulation using dist1 patterns derived from successful patterns
1770  while ( Ivy_FraigSelectBestPat(p) > p->pParams->MaxScore )
1771  {
1772  Ivy_FraigAssignDist1( p, p->pPatWords );
1773  Ivy_FraigSimulateOne( p );
1774  Ivy_FraigCleanPatScores( p );
1775  nChanges = Ivy_FraigRefineClasses( p );
1776  if ( p->pManFraig->pData )
1777  return;
1778 //printf( "Refined class!!! = %5d. Changes = %4d. Pairs = %6d.\n", p->lClasses.nItems, nChanges, Ivy_FraigCountPairsClasses(p) );
1779  if ( nChanges == 0 )
1780  break;
1781  }
1782 }
1783 
1784 
1785 /**Function*************************************************************
1786 
1787  Synopsis [Prints the status of the miter.]
1788 
1789  Description []
1790 
1791  SideEffects []
1792 
1793  SeeAlso []
1794 
1795 ***********************************************************************/
1796 void Ivy_FraigMiterPrint( Ivy_Man_t * pNtk, char * pString, abctime clk, int fVerbose )
1797 {
1798  if ( !fVerbose )
1799  return;
1800  printf( "Nodes = %7d. Levels = %4d. ", Ivy_ManNodeNum(pNtk), Ivy_ManLevels(pNtk) );
1801  ABC_PRT( pString, Abc_Clock() - clk );
1802 }
1803 
1804 /**Function*************************************************************
1805 
1806  Synopsis [Reports the status of the miter.]
1807 
1808  Description []
1809 
1810  SideEffects []
1811 
1812  SeeAlso []
1813 
1814 ***********************************************************************/
1815 int Ivy_FraigMiterStatus( Ivy_Man_t * pMan )
1816 {
1817  Ivy_Obj_t * pObj, * pObjNew;
1818  int i, CountConst0 = 0, CountNonConst0 = 0, CountUndecided = 0;
1819  if ( pMan->pData )
1820  return 0;
1821  Ivy_ManForEachPo( pMan, pObj, i )
1822  {
1823  pObjNew = Ivy_ObjChild0(pObj);
1824  // check if the output is constant 1
1825  if ( pObjNew == pMan->pConst1 )
1826  {
1827  CountNonConst0++;
1828  continue;
1829  }
1830  // check if the output is constant 0
1831  if ( pObjNew == Ivy_Not(pMan->pConst1) )
1832  {
1833  CountConst0++;
1834  continue;
1835  }
1836 /*
1837  // check if the output is a primary input
1838  if ( Ivy_ObjIsPi(Ivy_Regular(pObjNew)) )
1839  {
1840  CountNonConst0++;
1841  continue;
1842  }
1843 */
1844  // check if the output can be constant 0
1845  if ( Ivy_Regular(pObjNew)->fPhase != (unsigned)Ivy_IsComplement(pObjNew) )
1846  {
1847  CountNonConst0++;
1848  continue;
1849  }
1850  CountUndecided++;
1851  }
1852 /*
1853  if ( p->pParams->fVerbose )
1854  {
1855  printf( "Miter has %d outputs. ", Ivy_ManPoNum(p->pManAig) );
1856  printf( "Const0 = %d. ", CountConst0 );
1857  printf( "NonConst0 = %d. ", CountNonConst0 );
1858  printf( "Undecided = %d. ", CountUndecided );
1859  printf( "\n" );
1860  }
1861 */
1862  if ( CountNonConst0 )
1863  return 0;
1864  if ( CountUndecided )
1865  return -1;
1866  return 1;
1867 }
1868 
1869 /**Function*************************************************************
1870 
1871  Synopsis [Tries to prove each output of the miter until encountering a sat output.]
1872 
1873  Description []
1874 
1875  SideEffects []
1876 
1877  SeeAlso []
1878 
1879 ***********************************************************************/
1880 void Ivy_FraigMiterProve( Ivy_FraigMan_t * p )
1881 {
1882  Ivy_Obj_t * pObj, * pObjNew;
1883  int i, RetValue;
1884  abctime clk = Abc_Clock();
1885  int fVerbose = 0;
1886  Ivy_ManForEachPo( p->pManAig, pObj, i )
1887  {
1888  if ( i && fVerbose )
1889  {
1890  ABC_PRT( "Time", Abc_Clock() -clk );
1891  }
1892  pObjNew = Ivy_ObjChild0Equiv(pObj);
1893  // check if the output is constant 1
1894  if ( pObjNew == p->pManFraig->pConst1 )
1895  {
1896  if ( fVerbose )
1897  printf( "Output %2d (out of %2d) is constant 1. ", i, Ivy_ManPoNum(p->pManAig) );
1898  // assing constant 0 model
1899  p->pManFraig->pData = ABC_ALLOC( int, Ivy_ManPiNum(p->pManFraig) );
1900  memset( p->pManFraig->pData, 0, sizeof(int) * Ivy_ManPiNum(p->pManFraig) );
1901  break;
1902  }
1903  // check if the output is constant 0
1904  if ( pObjNew == Ivy_Not(p->pManFraig->pConst1) )
1905  {
1906  if ( fVerbose )
1907  printf( "Output %2d (out of %2d) is already constant 0. ", i, Ivy_ManPoNum(p->pManAig) );
1908  continue;
1909  }
1910  // check if the output can be constant 0
1911  if ( Ivy_Regular(pObjNew)->fPhase != (unsigned)Ivy_IsComplement(pObjNew) )
1912  {
1913  if ( fVerbose )
1914  printf( "Output %2d (out of %2d) cannot be constant 0. ", i, Ivy_ManPoNum(p->pManAig) );
1915  // assing constant 0 model
1916  p->pManFraig->pData = ABC_ALLOC( int, Ivy_ManPiNum(p->pManFraig) );
1917  memset( p->pManFraig->pData, 0, sizeof(int) * Ivy_ManPiNum(p->pManFraig) );
1918  break;
1919  }
1920 /*
1921  // check the representative of this node
1922  pRepr = Ivy_ObjClassNodeRepr(Ivy_ObjFanin0(pObj));
1923  if ( Ivy_Regular(pRepr) != p->pManAig->pConst1 )
1924  printf( "Representative is not constant 1.\n" );
1925  else
1926  printf( "Representative is constant 1.\n" );
1927 */
1928  // try to prove the output constant 0
1929  RetValue = Ivy_FraigNodeIsConst( p, Ivy_Regular(pObjNew) );
1930  if ( RetValue == 1 ) // proved equivalent
1931  {
1932  if ( fVerbose )
1933  printf( "Output %2d (out of %2d) was proved constant 0. ", i, Ivy_ManPoNum(p->pManAig) );
1934  // set the constant miter
1935  Ivy_ObjFanin0(pObj)->pEquiv = Ivy_NotCond( p->pManFraig->pConst1, !Ivy_ObjFaninC0(pObj) );
1936  continue;
1937  }
1938  if ( RetValue == -1 ) // failed
1939  {
1940  if ( fVerbose )
1941  printf( "Output %2d (out of %2d) has timed out at %d backtracks. ", i, Ivy_ManPoNum(p->pManAig), p->pParams->nBTLimitMiter );
1942  continue;
1943  }
1944  // proved satisfiable
1945  if ( fVerbose )
1946  printf( "Output %2d (out of %2d) was proved NOT a constant 0. ", i, Ivy_ManPoNum(p->pManAig) );
1947  // create the model
1948  p->pManFraig->pData = Ivy_FraigCreateModel(p);
1949  break;
1950  }
1951  if ( fVerbose )
1952  {
1953  ABC_PRT( "Time", Abc_Clock() -clk );
1954  }
1955 }
1956 
1957 /**Function*************************************************************
1958 
1959  Synopsis [Performs fraiging for the internal nodes.]
1960 
1961  Description []
1962 
1963  SideEffects []
1964 
1965  SeeAlso []
1966 
1967 ***********************************************************************/
1968 void Ivy_FraigSweep( Ivy_FraigMan_t * p )
1969 {
1970  Ivy_Obj_t * pObj;//, * pTemp;
1971  int i, k = 0;
1972 p->nClassesZero = p->lClasses.pHead? (Ivy_ObjIsConst1(p->lClasses.pHead) ? Ivy_FraigCountClassNodes(p->lClasses.pHead) : 0) : 0;
1973 p->nClassesBeg = p->lClasses.nItems;
1974  // duplicate internal nodes
1975  p->pProgress = Extra_ProgressBarStart( stdout, Ivy_ManNodeNum(p->pManAig) );
1976  Ivy_ManForEachNode( p->pManAig, pObj, i )
1977  {
1978  Extra_ProgressBarUpdate( p->pProgress, k++, NULL );
1979  // default to simple strashing if simulation detected a counter-example for a PO
1980  if ( p->pManFraig->pData )
1981  pObj->pEquiv = Ivy_And( p->pManFraig, Ivy_ObjChild0Equiv(pObj), Ivy_ObjChild1Equiv(pObj) );
1982  else
1983  pObj->pEquiv = Ivy_FraigAnd( p, pObj );
1984  assert( pObj->pEquiv != NULL );
1985 // pTemp = Ivy_Regular(pObj->pEquiv);
1986 // assert( Ivy_Regular(pObj->pEquiv)->Type );
1987  }
1988  Extra_ProgressBarStop( p->pProgress );
1989 p->nClassesEnd = p->lClasses.nItems;
1990  // try to prove the outputs of the miter
1991  p->nNodesMiter = Ivy_ManNodeNum(p->pManFraig);
1992 // Ivy_FraigMiterStatus( p->pManFraig );
1993  if ( p->pParams->fProve && p->pManFraig->pData == NULL )
1994  Ivy_FraigMiterProve( p );
1995  // add the POs
1996  Ivy_ManForEachPo( p->pManAig, pObj, i )
1997  Ivy_ObjCreatePo( p->pManFraig, Ivy_ObjChild0Equiv(pObj) );
1998  // clean the old manager
1999  Ivy_ManForEachObj( p->pManAig, pObj, i )
2000  pObj->pFanout = pObj->pNextFan0 = pObj->pNextFan1 = pObj->pPrevFan0 = pObj->pPrevFan1 = NULL;
2001  // clean the new manager
2002  Ivy_ManForEachObj( p->pManFraig, pObj, i )
2003  {
2004  if ( Ivy_ObjFaninVec(pObj) )
2005  Vec_PtrFree( Ivy_ObjFaninVec(pObj) );
2006  pObj->pNextFan0 = pObj->pNextFan1 = NULL;
2007  pObj->pEquiv = NULL;
2008  }
2009  // remove dangling nodes
2010  Ivy_ManCleanup( p->pManFraig );
2011  // clean up the class marks
2012  Ivy_FraigForEachEquivClass( p->lClasses.pHead, pObj )
2013  pObj->fMarkA = 0;
2014 }
2015 
2016 /**Function*************************************************************
2017 
2018  Synopsis [Performs fraiging for one node.]
2019 
2020  Description [Returns the fraiged node.]
2021 
2022  SideEffects []
2023 
2024  SeeAlso []
2025 
2026 ***********************************************************************/
2027 Ivy_Obj_t * Ivy_FraigAnd( Ivy_FraigMan_t * p, Ivy_Obj_t * pObjOld )
2028 {
2029  Ivy_Obj_t * pObjNew, * pFanin0New, * pFanin1New, * pObjReprNew;
2030  int RetValue;
2031  // get the fraiged fanins
2032  pFanin0New = Ivy_ObjChild0Equiv(pObjOld);
2033  pFanin1New = Ivy_ObjChild1Equiv(pObjOld);
2034  // get the candidate fraig node
2035  pObjNew = Ivy_And( p->pManFraig, pFanin0New, pFanin1New );
2036  // get representative of this class
2037  if ( Ivy_ObjClassNodeRepr(pObjOld) == NULL || // this is a unique node
2038  (!p->pParams->fDoSparse && Ivy_ObjClassNodeRepr(pObjOld) == p->pManAig->pConst1) ) // this is a sparse node
2039  {
2040 // assert( Ivy_Regular(pFanin0New) != Ivy_Regular(pFanin1New) );
2041 // assert( pObjNew != Ivy_Regular(pFanin0New) );
2042 // assert( pObjNew != Ivy_Regular(pFanin1New) );
2043  return pObjNew;
2044  }
2045  // get the fraiged representative
2046  pObjReprNew = Ivy_ObjFraig(Ivy_ObjClassNodeRepr(pObjOld));
2047  // if the fraiged nodes are the same return
2048  if ( Ivy_Regular(pObjNew) == Ivy_Regular(pObjReprNew) )
2049  return pObjNew;
2050  assert( Ivy_Regular(pObjNew) != Ivy_ManConst1(p->pManFraig) );
2051 // printf( "Node = %d. Repr = %d.\n", pObjOld->Id, Ivy_ObjClassNodeRepr(pObjOld)->Id );
2052 
2053  // they are different (the counter-example is in p->pPatWords)
2054  RetValue = Ivy_FraigNodesAreEquiv( p, Ivy_Regular(pObjReprNew), Ivy_Regular(pObjNew) );
2055  if ( RetValue == 1 ) // proved equivalent
2056  {
2057  // mark the class as proved
2058  if ( Ivy_ObjClassNodeNext(pObjOld) == NULL )
2059  Ivy_ObjClassNodeRepr(pObjOld)->fMarkA = 1;
2060  return Ivy_NotCond( pObjReprNew, pObjOld->fPhase ^ Ivy_ObjClassNodeRepr(pObjOld)->fPhase );
2061  }
2062  if ( RetValue == -1 ) // failed
2063  return pObjNew;
2064  // simulate the counter-example and return the new node
2065  Ivy_FraigResimulate( p );
2066  return pObjNew;
2067 }
2068 
2069 /**Function*************************************************************
2070 
2071  Synopsis [Prints variable activity.]
2072 
2073  Description []
2074 
2075  SideEffects []
2076 
2077  SeeAlso []
2078 
2079 ***********************************************************************/
2080 void Ivy_FraigPrintActivity( Ivy_FraigMan_t * p )
2081 {
2082  int i;
2083  for ( i = 0; i < p->nSatVars; i++ )
2084  printf( "%d %d ", i, p->pSat->activity[i] );
2085  printf( "\n" );
2086 }
2087 
2088 /**Function*************************************************************
2089 
2090  Synopsis [Runs equivalence test for the two nodes.]
2091 
2092  Description []
2093 
2094  SideEffects []
2095 
2096  SeeAlso []
2097 
2098 ***********************************************************************/
2099 int Ivy_FraigNodesAreEquiv( Ivy_FraigMan_t * p, Ivy_Obj_t * pOld, Ivy_Obj_t * pNew )
2100 {
2101  int pLits[4], RetValue, RetValue1, nBTLimit;
2102  abctime clk; //, clk2 = Abc_Clock();
2103 
2104  // make sure the nodes are not complemented
2105  assert( !Ivy_IsComplement(pNew) );
2106  assert( !Ivy_IsComplement(pOld) );
2107  assert( pNew != pOld );
2108 
2109  // if at least one of the nodes is a failed node, perform adjustments:
2110  // if the backtrack limit is small, simply skip this node
2111  // if the backtrack limit is > 10, take the quare root of the limit
2112  nBTLimit = p->pParams->nBTLimitNode;
2113  if ( nBTLimit > 0 && (pOld->fFailTfo || pNew->fFailTfo) )
2114  {
2115  p->nSatFails++;
2116  // fail immediately
2117 // return -1;
2118  if ( nBTLimit <= 10 )
2119  return -1;
2120  nBTLimit = (int)pow(nBTLimit, 0.7);
2121  }
2122  p->nSatCalls++;
2123 
2124  // make sure the solver is allocated and has enough variables
2125  if ( p->pSat == NULL )
2126  {
2127  p->pSat = sat_solver_new();
2128  sat_solver_setnvars( p->pSat, 1000 );
2129  p->pSat->factors = ABC_CALLOC( double, p->pSat->cap );
2130  p->nSatVars = 1;
2131  // var 0 is reserved for const1 node - add the clause
2132 // pLits[0] = toLit( 0 );
2133 // sat_solver_addclause( p->pSat, pLits, pLits + 1 );
2134  }
2135 
2136  // if the nodes do not have SAT variables, allocate them
2137  Ivy_FraigNodeAddToSolver( p, pOld, pNew );
2138 
2139  // prepare variable activity
2140  Ivy_FraigSetActivityFactors( p, pOld, pNew );
2141 
2142  // solve under assumptions
2143  // A = 1; B = 0 OR A = 1; B = 1
2144 clk = Abc_Clock();
2145  pLits[0] = toLitCond( Ivy_ObjSatNum(pOld), 0 );
2146  pLits[1] = toLitCond( Ivy_ObjSatNum(pNew), pOld->fPhase == pNew->fPhase );
2147 //Sat_SolverWriteDimacs( p->pSat, "temp.cnf", pLits, pLits + 2, 1 );
2148  RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2,
2149  (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0,
2150  p->nBTLimitGlobal, p->nInsLimitGlobal );
2151 p->timeSat += Abc_Clock() - clk;
2152  if ( RetValue1 == l_False )
2153  {
2154 p->timeSatUnsat += Abc_Clock() - clk;
2155  pLits[0] = lit_neg( pLits[0] );
2156  pLits[1] = lit_neg( pLits[1] );
2157  RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
2158  assert( RetValue );
2159  // continue solving the other implication
2160  p->nSatCallsUnsat++;
2161  }
2162  else if ( RetValue1 == l_True )
2163  {
2164 p->timeSatSat += Abc_Clock() - clk;
2165  Ivy_FraigSavePattern( p );
2166  p->nSatCallsSat++;
2167  return 0;
2168  }
2169  else // if ( RetValue1 == l_Undef )
2170  {
2171 p->timeSatFail += Abc_Clock() - clk;
2172 /*
2173  if ( nBTLimit > 1000 )
2174  {
2175  RetValue = Ivy_FraigCheckCone( p, p->pManFraig, pOld, pNew, nBTLimit );
2176  if ( RetValue != -1 )
2177  return RetValue;
2178  }
2179 */
2180  // mark the node as the failed node
2181  if ( pOld != p->pManFraig->pConst1 )
2182  pOld->fFailTfo = 1;
2183  pNew->fFailTfo = 1;
2184  p->nSatFailsReal++;
2185  return -1;
2186  }
2187 
2188  // if the old node was constant 0, we already know the answer
2189  if ( pOld == p->pManFraig->pConst1 )
2190  {
2191  p->nSatProof++;
2192  return 1;
2193  }
2194 
2195  // solve under assumptions
2196  // A = 0; B = 1 OR A = 0; B = 0
2197 clk = Abc_Clock();
2198  pLits[0] = toLitCond( Ivy_ObjSatNum(pOld), 1 );
2199  pLits[1] = toLitCond( Ivy_ObjSatNum(pNew), pOld->fPhase ^ pNew->fPhase );
2200  RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2,
2201  (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0,
2202  p->nBTLimitGlobal, p->nInsLimitGlobal );
2203 p->timeSat += Abc_Clock() - clk;
2204  if ( RetValue1 == l_False )
2205  {
2206 p->timeSatUnsat += Abc_Clock() - clk;
2207  pLits[0] = lit_neg( pLits[0] );
2208  pLits[1] = lit_neg( pLits[1] );
2209  RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
2210  assert( RetValue );
2211  p->nSatCallsUnsat++;
2212  }
2213  else if ( RetValue1 == l_True )
2214  {
2215 p->timeSatSat += Abc_Clock() - clk;
2216  Ivy_FraigSavePattern( p );
2217  p->nSatCallsSat++;
2218  return 0;
2219  }
2220  else // if ( RetValue1 == l_Undef )
2221  {
2222 p->timeSatFail += Abc_Clock() - clk;
2223 /*
2224  if ( nBTLimit > 1000 )
2225  {
2226  RetValue = Ivy_FraigCheckCone( p, p->pManFraig, pOld, pNew, nBTLimit );
2227  if ( RetValue != -1 )
2228  return RetValue;
2229  }
2230 */
2231  // mark the node as the failed node
2232  pOld->fFailTfo = 1;
2233  pNew->fFailTfo = 1;
2234  p->nSatFailsReal++;
2235  return -1;
2236  }
2237 /*
2238  // check BDD proof
2239  {
2240  int RetVal;
2241  ABC_PRT( "Sat", Abc_Clock() - clk2 );
2242  clk2 = Abc_Clock();
2243  RetVal = Ivy_FraigNodesAreEquivBdd( pOld, pNew );
2244 // printf( "%d ", RetVal );
2245  assert( RetVal );
2246  ABC_PRT( "Bdd", Abc_Clock() - clk2 );
2247  printf( "\n" );
2248  }
2249 */
2250  // return SAT proof
2251  p->nSatProof++;
2252  return 1;
2253 }
2254 
2255 /**Function*************************************************************
2256 
2257  Synopsis [Runs equivalence test for one node.]
2258 
2259  Description [Returns the fraiged node.]
2260 
2261  SideEffects []
2262 
2263  SeeAlso []
2264 
2265 ***********************************************************************/
2266 int Ivy_FraigNodeIsConst( Ivy_FraigMan_t * p, Ivy_Obj_t * pNew )
2267 {
2268  int pLits[2], RetValue1;
2269  abctime clk;
2270  int RetValue;
2271 
2272  // make sure the nodes are not complemented
2273  assert( !Ivy_IsComplement(pNew) );
2274  assert( pNew != p->pManFraig->pConst1 );
2275  p->nSatCalls++;
2276 
2277  // make sure the solver is allocated and has enough variables
2278  if ( p->pSat == NULL )
2279  {
2280  p->pSat = sat_solver_new();
2281  sat_solver_setnvars( p->pSat, 1000 );
2282  p->pSat->factors = ABC_CALLOC( double, p->pSat->cap );
2283  p->nSatVars = 1;
2284  // var 0 is reserved for const1 node - add the clause
2285 // pLits[0] = toLit( 0 );
2286 // sat_solver_addclause( p->pSat, pLits, pLits + 1 );
2287  }
2288 
2289  // if the nodes do not have SAT variables, allocate them
2290  Ivy_FraigNodeAddToSolver( p, NULL, pNew );
2291 
2292  // prepare variable activity
2293  Ivy_FraigSetActivityFactors( p, NULL, pNew );
2294 
2295  // solve under assumptions
2296 clk = Abc_Clock();
2297  pLits[0] = toLitCond( Ivy_ObjSatNum(pNew), pNew->fPhase );
2298  RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 1,
2299  (ABC_INT64_T)p->pParams->nBTLimitMiter, (ABC_INT64_T)0,
2300  p->nBTLimitGlobal, p->nInsLimitGlobal );
2301 p->timeSat += Abc_Clock() - clk;
2302  if ( RetValue1 == l_False )
2303  {
2304 p->timeSatUnsat += Abc_Clock() - clk;
2305  pLits[0] = lit_neg( pLits[0] );
2306  RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 1 );
2307  assert( RetValue );
2308  // continue solving the other implication
2309  p->nSatCallsUnsat++;
2310  }
2311  else if ( RetValue1 == l_True )
2312  {
2313 p->timeSatSat += Abc_Clock() - clk;
2314  if ( p->pPatWords )
2315  Ivy_FraigSavePattern( p );
2316  p->nSatCallsSat++;
2317  return 0;
2318  }
2319  else // if ( RetValue1 == l_Undef )
2320  {
2321 p->timeSatFail += Abc_Clock() - clk;
2322 /*
2323  if ( p->pParams->nBTLimitMiter > 1000 )
2324  {
2325  RetValue = Ivy_FraigCheckCone( p, p->pManFraig, p->pManFraig->pConst1, pNew, p->pParams->nBTLimitMiter );
2326  if ( RetValue != -1 )
2327  return RetValue;
2328  }
2329 */
2330  // mark the node as the failed node
2331  pNew->fFailTfo = 1;
2332  p->nSatFailsReal++;
2333  return -1;
2334  }
2335 
2336  // return SAT proof
2337  p->nSatProof++;
2338  return 1;
2339 }
2340 
2341 /**Function*************************************************************
2342 
2343  Synopsis [Addes clauses to the solver.]
2344 
2345  Description []
2346 
2347  SideEffects []
2348 
2349  SeeAlso []
2350 
2351 ***********************************************************************/
2352 void Ivy_FraigAddClausesMux( Ivy_FraigMan_t * p, Ivy_Obj_t * pNode )
2353 {
2354  Ivy_Obj_t * pNodeI, * pNodeT, * pNodeE;
2355  int pLits[4], RetValue, VarF, VarI, VarT, VarE, fCompT, fCompE;
2356 
2357  assert( !Ivy_IsComplement( pNode ) );
2358  assert( Ivy_ObjIsMuxType( pNode ) );
2359  // get nodes (I = if, T = then, E = else)
2360  pNodeI = Ivy_ObjRecognizeMux( pNode, &pNodeT, &pNodeE );
2361  // get the variable numbers
2362  VarF = Ivy_ObjSatNum(pNode);
2363  VarI = Ivy_ObjSatNum(pNodeI);
2364  VarT = Ivy_ObjSatNum(Ivy_Regular(pNodeT));
2365  VarE = Ivy_ObjSatNum(Ivy_Regular(pNodeE));
2366  // get the complementation flags
2367  fCompT = Ivy_IsComplement(pNodeT);
2368  fCompE = Ivy_IsComplement(pNodeE);
2369 
2370  // f = ITE(i, t, e)
2371 
2372  // i' + t' + f
2373  // i' + t + f'
2374  // i + e' + f
2375  // i + e + f'
2376 
2377  // create four clauses
2378  pLits[0] = toLitCond(VarI, 1);
2379  pLits[1] = toLitCond(VarT, 1^fCompT);
2380  pLits[2] = toLitCond(VarF, 0);
2381  RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
2382  assert( RetValue );
2383  pLits[0] = toLitCond(VarI, 1);
2384  pLits[1] = toLitCond(VarT, 0^fCompT);
2385  pLits[2] = toLitCond(VarF, 1);
2386  RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
2387  assert( RetValue );
2388  pLits[0] = toLitCond(VarI, 0);
2389  pLits[1] = toLitCond(VarE, 1^fCompE);
2390  pLits[2] = toLitCond(VarF, 0);
2391  RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
2392  assert( RetValue );
2393  pLits[0] = toLitCond(VarI, 0);
2394  pLits[1] = toLitCond(VarE, 0^fCompE);
2395  pLits[2] = toLitCond(VarF, 1);
2396  RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
2397  assert( RetValue );
2398 
2399  // two additional clauses
2400  // t' & e' -> f'
2401  // t & e -> f
2402 
2403  // t + e + f'
2404  // t' + e' + f
2405 
2406  if ( VarT == VarE )
2407  {
2408 // assert( fCompT == !fCompE );
2409  return;
2410  }
2411 
2412  pLits[0] = toLitCond(VarT, 0^fCompT);
2413  pLits[1] = toLitCond(VarE, 0^fCompE);
2414  pLits[2] = toLitCond(VarF, 1);
2415  RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
2416  assert( RetValue );
2417  pLits[0] = toLitCond(VarT, 1^fCompT);
2418  pLits[1] = toLitCond(VarE, 1^fCompE);
2419  pLits[2] = toLitCond(VarF, 0);
2420  RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
2421  assert( RetValue );
2422 }
2423 
2424 /**Function*************************************************************
2425 
2426  Synopsis [Addes clauses to the solver.]
2427 
2428  Description []
2429 
2430  SideEffects []
2431 
2432  SeeAlso []
2433 
2434 ***********************************************************************/
2435 void Ivy_FraigAddClausesSuper( Ivy_FraigMan_t * p, Ivy_Obj_t * pNode, Vec_Ptr_t * vSuper )
2436 {
2437  Ivy_Obj_t * pFanin;
2438  int * pLits, nLits, RetValue, i;
2439  assert( !Ivy_IsComplement(pNode) );
2440  assert( Ivy_ObjIsNode( pNode ) );
2441  // create storage for literals
2442  nLits = Vec_PtrSize(vSuper) + 1;
2443  pLits = ABC_ALLOC( int, nLits );
2444  // suppose AND-gate is A & B = C
2445  // add !A => !C or A + !C
2446  Vec_PtrForEachEntry( Ivy_Obj_t *, vSuper, pFanin, i )
2447  {
2448  pLits[0] = toLitCond(Ivy_ObjSatNum(Ivy_Regular(pFanin)), Ivy_IsComplement(pFanin));
2449  pLits[1] = toLitCond(Ivy_ObjSatNum(pNode), 1);
2450  RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
2451  assert( RetValue );
2452  }
2453  // add A & B => C or !A + !B + C
2454  Vec_PtrForEachEntry( Ivy_Obj_t *, vSuper, pFanin, i )
2455  pLits[i] = toLitCond(Ivy_ObjSatNum(Ivy_Regular(pFanin)), !Ivy_IsComplement(pFanin));
2456  pLits[nLits-1] = toLitCond(Ivy_ObjSatNum(pNode), 0);
2457  RetValue = sat_solver_addclause( p->pSat, pLits, pLits + nLits );
2458  assert( RetValue );
2459  ABC_FREE( pLits );
2460 }
2461 
2462 /**Function*************************************************************
2463 
2464  Synopsis [Collects the supergate.]
2465 
2466  Description []
2467 
2468  SideEffects []
2469 
2470  SeeAlso []
2471 
2472 ***********************************************************************/
2473 void Ivy_FraigCollectSuper_rec( Ivy_Obj_t * pObj, Vec_Ptr_t * vSuper, int fFirst, int fUseMuxes )
2474 {
2475  // if the new node is complemented or a PI, another gate begins
2476  if ( Ivy_IsComplement(pObj) || Ivy_ObjIsPi(pObj) || (!fFirst && Ivy_ObjRefs(pObj) > 1) ||
2477  (fUseMuxes && Ivy_ObjIsMuxType(pObj)) )
2478  {
2479  Vec_PtrPushUnique( vSuper, pObj );
2480  return;
2481  }
2482  // go through the branches
2483  Ivy_FraigCollectSuper_rec( Ivy_ObjChild0(pObj), vSuper, 0, fUseMuxes );
2484  Ivy_FraigCollectSuper_rec( Ivy_ObjChild1(pObj), vSuper, 0, fUseMuxes );
2485 }
2486 
2487 /**Function*************************************************************
2488 
2489  Synopsis [Collects the supergate.]
2490 
2491  Description []
2492 
2493  SideEffects []
2494 
2495  SeeAlso []
2496 
2497 ***********************************************************************/
2498 Vec_Ptr_t * Ivy_FraigCollectSuper( Ivy_Obj_t * pObj, int fUseMuxes )
2499 {
2500  Vec_Ptr_t * vSuper;
2501  assert( !Ivy_IsComplement(pObj) );
2502  assert( !Ivy_ObjIsPi(pObj) );
2503  vSuper = Vec_PtrAlloc( 4 );
2504  Ivy_FraigCollectSuper_rec( pObj, vSuper, 1, fUseMuxes );
2505  return vSuper;
2506 }
2507 
2508 /**Function*************************************************************
2509 
2510  Synopsis [Updates the solver clause database.]
2511 
2512  Description []
2513 
2514  SideEffects []
2515 
2516  SeeAlso []
2517 
2518 ***********************************************************************/
2519 void Ivy_FraigObjAddToFrontier( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj, Vec_Ptr_t * vFrontier )
2520 {
2521  assert( !Ivy_IsComplement(pObj) );
2522  if ( Ivy_ObjSatNum(pObj) )
2523  return;
2524  assert( Ivy_ObjSatNum(pObj) == 0 );
2525  assert( Ivy_ObjFaninVec(pObj) == NULL );
2526  if ( Ivy_ObjIsConst1(pObj) )
2527  return;
2528 //printf( "Assigning node %d number %d\n", pObj->Id, p->nSatVars );
2529  Ivy_ObjSetSatNum( pObj, p->nSatVars++ );
2530  if ( Ivy_ObjIsNode(pObj) )
2531  Vec_PtrPush( vFrontier, pObj );
2532 }
2533 
2534 /**Function*************************************************************
2535 
2536  Synopsis [Updates the solver clause database.]
2537 
2538  Description []
2539 
2540  SideEffects []
2541 
2542  SeeAlso []
2543 
2544 ***********************************************************************/
2545 void Ivy_FraigNodeAddToSolver( Ivy_FraigMan_t * p, Ivy_Obj_t * pOld, Ivy_Obj_t * pNew )
2546 {
2547  Vec_Ptr_t * vFrontier, * vFanins;
2548  Ivy_Obj_t * pNode, * pFanin;
2549  int i, k, fUseMuxes = 1;
2550  assert( pOld || pNew );
2551  // quit if CNF is ready
2552  if ( (!pOld || Ivy_ObjFaninVec(pOld)) && (!pNew || Ivy_ObjFaninVec(pNew)) )
2553  return;
2554  // start the frontier
2555  vFrontier = Vec_PtrAlloc( 100 );
2556  if ( pOld ) Ivy_FraigObjAddToFrontier( p, pOld, vFrontier );
2557  if ( pNew ) Ivy_FraigObjAddToFrontier( p, pNew, vFrontier );
2558  // explore nodes in the frontier
2559  Vec_PtrForEachEntry( Ivy_Obj_t *, vFrontier, pNode, i )
2560  {
2561  // create the supergate
2562  assert( Ivy_ObjSatNum(pNode) );
2563  assert( Ivy_ObjFaninVec(pNode) == NULL );
2564  if ( fUseMuxes && Ivy_ObjIsMuxType(pNode) )
2565  {
2566  vFanins = Vec_PtrAlloc( 4 );
2567  Vec_PtrPushUnique( vFanins, Ivy_ObjFanin0( Ivy_ObjFanin0(pNode) ) );
2568  Vec_PtrPushUnique( vFanins, Ivy_ObjFanin0( Ivy_ObjFanin1(pNode) ) );
2569  Vec_PtrPushUnique( vFanins, Ivy_ObjFanin1( Ivy_ObjFanin0(pNode) ) );
2570  Vec_PtrPushUnique( vFanins, Ivy_ObjFanin1( Ivy_ObjFanin1(pNode) ) );
2571  Vec_PtrForEachEntry( Ivy_Obj_t *, vFanins, pFanin, k )
2572  Ivy_FraigObjAddToFrontier( p, Ivy_Regular(pFanin), vFrontier );
2573  Ivy_FraigAddClausesMux( p, pNode );
2574  }
2575  else
2576  {
2577  vFanins = Ivy_FraigCollectSuper( pNode, fUseMuxes );
2578  Vec_PtrForEachEntry( Ivy_Obj_t *, vFanins, pFanin, k )
2579  Ivy_FraigObjAddToFrontier( p, Ivy_Regular(pFanin), vFrontier );
2580  Ivy_FraigAddClausesSuper( p, pNode, vFanins );
2581  }
2582  assert( Vec_PtrSize(vFanins) > 1 );
2583  Ivy_ObjSetFaninVec( pNode, vFanins );
2584  }
2585  Vec_PtrFree( vFrontier );
2586  sat_solver_simplify( p->pSat );
2587 }
2588 
2589 /**Function*************************************************************
2590 
2591  Synopsis [Sets variable activities in the cone.]
2592 
2593  Description []
2594 
2595  SideEffects []
2596 
2597  SeeAlso []
2598 
2599 ***********************************************************************/
2600 int Ivy_FraigSetActivityFactors_rec( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj, int LevelMin, int LevelMax )
2601 {
2602  Vec_Ptr_t * vFanins;
2603  Ivy_Obj_t * pFanin;
2604  int i, Counter = 0;
2605  assert( !Ivy_IsComplement(pObj) );
2606  assert( Ivy_ObjSatNum(pObj) );
2607  // skip visited variables
2608  if ( Ivy_ObjIsTravIdCurrent(p->pManFraig, pObj) )
2609  return 0;
2610  Ivy_ObjSetTravIdCurrent(p->pManFraig, pObj);
2611  // add the PI to the list
2612  if ( pObj->Level <= (unsigned)LevelMin || Ivy_ObjIsPi(pObj) )
2613  return 0;
2614  // set the factor of this variable
2615  // (LevelMax-LevelMin) / (pObj->Level-LevelMin) = p->pParams->dActConeBumpMax / ThisBump
2616  p->pSat->factors[Ivy_ObjSatNum(pObj)] = p->pParams->dActConeBumpMax * (pObj->Level - LevelMin)/(LevelMax - LevelMin);
2617  veci_push(&p->pSat->act_vars, Ivy_ObjSatNum(pObj));
2618  // explore the fanins
2619  vFanins = Ivy_ObjFaninVec( pObj );
2620  Vec_PtrForEachEntry( Ivy_Obj_t *, vFanins, pFanin, i )
2621  Counter += Ivy_FraigSetActivityFactors_rec( p, Ivy_Regular(pFanin), LevelMin, LevelMax );
2622  return 1 + Counter;
2623 }
2624 
2625 /**Function*************************************************************
2626 
2627  Synopsis [Sets variable activities in the cone.]
2628 
2629  Description []
2630 
2631  SideEffects []
2632 
2633  SeeAlso []
2634 
2635 ***********************************************************************/
2636 int Ivy_FraigSetActivityFactors( Ivy_FraigMan_t * p, Ivy_Obj_t * pOld, Ivy_Obj_t * pNew )
2637 {
2638  int LevelMin, LevelMax;
2639  abctime clk;
2640  assert( pOld || pNew );
2641 clk = Abc_Clock();
2642  // reset the active variables
2643  veci_resize(&p->pSat->act_vars, 0);
2644  // prepare for traversal
2645  Ivy_ManIncrementTravId( p->pManFraig );
2646  // determine the min and max level to visit
2647  assert( p->pParams->dActConeRatio > 0 && p->pParams->dActConeRatio < 1 );
2648  LevelMax = IVY_MAX( (pNew ? pNew->Level : 0), (pOld ? pOld->Level : 0) );
2649  LevelMin = (int)(LevelMax * (1.0 - p->pParams->dActConeRatio));
2650  // traverse
2651  if ( pOld && !Ivy_ObjIsConst1(pOld) )
2652  Ivy_FraigSetActivityFactors_rec( p, pOld, LevelMin, LevelMax );
2653  if ( pNew && !Ivy_ObjIsConst1(pNew) )
2654  Ivy_FraigSetActivityFactors_rec( p, pNew, LevelMin, LevelMax );
2655 //Ivy_FraigPrintActivity( p );
2656 p->timeTrav += Abc_Clock() - clk;
2657  return 1;
2658 }
2659 
2660 ABC_NAMESPACE_IMPL_END
2661 
2662 #include "bdd/cudd/cuddInt.h"
2663 
2664 ABC_NAMESPACE_IMPL_START
2665 
2666 
2667 /**Function*************************************************************
2668 
2669  Synopsis [Checks equivalence using BDDs.]
2670 
2671  Description []
2672 
2673  SideEffects []
2674 
2675  SeeAlso []
2676 
2677 ***********************************************************************/
2678 DdNode * Ivy_FraigNodesAreEquivBdd_int( DdManager * dd, DdNode * bFunc, Vec_Ptr_t * vFront, int Level )
2679 {
2680  DdNode ** pFuncs;
2681  DdNode * bFuncNew;
2682  Vec_Ptr_t * vTemp;
2683  Ivy_Obj_t * pObj, * pFanin;
2684  int i, NewSize;
2685  // create new frontier
2686  vTemp = Vec_PtrAlloc( 100 );
2687  Vec_PtrForEachEntry( Ivy_Obj_t *, vFront, pObj, i )
2688  {
2689  if ( (int)pObj->Level != Level )
2690  {
2691  pObj->fMarkB = 1;
2692  pObj->TravId = Vec_PtrSize(vTemp);
2693  Vec_PtrPush( vTemp, pObj );
2694  continue;
2695  }
2696 
2697  pFanin = Ivy_ObjFanin0(pObj);
2698  if ( pFanin->fMarkB == 0 )
2699  {
2700  pFanin->fMarkB = 1;
2701  pFanin->TravId = Vec_PtrSize(vTemp);
2702  Vec_PtrPush( vTemp, pFanin );
2703  }
2704 
2705  pFanin = Ivy_ObjFanin1(pObj);
2706  if ( pFanin->fMarkB == 0 )
2707  {
2708  pFanin->fMarkB = 1;
2709  pFanin->TravId = Vec_PtrSize(vTemp);
2710  Vec_PtrPush( vTemp, pFanin );
2711  }
2712  }
2713  // collect the permutation
2714  NewSize = IVY_MAX(dd->size, Vec_PtrSize(vTemp));
2715  pFuncs = ABC_ALLOC( DdNode *, NewSize );
2716  Vec_PtrForEachEntry( Ivy_Obj_t *, vFront, pObj, i )
2717  {
2718  if ( (int)pObj->Level != Level )
2719  pFuncs[i] = Cudd_bddIthVar( dd, pObj->TravId );
2720  else
2721  pFuncs[i] = Cudd_bddAnd( dd,
2722  Cudd_NotCond( Cudd_bddIthVar(dd, Ivy_ObjFanin0(pObj)->TravId), Ivy_ObjFaninC0(pObj) ),
2723  Cudd_NotCond( Cudd_bddIthVar(dd, Ivy_ObjFanin1(pObj)->TravId), Ivy_ObjFaninC1(pObj) ) );
2724  Cudd_Ref( pFuncs[i] );
2725  }
2726  // add the remaining vars
2727  assert( NewSize == dd->size );
2728  for ( i = Vec_PtrSize(vFront); i < dd->size; i++ )
2729  {
2730  pFuncs[i] = Cudd_bddIthVar( dd, i );
2731  Cudd_Ref( pFuncs[i] );
2732  }
2733 
2734  // create new
2735  bFuncNew = Cudd_bddVectorCompose( dd, bFunc, pFuncs ); Cudd_Ref( bFuncNew );
2736  // clean trav Id
2737  Vec_PtrForEachEntry( Ivy_Obj_t *, vTemp, pObj, i )
2738  {
2739  pObj->fMarkB = 0;
2740  pObj->TravId = 0;
2741  }
2742  // deref
2743  for ( i = 0; i < dd->size; i++ )
2744  Cudd_RecursiveDeref( dd, pFuncs[i] );
2745  ABC_FREE( pFuncs );
2746 
2747  ABC_FREE( vFront->pArray );
2748  *vFront = *vTemp;
2749 
2750  vTemp->nCap = vTemp->nSize = 0;
2751  vTemp->pArray = NULL;
2752  Vec_PtrFree( vTemp );
2753 
2754  Cudd_Deref( bFuncNew );
2755  return bFuncNew;
2756 }
2757 
2758 /**Function*************************************************************
2759 
2760  Synopsis [Checks equivalence using BDDs.]
2761 
2762  Description []
2763 
2764  SideEffects []
2765 
2766  SeeAlso []
2767 
2768 ***********************************************************************/
2769 int Ivy_FraigNodesAreEquivBdd( Ivy_Obj_t * pObj1, Ivy_Obj_t * pObj2 )
2770 {
2771  static DdManager * dd = NULL;
2772  DdNode * bFunc, * bTemp;
2773  Vec_Ptr_t * vFront;
2774  Ivy_Obj_t * pObj;
2775  int i, RetValue, Iter, Level;
2776  // start the manager
2777  if ( dd == NULL )
2778  dd = Cudd_Init( 50, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
2779  // create front
2780  vFront = Vec_PtrAlloc( 100 );
2781  Vec_PtrPush( vFront, pObj1 );
2782  Vec_PtrPush( vFront, pObj2 );
2783  // get the function
2784  bFunc = Cudd_bddXor( dd, Cudd_bddIthVar(dd,0), Cudd_bddIthVar(dd,1) ); Cudd_Ref( bFunc );
2785  bFunc = Cudd_NotCond( bFunc, pObj1->fPhase != pObj2->fPhase );
2786  // try running BDDs
2787  for ( Iter = 0; ; Iter++ )
2788  {
2789  // find max level
2790  Level = 0;
2791  Vec_PtrForEachEntry( Ivy_Obj_t *, vFront, pObj, i )
2792  if ( Level < (int)pObj->Level )
2793  Level = (int)pObj->Level;
2794  if ( Level == 0 )
2795  break;
2796  bFunc = Ivy_FraigNodesAreEquivBdd_int( dd, bTemp = bFunc, vFront, Level ); Cudd_Ref( bFunc );
2797  Cudd_RecursiveDeref( dd, bTemp );
2798  if ( bFunc == Cudd_ReadLogicZero(dd) ) // proved
2799  {printf( "%d", Iter ); break;}
2800  if ( Cudd_DagSize(bFunc) > 1000 )
2801  {printf( "b" ); break;}
2802  if ( dd->size > 120 )
2803  {printf( "s" ); break;}
2804  if ( Iter > 50 )
2805  {printf( "i" ); break;}
2806  }
2807  if ( bFunc == Cudd_ReadLogicZero(dd) ) // unsat
2808  RetValue = 1;
2809  else if ( Level == 0 ) // sat
2810  RetValue = 0;
2811  else
2812  RetValue = -1; // spaceout/timeout
2813  Cudd_RecursiveDeref( dd, bFunc );
2814  Vec_PtrFree( vFront );
2815  return RetValue;
2816 }
2817 
2818 ABC_NAMESPACE_IMPL_END
2819 
2820 #include "aig/aig/aig.h"
2821 
2822 ABC_NAMESPACE_IMPL_START
2823 
2824 
2825 /**Function*************************************************************
2826 
2827  Synopsis [Computes truth table of the cut.]
2828 
2829  Description []
2830 
2831  SideEffects []
2832 
2833  SeeAlso []
2834 
2835 ***********************************************************************/
2836 void Ivy_FraigExtractCone_rec( Ivy_Man_t * p, Ivy_Obj_t * pNode, Vec_Int_t * vLeaves, Vec_Int_t * vNodes )
2837 {
2838  if ( pNode->fMarkB )
2839  return;
2840  pNode->fMarkB = 1;
2841  if ( Ivy_ObjIsPi(pNode) )
2842  {
2843  Vec_IntPush( vLeaves, pNode->Id );
2844  return;
2845  }
2846  assert( Ivy_ObjIsAnd(pNode) );
2847  Ivy_FraigExtractCone_rec( p, Ivy_ObjFanin0(pNode), vLeaves, vNodes );
2848  Ivy_FraigExtractCone_rec( p, Ivy_ObjFanin1(pNode), vLeaves, vNodes );
2849  Vec_IntPush( vNodes, pNode->Id );
2850 }
2851 
2852 /**Function*************************************************************
2853 
2854  Synopsis [Checks equivalence using BDDs.]
2855 
2856  Description []
2857 
2858  SideEffects []
2859 
2860  SeeAlso []
2861 
2862 ***********************************************************************/
2863 Aig_Man_t * Ivy_FraigExtractCone( Ivy_Man_t * p, Ivy_Obj_t * pObj1, Ivy_Obj_t * pObj2, Vec_Int_t * vLeaves )
2864 {
2865  Aig_Man_t * pMan;
2866  Aig_Obj_t * pMiter;
2867  Vec_Int_t * vNodes;
2868  Ivy_Obj_t * pObjIvy;
2869  int i;
2870  // collect nodes
2871  vNodes = Vec_IntAlloc( 100 );
2872  Ivy_ManConst1(p)->fMarkB = 1;
2873  Ivy_FraigExtractCone_rec( p, pObj1, vLeaves, vNodes );
2874  Ivy_FraigExtractCone_rec( p, pObj2, vLeaves, vNodes );
2875  Ivy_ManConst1(p)->fMarkB = 0;
2876  // create new manager
2877  pMan = Aig_ManStart( 1000 );
2878  Ivy_ManConst1(p)->pEquiv = (Ivy_Obj_t *)Aig_ManConst1(pMan);
2879  Ivy_ManForEachNodeVec( p, vLeaves, pObjIvy, i )
2880  {
2881  pObjIvy->pEquiv = (Ivy_Obj_t *)Aig_ObjCreateCi( pMan );
2882  pObjIvy->fMarkB = 0;
2883  }
2884  // duplicate internal nodes
2885  Ivy_ManForEachNodeVec( p, vNodes, pObjIvy, i )
2886  {
2887 
2888  pObjIvy->pEquiv = (Ivy_Obj_t *)Aig_And( pMan, (Aig_Obj_t *)Ivy_ObjChild0Equiv(pObjIvy), (Aig_Obj_t *)Ivy_ObjChild1Equiv(pObjIvy) );
2889  pObjIvy->fMarkB = 0;
2890 
2891  pMiter = (Aig_Obj_t *)pObjIvy->pEquiv;
2892  assert( pMiter->fPhase == pObjIvy->fPhase );
2893  }
2894  // create the PO
2895  pMiter = Aig_Exor( pMan, (Aig_Obj_t *)pObj1->pEquiv, (Aig_Obj_t *)pObj2->pEquiv );
2896  pMiter = Aig_NotCond( pMiter, Aig_Regular(pMiter)->fPhase ^ Aig_IsComplement(pMiter) );
2897 
2898 /*
2899 printf( "Polarity = %d\n", pMiter->fPhase );
2900  if ( Ivy_ObjIsConst1(pObj1) || Ivy_ObjIsConst1(pObj2) )
2901  {
2902  pMiter = Aig_NotCond( pMiter, 1 );
2903 printf( "***************\n" );
2904  }
2905 */
2906  pMiter = Aig_ObjCreateCo( pMan, pMiter );
2907 //printf( "Polarity = %d\n", pMiter->fPhase );
2908  Aig_ManCleanup( pMan );
2909  Vec_IntFree( vNodes );
2910  return pMan;
2911 }
2912 
2913 /**Function*************************************************************
2914 
2915  Synopsis [Checks equivalence using BDDs.]
2916 
2917  Description []
2918 
2919  SideEffects []
2920 
2921  SeeAlso []
2922 
2923 ***********************************************************************/
2924 int Ivy_FraigCheckCone( Ivy_FraigMan_t * pGlo, Ivy_Man_t * p, Ivy_Obj_t * pObj1, Ivy_Obj_t * pObj2, int nConfLimit )
2925 {
2926  extern 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 );
2927  Vec_Int_t * vLeaves;
2928  Aig_Man_t * pMan;
2929  Aig_Obj_t * pObj;
2930  int i, RetValue;
2931  vLeaves = Vec_IntAlloc( 100 );
2932  pMan = Ivy_FraigExtractCone( p, pObj1, pObj2, vLeaves );
2933  RetValue = Fra_FraigSat( pMan, nConfLimit, 0, 0, 0, 0, 0, 0, 0, 1 );
2934  if ( RetValue == 0 )
2935  {
2936  int Counter = 0;
2937  memset( pGlo->pPatWords, 0, sizeof(unsigned) * pGlo->nPatWords );
2938  Aig_ManForEachCi( pMan, pObj, i )
2939  if ( ((int *)pMan->pData)[i] )
2940  {
2941  int iObjIvy = Vec_IntEntry( vLeaves, i );
2942  assert( iObjIvy > 0 && iObjIvy <= Ivy_ManPiNum(p) );
2943  Ivy_InfoSetBit( pGlo->pPatWords, iObjIvy-1 );
2944 //printf( "%d ", iObjIvy );
2945 Counter++;
2946  }
2947  assert( Counter > 0 );
2948  }
2949  Vec_IntFree( vLeaves );
2950  if ( RetValue == 1 )
2951  printf( "UNSAT\n" );
2952  else if ( RetValue == 0 )
2953  printf( "SAT\n" );
2954  else if ( RetValue == -1 )
2955  printf( "UNDEC\n" );
2956 
2957 // p->pModel = (int *)pMan->pData, pMan2->pData = NULL;
2958  Aig_ManStop( pMan );
2959  return RetValue;
2960 }
2961 
2962 ////////////////////////////////////////////////////////////////////////
2963 /// END OF FILE ///
2964 ////////////////////////////////////////////////////////////////////////
2965 
2966 
2967 ABC_NAMESPACE_IMPL_END
2968 
Ivy_Obj_t_::TravId
int TravId
Definition: ivy.h:76
memset
char * memset()
Aig_ObjCreateCo
Aig_Obj_t * Aig_ObjCreateCo(Aig_Man_t *p, Aig_Obj_t *pDriver)
Definition: aigObj.c:66
Ivy_FraigObjAddToFrontier
void Ivy_FraigObjAddToFrontier(Ivy_FraigMan_t *p, Ivy_Obj_t *pObj, Vec_Ptr_t *vFrontier)
Definition: ivyFraig.c:2519
Ivy_IsComplement
static int Ivy_IsComplement(Ivy_Obj_t *p)
Definition: ivy.h:196
Ivy_ObjSetEquivListPrev
static void Ivy_ObjSetEquivListPrev(Ivy_Obj_t *pObj, Ivy_Obj_t *pPrev)
Definition: ivyFraig.c:157
Ivy_Obj_t_::Level
unsigned Level
Definition: ivy.h:84
Ivy_FraigMan_t_::nClassesZero
int nClassesZero
Definition: ivyFraig.c:84
Prove_ParamsStruct_t_::nMiteringLimitStart
int nMiteringLimitStart
Definition: ivyFraig.c:119
IVY_MAX
#define IVY_MAX(a, b)
Definition: ivy.h:183
Ivy_BitWordNum
static int Ivy_BitWordNum(int nBits)
Definition: ivy.h:187
Ivy_ObjSetClassNodeLast
static void Ivy_ObjSetClassNodeLast(Ivy_Obj_t *pObj, Ivy_Obj_t *pLast)
Definition: ivyFraig.c:152
Ivy_FraigForEachEquivClassSafe
#define Ivy_FraigForEachEquivClassSafe(pList, pEnt, pEnt2)
Definition: ivyFraig.c:169
Ivy_ObjSetNodeHashNext
static void Ivy_ObjSetNodeHashNext(Ivy_Obj_t *pObj, Ivy_Obj_t *pNext)
Definition: ivyFraig.c:155
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
Ivy_NodeComplementSim
void Ivy_NodeComplementSim(Ivy_FraigMan_t *p, Ivy_Obj_t *pObj)
Definition: ivyFraig.c:790
Ivy_FraigSim_t_::pNext
Ivy_FraigSim_t * pNext
Definition: ivyFraig.c:47
Ivy_FraigRefineClass_rec
int Ivy_FraigRefineClass_rec(Ivy_FraigMan_t *p, Ivy_Obj_t *pClass)
Definition: ivyFraig.c:1244
Ivy_FraigMan_t_::nSimRounds
int nSimRounds
Definition: ivyFraig.c:82
Ivy_FraigMan_t_::pManFraig
Ivy_Man_t * pManFraig
Definition: ivyFraig.c:62
Ivy_FraigMan_t_::nInsLimitGlobal
ABC_INT64_T nInsLimitGlobal
Definition: ivyFraig.c:59
Ivy_FraigList_t_::nItems
int nItems
Definition: ivyFraig.c:41
Ivy_InfoHasBit
static int Ivy_InfoHasBit(unsigned *p, int i)
Definition: ivy.h:189
CUDD_UNIQUE_SLOTS
#define CUDD_UNIQUE_SLOTS
Definition: cudd.h:97
Ivy_FraigMan_t_::time1
abctime time1
Definition: ivyFraig.c:104
Ivy_FraigMan_t_::pSimStart
Ivy_FraigSim_t * pSimStart
Definition: ivyFraig.c:66
Ivy_ManConst1
static Ivy_Obj_t * Ivy_ManConst1(Ivy_Man_t *p)
Definition: ivy.h:199
Cudd_RecursiveDeref
void Cudd_RecursiveDeref(DdManager *table, DdNode *n)
Definition: cuddRef.c:154
Ivy_FraigParams_t_::fVerbose
int fVerbose
Definition: ivy.h:141
s_nInsLimitGlobal
static ABC_INT64_T s_nInsLimitGlobal
Definition: ivyFraig.c:208
DdNode
Definition: cudd.h:278
Prove_ParamsStruct_t_::fUseFraiging
int fUseFraiging
Definition: ivyFraig.c:112
Ivy_ManPi
static Ivy_Obj_t * Ivy_ManPi(Ivy_Man_t *p, int i)
Definition: ivy.h:201
Ivy_FraigList_t_::pHead
Ivy_Obj_t * pHead
Definition: ivyFraig.c:39
Ivy_Obj_t_::pPrevFan0
Ivy_Obj_t * pPrevFan0
Definition: ivy.h:91
Ivy_FraigParams_t_::dActConeRatio
double dActConeRatio
Definition: ivy.h:138
Aig_Man_t
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition: aig.h:50
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Ivy_FraigRefineClasses
int Ivy_FraigRefineClasses(Ivy_FraigMan_t *p)
Definition: ivyFraig.c:1387
sat_solver_addclause
int sat_solver_addclause(sat_solver *s, lit *begin, lit *end)
Definition: satSolver.c:1492
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
Ivy_ManForEachPi
#define Ivy_ManForEachPi(p, pObj, i)
ITERATORS ///.
Definition: ivy.h:387
Aig_ManStop
void Aig_ManStop(Aig_Man_t *p)
Definition: aigMan.c:187
Vec_PtrPushUnique
static int Vec_PtrPushUnique(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:656
Ivy_FraigCheckOutputSims
int Ivy_FraigCheckOutputSims(Ivy_FraigMan_t *p)
Definition: ivyFraig.c:1349
Ivy_FraigSim_t_::pFanin1
Ivy_FraigSim_t * pFanin1
Definition: ivyFraig.c:49
Ivy_FraigMan_t_::nSatFailsReal
int nSatFailsReal
Definition: ivyFraig.c:94
Ivy_FraigMan_t_::nPairsEnd
int nPairsEnd
Definition: ivyFraig.c:88
Ivy_FraigForEachBinNode
#define Ivy_FraigForEachBinNode(pBin, pEnt)
Definition: ivyFraig.c:181
Ivy_FraigMan_t_::pManAig
Ivy_Man_t * pManAig
Definition: ivyFraig.c:61
Ivy_FraigMan_t_::timeTrav
abctime timeTrav
Definition: ivyFraig.c:97
Prove_ParamsStruct_t_::nMiteringLimitMulti
float nMiteringLimitMulti
Definition: ivyFraig.c:120
Ivy_FraigMan_t_::nClassesBeg
int nClassesBeg
Definition: ivyFraig.c:85
Cudd_Deref
void Cudd_Deref(DdNode *node)
Definition: cuddRef.c:438
DdManager::size
int size
Definition: cuddInt.h:361
Ivy_ObjIsMuxType
int Ivy_ObjIsMuxType(Ivy_Obj_t *pObj)
Definition: ivyUtil.c:479
sat_solver_solve
int sat_solver_solve(sat_solver *s, lit *begin, lit *end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal)
Definition: satSolver.c:1700
Ivy_FraigMan_t_::nNodesMiter
int nNodesMiter
Definition: ivyFraig.c:83
Aig_Exor
Aig_Obj_t * Aig_Exor(Aig_Man_t *p, Aig_Obj_t *p0, Aig_Obj_t *p1)
Definition: aigOper.c:220
Ivy_FraigNodeIsConst
static int Ivy_FraigNodeIsConst(Ivy_FraigMan_t *p, Ivy_Obj_t *pObj)
Definition: ivyFraig.c:2266
Ivy_FraigCheckCone
static int Ivy_FraigCheckCone(Ivy_FraigMan_t *pGlo, Ivy_Man_t *p, Ivy_Obj_t *pObj1, Ivy_Obj_t *pObj2, int nConfLimit)
Definition: ivyFraig.c:2924
Ivy_FraigMan_t_::nSatCallsUnsat
int nSatCallsUnsat
Definition: ivyFraig.c:91
Cudd_ReadLogicZero
DdNode * Cudd_ReadLogicZero(DdManager *dd)
Definition: cuddAPI.c:1058
veci_push
static void veci_push(veci *v, int e)
Definition: satVec.h:53
Ivy_ObjIsPi
static int Ivy_ObjIsPi(Ivy_Obj_t *pObj)
Definition: ivy.h:236
Ivy_FraigList_t_
Definition: ivyFraig.c:37
sat_solver_delete
void sat_solver_delete(sat_solver *s)
Definition: satSolver.c:1141
Ivy_NodeSimulateSim
void Ivy_NodeSimulateSim(Ivy_FraigMan_t *p, Ivy_FraigSim_t *pSims)
Definition: ivyFraig.c:833
Aig_ManStart
Aig_Man_t * Aig_ManStart(int nNodesMax)
DECLARATIONS ///.
Definition: aigMan.c:47
Ivy_ManForEachPo
#define Ivy_ManForEachPo(p, pObj, i)
Definition: ivy.h:390
Ivy_FraigMiterProve
static void Ivy_FraigMiterProve(Ivy_FraigMan_t *p)
Definition: ivyFraig.c:1880
Ivy_NodeAssignRandom
void Ivy_NodeAssignRandom(Ivy_FraigMan_t *p, Ivy_Obj_t *pObj)
Definition: ivyFraig.c:680
Ivy_FraigPrintActivity
void Ivy_FraigPrintActivity(Ivy_FraigMan_t *p)
Definition: ivyFraig.c:2080
Aig_IsComplement
static int Aig_IsComplement(Aig_Obj_t *p)
Definition: aig.h:249
Ivy_FraigSim_t_::Type
int Type
Definition: ivyFraig.c:46
Aig_ManForEachCi
#define Aig_ManForEachCi(p, pObj, i)
ITERATORS ///.
Definition: aig.h:393
Prove_ParamsStruct_t_::fUseRewriting
int fUseRewriting
Definition: ivyFraig.c:113
Ivy_FraigProve
int Ivy_FraigProve(Ivy_Man_t **ppManAig, void *pPars)
Definition: ivyFraig.c:255
Ivy_FraigMan_t_::timeSatUnsat
abctime timeSatUnsat
Definition: ivyFraig.c:99
Ivy_FraigParams_t_::nBTLimitNode
int nBTLimitNode
Definition: ivy.h:143
Aig_Regular
static Aig_Obj_t * Aig_Regular(Aig_Obj_t *p)
Definition: aig.h:246
CUDD_CACHE_SLOTS
#define CUDD_CACHE_SLOTS
Definition: cudd.h:98
Aig_ObjCreateCi
Aig_Obj_t * Aig_ObjCreateCi(Aig_Man_t *p)
DECLARATIONS ///.
Definition: aigObj.c:45
Ivy_FraigParams_t_::dActConeBumpMax
double dActConeBumpMax
Definition: ivy.h:139
Vec_PtrPush
static void Vec_PtrPush(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:606
Ivy_FraigPrint
static void Ivy_FraigPrint(Ivy_FraigMan_t *p)
Definition: ivyFraig.c:644
Ivy_ManLatchNum
static int Ivy_ManLatchNum(Ivy_Man_t *p)
Definition: ivy.h:221
l_True
#define l_True
Definition: SolverTypes.h:84
Ivy_Obj_t_::pFanout
Ivy_Obj_t * pFanout
Definition: ivy.h:88
Ivy_Obj_t_::Id
int Id
Definition: ivy.h:75
Ivy_ObjSetSatNum
static void Ivy_ObjSetSatNum(Ivy_Obj_t *pObj, int Num)
Definition: ivyFraig.c:159
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
Ivy_ManDup
Ivy_Man_t * Ivy_ManDup(Ivy_Man_t *p)
Definition: ivyMan.c:110
Prove_ParamsStruct_t_::fUseBdds
int fUseBdds
Definition: ivyFraig.c:114
Ivy_NodeHash
unsigned Ivy_NodeHash(Ivy_FraigMan_t *p, Ivy_Obj_t *pObj)
Definition: ivyFraig.c:951
Ivy_ManForEachNode
#define Ivy_ManForEachNode(p, pObj, i)
Definition: ivy.h:402
Ivy_ObjSatNum
static int Ivy_ObjSatNum(Ivy_Obj_t *pObj)
Definition: ivyFraig.c:148
Ivy_ManPoNum
static int Ivy_ManPoNum(Ivy_Man_t *p)
Definition: ivy.h:219
veci_resize
static void veci_resize(veci *v, int k)
Definition: satVec.h:47
Ivy_NodeAssignConst
void Ivy_NodeAssignConst(Ivy_FraigMan_t *p, Ivy_Obj_t *pObj, int fConst1)
Definition: ivyFraig.c:701
Abc_Clock
static abctime Abc_Clock()
Definition: abc_global.h:279
Ivy_FraigSavePattern0
void Ivy_FraigSavePattern0(Ivy_FraigMan_t *p)
Definition: ivyFraig.c:1488
Vec_PtrSize
static int Vec_PtrSize(Vec_Ptr_t *p)
Definition: vecPtr.h:295
Ivy_FraigMan_t_::nPairs
int nPairs
Definition: ivyFraig.c:74
Ivy_NodeHasZeroSim
int Ivy_NodeHasZeroSim(Ivy_FraigMan_t *p, Ivy_Obj_t *pObj)
Definition: ivyFraig.c:768
Ivy_FraigMan_t_::nSatProof
int nSatProof
Definition: ivyFraig.c:92
Ivy_ManStop
void Ivy_ManStop(Ivy_Man_t *p)
Definition: ivyMan.c:238
Ivy_FraigCreateClasses
void Ivy_FraigCreateClasses(Ivy_FraigMan_t *p)
Definition: ivyFraig.c:1174
Ivy_Obj_t_::pNextFan0
Ivy_Obj_t * pNextFan0
Definition: ivy.h:89
Ivy_FraigNodesAreEquiv
static int Ivy_FraigNodesAreEquiv(Ivy_FraigMan_t *p, Ivy_Obj_t *pObj0, Ivy_Obj_t *pObj1)
Definition: ivyFraig.c:2099
Ivy_ObjRecognizeMux
Ivy_Obj_t * Ivy_ObjRecognizeMux(Ivy_Obj_t *pObj, Ivy_Obj_t **ppObjT, Ivy_Obj_t **ppObjE)
Definition: ivyUtil.c:517
Ivy_ObjFanin1
static Ivy_Obj_t * Ivy_ObjFanin1(Ivy_Obj_t *pObj)
Definition: ivy.h:272
sat_solver_var_value
static int sat_solver_var_value(sat_solver *s, int v)
Definition: satSolver.h:200
Ivy_ObjChild1Equiv
static Ivy_Obj_t * Ivy_ObjChild1Equiv(Ivy_Obj_t *pObj)
Definition: ivy.h:276
Ivy_FraigMan_t_
Definition: ivyFraig.c:53
Ivy_FraigStart
static Ivy_FraigMan_t * Ivy_FraigStart(Ivy_Man_t *pManAig, Ivy_FraigParams_t *pParams)
Definition: ivyFraig.c:554
Aig_And
Aig_Obj_t * Aig_And(Aig_Man_t *p, Aig_Obj_t *p0, Aig_Obj_t *p1)
Definition: aigOper.c:104
Ivy_FraigSetActivityFactors
static int Ivy_FraigSetActivityFactors(Ivy_FraigMan_t *p, Ivy_Obj_t *pOld, Ivy_Obj_t *pNew)
Definition: ivyFraig.c:2636
Cudd_bddVectorCompose
DdNode * Cudd_bddVectorCompose(DdManager *dd, DdNode *f, DdNode **vector)
Definition: cuddCompose.c:791
Ivy_FraigMan_t_::vPiVars
Vec_Ptr_t * vPiVars
Definition: ivyFraig.c:78
Ivy_FraigNodeAddToSolver
static void Ivy_FraigNodeAddToSolver(Ivy_FraigMan_t *p, Ivy_Obj_t *pObj0, Ivy_Obj_t *pObj1)
Definition: ivyFraig.c:2545
Ivy_Obj_t_::pNextFan1
Ivy_Obj_t * pNextFan1
Definition: ivy.h:90
Ivy_FraigParams_t_::nSimWords
int nSimWords
Definition: ivy.h:134
Ivy_FraigMan_t_::lClasses
Ivy_FraigList_t lClasses
Definition: ivyFraig.c:72
s_nBTLimitGlobal
static ABC_INT64_T s_nBTLimitGlobal
Definition: ivyFraig.c:207
IVY_MIN
#define IVY_MIN(a, b)
MACRO DEFINITIONS ///.
Definition: ivy.h:182
lit_neg
static lit lit_neg(lit l)
Definition: satVec.h:144
Ivy_ObjFaninVec
static Vec_Ptr_t * Ivy_ObjFaninVec(Ivy_Obj_t *pObj)
Definition: ivyFraig.c:149
Ivy_FraigMan_t
typedefABC_NAMESPACE_IMPL_START struct Ivy_FraigMan_t_ Ivy_FraigMan_t
DECLARATIONS ///.
Definition: ivyFraig.c:33
Ivy_FraigSimulateOne
void Ivy_FraigSimulateOne(Ivy_FraigMan_t *p)
Definition: ivyFraig.c:990
Ivy_ObjFanin0
static Ivy_Obj_t * Ivy_ObjFanin0(Ivy_Obj_t *pObj)
Definition: ivy.h:271
Ivy_FraigParams_t_::fProve
int fProve
Definition: ivy.h:140
Prove_ParamsStruct_t_::nTotalInspectsMade
ABC_INT64_T nTotalInspectsMade
Definition: ivyFraig.c:137
Ivy_FraigSelectBestPat
int Ivy_FraigSelectBestPat(Ivy_FraigMan_t *p)
Definition: ivyFraig.c:1713
Ivy_ManLevels
int Ivy_ManLevels(Ivy_Man_t *p)
Definition: ivyUtil.c:249
Ivy_FraigMan_t_::nPatWords
int nPatWords
Definition: ivyFraig.c:68
Ivy_FraigParams_t_::fDoSparse
int fDoSparse
Definition: ivy.h:142
Ivy_FraigRemoveClass
void Ivy_FraigRemoveClass(Ivy_FraigList_t *pList, Ivy_Obj_t *pClass)
Definition: ivyFraig.c:1120
Ivy_FraigAddClass
void Ivy_FraigAddClass(Ivy_FraigList_t *pList, Ivy_Obj_t *pClass)
Definition: ivyFraig.c:1067
Prove_ParamsStruct_t_::nMiteringLimitLast
int nMiteringLimitLast
Definition: ivyFraig.c:131
Prove_ParamsStruct_t_::nTotalBacktracksMade
ABC_INT64_T nTotalBacktracksMade
Definition: ivyFraig.c:136
Ivy_ObjRandomSim
static unsigned Ivy_ObjRandomSim()
Definition: ivyFraig.c:162
Ivy_ObjSetEquivListNext
static void Ivy_ObjSetEquivListNext(Ivy_Obj_t *pObj, Ivy_Obj_t *pNext)
Definition: ivyFraig.c:156
Ivy_FraigCountClassNodes
int Ivy_FraigCountClassNodes(Ivy_Obj_t *pClass)
Definition: ivyFraig.c:1446
ProgressBarStruct
DECLARATIONS ///.
Definition: extraUtilProgress.c:32
Ivy_ObjCreatePo
Ivy_Obj_t * Ivy_ObjCreatePo(Ivy_Man_t *p, Ivy_Obj_t *pDriver)
Definition: ivyObj.c:61
Ivy_FraigMan_t_::nSatCalls
int nSatCalls
Definition: ivyFraig.c:89
Ivy_FraigPrintClass
void Ivy_FraigPrintClass(Ivy_Obj_t *pClass)
Definition: ivyFraig.c:1426
Ivy_ManIncrementTravId
void Ivy_ManIncrementTravId(Ivy_Man_t *p)
DECLARATIONS ///.
Definition: ivyUtil.c:45
Ivy_FraigAddClausesMux
void Ivy_FraigAddClausesMux(Ivy_FraigMan_t *p, Ivy_Obj_t *pNode)
Definition: ivyFraig.c:2352
Vec_IntAlloc
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
Ivy_FraigStop
static void Ivy_FraigStop(Ivy_FraigMan_t *p)
Definition: ivyFraig.c:621
Ivy_FraigParamsDefault
void Ivy_FraigParamsDefault(Ivy_FraigParams_t *pParams)
FUNCTION DEFINITIONS ///.
Definition: ivyFraig.c:225
Ivy_FraigMiter
Ivy_Man_t * Ivy_FraigMiter(Ivy_Man_t *pManAig, Ivy_FraigParams_t *pParams)
Definition: ivyFraig.c:480
Ivy_FraigCollectSuper_rec
void Ivy_FraigCollectSuper_rec(Ivy_Obj_t *pObj, Vec_Ptr_t *vSuper, int fFirst, int fUseMuxes)
Definition: ivyFraig.c:2473
Ivy_NodeAddToClass
void Ivy_NodeAddToClass(Ivy_Obj_t *pClass, Ivy_Obj_t *pObj)
Definition: ivyFraig.c:1045
Ivy_FraigSavePattern3
void Ivy_FraigSavePattern3(Ivy_FraigMan_t *p)
Definition: ivyFraig.c:1591
Ivy_ObjSetFraig
static void Ivy_ObjSetFraig(Ivy_Obj_t *pObj, Ivy_Obj_t *pNode)
Definition: ivyFraig.c:158
Ivy_ObjFaninC1
static int Ivy_ObjFaninC1(Ivy_Obj_t *pObj)
Definition: ivy.h:270
Ivy_ObjChild0Equiv
static Ivy_Obj_t * Ivy_ObjChild0Equiv(Ivy_Obj_t *pObj)
Definition: ivy.h:275
Prove_ParamsStruct_t_::fBddReorder
int fBddReorder
Definition: ivyFraig.c:129
Ivy_FraigMan_t_::nSatFails
int nSatFails
Definition: ivyFraig.c:93
Ivy_FraigSavePattern1
void Ivy_FraigSavePattern1(Ivy_FraigMan_t *p)
Definition: ivyFraig.c:1504
Ivy_FraigMan_t_::timeRef
abctime timeRef
Definition: ivyFraig.c:102
Ivy_FraigExtractCone_rec
ABC_NAMESPACE_IMPL_END ABC_NAMESPACE_IMPL_START void Ivy_FraigExtractCone_rec(Ivy_Man_t *p, Ivy_Obj_t *pNode, Vec_Int_t *vLeaves, Vec_Int_t *vNodes)
Definition: ivyFraig.c:2836
Ivy_Obj_t_::fPhase
unsigned fPhase
Definition: ivy.h:81
toLitCond
static lit toLitCond(int v, int c)
Definition: satVec.h:143
sat_solver_setnvars
void sat_solver_setnvars(sat_solver *s, int n)
Definition: satSolver.c:1072
Ivy_FraigSavePattern2
void Ivy_FraigSavePattern2(Ivy_FraigMan_t *p)
Definition: ivyFraig.c:1567
Vec_IntEntry
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
Ivy_ObjRefs
static int Ivy_ObjRefs(Ivy_Obj_t *pObj)
Definition: ivy.h:264
Prove_ParamsStruct_t_::nRewritingLimitStart
int nRewritingLimitStart
Definition: ivyFraig.c:122
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
Cudd_Init
DdManager * Cudd_Init(unsigned int numVars, unsigned int numVarsZ, unsigned int numSlots, unsigned int cacheSize, unsigned long maxMemory)
Definition: cuddInit.c:125
Ivy_FraigAddToPatScores
static void Ivy_FraigAddToPatScores(Ivy_FraigMan_t *p, Ivy_Obj_t *pClass, Ivy_Obj_t *pClassNew)
Definition: ivyFraig.c:1682
Ivy_FraigCheckOutputSimsSavePattern
void Ivy_FraigCheckOutputSimsSavePattern(Ivy_FraigMan_t *p, Ivy_Obj_t *pObj)
Definition: ivyFraig.c:1307
Ivy_FraigParams_t_::MaxScore
int MaxScore
Definition: ivy.h:137
if
if(last==0)
Definition: sparse_int.h:34
Ivy_FraigMiterStatus
static int Ivy_FraigMiterStatus(Ivy_Man_t *pMan)
Definition: ivyFraig.c:1815
Prove_ParamsStruct_t_::nFraigingLimitStart
int nFraigingLimitStart
Definition: ivyFraig.c:125
Ivy_Obj_t_
Definition: ivy.h:73
Prove_ParamsStruct_t_::nTotalInspectLimit
ABC_INT64_T nTotalInspectLimit
Definition: ivyFraig.c:134
Ivy_Regular
static Ivy_Obj_t * Ivy_Regular(Ivy_Obj_t *p)
Definition: ivy.h:193
Ivy_ObjClassNodeRepr
static Ivy_Obj_t * Ivy_ObjClassNodeRepr(Ivy_Obj_t *pObj)
Definition: ivyFraig.c:142
Aig_Obj_t_
Definition: aig.h:69
Vec_IntPush
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
Ivy_FraigResimulate
void Ivy_FraigResimulate(Ivy_FraigMan_t *p)
Definition: ivyFraig.c:1752
Ivy_ObjSetSim
static void Ivy_ObjSetSim(Ivy_Obj_t *pObj, Ivy_FraigSim_t *pSim)
Definition: ivyFraig.c:151
Ivy_FraigMan_t_::pPatWords
unsigned * pPatWords
Definition: ivyFraig.c:69
Counter
static int Counter
Definition: extraBddMisc.c:1877
Ivy_FraigParams_t_
Definition: ivy.h:132
Ivy_ObjSetClassNodeNext
static void Ivy_ObjSetClassNodeNext(Ivy_Obj_t *pObj, Ivy_Obj_t *pNext)
Definition: ivyFraig.c:154
Ivy_ObjIsTravIdCurrent
static int Ivy_ObjIsTravIdCurrent(Ivy_Man_t *p, Ivy_Obj_t *pObj)
Definition: ivy.h:257
Ivy_ObjIsNode
static int Ivy_ObjIsNode(Ivy_Obj_t *pObj)
Definition: ivy.h:245
Ivy_FraigForEachEquivClass
#define Ivy_FraigForEachEquivClass(pList, pEnt)
Definition: ivyFraig.c:165
Ivy_ObjChild0
static Ivy_Obj_t * Ivy_ObjChild0(Ivy_Obj_t *pObj)
Definition: ivy.h:273
Ivy_ObjSim
static Ivy_FraigSim_t * Ivy_ObjSim(Ivy_Obj_t *pObj)
Definition: ivyFraig.c:140
Ivy_FraigNodesAreEquivBdd
static int Ivy_FraigNodesAreEquivBdd(Ivy_Obj_t *pObj1, Ivy_Obj_t *pObj2)
Definition: ivyFraig.c:2769
Ivy_FraigCountPairsClasses
int Ivy_FraigCountPairsClasses(Ivy_FraigMan_t *p)
Definition: ivyFraig.c:1147
Ivy_FraigMan_t_::lCand
Ivy_FraigList_t lCand
Definition: ivyFraig.c:73
Ivy_FraigMan_t_::timeSim
abctime timeSim
Definition: ivyFraig.c:96
Ivy_Obj_t_::fFailTfo
unsigned fFailTfo
Definition: ivy.h:82
Ivy_ObjEquivListNext
static Ivy_Obj_t * Ivy_ObjEquivListNext(Ivy_Obj_t *pObj)
Definition: ivyFraig.c:145
Extra_ProgressBarStop
void Extra_ProgressBarStop(ProgressBar *p)
Definition: extraUtilProgress.c:118
Ivy_FraigNodesAreEquivBdd_int
ABC_NAMESPACE_IMPL_END ABC_NAMESPACE_IMPL_START DdNode * Ivy_FraigNodesAreEquivBdd_int(DdManager *dd, DdNode *bFunc, Vec_Ptr_t *vFront, int Level)
Definition: ivyFraig.c:2678
Ivy_InfoSetBit
static void Ivy_InfoSetBit(unsigned *p, int i)
Definition: ivy.h:190
Prove_ParamsStruct_t_::nRewritingLimitMulti
float nRewritingLimitMulti
Definition: ivyFraig.c:123
Ivy_FraigCreateModel
static int * Ivy_FraigCreateModel(Ivy_FraigMan_t *p)
Definition: ivyFraig.c:1520
Ivy_Obj_t_::fMarkA
unsigned fMarkA
Definition: ivy.h:78
Ivy_FraigSim_t_::pFanin0
Ivy_FraigSim_t * pFanin0
Definition: ivyFraig.c:48
Ivy_ObjEquivListPrev
static Ivy_Obj_t * Ivy_ObjEquivListPrev(Ivy_Obj_t *pObj)
Definition: ivyFraig.c:146
Aig_ManConst1
static Aig_Obj_t * Aig_ManConst1(Aig_Man_t *p)
Definition: aig.h:264
Ivy_FraigInsertClass
void Ivy_FraigInsertClass(Ivy_FraigList_t *pList, Ivy_Obj_t *pBase, Ivy_Obj_t *pClass)
Definition: ivyFraig.c:1097
Ivy_Man_t
typedefABC_NAMESPACE_HEADER_START struct Ivy_Man_t_ Ivy_Man_t
INCLUDES ///.
Definition: ivy.h:46
Ivy_ManPiNum
static int Ivy_ManPiNum(Ivy_Man_t *p)
Definition: ivy.h:218
Ivy_FraigParams_t_::dSimSatur
double dSimSatur
Definition: ivy.h:135
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
Ivy_ObjClassNodeLast
static Ivy_Obj_t * Ivy_ObjClassNodeLast(Ivy_Obj_t *pObj)
Definition: ivyFraig.c:141
Ivy_ObjNodeHashNext
static Ivy_Obj_t * Ivy_ObjNodeHashNext(Ivy_Obj_t *pObj)
Definition: ivyFraig.c:144
Prove_ParamsStruct_t_::nBddSizeLimit
int nBddSizeLimit
Definition: ivyFraig.c:128
Ivy_Obj_t_::fMarkB
unsigned fMarkB
Definition: ivy.h:79
Prove_ParamsStruct_t_::nTotalBacktrackLimit
ABC_INT64_T nTotalBacktrackLimit
Definition: ivyFraig.c:133
Ivy_ObjClassNodeNext
static Ivy_Obj_t * Ivy_ObjClassNodeNext(Ivy_Obj_t *pObj)
Definition: ivyFraig.c:143
sat_solver_simplify
int sat_solver_simplify(sat_solver *s)
Definition: satSolver.c:1276
Prove_ParamsStruct_t_::nItersMax
int nItersMax
Definition: ivyFraig.c:117
Ivy_ObjIsAnd
static int Ivy_ObjIsAnd(Ivy_Obj_t *pObj)
Definition: ivy.h:242
Ivy_FraigSavePattern
void Ivy_FraigSavePattern(Ivy_FraigMan_t *p)
Definition: ivyFraig.c:1543
sat_solver_new
sat_solver * sat_solver_new(void)
Definition: satSolver.c:1001
Ivy_FraigSetActivityFactors_rec
int Ivy_FraigSetActivityFactors_rec(Ivy_FraigMan_t *p, Ivy_Obj_t *pObj, int LevelMin, int LevelMax)
Definition: ivyFraig.c:2600
Ivy_ObjIsConst1
static int Ivy_ObjIsConst1(Ivy_Obj_t *pObj)
Definition: ivy.h:233
Aig_Obj_t_::fPhase
unsigned int fPhase
Definition: aig.h:78
Ivy_FraigPerform_int
static Ivy_Man_t * Ivy_FraigPerform_int(Ivy_Man_t *pManAig, Ivy_FraigParams_t *pParams, ABC_INT64_T nBTLimitGlobal, ABC_INT64_T nInsLimitGlobal, ABC_INT64_T *pnSatConfs, ABC_INT64_T *pnSatInspects)
Definition: ivyFraig.c:414
Ivy_FraigSim_t_
Definition: ivyFraig.c:44
Ivy_InfoXorBit
static void Ivy_InfoXorBit(unsigned *p, int i)
Definition: ivy.h:191
Prove_ParamsStruct_t_::fVerbose
int fVerbose
Definition: ivyFraig.c:115
Ivy_FraigForEachClassNode
#define Ivy_FraigForEachClassNode(pClass, pEnt)
Definition: ivyFraig.c:176
Vec_PtrAlloc
static Vec_Ptr_t * Vec_PtrAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: vecPtr.h:83
Ivy_ManStartFrom
Ivy_Man_t * Ivy_ManStartFrom(Ivy_Man_t *p)
Definition: ivyMan.c:85
Ivy_FraigMan_t_::nSimWords
int nSimWords
Definition: ivyFraig.c:64
Ivy_FraigStartSimple
static Ivy_FraigMan_t * Ivy_FraigStartSimple(Ivy_Man_t *pManAig, Ivy_FraigParams_t *pParams)
Definition: ivyFraig.c:530
Ivy_FraigMan_t_::nClassesEnd
int nClassesEnd
Definition: ivyFraig.c:86
Ivy_FraigMan_t_::pSimWords
char * pSimWords
Definition: ivyFraig.c:65
Ivy_FraigPrintSimClasses
void Ivy_FraigPrintSimClasses(Ivy_FraigMan_t *p)
Definition: ivyFraig.c:1466
Ivy_ObjSetClassNodeRepr
static void Ivy_ObjSetClassNodeRepr(Ivy_Obj_t *pObj, Ivy_Obj_t *pRepr)
Definition: ivyFraig.c:153
Ivy_FraigMan_t_::nBTLimitGlobal
ABC_INT64_T nBTLimitGlobal
Definition: ivyFraig.c:58
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
ABC_PRT
#define ABC_PRT(a, t)
Definition: abc_global.h:220
Ivy_Not
static Ivy_Obj_t * Ivy_Not(Ivy_Obj_t *p)
Definition: ivy.h:194
Ivy_NotCond
static Ivy_Obj_t * Ivy_NotCond(Ivy_Obj_t *p, int c)
Definition: ivy.h:195
Cudd_bddIthVar
DdNode * Cudd_bddIthVar(DdManager *dd, int i)
Definition: cuddAPI.c:416
Ivy_ManForEachNodeVec
#define Ivy_ManForEachNodeVec(p, vIds, pObj, i)
Definition: ivy.h:408
Cudd_bddXor
DdNode * Cudd_bddXor(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddBddIte.c:476
Ivy_FraigMan_t_::pSat
sat_solver * pSat
Definition: ivyFraig.c:76
Ivy_FraigSim_t_::pData
unsigned pData[0]
Definition: ivyFraig.c:50
Ivy_ObjSetFaninVec
static void Ivy_ObjSetFaninVec(Ivy_Obj_t *pObj, Vec_Ptr_t *vFanins)
Definition: ivyFraig.c:160
Ivy_ManObjNum
static int Ivy_ManObjNum(Ivy_Man_t *p)
Definition: ivy.h:225
Extra_ProgressBarStart
ProgressBar * Extra_ProgressBarStart(FILE *pFile, int nItemsTotal)
FUNCTION DEFINITIONS ///.
Definition: extraUtilProgress.c:62
Ivy_FraigPerform
Ivy_Man_t * Ivy_FraigPerform(Ivy_Man_t *pManAig, Ivy_FraigParams_t *pParams)
Definition: ivyFraig.c:451
Prove_ParamsStruct_t_::nFraigingLimitMulti
float nFraigingLimitMulti
Definition: ivyFraig.c:126
ABC_CALLOC
#define ABC_CALLOC(type, num)
Definition: abc_global.h:230
Ivy_FraigMan_t_::time2
abctime time2
Definition: ivyFraig.c:105
Ivy_FraigSimulateOneSim
void Ivy_FraigSimulateOneSim(Ivy_FraigMan_t *p)
Definition: ivyFraig.c:1023
l_False
#define l_False
Definition: SolverTypes.h:85
Ivy_FraigList_t_::pTail
Ivy_Obj_t * pTail
Definition: ivyFraig.c:40
Ivy_ObjChild1
static Ivy_Obj_t * Ivy_ObjChild1(Ivy_Obj_t *pObj)
Definition: ivy.h:274
Cudd_NotCond
#define Cudd_NotCond(node, c)
Definition: cudd.h:383
Cudd_bddAnd
DdNode * Cudd_bddAnd(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddBddIte.c:314
Ivy_FraigMan_t_::nSatCallsSat
int nSatCallsSat
Definition: ivyFraig.c:90
Ivy_FraigAnd
static Ivy_Obj_t * Ivy_FraigAnd(Ivy_FraigMan_t *p, Ivy_Obj_t *pObjOld)
Definition: ivyFraig.c:2027
Ivy_ObjFaninPhase
static int Ivy_ObjFaninPhase(Ivy_Obj_t *pObj)
Definition: ivy.h:280
sat_solver_t
Definition: satSolver.h:91
Ivy_FraigMan_t_::nPairsBeg
int nPairsBeg
Definition: ivyFraig.c:87
assert
#define assert(ex)
Definition: util_old.h:213
Extra_ProgressBarUpdate
static void Extra_ProgressBarUpdate(ProgressBar *p, int nItemsCur, char *pString)
Definition: extra.h:243
Ivy_FraigSim_t
struct Ivy_FraigSim_t_ Ivy_FraigSim_t
Definition: ivyFraig.c:34
Ivy_FraigMan_t_::timeTotal
abctime timeTotal
Definition: ivyFraig.c:103
Ivy_ManNodeNum
static int Ivy_ManNodeNum(Ivy_Man_t *p)
Definition: ivy.h:227
Ivy_NodeCompareSims
int Ivy_NodeCompareSims(Ivy_FraigMan_t *p, Ivy_Obj_t *pObj0, Ivy_Obj_t *pObj1)
Definition: ivyFraig.c:810
Ivy_FraigSimulate
static void Ivy_FraigSimulate(Ivy_FraigMan_t *p)
Definition: ivyFraig.c:1615
Sat_SolverPrintStats
void Sat_SolverPrintStats(FILE *pFile, sat_solver *p)
Definition: satUtil.c:188
Cudd_Ref
void Cudd_Ref(DdNode *n)
Definition: cuddRef.c:129
Ivy_ManForEachObj
#define Ivy_ManForEachObj(p, pObj, i)
Definition: ivy.h:393
Ivy_FraigMiterPrint
static void Ivy_FraigMiterPrint(Ivy_Man_t *pNtk, char *pString, abctime clk, int fVerbose)
Definition: ivyFraig.c:1796
Aig_NotCond
static Aig_Obj_t * Aig_NotCond(Aig_Obj_t *p, int c)
Definition: aig.h:248
Ivy_FraigMan_t_::timeSatFail
abctime timeSatFail
Definition: ivyFraig.c:101
Ivy_FraigParams_t_::fPatScores
int fPatScores
Definition: ivy.h:136
Ivy_FraigCollectSuper
Vec_Ptr_t * Ivy_FraigCollectSuper(Ivy_Obj_t *pObj, int fUseMuxes)
Definition: ivyFraig.c:2498
Vec_IntFree
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
Vec_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition: vecPtr.h:55
Ivy_FraigMan_t_::pProgress
ProgressBar * pProgress
Definition: ivyFraig.c:80
Ivy_NodeSimulate
void Ivy_NodeSimulate(Ivy_FraigMan_t *p, Ivy_Obj_t *pObj)
Definition: ivyFraig.c:888
Ivy_FraigAddClausesSuper
void Ivy_FraigAddClausesSuper(Ivy_FraigMan_t *p, Ivy_Obj_t *pNode, Vec_Ptr_t *vSuper)
Definition: ivyFraig.c:2435
abctime
ABC_INT64_T abctime
Definition: abc_global.h:278
Ivy_FraigAssignRandom
void Ivy_FraigAssignRandom(Ivy_FraigMan_t *p)
Definition: ivyFraig.c:722
Ivy_FraigExtractCone
Aig_Man_t * Ivy_FraigExtractCone(Ivy_Man_t *p, Ivy_Obj_t *pObj1, Ivy_Obj_t *pObj2, Vec_Int_t *vLeaves)
Definition: ivyFraig.c:2863
Ivy_FraigCleanPatScores
void Ivy_FraigCleanPatScores(Ivy_FraigMan_t *p)
Definition: ivyFraig.c:1664
Ivy_FraigMan_t_::timeSatSat
abctime timeSatSat
Definition: ivyFraig.c:100
Ivy_FraigMan_t_::pParams
Ivy_FraigParams_t * pParams
Definition: ivyFraig.c:56
Ivy_FraigSweep
static void Ivy_FraigSweep(Ivy_FraigMan_t *p)
Definition: ivyFraig.c:1968
Aig_ManCleanup
int Aig_ManCleanup(Aig_Man_t *p)
Definition: aigMan.c:265
Ivy_ObjFaninC0
static int Ivy_ObjFaninC0(Ivy_Obj_t *pObj)
Definition: ivy.h:269
Ivy_FraigAssignDist1
void Ivy_FraigAssignDist1(Ivy_FraigMan_t *p, unsigned *pPat)
Definition: ivyFraig.c:741
Ivy_And
Ivy_Obj_t * Ivy_And(Ivy_Man_t *p, Ivy_Obj_t *p0, Ivy_Obj_t *p1)
Definition: ivyOper.c:84
Prove_ParamsStruct_t_
Definition: ivyFraig.c:109
Ivy_ManCleanup
int Ivy_ManCleanup(Ivy_Man_t *p)
Definition: ivyMan.c:265
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
Ivy_Obj_t_::pPrevFan1
Ivy_Obj_t * pPrevFan1
Definition: ivy.h:92
Ivy_FraigMan_t_::pPatScores
int * pPatScores
Definition: ivyFraig.c:70
Ivy_FraigMan_t_::timeSat
abctime timeSat
Definition: ivyFraig.c:98
Ivy_FraigMan_t_::nSatVars
int nSatVars
Definition: ivyFraig.c:77
Ivy_FraigParams_t_::nBTLimitMiter
int nBTLimitMiter
Definition: ivy.h:144
Ivy_ObjSetTravIdCurrent
static void Ivy_ObjSetTravIdCurrent(Ivy_Man_t *p, Ivy_Obj_t *pObj)
Definition: ivy.h:255
Cudd_DagSize
int Cudd_DagSize(DdNode *node)
Definition: cuddUtil.c:442
Ivy_ObjFraig
static Ivy_Obj_t * Ivy_ObjFraig(Ivy_Obj_t *pObj)
Definition: ivyFraig.c:147
Vec_PtrFree
static void Vec_PtrFree(Vec_Ptr_t *p)
Definition: vecPtr.h:223
Ivy_Obj_t_::pEquiv
Ivy_Obj_t * pEquiv
Definition: ivy.h:93