abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
saigGlaCba.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [saigGlaCba.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [Sequential AIG package.]
8 
9  Synopsis [Gate level abstraction.]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - June 20, 2005.]
16 
17  Revision [$Id: saigGlaCba.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "saig.h"
22 #include "sat/bsat/satSolver.h"
23 #include "sat/cnf/cnf.h"
24 
25 ABC_NAMESPACE_IMPL_START
26 
27 
28 ////////////////////////////////////////////////////////////////////////
29 /// DECLARATIONS ///
30 ////////////////////////////////////////////////////////////////////////
31 
32 typedef struct Aig_Gla1Man_t_ Aig_Gla1Man_t;
33 struct Aig_Gla1Man_t_
34 {
35  // user data
36  Aig_Man_t * pAig;
37  int nConfLimit;
38  int nFramesMax;
39  int fVerbose;
40  // unrolling
41  int nFrames;
42  Vec_Int_t * vObj2Vec; // maps obj ID into its vec ID
43  Vec_Int_t * vVec2Var; // maps vec ID into its sat Var (nFrames per vec ID)
44  Vec_Int_t * vVar2Inf; // maps sat Var into its frame and obj ID
45  // abstraction
46  Vec_Int_t * vAssigned; // collects objects whose SAT variables have been created
47  Vec_Int_t * vIncluded; // maps obj ID into its status (0=unused; 1=included in abstraction)
48  // components
49  Vec_Int_t * vPis; // primary inputs
50  Vec_Int_t * vPPis; // pseudo primary inputs
51  Vec_Int_t * vFlops; // flops
52  Vec_Int_t * vNodes; // nodes
53  // CNF computation
54  Vec_Ptr_t * vLeaves;
55  Vec_Ptr_t * vVolume;
56  Vec_Int_t * vCover;
57  Vec_Ptr_t * vObj2Cnf;
58  Vec_Int_t * vLits;
59  // SAT solver
60  sat_solver * pSat;
61  // statistics
62  clock_t timeSat;
63  clock_t timeRef;
64  clock_t timeTotal;
65 };
66 
67 ////////////////////////////////////////////////////////////////////////
68 /// FUNCTION DEFINITIONS ///
69 ////////////////////////////////////////////////////////////////////////
70 
71 /**Function*************************************************************
72 
73  Synopsis [Adds constant to the solver.]
74 
75  Description []
76 
77  SideEffects []
78 
79  SeeAlso []
80 
81 ***********************************************************************/
82 static inline int Aig_Gla1AddConst( sat_solver * pSat, int iVar, int fCompl )
83 {
84  lit Lit = toLitCond( iVar, fCompl );
85  if ( !sat_solver_addclause( pSat, &Lit, &Lit + 1 ) )
86  return 0;
87  return 1;
88 }
89 
90 /**Function*************************************************************
91 
92  Synopsis [Adds buffer to the solver.]
93 
94  Description []
95 
96  SideEffects []
97 
98  SeeAlso []
99 
100 ***********************************************************************/
101 static inline int Aig_Gla1AddBuffer( sat_solver * pSat, int iVar0, int iVar1, int fCompl )
102 {
103  lit Lits[2];
104 
105  Lits[0] = toLitCond( iVar0, 0 );
106  Lits[1] = toLitCond( iVar1, !fCompl );
107  if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) )
108  return 0;
109 
110  Lits[0] = toLitCond( iVar0, 1 );
111  Lits[1] = toLitCond( iVar1, fCompl );
112  if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) )
113  return 0;
114 
115  return 1;
116 }
117 
118 /**Function*************************************************************
119 
120  Synopsis [Adds buffer to the solver.]
121 
122  Description []
123 
124  SideEffects []
125 
126  SeeAlso []
127 
128 ***********************************************************************/
129 static inline int Aig_Gla1AddNode( sat_solver * pSat, int iVar, int iVar0, int iVar1, int fCompl0, int fCompl1 )
130 {
131  lit Lits[3];
132 
133  Lits[0] = toLitCond( iVar, 1 );
134  Lits[1] = toLitCond( iVar0, fCompl0 );
135  if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) )
136  return 0;
137 
138  Lits[0] = toLitCond( iVar, 1 );
139  Lits[1] = toLitCond( iVar1, fCompl1 );
140  if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) )
141  return 0;
142 
143  Lits[0] = toLitCond( iVar, 0 );
144  Lits[1] = toLitCond( iVar0, !fCompl0 );
145  Lits[2] = toLitCond( iVar1, !fCompl1 );
146  if ( !sat_solver_addclause( pSat, Lits, Lits + 3 ) )
147  return 0;
148 
149  return 1;
150 }
151 
152 /**Function*************************************************************
153 
154  Synopsis [Derives abstraction components (PIs, PPIs, flops, nodes).]
155 
156  Description []
157 
158  SideEffects []
159 
160  SeeAlso []
161 
162 ***********************************************************************/
163 void Aig_Gla1CollectAbstr( Aig_Gla1Man_t * p )
164 {
165  Aig_Obj_t * pObj;
166  int i, Entry;
167 /*
168  // make sure every neighbor of included objects is assigned a variable
169  Vec_IntForEachEntry( p->vIncluded, Entry, i )
170  {
171  if ( Entry == 0 )
172  continue;
173  assert( Entry == 1 );
174  pObj = Aig_ManObj( p->pAig, i );
175  if ( Vec_IntFind( p->vAssigned, Aig_ObjId(pObj) ) == -1 )
176  printf( "Aig_Gla1CollectAbstr(): Object not found\n" );
177  if ( Aig_ObjIsNode(pObj) )
178  {
179  if ( Vec_IntFind( p->vAssigned, Aig_ObjFaninId0(pObj) ) == -1 )
180  printf( "Aig_Gla1CollectAbstr(): Node's fanin is not found\n" );
181  if ( Vec_IntFind( p->vAssigned, Aig_ObjFaninId1(pObj) ) == -1 )
182  printf( "Aig_Gla1CollectAbstr(): Node's fanin is not found\n" );
183  }
184  else if ( Saig_ObjIsLo(p->pAig, pObj) )
185  {
186  Aig_Obj_t * pObjLi;
187  pObjLi = Saig_ObjLoToLi(p->pAig, pObj);
188  if ( Vec_IntFind( p->vAssigned, Aig_ObjFaninId0(pObjLi) ) == -1 )
189  printf( "Aig_Gla1CollectAbstr(): Flop's fanin is not found\n" );
190  }
191  else assert( Aig_ObjIsConst1(pObj) );
192  }
193 */
194  Vec_IntClear( p->vPis );
195  Vec_IntClear( p->vPPis );
196  Vec_IntClear( p->vFlops );
197  Vec_IntClear( p->vNodes );
198  Vec_IntForEachEntryReverse( p->vAssigned, Entry, i )
199  {
200  pObj = Aig_ManObj( p->pAig, Entry );
201  if ( Saig_ObjIsPi(p->pAig, pObj) )
202  Vec_IntPush( p->vPis, Aig_ObjId(pObj) );
203  else if ( !Vec_IntEntry(p->vIncluded, Aig_ObjId(pObj)) )
204  Vec_IntPush( p->vPPis, Aig_ObjId(pObj) );
205  else if ( Aig_ObjIsNode(pObj) )
206  Vec_IntPush( p->vNodes, Aig_ObjId(pObj) );
207  else if ( Saig_ObjIsLo(p->pAig, pObj) )
208  Vec_IntPush( p->vFlops, Aig_ObjId(pObj) );
209  else assert( Aig_ObjIsConst1(pObj) );
210  }
211 }
212 
213 /**Function*************************************************************
214 
215  Synopsis [Duplicates the AIG manager recursively.]
216 
217  Description []
218 
219  SideEffects []
220 
221  SeeAlso []
222 
223 ***********************************************************************/
224 void Aig_Gla1DeriveAbs_rec( Aig_Man_t * pNew, Aig_Obj_t * pObj )
225 {
226  if ( pObj->pData )
227  return;
228  assert( Aig_ObjIsNode(pObj) );
229  Aig_Gla1DeriveAbs_rec( pNew, Aig_ObjFanin0(pObj) );
230  Aig_Gla1DeriveAbs_rec( pNew, Aig_ObjFanin1(pObj) );
231  pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
232 }
233 
234 /**Function*************************************************************
235 
236  Synopsis [Derives abstraction.]
237 
238  Description []
239 
240  SideEffects []
241 
242  SeeAlso []
243 
244 ***********************************************************************/
245 Aig_Man_t * Aig_Gla1DeriveAbs( Aig_Gla1Man_t * p )
246 {
247  Aig_Man_t * pNew;
248  Aig_Obj_t * pObj;
249  int i, RetValue;
250  assert( Saig_ManPoNum(p->pAig) == 1 );
251  // start the new manager
252  pNew = Aig_ManStart( 5000 );
253  pNew->pName = Abc_UtilStrsav( p->pAig->pName );
254  // create constant
255  Aig_ManCleanData( p->pAig );
256  Aig_ManConst1(p->pAig)->pData = Aig_ManConst1(pNew);
257  // create PIs
258  Aig_ManForEachObjVec( p->vPis, p->pAig, pObj, i )
259  pObj->pData = Aig_ObjCreateCi(pNew);
260  // create additional PIs
261  Aig_ManForEachObjVec( p->vPPis, p->pAig, pObj, i )
262  pObj->pData = Aig_ObjCreateCi(pNew);
263  // create ROs
264  Aig_ManForEachObjVec( p->vFlops, p->pAig, pObj, i )
265  pObj->pData = Aig_ObjCreateCi(pNew);
266  // create internal nodes
267  Aig_ManForEachObjVec( p->vNodes, p->pAig, pObj, i )
268 // pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
269  Aig_Gla1DeriveAbs_rec( pNew, pObj );
270  // create PO
271  Saig_ManForEachPo( p->pAig, pObj, i )
272  pObj->pData = Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
273  // create RIs
274  Aig_ManForEachObjVec( p->vFlops, p->pAig, pObj, i )
275  {
276  assert( Saig_ObjIsLo(p->pAig, pObj) );
277  pObj = Saig_ObjLoToLi( p->pAig, pObj );
278  pObj->pData = Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
279  }
280  Aig_ManSetRegNum( pNew, Vec_IntSize(p->vFlops) );
281  // clean up
282  RetValue = Aig_ManCleanup( pNew );
283  if ( RetValue > 0 )
284  printf( "Aig_Gla1DeriveAbs(): Internal error! Object count mismatch.\n" );
285  assert( RetValue == 0 );
286  return pNew;
287 }
288 
289 /**Function*************************************************************
290 
291  Synopsis [Finds existing SAT variable or creates a new one.]
292 
293  Description []
294 
295  SideEffects []
296 
297  SeeAlso []
298 
299 ***********************************************************************/
300 static inline int Aig_Gla1FetchVecId( Aig_Gla1Man_t * p, Aig_Obj_t * pObj )
301 {
302  int i, iVecId;
303  iVecId = Vec_IntEntry( p->vObj2Vec, Aig_ObjId(pObj) );
304  if ( iVecId == 0 )
305  {
306  iVecId = Vec_IntSize( p->vVec2Var ) / p->nFrames;
307  for ( i = 0; i < p->nFrames; i++ )
308  Vec_IntPush( p->vVec2Var, 0 );
309  Vec_IntWriteEntry( p->vObj2Vec, Aig_ObjId(pObj), iVecId );
310  Vec_IntPushOrderReverse( p->vAssigned, Aig_ObjId(pObj) );
311  }
312  return iVecId;
313 }
314 
315 /**Function*************************************************************
316 
317  Synopsis [Finds existing SAT variable or creates a new one.]
318 
319  Description []
320 
321  SideEffects []
322 
323  SeeAlso []
324 
325 ***********************************************************************/
326 static inline int Aig_Gla1FetchVar( Aig_Gla1Man_t * p, Aig_Obj_t * pObj, int k )
327 {
328  int iVecId, iSatVar;
329  assert( k < p->nFrames );
330  iVecId = Aig_Gla1FetchVecId( p, pObj );
331  iSatVar = Vec_IntEntry( p->vVec2Var, iVecId * p->nFrames + k );
332  if ( iSatVar == 0 )
333  {
334  iSatVar = Vec_IntSize( p->vVar2Inf ) / 2;
335  Vec_IntPush( p->vVar2Inf, Aig_ObjId(pObj) );
336  Vec_IntPush( p->vVar2Inf, k );
337  Vec_IntWriteEntry( p->vVec2Var, iVecId * p->nFrames + k, iSatVar );
338  sat_solver_setnvars( p->pSat, iSatVar + 1 );
339  }
340  return iSatVar;
341 }
342 
343 /**Function*************************************************************
344 
345  Synopsis [Adds CNF for the given object in the given frame.]
346 
347  Description [Returns 0, if the solver becames UNSAT.]
348 
349  SideEffects []
350 
351  SeeAlso []
352 
353 ***********************************************************************/
354 int Aig_Gla1ObjAddToSolver( Aig_Gla1Man_t * p, Aig_Obj_t * pObj, int k )
355 {
356  if ( k == p->nFrames )
357  {
358  int i, j, nVecIds = Vec_IntSize( p->vVec2Var ) / p->nFrames;
359  Vec_Int_t * vVec2VarNew = Vec_IntAlloc( 4 * nVecIds * p->nFrames );
360  for ( i = 0; i < nVecIds; i++ )
361  {
362  for ( j = 0; j < p->nFrames; j++ )
363  Vec_IntPush( vVec2VarNew, Vec_IntEntry( p->vVec2Var, i * p->nFrames + j ) );
364  for ( j = 0; j < p->nFrames; j++ )
365  Vec_IntPush( vVec2VarNew, i ? 0 : -1 );
366  }
367  Vec_IntFree( p->vVec2Var );
368  p->vVec2Var = vVec2VarNew;
369  p->nFrames *= 2;
370  }
371  assert( k < p->nFrames );
372  assert( Vec_IntEntry(p->vIncluded, Aig_ObjId(pObj)) );
373  if ( Aig_ObjIsConst1(pObj) )
374  return Aig_Gla1AddConst( p->pSat, Aig_Gla1FetchVar(p, pObj, k), 0 );
375  if ( Saig_ObjIsLo(p->pAig, pObj) )
376  {
377  Aig_Obj_t * pObjLi = Saig_ObjLoToLi(p->pAig, pObj);
378  if ( k == 0 )
379  {
380  Aig_Gla1FetchVecId( p, Aig_ObjFanin0(pObjLi) );
381  return Aig_Gla1AddConst( p->pSat, Aig_Gla1FetchVar(p, pObj, k), 1 );
382  }
383  return Aig_Gla1AddBuffer( p->pSat, Aig_Gla1FetchVar(p, pObj, k),
384  Aig_Gla1FetchVar(p, Aig_ObjFanin0(pObjLi), k-1),
385  Aig_ObjFaninC0(pObjLi) );
386  }
387  else
388  {
389  Vec_Int_t * vClauses;
390  int i, Entry;
391  assert( Aig_ObjIsNode(pObj) );
392  if ( p->vObj2Cnf == NULL )
393  return Aig_Gla1AddNode( p->pSat, Aig_Gla1FetchVar(p, pObj, k),
394  Aig_Gla1FetchVar(p, Aig_ObjFanin0(pObj), k),
395  Aig_Gla1FetchVar(p, Aig_ObjFanin1(pObj), k),
396  Aig_ObjFaninC0(pObj), Aig_ObjFaninC1(pObj) );
397  // derive clauses
398  assert( pObj->fMarkA );
399  vClauses = (Vec_Int_t *)Vec_PtrEntry( p->vObj2Cnf, Aig_ObjId(pObj) );
400  if ( vClauses == NULL )
401  {
402  Vec_PtrWriteEntry( p->vObj2Cnf, Aig_ObjId(pObj), (vClauses = Vec_IntAlloc(16)) );
403  Cnf_ComputeClauses( p->pAig, pObj, p->vLeaves, p->vVolume, NULL, p->vCover, vClauses );
404  }
405  // derive variables
406  Cnf_CollectLeaves( pObj, p->vLeaves, 0 );
407  Vec_PtrForEachEntry( Aig_Obj_t *, p->vLeaves, pObj, i )
408  Aig_Gla1FetchVar( p, pObj, k );
409  // translate clauses
410  assert( Vec_IntSize(vClauses) >= 2 );
411  assert( Vec_IntEntry(vClauses, 0) == 0 );
412  Vec_IntForEachEntry( vClauses, Entry, i )
413  {
414  if ( Entry == 0 )
415  {
416  Vec_IntClear( p->vLits );
417  continue;
418  }
419  Vec_IntPush( p->vLits, (Entry & 1) ^ (2 * Aig_Gla1FetchVar(p, Aig_ManObj(p->pAig, Entry >> 1), k)) );
420  if ( i == Vec_IntSize(vClauses) - 1 || Vec_IntEntry(vClauses, i+1) == 0 )
421  {
422  if ( !sat_solver_addclause( p->pSat, Vec_IntArray(p->vLits), Vec_IntArray(p->vLits)+Vec_IntSize(p->vLits) ) )
423  return 0;
424  }
425  }
426  return 1;
427  }
428 }
429 
430 /**Function*************************************************************
431 
432  Synopsis [Returns the array of neighbors.]
433 
434  Description []
435 
436  SideEffects []
437 
438  SeeAlso []
439 
440 ***********************************************************************/
441 void Aig_Gla1CollectAssigned( Aig_Gla1Man_t * p, Vec_Int_t * vGateClasses )
442 {
443  Aig_Obj_t * pObj;
444  int i, Entry;
445  Vec_IntForEachEntryReverse( vGateClasses, Entry, i )
446  {
447  if ( Entry == 0 )
448  continue;
449  assert( Entry == 1 );
450  pObj = Aig_ManObj( p->pAig, i );
451  Aig_Gla1FetchVecId( p, pObj );
452  if ( Aig_ObjIsNode(pObj) )
453  {
454  Aig_Gla1FetchVecId( p, Aig_ObjFanin0(pObj) );
455  Aig_Gla1FetchVecId( p, Aig_ObjFanin1(pObj) );
456  }
457  else if ( Saig_ObjIsLo(p->pAig, pObj) )
458  Aig_Gla1FetchVecId( p, Aig_ObjFanin0(Saig_ObjLoToLi(p->pAig, pObj)) );
459  else assert( Aig_ObjIsConst1(pObj) );
460  }
461 }
462 
463 /**Function*************************************************************
464 
465  Synopsis []
466 
467  Description []
468 
469  SideEffects []
470 
471  SeeAlso []
472 
473 ***********************************************************************/
474 Aig_Gla1Man_t * Aig_Gla1ManStart( Aig_Man_t * pAig, Vec_Int_t * vGateClassesOld, int fNaiveCnf )
475 {
476  Aig_Gla1Man_t * p;
477  int i;
478 
479  p = ABC_CALLOC( Aig_Gla1Man_t, 1 );
480  p->pAig = pAig;
481  p->nFrames = 32;
482 
483  // unrolling
484  p->vObj2Vec = Vec_IntStart( Aig_ManObjNumMax(pAig) );
485  p->vVec2Var = Vec_IntAlloc( 1 << 20 );
486  p->vVar2Inf = Vec_IntAlloc( 1 << 20 );
487 
488  // skip first vector ID
489  for ( i = 0; i < p->nFrames; i++ )
490  Vec_IntPush( p->vVec2Var, -1 );
491  // skip first SAT variable
492  Vec_IntPush( p->vVar2Inf, -1 );
493  Vec_IntPush( p->vVar2Inf, -1 );
494 
495  // abstraction
496  p->vAssigned = Vec_IntAlloc( 1000 );
497  if ( vGateClassesOld )
498  {
499  p->vIncluded = Vec_IntDup( vGateClassesOld );
500  Aig_Gla1CollectAssigned( p, vGateClassesOld );
501  assert( fNaiveCnf );
502  }
503  else
504  p->vIncluded = Vec_IntStart( Aig_ManObjNumMax(pAig) );
505 
506  // components
507  p->vPis = Vec_IntAlloc( 1000 );
508  p->vPPis = Vec_IntAlloc( 1000 );
509  p->vFlops = Vec_IntAlloc( 1000 );
510  p->vNodes = Vec_IntAlloc( 1000 );
511 
512  // CNF computation
513  if ( !fNaiveCnf )
514  {
515  p->vLeaves = Vec_PtrAlloc( 100 );
516  p->vVolume = Vec_PtrAlloc( 100 );
517  p->vCover = Vec_IntAlloc( 1 << 16 );
518  p->vObj2Cnf = Vec_PtrStart( Aig_ManObjNumMax(pAig) );
519  p->vLits = Vec_IntAlloc( 100 );
520  Cnf_DeriveFastMark( pAig );
521  }
522 
523  // start the SAT solver
524  p->pSat = sat_solver_new();
525  sat_solver_setnvars( p->pSat, 256 );
526  return p;
527 }
528 
529 
530 /**Function*************************************************************
531 
532  Synopsis []
533 
534  Description []
535 
536  SideEffects []
537 
538  SeeAlso []
539 
540 ***********************************************************************/
541 void Aig_Gla1ManStop( Aig_Gla1Man_t * p )
542 {
543  Vec_IntFreeP( &p->vObj2Vec );
544  Vec_IntFreeP( &p->vVec2Var );
545  Vec_IntFreeP( &p->vVar2Inf );
546 
547  Vec_IntFreeP( &p->vAssigned );
548  Vec_IntFreeP( &p->vIncluded );
549 
550  Vec_IntFreeP( &p->vPis );
551  Vec_IntFreeP( &p->vPPis );
552  Vec_IntFreeP( &p->vFlops );
553  Vec_IntFreeP( &p->vNodes );
554 
555  if ( p->vObj2Cnf )
556  {
557  Vec_PtrFreeP( &p->vLeaves );
558  Vec_PtrFreeP( &p->vVolume );
559  Vec_IntFreeP( &p->vCover );
560  Vec_VecFreeP( (Vec_Vec_t **)&p->vObj2Cnf );
561  Vec_IntFreeP( &p->vLits );
562  Aig_ManCleanMarkA( p->pAig );
563  }
564 
565  if ( p->pSat )
566  sat_solver_delete( p->pSat );
567  ABC_FREE( p );
568 }
569 
570 /**Function*************************************************************
571 
572  Synopsis []
573 
574  Description []
575 
576  SideEffects []
577 
578  SeeAlso []
579 
580 ***********************************************************************/
581 Abc_Cex_t * Aig_Gla1DeriveCex( Aig_Gla1Man_t * p, int iFrame )
582 {
583  Abc_Cex_t * pCex;
584  Aig_Obj_t * pObj;
585  int i, f, iVecId, iSatId;
586  pCex = Abc_CexAlloc( Vec_IntSize(p->vFlops), Vec_IntSize(p->vPis) + Vec_IntSize(p->vPPis), iFrame+1 );
587  pCex->iFrame = iFrame;
588  Aig_ManForEachObjVec( p->vPis, p->pAig, pObj, i )
589  {
590  iVecId = Vec_IntEntry( p->vObj2Vec, Aig_ObjId(pObj) );
591  assert( iVecId > 0 );
592  for ( f = 0; f <= iFrame; f++ )
593  {
594  iSatId = Vec_IntEntry( p->vVec2Var, iVecId * p->nFrames + f );
595  if ( iSatId == 0 )
596  continue;
597  assert( iSatId > 0 );
598  if ( sat_solver_var_value(p->pSat, iSatId) )
599  Abc_InfoSetBit( pCex->pData, pCex->nRegs + f * pCex->nPis + i );
600  }
601  }
602  Aig_ManForEachObjVec( p->vPPis, p->pAig, pObj, i )
603  {
604  iVecId = Vec_IntEntry( p->vObj2Vec, Aig_ObjId(pObj) );
605  assert( iVecId > 0 );
606  for ( f = 0; f <= iFrame; f++ )
607  {
608  iSatId = Vec_IntEntry( p->vVec2Var, iVecId * p->nFrames + f );
609  if ( iSatId == 0 )
610  continue;
611  assert( iSatId > 0 );
612  if ( sat_solver_var_value(p->pSat, iSatId) )
613  Abc_InfoSetBit( pCex->pData, pCex->nRegs + f * pCex->nPis + Vec_IntSize(p->vPis) + i );
614  }
615  }
616  return pCex;
617 }
618 
619 /**Function*************************************************************
620 
621  Synopsis [Prints current abstraction statistics.]
622 
623  Description []
624 
625  SideEffects []
626 
627  SeeAlso []
628 
629 ***********************************************************************/
630 void Aig_Gla1PrintAbstr( Aig_Gla1Man_t * p, int f, int r, int v, int c )
631 {
632  if ( r == 0 )
633  printf( "== %3d ==", f );
634  else
635  printf( " " );
636  printf( " %4d PI =%6d PPI =%6d FF =%6d Node =%6d Var =%7d Conf =%6d\n",
637  r, Vec_IntSize(p->vPis), Vec_IntSize(p->vPPis), Vec_IntSize(p->vFlops), Vec_IntSize(p->vNodes), v, c );
638 }
639 
640 /**Function*************************************************************
641 
642  Synopsis [Prints current abstraction statistics.]
643 
644  Description []
645 
646  SideEffects []
647 
648  SeeAlso []
649 
650 ***********************************************************************/
651 void Aig_Gla1ExtendIncluded( Aig_Gla1Man_t * p )
652 {
653  Aig_Obj_t * pObj;
654  int i, k;
655  Aig_ManForEachNode( p->pAig, pObj, i )
656  {
657  if ( !Vec_IntEntry( p->vIncluded, i ) )
658  continue;
659  Cnf_ComputeClauses( p->pAig, pObj, p->vLeaves, p->vVolume, NULL, p->vCover, p->vNodes );
660  Vec_PtrForEachEntry( Aig_Obj_t *, p->vVolume, pObj, k )
661  {
662  assert( Aig_ObjId(pObj) <= i );
663  Vec_IntWriteEntry( p->vIncluded, Aig_ObjId(pObj), 1 );
664  }
665  }
666 }
667 
668 /**Function*************************************************************
669 
670  Synopsis [Performs gate-level localization abstraction.]
671 
672  Description [Returns array of objects included in the abstraction. This array
673  may contain only const1, flop outputs, and internal nodes, that is, objects
674  that should have clauses added to the SAT solver.]
675 
676  SideEffects []
677 
678  SeeAlso []
679 
680 ***********************************************************************/
681 Vec_Int_t * Aig_Gla1ManPerform( Aig_Man_t * pAig, Vec_Int_t * vGateClassesOld, int nStart, int nFramesMax, int nConfLimit, int TimeLimit, int fNaiveCnf, int fVerbose, int * piFrame )
682 {
683  Vec_Int_t * vResult = NULL;
684  Aig_Gla1Man_t * p;
685  Aig_Man_t * pAbs;
686  Aig_Obj_t * pObj;
687  Abc_Cex_t * pCex;
688  Vec_Int_t * vPPiRefine;
689  int f, g, r, i, iSatVar, Lit, Entry, RetValue;
690  int nConfBef, nConfAft;
691  clock_t clk, clkTotal = clock();
692  clock_t nTimeToStop = TimeLimit ? TimeLimit * CLOCKS_PER_SEC + clock(): 0;
693  assert( Saig_ManPoNum(pAig) == 1 );
694 
695  if ( nFramesMax == 0 )
696  nFramesMax = ABC_INFINITY;
697 
698  if ( fVerbose )
699  {
700  if ( TimeLimit )
701  printf( "Abstracting from frame %d to frame %d with timeout %d sec.\n", nStart, nFramesMax, TimeLimit );
702  else
703  printf( "Abstracting from frame %d to frame %d with no timeout.\n", nStart, nFramesMax );
704  }
705 
706  // start the solver
707  p = Aig_Gla1ManStart( pAig, vGateClassesOld, fNaiveCnf );
708  p->nFramesMax = nFramesMax;
709  p->nConfLimit = nConfLimit;
710  p->fVerbose = fVerbose;
711 
712  // include constant node
713  Vec_IntWriteEntry( p->vIncluded, 0, 1 );
714  Aig_Gla1FetchVecId( p, Aig_ManConst1(pAig) );
715 
716  // set runtime limit
717  if ( TimeLimit )
718  sat_solver_set_runtime_limit( p->pSat, nTimeToStop );
719 
720  // iterate over the timeframes
721  for ( f = 0; f < nFramesMax; f++ )
722  {
723  // initialize abstraction in this timeframe
724  Aig_ManForEachObjVec( p->vAssigned, pAig, pObj, i )
725  if ( Vec_IntEntry(p->vIncluded, Aig_ObjId(pObj)) )
726  if ( !Aig_Gla1ObjAddToSolver( p, pObj, f ) )
727  printf( "Error! SAT solver became UNSAT.\n" );
728 
729  // skip checking if we are not supposed to
730  if ( f < nStart )
731  continue;
732 
733  // create output literal to represent property failure
734  pObj = Aig_ManCo( pAig, 0 );
735  iSatVar = Aig_Gla1FetchVar( p, Aig_ObjFanin0(pObj), f );
736  Lit = toLitCond( iSatVar, Aig_ObjFaninC0(pObj) );
737 
738  // try solving the abstraction
739  Aig_Gla1CollectAbstr( p );
740  for ( r = 0; r < ABC_INFINITY; r++ )
741  {
742  // try to find a counter-example
743  clk = clock();
744  nConfBef = p->pSat->stats.conflicts;
745  RetValue = sat_solver_solve( p->pSat, &Lit, &Lit + 1,
746  (ABC_INT64_T)nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
747  nConfAft = p->pSat->stats.conflicts;
748  p->timeSat += clock() - clk;
749  if ( RetValue != l_True )
750  {
751  if ( fVerbose )
752  {
753  if ( r == 0 )
754  printf( "== %3d ==", f );
755  else
756  printf( " " );
757  if ( TimeLimit && clock() > nTimeToStop )
758  printf( " SAT solver timed out after %d seconds.\n", TimeLimit );
759  else if ( RetValue != l_False )
760  printf( " SAT solver returned UNDECIDED after %5d conflicts.\n", nConfAft - nConfBef );
761  else
762  {
763  printf( " SAT solver returned UNSAT after %5d conflicts. ", nConfAft - nConfBef );
764  Abc_PrintTime( 1, "Total time", clock() - clkTotal );
765  }
766  }
767  break;
768  }
769  clk = clock();
770  // derive abstraction
771  pAbs = Aig_Gla1DeriveAbs( p );
772  // derive counter-example
773  pCex = Aig_Gla1DeriveCex( p, f );
774  // verify the counter-example
775  RetValue = Saig_ManVerifyCex( pAbs, pCex );
776  if ( RetValue == 0 )
777  printf( "Error! CEX is invalid.\n" );
778  // perform refinement
779  vPPiRefine = Saig_ManCbaFilterInputs( pAbs, Vec_IntSize(p->vPis), pCex, 0 );
780  Vec_IntForEachEntry( vPPiRefine, Entry, i )
781  {
782  pObj = Aig_ManObj( pAig, Vec_IntEntry(p->vPPis, Entry) );
783  assert( Aig_ObjIsNode(pObj) || Saig_ObjIsLo(p->pAig, pObj) );
784  assert( Vec_IntEntry( p->vIncluded, Aig_ObjId(pObj) ) == 0 );
785  Vec_IntWriteEntry( p->vIncluded, Aig_ObjId(pObj), 1 );
786  for ( g = 0; g <= f; g++ )
787  if ( !Aig_Gla1ObjAddToSolver( p, pObj, g ) )
788  printf( "Error! SAT solver became UNSAT.\n" );
789  }
790  if ( Vec_IntSize(vPPiRefine) == 0 )
791  {
792  Vec_IntFreeP( &p->vIncluded );
793  Vec_IntFree( vPPiRefine );
794  Aig_ManStop( pAbs );
795  Abc_CexFree( pCex );
796  break;
797  }
798  Vec_IntFree( vPPiRefine );
799  Aig_ManStop( pAbs );
800  Abc_CexFree( pCex );
801  p->timeRef += clock() - clk;
802 
803  // prepare abstraction
804  Aig_Gla1CollectAbstr( p );
805  if ( fVerbose )
806  Aig_Gla1PrintAbstr( p, f, r, p->pSat->size, nConfAft - nConfBef );
807  }
808  if ( RetValue != l_False )
809  break;
810  }
811  p->timeTotal = clock() - clkTotal;
812  if ( f == nFramesMax )
813  printf( "Finished %d frames without exceeding conflict limit (%d).\n", f, nConfLimit );
814  else if ( p->vIncluded == NULL )
815  printf( "The problem is SAT in frame %d. The CEX is currently not produced.\n", f );
816  else
817  printf( "Ran out of conflict limit (%d) at frame %d.\n", nConfLimit, f );
818  *piFrame = f;
819  // print stats
820  if ( fVerbose )
821  {
822  ABC_PRTP( "Sat ", p->timeSat, p->timeTotal );
823  ABC_PRTP( "Ref ", p->timeRef, p->timeTotal );
824  ABC_PRTP( "Total ", p->timeTotal, p->timeTotal );
825  }
826  // prepare return value
827  if ( !fNaiveCnf && p->vIncluded )
828  Aig_Gla1ExtendIncluded( p );
829  vResult = p->vIncluded; p->vIncluded = NULL;
830  Aig_Gla1ManStop( p );
831  return vResult;
832 }
833 
834 ////////////////////////////////////////////////////////////////////////
835 /// END OF FILE ///
836 ////////////////////////////////////////////////////////////////////////
837 
838 
839 ABC_NAMESPACE_IMPL_END
840 
Aig_Gla1ManStop
void Aig_Gla1ManStop(Aig_Gla1Man_t *p)
Definition: saigGlaCba.c:541
Aig_ObjCreateCo
Aig_Obj_t * Aig_ObjCreateCo(Aig_Man_t *p, Aig_Obj_t *pDriver)
Definition: aigObj.c:66
sat_solver_set_runtime_limit
static abctime sat_solver_set_runtime_limit(sat_solver *s, abctime Limit)
Definition: satSolver.h:233
Vec_IntArray
static int * Vec_IntArray(Vec_Int_t *p)
Definition: vecInt.h:328
Aig_Gla1Man_t_::vIncluded
Vec_Int_t * vIncluded
Definition: saigGlaCba.c:47
Vec_PtrStart
static Vec_Ptr_t * Vec_PtrStart(int nSize)
Definition: vecPtr.h:106
Aig_Gla1Man_t_::fVerbose
int fVerbose
Definition: saigGlaCba.c:39
Cnf_DeriveFastMark
void Cnf_DeriveFastMark(Aig_Man_t *p)
Definition: cnfFast.c:297
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
Aig_Gla1Man_t_::vPPis
Vec_Int_t * vPPis
Definition: saigGlaCba.c:50
Vec_IntDup
static Vec_Int_t * Vec_IntDup(Vec_Int_t *pVec)
Definition: vecInt.h:214
Vec_Vec_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Vec_t_ Vec_Vec_t
INCLUDES ///.
Definition: vecVec.h:42
Saig_ManPoNum
static int Saig_ManPoNum(Aig_Man_t *p)
Definition: saig.h:74
Saig_ObjIsLo
static int Saig_ObjIsLo(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: saig.h:84
Aig_ManForEachObjVec
#define Aig_ManForEachObjVec(vIds, p, pObj, i)
Definition: aig.h:408
Aig_Man_t
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition: aig.h:50
Aig_Gla1Man_t_::vCover
Vec_Int_t * vCover
Definition: saigGlaCba.c:56
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
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
Aig_ManStop
void Aig_ManStop(Aig_Man_t *p)
Definition: aigMan.c:187
Abc_CexAlloc
ABC_NAMESPACE_IMPL_START Abc_Cex_t * Abc_CexAlloc(int nRegs, int nRealPis, int nFrames)
DECLARATIONS ///.
Definition: utilCex.c:51
Aig_Gla1Man_t_::nConfLimit
int nConfLimit
Definition: saigGlaCba.c:37
Saig_ObjLoToLi
static Aig_Obj_t * Saig_ObjLoToLi(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: saig.h:86
Saig_ManVerifyCex
int Saig_ManVerifyCex(Aig_Man_t *pAig, Abc_Cex_t *p)
Definition: saigDup.c:279
Aig_Gla1Man_t_::vObj2Cnf
Vec_Ptr_t * vObj2Cnf
Definition: saigGlaCba.c:57
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
Aig_Gla1CollectAbstr
void Aig_Gla1CollectAbstr(Aig_Gla1Man_t *p)
Definition: saigGlaCba.c:163
Aig_Obj_t_::pData
void * pData
Definition: aig.h:87
Aig_Gla1Man_t_::vVec2Var
Vec_Int_t * vVec2Var
Definition: saigGlaCba.c:43
sat_solver_delete
void sat_solver_delete(sat_solver *s)
Definition: satSolver.c:1141
Aig_ObjFanin0
static Aig_Obj_t * Aig_ObjFanin0(Aig_Obj_t *pObj)
Definition: aig.h:308
Aig_ManStart
Aig_Man_t * Aig_ManStart(int nNodesMax)
DECLARATIONS ///.
Definition: aigMan.c:47
Vec_IntForEachEntryReverse
#define Vec_IntForEachEntryReverse(vVec, pEntry, i)
Definition: vecInt.h:62
Aig_Gla1Man_t_::pAig
Aig_Man_t * pAig
Definition: saigGlaCba.c:36
Aig_ObjCreateCi
Aig_Obj_t * Aig_ObjCreateCi(Aig_Man_t *p)
DECLARATIONS ///.
Definition: aigObj.c:45
Aig_Obj_t_::fMarkA
unsigned int fMarkA
Definition: aig.h:79
l_True
#define l_True
Definition: SolverTypes.h:84
Aig_Gla1Man_t_::vLits
Vec_Int_t * vLits
Definition: saigGlaCba.c:58
Aig_ManObj
static Aig_Obj_t * Aig_ManObj(Aig_Man_t *p, int i)
Definition: aig.h:270
Aig_Gla1Man_t_::timeSat
clock_t timeSat
Definition: saigGlaCba.c:62
Aig_Gla1DeriveCex
Abc_Cex_t * Aig_Gla1DeriveCex(Aig_Gla1Man_t *p, int iFrame)
Definition: saigGlaCba.c:581
Aig_Gla1ExtendIncluded
void Aig_Gla1ExtendIncluded(Aig_Gla1Man_t *p)
Definition: saigGlaCba.c:651
Cnf_ComputeClauses
void Cnf_ComputeClauses(Aig_Man_t *p, Aig_Obj_t *pRoot, Vec_Ptr_t *vLeaves, Vec_Ptr_t *vNodes, Vec_Int_t *vMap, Vec_Int_t *vCover, Vec_Int_t *vClauses)
Definition: cnfFast.c:198
Aig_Gla1Man_t_::nFramesMax
int nFramesMax
Definition: saigGlaCba.c:38
Aig_Gla1AddNode
static int Aig_Gla1AddNode(sat_solver *pSat, int iVar, int iVar0, int iVar1, int fCompl0, int fCompl1)
Definition: saigGlaCba.c:129
Aig_ObjFanin1
static Aig_Obj_t * Aig_ObjFanin1(Aig_Obj_t *pObj)
Definition: aig.h:309
sat_solver_var_value
static int sat_solver_var_value(sat_solver *s, int v)
Definition: satSolver.h:200
Aig_Gla1FetchVar
static int Aig_Gla1FetchVar(Aig_Gla1Man_t *p, Aig_Obj_t *pObj, int k)
Definition: saigGlaCba.c:326
lit
int lit
Definition: satVec.h:130
Aig_And
Aig_Obj_t * Aig_And(Aig_Man_t *p, Aig_Obj_t *p0, Aig_Obj_t *p1)
Definition: aigOper.c:104
Aig_Gla1Man_t_::vAssigned
Vec_Int_t * vAssigned
Definition: saigGlaCba.c:46
Aig_Gla1ManPerform
Vec_Int_t * Aig_Gla1ManPerform(Aig_Man_t *pAig, Vec_Int_t *vGateClassesOld, int nStart, int nFramesMax, int nConfLimit, int TimeLimit, int fNaiveCnf, int fVerbose, int *piFrame)
Definition: saigGlaCba.c:681
ABC_PRTP
#define ABC_PRTP(a, t, T)
Definition: abc_global.h:223
Aig_Gla1ObjAddToSolver
int Aig_Gla1ObjAddToSolver(Aig_Gla1Man_t *p, Aig_Obj_t *pObj, int k)
Definition: saigGlaCba.c:354
Abc_PrintTime
static void Abc_PrintTime(int level, const char *pStr, abctime time)
Definition: abc_global.h:367
Aig_ObjIsNode
static int Aig_ObjIsNode(Aig_Obj_t *pObj)
Definition: aig.h:280
Vec_IntWriteEntry
static void Vec_IntWriteEntry(Vec_Int_t *p, int i, int Entry)
Definition: bblif.c:285
Vec_IntStart
static Vec_Int_t * Vec_IntStart(int nSize)
Definition: bblif.c:172
Aig_Gla1AddConst
static int Aig_Gla1AddConst(sat_solver *pSat, int iVar, int fCompl)
FUNCTION DEFINITIONS ///.
Definition: saigGlaCba.c:82
Aig_ManForEachNode
#define Aig_ManForEachNode(p, pObj, i)
Definition: aig.h:413
Vec_IntAlloc
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
Aig_Gla1Man_t_::vObj2Vec
Vec_Int_t * vObj2Vec
Definition: saigGlaCba.c:42
Aig_ManSetRegNum
void Aig_ManSetRegNum(Aig_Man_t *p, int nRegs)
Definition: aigMan.c:438
Aig_Gla1FetchVecId
static int Aig_Gla1FetchVecId(Aig_Gla1Man_t *p, Aig_Obj_t *pObj)
Definition: saigGlaCba.c:300
Aig_Gla1Man_t_::vLeaves
Vec_Ptr_t * vLeaves
Definition: saigGlaCba.c:54
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
Vec_IntEntry
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
Aig_ObjIsConst1
static int Aig_ObjIsConst1(Aig_Obj_t *pObj)
Definition: aig.h:274
Aig_ObjChild1Copy
static Aig_Obj_t * Aig_ObjChild1Copy(Aig_Obj_t *pObj)
Definition: aig.h:313
Aig_Gla1Man_t_
Definition: saigGlaCba.c:33
Aig_Obj_t_
Definition: aig.h:69
Vec_IntPush
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
Cnf_CollectLeaves
void Cnf_CollectLeaves(Aig_Obj_t *pRoot, Vec_Ptr_t *vSuper, int fStopCompl)
Definition: cnfFast.c:76
Aig_ObjChild0Copy
static Aig_Obj_t * Aig_ObjChild0Copy(Aig_Obj_t *pObj)
Definition: aig.h:312
Vec_IntFreeP
static void Vec_IntFreeP(Vec_Int_t **p)
Definition: vecInt.h:289
Aig_Gla1Man_t_::vVar2Inf
Vec_Int_t * vVar2Inf
Definition: saigGlaCba.c:44
Aig_Gla1Man_t_::vNodes
Vec_Int_t * vNodes
Definition: saigGlaCba.c:52
Aig_Gla1DeriveAbs
Aig_Man_t * Aig_Gla1DeriveAbs(Aig_Gla1Man_t *p)
Definition: saigGlaCba.c:245
Aig_Gla1Man_t_::pSat
sat_solver * pSat
Definition: saigGlaCba.c:60
Aig_ObjFaninC0
static int Aig_ObjFaninC0(Aig_Obj_t *pObj)
Definition: aig.h:306
Vec_PtrWriteEntry
static void Vec_PtrWriteEntry(Vec_Ptr_t *p, int i, void *Entry)
Definition: vecPtr.h:396
Aig_ManObjNumMax
static int Aig_ManObjNumMax(Aig_Man_t *p)
Definition: aig.h:259
Aig_ManConst1
static Aig_Obj_t * Aig_ManConst1(Aig_Man_t *p)
Definition: aig.h:264
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
Vec_PtrEntry
static void * Vec_PtrEntry(Vec_Ptr_t *p, int i)
Definition: vecPtr.h:362
Abc_InfoSetBit
static void Abc_InfoSetBit(unsigned *p, int i)
Definition: abc_global.h:259
Aig_ManCo
static Aig_Obj_t * Aig_ManCo(Aig_Man_t *p, int i)
Definition: aig.h:267
Aig_Gla1Man_t_::vVolume
Vec_Ptr_t * vVolume
Definition: saigGlaCba.c:55
sat_solver_new
sat_solver * sat_solver_new(void)
Definition: satSolver.c:1001
Vec_IntSize
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
Vec_IntPushOrderReverse
static void Vec_IntPushOrderReverse(Vec_Int_t *p, int Entry)
Definition: vecInt.h:781
Aig_Gla1ManStart
Aig_Gla1Man_t * Aig_Gla1ManStart(Aig_Man_t *pAig, Vec_Int_t *vGateClassesOld, int fNaiveCnf)
Definition: saigGlaCba.c:474
Vec_PtrAlloc
static Vec_Ptr_t * Vec_PtrAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: vecPtr.h:83
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
Aig_Gla1PrintAbstr
void Aig_Gla1PrintAbstr(Aig_Gla1Man_t *p, int f, int r, int v, int c)
Definition: saigGlaCba.c:630
Saig_ManCbaFilterInputs
Vec_Int_t * Saig_ManCbaFilterInputs(Aig_Man_t *pAig, int iFirstFlopPi, Abc_Cex_t *pCex, int fVerbose)
Definition: absOldCex.c:785
Aig_Gla1CollectAssigned
void Aig_Gla1CollectAssigned(Aig_Gla1Man_t *p, Vec_Int_t *vGateClasses)
Definition: saigGlaCba.c:441
Aig_ManCleanMarkA
void Aig_ManCleanMarkA(Aig_Man_t *p)
Definition: aigUtil.c:148
ABC_CALLOC
#define ABC_CALLOC(type, num)
Definition: abc_global.h:230
Aig_Gla1Man_t_::timeTotal
clock_t timeTotal
Definition: saigGlaCba.c:64
l_False
#define l_False
Definition: SolverTypes.h:85
Aig_Gla1Man_t
typedefABC_NAMESPACE_IMPL_START struct Aig_Gla1Man_t_ Aig_Gla1Man_t
DECLARATIONS ///.
Definition: saigGlaCba.c:32
Vec_PtrFreeP
static void Vec_PtrFreeP(Vec_Ptr_t **p)
Definition: vecPtr.h:240
Aig_Gla1Man_t_::nFrames
int nFrames
Definition: saigGlaCba.c:41
Aig_ObjFaninC1
static int Aig_ObjFaninC1(Aig_Obj_t *pObj)
Definition: aig.h:307
ABC_INFINITY
#define ABC_INFINITY
MACRO DEFINITIONS ///.
Definition: abc_global.h:216
sat_solver_t
Definition: satSolver.h:91
Vec_VecFreeP
static void Vec_VecFreeP(Vec_Vec_t **p)
Definition: vecVec.h:367
Saig_ManForEachPo
#define Saig_ManForEachPo(p, pObj, i)
Definition: saig.h:93
Aig_ObjId
static int Aig_ObjId(Aig_Obj_t *pObj)
Definition: aig.h:286
assert
#define assert(ex)
Definition: util_old.h:213
Abc_Cex_t
typedefABC_NAMESPACE_HEADER_START struct Abc_Cex_t_ Abc_Cex_t
INCLUDES ///.
Definition: utilCex.h:39
Aig_Gla1DeriveAbs_rec
void Aig_Gla1DeriveAbs_rec(Aig_Man_t *pNew, Aig_Obj_t *pObj)
Definition: saigGlaCba.c:224
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
Abc_CexFree
void Abc_CexFree(Abc_Cex_t *p)
Definition: utilCex.c:371
Vec_IntClear
static void Vec_IntClear(Vec_Int_t *p)
Definition: bblif.c:452
Aig_Gla1Man_t_::vPis
Vec_Int_t * vPis
Definition: saigGlaCba.c:49
Abc_UtilStrsav
char * Abc_UtilStrsav(char *s)
Definition: starter.c:47
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
Aig_Gla1Man_t_::vFlops
Vec_Int_t * vFlops
Definition: saigGlaCba.c:51
Aig_ManCleanData
void Aig_ManCleanData(Aig_Man_t *p)
Definition: aigUtil.c:205
Saig_ObjIsPi
static int Saig_ObjIsPi(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: saig.h:82
Aig_ManCleanup
int Aig_ManCleanup(Aig_Man_t *p)
Definition: aigMan.c:265
Aig_Gla1Man_t_::timeRef
clock_t timeRef
Definition: saigGlaCba.c:63
Aig_Gla1AddBuffer
static int Aig_Gla1AddBuffer(sat_solver *pSat, int iVar0, int iVar1, int fCompl)
Definition: saigGlaCba.c:101