abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
sscCore.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [sscCore.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [SAT sweeping under constraints.]
8 
9  Synopsis [The core procedures.]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - June 29, 2008.]
16 
17  Revision [$Id: sscCore.c,v 1.00 2008/07/29 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "sscInt.h"
22 #include "proof/cec/cec.h"
23 
24 ABC_NAMESPACE_IMPL_START
25 
26 
27 ////////////////////////////////////////////////////////////////////////
28 /// DECLARATIONS ///
29 ////////////////////////////////////////////////////////////////////////
30 
31 ////////////////////////////////////////////////////////////////////////
32 /// FUNCTION DEFINITIONS ///
33 ////////////////////////////////////////////////////////////////////////
34 
35 /**Function*************************************************************
36 
37  Synopsis [This procedure sets default parameters.]
38 
39  Description []
40 
41  SideEffects []
42 
43  SeeAlso []
44 
45 ***********************************************************************/
46 void Ssc_ManSetDefaultParams( Ssc_Pars_t * p )
47 {
48  memset( p, 0, sizeof(Ssc_Pars_t) );
49  p->nWords = 1; // the number of simulation words
50  p->nBTLimit = 1000; // conflict limit at a node
51  p->nSatVarMax = 5000; // the max number of SAT variables
52  p->nCallsRecycle = 100; // calls to perform before recycling SAT solver
53  p->fVerbose = 0; // verbose stats
54 }
55 
56 /**Function*************************************************************
57 
58  Synopsis []
59 
60  Description []
61 
62  SideEffects []
63 
64  SeeAlso []
65 
66 ***********************************************************************/
67 void Ssc_ManStop( Ssc_Man_t * p )
68 {
69  Vec_IntFreeP( &p->vFront );
70  Vec_IntFreeP( &p->vFanins );
71  Vec_IntFreeP( &p->vPattern );
72  Vec_IntFreeP( &p->vDisPairs );
73  Vec_IntFreeP( &p->vPivot );
74  Vec_IntFreeP( &p->vId2Var );
75  Vec_IntFreeP( &p->vVar2Id );
76  if ( p->pSat ) sat_solver_delete( p->pSat );
77  Gia_ManStopP( &p->pFraig );
78  ABC_FREE( p );
79 }
80 Ssc_Man_t * Ssc_ManStart( Gia_Man_t * pAig, Gia_Man_t * pCare, Ssc_Pars_t * pPars )
81 {
82  Ssc_Man_t * p;
83  p = ABC_CALLOC( Ssc_Man_t, 1 );
84  p->pPars = pPars;
85  p->pAig = pAig;
86  p->pCare = pCare;
87  p->pFraig = Gia_ManDupDfs( p->pCare );
88  assert( p->pFraig->pHTable == NULL );
89  assert( !Gia_ManHasDangling(p->pFraig) );
90  Gia_ManInvertPos( p->pFraig );
91  Ssc_ManStartSolver( p );
92  if ( p->pSat == NULL )
93  {
94  printf( "Constraints are UNSAT after propagation.\n" );
95  Ssc_ManStop( p );
96  return (Ssc_Man_t *)(ABC_PTRINT_T)1;
97  }
98 // p->vPivot = Ssc_GiaFindPivotSim( p->pFraig );
99 // Vec_IntFreeP( &p->vPivot );
100  p->vPivot = Ssc_ManFindPivotSat( p );
101  if ( p->vPivot == (Vec_Int_t *)(ABC_PTRINT_T)1 )
102  {
103  printf( "Constraints are UNSAT.\n" );
104  Ssc_ManStop( p );
105  return (Ssc_Man_t *)(ABC_PTRINT_T)1;
106  }
107  if ( p->vPivot == NULL )
108  {
109  printf( "Conflict limit is reached while trying to find one SAT assignment.\n" );
110  Ssc_ManStop( p );
111  return NULL;
112  }
113  sat_solver_bookmark( p->pSat );
114 // Vec_IntPrint( p->vPivot );
115  Gia_ManSetPhasePattern( p->pAig, p->vPivot );
116  Gia_ManSetPhasePattern( p->pCare, p->vPivot );
117  if ( Gia_ManCheckCoPhase(p->pCare) )
118  {
119  printf( "Computed reference pattern violates %d constraints (this is a bug!).\n", Gia_ManCheckCoPhase(p->pCare) );
120  Ssc_ManStop( p );
121  return NULL;
122  }
123  // other things
124  p->vDisPairs = Vec_IntAlloc( 100 );
125  p->vPattern = Vec_IntAlloc( 100 );
126  p->vFanins = Vec_IntAlloc( 100 );
127  p->vFront = Vec_IntAlloc( 100 );
128  Ssc_GiaClassesInit( pAig );
129  // now it is ready for refinement using simulation
130  return p;
131 }
132 void Ssc_ManPrintStats( Ssc_Man_t * p )
133 {
134  Abc_Print( 1, "Parameters: SimWords = %d. SatConfs = %d. SatVarMax = %d. CallsRec = %d. Verbose = %d.\n",
135  p->pPars->nWords, p->pPars->nBTLimit, p->pPars->nSatVarMax, p->pPars->nCallsRecycle, p->pPars->fVerbose );
136  Abc_Print( 1, "SAT calls : Total = %d. Proof = %d. Cex = %d. Undec = %d.\n",
137  p->nSatCalls, p->nSatCallsUnsat, p->nSatCallsSat, p->nSatCallsUndec );
138  Abc_Print( 1, "SAT solver: Vars = %d. Clauses = %d. Recycles = %d. Sim rounds = %d.\n",
139  sat_solver_nvars(p->pSat), sat_solver_nclauses(p->pSat), p->nRecycles, p->nSimRounds );
140 
141  p->timeOther = p->timeTotal - p->timeSimInit - p->timeSimSat - p->timeCnfGen - p->timeSatSat - p->timeSatUnsat - p->timeSatUndec;
142  ABC_PRTP( "Initialization ", p->timeSimInit, p->timeTotal );
143  ABC_PRTP( "SAT simulation ", p->timeSimSat, p->timeTotal );
144  ABC_PRTP( "CNF generation ", p->timeSimSat, p->timeTotal );
145  ABC_PRTP( "SAT solving ", p->timeSat-p->timeCnfGen, p->timeTotal );
146  ABC_PRTP( " unsat ", p->timeSatUnsat, p->timeTotal );
147  ABC_PRTP( " sat ", p->timeSatSat, p->timeTotal );
148  ABC_PRTP( " undecided ", p->timeSatUndec, p->timeTotal );
149  ABC_PRTP( "Other ", p->timeOther, p->timeTotal );
150  ABC_PRTP( "TOTAL ", p->timeTotal, p->timeTotal );
151 }
152 
153 /**Function*************************************************************
154 
155  Synopsis [Refine one class by resimulating one pattern.]
156 
157  Description []
158 
159  SideEffects []
160 
161  SeeAlso []
162 
163 ***********************************************************************/
164 int Ssc_GiaSimulatePatternFraig_rec( Ssc_Man_t * p, int iFraigObj )
165 {
166  Gia_Obj_t * pObj;
167  int Res0, Res1;
168  if ( Ssc_ObjSatVar(p, iFraigObj) )
169  return sat_solver_var_value( p->pSat, Ssc_ObjSatVar(p, iFraigObj) );
170  pObj = Gia_ManObj( p->pFraig, iFraigObj );
171  assert( Gia_ObjIsAnd(pObj) );
172  Res0 = Ssc_GiaSimulatePatternFraig_rec( p, Gia_ObjFaninId0(pObj, iFraigObj) );
173  Res1 = Ssc_GiaSimulatePatternFraig_rec( p, Gia_ObjFaninId1(pObj, iFraigObj) );
174  pObj->fMark0 = (Res0 ^ Gia_ObjFaninC0(pObj)) & (Res1 ^ Gia_ObjFaninC1(pObj));
175  return pObj->fMark0;
176 }
177 int Ssc_GiaSimulatePattern_rec( Ssc_Man_t * p, Gia_Obj_t * pObj )
178 {
179  int Res0, Res1;
180  if ( Gia_ObjIsTravIdCurrent(p->pAig, pObj) )
181  return pObj->fMark0;
182  Gia_ObjSetTravIdCurrent(p->pAig, pObj);
183  if ( ~pObj->Value ) // mapping into FRAIG exists - simulate FRAIG
184  {
185  Res0 = Ssc_GiaSimulatePatternFraig_rec( p, Abc_Lit2Var(pObj->Value) );
186  pObj->fMark0 = Res0 ^ Abc_LitIsCompl(pObj->Value);
187  }
188  else // mapping into FRAIG does not exist - simulate AIG
189  {
190  Res0 = Ssc_GiaSimulatePattern_rec( p, Gia_ObjFanin0(pObj) );
191  Res1 = Ssc_GiaSimulatePattern_rec( p, Gia_ObjFanin1(pObj) );
192  pObj->fMark0 = (Res0 ^ Gia_ObjFaninC0(pObj)) & (Res1 ^ Gia_ObjFaninC1(pObj));
193  }
194  return pObj->fMark0;
195 }
196 int Ssc_GiaResimulateOneClass( Ssc_Man_t * p, int iRepr, int iObj )
197 {
198  int Ent, RetValue;
199  assert( iRepr == Gia_ObjRepr(p->pAig, iObj) );
200  assert( Gia_ObjIsHead( p->pAig, iRepr ) );
201  // set bit-values at the nodes according to the counter-example
202  Gia_ManIncrementTravId( p->pAig );
203  Gia_ClassForEachObj( p->pAig, iRepr, Ent )
204  Ssc_GiaSimulatePattern_rec( p, Gia_ManObj(p->pAig, Ent) );
205  // refine one class using these bit-values
206  RetValue = Ssc_GiaSimClassRefineOneBit( p->pAig, iRepr );
207  // check that the candidate equivalence is indeed refined
208  assert( iRepr != Gia_ObjRepr(p->pAig, iObj) );
209  return RetValue;
210 }
211 
212 /**Function*************************************************************
213 
214  Synopsis [Perform verification of conditional sweeping.]
215 
216  Description []
217 
218  SideEffects []
219 
220  SeeAlso []
221 
222 ***********************************************************************/
223 int Ssc_PerformVerification( Gia_Man_t * p0, Gia_Man_t * p1, Gia_Man_t * pC )
224 {
225  int Status;
226  Cec_ParCec_t ParsCec, * pPars = &ParsCec;
227  // derive the OR of constraint outputs
228  Gia_Man_t * pCond = Gia_ManDupAndOr( pC, Gia_ManPoNum(p0), 1, 0 );
229  // derive F = F & !OR(c0, c1, c2, ...)
230  Gia_Man_t * p0c = Gia_ManMiter( p0, pCond, 0, 0, 0, 1, 0 );
231  // derive F = F & !OR(c0, c1, c2, ...)
232  Gia_Man_t * p1c = Gia_ManMiter( p1, pCond, 0, 0, 0, 1, 0 );
233  // derive dual-output miter
234  Gia_Man_t * pMiter = Gia_ManMiter( p0c, p1c, 0, 1, 0, 0, 0 );
235  Gia_ManStop( p0c );
236  Gia_ManStop( p1c );
237  Gia_ManStop( pCond );
238  // run equivalence checking
239  Cec_ManCecSetDefaultParams( pPars );
240  Status = Cec_ManVerify( pMiter, pPars );
241  Gia_ManStop( pMiter );
242  // report the results
243  if ( Status == 1 )
244  printf( "Verification succeeded.\n" );
245  else if ( Status == 0 )
246  printf( "Verification failed.\n" );
247  else if ( Status == -1 )
248  printf( "Verification undecided.\n" );
249  else assert( 0 );
250  return Status;
251 }
252 
253 /**Function*************************************************************
254 
255  Synopsis []
256 
257  Description []
258 
259  SideEffects []
260 
261  SeeAlso []
262 
263 ***********************************************************************/
264 Gia_Man_t * Ssc_PerformSweepingInt( Gia_Man_t * pAig, Gia_Man_t * pCare, Ssc_Pars_t * pPars )
265 {
266  Ssc_Man_t * p;
267  Gia_Man_t * pResult, * pTemp;
268  Gia_Obj_t * pObj, * pRepr;
269  abctime clk, clkTotal = Abc_Clock();
270  int i, fCompl, nRefined, status;
271 clk = Abc_Clock();
272  assert( Gia_ManRegNum(pCare) == 0 );
273  assert( Gia_ManCiNum(pAig) == Gia_ManCiNum(pCare) );
274  assert( Gia_ManIsNormalized(pAig) );
275  assert( Gia_ManIsNormalized(pCare) );
276  // reset random numbers
277  Gia_ManRandom( 1 );
278  // sweeping manager
279  p = Ssc_ManStart( pAig, pCare, pPars );
280  if ( p == (Ssc_Man_t *)(ABC_PTRINT_T)1 ) // UNSAT
281  return Gia_ManDupZero( pAig );
282  if ( p == NULL ) // timeout
283  return Gia_ManDup( pAig );
284  if ( p->pPars->fVerbose )
285  printf( "Care set produced %d hits out of %d.\n", Ssc_GiaEstimateCare(p->pFraig, 5), 640 );
286  // perform simulation
287  while ( 1 )
288  {
289  // simulate care set
290  Ssc_GiaRandomPiPattern( p->pFraig, 5, NULL );
291  Ssc_GiaSimRound( p->pFraig );
292  // transfer care patterns to user's AIG
293  if ( !Ssc_GiaTransferPiPattern( pAig, p->pFraig, p->vPivot ) )
294  break;
295  // simulate the main AIG
296  Ssc_GiaSimRound( pAig );
297  nRefined = Ssc_GiaClassesRefine( pAig );
298  if ( pPars->fVerbose )
299  Gia_ManEquivPrintClasses( pAig, 0, 0 );
300  if ( nRefined <= Gia_ManCandNum(pAig) / 100 )
301  break;
302  }
303 p->timeSimInit += Abc_Clock() - clk;
304 
305  // prepare user's AIG
306  Gia_ManFillValue(pAig);
307  Gia_ManConst0(pAig)->Value = 0;
308  Gia_ManForEachCi( pAig, pObj, i )
309  pObj->Value = Gia_Obj2Lit( p->pFraig, Gia_ManCi(p->pFraig, i) );
310 // Gia_ManLevelNum(pAig);
311  // prepare swept AIG (should be done after starting SAT solver in Ssc_ManStart)
312  Gia_ManHashStart( p->pFraig );
313  // perform sweeping
314  Ssc_GiaResetPiPattern( pAig, pPars->nWords );
315  Ssc_GiaSavePiPattern( pAig, p->vPivot );
316  Gia_ManForEachCand( pAig, pObj, i )
317  {
318  if ( pAig->iPatsPi == 64 * pPars->nWords )
319  {
320 clk = Abc_Clock();
321  Ssc_GiaSimRound( pAig );
322  Ssc_GiaClassesRefine( pAig );
323  if ( pPars->fVerbose )
324  Gia_ManEquivPrintClasses( pAig, 0, 0 );
325  Ssc_GiaClassesCheckPairs( pAig, p->vDisPairs );
326  Vec_IntClear( p->vDisPairs );
327  // prepare next patterns
328  Ssc_GiaResetPiPattern( pAig, pPars->nWords );
329  Ssc_GiaSavePiPattern( pAig, p->vPivot );
330 p->timeSimSat += Abc_Clock() - clk;
331 //printf( "\n" );
332  }
333  if ( Gia_ObjIsAnd(pObj) )
334  pObj->Value = Gia_ManHashAnd( p->pFraig, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
335  if ( !Gia_ObjHasRepr(pAig, i) )
336  continue;
337  pRepr = Gia_ObjReprObj(pAig, i);
338  if ( (int)pObj->Value == Abc_LitNotCond( pRepr->Value, pRepr->fPhase ^ pObj->fPhase ) )
339  {
340  Gia_ObjSetProved( pAig, i );
341  continue;
342  }
343  assert( Abc_Lit2Var(pRepr->Value) != Abc_Lit2Var(pObj->Value) );
344  fCompl = pRepr->fPhase ^ pObj->fPhase ^ Abc_LitIsCompl(pRepr->Value) ^ Abc_LitIsCompl(pObj->Value);
345 
346  // perform SAT call
347 clk = Abc_Clock();
348  p->nSatCalls++;
349  status = Ssc_ManCheckEquivalence( p, Abc_Lit2Var(pRepr->Value), Abc_Lit2Var(pObj->Value), fCompl );
350  if ( status == l_False )
351  {
352  p->nSatCallsUnsat++;
353  pObj->Value = Abc_LitNotCond( pRepr->Value, pRepr->fPhase ^ pObj->fPhase );
354  Gia_ObjSetProved( pAig, i );
355  }
356  else if ( status == l_True )
357  {
358  p->nSatCallsSat++;
359  Ssc_GiaSavePiPattern( pAig, p->vPattern );
360  Vec_IntPush( p->vDisPairs, Gia_ObjRepr(p->pAig, i) );
361  Vec_IntPush( p->vDisPairs, i );
362 // printf( "Try %2d and %2d: ", Gia_ObjRepr(p->pAig, i), i );
363 // Vec_IntPrint( p->vPattern );
364  if ( Gia_ObjRepr(p->pAig, i) > 0 )
365  Ssc_GiaResimulateOneClass( p, Gia_ObjRepr(p->pAig, i), i );
366  }
367  else if ( status == l_Undef )
368  p->nSatCallsUndec++;
369  else assert( 0 );
370 p->timeSat += Abc_Clock() - clk;
371  }
372  if ( pAig->iPatsPi > 1 )
373  {
374 clk = Abc_Clock();
375  while ( pAig->iPatsPi < 64 * pPars->nWords )
376  Ssc_GiaSavePiPattern( pAig, p->vPivot );
377  Ssc_GiaSimRound( pAig );
378  Ssc_GiaClassesRefine( pAig );
379  if ( pPars->fVerbose )
380  Gia_ManEquivPrintClasses( pAig, 0, 0 );
381  Ssc_GiaClassesCheckPairs( pAig, p->vDisPairs );
382  Vec_IntClear( p->vDisPairs );
383 p->timeSimSat += Abc_Clock() - clk;
384  }
385 // Gia_ManEquivPrintClasses( pAig, 1, 0 );
386 // Gia_ManPrint( pAig );
387 
388  // generate the resulting AIG
389  pResult = Gia_ManEquivReduce( pAig, 0, 0, 1, 0 );
390  if ( pResult == NULL )
391  {
392  printf( "There is no equivalences.\n" );
393  ABC_FREE( pAig->pReprs );
394  ABC_FREE( pAig->pNexts );
395  pResult = Gia_ManDup( pAig );
396  }
397  pResult = Gia_ManCleanup( pTemp = pResult );
398  Gia_ManStop( pTemp );
399  p->timeTotal = Abc_Clock() - clkTotal;
400  if ( pPars->fVerbose )
401  Ssc_ManPrintStats( p );
402  Ssc_ManStop( p );
403  // count the number of representatives
404  if ( pPars->fVerbose )
405  {
406  Abc_Print( 1, "Reduction in AIG nodes:%8d ->%8d (%6.2f %%). ",
407  Gia_ManAndNum(pAig), Gia_ManAndNum(pResult),
408  100.0 - 100.0 * Gia_ManAndNum(pResult) / Gia_ManAndNum(pAig) );
409  Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal );
410  }
411  return pResult;
412 }
413 Gia_Man_t * Ssc_PerformSweeping( Gia_Man_t * pAig, Gia_Man_t * pCare, Ssc_Pars_t * pPars )
414 {
415  Gia_Man_t * pResult = Ssc_PerformSweepingInt( pAig, pCare, pPars );
416  if ( pPars->fVerify )
417  Ssc_PerformVerification( pAig, pResult, pCare );
418  return pResult;
419 }
420 Gia_Man_t * Ssc_PerformSweepingConstr( Gia_Man_t * p, Ssc_Pars_t * pPars )
421 {
422  Gia_Man_t * pAig, * pCare, * pResult;
423  int i;
424  if ( pPars->fVerbose )
425  Abc_Print( 0, "SAT sweeping AIG with %d constraints.\n", p->nConstrs );
426  if ( p->nConstrs == 0 )
427  {
428  pAig = Gia_ManDup( p );
429  pCare = Gia_ManStart( Gia_ManCiNum(p) + 2 );
430  pCare->pName = Abc_UtilStrsav( "care" );
431  for ( i = 0; i < Gia_ManCiNum(p); i++ )
432  Gia_ManAppendCi( pCare );
433  Gia_ManAppendCo( pCare, 0 );
434  }
435  else
436  {
437  Vec_Int_t * vOuts = Vec_IntStartNatural( Gia_ManPoNum(p) );
438  pAig = Gia_ManDupCones( p, Vec_IntArray(vOuts), Gia_ManPoNum(p) - p->nConstrs, 0 );
439  pCare = Gia_ManDupCones( p, Vec_IntArray(vOuts) + Gia_ManPoNum(p) - p->nConstrs, p->nConstrs, 0 );
440  Vec_IntFree( vOuts );
441  }
442  if ( pPars->fVerbose )
443  {
444  printf( "User AIG: " );
445  Gia_ManPrintStats( pAig, NULL );
446  printf( "Care AIG: " );
447  Gia_ManPrintStats( pCare, NULL );
448  }
449 
450  pAig = Gia_ManDupLevelized( pResult = pAig );
451  Gia_ManStop( pResult );
452  pResult = Ssc_PerformSweeping( pAig, pCare, pPars );
453  if ( pPars->fAppend )
454  {
455  Gia_ManDupAppendShare( pResult, pCare );
456  pResult->nConstrs = Gia_ManPoNum(pCare);
457  }
458  Gia_ManStop( pAig );
459  Gia_ManStop( pCare );
460  return pResult;
461 }
462 
463 ////////////////////////////////////////////////////////////////////////
464 /// END OF FILE ///
465 ////////////////////////////////////////////////////////////////////////
466 
467 
468 ABC_NAMESPACE_IMPL_END
469 
memset
char * memset()
Ssc_GiaSimulatePatternFraig_rec
int Ssc_GiaSimulatePatternFraig_rec(Ssc_Man_t *p, int iFraigObj)
Definition: sscCore.c:164
Vec_IntArray
static int * Vec_IntArray(Vec_Int_t *p)
Definition: vecInt.h:328
Ssc_PerformSweepingInt
Gia_Man_t * Ssc_PerformSweepingInt(Gia_Man_t *pAig, Gia_Man_t *pCare, Ssc_Pars_t *pPars)
Definition: sscCore.c:264
Gia_ManDupCones
Gia_Man_t * Gia_ManDupCones(Gia_Man_t *p, int *pPos, int nPos, int fTrimPis)
Definition: giaDup.c:2691
Ssc_ObjSatVar
static int Ssc_ObjSatVar(Ssc_Man_t *p, int iObj)
MACRO DEFINITIONS ///.
Definition: sscInt.h:90
Gia_ManDup
Gia_Man_t * Gia_ManDup(Gia_Man_t *p)
Definition: giaDup.c:552
Gia_ManStop
void Gia_ManStop(Gia_Man_t *p)
Definition: giaMan.c:77
Gia_ManPrintStats
void Gia_ManPrintStats(Gia_Man_t *p, Gps_Par_t *pPars)
Definition: giaMan.c:389
Gia_Man_t_::pNexts
int * pNexts
Definition: gia.h:122
Gia_ManPoNum
static int Gia_ManPoNum(Gia_Man_t *p)
Definition: gia.h:386
Gia_ObjFaninC1
static int Gia_ObjFaninC1(Gia_Obj_t *pObj)
Definition: gia.h:452
Gia_ManCi
static Gia_Obj_t * Gia_ManCi(Gia_Man_t *p, int v)
Definition: gia.h:403
Gia_ManAppendCo
static int Gia_ManAppendCo(Gia_Man_t *p, int iLit0)
Definition: gia.h:703
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Ssc_GiaSimClassRefineOneBit
int Ssc_GiaSimClassRefineOneBit(Gia_Man_t *p, int i)
Definition: sscClass.c:162
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
Ssc_GiaResetPiPattern
void Ssc_GiaResetPiPattern(Gia_Man_t *p, int nWords)
Definition: sscSim.c:141
Ssc_ManStart
Ssc_Man_t * Ssc_ManStart(Gia_Man_t *pAig, Gia_Man_t *pCare, Ssc_Pars_t *pPars)
Definition: sscCore.c:80
sat_solver_bookmark
static void sat_solver_bookmark(sat_solver *s)
Definition: satSolver.h:247
Gia_ObjIsTravIdCurrent
static int Gia_ObjIsTravIdCurrent(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:533
l_Undef
#define l_Undef
Definition: SolverTypes.h:86
Ssc_Man_t
typedefABC_NAMESPACE_HEADER_START struct Ssc_Man_t_ Ssc_Man_t
INCLUDES ///.
Definition: sscInt.h:46
Gia_ManInvertPos
void Gia_ManInvertPos(Gia_Man_t *pAig)
Definition: giaUtil.c:1425
Ssc_Pars_t
typedefABC_NAMESPACE_HEADER_START struct Ssc_Pars_t_ Ssc_Pars_t
INCLUDES ///.
Definition: ssc.h:43
Gia_ManAppendCi
static int Gia_ManAppendCi(Gia_Man_t *p)
Definition: gia.h:583
sat_solver_delete
void sat_solver_delete(sat_solver *s)
Definition: satSolver.c:1141
Ssc_ManPrintStats
void Ssc_ManPrintStats(Ssc_Man_t *p)
Definition: sscCore.c:132
Gia_ObjIsHead
static int Gia_ObjIsHead(Gia_Man_t *p, int Id)
Definition: gia.h:916
l_True
#define l_True
Definition: SolverTypes.h:84
Gia_ManDupZero
Gia_Man_t * Gia_ManDupZero(Gia_Man_t *p)
Definition: giaDup.c:608
Abc_Clock
static abctime Abc_Clock()
Definition: abc_global.h:279
Gia_ManDupAndOr
Gia_Man_t * Gia_ManDupAndOr(Gia_Man_t *p, int nOuts, int fUseOr, int fCompl)
Definition: giaDup.c:2275
Vec_IntStartNatural
static Vec_Int_t * Vec_IntStartNatural(int nSize)
Definition: bblif.c:192
Gia_ManObj
static Gia_Obj_t * Gia_ManObj(Gia_Man_t *p, int v)
Definition: gia.h:402
Abc_LitNotCond
static int Abc_LitNotCond(int Lit, int c)
Definition: abc_global.h:267
Gia_Obj_t_
Definition: gia.h:75
sat_solver_var_value
static int sat_solver_var_value(sat_solver *s, int v)
Definition: satSolver.h:200
Gia_ManEquivPrintClasses
void Gia_ManEquivPrintClasses(Gia_Man_t *p, int fVerbose, float Mem)
Definition: giaEquiv.c:304
Gia_ManStopP
void Gia_ManStopP(Gia_Man_t **p)
Definition: giaMan.c:177
Gia_ManHasDangling
int Gia_ManHasDangling(Gia_Man_t *p)
Definition: giaUtil.c:1155
Ssc_GiaClassesInit
void Ssc_GiaClassesInit(Gia_Man_t *p)
FUNCTION DECLARATIONS ///.
Definition: sscClass.c:265
Gia_ManRandom
unsigned Gia_ManRandom(int fReset)
FUNCTION DEFINITIONS ///.
Definition: giaUtil.c:49
Ssc_PerformVerification
int Ssc_PerformVerification(Gia_Man_t *p0, Gia_Man_t *p1, Gia_Man_t *pC)
Definition: sscCore.c:223
ABC_PRTP
#define ABC_PRTP(a, t, T)
Definition: abc_global.h:223
Gia_ManForEachCi
#define Gia_ManForEachCi(p, pObj, i)
Definition: gia.h:1016
Gia_ManEquivReduce
Gia_Man_t * Gia_ManEquivReduce(Gia_Man_t *p, int fUseAll, int fDualOut, int fSkipPhase, int fVerbose)
Definition: giaEquiv.c:417
Abc_PrintTime
static void Abc_PrintTime(int level, const char *pStr, abctime time)
Definition: abc_global.h:367
Ssc_GiaSavePiPattern
void Ssc_GiaSavePiPattern(Gia_Man_t *p, Vec_Int_t *vPat)
Definition: sscSim.c:149
Ssc_GiaClassesRefine
int Ssc_GiaClassesRefine(Gia_Man_t *p)
Definition: sscClass.c:279
Gia_ManAndNum
static int Gia_ManAndNum(Gia_Man_t *p)
Definition: gia.h:389
Abc_LitIsCompl
static int Abc_LitIsCompl(int Lit)
Definition: abc_global.h:265
Gia_ObjFanin0
static Gia_Obj_t * Gia_ObjFanin0(Gia_Obj_t *pObj)
Definition: gia.h:454
Gia_Man_t_::nConstrs
int nConstrs
Definition: gia.h:117
Gia_Man_t_::pName
char * pName
Definition: gia.h:97
Vec_IntAlloc
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
Ssc_ManStartSolver
void Ssc_ManStartSolver(Ssc_Man_t *p)
Definition: sscSat.c:261
Ssc_GiaTransferPiPattern
int Ssc_GiaTransferPiPattern(Gia_Man_t *pAig, Gia_Man_t *pCare, Vec_Int_t *vPivot)
Definition: sscSim.c:201
Gia_Man_t_::iPatsPi
int iPatsPi
Definition: gia.h:176
Gia_ObjSetProved
static void Gia_ObjSetProved(Gia_Man_t *p, int Id)
Definition: gia.h:897
Gia_ObjFanin1Copy
static int Gia_ObjFanin1Copy(Gia_Obj_t *pObj)
Definition: gia.h:482
Ssc_ManFindPivotSat
Vec_Int_t * Ssc_ManFindPivotSat(Ssc_Man_t *p)
Definition: sscSat.c:323
Ssc_PerformSweeping
Gia_Man_t * Ssc_PerformSweeping(Gia_Man_t *pAig, Gia_Man_t *pCare, Ssc_Pars_t *pPars)
Definition: sscCore.c:413
Gia_ManDupDfs
Gia_Man_t * Gia_ManDupDfs(Gia_Man_t *p)
Definition: giaDup.c:1238
Gia_ObjSetTravIdCurrent
static void Gia_ObjSetTravIdCurrent(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:531
Ssc_GiaResimulateOneClass
int Ssc_GiaResimulateOneClass(Ssc_Man_t *p, int iRepr, int iObj)
Definition: sscCore.c:196
sat_solver_nvars
int sat_solver_nvars(sat_solver *s)
Definition: satSolver.c:1896
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
Ssc_GiaSimulatePattern_rec
int Ssc_GiaSimulatePattern_rec(Ssc_Man_t *p, Gia_Obj_t *pObj)
Definition: sscCore.c:177
Cec_ManCecSetDefaultParams
void Cec_ManCecSetDefaultParams(Cec_ParCec_t *p)
Definition: cecCore.c:157
Gia_ManHashStart
void Gia_ManHashStart(Gia_Man_t *p)
Definition: giaHash.c:117
Gia_ManStart
Gia_Man_t * Gia_ManStart(int nObjsMax)
DECLARATIONS ///.
Definition: giaMan.c:52
Gia_ManCheckCoPhase
int Gia_ManCheckCoPhase(Gia_Man_t *p)
Definition: giaUtil.c:450
Vec_IntPush
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
Gia_ManFillValue
void Gia_ManFillValue(Gia_Man_t *p)
Definition: giaUtil.c:328
Gia_ManCandNum
static int Gia_ManCandNum(Gia_Man_t *p)
Definition: gia.h:394
Vec_IntFreeP
static void Vec_IntFreeP(Vec_Int_t **p)
Definition: vecInt.h:289
Ssc_PerformSweepingConstr
Gia_Man_t * Ssc_PerformSweepingConstr(Gia_Man_t *p, Ssc_Pars_t *pPars)
Definition: sscCore.c:420
Abc_Print
static void Abc_Print(int level, const char *format,...)
Definition: abc_global.h:313
Cec_ParCec_t_
Definition: cec.h:118
Gia_ObjFanin0Copy
static int Gia_ObjFanin0Copy(Gia_Obj_t *pObj)
Definition: gia.h:481
Gia_ClassForEachObj
#define Gia_ClassForEachObj(p, i, iObj)
Definition: gia.h:931
Gia_ManForEachCand
#define Gia_ManForEachCand(p, pObj, i)
Definition: gia.h:1008
Gia_ManDupAppendShare
void Gia_ManDupAppendShare(Gia_Man_t *p, Gia_Man_t *pTwo)
Definition: giaDup.c:765
sat_solver_nclauses
int sat_solver_nclauses(sat_solver *s)
Definition: satSolver.c:1902
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
Gia_ObjReprObj
static Gia_Obj_t * Gia_ObjReprObj(Gia_Man_t *p, int Id)
Definition: gia.h:886
Gia_ManCiNum
static int Gia_ManCiNum(Gia_Man_t *p)
Definition: gia.h:383
Gia_Obj_t_::fPhase
unsigned fPhase
Definition: gia.h:85
Ssc_ManSetDefaultParams
ABC_NAMESPACE_IMPL_START void Ssc_ManSetDefaultParams(Ssc_Pars_t *p)
DECLARATIONS ///.
Definition: sscCore.c:46
Gia_Obj_t_::fMark0
unsigned fMark0
Definition: gia.h:79
Ssc_GiaEstimateCare
int Ssc_GiaEstimateCare(Gia_Man_t *p, int nWords)
Definition: sscSim.c:351
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
Gia_Man_t_
Definition: gia.h:95
Gia_ManIsNormalized
int Gia_ManIsNormalized(Gia_Man_t *p)
Definition: giaTim.c:109
Gia_ObjIsAnd
static int Gia_ObjIsAnd(Gia_Obj_t *pObj)
Definition: gia.h:422
Gia_ManConst0
static Gia_Obj_t * Gia_ManConst0(Gia_Man_t *p)
Definition: gia.h:400
Cec_ManVerify
int Cec_ManVerify(Gia_Man_t *p, Cec_ParCec_t *pPars)
MACRO DEFINITIONS ///.
Definition: cecCec.c:308
Abc_Lit2Var
static int Abc_Lit2Var(int Lit)
Definition: abc_global.h:264
ABC_CALLOC
#define ABC_CALLOC(type, num)
Definition: abc_global.h:230
l_False
#define l_False
Definition: SolverTypes.h:85
Gia_ObjFanin1
static Gia_Obj_t * Gia_ObjFanin1(Gia_Obj_t *pObj)
Definition: gia.h:455
Ssc_ManCheckEquivalence
int Ssc_ManCheckEquivalence(Ssc_Man_t *p, int iRepr, int iObj, int fCompl)
Definition: sscSat.c:348
Ssc_GiaRandomPiPattern
void Ssc_GiaRandomPiPattern(Gia_Man_t *p, int nWords, Vec_Int_t *vPivot)
Definition: sscSim.c:163
Ssc_GiaSimRound
void Ssc_GiaSimRound(Gia_Man_t *p)
Definition: sscSim.c:247
Gia_Man_t_::pReprs
Gia_Rpr_t * pReprs
Definition: gia.h:121
assert
#define assert(ex)
Definition: util_old.h:213
Gia_Obj_t_::Value
unsigned Value
Definition: gia.h:87
Ssc_ManStop
void Ssc_ManStop(Ssc_Man_t *p)
Definition: sscCore.c:67
Gia_ManIncrementTravId
void Gia_ManIncrementTravId(Gia_Man_t *p)
Definition: giaUtil.c:149
Gia_ManDupLevelized
Gia_Man_t * Gia_ManDupLevelized(Gia_Man_t *p)
Definition: giaDup.c:2812
Gia_ObjFaninC0
static int Gia_ObjFaninC0(Gia_Obj_t *pObj)
Definition: gia.h:451
Vec_IntFree
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
Vec_IntClear
static void Vec_IntClear(Vec_Int_t *p)
Definition: bblif.c:452
abctime
ABC_INT64_T abctime
Definition: abc_global.h:278
Gia_ManCleanup
Gia_Man_t * Gia_ManCleanup(Gia_Man_t *p)
Definition: giaScl.c:84
Abc_UtilStrsav
char * Abc_UtilStrsav(char *s)
Definition: starter.c:47
Gia_ObjFaninId1
static int Gia_ObjFaninId1(Gia_Obj_t *pObj, int ObjId)
Definition: gia.h:461
Gia_ManSetPhasePattern
void Gia_ManSetPhasePattern(Gia_Man_t *p, Vec_Int_t *vCiValues)
Definition: giaUtil.c:386
Gia_ManHashAnd
int Gia_ManHashAnd(Gia_Man_t *p, int iLit0, int iLit1)
Definition: giaHash.c:572
Gia_ManMiter
Gia_Man_t * Gia_ManMiter(Gia_Man_t *pAig0, Gia_Man_t *pAig1, int nInsDup, int fDualOut, int fSeq, int fImplic, int fVerbose)
Definition: giaDup.c:2128
Gia_Obj2Lit
static int Gia_Obj2Lit(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:433
Gia_ObjRepr
static int Gia_ObjRepr(Gia_Man_t *p, int Id)
Definition: gia.h:887
Ssc_GiaClassesCheckPairs
void Ssc_GiaClassesCheckPairs(Gia_Man_t *p, Vec_Int_t *vDisPairs)
Definition: sscClass.c:309
Gia_ObjFaninId0
static int Gia_ObjFaninId0(Gia_Obj_t *pObj, int ObjId)
Definition: gia.h:460
Gia_ObjHasRepr
static int Gia_ObjHasRepr(Gia_Man_t *p, int Id)
Definition: gia.h:891
Gia_ManRegNum
static int Gia_ManRegNum(Gia_Man_t *p)
Definition: gia.h:387