abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
absVta.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [absVta.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [Abstraction package.]
8 
9  Synopsis [Variable time-frame 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: absVta.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "sat/bsat/satSolver2.h"
22 #include "base/main/main.h"
23 #include "abs.h"
24 
25 ABC_NAMESPACE_IMPL_START
26 
27 #define VTA_LARGE 0xFFFFFFF
28 
29 ////////////////////////////////////////////////////////////////////////
30 /// DECLARATIONS ///
31 ////////////////////////////////////////////////////////////////////////
32 
33 typedef struct Vta_Obj_t_ Vta_Obj_t; // object
34 struct Vta_Obj_t_
35 {
36  int iObj;
37  int iFrame;
38  int iNext;
39  unsigned Prio : 28; // related to VTA_LARGE
40  unsigned Value : 2;
41  unsigned fAdded : 1;
42  unsigned fVisit : 1;
43 };
44 
45 typedef struct Vta_Man_t_ Vta_Man_t; // manager
46 struct Vta_Man_t_
47 {
48  // user data
49  Gia_Man_t * pGia; // AIG manager
50  Abs_Par_t * pPars; // parameters
51  // internal data
52  int nObjs; // the number of objects
53  int nObjsAlloc; // the number of objects allocated
54  int nBins; // number of hash table entries
55  int * pBins; // hash table bins
56  Vta_Obj_t * pObjs; // storage for objects
57  Vec_Int_t * vOrder; // objects in DPS order
58  // abstraction
59  int nObjBits; // the number of bits to represent objects
60  unsigned nObjMask; // object mask
61  Vec_Ptr_t * vFrames; // start abstraction for each frame
62  int nWords; // the number of words in the record
63  int nCexes; // the number of CEXes
64  int nObjAdded; // objects added to the abstraction
65  Vec_Int_t * vSeens; // seen objects
66  Vec_Bit_t * vSeenGla; // seen objects in all frames
67  int nSeenGla; // seen objects in all frames
68  int nSeenAll; // seen objects in all frames
69  // other data
70  Vec_Ptr_t * vCores; // unsat core for each frame
71  sat_solver2 * pSat; // incremental SAT solver
72  Vec_Int_t * vAddedNew; // the IDs of variables added to the solver
73  // statistics
74  abctime timeSat;
75  abctime timeUnsat;
76  abctime timeCex;
77  abctime timeOther;
78 };
79 
80 
81 // ternary simulation
82 
83 #define VTA_VAR0 1
84 #define VTA_VAR1 2
85 #define VTA_VARX 3
86 
87 static inline int Vta_ValIs0( Vta_Obj_t * pThis, int fCompl )
88 {
89  if ( pThis->Value == VTA_VAR1 && fCompl )
90  return 1;
91  if ( pThis->Value == VTA_VAR0 && !fCompl )
92  return 1;
93  return 0;
94 }
95 static inline int Vta_ValIs1( Vta_Obj_t * pThis, int fCompl )
96 {
97  if ( pThis->Value == VTA_VAR0 && fCompl )
98  return 1;
99  if ( pThis->Value == VTA_VAR1 && !fCompl )
100  return 1;
101  return 0;
102 }
103 
104 static inline Vta_Obj_t * Vta_ManObj( Vta_Man_t * p, int i ) { assert( i >= 0 && i < p->nObjs ); return i ? p->pObjs + i : NULL; }
105 static inline int Vta_ObjId( Vta_Man_t * p, Vta_Obj_t * pObj ) { assert( pObj > p->pObjs && pObj < p->pObjs + p->nObjs ); return pObj - p->pObjs; }
106 
107 #define Vta_ManForEachObj( p, pObj, i ) \
108  for ( i = 1; (i < p->nObjs) && ((pObj) = Vta_ManObj(p, i)); i++ )
109 #define Vta_ManForEachObjObj( p, pObjVta, pObjGia, i ) \
110  for ( i = 1; (i < p->nObjs) && ((pObjVta) = Vta_ManObj(p, i)) && ((pObjGia) = Gia_ManObj(p->pGia, pObjVta->iObj)); i++ )
111 #define Vta_ManForEachObjObjReverse( p, pObjVta, pObjGia, i ) \
112  for ( i = Vec_IntSize(vVec) - 1; (i >= 1) && ((pObjVta) = Vta_ManObj(p, i)) && ((pObjGia) = Gia_ManObj(p->pGia, pObjVta->iObj)); i++ )
113 
114 #define Vta_ManForEachObjVec( vVec, p, pObj, i ) \
115  for ( i = 0; (i < Vec_IntSize(vVec)) && ((pObj) = Vta_ManObj(p, Vec_IntEntry(vVec,i))); i++ )
116 #define Vta_ManForEachObjVecReverse( vVec, p, pObj, i ) \
117  for ( i = Vec_IntSize(vVec) - 1; (i >= 0) && ((pObj) = Vta_ManObj(p, Vec_IntEntry(vVec,i))); i-- )
118 
119 #define Vta_ManForEachObjObjVec( vVec, p, pObj, pObjG, i ) \
120  for ( i = 0; (i < Vec_IntSize(vVec)) && ((pObj) = Vta_ManObj(p, Vec_IntEntry(vVec,i))) && ((pObjG) = Gia_ManObj(p->pGia, pObj->iObj)); i++ )
121 #define Vta_ManForEachObjObjVecReverse( vVec, p, pObj, pObjG, i ) \
122  for ( i = Vec_IntSize(vVec) - 1; (i >= 0) && ((pObj) = Vta_ManObj(p, Vec_IntEntry(vVec,i))) && ((pObjG) = Gia_ManObj(p->pGia, pObj->iObj)); i-- )
123 
124 
125 // abstraction is given as an array of integers:
126 // - the first entry is the number of timeframes (F)
127 // - the next (F+1) entries give the beginning position of each timeframe
128 // - the following entries give the object IDs
129 // invariant: assert( vec[vec[0]+1] == size(vec) );
130 
131 extern void Vga_ManAddClausesOne( Vta_Man_t * p, int iObj, int iFrame );
132 
133 ////////////////////////////////////////////////////////////////////////
134 /// FUNCTION DEFINITIONS ///
135 ////////////////////////////////////////////////////////////////////////
136 
137 /**Function*************************************************************
138 
139  Synopsis [Converting from one array to per-frame arrays.]
140 
141  Description []
142 
143  SideEffects []
144 
145  SeeAlso []
146 
147 ***********************************************************************/
148 Vec_Ptr_t * Gia_VtaAbsToFrames( Vec_Int_t * vAbs )
149 {
150  Vec_Ptr_t * vFrames;
151  Vec_Int_t * vFrame;
152  int i, k, Entry, iStart, iStop = -1;
153  int nFrames = Vec_IntEntry( vAbs, 0 );
154  assert( Vec_IntEntry(vAbs, nFrames+1) == Vec_IntSize(vAbs) );
155  vFrames = Vec_PtrAlloc( nFrames );
156  for ( i = 0; i < nFrames; i++ )
157  {
158  iStart = Vec_IntEntry( vAbs, i+1 );
159  iStop = Vec_IntEntry( vAbs, i+2 );
160  vFrame = Vec_IntAlloc( iStop - iStart );
161  Vec_IntForEachEntryStartStop( vAbs, Entry, k, iStart, iStop )
162  Vec_IntPush( vFrame, Entry );
163  Vec_PtrPush( vFrames, vFrame );
164  }
165  assert( iStop == Vec_IntSize(vAbs) );
166  return vFrames;
167 }
168 
169 /**Function*************************************************************
170 
171  Synopsis [Converting from per-frame arrays to one integer array.]
172 
173  Description []
174 
175  SideEffects []
176 
177  SeeAlso []
178 
179 ***********************************************************************/
180 Vec_Int_t * Gia_VtaFramesToAbs( Vec_Vec_t * vFrames )
181 {
182  Vec_Int_t * vOne, * vAbs;
183  int i, k, Entry, nSize;
184  vAbs = Vec_IntAlloc( 2 + Vec_VecSize(vFrames) + Vec_VecSizeSize(vFrames) );
185  Vec_IntPush( vAbs, Vec_VecSize(vFrames) );
186  nSize = Vec_VecSize(vFrames) + 2;
187  Vec_VecForEachLevelInt( vFrames, vOne, i )
188  {
189  Vec_IntPush( vAbs, nSize );
190  nSize += Vec_IntSize( vOne );
191  }
192  Vec_IntPush( vAbs, nSize );
193  assert( Vec_IntSize(vAbs) == Vec_VecSize(vFrames) + 2 );
194  Vec_VecForEachLevelInt( vFrames, vOne, i )
195  Vec_IntForEachEntry( vOne, Entry, k )
196  Vec_IntPush( vAbs, Entry );
197  assert( Vec_IntEntry(vAbs, Vec_IntEntry(vAbs,0)+1) == Vec_IntSize(vAbs) );
198  return vAbs;
199 }
200 
201 /**Function*************************************************************
202 
203  Synopsis [Detects how many frames are completed.]
204 
205  Description []
206 
207  SideEffects []
208 
209  SeeAlso []
210 
211 ***********************************************************************/
212 static inline Vec_Int_t * Vta_ManDeriveAbsAll( Vec_Int_t * p, int nWords )
213 {
214  Vec_Int_t * vRes;
215  unsigned * pThis;
216  int i, w, nObjs = Vec_IntSize(p) / nWords;
217  assert( Vec_IntSize(p) % nWords == 0 );
218  vRes = Vec_IntAlloc( nObjs );
219  for ( i = 0; i < nObjs; i++ )
220  {
221  pThis = (unsigned *)Vec_IntEntryP( p, nWords * i );
222  for ( w = 0; w < nWords; w++ )
223  if ( pThis[w] )
224  break;
225  Vec_IntPush( vRes, (int)(w < nWords) );
226  }
227  return vRes;
228 }
229 
230 /**Function*************************************************************
231 
232  Synopsis [Collect nodes/flops involved in different timeframes.]
233 
234  Description []
235 
236  SideEffects []
237 
238  SeeAlso []
239 
240 ***********************************************************************/
241 int Vec_IntDoubleWidth( Vec_Int_t * p, int nWords )
242 {
243  int * pArray = ABC_CALLOC( int, Vec_IntSize(p) * 2 );
244  int i, w, nObjs = Vec_IntSize(p) / nWords;
245  assert( Vec_IntSize(p) % nWords == 0 );
246  for ( i = 0; i < nObjs; i++ )
247  for ( w = 0; w < nWords; w++ )
248  pArray[2 * nWords * i + w] = p->pArray[nWords * i + w];
249  ABC_FREE( p->pArray );
250  p->pArray = pArray;
251  p->nSize *= 2;
252  p->nCap = p->nSize;
253  return 2 * nWords;
254 }
255 
256 
257 
258 /**Function*************************************************************
259 
260  Synopsis []
261 
262  Description []
263 
264  SideEffects []
265 
266  SeeAlso []
267 
268 ***********************************************************************/
269 static inline int Vga_ManHash( int iObj, int iFrame, int nBins )
270 {
271  return ((unsigned)((iObj + iFrame)*(iObj + iFrame + 1))) % nBins;
272 }
273 static inline int * Vga_ManLookup( Vta_Man_t * p, int iObj, int iFrame )
274 {
275  Vta_Obj_t * pThis;
276  int * pPlace = p->pBins + Vga_ManHash( iObj, iFrame, p->nBins );
277  for ( pThis = Vta_ManObj(p, *pPlace);
278  pThis; pPlace = &pThis->iNext,
279  pThis = Vta_ManObj(p, *pPlace) )
280  if ( pThis->iObj == iObj && pThis->iFrame == iFrame )
281  break;
282  return pPlace;
283 }
284 static inline Vta_Obj_t * Vga_ManFind( Vta_Man_t * p, int iObj, int iFrame )
285 {
286  int * pPlace = Vga_ManLookup( p, iObj, iFrame );
287  return Vta_ManObj(p, *pPlace);
288 }
289 static inline Vta_Obj_t * Vga_ManFindOrAdd( Vta_Man_t * p, int iObj, int iFrame )
290 {
291  Vta_Obj_t * pThis;
292  int i, * pPlace;
293  assert( iObj >= 0 && iFrame >= -1 );
294  if ( p->nObjs == p->nObjsAlloc )
295  {
296  // resize objects
297  p->pObjs = ABC_REALLOC( Vta_Obj_t, p->pObjs, 2 * p->nObjsAlloc );
298  memset( p->pObjs + p->nObjsAlloc, 0, p->nObjsAlloc * sizeof(Vta_Obj_t) );
299  p->nObjsAlloc *= 2;
300  // rehash entries in the table
301  ABC_FREE( p->pBins );
302  p->nBins = Abc_PrimeCudd( 2 * p->nBins );
303  p->pBins = ABC_CALLOC( int, p->nBins );
304  Vta_ManForEachObj( p, pThis, i )
305  {
306  pThis->iNext = 0;
307  pPlace = Vga_ManLookup( p, pThis->iObj, pThis->iFrame );
308  assert( *pPlace == 0 );
309  *pPlace = i;
310  }
311  }
312  pPlace = Vga_ManLookup( p, iObj, iFrame );
313  if ( *pPlace )
314  return Vta_ManObj(p, *pPlace);
315  *pPlace = p->nObjs++;
316  pThis = Vta_ManObj(p, *pPlace);
317  pThis->iObj = iObj;
318  pThis->iFrame = iFrame;
319  return pThis;
320 }
321 static inline void Vga_ManDelete( Vta_Man_t * p, int iObj, int iFrame )
322 {
323  int * pPlace = Vga_ManLookup( p, iObj, iFrame );
324  Vta_Obj_t * pThis = Vta_ManObj(p, *pPlace);
325  assert( pThis != NULL );
326  *pPlace = pThis->iNext;
327  pThis->iNext = -1;
328 }
329 
330 
331 /**Function*************************************************************
332 
333  Synopsis [Derives counter-example using current assignments.]
334 
335  Description []
336 
337  SideEffects []
338 
339  SeeAlso []
340 
341 ***********************************************************************/
342 Abc_Cex_t * Vga_ManDeriveCex( Vta_Man_t * p )
343 {
344  Abc_Cex_t * pCex;
345  Vta_Obj_t * pThis;
346  Gia_Obj_t * pObj;
347  int i;
348  pCex = Abc_CexAlloc( Gia_ManRegNum(p->pGia), Gia_ManPiNum(p->pGia), p->pPars->iFrame+1 );
349  pCex->iPo = 0;
350  pCex->iFrame = p->pPars->iFrame;
351  Vta_ManForEachObjObj( p, pThis, pObj, i )
352  if ( Gia_ObjIsPi(p->pGia, pObj) && sat_solver2_var_value(p->pSat, Vta_ObjId(p, pThis)) )
353  Abc_InfoSetBit( pCex->pData, pCex->nRegs + pThis->iFrame * pCex->nPis + Gia_ObjCioId(pObj) );
354  return pCex;
355 }
356 
357 /**Function*************************************************************
358 
359  Synopsis [Remaps core into frame/node pairs.]
360 
361  Description []
362 
363  SideEffects []
364 
365  SeeAlso []
366 
367 ***********************************************************************/
368 void Vta_ManUnsatCoreRemap( Vta_Man_t * p, Vec_Int_t * vCore )
369 {
370  Vta_Obj_t * pThis;
371  int i, Entry;
372  Vec_IntForEachEntry( vCore, Entry, i )
373  {
374  pThis = Vta_ManObj( p, Entry );
375  Entry = (pThis->iFrame << p->nObjBits) | pThis->iObj;
376  Vec_IntWriteEntry( vCore, i, Entry );
377  }
378 }
379 
380 /**Function*************************************************************
381 
382  Synopsis [Compares two objects by their distance.]
383 
384  Description []
385 
386  SideEffects []
387 
388  SeeAlso []
389 
390 ***********************************************************************/
391 int Vta_ManComputeDepthIncrease( Vta_Obj_t ** pp1, Vta_Obj_t ** pp2 )
392 {
393  int Diff = (*pp1)->Prio - (*pp2)->Prio;
394  if ( Diff < 0 )
395  return -1;
396  if ( Diff > 0 )
397  return 1;
398  Diff = (*pp1) - (*pp2);
399  if ( Diff < 0 )
400  return -1;
401  if ( Diff > 0 )
402  return 1;
403  return 0;
404 }
405 
406 /**Function*************************************************************
407 
408  Synopsis [Returns 1 if the object is already used.]
409 
410  Description []
411 
412  SideEffects []
413 
414  SeeAlso []
415 
416 ***********************************************************************/
417 int Vta_ManObjIsUsed( Vta_Man_t * p, int iObj )
418 {
419  int i;
420  unsigned * pInfo = (unsigned *)Vec_IntEntryP( p->vSeens, p->nWords * iObj );
421  for ( i = 0; i < p->nWords; i++ )
422  if ( pInfo[i] )
423  return 1;
424  return 0;
425 }
426 
427 /**Function*************************************************************
428 
429  Synopsis [Finds predecessors of the node.]
430 
431  Description []
432 
433  SideEffects []
434 
435  SeeAlso []
436 
437 ***********************************************************************/
438 static inline void Vta_ObjPreds( Vta_Man_t * p, Vta_Obj_t * pThis, Gia_Obj_t * pObj, Vta_Obj_t ** ppThis0, Vta_Obj_t ** ppThis1 )
439 {
440  *ppThis0 = NULL;
441  *ppThis1 = NULL;
442 // if ( !pThis->fAdded )
443 // return;
444  assert( !Gia_ObjIsPi(p->pGia, pObj) );
445  if ( Gia_ObjIsConst0(pObj) || (Gia_ObjIsCi(pObj) && pThis->iFrame == 0) )
446  return;
447  if ( Gia_ObjIsAnd(pObj) )
448  {
449  *ppThis0 = Vga_ManFind( p, Gia_ObjFaninId0p(p->pGia, pObj), pThis->iFrame );
450  *ppThis1 = Vga_ManFind( p, Gia_ObjFaninId1p(p->pGia, pObj), pThis->iFrame );
451 // assert( *ppThis0 && *ppThis1 );
452  return;
453  }
454  assert( Gia_ObjIsRo(p->pGia, pObj) && pThis->iFrame > 0 );
455  pObj = Gia_ObjRoToRi( p->pGia, pObj );
456  *ppThis0 = Vga_ManFind( p, Gia_ObjFaninId0p(p->pGia, pObj), pThis->iFrame-1 );
457 // assert( *ppThis0 );
458 }
459 
460 /**Function*************************************************************
461 
462  Synopsis [Collect const/PI/RO/AND in a topological order.]
463 
464  Description []
465 
466  SideEffects []
467 
468  SeeAlso []
469 
470 ***********************************************************************/
471 void Vta_ManCollectNodes_rec( Vta_Man_t * p, Vta_Obj_t * pThis, Vec_Int_t * vOrder )
472 {
473  Gia_Obj_t * pObj;
474  Vta_Obj_t * pThis0, * pThis1;
475  if ( pThis->fVisit )
476  return;
477  pThis->fVisit = 1;
478  pObj = Gia_ManObj( p->pGia, pThis->iObj );
479  if ( pThis->fAdded )
480  {
481  Vta_ObjPreds( p, pThis, pObj, &pThis0, &pThis1 );
482  if ( pThis0 ) Vta_ManCollectNodes_rec( p, pThis0, vOrder );
483  if ( pThis1 ) Vta_ManCollectNodes_rec( p, pThis1, vOrder );
484  }
485  Vec_IntPush( vOrder, Vta_ObjId(p, pThis) );
486 }
487 Vec_Int_t * Vta_ManCollectNodes( Vta_Man_t * p, int f )
488 {
489  Vta_Obj_t * pThis;
490  Gia_Obj_t * pObj;
491  Vec_IntClear( p->vOrder );
492  pObj = Gia_ManPo( p->pGia, 0 );
493  pThis = Vga_ManFind( p, Gia_ObjFaninId0p(p->pGia, pObj), f );
494  assert( pThis != NULL );
495  assert( !pThis->fVisit );
496  Vta_ManCollectNodes_rec( p, pThis, p->vOrder );
497  assert( pThis->fVisit );
498  return p->vOrder;
499 }
500 
501 /**Function*************************************************************
502 
503  Synopsis [Refines abstraction.]
504 
505  Description []
506 
507  SideEffects []
508 
509  SeeAlso []
510 
511 ***********************************************************************/
512 void Vta_ManSatVerify( Vta_Man_t * p )
513 {
514  Vta_Obj_t * pThis, * pThis0, * pThis1;
515  Gia_Obj_t * pObj;
516  int i;
517  Vta_ManForEachObj( p, pThis, i )
518  pThis->Value = (sat_solver2_var_value(p->pSat, i) ? VTA_VAR1 : VTA_VAR0);
519  Vta_ManForEachObjObj( p, pThis, pObj, i )
520  {
521  if ( !pThis->fAdded )
522  continue;
523  Vta_ObjPreds( p, pThis, pObj, &pThis0, &pThis1 );
524  if ( Gia_ObjIsAnd(pObj) )
525  {
526  if ( pThis->Value == VTA_VAR1 )
527  assert( Vta_ValIs1(pThis0, Gia_ObjFaninC0(pObj)) && Vta_ValIs1(pThis1, Gia_ObjFaninC1(pObj)) );
528  else if ( pThis->Value == VTA_VAR0 )
529  assert( Vta_ValIs0(pThis0, Gia_ObjFaninC0(pObj)) || Vta_ValIs0(pThis1, Gia_ObjFaninC1(pObj)) );
530  else assert( 0 );
531  }
532  else if ( Gia_ObjIsRo(p->pGia, pObj) )
533  {
534  pObj = Gia_ObjRoToRi( p->pGia, pObj );
535  if ( pThis->iFrame == 0 )
536  assert( pThis->Value == VTA_VAR0 );
537  else if ( pThis->Value == VTA_VAR0 )
538  assert( Vta_ValIs0(pThis0, Gia_ObjFaninC0(pObj)) );
539  else if ( pThis->Value == VTA_VAR1 )
540  assert( Vta_ValIs1(pThis0, Gia_ObjFaninC0(pObj)) );
541  else assert( 0 );
542  }
543  }
544 }
545 
546 /**Function*************************************************************
547 
548  Synopsis [Refines abstraction.]
549 
550  Description []
551 
552  SideEffects []
553 
554  SeeAlso []
555 
556 ***********************************************************************/
557 void Vta_ManProfileAddition( Vta_Man_t * p, Vec_Int_t * vTermsToAdd )
558 {
559  Vta_Obj_t * pThis;
560  Gia_Obj_t * pObj;
561  // profile the added ones
562  int i, * pCounters = ABC_CALLOC( int, p->pPars->iFrame+1 );
563  Vta_ManForEachObjObjVec( vTermsToAdd, p, pThis, pObj, i )
564  pCounters[pThis->iFrame]++;
565  for ( i = 0; i <= p->pPars->iFrame; i++ )
566  Abc_Print( 1, "%2d", pCounters[i] );
567  Abc_Print( 1, "***\n" );
568 }
569 
570 /**Function*************************************************************
571 
572  Synopsis [Refines abstraction.]
573 
574  Description []
575 
576  SideEffects []
577 
578  SeeAlso []
579 
580 ***********************************************************************/
581 Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p, int f )
582 {
583  int fVerify = 0;
584  Abc_Cex_t * pCex = NULL;
585  Vec_Int_t * vOrder, * vTermsToAdd;
586  Vec_Ptr_t * vTermsUsed, * vTermsUnused;
587  Vta_Obj_t * pThis, * pThis0, * pThis1, * pTop;
588  Gia_Obj_t * pObj;
589  int i, Counter;
590 
591  if ( fVerify )
592  Vta_ManSatVerify( p );
593 
594  // collect nodes in a topological order
595  vOrder = Vta_ManCollectNodes( p, f );
596  Vta_ManForEachObjObjVec( vOrder, p, pThis, pObj, i )
597  {
598  pThis->Prio = VTA_LARGE;
599  pThis->Value = sat_solver2_var_value(p->pSat, Vta_ObjId(p, pThis)) ? VTA_VAR1 : VTA_VAR0;
600  pThis->fVisit = 0;
601  }
602 
603  // verify
604  if ( fVerify )
605  Vta_ManForEachObjObjVec( vOrder, p, pThis, pObj, i )
606  {
607  if ( !pThis->fAdded )
608  continue;
609  Vta_ObjPreds( p, pThis, pObj, &pThis0, &pThis1 );
610  if ( Gia_ObjIsAnd(pObj) )
611  {
612  if ( pThis->Value == VTA_VAR1 )
613  assert( Vta_ValIs1(pThis0, Gia_ObjFaninC0(pObj)) && Vta_ValIs1(pThis1, Gia_ObjFaninC1(pObj)) );
614  else if ( pThis->Value == VTA_VAR0 )
615  assert( Vta_ValIs0(pThis0, Gia_ObjFaninC0(pObj)) || Vta_ValIs0(pThis1, Gia_ObjFaninC1(pObj)) );
616  else assert( 0 );
617  }
618  else if ( Gia_ObjIsRo(p->pGia, pObj) )
619  {
620  pObj = Gia_ObjRoToRi( p->pGia, pObj );
621  if ( pThis->iFrame == 0 )
622  assert( pThis->Value == VTA_VAR0 );
623  else if ( pThis->Value == VTA_VAR0 )
624  assert( Vta_ValIs0(pThis0, Gia_ObjFaninC0(pObj)) );
625  else if ( pThis->Value == VTA_VAR1 )
626  assert( Vta_ValIs1(pThis0, Gia_ObjFaninC0(pObj)) );
627  else assert( 0 );
628  }
629  }
630 
631  // compute distance in reverse order
632  pThis = Vta_ManObj( p, Vec_IntEntryLast(vOrder) );
633  pThis->Prio = 1;
634  // collect used and unused terms
635  vTermsUsed = Vec_PtrAlloc( 1015 );
636  vTermsUnused = Vec_PtrAlloc( 1016 );
637  Vta_ManForEachObjObjVecReverse( vOrder, p, pThis, pObj, i )
638  {
639  // there is no unreachable states
640  assert( pThis->Prio < VTA_LARGE );
641  // skip constants and PIs
642  if ( Gia_ObjIsConst0(pObj) || Gia_ObjIsPi(p->pGia, pObj) )
643  {
644  pThis->Prio = 0; // set highest priority
645  continue;
646  }
647  // collect terminals
648  assert( Gia_ObjIsAnd(pObj) || Gia_ObjIsRo(p->pGia, pObj) );
649  if ( !pThis->fAdded )
650  {
651  assert( pThis->Prio > 0 );
652  if ( Vta_ManObjIsUsed(p, pThis->iObj) )
653  Vec_PtrPush( vTermsUsed, pThis );
654  else
655  Vec_PtrPush( vTermsUnused, pThis );
656  continue;
657  }
658  // propagate
659  Vta_ObjPreds( p, pThis, pObj, &pThis0, &pThis1 );
660  if ( pThis0 )
661  pThis0->Prio = Abc_MinInt( pThis0->Prio, pThis->Prio + 1 );
662  if ( pThis1 )
663  pThis1->Prio = Abc_MinInt( pThis1->Prio, pThis->Prio + 1 );
664  }
665 
666 /*
667  Vta_ManForEachObjObjVecReverse( vOrder, p, pThis, pObj, i )
668  if ( pThis->Prio > 0 )
669  pThis->Prio = 10;
670 */
671 /*
672  // update priorities according to reconvergence counters
673  Vec_PtrForEachEntry( Vta_Obj_t *, vTermsUsed, pThis, i )
674  {
675  Vta_Obj_t * pThis0, * pThis1;
676  Gia_Obj_t * pObj = Gia_ManObj( p->pGia, pThis->iObj );
677  Vta_ObjPreds( p, pThis, pObj, &pThis0, &pThis1 );
678  pThis->Prio += 10000000;
679  if ( pThis0 )
680  pThis->Prio -= 1000000 * pThis0->fAdded;
681  if ( pThis1 )
682  pThis->Prio -= 1000000 * pThis1->fAdded;
683  }
684  Vec_PtrForEachEntry( Vta_Obj_t *, vTermsUnused, pThis, i )
685  {
686  Vta_Obj_t * pThis0, * pThis1;
687  Gia_Obj_t * pObj = Gia_ManObj( p->pGia, pThis->iObj );
688  Vta_ObjPreds( p, pThis, pObj, &pThis0, &pThis1 );
689  pThis->Prio += 10000000;
690  if ( pThis0 )
691  pThis->Prio -= 1000000 * pThis0->fAdded;
692  if ( pThis1 )
693  pThis->Prio -= 1000000 * pThis1->fAdded;
694  }
695 */
696 
697 
698  // update priorities according to reconvergence counters
699  Vec_PtrForEachEntry( Vta_Obj_t *, vTermsUsed, pThis, i )
700  pThis->Prio = pThis->iObj;
701  Vec_PtrForEachEntry( Vta_Obj_t *, vTermsUnused, pThis, i )
702  pThis->Prio = pThis->iObj;
703 
704 
705  // objects with equal distance should receive priority based on number
706  // those objects whose prototypes have been added in other timeframes
707  // should have higher priority than the current object
708  Vec_PtrSort( vTermsUsed, (int (*)(void))Vta_ManComputeDepthIncrease );
709  Vec_PtrSort( vTermsUnused, (int (*)(void))Vta_ManComputeDepthIncrease );
710  if ( Vec_PtrSize(vTermsUsed) > 1 )
711  {
712  pThis0 = (Vta_Obj_t *)Vec_PtrEntry(vTermsUsed, 0);
713  pThis1 = (Vta_Obj_t *)Vec_PtrEntryLast(vTermsUsed);
714  assert( pThis0->Prio <= pThis1->Prio );
715  }
716  // assign the priority based on these orders
717  Counter = 1;
718  Vec_PtrForEachEntry( Vta_Obj_t *, vTermsUsed, pThis, i )
719  pThis->Prio = Counter++;
720  Vec_PtrForEachEntry( Vta_Obj_t *, vTermsUnused, pThis, i )
721  pThis->Prio = Counter++;
722 // Abc_Print( 1, "Used %d Unused %d\n", Vec_PtrSize(vTermsUsed), Vec_PtrSize(vTermsUnused) );
723 
724 
725  // propagate in the direct order
726  Vta_ManForEachObjObjVec( vOrder, p, pThis, pObj, i )
727  {
728  assert( pThis->fVisit == 0 );
729  assert( pThis->Prio < VTA_LARGE );
730  // skip terminal objects
731  if ( !pThis->fAdded )
732  continue;
733  // assumes that values are assigned!!!
734  assert( pThis->Value != 0 );
735  // propagate
736  if ( Gia_ObjIsAnd(pObj) )
737  {
738  pThis0 = Vga_ManFind( p, Gia_ObjFaninId0p(p->pGia, pObj), pThis->iFrame );
739  pThis1 = Vga_ManFind( p, Gia_ObjFaninId1p(p->pGia, pObj), pThis->iFrame );
740  assert( pThis0 && pThis1 );
741  if ( pThis->Value == VTA_VAR1 )
742  {
743  assert( Vta_ValIs1(pThis0, Gia_ObjFaninC0(pObj)) && Vta_ValIs1(pThis1, Gia_ObjFaninC1(pObj)) );
744  pThis->Prio = Abc_MaxInt( pThis0->Prio, pThis1->Prio );
745  }
746  else if ( pThis->Value == VTA_VAR0 )
747  {
748  if ( Vta_ValIs0(pThis0, Gia_ObjFaninC0(pObj)) && Vta_ValIs0(pThis1, Gia_ObjFaninC1(pObj)) )
749  pThis->Prio = Abc_MinInt( pThis0->Prio, pThis1->Prio ); // choice!!!
750  else if ( Vta_ValIs0(pThis0, Gia_ObjFaninC0(pObj)) )
751  pThis->Prio = pThis0->Prio;
752  else if ( Vta_ValIs0(pThis1, Gia_ObjFaninC1(pObj)) )
753  pThis->Prio = pThis1->Prio;
754  else assert( 0 );
755  }
756  else assert( 0 );
757  }
758  else if ( Gia_ObjIsRo(p->pGia, pObj) )
759  {
760  if ( pThis->iFrame > 0 )
761  {
762  pObj = Gia_ObjRoToRi( p->pGia, pObj );
763  pThis0 = Vga_ManFind( p, Gia_ObjFaninId0p(p->pGia, pObj), pThis->iFrame-1 );
764  assert( pThis0 );
765  pThis->Prio = pThis0->Prio;
766  }
767  else
768  pThis->Prio = 0;
769  }
770  else if ( Gia_ObjIsConst0(pObj) )
771  pThis->Prio = 0;
772  else
773  assert( 0 );
774  }
775 
776  // select important values
777  pTop = Vta_ManObj( p, Vec_IntEntryLast(vOrder) );
778  pTop->fVisit = 1;
779  vTermsToAdd = Vec_IntAlloc( 100 );
780  Vta_ManForEachObjObjVecReverse( vOrder, p, pThis, pObj, i )
781  {
782  if ( !pThis->fVisit )
783  continue;
784  pThis->fVisit = 0;
785  assert( pThis->Prio >= 0 && pThis->Prio <= pTop->Prio );
786  // skip terminal objects
787  if ( !pThis->fAdded )
788  {
789  assert( Gia_ObjIsAnd(pObj) || Gia_ObjIsRo(p->pGia, pObj) || Gia_ObjIsConst0(pObj) || Gia_ObjIsPi(p->pGia, pObj) );
790  Vec_IntPush( vTermsToAdd, Vta_ObjId(p, pThis) );
791  continue;
792  }
793  // assumes that values are assigned!!!
794  assert( pThis->Value != 0 );
795  // propagate
796  if ( Gia_ObjIsAnd(pObj) )
797  {
798  pThis0 = Vga_ManFind( p, Gia_ObjFaninId0p(p->pGia, pObj), pThis->iFrame );
799  pThis1 = Vga_ManFind( p, Gia_ObjFaninId1p(p->pGia, pObj), pThis->iFrame );
800  assert( pThis0 && pThis1 );
801  if ( pThis->Value == VTA_VAR1 )
802  {
803  assert( Vta_ValIs1(pThis0, Gia_ObjFaninC0(pObj)) && Vta_ValIs1(pThis1, Gia_ObjFaninC1(pObj)) );
804  assert( pThis0->Prio <= pThis->Prio );
805  assert( pThis1->Prio <= pThis->Prio );
806  pThis0->fVisit = 1;
807  pThis1->fVisit = 1;
808  }
809  else if ( pThis->Value == VTA_VAR0 )
810  {
811  if ( Vta_ValIs0(pThis0, Gia_ObjFaninC0(pObj)) && Vta_ValIs0(pThis1, Gia_ObjFaninC1(pObj)) )
812  {
813  if ( pThis0->fVisit )
814  {
815  }
816  else if ( pThis1->fVisit )
817  {
818  }
819  else if ( pThis0->Prio <= pThis1->Prio ) // choice!!!
820  {
821  pThis0->fVisit = 1;
822  assert( pThis0->Prio == pThis->Prio );
823  }
824  else
825  {
826  pThis1->fVisit = 1;
827  assert( pThis1->Prio == pThis->Prio );
828  }
829  }
830  else if ( Vta_ValIs0(pThis0, Gia_ObjFaninC0(pObj)) )
831  {
832  pThis0->fVisit = 1;
833  assert( pThis0->Prio == pThis->Prio );
834  }
835  else if ( Vta_ValIs0(pThis1, Gia_ObjFaninC1(pObj)) )
836  {
837  pThis1->fVisit = 1;
838  assert( pThis1->Prio == pThis->Prio );
839  }
840  else assert( 0 );
841  }
842  else assert( 0 );
843  }
844  else if ( Gia_ObjIsRo(p->pGia, pObj) )
845  {
846  if ( pThis->iFrame > 0 )
847  {
848  pObj = Gia_ObjRoToRi( p->pGia, pObj );
849  pThis0 = Vga_ManFind( p, Gia_ObjFaninId0p(p->pGia, pObj), pThis->iFrame-1 );
850  assert( pThis0 );
851  pThis0->fVisit = 1;
852  assert( pThis0->Prio == pThis->Prio );
853  }
854  }
855  else if ( !Gia_ObjIsConst0(pObj) )
856  assert( 0 );
857  }
858 
859  if ( p->pPars->fAddLayer )
860  {
861  // mark those currently included
862  Vta_ManForEachObjVec( vTermsToAdd, p, pThis, i )
863  {
864  assert( pThis->fVisit == 0 );
865  pThis->fVisit = 1;
866  }
867  // add used terms, which have close relationship
868  Counter = Vec_IntSize(vTermsToAdd);
869  Vec_PtrForEachEntry( Vta_Obj_t *, vTermsUsed, pThis, i )
870  {
871  if ( pThis->fVisit )
872  continue;
873  // Vta_ObjPreds( p, pThis, Gia_ManObj(p->pGia, pThis->iObj), &pThis0, &pThis1 );
874  // if ( (pThis0 && (pThis0->fAdded || pThis0->fVisit)) || (pThis1 && (pThis1->fAdded || pThis1->fVisit)) )
875  Vec_IntPush( vTermsToAdd, Vta_ObjId(p, pThis) );
876  }
877  // remove those currenty included
878  Vta_ManForEachObjVec( vTermsToAdd, p, pThis, i )
879  pThis->fVisit = 0;
880  }
881 // printf( "\n%d -> %d\n", Counter, Vec_IntSize(vTermsToAdd) );
882 //Vec_IntReverseOrder( vTermsToAdd );
883 //Vec_IntSort( vTermsToAdd, 1 );
884 
885 
886  // cleanup
887  Vec_PtrFree( vTermsUsed );
888  Vec_PtrFree( vTermsUnused );
889 
890 
891  if ( fVerify )
892  {
893  // verify
894  Vta_ManForEachObjVec( vOrder, p, pThis, i )
895  pThis->Value = VTA_VARX;
896  Vta_ManForEachObjVec( vTermsToAdd, p, pThis, i )
897  {
898  assert( !pThis->fAdded );
899  pThis->Value = sat_solver2_var_value(p->pSat, Vta_ObjId(p, pThis)) ? VTA_VAR1 : VTA_VAR0;
900  }
901  // simulate
902  Vta_ManForEachObjObjVec( vOrder, p, pThis, pObj, i )
903  {
904  assert( pThis->fVisit == 0 );
905  if ( !pThis->fAdded )
906  continue;
907  if ( Gia_ObjIsAnd(pObj) )
908  {
909  pThis0 = Vga_ManFind( p, Gia_ObjFaninId0p(p->pGia, pObj), pThis->iFrame );
910  pThis1 = Vga_ManFind( p, Gia_ObjFaninId1p(p->pGia, pObj), pThis->iFrame );
911  assert( pThis0 && pThis1 );
912  if ( Vta_ValIs1(pThis0, Gia_ObjFaninC0(pObj)) && Vta_ValIs1(pThis1, Gia_ObjFaninC1(pObj)) )
913  pThis->Value = VTA_VAR1;
914  else if ( Vta_ValIs0(pThis0, Gia_ObjFaninC0(pObj)) || Vta_ValIs0(pThis1, Gia_ObjFaninC1(pObj)) )
915  pThis->Value = VTA_VAR0;
916  else
917  pThis->Value = VTA_VARX;
918  }
919  else if ( Gia_ObjIsRo(p->pGia, pObj) )
920  {
921  if ( pThis->iFrame > 0 )
922  {
923  pObj = Gia_ObjRoToRi( p->pGia, pObj );
924  pThis0 = Vga_ManFind( p, Gia_ObjFaninId0p(p->pGia, pObj), pThis->iFrame-1 );
925  assert( pThis0 );
926  if ( Vta_ValIs0(pThis0, Gia_ObjFaninC0(pObj)) )
927  pThis->Value = VTA_VAR0;
928  else if ( Vta_ValIs1(pThis0, Gia_ObjFaninC0(pObj)) )
929  pThis->Value = VTA_VAR1;
930  else
931  pThis->Value = VTA_VARX;
932  }
933  else
934  {
935  pThis->Value = VTA_VAR0;
936  }
937  }
938  else if ( Gia_ObjIsConst0(pObj) )
939  {
940  pThis->Value = VTA_VAR0;
941  }
942  else assert( 0 );
943  // double check the solver
944  assert( pThis->Value == VTA_VARX || (int)pThis->Value == (sat_solver2_var_value(p->pSat, Vta_ObjId(p, pThis)) ? VTA_VAR1 : VTA_VAR0) );
945  }
946 
947  // check the output
948  if ( !Vta_ValIs1(pTop, Gia_ObjFaninC0(Gia_ManPo(p->pGia, 0))) )
949  Abc_Print( 1, "Vta_ManRefineAbstraction(): Terminary simulation verification failed!\n" );
950 // else
951 // Abc_Print( 1, "Verification OK.\n" );
952  }
953 
954 
955  // produce true counter-example
956  if ( pTop->Prio == 0 )
957  pCex = Vga_ManDeriveCex( p );
958  else
959  {
960 // Vta_ManProfileAddition( p, vTermsToAdd );
961 
962  Vta_ManForEachObjObjVec( vTermsToAdd, p, pThis, pObj, i )
963  if ( !Gia_ObjIsPi(p->pGia, pObj) )
964  Vga_ManAddClausesOne( p, pThis->iObj, pThis->iFrame );
965  sat_solver2_simplify( p->pSat );
966  }
967  p->nObjAdded += Vec_IntSize(vTermsToAdd);
968  Vec_IntFree( vTermsToAdd );
969  return pCex;
970 }
971 
972 /**Function*************************************************************
973 
974  Synopsis []
975 
976  Description []
977 
978  SideEffects []
979 
980  SeeAlso []
981 
982 ***********************************************************************/
983 Vta_Man_t * Vga_ManStart( Gia_Man_t * pGia, Abs_Par_t * pPars )
984 {
985  Vta_Man_t * p;
986  p = ABC_CALLOC( Vta_Man_t, 1 );
987  p->pGia = pGia;
988  p->pPars = pPars;
989  // internal data
990  p->nObjsAlloc = (1 << 18);
991  p->pObjs = ABC_CALLOC( Vta_Obj_t, p->nObjsAlloc );
992  p->nObjs = 1;
993  p->nBins = Abc_PrimeCudd( 2*p->nObjsAlloc );
994  p->pBins = ABC_CALLOC( int, p->nBins );
995  p->vOrder = Vec_IntAlloc( 1013 );
996  // abstraction
997  p->nObjBits = Abc_Base2Log( Gia_ManObjNum(pGia) );
998  p->nObjMask = (1 << p->nObjBits) - 1;
999  assert( Gia_ManObjNum(pGia) <= (int)p->nObjMask );
1000  p->nWords = 1;
1001  p->vSeens = Vec_IntStart( Gia_ManObjNum(pGia) * p->nWords );
1002  p->vSeenGla = Vec_BitStart( Gia_ManObjNum(pGia) );
1003  p->nSeenGla = 1;
1004  p->nSeenAll = 1;
1005  // other data
1006  p->vCores = Vec_PtrAlloc( 100 );
1007  p->pSat = sat_solver2_new();
1008  p->pSat->pPrf1 = Vec_SetAlloc( 20 );
1009 // p->pSat->fVerbose = p->pPars->fVerbose;
1010 // sat_solver2_set_learntmax( p->pSat, pPars->nLearnedMax );
1011  p->pSat->nLearntStart = p->pPars->nLearnedStart;
1012  p->pSat->nLearntDelta = p->pPars->nLearnedDelta;
1013  p->pSat->nLearntRatio = p->pPars->nLearnedPerce;
1014  p->pSat->nLearntMax = p->pSat->nLearntStart;
1015  // start the abstraction
1016  assert( pGia->vObjClasses != NULL );
1017  p->vFrames = Gia_VtaAbsToFrames( pGia->vObjClasses );
1018  p->vAddedNew = Vec_IntAlloc( 1000 );
1019  return p;
1020 }
1021 
1022 /**Function*************************************************************
1023 
1024  Synopsis [Delete manager.]
1025 
1026  Description []
1027 
1028  SideEffects []
1029 
1030  SeeAlso []
1031 
1032 ***********************************************************************/
1033 void Vga_ManStop( Vta_Man_t * p )
1034 {
1035  if ( p->pPars->fVerbose )
1036  Abc_Print( 1, "SAT solver: Var = %d Cla = %d Conf = %d Lrn = %d Reduce = %d Cex = %d Objs+ = %d\n",
1037  sat_solver2_nvars(p->pSat), sat_solver2_nclauses(p->pSat), sat_solver2_nconflicts(p->pSat),
1038  sat_solver2_nlearnts(p->pSat), p->pSat->nDBreduces, p->nCexes, p->nObjAdded );
1039  Vec_VecFreeP( (Vec_Vec_t **)&p->vCores );
1040  Vec_VecFreeP( (Vec_Vec_t **)&p->vFrames );
1041  Vec_BitFreeP( &p->vSeenGla );
1042  Vec_IntFreeP( &p->vSeens );
1043  Vec_IntFreeP( &p->vOrder );
1044  Vec_IntFreeP( &p->vAddedNew );
1045  sat_solver2_delete( p->pSat );
1046  ABC_FREE( p->pBins );
1047  ABC_FREE( p->pObjs );
1048  ABC_FREE( p );
1049 }
1050 
1051 /**Function*************************************************************
1052 
1053  Synopsis [Returns the output literal.]
1054 
1055  Description []
1056 
1057  SideEffects []
1058 
1059  SeeAlso []
1060 
1061 ***********************************************************************/
1062 static inline int Vga_ManGetOutLit( Vta_Man_t * p, int f )
1063 {
1064  Gia_Obj_t * pObj = Gia_ManPo(p->pGia, 0);
1065  Vta_Obj_t * pThis = Vga_ManFind( p, Gia_ObjFaninId0p(p->pGia, pObj), f );
1066  assert( pThis != NULL && pThis->fAdded );
1067  if ( f == 0 && Gia_ObjIsRo(p->pGia, Gia_ObjFanin0(pObj)) && !Gia_ObjFaninC0(pObj) )
1068  return -Vta_ObjId(p, pThis);
1069  return Abc_Var2Lit( Vta_ObjId(p, pThis), Gia_ObjFaninC0(pObj) );
1070 }
1071 
1072 /**Function*************************************************************
1073 
1074  Synopsis [Finds the set of clauses involved in the UNSAT core.]
1075 
1076  Description []
1077 
1078  SideEffects []
1079 
1080  SeeAlso []
1081 
1082 ***********************************************************************/
1083 Vec_Int_t * Vta_ManUnsatCore( int iLit, sat_solver2 * pSat, int nConfMax, int fVerbose, int * piRetValue, int * pnConfls )
1084 {
1085  abctime clk = Abc_Clock();
1086  Vec_Int_t * vCore;
1087  int RetValue, nConfPrev = pSat->stats.conflicts;
1088  if ( piRetValue )
1089  *piRetValue = 1;
1090  // consider special case when PO points to the flop
1091  // this leads to immediate conflict in the first timeframe
1092  if ( iLit < 0 )
1093  {
1094  vCore = Vec_IntAlloc( 1 );
1095  Vec_IntPush( vCore, -iLit );
1096  return vCore;
1097  }
1098  // solve the problem
1099  RetValue = sat_solver2_solve( pSat, &iLit, &iLit+1, (ABC_INT64_T)nConfMax, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
1100  if ( pnConfls )
1101  *pnConfls = (int)pSat->stats.conflicts - nConfPrev;
1102  if ( RetValue == l_Undef )
1103  {
1104  if ( piRetValue )
1105  *piRetValue = -1;
1106  return NULL;
1107  }
1108  if ( RetValue == l_True )
1109  {
1110  if ( piRetValue )
1111  *piRetValue = 0;
1112  return NULL;
1113  }
1114  if ( fVerbose )
1115  {
1116 // Abc_Print( 1, "%6d", (int)pSat->stats.conflicts - nConfPrev );
1117 // Abc_Print( 1, "UNSAT after %7d conflicts. ", pSat->stats.conflicts );
1118 // Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
1119  }
1120  assert( RetValue == l_False );
1121  // derive the UNSAT core
1122  clk = Abc_Clock();
1123  vCore = (Vec_Int_t *)Sat_ProofCore( pSat );
1124  if ( fVerbose )
1125  {
1126 // Abc_Print( 1, "Core is %8d vars (out of %8d). ", Vec_IntSize(vCore), sat_solver2_nvars(pSat) );
1127 // Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
1128  }
1129  return vCore;
1130 }
1131 
1132 /**Function*************************************************************
1133 
1134  Synopsis []
1135 
1136  Description []
1137 
1138  SideEffects []
1139 
1140  SeeAlso []
1141 
1142 ***********************************************************************/
1143 int Vta_ManAbsPrintFrame( Vta_Man_t * p, Vec_Int_t * vCore, int nFrames, int nConfls, int nCexes, abctime Time, int fVerbose )
1144 {
1145  unsigned * pInfo;
1146  int * pCountAll = NULL, * pCountUni = NULL;
1147  int i, iFrame, iObj, Entry, fChanges = 0;
1148  // print info about frames
1149  if ( vCore )
1150  {
1151  pCountAll = ABC_CALLOC( int, nFrames + 1 );
1152  pCountUni = ABC_CALLOC( int, nFrames + 1 );
1153  Vec_IntForEachEntry( vCore, Entry, i )
1154  {
1155  iObj = (Entry & p->nObjMask);
1156  iFrame = (Entry >> p->nObjBits);
1157  assert( iFrame < nFrames );
1158  pInfo = (unsigned *)Vec_IntEntryP( p->vSeens, p->nWords * iObj );
1159  if ( !Abc_InfoHasBit(pInfo, iFrame) )
1160  {
1161  Abc_InfoSetBit( pInfo, iFrame );
1162  pCountUni[iFrame+1]++;
1163  pCountUni[0]++;
1164  p->nSeenAll++;
1165  }
1166  pCountAll[iFrame+1]++;
1167  pCountAll[0]++;
1168  if ( !Vec_BitEntry(p->vSeenGla, iObj) )
1169  {
1170  Vec_BitWriteEntry(p->vSeenGla, iObj, 1);
1171  p->nSeenGla++;
1172  fChanges = 1;
1173  }
1174  }
1175  }
1176  if ( !fVerbose )
1177  {
1178  ABC_FREE( pCountAll );
1179  ABC_FREE( pCountUni );
1180  return fChanges;
1181  }
1182 
1183  if ( Abc_FrameIsBatchMode() && !vCore )
1184  return fChanges;
1185 
1186 // Abc_Print( 1, "%5d%5d", pCountAll[0], pCountUni[0] );
1187  Abc_Print( 1, "%4d :", nFrames-1 );
1188  Abc_Print( 1, "%4d", Abc_MinInt(100, 100 * p->nSeenGla / (Gia_ManRegNum(p->pGia) + Gia_ManAndNum(p->pGia) + 1)) );
1189  Abc_Print( 1, "%6d", p->nSeenGla );
1190  Abc_Print( 1, "%4d", Abc_MinInt(100, 100 * p->nSeenAll / (p->nSeenGla * nFrames)) );
1191  Abc_Print( 1, "%8d", nConfls );
1192  if ( nCexes == 0 )
1193  Abc_Print( 1, "%5c", '-' );
1194  else
1195  Abc_Print( 1, "%5d", nCexes );
1196 // Abc_Print( 1, " %9d", sat_solver2_nvars(p->pSat) );
1197  Abc_PrintInt( sat_solver2_nvars(p->pSat) );
1198  Abc_PrintInt( sat_solver2_nclauses(p->pSat) );
1199  Abc_PrintInt( sat_solver2_nlearnts(p->pSat) );
1200  if ( vCore == NULL )
1201  {
1202  Abc_Print( 1, " ..." );
1203 // for ( k = 0; k < 7; k++ )
1204 // Abc_Print( 1, " " );
1205  Abc_Print( 1, "%9.2f sec", 1.0*Time/CLOCKS_PER_SEC );
1206  Abc_Print( 1, "%5.1f GB", (sat_solver2_memory_proof(p->pSat) + sat_solver2_memory(p->pSat, 0)) / (1<<30) );
1207  Abc_Print( 1, "\r" );
1208  }
1209  else
1210  {
1211  Abc_PrintInt( pCountAll[0] );
1212 /*
1213  if ( nFrames > 7 )
1214  {
1215  for ( k = 0; k < 3; k++ )
1216  Abc_Print( 1, "%5d", pCountAll[k+1] );
1217  Abc_Print( 1, " ..." );
1218  for ( k = nFrames-3; k < nFrames; k++ )
1219  Abc_Print( 1, "%5d", pCountAll[k+1] );
1220  }
1221  else
1222  {
1223  for ( k = 0; k < nFrames; k++ )
1224  Abc_Print( 1, "%5d", pCountAll[k+1] );
1225  for ( k = nFrames; k < 7; k++ )
1226  Abc_Print( 1, " " );
1227  }
1228 */
1229  Abc_Print( 1, "%9.2f sec", 1.0*Time/CLOCKS_PER_SEC );
1230  Abc_Print( 1, "%5.1f GB", (sat_solver2_memory_proof(p->pSat) + sat_solver2_memory(p->pSat, 0)) / (1<<30) );
1231  Abc_Print( 1, "\n" );
1232  }
1233  fflush( stdout );
1234 
1235  if ( vCore )
1236  {
1237  ABC_FREE( pCountAll );
1238  ABC_FREE( pCountUni );
1239  }
1240  return fChanges;
1241 }
1242 
1243 /**Function*************************************************************
1244 
1245  Synopsis [Adds clauses to the solver.]
1246 
1247  Description []
1248 
1249  SideEffects []
1250 
1251  SeeAlso []
1252 
1253 ***********************************************************************/
1254 void Vga_ManAddClausesOne( Vta_Man_t * p, int iObj, int iFrame )
1255 {
1256  Vta_Obj_t * pThis0, * pThis1;
1257  Gia_Obj_t * pObj = Gia_ManObj( p->pGia, iObj );
1258  Vta_Obj_t * pThis = Vga_ManFindOrAdd( p, iObj, iFrame );
1259  int iThis0, iMainVar = Vta_ObjId(p, pThis);
1260  assert( pThis->iObj == iObj && pThis->iFrame == iFrame );
1261  if ( pThis->fAdded )
1262  return;
1263  pThis->fAdded = 1;
1264  Vec_IntPush( p->vAddedNew, iMainVar );
1265  if ( Gia_ObjIsAnd(pObj) )
1266  {
1267  pThis0 = Vga_ManFindOrAdd( p, Gia_ObjFaninId0p(p->pGia, pObj), iFrame );
1268  iThis0 = Vta_ObjId(p, pThis0);
1269  pThis1 = Vga_ManFindOrAdd( p, Gia_ObjFaninId1p(p->pGia, pObj), iFrame );
1270  sat_solver2_add_and( p->pSat, iMainVar, iThis0, Vta_ObjId(p, pThis1),
1271  Gia_ObjFaninC0(pObj), Gia_ObjFaninC1(pObj), 0, iMainVar );
1272  }
1273  else if ( Gia_ObjIsRo(p->pGia, pObj) )
1274  {
1275  if ( iFrame == 0 )
1276  {
1277  if ( p->pPars->fUseTermVars )
1278  {
1279  pThis0 = Vga_ManFindOrAdd( p, iObj, -1 );
1280  sat_solver2_add_constraint( p->pSat, iMainVar, Vta_ObjId(p, pThis0), 1, 0, iMainVar );
1281  }
1282  else
1283  {
1284  sat_solver2_add_const( p->pSat, iMainVar, 1, 0, iMainVar );
1285  }
1286  }
1287  else
1288  {
1289  pObj = Gia_ObjRoToRi( p->pGia, pObj );
1290  pThis0 = Vga_ManFindOrAdd( p, Gia_ObjFaninId0p(p->pGia, pObj), iFrame-1 );
1291  sat_solver2_add_buffer( p->pSat, iMainVar, Vta_ObjId(p, pThis0), Gia_ObjFaninC0(pObj), 0, iMainVar );
1292  }
1293  }
1294  else if ( Gia_ObjIsConst0(pObj) )
1295  {
1296  sat_solver2_add_const( p->pSat, iMainVar, 1, 0, iMainVar );
1297  }
1298  else //if ( !Gia_ObjIsPi(p->pGia, pObj) )
1299  assert( 0 );
1300 }
1301 
1302 /**Function*************************************************************
1303 
1304  Synopsis []
1305 
1306  Description []
1307 
1308  SideEffects []
1309 
1310  SeeAlso []
1311 
1312 ***********************************************************************/
1313 void Vga_ManLoadSlice( Vta_Man_t * p, Vec_Int_t * vOne, int Lift )
1314 {
1315  int i, Entry;
1316  Vec_IntForEachEntry( vOne, Entry, i )
1317  Vga_ManAddClausesOne( p, Entry & p->nObjMask, (Entry >> p->nObjBits) + Lift );
1318  sat_solver2_simplify( p->pSat );
1319 }
1320 
1321 /**Function*************************************************************
1322 
1323  Synopsis []
1324 
1325  Description []
1326 
1327  SideEffects []
1328 
1329  SeeAlso []
1330 
1331 ***********************************************************************/
1332 void Vga_ManPrintCore( Vta_Man_t * p, Vec_Int_t * vCore, int Lift )
1333 {
1334  int i, Entry, iObj, iFrame;
1335  Vec_IntForEachEntry( vCore, Entry, i )
1336  {
1337  iObj = (Entry & p->nObjMask);
1338  iFrame = (Entry >> p->nObjBits);
1339  Abc_Print( 1, "%d*%d ", iObj, iFrame+Lift );
1340  }
1341  Abc_Print( 1, "\n" );
1342 }
1343 
1344 /**Function*************************************************************
1345 
1346  Synopsis []
1347 
1348  Description []
1349 
1350  SideEffects []
1351 
1352  SeeAlso []
1353 
1354 ***********************************************************************/
1355 void Vga_ManRollBack( Vta_Man_t * p, int nObjOld )
1356 {
1357  Vta_Obj_t * pThis = p->pObjs + nObjOld;
1358  Vta_Obj_t * pLimit = p->pObjs + p->nObjs;
1359  int i, Entry;
1360  for ( ; pThis < pLimit; pThis++ )
1361  Vga_ManDelete( p, pThis->iObj, pThis->iFrame );
1362  memset( p->pObjs + nObjOld, 0, sizeof(Vta_Obj_t) * (p->nObjs - nObjOld) );
1363  p->nObjs = nObjOld;
1364  Vec_IntForEachEntry( p->vAddedNew, Entry, i )
1365  if ( Entry < p->nObjs )
1366  {
1367  pThis = Vta_ManObj(p, Entry);
1368  assert( pThis->fAdded == 1 );
1369  pThis->fAdded = 0;
1370  }
1371 }
1372 
1373 /**Function*************************************************************
1374 
1375  Synopsis [Send abstracted model or send cancel.]
1376 
1377  Description [Counter-example will be sent automatically when &vta terminates.]
1378 
1379  SideEffects []
1380 
1381  SeeAlso []
1382 
1383 ***********************************************************************/
1384 void Gia_VtaSendAbsracted( Vta_Man_t * p, int fVerbose )
1385 {
1386  Gia_Man_t * pAbs;
1387  assert( Abc_FrameIsBridgeMode() );
1388 // if ( fVerbose )
1389 // Abc_Print( 1, "Sending abstracted model...\n" );
1390  // create obj classes
1391  Vec_IntFreeP( &p->pGia->vObjClasses );
1392  p->pGia->vObjClasses = Gia_VtaFramesToAbs( (Vec_Vec_t *)p->vCores );
1393  // create gate classes
1394  Vec_IntFreeP( &p->pGia->vGateClasses );
1395  p->pGia->vGateClasses = Gia_VtaConvertToGla( p->pGia, p->pGia->vObjClasses );
1396  Vec_IntFreeP( &p->pGia->vObjClasses );
1397  // create abstrated model
1398  pAbs = Gia_ManDupAbsGates( p->pGia, p->pGia->vGateClasses );
1399  Vec_IntFreeP( &p->pGia->vGateClasses );
1400  // send it out
1401  Gia_ManToBridgeAbsNetlist( stdout, pAbs, BRIDGE_ABS_NETLIST );
1402  Gia_ManStop( pAbs );
1403 }
1404 void Gia_VtaSendCancel( Vta_Man_t * p, int fVerbose )
1405 {
1406  extern int Gia_ManToBridgeBadAbs( FILE * pFile );
1407  assert( Abc_FrameIsBridgeMode() );
1408 // if ( fVerbose )
1409 // Abc_Print( 1, "Cancelling previously sent model...\n" );
1410  Gia_ManToBridgeBadAbs( stdout );
1411 }
1412 
1413 /**Function*************************************************************
1414 
1415  Synopsis [Send abstracted model or send cancel.]
1416 
1417  Description [Counter-example will be sent automatically when &vta terminates.]
1418 
1419  SideEffects []
1420 
1421  SeeAlso []
1422 
1423 ***********************************************************************/
1424 void Gia_VtaDumpAbsracted( Vta_Man_t * p, int fVerbose )
1425 {
1426  char * pFileNameDef = "vabs.aig";
1427  char * pFileName = p->pPars->pFileVabs ? p->pPars->pFileVabs : pFileNameDef;
1428  Gia_Man_t * pAbs;
1429  if ( fVerbose )
1430  Abc_Print( 1, "Dumping abstracted model into file \"%s\"...\n", pFileName );
1431  // create obj classes
1432  Vec_IntFreeP( &p->pGia->vObjClasses );
1433  p->pGia->vObjClasses = Gia_VtaFramesToAbs( (Vec_Vec_t *)p->vCores );
1434  // create gate classes
1435  Vec_IntFreeP( &p->pGia->vGateClasses );
1436  p->pGia->vGateClasses = Gia_VtaConvertToGla( p->pGia, p->pGia->vObjClasses );
1437  Vec_IntFreeP( &p->pGia->vObjClasses );
1438  // create abstrated model
1439  pAbs = Gia_ManDupAbsGates( p->pGia, p->pGia->vGateClasses );
1440  Vec_IntFreeP( &p->pGia->vGateClasses );
1441  // send it out
1442  Gia_AigerWrite( pAbs, pFileName, 0, 0 );
1443  Gia_ManStop( pAbs );
1444 }
1445 
1446 
1447 /**Function*************************************************************
1448 
1449  Synopsis [Print memory report.]
1450 
1451  Description []
1452 
1453  SideEffects []
1454 
1455  SeeAlso []
1456 
1457 ***********************************************************************/
1458 void Gia_VtaPrintMemory( Vta_Man_t * p )
1459 {
1460  double memTot = 0;
1461  double memAig = Gia_ManObjNum(p->pGia) * sizeof(Gia_Obj_t);
1462  double memSat = sat_solver2_memory( p->pSat, 1 );
1463  double memPro = sat_solver2_memory_proof( p->pSat );
1464  double memMap = p->nObjsAlloc * sizeof(Vta_Obj_t) + p->nBins * sizeof(int);
1465  double memOth = sizeof(Vta_Man_t);
1466  memOth += Vec_IntCap(p->vOrder) * sizeof(int);
1467  memOth += Vec_VecMemoryInt( (Vec_Vec_t *)p->vFrames );
1468  memOth += Vec_BitCap(p->vSeenGla) * sizeof(int);
1469  memOth += Vec_VecMemoryInt( (Vec_Vec_t *)p->vCores );
1470  memOth += Vec_IntCap(p->vAddedNew) * sizeof(int);
1471  memTot = memAig + memSat + memPro + memMap + memOth;
1472  ABC_PRMP( "Memory: AIG ", memAig, memTot );
1473  ABC_PRMP( "Memory: SAT ", memSat, memTot );
1474  ABC_PRMP( "Memory: Proof ", memPro, memTot );
1475  ABC_PRMP( "Memory: Map ", memMap, memTot );
1476  ABC_PRMP( "Memory: Other ", memOth, memTot );
1477  ABC_PRMP( "Memory: TOTAL ", memTot, memTot );
1478 }
1479 
1480 
1481 /**Function*************************************************************
1482 
1483  Synopsis [Collect nodes/flops involved in different timeframes.]
1484 
1485  Description []
1486 
1487  SideEffects []
1488 
1489  SeeAlso []
1490 
1491 ***********************************************************************/
1492 int Gia_VtaPerformInt( Gia_Man_t * pAig, Abs_Par_t * pPars )
1493 {
1494  Vta_Man_t * p;
1495  Vec_Int_t * vCore;
1496  Abc_Cex_t * pCex = NULL;
1497  int i, f, nConfls, Status, nObjOld, RetValue = -1, nCountNoChange = 0, fOneIsSent = 0;
1498  abctime clk = Abc_Clock(), clk2;
1499  // preconditions
1500  assert( Gia_ManPoNum(pAig) == 1 );
1501  assert( pPars->nFramesMax == 0 || pPars->nFramesStart <= pPars->nFramesMax );
1502  if ( Gia_ObjIsConst0(Gia_ObjFanin0(Gia_ManPo(pAig,0))) )
1503  {
1504  if ( !Gia_ObjFaninC0(Gia_ManPo(pAig,0)) )
1505  {
1506  printf( "Sequential miter is trivially UNSAT.\n" );
1507  return 1;
1508  }
1509  ABC_FREE( pAig->pCexSeq );
1510  pAig->pCexSeq = Abc_CexMakeTriv( Gia_ManRegNum(pAig), Gia_ManPiNum(pAig), 1, 0 );
1511  printf( "Sequential miter is trivially SAT.\n" );
1512  return 0;
1513  }
1514 
1515  // compute intial abstraction
1516  if ( pAig->vObjClasses == NULL )
1517  {
1518  pAig->vObjClasses = Vec_IntAlloc( 5 );
1519  Vec_IntPush( pAig->vObjClasses, 1 );
1520  Vec_IntPush( pAig->vObjClasses, 3 );
1521  Vec_IntPush( pAig->vObjClasses, 4 );
1522  Vec_IntPush( pAig->vObjClasses, Gia_ObjFaninId0p(pAig, Gia_ManPo(pAig, 0)) );
1523  }
1524  // start the manager
1525  p = Vga_ManStart( pAig, pPars );
1526  // set runtime limit
1527  if ( p->pPars->nTimeOut )
1528  sat_solver2_set_runtime_limit( p->pSat, p->pPars->nTimeOut * CLOCKS_PER_SEC + Abc_Clock() );
1529  // perform initial abstraction
1530  if ( p->pPars->fVerbose )
1531  {
1532  Abc_Print( 1, "Running variable-timeframe abstraction (VTA) with the following parameters:\n" );
1533  Abc_Print( 1, "FramePast = %d FrameMax = %d ConfMax = %d Timeout = %d RatioMin = %d %%\n",
1534  pPars->nFramesPast, pPars->nFramesMax, pPars->nConfLimit, pPars->nTimeOut, pPars->nRatioMin );
1535  Abc_Print( 1, "LearnStart = %d LearnDelta = %d LearnRatio = %d %%.\n",
1536  pPars->nLearnedStart, pPars->nLearnedDelta, pPars->nLearnedPerce );
1537 // Abc_Print( 1, "Frame %% Abs %% Confl Cex SatVar Core F0 F1 F2 ...\n" );
1538  Abc_Print( 1, " Frame %% Abs %% Confl Cex Vars Clas Lrns Core Time Mem\n" );
1539  }
1540  assert( Vec_PtrSize(p->vFrames) > 0 );
1541  for ( f = i = 0; !p->pPars->nFramesMax || f < p->pPars->nFramesMax; f++ )
1542  {
1543  int nConflsBeg = sat_solver2_nconflicts(p->pSat);
1544  p->pPars->iFrame = f;
1545  // realloc storage for abstraction marks
1546  if ( f == p->nWords * 32 )
1547  p->nWords = Vec_IntDoubleWidth( p->vSeens, p->nWords );
1548 
1549  // create bookmark to be used for rollback
1550  nObjOld = p->nObjs;
1551  sat_solver2_bookmark( p->pSat );
1552  Vec_IntClear( p->vAddedNew );
1553 
1554  // load new timeframe
1555  Vga_ManAddClausesOne( p, 0, f );
1556  if ( f < Vec_PtrSize(p->vFrames) )
1557  Vga_ManLoadSlice( p, (Vec_Int_t *)Vec_PtrEntry(p->vFrames, f), 0 );
1558  else
1559  {
1560  for ( i = 1; i <= Abc_MinInt(p->pPars->nFramesPast, f); i++ )
1561  Vga_ManLoadSlice( p, (Vec_Int_t *)Vec_PtrEntry(p->vCores, f-i), i );
1562  }
1563 
1564  // iterate as long as there are counter-examples
1565  for ( i = 0; ; i++ )
1566  {
1567  clk2 = Abc_Clock();
1568  vCore = Vta_ManUnsatCore( Vga_ManGetOutLit(p, f), p->pSat, pPars->nConfLimit, pPars->fVerbose, &Status, &nConfls );
1569  assert( (vCore != NULL) == (Status == 1) );
1570  if ( Status == -1 ) // resource limit is reached
1571  {
1572  Vga_ManRollBack( p, nObjOld );
1573  goto finish;
1574  }
1575  // check timeout
1576  if ( p->pSat->nRuntimeLimit && Abc_Clock() > p->pSat->nRuntimeLimit )
1577  {
1578  Vga_ManRollBack( p, nObjOld );
1579  goto finish;
1580  }
1581  if ( vCore != NULL )
1582  {
1583  p->timeUnsat += Abc_Clock() - clk2;
1584  break;
1585  }
1586  p->timeSat += Abc_Clock() - clk2;
1587  assert( Status == 0 );
1588  p->nCexes++;
1589  // perform the refinement
1590  clk2 = Abc_Clock();
1591  pCex = Vta_ManRefineAbstraction( p, f );
1592  p->timeCex += Abc_Clock() - clk2;
1593  if ( pCex != NULL )
1594  goto finish;
1595  // print the result (do not count it towards change)
1596  Vta_ManAbsPrintFrame( p, NULL, f+1, sat_solver2_nconflicts(p->pSat)-nConflsBeg, i, Abc_Clock() - clk, p->pPars->fVerbose );
1597  }
1598  assert( Status == 1 );
1599  // valid core is obtained
1600  Vta_ManUnsatCoreRemap( p, vCore );
1601  Vec_IntSort( vCore, 1 );
1602  // update the SAT solver
1603  sat_solver2_rollback( p->pSat );
1604  // update storage
1605  Vga_ManRollBack( p, nObjOld );
1606  // load this timeframe
1607  Vga_ManLoadSlice( p, vCore, 0 );
1608  Vec_IntFree( vCore );
1609 
1610  // run SAT solver
1611  clk2 = Abc_Clock();
1612  vCore = Vta_ManUnsatCore( Vga_ManGetOutLit(p, f), p->pSat, pPars->nConfLimit, p->pPars->fVerbose, &Status, &nConfls );
1613  p->timeUnsat += Abc_Clock() - clk2;
1614  assert( (vCore != NULL) == (Status == 1) );
1615  if ( Status == -1 ) // resource limit is reached
1616  break;
1617  if ( Status == 0 )
1618  {
1619  Vta_ManSatVerify( p );
1620  // make sure, there was no initial abstraction (otherwise, it was invalid)
1621  assert( pAig->vObjClasses == NULL && f < p->pPars->nFramesStart );
1622  pCex = Vga_ManDeriveCex( p );
1623  break;
1624  }
1625  // add the core
1626  Vta_ManUnsatCoreRemap( p, vCore );
1627  // add in direct topological order
1628  Vec_IntSort( vCore, 1 );
1629  Vec_PtrPush( p->vCores, vCore );
1630  // print the result
1631  if ( Vta_ManAbsPrintFrame( p, vCore, f+1, sat_solver2_nconflicts(p->pSat)-nConflsBeg, i, Abc_Clock() - clk, p->pPars->fVerbose ) )
1632  {
1633  // reset the counter of frames without change
1634  nCountNoChange = 1;
1635  p->pPars->nFramesNoChange = 0;
1636  }
1637  else if ( ++nCountNoChange == 2 ) // time to send
1638  {
1639  p->pPars->nFramesNoChange++;
1640  if ( Abc_FrameIsBridgeMode() )
1641  {
1642  // cancel old one if it was sent
1643  if ( fOneIsSent )
1644  Gia_VtaSendCancel( p, pPars->fVerbose );
1645  // send new one
1646  Gia_VtaSendAbsracted( p, pPars->fVerbose );
1647  fOneIsSent = 1;
1648  }
1649  }
1650  // dump the model
1651  if ( p->pPars->fDumpVabs && (f & 1) )
1652  {
1653  char Command[1000];
1654  Abc_FrameSetStatus( -1 );
1655  Abc_FrameSetCex( NULL );
1656  Abc_FrameSetNFrames( f+1 );
1657  sprintf( Command, "write_status %s", Extra_FileNameGenericAppend((char *)(p->pPars->pFileVabs ? p->pPars->pFileVabs : "vtabs.aig"), ".status") );
1658  Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), Command );
1659  Gia_VtaDumpAbsracted( p, pPars->fVerbose );
1660  }
1661  // check if the number of objects is below limit
1662  if ( p->nSeenGla >= Gia_ManCandNum(pAig) * (100-pPars->nRatioMin) / 100 )
1663  {
1664  Status = -1;
1665  break;
1666  }
1667  }
1668 finish:
1669  // analize the results
1670  if ( pCex == NULL )
1671  {
1672  if ( p->pPars->fVerbose && Status == -1 )
1673  printf( "\n" );
1674  if ( Vec_PtrSize(p->vCores) == 0 )
1675  Abc_Print( 1, "Abstraction is not produced because first frame is not solved. " );
1676  else
1677  {
1678  assert( Vec_PtrSize(p->vCores) > 0 );
1679 // if ( pAig->vObjClasses != NULL )
1680 // Abc_Print( 1, "Replacing the old abstraction by a new one.\n" );
1681  Vec_IntFreeP( &pAig->vObjClasses );
1682  pAig->vObjClasses = Gia_VtaFramesToAbs( (Vec_Vec_t *)p->vCores );
1683  if ( Status == -1 )
1684  {
1685  if ( p->pPars->nTimeOut && Abc_Clock() >= p->pSat->nRuntimeLimit )
1686  Abc_Print( 1, "Timeout %d sec in frame %d with a %d-stable abstraction. ", p->pPars->nTimeOut, f, p->pPars->nFramesNoChange );
1687  else if ( pPars->nConfLimit && sat_solver2_nconflicts(p->pSat) >= pPars->nConfLimit )
1688  Abc_Print( 1, "Exceeded %d conflicts in frame %d with a %d-stable abstraction. ", pPars->nConfLimit, f, p->pPars->nFramesNoChange );
1689  else if ( p->nSeenGla >= Gia_ManCandNum(pAig) * (100-pPars->nRatioMin) / 100 )
1690  Abc_Print( 1, "The ratio of abstracted objects is less than %d %% in frame %d. ", pPars->nRatioMin, f );
1691  else
1692  Abc_Print( 1, "Abstraction stopped for unknown reason in frame %d. ", f );
1693  }
1694  else
1695  {
1696  p->pPars->iFrame++;
1697  Abc_Print( 1, "VTA completed %d frames with a %d-stable abstraction. ", f, p->pPars->nFramesNoChange );
1698  }
1699  }
1700  }
1701  else
1702  {
1703  if ( p->pPars->fVerbose )
1704  printf( "\n" );
1705  ABC_FREE( p->pGia->pCexSeq );
1706  p->pGia->pCexSeq = pCex;
1707  if ( !Gia_ManVerifyCex( p->pGia, pCex, 0 ) )
1708  Abc_Print( 1, " Gia_VtaPerform(): CEX verification has failed!\n" );
1709  Abc_Print( 1, "Counter-example detected in frame %d. ", f );
1710  p->pPars->iFrame = pCex->iFrame - 1;
1711  Vec_IntFreeP( &pAig->vObjClasses );
1712  RetValue = 0;
1713  }
1714  Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
1715 
1716  if ( p->pPars->fVerbose )
1717  {
1718  p->timeOther = (Abc_Clock() - clk) - p->timeUnsat - p->timeSat - p->timeCex;
1719  ABC_PRTP( "Runtime: Solver UNSAT", p->timeUnsat, Abc_Clock() - clk );
1720  ABC_PRTP( "Runtime: Solver SAT ", p->timeSat, Abc_Clock() - clk );
1721  ABC_PRTP( "Runtime: Refinement ", p->timeCex, Abc_Clock() - clk );
1722  ABC_PRTP( "Runtime: Other ", p->timeOther, Abc_Clock() - clk );
1723  ABC_PRTP( "Runtime: TOTAL ", Abc_Clock() - clk, Abc_Clock() - clk );
1724  Gia_VtaPrintMemory( p );
1725  }
1726 
1727  Vga_ManStop( p );
1728  fflush( stdout );
1729  return RetValue;
1730 }
1731 
1732 /**Function*************************************************************
1733 
1734  Synopsis [Collect nodes/flops involved in different timeframes.]
1735 
1736  Description []
1737 
1738  SideEffects []
1739 
1740  SeeAlso []
1741 
1742 ***********************************************************************/
1743 int Gia_VtaPerform( Gia_Man_t * pAig, Abs_Par_t * pPars )
1744 {
1745  int RetValue = -1;
1746  if ( pAig->vObjClasses == NULL && pPars->fUseRollback )
1747  {
1748  int nFramesMaxOld = pPars->nFramesMax;
1749  pPars->nFramesMax = pPars->nFramesStart;
1750  RetValue = Gia_VtaPerformInt( pAig, pPars );
1751  pPars->nFramesMax = nFramesMaxOld;
1752  }
1753  if ( RetValue == 0 )
1754  return RetValue;
1755  return Gia_VtaPerformInt( pAig, pPars );
1756 }
1757 
1758 ////////////////////////////////////////////////////////////////////////
1759 /// END OF FILE ///
1760 ////////////////////////////////////////////////////////////////////////
1761 
1762 
1763 ABC_NAMESPACE_IMPL_END
1764 
memset
char * memset()
Vga_ManStop
void Vga_ManStop(Vta_Man_t *p)
Definition: absVta.c:1033
sat_solver2_nlearnts
static int sat_solver2_nlearnts(sat_solver2 *s)
Definition: satSolver2.h:200
Vga_ManDelete
static void Vga_ManDelete(Vta_Man_t *p, int iObj, int iFrame)
Definition: absVta.c:321
Vta_Man_t_::nSeenGla
int nSeenGla
Definition: absVta.c:67
Vta_Obj_t_::Prio
unsigned Prio
Definition: absVta.c:39
Vta_ObjId
static int Vta_ObjId(Vta_Man_t *p, Vta_Obj_t *pObj)
Definition: absVta.c:105
Vta_Man_t_::nBins
int nBins
Definition: absVta.c:54
VTA_LARGE
#define VTA_LARGE
Definition: absVta.c:27
Abc_FrameIsBridgeMode
ABC_DLL int Abc_FrameIsBridgeMode()
Definition: mainFrame.c:94
Vga_ManLoadSlice
void Vga_ManLoadSlice(Vta_Man_t *p, Vec_Int_t *vOne, int Lift)
Definition: absVta.c:1313
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
Vta_Man_t
struct Vta_Man_t_ Vta_Man_t
Definition: absVta.c:45
Abc_PrimeCudd
static int Abc_PrimeCudd(unsigned int p)
Definition: abc_global.h:383
Vta_Man_t_
Definition: absVta.c:46
Vga_ManGetOutLit
static int Vga_ManGetOutLit(Vta_Man_t *p, int f)
Definition: absVta.c:1062
sat_solver2_t::nLearntMax
int nLearntMax
Definition: satSolver2.h:118
Vta_ManCollectNodes
Vec_Int_t * Vta_ManCollectNodes(Vta_Man_t *p, int f)
Definition: absVta.c:487
sat_solver2_t::nLearntStart
int nLearntStart
Definition: satSolver2.h:119
Vta_Man_t_::nObjsAlloc
int nObjsAlloc
Definition: absVta.c:53
Gia_ManStop
void Gia_ManStop(Gia_Man_t *p)
Definition: giaMan.c:77
sat_solver2_nclauses
static int sat_solver2_nclauses(sat_solver2 *s)
Definition: satSolver2.h:195
Gia_ManVerifyCex
int Gia_ManVerifyCex(Gia_Man_t *pAig, Abc_Cex_t *p, int fDualOut)
DECLARATIONS ///.
Definition: giaCex.c:44
Gia_VtaSendCancel
void Gia_VtaSendCancel(Vta_Man_t *p, int fVerbose)
Definition: absVta.c:1404
Vec_Vec_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Vec_t_ Vec_Vec_t
INCLUDES ///.
Definition: vecVec.h:42
Sat_ProofCore
void * Sat_ProofCore(sat_solver2 *s)
Definition: satSolver2.c:1985
VTA_VAR1
#define VTA_VAR1
Definition: absVta.c:84
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_VtaDumpAbsracted
void Gia_VtaDumpAbsracted(Vta_Man_t *p, int fVerbose)
Definition: absVta.c:1424
Vec_VecMemoryInt
static double Vec_VecMemoryInt(Vec_Vec_t *p)
Definition: vecVec.h:304
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Vec_IntDoubleWidth
int Vec_IntDoubleWidth(Vec_Int_t *p, int nWords)
Definition: absVta.c:241
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
Vga_ManFindOrAdd
static Vta_Obj_t * Vga_ManFindOrAdd(Vta_Man_t *p, int iObj, int iFrame)
Definition: absVta.c:289
Cmd_CommandExecute
int Cmd_CommandExecute(void *pAbc, char *pCommandLine)
Vta_Man_t_::vSeenGla
Vec_Bit_t * vSeenGla
Definition: absVta.c:66
Abc_InfoHasBit
static int Abc_InfoHasBit(unsigned *p, int i)
Definition: abc_global.h:258
Abc_CexAlloc
ABC_NAMESPACE_IMPL_START Abc_Cex_t * Abc_CexAlloc(int nRegs, int nRealPis, int nFrames)
DECLARATIONS ///.
Definition: utilCex.c:51
l_Undef
#define l_Undef
Definition: SolverTypes.h:86
sat_solver2_memory_proof
double sat_solver2_memory_proof(sat_solver2 *s)
Definition: satSolver2.c:1733
Gia_Man_t_::vObjClasses
Vec_Int_t * vObjClasses
Definition: gia.h:142
Gia_ManPo
static Gia_Obj_t * Gia_ManPo(Gia_Man_t *p, int v)
Definition: gia.h:406
ABC_REALLOC
#define ABC_REALLOC(type, obj, num)
Definition: abc_global.h:233
Vga_ManHash
static int Vga_ManHash(int iObj, int iFrame, int nBins)
Definition: absVta.c:269
Vta_ValIs0
static int Vta_ValIs0(Vta_Obj_t *pThis, int fCompl)
Definition: absVta.c:87
Vta_ManForEachObjObjVecReverse
#define Vta_ManForEachObjObjVecReverse(vVec, p, pObj, pObjG, i)
Definition: absVta.c:121
Abc_FrameIsBatchMode
ABC_DLL int Abc_FrameIsBatchMode()
Definition: mainFrame.c:92
Vta_Man_t_::timeSat
abctime timeSat
Definition: absVta.c:74
Vec_VecForEachLevelInt
#define Vec_VecForEachLevelInt(vGlob, vVec, i)
Definition: vecVec.h:71
sat_solver2_delete
void sat_solver2_delete(sat_solver2 *s)
Definition: satSolver2.c:1225
sat_solver2_t
Definition: satSolver2.h:90
VTA_VARX
#define VTA_VARX
Definition: absVta.c:85
Gia_ManDupAbsGates
Gia_Man_t * Gia_ManDupAbsGates(Gia_Man_t *p, Vec_Int_t *vGateClasses)
Definition: absDup.c:220
Gia_ObjIsConst0
static int Gia_ObjIsConst0(Gia_Obj_t *pObj)
Definition: gia.h:430
Abc_Var2Lit
static int Abc_Var2Lit(int Var, int fCompl)
Definition: abc_global.h:263
Vec_SetAlloc
static Vec_Set_t * Vec_SetAlloc(int nPageSize)
Definition: vecSet.h:128
Vga_ManDeriveCex
Abc_Cex_t * Vga_ManDeriveCex(Vta_Man_t *p)
Definition: absVta.c:342
sat_solver2_t::nLearntDelta
int nLearntDelta
Definition: satSolver2.h:120
Vta_Man_t_::timeUnsat
abctime timeUnsat
Definition: absVta.c:75
Vta_Man_t_::nObjs
int nObjs
Definition: absVta.c:52
Vec_PtrSort
static void Vec_PtrSort(Vec_Ptr_t *p, int(*Vec_PtrSortCompare)()) ___unused
Definition: vecPtr.h:851
Gia_ObjFaninId1p
static int Gia_ObjFaninId1p(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:464
Gia_ManToBridgeBadAbs
int Gia_ManToBridgeBadAbs(FILE *pFile)
Definition: utilBridge.c:199
Vec_PtrPush
static void Vec_PtrPush(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:606
Vta_ManDeriveAbsAll
static Vec_Int_t * Vta_ManDeriveAbsAll(Vec_Int_t *p, int nWords)
Definition: absVta.c:212
l_True
#define l_True
Definition: SolverTypes.h:84
Vta_Man_t_::nWords
int nWords
Definition: absVta.c:62
Gia_VtaFramesToAbs
Vec_Int_t * Gia_VtaFramesToAbs(Vec_Vec_t *vFrames)
Definition: absVta.c:180
sat_solver2_new
sat_solver2 * sat_solver2_new(void)
Definition: satSolver2.c:1109
Vta_ManObj
static Vta_Obj_t * Vta_ManObj(Vta_Man_t *p, int i)
Definition: absVta.c:104
Vta_ManSatVerify
void Vta_ManSatVerify(Vta_Man_t *p)
Definition: absVta.c:512
Gia_VtaConvertToGla
Vec_Int_t * Gia_VtaConvertToGla(Gia_Man_t *p, Vec_Int_t *vVta)
Definition: absUtil.c:78
Vta_ManRefineAbstraction
Abc_Cex_t * Vta_ManRefineAbstraction(Vta_Man_t *p, int f)
Definition: absVta.c:581
Vta_Man_t_::timeCex
abctime timeCex
Definition: absVta.c:76
Gia_VtaAbsToFrames
Vec_Ptr_t * Gia_VtaAbsToFrames(Vec_Int_t *vAbs)
FUNCTION DEFINITIONS ///.
Definition: absVta.c:148
Abc_FrameSetStatus
ABC_DLL void Abc_FrameSetStatus(int Status)
Definition: mainFrame.c:88
Vec_BitFreeP
static void Vec_BitFreeP(Vec_Bit_t **p)
Definition: vecBit.h:184
Vec_BitWriteEntry
static void Vec_BitWriteEntry(Vec_Bit_t *p, int i, int Entry)
Definition: vecBit.h:304
Abc_Clock
static abctime Abc_Clock()
Definition: abc_global.h:279
Abc_MaxInt
static int Abc_MaxInt(int a, int b)
Definition: abc_global.h:238
Vta_ManForEachObjVec
#define Vta_ManForEachObjVec(vVec, p, pObj, i)
Definition: absVta.c:114
Vec_PtrSize
static int Vec_PtrSize(Vec_Ptr_t *p)
Definition: vecPtr.h:295
Vta_ValIs1
static int Vta_ValIs1(Vta_Obj_t *pThis, int fCompl)
Definition: absVta.c:95
Vec_IntSort
static void Vec_IntSort(Vec_Int_t *p, int fReverse)
Definition: vecInt.h:1293
sat_solver2_t::stats
stats_t stats
Definition: satSolver2.h:172
nWords
int nWords
Definition: abcNpn.c:127
Gia_ManObj
static Gia_Obj_t * Gia_ManObj(Gia_Man_t *p, int v)
Definition: gia.h:402
Vta_Man_t_::nSeenAll
int nSeenAll
Definition: absVta.c:68
sat_solver2_var_value
static int sat_solver2_var_value(sat_solver2 *s, int v)
Definition: satSolver2.h:210
Gia_Obj_t_
Definition: gia.h:75
Vec_Bit_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Bit_t_ Vec_Bit_t
INCLUDES ///.
Definition: vecBit.h:42
Abc_CexMakeTriv
Abc_Cex_t * Abc_CexMakeTriv(int nRegs, int nTruePis, int nTruePos, int iFrameOut)
Definition: utilCex.c:85
Vta_ManComputeDepthIncrease
int Vta_ManComputeDepthIncrease(Vta_Obj_t **pp1, Vta_Obj_t **pp2)
Definition: absVta.c:391
ABC_PRTP
#define ABC_PRTP(a, t, T)
Definition: abc_global.h:223
sat_solver2_memory
double sat_solver2_memory(sat_solver2 *s, int fAll)
Definition: satSolver2.c:1692
Gia_VtaPerformInt
int Gia_VtaPerformInt(Gia_Man_t *pAig, Abs_Par_t *pPars)
Definition: absVta.c:1492
Vta_Man_t_::nObjMask
unsigned nObjMask
Definition: absVta.c:60
Abc_PrintTime
static void Abc_PrintTime(int level, const char *pStr, abctime time)
Definition: abc_global.h:367
Gia_Obj_t
struct Gia_Obj_t_ Gia_Obj_t
Definition: gia.h:74
Vec_IntWriteEntry
static void Vec_IntWriteEntry(Vec_Int_t *p, int i, int Entry)
Definition: bblif.c:285
Gia_ManAndNum
static int Gia_ManAndNum(Gia_Man_t *p)
Definition: gia.h:389
Vta_Man_t_::vOrder
Vec_Int_t * vOrder
Definition: absVta.c:57
Abc_MinInt
static int Abc_MinInt(int a, int b)
Definition: abc_global.h:239
Vec_IntStart
static Vec_Int_t * Vec_IntStart(int nSize)
Definition: bblif.c:172
Vta_Obj_t_::iNext
int iNext
Definition: absVta.c:38
Vec_BitStart
static Vec_Bit_t * Vec_BitStart(int nSize)
Definition: vecBit.h:102
Gia_ObjFanin0
static Gia_Obj_t * Gia_ObjFanin0(Gia_Obj_t *pObj)
Definition: gia.h:454
Vta_Obj_t_::Value
unsigned Value
Definition: absVta.c:40
Vta_ManCollectNodes_rec
void Vta_ManCollectNodes_rec(Vta_Man_t *p, Vta_Obj_t *pThis, Vec_Int_t *vOrder)
Definition: absVta.c:471
Vec_IntAlloc
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
Vta_ManProfileAddition
void Vta_ManProfileAddition(Vta_Man_t *p, Vec_Int_t *vTermsToAdd)
Definition: absVta.c:557
Vec_PtrEntryLast
static void * Vec_PtrEntryLast(Vec_Ptr_t *p)
Definition: vecPtr.h:413
Vta_Obj_t_
Definition: absVta.c:34
VTA_VAR0
#define VTA_VAR0
Definition: absVta.c:83
sat_solver2_simplify
int sat_solver2_simplify(sat_solver2 *s)
Definition: satSolver2.c:996
Vta_Obj_t_::fAdded
unsigned fAdded
Definition: absVta.c:41
sat_solver2_rollback
void sat_solver2_rollback(sat_solver2 *s)
Definition: satSolver2.c:1586
Gia_ObjIsRo
static int Gia_ObjIsRo(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:443
sat_solver2_add_constraint
static int sat_solver2_add_constraint(sat_solver2 *pSat, int iVar, int iVar2, int fCompl, int fMark, int Id)
Definition: satSolver2.h:354
Abc_FrameSetCex
ABC_DLL void Abc_FrameSetCex(Abc_Cex_t *pCex)
Definition: mainFrame.c:86
Gia_Man_t_::vGateClasses
Vec_Int_t * vGateClasses
Definition: gia.h:141
sat_solver2_t::nDBreduces
int nDBreduces
Definition: satSolver2.h:122
Gia_ObjRoToRi
static Gia_Obj_t * Gia_ObjRoToRi(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:446
Vta_Man_t_::pGia
Gia_Man_t * pGia
Definition: absVta.c:49
Vec_IntEntry
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
Vta_ManForEachObj
#define Vta_ManForEachObj(p, pObj, i)
Definition: absVta.c:107
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
Abc_FrameGetGlobalFrame
void * Abc_FrameGetGlobalFrame()
Definition: mainFrame.c:593
if
if(last==0)
Definition: sparse_int.h:34
Vec_IntPush
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
Vta_ObjPreds
static void Vta_ObjPreds(Vta_Man_t *p, Vta_Obj_t *pThis, Gia_Obj_t *pObj, Vta_Obj_t **ppThis0, Vta_Obj_t **ppThis1)
Definition: absVta.c:438
sprintf
char * sprintf()
Counter
static int Counter
Definition: extraBddMisc.c:1877
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
sat_solver2_bookmark
static void sat_solver2_bookmark(sat_solver2 *s)
Definition: satSolver2.h:248
Vec_IntCap
static int Vec_IntCap(Vec_Int_t *p)
Definition: vecInt.h:368
Gia_VtaSendAbsracted
void Gia_VtaSendAbsracted(Vta_Man_t *p, int fVerbose)
Definition: absVta.c:1384
Vta_Man_t_::vFrames
Vec_Ptr_t * vFrames
Definition: absVta.c:61
Abc_Print
static void Abc_Print(int level, const char *format,...)
Definition: abc_global.h:313
Vta_ManForEachObjObj
#define Vta_ManForEachObjObj(p, pObjVta, pObjGia, i)
Definition: absVta.c:109
Gia_VtaPerform
int Gia_VtaPerform(Gia_Man_t *pAig, Abs_Par_t *pPars)
Definition: absVta.c:1743
Gia_AigerWrite
void Gia_AigerWrite(Gia_Man_t *p, char *pFileName, int fWriteSymbols, int fCompact)
Definition: giaAiger.c:1024
Vec_BitCap
static int Vec_BitCap(Vec_Bit_t *p)
Definition: vecBit.h:255
Vta_ManForEachObjObjVec
#define Vta_ManForEachObjObjVec(vVec, p, pObj, pObjG, i)
Definition: absVta.c:119
Vta_Man_t_::vCores
Vec_Ptr_t * vCores
Definition: absVta.c:70
Vta_Obj_t_::fVisit
unsigned fVisit
Definition: absVta.c:42
Vga_ManLookup
static int * Vga_ManLookup(Vta_Man_t *p, int iObj, int iFrame)
Definition: absVta.c:273
Vga_ManStart
Vta_Man_t * Vga_ManStart(Gia_Man_t *pGia, Abs_Par_t *pPars)
Definition: absVta.c:983
Vta_Obj_t
struct Vta_Obj_t_ Vta_Obj_t
DECLARATIONS ///.
Definition: absVta.c:33
sat_solver2_t::nConfLimit
ABC_INT64_T nConfLimit
Definition: satSolver2.h:173
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
sat_solver2_add_buffer
static int sat_solver2_add_buffer(sat_solver2 *pSat, int iVarA, int iVarB, int fCompl, int fMark, int Id)
Definition: satSolver2.h:275
stats_t::conflicts
ABC_INT64_T conflicts
Definition: satVec.h:154
Vec_IntEntryLast
static int Vec_IntEntryLast(Vec_Int_t *p)
Definition: bblif.c:319
Vta_Obj_t_::iObj
int iObj
Definition: absVta.c:36
Vec_IntSize
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
Vta_Man_t_::nCexes
int nCexes
Definition: absVta.c:63
Abc_FrameSetNFrames
ABC_DLL void Abc_FrameSetNFrames(int nFrames)
Definition: mainFrame.c:87
Vec_PtrAlloc
static Vec_Ptr_t * Vec_PtrAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: vecPtr.h:83
sat_solver2_add_and
static int sat_solver2_add_and(sat_solver2 *pSat, int iVar, int iVar0, int iVar1, int fCompl0, int fCompl1, int fMark, int Id)
Definition: satSolver2.h:294
sat_solver2_t::pPrf1
Vec_Set_t * pPrf1
Definition: satSolver2.h:162
Vta_Man_t_::timeOther
abctime timeOther
Definition: absVta.c:77
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
Gia_Man_t_
Definition: gia.h:95
ABC_PRMP
#define ABC_PRMP(a, f, F)
Definition: abc_global.h:227
Abc_Base2Log
static int Abc_Base2Log(unsigned n)
Definition: abc_global.h:251
Vta_Man_t_::pSat
sat_solver2 * pSat
Definition: absVta.c:71
sat_solver2_nvars
static int sat_solver2_nvars(sat_solver2 *s)
Definition: satSolver2.h:190
Vec_VecSizeSize
static int Vec_VecSizeSize(Vec_Vec_t *p)
Definition: vecVec.h:417
Gia_ObjIsAnd
static int Gia_ObjIsAnd(Gia_Obj_t *pObj)
Definition: gia.h:422
Vec_BitEntry
static int Vec_BitEntry(Vec_Bit_t *p, int i)
Definition: vecBit.h:287
Gia_ManToBridgeAbsNetlist
int Gia_ManToBridgeAbsNetlist(FILE *pFile, void *p, int pkg_type)
Definition: utilBridge.c:189
Vta_Obj_t_::iFrame
int iFrame
Definition: absVta.c:37
sat_solver2_add_const
static int sat_solver2_add_const(sat_solver2 *pSat, int iVar, int fCompl, int fMark, int Id)
Definition: satSolver2.h:263
Vga_ManRollBack
void Vga_ManRollBack(Vta_Man_t *p, int nObjOld)
Definition: absVta.c:1355
ABC_CALLOC
#define ABC_CALLOC(type, num)
Definition: abc_global.h:230
Vec_VecSize
static int Vec_VecSize(Vec_Vec_t *p)
Definition: vecVec.h:222
l_False
#define l_False
Definition: SolverTypes.h:85
Gia_ObjFaninId0p
static int Gia_ObjFaninId0p(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:463
sat_solver2_solve
int sat_solver2_solve(sat_solver2 *s, lit *begin, lit *end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal)
Definition: satSolver2.c:1835
Vta_ManUnsatCore
Vec_Int_t * Vta_ManUnsatCore(int iLit, sat_solver2 *pSat, int nConfMax, int fVerbose, int *piRetValue, int *pnConfls)
Definition: absVta.c:1083
Vta_Man_t_::nObjAdded
int nObjAdded
Definition: absVta.c:64
Vec_VecFreeP
static void Vec_VecFreeP(Vec_Vec_t **p)
Definition: vecVec.h:367
assert
#define assert(ex)
Definition: util_old.h:213
Extra_FileNameGenericAppend
char * Extra_FileNameGenericAppend(char *pBase, char *pSuffix)
Definition: extraUtilFile.c:185
Vec_IntEntryP
static int * Vec_IntEntryP(Vec_Int_t *p, int i)
Definition: vecInt.h:417
Vta_Man_t_::pBins
int * pBins
Definition: absVta.c:55
Vec_IntForEachEntryStartStop
#define Vec_IntForEachEntryStartStop(vVec, Entry, i, Start, Stop)
Definition: vecInt.h:60
BRIDGE_ABS_NETLIST
#define BRIDGE_ABS_NETLIST
Definition: abc_global.h:295
Abc_Cex_t
typedefABC_NAMESPACE_HEADER_START struct Abc_Cex_t_ Abc_Cex_t
INCLUDES ///.
Definition: utilCex.h:39
Vta_Man_t_::vAddedNew
Vec_Int_t * vAddedNew
Definition: absVta.c:72
Vta_ManObjIsUsed
int Vta_ManObjIsUsed(Vta_Man_t *p, int iObj)
Definition: absVta.c:417
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_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition: vecPtr.h:55
Gia_ManPiNum
static int Gia_ManPiNum(Gia_Man_t *p)
Definition: gia.h:385
Vta_Man_t_::pObjs
Vta_Obj_t * pObjs
Definition: absVta.c:56
Vta_Man_t_::vSeens
Vec_Int_t * vSeens
Definition: absVta.c:65
Gia_VtaPrintMemory
void Gia_VtaPrintMemory(Vta_Man_t *p)
Definition: absVta.c:1458
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_ObjIsCi
static int Gia_ObjIsCi(Gia_Obj_t *pObj)
Definition: gia.h:420
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
sat_solver2_t::nRuntimeLimit
abctime nRuntimeLimit
Definition: satSolver2.h:175
Vta_Man_t_::nObjBits
int nObjBits
Definition: absVta.c:59
Abc_PrintInt
static void Abc_PrintInt(int i)
Definition: abc_global.h:342
Vga_ManFind
static Vta_Obj_t * Vga_ManFind(Vta_Man_t *p, int iObj, int iFrame)
Definition: absVta.c:284
sat_solver2_nconflicts
static int sat_solver2_nconflicts(sat_solver2 *s)
Definition: satSolver2.h:205
sat_solver2_t::nLearntRatio
int nLearntRatio
Definition: satSolver2.h:121
Vga_ManPrintCore
void Vga_ManPrintCore(Vta_Man_t *p, Vec_Int_t *vCore, int Lift)
Definition: absVta.c:1332
Gia_ObjCioId
static int Gia_ObjCioId(Gia_Obj_t *pObj)
Definition: gia.h:411
Gia_ManObjNum
static int Gia_ManObjNum(Gia_Man_t *p)
Definition: gia.h:388
Abs_Par_t
typedefABC_NAMESPACE_HEADER_START struct Abs_Par_t_ Abs_Par_t
INCLUDES ///.
Definition: abs.h:46
sat_solver2_set_runtime_limit
static abctime sat_solver2_set_runtime_limit(sat_solver2 *s, abctime Limit)
Definition: satSolver2.h:234
Vec_PtrFree
static void Vec_PtrFree(Vec_Ptr_t *p)
Definition: vecPtr.h:223
Vta_ManUnsatCoreRemap
void Vta_ManUnsatCoreRemap(Vta_Man_t *p, Vec_Int_t *vCore)
Definition: absVta.c:368
Gia_ObjIsPi
static int Gia_ObjIsPi(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:441
Vta_Man_t_::pPars
Abs_Par_t * pPars
Definition: absVta.c:50
Vta_ManAbsPrintFrame
int Vta_ManAbsPrintFrame(Vta_Man_t *p, Vec_Int_t *vCore, int nFrames, int nConfls, int nCexes, abctime Time, int fVerbose)
Definition: absVta.c:1143
Vga_ManAddClausesOne
void Vga_ManAddClausesOne(Vta_Man_t *p, int iObj, int iFrame)
Definition: absVta.c:1254
Gia_Man_t_::pCexSeq
Abc_Cex_t * pCexSeq
Definition: gia.h:136
Gia_ManRegNum
static int Gia_ManRegNum(Gia_Man_t *p)
Definition: gia.h:387