abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
pdrCore.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [pdrCore.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [Property driven reachability.]
8 
9  Synopsis [Core procedures.]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - November 20, 2010.]
16 
17  Revision [$Id: pdrCore.c,v 1.00 2010/11/20 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "pdrInt.h"
22 
23 ABC_NAMESPACE_IMPL_START
24 
25 
26 ////////////////////////////////////////////////////////////////////////
27 /// DECLARATIONS ///
28 ////////////////////////////////////////////////////////////////////////
29 
30 extern int Gia_ManToBridgeResult( FILE * pFile, int Result, Abc_Cex_t * pCex, int iPoProved );
31 extern int Gia_ManToBridgeAbort( FILE * pFile, int Size, unsigned char * pBuffer );
32 
33 ////////////////////////////////////////////////////////////////////////
34 /// FUNCTION DEFINITIONS ///
35 ////////////////////////////////////////////////////////////////////////
36 
37 /**Function*************************************************************
38 
39  Synopsis [Returns 1 if the state could be blocked.]
40 
41  Description []
42 
43  SideEffects []
44 
45  SeeAlso []
46 
47 ***********************************************************************/
48 void Pdr_ManSetDefaultParams( Pdr_Par_t * pPars )
49 {
50  memset( pPars, 0, sizeof(Pdr_Par_t) );
51 // pPars->iOutput = -1; // zero-based output number
52  pPars->nRecycle = 300; // limit on vars for recycling
53  pPars->nFrameMax = 10000; // limit on number of timeframes
54  pPars->nTimeOut = 0; // timeout in seconds
55  pPars->nTimeOutGap = 0; // timeout in seconds since the last solved
56  pPars->nConfLimit = 0; // limit on SAT solver conflicts
57  pPars->nRestLimit = 0; // limit on the number of proof-obligations
58  pPars->fTwoRounds = 0; // use two rounds for generalization
59  pPars->fMonoCnf = 0; // monolythic CNF
60  pPars->fDumpInv = 0; // dump inductive invariant
61  pPars->fShortest = 0; // forces bug traces to be shortest
62  pPars->fVerbose = 0; // verbose output
63  pPars->fVeryVerbose = 0; // very verbose output
64  pPars->fNotVerbose = 0; // not printing line-by-line progress
65  pPars->iFrame = -1; // explored up to this frame
66  pPars->nFailOuts = 0; // the number of disproved outputs
67  pPars->nDropOuts = 0; // the number of timed out outputs
68  pPars->timeLastSolved = 0; // last one solved
69 }
70 
71 /**Function*************************************************************
72 
73  Synopsis [Reduces clause using analyzeFinal.]
74 
75  Description [Assumes that the SAT solver just terminated an UNSAT call.]
76 
77  SideEffects []
78 
79  SeeAlso []
80 
81 ***********************************************************************/
82 Pdr_Set_t * Pdr_ManReduceClause( Pdr_Man_t * p, int k, Pdr_Set_t * pCube )
83 {
84  Pdr_Set_t * pCubeMin;
85  Vec_Int_t * vLits;
86  int i, Entry, nCoreLits, * pCoreLits;
87  // get relevant SAT literals
88  nCoreLits = sat_solver_final(Pdr_ManSolver(p, k), &pCoreLits);
89  // translate them into register literals and remove auxiliary
90  vLits = Pdr_ManLitsToCube( p, k, pCoreLits, nCoreLits );
91  // skip if there is no improvement
92  if ( Vec_IntSize(vLits) == pCube->nLits )
93  return NULL;
94  assert( Vec_IntSize(vLits) < pCube->nLits );
95  // if the cube overlaps with init, add any literal
96  Vec_IntForEachEntry( vLits, Entry, i )
97  if ( lit_sign(Entry) == 0 ) // positive literal
98  break;
99  if ( i == Vec_IntSize(vLits) ) // only negative literals
100  {
101  // add the first positive literal
102  for ( i = 0; i < pCube->nLits; i++ )
103  if ( lit_sign(pCube->Lits[i]) == 0 ) // positive literal
104  {
105  Vec_IntPush( vLits, pCube->Lits[i] );
106  break;
107  }
108  assert( i < pCube->nLits );
109  }
110  // generate a starting cube
111  pCubeMin = Pdr_SetCreateSubset( pCube, Vec_IntArray(vLits), Vec_IntSize(vLits) );
112  assert( !Pdr_SetIsInit(pCubeMin, -1) );
113 /*
114  // make sure the cube works
115  {
116  int RetValue;
117  RetValue = Pdr_ManCheckCube( p, k, pCubeMin, NULL, 0 );
118  assert( RetValue );
119  }
120 */
121  return pCubeMin;
122 }
123 
124 /**Function*************************************************************
125 
126  Synopsis [Returns 1 if the state could be blocked.]
127 
128  Description []
129 
130  SideEffects []
131 
132  SeeAlso []
133 
134 ***********************************************************************/
135 int Pdr_ManPushClauses( Pdr_Man_t * p )
136 {
137  Pdr_Set_t * pTemp, * pCubeK, * pCubeK1;
138  Vec_Ptr_t * vArrayK, * vArrayK1;
139  int i, j, k, m, RetValue = 0, RetValue2, kMax = Vec_PtrSize(p->vSolvers)-1;
140  int iStartFrame = p->pPars->fShiftStart ? p->iUseFrame : 1;
141  int Counter = 0;
142  abctime clk = Abc_Clock();
143  assert( p->iUseFrame > 0 );
144  Vec_VecForEachLevelStartStop( p->vClauses, vArrayK, k, iStartFrame, kMax )
145  {
146  Vec_PtrSort( vArrayK, (int (*)(void))Pdr_SetCompare );
147  vArrayK1 = Vec_VecEntry( p->vClauses, k+1 );
148  Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pCubeK, j )
149  {
150  Counter++;
151 
152  // remove cubes in the same frame that are contained by pCubeK
153  Vec_PtrForEachEntryStart( Pdr_Set_t *, vArrayK, pTemp, m, j+1 )
154  {
155  if ( !Pdr_SetContains( pTemp, pCubeK ) ) // pCubeK contains pTemp
156  continue;
157  Pdr_SetDeref( pTemp );
158  Vec_PtrWriteEntry( vArrayK, m, Vec_PtrEntryLast(vArrayK) );
159  Vec_PtrPop(vArrayK);
160  m--;
161  }
162 
163  // check if the clause can be moved to the next frame
164  RetValue2 = Pdr_ManCheckCube( p, k, pCubeK, NULL, 0 );
165  if ( RetValue2 == -1 )
166  return -1;
167  if ( !RetValue2 )
168  continue;
169 
170  {
171  Pdr_Set_t * pCubeMin;
172  pCubeMin = Pdr_ManReduceClause( p, k, pCubeK );
173  if ( pCubeMin != NULL )
174  {
175 // Abc_Print( 1, "%d ", pCubeK->nLits - pCubeMin->nLits );
176  Pdr_SetDeref( pCubeK );
177  pCubeK = pCubeMin;
178  }
179  }
180 
181  // if it can be moved, add it to the next frame
182  Pdr_ManSolverAddClause( p, k+1, pCubeK );
183  // check if the clause subsumes others
184  Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK1, pCubeK1, i )
185  {
186  if ( !Pdr_SetContains( pCubeK1, pCubeK ) ) // pCubeK contains pCubeK1
187  continue;
188  Pdr_SetDeref( pCubeK1 );
189  Vec_PtrWriteEntry( vArrayK1, i, Vec_PtrEntryLast(vArrayK1) );
190  Vec_PtrPop(vArrayK1);
191  i--;
192  }
193  // add the last clause
194  Vec_PtrPush( vArrayK1, pCubeK );
195  Vec_PtrWriteEntry( vArrayK, j, Vec_PtrEntryLast(vArrayK) );
196  Vec_PtrPop(vArrayK);
197  j--;
198  }
199  if ( Vec_PtrSize(vArrayK) == 0 )
200  RetValue = 1;
201  }
202 
203  // clean up the last one
204  vArrayK = Vec_VecEntry( p->vClauses, kMax );
205  Vec_PtrSort( vArrayK, (int (*)(void))Pdr_SetCompare );
206  Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pCubeK, j )
207  {
208  // remove cubes in the same frame that are contained by pCubeK
209  Vec_PtrForEachEntryStart( Pdr_Set_t *, vArrayK, pTemp, m, j+1 )
210  {
211  if ( !Pdr_SetContains( pTemp, pCubeK ) ) // pCubeK contains pTemp
212  continue;
213 /*
214  Abc_Print( 1, "===\n" );
215  Pdr_SetPrint( stdout, pCubeK, Aig_ManRegNum(p->pAig), NULL );
216  Abc_Print( 1, "\n" );
217  Pdr_SetPrint( stdout, pTemp, Aig_ManRegNum(p->pAig), NULL );
218  Abc_Print( 1, "\n" );
219 */
220  Pdr_SetDeref( pTemp );
221  Vec_PtrWriteEntry( vArrayK, m, Vec_PtrEntryLast(vArrayK) );
222  Vec_PtrPop(vArrayK);
223  m--;
224  }
225  }
226  p->tPush += Abc_Clock() - clk;
227  return RetValue;
228 }
229 
230 /**Function*************************************************************
231 
232  Synopsis [Returns 1 if the clause is contained in higher clauses.]
233 
234  Description []
235 
236  SideEffects []
237 
238  SeeAlso []
239 
240 ***********************************************************************/
241 int Pdr_ManCheckContainment( Pdr_Man_t * p, int k, Pdr_Set_t * pSet )
242 {
243  Pdr_Set_t * pThis;
244  Vec_Ptr_t * vArrayK;
245  int i, j, kMax = Vec_PtrSize(p->vSolvers)-1;
246  Vec_VecForEachLevelStartStop( p->vClauses, vArrayK, i, k, kMax+1 )
247  Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pThis, j )
248  if ( Pdr_SetContains( pSet, pThis ) )
249  return 1;
250  return 0;
251 }
252 
253 
254 /**Function*************************************************************
255 
256  Synopsis [Sorts literals by priority.]
257 
258  Description []
259 
260  SideEffects []
261 
262  SeeAlso []
263 
264 ***********************************************************************/
265 int * Pdr_ManSortByPriority( Pdr_Man_t * p, Pdr_Set_t * pCube )
266 {
267  int * pPrios = Vec_IntArray(p->vPrio);
268  int * pArray = p->pOrder;
269  int temp, i, j, best_i, nSize = pCube->nLits;
270  // initialize variable order
271  for ( i = 0; i < nSize; i++ )
272  pArray[i] = i;
273  for ( i = 0; i < nSize-1; i++ )
274  {
275  best_i = i;
276  for ( j = i+1; j < nSize; j++ )
277 // if ( pArray[j] < pArray[best_i] )
278  if ( pPrios[pCube->Lits[pArray[j]]>>1] < pPrios[pCube->Lits[pArray[best_i]]>>1] )
279  best_i = j;
280  temp = pArray[i];
281  pArray[i] = pArray[best_i];
282  pArray[best_i] = temp;
283  }
284 /*
285  for ( i = 0; i < pCube->nLits; i++ )
286  Abc_Print( 1, "%2d : %5d %5d %5d\n", i, pArray[i], pCube->Lits[pArray[i]]>>1, pPrios[pCube->Lits[pArray[i]]>>1] );
287  Abc_Print( 1, "\n" );
288 */
289  return pArray;
290 }
291 
292 
293 /**Function*************************************************************
294 
295  Synopsis [Returns 1 if the state could be blocked.]
296 
297  Description []
298 
299  SideEffects []
300 
301  SeeAlso []
302 
303 ***********************************************************************/
304 int Pdr_ManGeneralize( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppPred, Pdr_Set_t ** ppCubeMin )
305 {
306  Pdr_Set_t * pCubeMin, * pCubeTmp = NULL;
307  int i, j, n, Lit, RetValue;
308  abctime clk = Abc_Clock();
309  int * pOrder;
310  // if there is no induction, return
311  *ppCubeMin = NULL;
312  RetValue = Pdr_ManCheckCube( p, k, pCube, ppPred, p->pPars->nConfLimit );
313  if ( RetValue == -1 )
314  return -1;
315  if ( RetValue == 0 )
316  {
317  p->tGeneral += Abc_Clock() - clk;
318  return 0;
319  }
320 
321  // reduce clause using assumptions
322 // pCubeMin = Pdr_SetDup( pCube );
323  pCubeMin = Pdr_ManReduceClause( p, k, pCube );
324  if ( pCubeMin == NULL )
325  pCubeMin = Pdr_SetDup( pCube );
326 
327  // perform generalization
328  if ( !p->pPars->fSkipGeneral )
329  {
330  // sort literals by their occurences
331  pOrder = Pdr_ManSortByPriority( p, pCubeMin );
332  // try removing literals
333  for ( j = 0; j < pCubeMin->nLits; j++ )
334  {
335  // use ordering
336  // i = j;
337  i = pOrder[j];
338 
339  // check init state
340  assert( pCubeMin->Lits[i] != -1 );
341  if ( Pdr_SetIsInit(pCubeMin, i) )
342  continue;
343  // try removing this literal
344  Lit = pCubeMin->Lits[i]; pCubeMin->Lits[i] = -1;
345  RetValue = Pdr_ManCheckCube( p, k, pCubeMin, NULL, p->pPars->nConfLimit );
346  if ( RetValue == -1 )
347  {
348  Pdr_SetDeref( pCubeMin );
349  return -1;
350  }
351  pCubeMin->Lits[i] = Lit;
352  if ( RetValue == 0 )
353  continue;
354 
355  // remove j-th entry
356  for ( n = j; n < pCubeMin->nLits-1; n++ )
357  pOrder[n] = pOrder[n+1];
358  j--;
359 
360  // success - update the cube
361  pCubeMin = Pdr_SetCreateFrom( pCubeTmp = pCubeMin, i );
362  Pdr_SetDeref( pCubeTmp );
363  assert( pCubeMin->nLits > 0 );
364  i--;
365 
366  // get the ordering by decreasing priorit
367  pOrder = Pdr_ManSortByPriority( p, pCubeMin );
368  }
369 
370  if ( p->pPars->fTwoRounds )
371  for ( j = 0; j < pCubeMin->nLits; j++ )
372  {
373  // use ordering
374  // i = j;
375  i = pOrder[j];
376 
377  // check init state
378  assert( pCubeMin->Lits[i] != -1 );
379  if ( Pdr_SetIsInit(pCubeMin, i) )
380  continue;
381  // try removing this literal
382  Lit = pCubeMin->Lits[i]; pCubeMin->Lits[i] = -1;
383  RetValue = Pdr_ManCheckCube( p, k, pCubeMin, NULL, p->pPars->nConfLimit );
384  if ( RetValue == -1 )
385  {
386  Pdr_SetDeref( pCubeMin );
387  return -1;
388  }
389  pCubeMin->Lits[i] = Lit;
390  if ( RetValue == 0 )
391  continue;
392 
393  // remove j-th entry
394  for ( n = j; n < pCubeMin->nLits-1; n++ )
395  pOrder[n] = pOrder[n+1];
396  j--;
397 
398  // success - update the cube
399  pCubeMin = Pdr_SetCreateFrom( pCubeTmp = pCubeMin, i );
400  Pdr_SetDeref( pCubeTmp );
401  assert( pCubeMin->nLits > 0 );
402  i--;
403 
404  // get the ordering by decreasing priorit
405  pOrder = Pdr_ManSortByPriority( p, pCubeMin );
406  }
407  }
408 
409  assert( ppCubeMin != NULL );
410  *ppCubeMin = pCubeMin;
411  p->tGeneral += Abc_Clock() - clk;
412  return 1;
413 }
414 
415 /**Function*************************************************************
416 
417  Synopsis [Returns 1 if the state could be blocked.]
418 
419  Description []
420 
421  SideEffects []
422 
423  SeeAlso []
424 
425 ***********************************************************************/
426 int Pdr_ManBlockCube( Pdr_Man_t * p, Pdr_Set_t * pCube )
427 {
428  Pdr_Obl_t * pThis;
429  Pdr_Set_t * pPred, * pCubeMin;
430  int i, k, RetValue, Prio = ABC_INFINITY, Counter = 0;
431  int kMax = Vec_PtrSize(p->vSolvers)-1;
432  abctime clk;
433  p->nBlocks++;
434  // create first proof obligation
435 // assert( p->pQueue == NULL );
436  pThis = Pdr_OblStart( kMax, Prio--, pCube, NULL ); // consume ref
437  Pdr_QueuePush( p, pThis );
438  // try to solve it recursively
439  while ( !Pdr_QueueIsEmpty(p) )
440  {
441  Counter++;
442  pThis = Pdr_QueueHead( p );
443  if ( pThis->iFrame == 0 )
444  return 0; // SAT
445  if ( pThis->iFrame > kMax ) // finished this level
446  return 1;
447  if ( p->nQueLim && p->nQueCur >= p->nQueLim )
448  {
449  p->nQueLim = p->nQueLim * 3 / 2;
450  Pdr_QueueStop( p );
451  return 1; // restart
452  }
453  pThis = Pdr_QueuePop( p );
454  assert( pThis->iFrame > 0 );
455  assert( !Pdr_SetIsInit(pThis->pState, -1) );
456  p->iUseFrame = Abc_MinInt( p->iUseFrame, pThis->iFrame );
457  clk = Abc_Clock();
458  if ( Pdr_ManCheckContainment( p, pThis->iFrame, pThis->pState ) )
459  {
460  p->tContain += Abc_Clock() - clk;
461  Pdr_OblDeref( pThis );
462  continue;
463  }
464  p->tContain += Abc_Clock() - clk;
465 
466  // check if the cube is already contained
467  RetValue = Pdr_ManCheckCubeCs( p, pThis->iFrame, pThis->pState );
468  if ( RetValue == -1 ) // resource limit is reached
469  {
470  Pdr_OblDeref( pThis );
471  return -1;
472  }
473  if ( RetValue ) // cube is blocked by clauses in this frame
474  {
475  Pdr_OblDeref( pThis );
476  continue;
477  }
478 
479  // check if the cube holds with relative induction
480  pCubeMin = NULL;
481  RetValue = Pdr_ManGeneralize( p, pThis->iFrame-1, pThis->pState, &pPred, &pCubeMin );
482  if ( RetValue == -1 ) // resource limit is reached
483  {
484  Pdr_OblDeref( pThis );
485  return -1;
486  }
487  if ( RetValue ) // cube is blocked inductively in this frame
488  {
489  assert( pCubeMin != NULL );
490  // k is the last frame where pCubeMin holds
491  k = pThis->iFrame;
492  // check other frames
493  assert( pPred == NULL );
494  for ( k = pThis->iFrame; k < kMax; k++ )
495  {
496  RetValue = Pdr_ManCheckCube( p, k, pCubeMin, NULL, 0 );
497  if ( RetValue == -1 )
498  {
499  Pdr_OblDeref( pThis );
500  return -1;
501  }
502  if ( !RetValue )
503  break;
504  }
505  // add new clause
506  if ( p->pPars->fVeryVerbose )
507  {
508  Abc_Print( 1, "Adding cube " );
509  Pdr_SetPrint( stdout, pCubeMin, Aig_ManRegNum(p->pAig), NULL );
510  Abc_Print( 1, " to frame %d.\n", k );
511  }
512  // set priority flops
513  for ( i = 0; i < pCubeMin->nLits; i++ )
514  {
515  assert( pCubeMin->Lits[i] >= 0 );
516  assert( (pCubeMin->Lits[i] / 2) < Aig_ManRegNum(p->pAig) );
517  Vec_IntAddToEntry( p->vPrio, pCubeMin->Lits[i] / 2, 1 );
518  }
519  Vec_VecPush( p->vClauses, k, pCubeMin ); // consume ref
520  p->nCubes++;
521  // add clause
522  for ( i = 1; i <= k; i++ )
523  Pdr_ManSolverAddClause( p, i, pCubeMin );
524  // schedule proof obligation
525  if ( (k < kMax || p->pPars->fReuseProofOblig) && !p->pPars->fShortest )
526  {
527  pThis->iFrame = k+1;
528  pThis->prio = Prio--;
529  Pdr_QueuePush( p, pThis );
530  }
531  else
532  {
533  Pdr_OblDeref( pThis );
534  }
535  }
536  else
537  {
538  assert( pCubeMin == NULL );
539  assert( pPred != NULL );
540  pThis->prio = Prio--;
541  Pdr_QueuePush( p, pThis );
542  pThis = Pdr_OblStart( pThis->iFrame-1, Prio--, pPred, Pdr_OblRef(pThis) );
543  Pdr_QueuePush( p, pThis );
544  }
545 
546  // check termination
547  if ( p->pPars->pFuncStop && p->pPars->pFuncStop(p->pPars->RunId) )
548  return -1;
549  if ( p->timeToStop && Abc_Clock() > p->timeToStop )
550  return -1;
551  if ( p->timeToStopOne && Abc_Clock() > p->timeToStopOne )
552  return -1;
553  if ( p->pPars->nTimeOutGap && p->pPars->timeLastSolved && Abc_Clock() > p->pPars->timeLastSolved + p->pPars->nTimeOutGap * CLOCKS_PER_SEC )
554  return -1;
555  }
556  return 1;
557 }
558 
559 /**Function*************************************************************
560 
561  Synopsis []
562 
563  Description []
564 
565  SideEffects []
566 
567  SeeAlso []
568 
569 ***********************************************************************/
570 int Pdr_ManSolveInt( Pdr_Man_t * p )
571 {
572  int fPrintClauses = 0;
573  Pdr_Set_t * pCube = NULL;
574  Aig_Obj_t * pObj;
575  Abc_Cex_t * pCexNew;
576  int k, RetValue = -1;
577  int nOutDigits = Abc_Base10Log( Saig_ManPoNum(p->pAig) );
578  abctime clkStart = Abc_Clock(), clkOne = 0;
579  p->timeToStop = p->pPars->nTimeOut ? p->pPars->nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0;
580  assert( Vec_PtrSize(p->vSolvers) == 0 );
581  // in the multi-output mode, mark trivial POs (those fed by const0) as solved
582  if ( p->pPars->fSolveAll )
583  Saig_ManForEachPo( p->pAig, pObj, k )
584  if ( Aig_ObjChild0(pObj) == Aig_ManConst0(p->pAig) )
585  {
586  Vec_IntWriteEntry( p->pPars->vOutMap, k, 1 ); // unsat
587  p->pPars->nProveOuts++;
588  if ( p->pPars->fUseBridge )
589  Gia_ManToBridgeResult( stdout, 1, NULL, k );
590  }
591  // create the first timeframe
592  p->pPars->timeLastSolved = Abc_Clock();
593  Pdr_ManCreateSolver( p, (k = 0) );
594  while ( 1 )
595  {
596  p->nFrames = k;
597  assert( k == Vec_PtrSize(p->vSolvers)-1 );
598  p->iUseFrame = Abc_MaxInt(k, 1);
599  Saig_ManForEachPo( p->pAig, pObj, p->iOutCur )
600  {
601  // skip disproved outputs
602  if ( p->vCexes && Vec_PtrEntry(p->vCexes, p->iOutCur) )
603  continue;
604  // skip output whose time has run out
605  if ( p->pTime4Outs && p->pTime4Outs[p->iOutCur] == 0 )
606  continue;
607  // check if the output is trivially solved
608  if ( Aig_ObjChild0(pObj) == Aig_ManConst0(p->pAig) )
609  continue;
610  // check if the output is trivially solved
611  if ( Aig_ObjChild0(pObj) == Aig_ManConst1(p->pAig) )
612  {
613  if ( !p->pPars->fSolveAll )
614  {
615  pCexNew = Abc_CexMakeTriv( Aig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), Saig_ManPoNum(p->pAig), k*Saig_ManPoNum(p->pAig)+p->iOutCur );
616  p->pAig->pSeqModel = pCexNew;
617  return 0; // SAT
618  }
619  pCexNew = (p->pPars->fUseBridge || p->pPars->fStoreCex) ? Abc_CexMakeTriv( Aig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), Saig_ManPoNum(p->pAig), k*Saig_ManPoNum(p->pAig)+p->iOutCur ) : (Abc_Cex_t *)(ABC_PTRINT_T)1;
620  p->pPars->nFailOuts++;
621  if ( p->pPars->vOutMap ) Vec_IntWriteEntry( p->pPars->vOutMap, p->iOutCur, 0 );
622  if ( !p->pPars->fNotVerbose )
623  Abc_Print( 1, "Output %*d was trivially asserted in frame %2d (solved %*d out of %*d outputs).\n",
624  nOutDigits, p->iOutCur, k, nOutDigits, p->pPars->nFailOuts, nOutDigits, Saig_ManPoNum(p->pAig) );
625  assert( Vec_PtrEntry(p->vCexes, p->iOutCur) == NULL );
626  if ( p->pPars->fUseBridge )
627  Gia_ManToBridgeResult( stdout, 0, pCexNew, pCexNew->iPo );
628  Vec_PtrWriteEntry( p->vCexes, p->iOutCur, pCexNew );
629  if ( p->pPars->pFuncOnFail && p->pPars->pFuncOnFail(p->iOutCur, p->pPars->fStoreCex ? (Abc_Cex_t *)Vec_PtrEntry(p->vCexes, p->iOutCur) : NULL) )
630  {
631  if ( p->pPars->fVerbose )
632  Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
633  if ( !p->pPars->fSilent )
634  Abc_Print( 1, "Quitting due to callback on fail.\n" );
635  p->pPars->iFrame = k;
636  return -1;
637  }
638  if ( p->pPars->nFailOuts + p->pPars->nDropOuts == Saig_ManPoNum(p->pAig) )
639  return p->pPars->nFailOuts ? 0 : -1; // SAT or UNDEC
640  p->pPars->timeLastSolved = Abc_Clock();
641  continue;
642  }
643  // try to solve this output
644  if ( p->pTime4Outs )
645  {
646  assert( p->pTime4Outs[p->iOutCur] > 0 );
647  clkOne = Abc_Clock();
648  p->timeToStopOne = p->pTime4Outs[p->iOutCur] + Abc_Clock();
649  }
650  while ( 1 )
651  {
652  if ( p->pPars->nTimeOutGap && p->pPars->timeLastSolved && Abc_Clock() > p->pPars->timeLastSolved + p->pPars->nTimeOutGap * CLOCKS_PER_SEC )
653  {
654  if ( p->pPars->fVerbose )
655  Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
656  if ( !p->pPars->fSilent )
657  Abc_Print( 1, "Reached gap timeout (%d seconds).\n", p->pPars->nTimeOutGap );
658  p->pPars->iFrame = k;
659  return -1;
660  }
661  RetValue = Pdr_ManCheckCube( p, k, NULL, &pCube, p->pPars->nConfLimit );
662  if ( RetValue == 1 )
663  break;
664  if ( RetValue == -1 )
665  {
666  if ( p->pPars->fVerbose )
667  Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
668  if ( p->timeToStop && Abc_Clock() > p->timeToStop )
669  Abc_Print( 1, "Reached timeout (%d seconds).\n", p->pPars->nTimeOut );
670  else if ( p->pPars->nTimeOutGap && p->pPars->timeLastSolved && Abc_Clock() > p->pPars->timeLastSolved + p->pPars->nTimeOutGap * CLOCKS_PER_SEC )
671  Abc_Print( 1, "Reached gap timeout (%d seconds).\n", p->pPars->nTimeOutGap );
672  else if ( p->timeToStopOne && Abc_Clock() > p->timeToStopOne )
673  {
674  Pdr_QueueClean( p );
675  pCube = NULL;
676  break; // keep solving
677  }
678  else if ( p->pPars->nConfLimit )
679  Abc_Print( 1, "Reached conflict limit (%d).\n", p->pPars->nConfLimit );
680  else if ( p->pPars->fVerbose )
681  Abc_Print( 1, "Computation cancelled by the callback.\n" );
682  p->pPars->iFrame = k;
683  return -1;
684  }
685  if ( RetValue == 0 )
686  {
687  RetValue = Pdr_ManBlockCube( p, pCube );
688  if ( RetValue == -1 )
689  {
690  if ( p->pPars->fVerbose )
691  Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
692  if ( p->timeToStop && Abc_Clock() > p->timeToStop )
693  Abc_Print( 1, "Reached timeout (%d seconds).\n", p->pPars->nTimeOut );
694  else if ( p->pPars->nTimeOutGap && p->pPars->timeLastSolved && Abc_Clock() > p->pPars->timeLastSolved + p->pPars->nTimeOutGap * CLOCKS_PER_SEC )
695  Abc_Print( 1, "Reached gap timeout (%d seconds).\n", p->pPars->nTimeOutGap );
696  else if ( p->timeToStopOne && Abc_Clock() > p->timeToStopOne )
697  {
698  Pdr_QueueClean( p );
699  pCube = NULL;
700  break; // keep solving
701  }
702  else if ( p->pPars->nConfLimit )
703  Abc_Print( 1, "Reached conflict limit (%d).\n", p->pPars->nConfLimit );
704  else if ( p->pPars->fVerbose )
705  Abc_Print( 1, "Computation cancelled by the callback.\n" );
706  p->pPars->iFrame = k;
707  return -1;
708  }
709  if ( RetValue == 0 )
710  {
711  if ( fPrintClauses )
712  {
713  Abc_Print( 1, "*** Clauses after frame %d:\n", k );
714  Pdr_ManPrintClauses( p, 0 );
715  }
716  if ( p->pPars->fVerbose )
717  Pdr_ManPrintProgress( p, !p->pPars->fSolveAll, Abc_Clock() - clkStart );
718  p->pPars->iFrame = k;
719  if ( !p->pPars->fSolveAll )
720  {
721  p->pAig->pSeqModel = Pdr_ManDeriveCex(p);
722  return 0; // SAT
723  }
724  p->pPars->nFailOuts++;
725  pCexNew = (p->pPars->fUseBridge || p->pPars->fStoreCex) ? Pdr_ManDeriveCex(p) : (Abc_Cex_t *)(ABC_PTRINT_T)1;
726  if ( p->pPars->vOutMap ) Vec_IntWriteEntry( p->pPars->vOutMap, p->iOutCur, 0 );
727  assert( Vec_PtrEntry(p->vCexes, p->iOutCur) == NULL );
728  if ( p->pPars->fUseBridge )
729  Gia_ManToBridgeResult( stdout, 0, pCexNew, pCexNew->iPo );
730  Vec_PtrWriteEntry( p->vCexes, p->iOutCur, pCexNew );
731  if ( p->pPars->pFuncOnFail && p->pPars->pFuncOnFail(p->iOutCur, p->pPars->fStoreCex ? (Abc_Cex_t *)Vec_PtrEntry(p->vCexes, p->iOutCur) : NULL) )
732  {
733  if ( p->pPars->fVerbose )
734  Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
735  if ( !p->pPars->fSilent )
736  Abc_Print( 1, "Quitting due to callback on fail.\n" );
737  p->pPars->iFrame = k;
738  return -1;
739  }
740  if ( !p->pPars->fNotVerbose )
741  Abc_Print( 1, "Output %*d was asserted in frame %2d (%2d) (solved %*d out of %*d outputs).\n",
742  nOutDigits, p->iOutCur, k, k, nOutDigits, p->pPars->nFailOuts, nOutDigits, Saig_ManPoNum(p->pAig) );
743  if ( p->pPars->nFailOuts == Saig_ManPoNum(p->pAig) )
744  return 0; // all SAT
745  Pdr_QueueClean( p );
746  pCube = NULL;
747  break; // keep solving
748  }
749  if ( p->pPars->fVerbose )
750  Pdr_ManPrintProgress( p, 0, Abc_Clock() - clkStart );
751  }
752  }
753  if ( p->pTime4Outs )
754  {
755  abctime timeSince = Abc_Clock() - clkOne;
756  assert( p->pTime4Outs[p->iOutCur] > 0 );
757  p->pTime4Outs[p->iOutCur] = (p->pTime4Outs[p->iOutCur] > timeSince) ? p->pTime4Outs[p->iOutCur] - timeSince : 0;
758  if ( p->pTime4Outs[p->iOutCur] == 0 && Vec_PtrEntry(p->vCexes, p->iOutCur) == NULL ) // undecided
759  {
760  p->pPars->nDropOuts++;
761  if ( p->pPars->vOutMap )
762  Vec_IntWriteEntry( p->pPars->vOutMap, p->iOutCur, -1 );
763  if ( !p->pPars->fNotVerbose )
764  Abc_Print( 1, "Timing out on output %*d.\n", nOutDigits, p->iOutCur );
765  }
766  p->timeToStopOne = 0;
767  }
768  }
769 
770  if ( p->pPars->fVerbose )
771  Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
772  // open a new timeframe
773  p->nQueLim = p->pPars->nRestLimit;
774  assert( pCube == NULL );
775  Pdr_ManSetPropertyOutput( p, k );
776  Pdr_ManCreateSolver( p, ++k );
777  if ( fPrintClauses )
778  {
779  Abc_Print( 1, "*** Clauses after frame %d:\n", k );
780  Pdr_ManPrintClauses( p, 0 );
781  }
782  // push clauses into this timeframe
783  RetValue = Pdr_ManPushClauses( p );
784  if ( RetValue == -1 )
785  {
786  if ( p->pPars->fVerbose )
787  Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
788  if ( !p->pPars->fSilent )
789  {
790  if ( p->timeToStop && Abc_Clock() > p->timeToStop )
791  Abc_Print( 1, "Reached timeout (%d seconds).\n", p->pPars->nTimeOut );
792  else
793  Abc_Print( 1, "Reached conflict limit (%d).\n", p->pPars->nConfLimit );
794  }
795  p->pPars->iFrame = k;
796  return -1;
797  }
798  if ( RetValue )
799  {
800  if ( p->pPars->fVerbose )
801  Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
802  if ( !p->pPars->fSilent )
803  Pdr_ManReportInvariant( p );
804  if ( !p->pPars->fSilent )
805  Pdr_ManVerifyInvariant( p );
806  p->pPars->iFrame = k;
807  // count the number of UNSAT outputs
808  p->pPars->nProveOuts = Saig_ManPoNum(p->pAig) - p->pPars->nFailOuts - p->pPars->nDropOuts;
809  // convert previously 'unknown' into 'unsat'
810  if ( p->pPars->vOutMap )
811  for ( k = 0; k < Saig_ManPoNum(p->pAig); k++ )
812  if ( Vec_IntEntry(p->pPars->vOutMap, k) == -2 ) // unknown
813  {
814  Vec_IntWriteEntry( p->pPars->vOutMap, k, 1 ); // unsat
815  if ( p->pPars->fUseBridge )
816  Gia_ManToBridgeResult( stdout, 1, NULL, k );
817  }
818  if ( p->pPars->nProveOuts == Saig_ManPoNum(p->pAig) )
819  return 1; // UNSAT
820  if ( p->pPars->nFailOuts > 0 )
821  return 0; // SAT
822  return -1;
823  }
824  if ( p->pPars->fVerbose )
825  Pdr_ManPrintProgress( p, 0, Abc_Clock() - clkStart );
826 
827  // check termination
828  if ( p->pPars->pFuncStop && p->pPars->pFuncStop(p->pPars->RunId) )
829  {
830  p->pPars->iFrame = k;
831  return -1;
832  }
833  if ( p->timeToStop && Abc_Clock() > p->timeToStop )
834  {
835  if ( fPrintClauses )
836  {
837  Abc_Print( 1, "*** Clauses after frame %d:\n", k );
838  Pdr_ManPrintClauses( p, 0 );
839  }
840  if ( p->pPars->fVerbose )
841  Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
842  if ( !p->pPars->fSilent )
843  Abc_Print( 1, "Reached timeout (%d seconds).\n", p->pPars->nTimeOut );
844  p->pPars->iFrame = k;
845  return -1;
846  }
847  if ( p->pPars->nTimeOutGap && p->pPars->timeLastSolved && Abc_Clock() > p->pPars->timeLastSolved + p->pPars->nTimeOutGap * CLOCKS_PER_SEC )
848  {
849  if ( fPrintClauses )
850  {
851  Abc_Print( 1, "*** Clauses after frame %d:\n", k );
852  Pdr_ManPrintClauses( p, 0 );
853  }
854  if ( p->pPars->fVerbose )
855  Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
856  if ( !p->pPars->fSilent )
857  Abc_Print( 1, "Reached gap timeout (%d seconds).\n", p->pPars->nTimeOutGap );
858  p->pPars->iFrame = k;
859  return -1;
860  }
861  if ( p->pPars->nFrameMax && k >= p->pPars->nFrameMax )
862  {
863  if ( p->pPars->fVerbose )
864  Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
865  if ( !p->pPars->fSilent )
866  Abc_Print( 1, "Reached limit on the number of timeframes (%d).\n", p->pPars->nFrameMax );
867  p->pPars->iFrame = k;
868  return -1;
869  }
870  }
871  assert( 0 );
872  return -1;
873 }
874 
875 /**Function*************************************************************
876 
877  Synopsis []
878 
879  Description []
880 
881  SideEffects []
882 
883  SeeAlso []
884 
885 ***********************************************************************/
886 int Pdr_ManSolve( Aig_Man_t * pAig, Pdr_Par_t * pPars )
887 {
888  Pdr_Man_t * p;
889  int k, RetValue;
890  abctime clk = Abc_Clock();
891  if ( pPars->nTimeOutOne && !pPars->fSolveAll )
892  pPars->nTimeOutOne = 0;
893  if ( pPars->nTimeOutOne && pPars->nTimeOut == 0 )
894  pPars->nTimeOut = pPars->nTimeOutOne * Saig_ManPoNum(pAig) / 1000 + (int)((pPars->nTimeOutOne * Saig_ManPoNum(pAig) % 1000) > 0);
895  if ( pPars->fVerbose )
896  {
897 // Abc_Print( 1, "Running PDR by Niklas Een (aka IC3 by Aaron Bradley) with these parameters:\n" );
898  Abc_Print( 1, "VarMax = %d. FrameMax = %d. QueMax = %d. TimeMax = %d. ",
899  pPars->nRecycle,
900  pPars->nFrameMax,
901  pPars->nRestLimit,
902  pPars->nTimeOut );
903  Abc_Print( 1, "MonoCNF = %s. SkipGen = %s. SolveAll = %s.\n",
904  pPars->fMonoCnf ? "yes" : "no",
905  pPars->fSkipGeneral ? "yes" : "no",
906  pPars->fSolveAll ? "yes" : "no" );
907  }
908  ABC_FREE( pAig->pSeqModel );
909  p = Pdr_ManStart( pAig, pPars, NULL );
910  RetValue = Pdr_ManSolveInt( p );
911  if ( RetValue == 0 )
912  assert( pAig->pSeqModel != NULL || p->vCexes != NULL );
913  if ( p->vCexes )
914  {
915  assert( p->pAig->vSeqModelVec == NULL );
916  p->pAig->vSeqModelVec = p->vCexes;
917  p->vCexes = NULL;
918  }
919  if ( p->pPars->fDumpInv )
920  Pdr_ManDumpClauses( p, (char *)"inv.pla", RetValue==1 );
921  p->tTotal += Abc_Clock() - clk;
922  Pdr_ManStop( p );
923  pPars->iFrame--;
924  // convert all -2 (unknown) entries into -1 (undec)
925  if ( pPars->vOutMap )
926  for ( k = 0; k < Saig_ManPoNum(pAig); k++ )
927  if ( Vec_IntEntry(pPars->vOutMap, k) == -2 ) // unknown
928  Vec_IntWriteEntry( pPars->vOutMap, k, -1 ); // undec
929  if ( pPars->fUseBridge )
930  Gia_ManToBridgeAbort( stdout, 7, (unsigned char *)"timeout" );
931  return RetValue;
932 }
933 
934 ////////////////////////////////////////////////////////////////////////
935 /// END OF FILE ///
936 ////////////////////////////////////////////////////////////////////////
937 
938 
939 ABC_NAMESPACE_IMPL_END
memset
char * memset()
Pdr_ManPrintProgress
void Pdr_ManPrintProgress(Pdr_Man_t *p, int fClose, abctime Time)
DECLARATIONS ///.
Definition: pdrInv.c:48
Vec_IntArray
static int * Vec_IntArray(Vec_Int_t *p)
Definition: vecInt.h:328
Pdr_ManCheckCube
int Pdr_ManCheckCube(Pdr_Man_t *p, int k, Pdr_Set_t *pCube, Pdr_Set_t **ppPred, int nConfLimit)
Definition: pdrSat.c:286
Pdr_Man_t_::pAig
Aig_Man_t * pAig
Definition: pdrInt.h:70
Pdr_Man_t_::vSolvers
Vec_Ptr_t * vSolvers
Definition: pdrInt.h:83
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
Pdr_Man_t_::tGeneral
abctime tGeneral
Definition: pdrInt.h:127
Pdr_SetCreateSubset
Pdr_Set_t * Pdr_SetCreateSubset(Pdr_Set_t *pSet, int *pLits, int nLits)
Definition: pdrUtil.c:132
Vec_VecPush
static void Vec_VecPush(Vec_Vec_t *p, int Level, void *Entry)
Definition: vecVec.h:456
Pdr_ManPushClauses
int Pdr_ManPushClauses(Pdr_Man_t *p)
Definition: pdrCore.c:135
Vec_PtrForEachEntryStart
#define Vec_PtrForEachEntryStart(Type, vVec, pEntry, i, Start)
Definition: vecPtr.h:57
Pdr_Man_t_::vPrio
Vec_Int_t * vPrio
Definition: pdrInt.h:90
Saig_ManPoNum
static int Saig_ManPoNum(Aig_Man_t *p)
Definition: saig.h:74
Pdr_Obl_t_::prio
int prio
Definition: pdrInt.h:58
Aig_Man_t
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition: aig.h:50
Aig_ObjChild0
static Aig_Obj_t * Aig_ObjChild0(Aig_Obj_t *pObj)
Definition: aig.h:310
Pdr_Man_t_::tContain
abctime tContain
Definition: pdrInt.h:130
Pdr_Man_t_::iUseFrame
int iUseFrame
Definition: pdrInt.h:88
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
Pdr_Obl_t_::pState
Pdr_Set_t * pState
Definition: pdrInt.h:60
Pdr_Par_t
typedefABC_NAMESPACE_HEADER_START struct Pdr_Par_t_ Pdr_Par_t
INCLUDES ///.
Definition: pdr.h:40
Pdr_ManLitsToCube
Vec_Int_t * Pdr_ManLitsToCube(Pdr_Man_t *p, int k, int *pArray, int nArray)
Definition: pdrSat.c:115
Pdr_Man_t_::iOutCur
int iOutCur
Definition: pdrInt.h:81
Pdr_ManSetDefaultParams
void Pdr_ManSetDefaultParams(Pdr_Par_t *pPars)
FUNCTION DEFINITIONS ///.
Definition: pdrCore.c:48
Pdr_ManSolve
int Pdr_ManSolve(Aig_Man_t *pAig, Pdr_Par_t *pPars)
Definition: pdrCore.c:886
Pdr_Obl_t_
Definition: pdrInt.h:55
Pdr_ManReportInvariant
void Pdr_ManReportInvariant(Pdr_Man_t *p)
Definition: pdrInv.c:385
Pdr_ManSolverAddClause
void Pdr_ManSolverAddClause(Pdr_Man_t *p, int k, Pdr_Set_t *pCube)
Definition: pdrSat.c:209
Vec_PtrSort
static void Vec_PtrSort(Vec_Ptr_t *p, int(*Vec_PtrSortCompare)()) ___unused
Definition: vecPtr.h:851
Pdr_ManGeneralize
int Pdr_ManGeneralize(Pdr_Man_t *p, int k, Pdr_Set_t *pCube, Pdr_Set_t **ppPred, Pdr_Set_t **ppCubeMin)
Definition: pdrCore.c:304
Pdr_SetDeref
void Pdr_SetDeref(Pdr_Set_t *p)
Definition: pdrUtil.c:208
Pdr_SetContains
int Pdr_SetContains(Pdr_Set_t *pOld, Pdr_Set_t *pNew)
Definition: pdrUtil.c:263
Vec_PtrPush
static void Vec_PtrPush(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:606
Aig_ManConst0
static Aig_Obj_t * Aig_ManConst0(Aig_Man_t *p)
Definition: aig.h:263
Pdr_Man_t_
Definition: pdrInt.h:66
Pdr_SetPrint
void Pdr_SetPrint(FILE *pFile, Pdr_Set_t *p, int nRegs, Vec_Int_t *vFlopCounts)
Definition: pdrUtil.c:225
Pdr_Man_t_::nCubes
int nCubes
Definition: pdrInt.h:107
Pdr_ManStart
Pdr_Man_t * Pdr_ManStart(Aig_Man_t *pAig, Pdr_Par_t *pPars, Vec_Int_t *vPrioInit)
DECLARATIONS ///.
Definition: pdrMan.c:45
Pdr_Man_t_::pOrder
int * pOrder
Definition: pdrInt.h:86
Pdr_ManDeriveCex
Abc_Cex_t * Pdr_ManDeriveCex(Pdr_Man_t *p)
FUNCTION DECLARATIONS ///.
Definition: pdrMan.c:189
Pdr_ManSetPropertyOutput
void Pdr_ManSetPropertyOutput(Pdr_Man_t *p, int k)
Definition: pdrSat.c:177
Abc_Clock
static abctime Abc_Clock()
Definition: abc_global.h:279
Pdr_Man_t_::pTime4Outs
abctime * pTime4Outs
Definition: pdrInt.h:103
Abc_MaxInt
static int Abc_MaxInt(int a, int b)
Definition: abc_global.h:238
Vec_PtrSize
static int Vec_PtrSize(Vec_Ptr_t *p)
Definition: vecPtr.h:295
Pdr_OblRef
Pdr_Obl_t * Pdr_OblRef(Pdr_Obl_t *p)
Definition: pdrUtil.c:420
Vec_PtrPop
static void * Vec_PtrPop(Vec_Ptr_t *p)
Definition: vecPtr.h:677
Pdr_Obl_t_::iFrame
int iFrame
Definition: pdrInt.h:57
sat_solver_final
static int sat_solver_final(sat_solver *s, int **ppArray)
Definition: satSolver.h:227
Pdr_QueuePush
void Pdr_QueuePush(Pdr_Man_t *p, Pdr_Obl_t *pObl)
Definition: pdrUtil.c:532
Abc_CexMakeTriv
Abc_Cex_t * Abc_CexMakeTriv(int nRegs, int nTruePis, int nTruePos, int iFrameOut)
Definition: utilCex.c:85
Vec_IntWriteEntry
static void Vec_IntWriteEntry(Vec_Int_t *p, int i, int Entry)
Definition: bblif.c:285
Abc_MinInt
static int Abc_MinInt(int a, int b)
Definition: abc_global.h:239
Pdr_QueuePop
Pdr_Obl_t * Pdr_QueuePop(Pdr_Man_t *p)
Definition: pdrUtil.c:491
Pdr_SetDup
Pdr_Set_t * Pdr_SetDup(Pdr_Set_t *pSet)
Definition: pdrUtil.c:166
Vec_PtrEntryLast
static void * Vec_PtrEntryLast(Vec_Ptr_t *p)
Definition: vecPtr.h:413
Pdr_ManSortByPriority
int * Pdr_ManSortByPriority(Pdr_Man_t *p, Pdr_Set_t *pCube)
Definition: pdrCore.c:265
Vec_IntAddToEntry
static void Vec_IntAddToEntry(Vec_Int_t *p, int i, int Addition)
Definition: bblif.c:302
Pdr_QueueStop
void Pdr_QueueStop(Pdr_Man_t *p)
Definition: pdrUtil.c:580
Pdr_ManSolveInt
int Pdr_ManSolveInt(Pdr_Man_t *p)
Definition: pdrCore.c:570
Vec_IntEntry
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
Abc_Base10Log
static int Abc_Base10Log(unsigned n)
Definition: abc_global.h:252
Pdr_Man_t_::pPars
Pdr_Par_t * pPars
Definition: pdrInt.h:69
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
if
if(last==0)
Definition: sparse_int.h:34
Pdr_ManVerifyInvariant
void Pdr_ManVerifyInvariant(Pdr_Man_t *p)
Definition: pdrInv.c:406
Pdr_Man_t_::nBlocks
int nBlocks
Definition: pdrInt.h:105
Pdr_Man_t_::nQueLim
int nQueLim
Definition: pdrInt.h:119
Pdr_QueueClean
void Pdr_QueueClean(Pdr_Man_t *p)
Definition: pdrUtil.c:513
Pdr_Set_t
typedefABC_NAMESPACE_HEADER_START struct Pdr_Set_t_ Pdr_Set_t
INCLUDES ///.
Definition: pdrInt.h:44
Aig_Obj_t_
Definition: aig.h:69
Vec_IntPush
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
Counter
static int Counter
Definition: extraBddMisc.c:1877
Pdr_Man_t_::vClauses
Vec_Vec_t * vClauses
Definition: pdrInt.h:84
Pdr_ManDumpClauses
void Pdr_ManDumpClauses(Pdr_Man_t *p, char *pFileName, int fProved)
Definition: pdrInv.c:313
Gia_ManToBridgeResult
ABC_NAMESPACE_IMPL_START int Gia_ManToBridgeResult(FILE *pFile, int Result, Abc_Cex_t *pCex, int iPoProved)
DECLARATIONS ///.
Definition: utilBridge.c:284
Pdr_OblDeref
void Pdr_OblDeref(Pdr_Obl_t *p)
Definition: pdrUtil.c:437
Pdr_ManBlockCube
int Pdr_ManBlockCube(Pdr_Man_t *p, Pdr_Set_t *pCube)
Definition: pdrCore.c:426
Abc_Print
static void Abc_Print(int level, const char *format,...)
Definition: abc_global.h:313
Vec_PtrWriteEntry
static void Vec_PtrWriteEntry(Vec_Ptr_t *p, int i, void *Entry)
Definition: vecPtr.h:396
Pdr_SetCompare
int Pdr_SetCompare(Pdr_Set_t **pp1, Pdr_Set_t **pp2)
Definition: pdrUtil.c:366
Aig_ManConst1
static Aig_Obj_t * Aig_ManConst1(Aig_Man_t *p)
Definition: aig.h:264
Pdr_Man_t_::timeToStop
abctime timeToStop
Definition: pdrInt.h:121
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
Pdr_ManSolver
static sat_solver * Pdr_ManSolver(Pdr_Man_t *p, int k)
MACRO DEFINITIONS ///.
Definition: pdrInt.h:139
Pdr_ManCheckContainment
int Pdr_ManCheckContainment(Pdr_Man_t *p, int k, Pdr_Set_t *pSet)
Definition: pdrCore.c:241
Pdr_ManReduceClause
Pdr_Set_t * Pdr_ManReduceClause(Pdr_Man_t *p, int k, Pdr_Set_t *pCube)
Definition: pdrCore.c:82
Aig_ManRegNum
static int Aig_ManRegNum(Aig_Man_t *p)
Definition: aig.h:260
Pdr_Man_t_::tTotal
abctime tTotal
Definition: pdrInt.h:132
Vec_IntSize
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
Pdr_ManPrintClauses
void Pdr_ManPrintClauses(Pdr_Man_t *p, int kStart)
Definition: pdrInv.c:205
Pdr_Man_t_::timeToStopOne
abctime timeToStopOne
Definition: pdrInt.h:122
lit_sign
static int lit_sign(lit l)
Definition: satVec.h:146
Saig_ManPiNum
static int Saig_ManPiNum(Aig_Man_t *p)
MACRO DEFINITIONS ///.
Definition: saig.h:73
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
Pdr_ManStop
void Pdr_ManStop(Pdr_Man_t *p)
Definition: pdrMan.c:106
Gia_ManToBridgeAbort
int Gia_ManToBridgeAbort(FILE *pFile, int Size, unsigned char *pBuffer)
Definition: utilBridge.c:175
Pdr_ManCreateSolver
sat_solver * Pdr_ManCreateSolver(Pdr_Man_t *p, int k)
DECLARATIONS ///.
Definition: pdrSat.c:45
Vec_VecForEachLevelStartStop
#define Vec_VecForEachLevelStartStop(vGlob, vVec, i, LevelStart, LevelStop)
Definition: vecVec.h:61
Pdr_Man_t_::nFrames
int nFrames
Definition: pdrInt.h:112
Pdr_Man_t_::vCexes
Vec_Ptr_t * vCexes
Definition: pdrInt.h:82
Pdr_QueueHead
Pdr_Obl_t * Pdr_QueueHead(Pdr_Man_t *p)
Definition: pdrUtil.c:475
ABC_INFINITY
#define ABC_INFINITY
MACRO DEFINITIONS ///.
Definition: abc_global.h:216
Saig_ManForEachPo
#define Saig_ManForEachPo(p, pObj, i)
Definition: saig.h:93
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
Pdr_OblStart
Pdr_Obl_t * Pdr_OblStart(int k, int prio, Pdr_Set_t *pState, Pdr_Obl_t *pNext)
Definition: pdrUtil.c:396
Vec_VecEntry
static Vec_Ptr_t * Vec_VecEntry(Vec_Vec_t *p, int i)
Definition: vecVec.h:271
Pdr_Man_t_::nQueCur
int nQueCur
Definition: pdrInt.h:117
Vec_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition: vecPtr.h:55
Pdr_Man_t_::tPush
abctime tPush
Definition: pdrInt.h:128
abctime
ABC_INT64_T abctime
Definition: abc_global.h:278
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
Pdr_ManCheckCubeCs
int Pdr_ManCheckCubeCs(Pdr_Man_t *p, int k, Pdr_Set_t *pCube)
Definition: pdrSat.c:258
Pdr_SetIsInit
int Pdr_SetIsInit(Pdr_Set_t *p, int iRemove)
Definition: pdrUtil.c:341
Pdr_QueueIsEmpty
int Pdr_QueueIsEmpty(Pdr_Man_t *p)
Definition: pdrUtil.c:459
Pdr_SetCreateFrom
Pdr_Set_t * Pdr_SetCreateFrom(Pdr_Set_t *pSet, int iRemove)
Definition: pdrUtil.c:98